跳到主要内容

Lean 证明状态操作

在Lean中，证明状态（Proof State）是证明过程中的核心概念。它代表了当前证明的上下文，包括已知的假设、目标以及可能的中间步骤。理解如何操作证明状态是掌握Lean高级证明技术的关键。本文将逐步介绍Lean中的证明状态操作，并通过实际案例帮助你更好地理解这一概念。

什么是证明状态？​

在Lean中，证明状态是一个动态的结构，它包含了当前证明的所有信息。当你开始一个证明时，Lean会初始化一个证明状态，其中包含你的目标（即需要证明的命题）以及已知的假设。随着你逐步应用策略（tactics），证明状态会不断变化，直到最终完成证明。

证明状态的结构​

证明状态通常由以下几个部分组成：

  1. 目标（Goal）：当前需要证明的命题。
  2. 假设（Hypotheses）：已知的命题，可以作为证明的依据。
  3. 上下文（Context）：当前作用域内的变量和假设。

操作证明状态的基本策略​

在Lean中，你可以使用多种策略来操作证明状态。以下是一些常用的策略：

1. intro 策略​

intro 策略用于引入假设。当你有一个形如 ∀ x, P x 的目标时，intro 会将 x 引入到上下文中，并将目标变为 P x。

lean
example : ∀ (n : ℕ), n = n :=
begin
  intro n,
  -- 现在目标变为 `n = n`
  reflexivity
end

2. apply 策略​

apply 策略用于将一个命题应用到当前目标上。如果你有一个形如 P → Q 的假设，并且当前目标是 Q，那么 apply 会将目标变为 P。

lean
example (P Q : Prop) (h : P → Q) (p : P) : Q :=
begin
  apply h,
  -- 现在目标变为 `P`
  exact p
end

3. rewrite 策略​

rewrite 策略用于根据等式重写目标或假设。如果你有一个等式 h : a = b，那么 rewrite h 会将目标中所有的 a 替换为 b。

lean
example (a b : ℕ) (h : a = b) : a + 1 = b + 1 :=
begin
  rewrite h,
  -- 现在目标变为 `b + 1 = b + 1`
  reflexivity
end

实际案例：证明一个简单的命题​

让我们通过一个简单的例子来展示如何操作证明状态。假设我们要证明以下命题：

lean
example (P Q : Prop) (h1 : P → Q) (h2 : P) : Q :=
begin
  apply h1,
  exact h2
end

在这个例子中，我们首先使用 apply h1 将目标从 Q 变为 P，然后使用 exact h2 来完成证明。

总结​

通过本文，你已经了解了Lean中证明状态的基本概念以及如何操作证明状态。掌握这些基础策略是进一步学习高级证明技术的关键。在实际的证明过程中，灵活运用这些策略可以帮助你更高效地完成证明。

附加资源与练习​

为了巩固你的知识，建议你尝试以下练习：

  1. 证明以下命题：

    lean
    example (P Q R : Prop) (h1 : P → Q) (h2 : Q → R) (h3 : P) : R :=
    begin
      -- 你的证明
    end

  2. 使用 rewrite 策略证明以下命题：

    lean
    example (a b c : ℕ) (h1 : a = b) (h2 : b = c) : a = c :=
    begin
      -- 你的证明
    end

通过这些练习，你将更加熟悉Lean中的证明状态操作，并为学习更高级的证明技术打下坚实的基础。