# Lean series 04: Linperm

### Every hero needs a nemesis

While `perm` has been a crucial ingredient in our previous victory against malevolent `length_sum_perm_of_B`, it is still but a young padawan and must be trained properly to reach its full potential. And the best way to do that, of course, is introducing a formidable enemy:

``````theorem perm_training_ground
(Bacb : B a c b)
(Bcbe : B c b e)
(Bbed : B b e d)
(h1 : length b a = length d b)
(h2 : length e b + length a c = length d e + length c b)
(h3 : length a c + length d e = length e c) :
length a c = length b c ∧
length b e = length c b ∧
length e b = length e d := by sorry
``````

Yikes. Even the point order is unsettling. Let's not get intimidated and try to analyze the situation. The goal only talks about lengths, but we need to get the information about betweenness into play. Invoking `length_sum_of_B` seems like a promising start:

``````have accb := length_sum_of_B Bacb
have beed := length_sum_of_B Bbed
have cbbe := length_sum_of_B Bcbe
``````

### Growing `perm`'s boundaries

Now it would be nice to substitute these new equations into the original hypotheses, but unfortunately all of them have swapped arguments. Sounds like a time for `perm` to shine! But…it can only handle permutations in the goal, not in the hypotheses. Luckily, `conv` can also target a hypothesis, so let's fix that:

``````namespace Lean.Elab.Tactic

syntax "perm" ("at " ident)? : tactic
macro_rules
| `(tactic| perm) =>`(tactic|
(try conv in (occs := *) length _ _ => all_goals length_nf))
| `(tactic| perm at \$name) =>`(tactic|
(try conv at \$name in (occs := *) length _ _ => all_goals length_nf))

end Lean.Elab.Tactic
``````

This was relatively straightforward — we just replaced `macro` with `syntax` and `macro_rules`, extending the syntax with pattern matching (`ident` will be matched to a hypothesis name and `?` means that `"at " ident` is optional). Calling `perm; perm at h1; perm at h2; perm at h3` now puts all the arguments in the right order. But it seems a little awkward. Is this the best you can do, `perm`?

