Lean series 03: Tactics

Automating low-level tasks

Not even the tricks from the previous post were enough to prove length_sum_perm_of_B. While we could manually split the conjunctions and prove every part separately, it wouldn't be a good use of our time. Instead, we can see that by applying the

(length_symm : ∀ (a b : point), length a b = length b a)

axiom at the right places, the goal easily follows from the lemma len_pos_of_neq and the axiom length_sum_of_B. But how do we know when to apply length_symm to an expression and when to leave it alone?

Enter metaprogramming

Instead of having to provide explicit proof terms, Lean allows us to use tactics. These have different purposes, but in general allow us to partially automate the process and think on a higher level, getting the "obvious" stuff out of the way. In fact, we've already seen a few tactics the last time, namely have, constructor, exact, rw, and sorry. Tactics can be chained together and extended, and we can also create our own — which is exactly what we're gonna do!

If we just want to bundle several tactics together in a single one, macros are enough — that's the easier variant. But when we actually need to access the internal state, we need to get our hands dirty and use elabs (short for elaborations). Brace yourselves! (And just like last time, you can follow along.)

Normal form for length

Let's start with a simpler goal — given a single length expression, put it in a normal form. In other words, both length a b and length b a should result in the same output after using the tactic. Lexicographic ordering of the arguments is one natural choice.

namespace Lean.Elab.Tactic

def getNthArgName (tgt : Expr) (n : Nat) : MetaM Name :=
  do
    let some id := Lean.Expr.fvarId? (Lean.Expr.getArg! tgt n) | throwError "argument {n} is not a free variable"
    id.getUserName

elab "length_nf" : conv => withMainContext do
  let tgt ← instantiateMVars (← Conv.getLhs)
  let n1 ← getNthArgName tgt 1
  let n2 ← getNthArgName tgt 2
  if n2.lt n1 then
    evalTactic (← `(tactic| rw [@length_symm _ _] ))

end Lean.Elab.Tactic

Indeed, this does it! We just defined a new tactic length_nf usable in conv mode. It accesses the user names of the arguments, and then swaps them if the second one is lexicographically smaller than the first one. Note the use of _ _ — the correct arguments are automatically substituted. The tactic lives inside the Lean.Elab.Tactic namespace and for good form, we should put all following tactics there (i.e., before the end line) as well.

(These lines might not look like much, but without a tutorial like this one, it took me a few weeks to figure them out. Luckily, I persisted, as I had no clue what I was getting into…)

Extending to all expressions

Now we need to apply length_nf to all occurrences of length in a given expression, no matter how deeply nested they are. This seems daunting, but the conv mode saves the day by letting us target expressions with surgical precision! We can combine it with the tactic all_goals, which tries to dispatch all goals with what follows in one fell swoop, and try, which ensures that the following tactic never fails. Pattern matching now gives rise to the brand new perm tactic:

macro "perm" : tactic =>
  `(tactic| try conv in (occs := *) length _ _ => all_goals length_nf)

Calling perm while in tactic mode will now normalize all length expressions in the goal. Try it out! There's something immensely satisfying about seeing the variables switch places in the infoview. (In the original project, perm is even more powerful, as it normalizes all symmetric primitives. For length, we only have two options (swap or not), but for triangles, perm saves us from manually choosing from 3! separate permutations. Gotta love triangles!)

Splitting the conjunctions

But we are not done yet. To split the conjunctions in length_sum_perm_of_B, we could just call constructor (followed by a tactic closing the subgoal) thirteen times, but by now we know better! There is a repeat tactic which repeatedly applies a given tactic until it fails. Unfortunately, repeat constructor doesn't help, because after the first application, the new first goal will not be splittable anymore. However, the cousin repeat' recurses on all newly generated subgoals, which is exactly what we need. Splitting large goals sounds useful in general (even in everyday life), so we might as well get more practice and create our own splitAll tactic:

macro "splitAll" : tactic => `(tactic | repeat' constructor)

(Note the use of ; — it allow us to chain tactics on a single line. By the way, we could also just use the Mathlib tactic split_ands with a very similar effect.)

Everything falls into place

Now grab some healthy alternative to popcorn and behold:

theorem length_sum_perm_of_B (Babc : B a b c) :
      0 < length a b ∧ 0 < length b a ∧ 0 < length b c ∧
      0 < length c b ∧ 0 < length a c ∧ 0 < length c a ∧
      length a b + length b c = length a c ∧
      length b a + length b c = length a c ∧
      length b a + length c b = length a c ∧
      length b a + length b c = length c a ∧
      length b a + length c b = length c a ∧
      length a b + length c b = length a c ∧
      length a b + length b c = length c a ∧
      length a b + length c b = length c a
   := by
  perm
  splitAll
  all_goals
  try exact len_pos_of_neq $ ne_12_of_B Babc
  try exact len_pos_of_neq $ ne_23_of_B Babc
  try exact len_pos_of_neq $ ne_13_of_B Babc
  try exact length_sum_of_B Babc

Feels pretty good, doesn't it?

It turns out that this version of perm still isn't strong enough for many practical purposes. So in the next blog post, we will feed it steroids…

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

Back