编辑“︁Lean高级证明技术 Lean证明搜索”︁（章节）

== 高级证明搜索技术 ==
对于更复杂的目标，Lean允许用户结合高阶策略和元编程来实现深度证明搜索。

=== 使用 <code>solve_by_elim</code> ===
该策略通过回溯搜索可能的证明路径：

<syntaxhighlight lang="lean">
example (P Q R : Prop) : (P → Q) → (Q → R) → P → R := by
  solve_by_elim -- 自动应用蕴含规则
</syntaxhighlight>

=== 自定义策略库 ===
用户可以通过定义新的策略扩展证明搜索的能力：

<syntaxhighlight lang="lean">
macro "my_auto" : tactic =>
  `(tactic| (simp; apply?; try assumption))

example (x : Nat) : x = x := by
  my_auto -- 自定义策略组合
</syntaxhighlight>