repeat_apply tactic
We start with an example of a routine proof we might do. To prove 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! 🐙
While this works for our specific case, we can make it far more useful by abstracting the theorems. Let's construct a parameterized 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! 🐙