``````syntax "perm" ("at " ident)? ("at *")? : tactic
macro_rules
| `(tactic| perm) =>`(tactic|
(try conv in (occs := *) length _ _ => all_goals length_nf))
| `(tactic| perm at \$name) =>`(tactic|
(try conv at \$name in (occs := *) length _ _ => all_goals length_nf))
elab_rules : tactic
| `(tactic| perm at *) => withMainContext do
evalTactic (← `(tactic| perm))
for ldecl in ← getLCtx do
if !ldecl.isImplementationDetail then
evalTactic (← `(tactic| perm at \$name))
``````

Now we're talking! `elab_rules` allows us to go deeper, invoking `perm` first by itself and that at every relevant hypothesis. (You might object this is a little wasteful, but in practice it's not an issue). Note that we also had to extend the syntax.

Let's continue the proof (`←` refers to the symmetric version, so `rw [← abbc] at h1` replaces the right hand side of `abbc` at `h1` by the left hand side):

``````perm at *
rw [← accb] at h1
rw [← beed] at h1
rw [← cbbe] at h3
``````

The infoview is now cluttered with obsolete assumptions, so let's `clear` it a bit: `clear Bacb Bcbe Bbed accb beed cbbe`. Now it reads:

``````i : incidence_geometry
a b c d e: point
h1 : length a b + length b c = length c d + length d e
h2 : length c d + length a b = length d e + length b c
h3 : length a b + length d e = length b c + length c d
⊢ length a b = length b c ∧ length c d = length b c ∧ length c d = length d e
``````

What is not so `clear`, however, is how to proceed. Sure, we can call our pal `splitAll` to get three subgoals, but what's next?

### The holy grail of linear algebra

This is an ideal place for getting stuck. We could try various things — subtracting terms from both sides of the equation and them substituting them elsewhere (perhaps in calc mode), using commutativity,…or we can just use `linarith`. Isn't that cheating? Maybe a little, but this a powerful finishing tactic makes our live much easier. It closes the goal if it follows from linear (in)equalities in the context (or else fails), which is exactly case. Let's see it in action:

``````theorem perm_training_ground
(Bacb : B a c b)
(Bcbe : B c b e)
(Bbed : B b e d)
(h1 : length b a = length d b)
(h2 : length e b + length a c = length d e + length c b)
(h3 : length a c + length d e = length e c) :
length a c = length b c ∧
length b e = length c b ∧
length e b = length e d := by
have accb := length_sum_of_B Bacb
have beed := length_sum_of_B Bbed
have cbbe := length_sum_of_B Bcbe
perm at *
rw [← accb] at h1
rw [← beed] at h1
rw [← cbbe] at h3
clear Bacb Bcbe Bbed accb beed cbbe
splitAll
repeat linarith
``````

Tada! The big bad boss has been conquered. And yet…it still feels like the proof could be more efficient. `linarith` has a nice feature — `linarith[H1, H2,...]` basically acts as `have := H1; have := H2; linarith` without polluting the infoview. So maybe we could write `linarith[length_sum_of_B Bacb, length_sum_of_B Bbed, length_sum_of_B Bcbe]` and get rid of the `have`'s and `rw`'s? Normally this would work well, but in this case, the hypotheses added inside `linarith` would have the wrong order, and there is no opportunity to call `perm` on them, as everything happens at once. What to do?

### A match made in heaven

Sometimes, a hero must make sacrifices and become a part of a greater whole. And what's better than both `perm` and `linarith`? You guessed it — their fusion, `linperm`! We just need to augment `perm at *` with `linarith`'s `[]` capabilities and finish with `linarith`. First, we need to mimic the `have` behavior:

``````open Lean Meta in
def haveExpr (n:Name) (h:Expr) :=
withMainContext do
let t ← inferType h
liftMetaTactic fun mvarId => do
let mvarIdNew ← Lean.MVarId.assert mvarId n t h
let (_, mvarIdNew) ← Lean.MVarId.intro1P mvarIdNew
return [mvarIdNew]
``````

Now we can use `haveExpr` inside an auxilliary `havePerms` tactic, which parses its arguments in brackets, adds them to the context as `this`, and runs `perm` on them:

``````open Parser Tactic Syntax

syntax "havePerms" (" [" term,* "]")? : tactic
elab_rules : tactic
| `(tactic| havePerms \$[[\$args,*]]?) => withMainContext do
let hyps := (← ((args.map (TSepArray.getElems)).getD {}).mapM
(elabTerm ·.raw none)).toList
for h in hyps do
haveExpr "this" h
evalTactic (← `(tactic| perm at \$(mkIdent "this")))
``````

It remains to extend `perm`'s syntax again by replacing

``````syntax "perm"("at " ident)? ("at *")? : tactic
``````

with

``````syntax "perm" (" [" term,* "]")? ("at " ident)? ("at *")? : tactic
``````

and let it use `havePerms` internally:

``````macro_rules
| `(tactic| perm [\$args,*] ) => `(tactic| havePerms [\$args,*])
``````

Finally, let's define `linperm` by bundling it all together:

``````syntax "linperm " ("[" term,* "]")? : tactic
macro_rules
| `(tactic| linperm) => `(tactic| perm at *; linarith)
| `(tactic| linperm [\$args,*] ) =>
`(tactic| perm at *; havePerms [\$args,*]; linarith)
``````

Phew. After all this hard work, it's time the harvest the fruit and watch `linperm` in its moment of glory. Oh, how far has it come!

``````theorem perm_training_ground'
(Bacb : B a c b)
(Bcbe : B c b e)
(Bbed : B b e d)
(h1 : length b a = length d b)
(h2 : length e b + length a c = length d e + length c b)
(h3 : length a c + length d e = length e c) :
length a c = length b c ∧
length b e = length c b ∧
length e b = length e d := by
splitAll
repeat linperm [length_sum_of_B Bacb, length_sum_of_B Bcbe, length_sum_of_B Bbed]
``````

There are still many other ways `(lin)perm` could keep growing, but unlike lines in Euclidean geometry, stories must come to an end. So get out your handkerchiefs and say your goodbyes to our friend `(lin)perm`, at least for now. I hope its journey through the tactic-writing world inspired you and you'll be able to level up your skills in the same way it did.

If you have any suggestions for improving this blog post, please let me know.