编辑“︁Lean命题与定理”︁

= Lean命题与定理 =

== 介绍 ==

在Lean定理证明器中，'''命题（Proposition）'''和'''定理（Theorem）'''是形式化数学的核心概念。命题是一个可以被证明或证伪的陈述，而定理是一个已被证明的命题。Lean使用类型论作为基础，其中命题被视为类型，其证明是该类型的项（term）。这种“命题即类型”（Propositions as Types）的对应关系是Lean的核心思想之一。

对于程序员来说，可以将命题类比为返回布尔值的函数，而定理则是该函数始终返回`true`的证明。Lean允许用户以编程方式构造证明，并通过类型检查器验证其正确性。

== 基本语法 ==

在Lean中，命题和定理通过`def`、`theorem`或`lemma`关键字声明。以下是基本示例：

<syntaxhighlight lang="lean">
-- 声明一个命题
def isEven (n : Nat) : Prop := ∃ k, n = 2 * k

-- 声明一个定理
theorem two_is_even : isEven 2 :=
  Exists.intro 1 (by rfl)  -- 构造证明：取k=1，通过反射性证明2=2*1
</syntaxhighlight>

=== 代码解释 ===
* `isEven`是一个命题，表示“存在自然数k使得n=2k”。
* `two_is_even`是一个定理，其类型是`isEven 2`（即“2是偶数”这一命题）。
* `Exists.intro`用于构造存在量词的证明，`by rfl`表示通过计算简化完成证明。

== 命题逻辑示例 ==

Lean支持标准的逻辑连接词：
* 合取（∧）：`And`
* 析取（∨）：`Or`
* 蕴含（→）：箭头符号
* 否定（¬）：`Not`

<syntaxhighlight lang="lean">
-- 合取示例
theorem and_example : 2 + 2 = 4 ∧ 3 + 3 = 6 :=
  ⟨by rfl, by rfl⟩  -- 使用⟨⟩构造合取证明

-- 蕴含示例
theorem imp_example (P Q : Prop) (h : P → Q) (p : P) : Q :=
  h p  -- 应用蕴含规则
</syntaxhighlight>

== 一阶逻辑与量词 ==

Lean支持全称量词（∀）和存在量词（∃）：

<syntaxhighlight lang="lean">
-- 全称量词
theorem forall_example : ∀ n : Nat, n + 0 = n :=
  fun n => by rfl  -- 使用lambda表达式构造证明

-- 存在量词
theorem exists_example : ∃ n : Nat, n > 0 :=
  Exists.intro 1 (by decide)  -- 选择n=1作为见证
</syntaxhighlight>

== 定理证明流程 ==

在Lean中证明定理通常遵循以下步骤：
1. '''陈述定理'''：明确声明命题和变量。
2. '''选择策略'''：使用诸如`induction`、`rewrite`等策略。
3. '''构造证明项'''：通过交互式证明或直接编写证明项。

<mermaid>
graph TD
    A[陈述定理] --> B[选择策略]
    B --> C[应用策略]
    C --> D{是否完成?}
    D -->|否| B
    D -->|是| E[QED]
</mermaid>

== 实际案例：费马小定理 ==

以下是一个高级示例，展示如何在Lean中形式化费马小定理：

<syntaxhighlight lang="lean">
import Mathlib.NumberTheory.FermatLittle

-- 形式化费马小定理
theorem fermat_little {p : ℕ} (hp : Prime p) {a : ℕ} (ha : ¬ p ∣ a) :
    a^(p - 1) ≡ 1 [MOD p] :=
  fermat_little_of_prime hp ha  -- 调用Mathlib中的证明
</syntaxhighlight>

== 命题与类型的对应 ==

根据Curry-Howard同构，Lean中的命题和类型具有深刻对应关系：

{| class="wikitable"
! 逻辑概念 !! Lean类型论对应
|-
| 命题 | `Prop`类型
|-
| 证明 | 类型的项（term）
|-
| 真命题 | 非空类型
|-
| 假命题 | 空类型
|}

数学公式示例：命题<math>P \land Q</math>对应乘积类型<math>P \times Q</math>。

== 常见问题 ==

=== 命题 vs 布尔表达式 ===
* '''命题'''是逻辑陈述，其证明是构造性的。
* '''布尔表达式'''是可计算的，返回`true`或`false`。

<syntaxhighlight lang="lean">
-- 布尔版本
def isEvenBool (n : Nat) : Bool := n % 2 == 0

-- 命题版本
def isEvenProp (n : Nat) : Prop := ∃ k, n = 2 * k
</syntaxhighlight>

=== 如何选择定理vs引理 ===
* '''定理'''：重要的主要结果。
* '''引理'''：辅助性结果，通常用于证明更大的定理。

== 进阶主题 ==

对于高级用户，Lean还支持：
* '''类型类'''：用于组织命题结构
* '''策略模式'''：自动化证明构造
* '''元编程'''：生成命题和定理的工具

<syntaxhighlight lang="lean">
-- 类型类示例
class Group (G : Type) where
  mul : G → G → G
  one : G
  inv : G → G
  -- 群公理作为命题
  mul_assoc : ∀ a b c : G, mul (mul a b) c = mul a (mul b c)
  one_mul : ∀ a : G, mul one a = a
  mul_left_inv : ∀ a : G, mul (inv a) a = one
</syntaxhighlight>

== 总结 ==

Lean中的命题与定理构成了形式化数学的基础：
1. 命题是`Prop`类型的项，表示数学陈述。
2. 定理是被证明的命题，是Lean的核心对象。
3. 证明是构造性的，可通过编程方式创建。
4. 命题逻辑和一阶逻辑被完全支持。

通过实践这些概念，用户可以在Lean中逐步构建复杂的数学形式化项目。

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