编辑“︁Lean证明状态”︁（章节）

= Lean证明状态 =

'''Lean证明状态'''（Proof State）是交互式定理证明器Lean中表示当前证明进度的核心概念。它反映了在证明过程中已知的假设、待证目标以及上下文信息。理解证明状态对于编写结构化证明至关重要，本节将系统介绍其组成、交互方式及实际应用。

== 核心概念 ==

在Lean中，证明状态是一个动态数据结构，包含以下关键元素：
* '''目标（Goals）'''：当前需要证明的命题
* '''假设（Hypotheses）'''：当前可用的已知条件
* '''上下文（Context）'''：包括局部变量、类型信息等元数据

当使用'''tactic'''（策略）进行交互式证明时，证明状态会随着每个策略的应用而改变，直到所有目标被解决。

=== 数学表示 ===
证明状态可以形式化为一个四元组：
<math>
\Gamma \vdash G \mid \mathcal{H}
</math>
其中：
* <math>\Gamma</math> 表示上下文
* <math>G</math> 表示当前目标
* <math>\mathcal{H}</math> 表示假设集合

== 基础交互 ==

=== 查看证明状态 ===
在Lean4中，使用<code>_</code>表示当前证明状态。以下是一个简单示例：

<syntaxhighlight lang="lean">
example : ∀ n : Nat, n = n := by
  intro n
  -- 此时证明状态显示：
  -- n : Nat
  -- ⊢ n = n
  rfl
</syntaxhighlight>

=== 状态变化示例 ===
观察应用策略前后的状态变化：

<syntaxhighlight lang="lean">
example (P Q : Prop) : P → Q → P ∧ Q := by
  intro hP hQ
  /-
  当前状态：
  P Q : Prop,
  hP : P,
  hQ : Q
  ⊢ P ∧ Q
  -/
  apply And.intro
  /-
  状态变为两个子目标：
  case left
  ⊢ P
  
  case right
  ⊢ Q
  -/
  exact hP
  exact hQ
</syntaxhighlight>

== 状态分解 ==

=== 目标树结构 ===
复杂证明会产生多级目标，形成树状结构：
<mermaid>
graph TD
  A[初始目标] --> B[子目标1]
  A --> C[子目标2]
  C --> D[子目标2.1]
  C --> E[子目标2.2]
</mermaid>

=== 焦点切换 ===
使用<code>·</code>或<code>focus</code>可以聚焦特定子目标：
<syntaxhighlight lang="lean">
example : (True ∧ True) ∧ True := by
  apply And.intro
  · apply And.intro
    exact True.intro
    exact True.intro
  exact True.intro
</syntaxhighlight>

== 高级特性 ==

=== 元编程访问 ===
通过Lean4的元编程接口可以直接操作证明状态：
<syntaxhighlight lang="lean">
macro "show_state" : tactic => `(tactic| (
  let state ← Lean.Elab.Tactic.getGoals
  Lean.logInfo m!"当前目标数: {state.length}"
))
</syntaxhighlight>

=== 假设依赖分析 ===
证明状态会跟踪假设间的依赖关系。例如在存在量词消除时：
<syntaxhighlight lang="lean">
example (P : Nat → Prop) : (∃ x, P x) → True := by
  intro ⟨w, h⟩  -- 引入存在量词时生成新假设w和h
  /-
  状态包含：
  w : Nat
  h : P w
  ⊢ True
  -/
  trivial
</syntaxhighlight>

== 实际案例 ==

=== 数学证明 ===
考虑自然数加法的交换律证明片段：
<syntaxhighlight lang="lean">
theorem add_comm (n m : Nat) : n + m = m + n := by
  induction n with
  | zero =>
    /-
    状态：
    m : Nat
    ⊢ 0 + m = m + 0
    -/
    simp
  | succ n ih =>
    /-
    状态：
    n m : Nat,
    ih : n + m = m + n
    ⊢ Nat.succ n + m = m + Nat.succ n
    -/
    simp [Nat.add_succ, Nat.succ_add, ih]
</syntaxhighlight>

=== 程序验证 ===
验证列表反转函数的性质：
<syntaxhighlight lang="lean">
theorem rev_rev_eq {α} (l : List α) : l.reverse.reverse = l := by
  induction l with
  | nil => rfl
  | cons h t ih =>
    /-
    状态：
    h : α,
    t : List α,
    ih : t.reverse.reverse = t
    ⊢ (h :: t).reverse.reverse = h :: t
    -/
    simp [List.reverse_cons, ih]
</syntaxhighlight>

== 常见模式 ==

{| class="wikitable"
|+ 证明状态转换模式
! 模式类型 !! 初始状态 !! 应用策略 !! 结果状态
|-
| 假设引入 || <code>⊢ P → Q</code> || <code>intro h</code> || <code>h : P ⊢ Q</code>
|-
| 合取分解 || <code>⊢ P ∧ Q</code> || <code>apply And.intro</code> || 两个目标: <code>⊢ P</code> 和 <code>⊢ Q</code>
|-
| 析取消除 || <code>h : P ∨ Q ⊢ R</code> || <code>cases h</code> || 两个分支: <code>hP : P ⊢ R</code> 和 <code>hQ : Q ⊢ R</code>
|}

== 调试技巧 ==

* 使用<code>set_option trace.Meta true</code>查看详细状态转换
* 在VSCode中悬停策略可以看到前后的状态差异
* 对于复杂目标，使用<code>simp?</code>获取可行的化简建议

== 总结 ==

Lean证明状态是交互式证明的核心抽象，掌握其结构和工作原理能够：
* 有效规划证明策略
* 理解策略应用的副作用
* 调试失败的证明尝试
* 编写可维护的结构化证明

通过持续观察证明状态的变化，开发者可以培养对形式化证明的直觉，逐步掌握高级证明技术。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean证明基础]]