Lean证明状态[编辑 | 编辑源代码]

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

核心概念[编辑 | 编辑源代码]

在Lean中，证明状态是一个动态数据结构，包含以下关键元素：

目标（Goals）：当前需要证明的命题
假设（Hypotheses）：当前可用的已知条件
上下文（Context）：包括局部变量、类型信息等元数据

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

数学表示[编辑 | 编辑源代码]

证明状态可以形式化为一个四元组： $Γ ⊢ G ∣ ℋ$ 其中：

$Γ$ 表示上下文
$G$ 表示当前目标
$ℋ$ 表示假设集合

基础交互[编辑 | 编辑源代码]

查看证明状态[编辑 | 编辑源代码]

在Lean4中，使用_表示当前证明状态。以下是一个简单示例：

example : ∀ n : Nat, n = n := by
  intro n
  -- 此时证明状态显示：
  -- n : Nat
  -- ⊢ n = n
  rfl

状态变化示例[编辑 | 编辑源代码]

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

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

状态分解[编辑 | 编辑源代码]

目标树结构[编辑 | 编辑源代码]

复杂证明会产生多级目标，形成树状结构：

焦点切换[编辑 | 编辑源代码]

使用·或focus可以聚焦特定子目标：

example : (True ∧ True) ∧ True := by
  apply And.intro
  · apply And.intro
    exact True.intro
    exact True.intro
  exact True.intro

高级特性[编辑 | 编辑源代码]

元编程访问[编辑 | 编辑源代码]

通过Lean4的元编程接口可以直接操作证明状态：

macro "show_state" : tactic => `(tactic| (
  let state ← Lean.Elab.Tactic.getGoals
  Lean.logInfo m!"当前目标数: {state.length}"
))

假设依赖分析[编辑 | 编辑源代码]

证明状态会跟踪假设间的依赖关系。例如在存在量词消除时：

example (P : Nat → Prop) : (∃ x, P x) → True := by
  intro ⟨w, h⟩  -- 引入存在量词时生成新假设w和h
  /-
  状态包含：
  w : Nat
  h : P w
  ⊢ True
  -/
  trivial

实际案例[编辑 | 编辑源代码]

数学证明[编辑 | 编辑源代码]

考虑自然数加法的交换律证明片段：

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]

程序验证[编辑 | 编辑源代码]

验证列表反转函数的性质：

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]

常见模式[编辑 | 编辑源代码]

证明状态转换模式
模式类型	初始状态	应用策略	结果状态
假设引入	`⊢ P → Q`	`intro h`	`h : P ⊢ Q`
合取分解	`⊢ P ∧ Q`	`apply And.intro`	两个目标: `⊢ P` 和 `⊢ Q`
析取消除	`h : P ∨ Q ⊢ R`	`cases h`	两个分支: `hP : P ⊢ R` 和 `hQ : Q ⊢ R`

调试技巧[编辑 | 编辑源代码]

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

总结[编辑 | 编辑源代码]

Lean证明状态是交互式证明的核心抽象，掌握其结构和工作原理能够：

有效规划证明策略
理解策略应用的副作用
调试失败的证明尝试
编写可维护的结构化证明

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