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
let name := mkIdent ldecl.userName
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.