### 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.*