Tactics as shortcuts
We have seen how to write custom syntax and a macro that parses that syntax in the recipe Writing a Macro. In this recipe, we will see how to use macro to write a custom tactic. We will start with a simple example of a tactic that applies the same theorem repeatedly until it can no longer be applied, and then we will generalize it to a tactic that takes two theorems as arguments and applies them in a specific order.
Tactic to prove natural number inequalities
We start with an example of a routine proof we might write to prove 2 ≤ 6.
Often the same or similar patterns of tactics work for a range of problems. To avoid having to repeatedly type the sequence we can create a tactic using a macro for the pattern. More importantly, we can give the tactic a descriptive name that is easier to remember and understand.
We start with an example of a routine proof, namely 2 ≤ 6.
example : 2 ≤ 6 := ⊢ 2 ≤ 6
⊢ 2 ≤ 5
⊢ 2 ≤ 4
⊢ 2 ≤ 3
⊢ 2 ≤ 2
All goals completed! 🐙
This approach is highly repetitive. We can simplify it by using the repeat and first tactic combinators.
example : 2 ≤ 6 := ⊢ 2 ≤ 6
repeat (first| All goals completed! 🐙 |
⊢ 2 ≤ 2)
To reduce this to a single, readable line, we can define a custom tactic using a macro.
macro "nat_le" : tactic =>
`(tactic| repeat(first| apply Nat.le_refl |
apply Nat.le_succ_of_le))
example: 2 ≤ 6 := ⊢ 2 ≤ 6 All goals completed! 🐙
Tactic to repeat applications of theorems
While nat_le works for our specific case, we can make it far more useful by abstracting over the theorems. Let's construct a parametrized macro that accepts two theorems as arguments. It will repeatedly attempt to apply the second theorem (t₂) to close the goal, and whenever that fails, it makes progress by applying the first theorem (t₁).
Here is how we construct such a tactic:
macro "repeat_apply" t₁:term "then" t₂:term : tactic =>
`(tactic| repeat(first| apply $t₂| apply $t₁ ))
example : 10 ≤ 12 := ⊢ 10 ≤ 12
All goals completed! 🐙