跳到主要内容

Lean 基本战术

Lean是一个交互式定理证明器，它允许用户通过编写代码来构造数学证明。在Lean中，**战术（Tactics）**是用于指导证明过程的关键工具。它们帮助用户分解复杂的证明目标，逐步简化问题，直到最终完成证明。本文将介绍Lean中的一些基本战术，并通过示例展示如何使用它们。

什么是战术？​

战术是Lean中用于操作证明状态的命令。每个战术都会根据当前的目标（Goal）执行特定的操作，例如分解假设、应用定理或简化表达式。通过组合使用不同的战术，用户可以逐步构建出完整的证明。

基本战术介绍​

1. intro​

intro 战术用于处理形如 ∀ x, P x 或 P → Q 的目标。它会将目标中的全称量词或蕴含前提引入到假设中。

示例：

lean
example : ∀ (n : ℕ), n = n :=
begin
  intro n,  -- 将 `n` 引入为假设
  reflexivity  -- 使用自反性证明 `n = n`
end

在这个例子中，intro n 将 ∀ n 中的 n 引入为假设，使得我们可以直接使用 n 来证明 n = n。

2. apply​

apply 战术用于将目标与某个定理或引理的结论匹配。如果目标与定理的结论一致，apply 会将目标替换为定理的前提。

示例：

lean
example (P Q : Prop) (h : P → Q) (p : P) : Q :=
begin
  apply h,  -- 应用 `h : P → Q`，将目标 `Q` 替换为 `P`
  exact p    -- 使用 `p : P` 完成证明
end

在这个例子中，apply h 将目标 Q 替换为 P，然后我们使用 exact p 来证明 P。

3. exact​

exact 战术用于直接提供目标所需的证明项。如果当前目标与提供的项完全匹配，exact 将完成证明。

示例：

lean
example (P : Prop) (h : P) : P :=
begin
  exact h  -- 直接使用 `h` 完成证明
end

这里，exact h 直接使用假设 h 来证明目标 P。

4. split​

split 战术用于处理合取目标（即形如 P ∧ Q 的目标）。它会将目标分解为两个子目标，分别对应 P 和 Q。

示例：

lean
example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q :=
begin
  split,  -- 将目标 `P ∧ Q` 分解为 `P` 和 `Q`
  { exact hP },  -- 证明 `P`
  { exact hQ }   -- 证明 `Q`
end

在这个例子中，split 将目标 P ∧ Q 分解为两个子目标 P 和 Q，然后我们分别使用 hP 和 hQ 来证明它们。

5. cases​

cases 战术用于分解假设中的合取或析取命题。它会将假设分解为多个子假设，并为每个子假设生成一个新的目标。

示例：

lean
example (P Q : Prop) (h : P ∨ Q) : Q ∨ P :=
begin
  cases h,  -- 分解假设 `h : P ∨ Q`
  { right, exact h },  -- 如果 `h` 是 `P`，则证明 `Q ∨ P` 的右分支
  { left, exact h }    -- 如果 `h` 是 `Q`，则证明 `Q ∨ P` 的左分支
end

在这个例子中，cases h 将假设 h : P ∨ Q 分解为两个子假设 P 和 Q，然后我们分别处理这两种情况。

实际应用案例​

让我们通过一个稍微复杂的例子来展示这些战术的实际应用。

目标： 证明 ∀ (n : ℕ), n + 0 = n。

lean
example : ∀ (n : ℕ), n + 0 = n :=
begin
  intro n,  -- 引入 `n`
  induction n,  -- 对 `n` 进行归纳
  { reflexivity },  -- 基本情况：`0 + 0 = 0`
  { simp [nat.succ_add],  -- 归纳步骤：简化 `succ n + 0 = succ n`
    assumption }  -- 使用归纳假设完成证明
end

在这个例子中，我们使用了 intro、induction、reflexivity 和 simp 等战术来逐步完成证明。

总结​

Lean中的基本战术是构建证明的基础工具。通过掌握 intro、apply、exact、split 和 cases 等战术，你可以逐步分解复杂的证明目标，最终完成证明。希望本文的内容能帮助你更好地理解这些战术，并在实践中灵活运用它们。

附加资源与练习​

  • 练习1： 尝试证明 ∀ (n : ℕ), 0 + n = n。
  • 练习2： 使用 cases 战术证明 ∀ (P Q : Prop), P ∨ Q → Q ∨ P。
  • 附加资源： 阅读Lean官方文档中的战术库部分，了解更多高级战术。

通过不断练习和探索，你将逐渐掌握Lean中的证明技巧，成为一名熟练的定理证明者！