13.8. Custom Tactics
Tactics are productions in the syntax category tactic.
Given the syntax of a tactic, the tactic interpreter is responsible for carrying out actions in the tactic monad TacticM, which is a wrapper around Lean's term elaborator that keeps track of the additional state needed to execute tactics.
A custom tactic consists of an extension to the tactic category along with either:
-
a macro that translates the new syntax into existing syntax, or
-
an elaborator that carries out
TacticMactions to implement the tactic.
13.8.1. Tactic Macros
The easiest way to define a new tactic is as a macro that expands into already-existing tactics. Macro expansion is interleaved with tactic execution. The tactic interpreter first expands tactic macros just before they are to be interpreted. Because tactic macros are not fully expanded prior to running a tactic script, they can use recursion; as long as the recursive occurrence of the macro syntax is beneath a tactic that can be executed, there will not be an infinite chain of expansion.
Recursive tactic macro
This recursive implementation of a tactic akin to repeat is defined via macro expansion.
When the argument $t fails, the recursive occurrence of rep is never invoked, and is thus never macro expanded.
syntax "rep" tactic : tactic
macro_rules
| `(tactic|rep $t) =>
`(tactic|
first
| $t; rep $t
| skip)
example : 0 ≤ 4 := ⊢ 0 ≤ 4
rep (⊢ Nat.le 0 0)
All goals completed! 🐙
Like other Lean macros, tactic macros are hygienic. References to global names are resolved when the macro is defined, and names introduced by the tactic macro cannot capture names from its invocation site.
When defining a tactic macro, it's important to specify that the syntax being matched or constructed is for the syntax category tactic.
Otherwise, the syntax will be interpreted as that of a term, which will match against or construct an incorrect AST for tactics.
13.8.1.1. Extensible Tactic Macros
Because macro expansion can fail, multiple macros can match the same syntax, allowing backtracking.
Tactic macros take this further: even if a tactic macro expands successfully, if the expansion fails when interpreted, the tactic interpreter will attempt the next expansion.
This is used to make a number of Lean's built-in tactics extensible—new behavior can be added to a tactic by adding a Lean.Parser.Command.macro_rules : commandmacro_rules declaration.
Extending trivial
The trivial, which is used by many other tactics to quickly dispatch subgoals that are not worth bothering the user with, is designed to be extended through new macro expansions.
Lean's default trivial can't solve IsEmpty [] goals:
def IsEmpty (xs : List α) : Prop :=
¬ xs ≠ []
example (α : Type u) : IsEmpty (α := α) [] := α:Type u⊢ IsEmpty [] α:Type u⊢ IsEmpty []
The error message is an artifact of trivial trying assumption last.
Adding another expansion allows trivial to take care of these goals:
def emptyIsEmpty : IsEmpty (α := α) [] := α:Type u_1⊢ IsEmpty [] All goals completed! 🐙
macro_rules | `(tactic|trivial) => `(tactic|exact emptyIsEmpty)
example (α : Type u) : IsEmpty (α := α) [] := α:Type u⊢ IsEmpty []
All goals completed! 🐙
Expansion Backtracking
Macro expansion can induce backtracking when the failure arises from any part of the expanded syntax.
An infix version of first can be defined by providing multiple expansions in separate Lean.Parser.Command.macro_rules : commandmacro_rules declarations:
syntax tactic "<|||>" tactic : tactic
macro_rules
| `(tactic|$t1 <|||> $t2) => pure t1
macro_rules
| `(tactic|$t1 <|||> $t2) => pure t2
example : 2 = 2 := ⊢ 2 = 2
All goals completed! 🐙 <|||> apply And.intro
example : 2 = 2 := ⊢ 2 = 2
apply And.intro <|||> All goals completed! 🐙
Multiple Lean.Parser.Command.macro_rules : commandmacro_rules declarations are needed because each defines a pattern-matching function that will always take the first matching alternative.
Backtracking is at the granularity of Lean.Parser.Command.macro_rules : commandmacro_rules declarations, not their individual cases.