14.8. 定制策略
策略是语法类别 tactic 中的产品。
给定策略的语法，策略解释器负责执行策略单子 TacticM 中的操作，它是 Lean 的术语精化器的包装器，用于跟踪执行所需的附加状态策略。
自定义策略包含 tactic 类别的扩展以及：
-
将新语法转换为现有语法的 宏，或者
-
执行
TacticM操作以实现策略的精化器。
14.8.1. 策略宏
定义新策略的最简单方法是将 宏 扩展为已存在的策略。 宏展开与策略交错执行。 策略解释器首先在解释策略宏之前对其进行扩展。 由于策略宏在运行策略脚本之前未完全展开，因此它们可以使用递归；只要宏语法的递归出现位于可执行的策略之下，就不会有无限的扩展链。
Recursive tactic macro
与其他 Lean 宏一样，策略宏是 卫生。 对全局名称的引用在定义宏时解析，并且策略宏引入的名称无法从其调用站点捕获名称。
定义策略宏时，指定匹配或构造的语法适用于语法类别 tactic 非常重要。
否则，语法将被解释为术语的语法，这将与策略匹配或构造不正确的 AST。
14.8.1.1. 可扩展策略宏
由于宏展开可能会失败，因此 多个宏可以匹配相同的语法，从而允许回溯。
策略宏更进一步：即使策略宏扩展成功，如果在解释时扩展失败，策略解释器将尝试下一次扩展。
这用于使许多 Lean 的内置策略可扩展 — 可以通过添加 Lean.Parser.Command.macro_rules : commandmacro_rules 声明将新行为添加到策略。
Extending trivial
trivial 被许多其他策略用于快速调度不值得打扰用户的子目标，旨在通过新的宏扩展进行扩展。
Lean 的默认 trivial 无法解决 IsEmpty [] 目标：
def IsEmpty (xs : List α) : Prop :=
¬ xs ≠ []
example (α : Type u) : IsEmpty (α := α) [] := α:Type u⊢ IsEmpty [] α:Type u⊢ IsEmpty []
该错误消息是 trivial 最后尝试 assumption 的产物。
添加另一个扩展允许 trivial 实现以下目标：
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
当扩展语法的任何部分出现故障时，宏展开可能会导致回溯。
可以通过在单独的 Lean.Parser.Command.macro_rules : commandmacro_rules 声明中提供多个扩展来定义 first 的中缀版本：
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! 🐙
需要多个 Lean.Parser.Command.macro_rules : commandmacro_rules 声明，因为每个声明都定义一个模式匹配函数，该函数始终采用第一个匹配替代项。
回溯是按 Lean.Parser.Command.macro_rules : commandmacro_rules 声明的粒度进行的，而不是按个别情况进行。