Lean命题与定理

Lean命题与定理

介绍

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

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

基本语法

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

-- 声明一个命题
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

代码解释

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

命题逻辑示例

Lean支持标准的逻辑连接词：

• 合取（∧）：`And`
• 析取（∨）：`Or`
• 蕴含（→）：箭头符号
• 否定（¬）：`Not`

-- 合取示例
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  -- 应用蕴含规则

一阶逻辑与量词

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作为见证

定理证明流程

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

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

实际案例：费马小定理

以下是一个高级示例，展示如何在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中的证明

命题与类型的对应

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

逻辑概念	Lean类型论对应
`Prop`类型
类型的项（term）
非空类型
空类型

数学公式示例：命题$P\wedge Q$对应乘积类型$P\times Q$。

常见问题

命题 vs 布尔表达式

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

-- 布尔版本
def isEvenBool (n : Nat) : Bool := n % 2 == 0

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

如何选择定理vs引理

• 定理：重要的主要结果。
• 引理：辅助性结果，通常用于证明更大的定理。

进阶主题

对于高级用户，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

总结

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

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