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

在Lean定理证明器中，证明状态操作是指通过策略(tactics)与当前证明环境交互、查看和修改证明状态的过程。理解证明状态是掌握Lean高级证明技术的核心基础，它允许证明者精确控制证明流程并诊断问题。

基本概念[编辑 | 编辑源代码]

在Lean中，每当开始一个证明时，系统会维护一个证明状态（Proof State），包含以下核心组成部分：

当前假设（Hypotheses）：已知的前提条件
目标（Goals）：需要证明的命题
元变量（Metavariables）：待解决的约束

证明状态通常呈现为如下形式： ``` hp : P, hq : Q ⊢ R ``` 其中`hp`和`hq`是假设，`⊢ R`表示需要证明的目标。

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

基础查看[编辑 | 编辑源代码]

在Lean交互模式中，证明状态会自动显示。但也可以通过命令显式查看：

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  -- 查看当前状态
  trace_state
  /- 输出：
  p q : Prop,
  hp : p,
  hq : q
  ⊢ p ∧ q
  -/
  apply And.intro
  · exact hp
  · exact hq

高级查看技巧[编辑 | 编辑源代码]

1. 查看全部目标：使用`all_goals`组合器 2. 查看隐藏信息：`set_option pp.all true`显示完整信息 3. 查看类型：`#check`命令或`infer_type`策略

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

基本策略[编辑 | 编辑源代码]

常用状态操作策略包括：

策略	作用	示例
`intro`	引入假设	`intro h` 将`∀ x, P x`变为`h : x ⊢ P x`
`apply`	反向推理	`apply h` 用`h : P → Q`将目标`Q`变为`P`
`rewrite`	重写目标	`rewrite [h]` 用等式`h`重写
`simp`	简化目标	`simp [h₁, h₂]` 用h₁ h₂简化

状态导航[编辑 | 编辑源代码]

使用焦点操作可以精细控制证明状态：

example (p q r : Prop) : p → (q → r) → q → (p → r) := by
  intros hp hqr hq hpr
  -- 聚焦第一个目标
  focus
    apply hqr
    exact hq
  -- 聚焦剩余目标
  focus
    exact hpr hp

高级操作技术[编辑 | 编辑源代码]

元编程接口[编辑 | 编辑源代码]

通过Lean的元编程可以深度操作证明状态：

macro "solve" : tactic => `(tactic| (repeat (first | assumption | apply And.intro)))

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  solve  -- 自定义策略处理状态

状态可视化[编辑 | 编辑源代码]

使用mermaid可以表示状态转换：

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

案例1：等价关系证明[编辑 | 编辑源代码]

theorem and_comm (p q : Prop) : p ∧ q ↔ q ∧ p := by
  apply Iff.intro
  · intro ⟨hp, hq⟩
    trace_state  -- 查看中间状态
    exact ⟨hq, hp⟩
  · intro ⟨hq, hp⟩
    exact ⟨hp, hq⟩

案例2：归纳证明中的状态管理[编辑 | 编辑源代码]

theorem nat_add_comm (m n : ℕ) : m + n = n + m := by
  induction n with
  | zero =>
      simp
      trace_state  -- 显示基础情况状态
  | succ k ih =>
      rw [Nat.add_succ, Nat.succ_add, ih]
      trace_state  -- 显示归纳步骤状态

常见问题[编辑 | 编辑源代码]

Q: 如何调试复杂的证明状态？ A: 组合使用： 1. `trace_state`在不同步骤打印状态 2. `set_option pp.proofs false`隐藏证明项 3. 使用`sorry`临时跳过子目标

Q: 为什么我的rewrite没有改变目标？ A: 可能原因： 1. 等式方向错误，尝试`←`（`\l`） 2. 匹配模式不精确，使用`@eq`限定

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

证明状态可以形式化为四元组： $S t a t e = ⟨ Γ, ℳ, G, 𝒰 ⟩$ 其中：

$Γ$ 是假设上下文
$ℳ$ 是元变量集合
$G$ 是当前目标栈
$𝒰$ 是约束系统

进阶阅读[编辑 | 编辑源代码]

掌握证明状态操作后，可以进一步学习：

自定义策略编写
交互式定理证明元编程
复杂目标的自动化处理

通过深入理解Lean证明状态操作，证明者可以更高效地构建复杂证明，并开发领域特定的证明自动化工具。