编辑“︁Lean高级证明技术 Lean证明搜索”︁

{{DISPLAYTITLE:Lean高级证明技术：Lean证明搜索}}

'''Lean证明搜索'''是Lean定理证明器中的一种自动化工具，它通过内置的策略和启发式方法帮助用户完成数学证明的构造。本教程将详细介绍Lean证明搜索的工作原理、常用策略及其实际应用。

== 概述 ==
在Lean中，'''证明搜索'''（Proof Search）是指系统自动尝试寻找满足当前目标的证明过程。它通过组合应用预定义的证明策略（如<code>simp</code>、<code>rw</code>、<code>apply</code>等）来推导出结论，而无需用户手动编写完整的证明步骤。证明搜索特别适用于以下场景：
* 目标简单且可通过标准化策略解决。
* 用户希望快速验证某个中间步骤的正确性。
* 复杂的证明中需要自动化辅助以减少手动输入。

== 基本证明搜索策略 ==
Lean提供了多种策略用于自动化证明搜索，以下是几种核心方法：

=== <code>simp</code> 策略 ===
<code>simp</code>是Lean中最常用的自动化策略之一，它通过应用预定义的简化规则（如定义展开、等式重写）来简化目标。

<syntaxhighlight lang="lean">
example : ∀ (n : Nat), n + 0 = n := by
  simp -- 自动应用Nat.add_zero规则
</syntaxhighlight>

输出：
<pre>
Proof completed!
</pre>

=== <code>auto</code> 策略 ===
<code>auto</code>是一个更强大的证明搜索策略，它会尝试组合多种策略（如<code>simp</code>、<code>apply</code>、<code>intro</code>）来求解目标。

<syntaxhighlight lang="lean">
example (P Q : Prop) : P ∧ Q → Q ∧ P := by
  auto -- 自动处理合取逻辑
</syntaxhighlight>

=== <code>tactic</code> 组合 ===
用户可以通过组合多个策略来定制证明搜索流程：

<syntaxhighlight lang="lean">
example (a b : Nat) : a = b → b = a := by
  intro h
  rw [h] -- 使用rewrite策略
</syntaxhighlight>

== 高级证明搜索技术 ==
对于更复杂的目标，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>

== 实际案例 ==
以下是一个结合证明搜索的完整数学证明示例：

<syntaxhighlight lang="lean">
theorem succ_inj : ∀ (n m : Nat), n.succ = m.succ → n = m := by
  intros n m h
  injection h -- 使用注入引理自动推导
</syntaxhighlight>

== 性能优化与限制 ==
证明搜索虽然方便，但可能因搜索空间过大而失败。以下方法可提高效率：
* 使用<code>simp only [...]</code>限制简化规则。
* 通过<code>apply?</code>交互式选择候选定理。
* 设置策略超时：<code>set_option maxHeartbeats 100000</code>。

== 可视化证明搜索流程 ==
以下Mermaid图展示了一个典型的证明搜索过程：

<mermaid>
graph TD
  A[开始证明目标] --> B{是否可直接简化?}
  B -->|是| C[应用simp]
  B -->|否| D{是否存在可应用定理?}
  D -->|是| E[尝试apply]
  D -->|否| F[失败/需手动干预]
  C --> G[新子目标]
  E --> G
  G --> H{是否所有目标解决?}
  H -->|是| I[完成]
  H -->|否| B
</mermaid>

== 数学背景 ==
证明搜索的理论基础是'''逻辑可满足性'''（Satisfiability）和'''类型 inhabitation'''问题。在Lean中，目标可表示为以下形式：
<math>
\Gamma \vdash ?t : \tau
</math>
其中<math>\Gamma</math>是上下文，<math>?t</math>是待构造的项，<math>\tau</math>是目标类型。

== 延伸阅读 ==
* 在更复杂的证明中，可以结合<code>have</code>语句引导搜索方向。
* 使用<code>library_search</code>策略从标准库中查找相关定理。
* 了解<code>MetaM</code>元编程框架可进一步定制证明搜索。

== 总结 ==
Lean的证明搜索功能显著提升了交互式证明的效率，尤其适合：
1. 初学者快速验证基本证明思路
2. 专家处理重复性高的证明结构
3. 教学场景中展示自动化推理能力

通过合理组合策略和逐步扩展自定义方法，用户可以构建出强大的个性化证明搜索流程。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean高级证明技术]]