Lean逻辑等价
逻辑等价是命题逻辑中的核心概念，指两个命题在所有可能情况下具有相同的真值。在Lean定理证明器中，逻辑等价不仅作为理论概念存在，更通过可操作的证明机制实现形式化验证。本文将系统讲解逻辑等价在Lean中的表示、证明方法及实际应用。
逻辑等价的基本定义[编辑 | 编辑源代码]
在命题逻辑中，两个命题和称为逻辑等价（记作或），当且仅当它们在所有真值赋值下具有相同的真值。其真值表如下：
在Lean中，逻辑等价通过双条件语句↔（Unicode符号，可输入为\iff或\lr）表示，实际是iff类型的语法糖。
Lean中的逻辑等价表示[编辑 | 编辑源代码]
Lean将逻辑等价定义为双向蕴涵的合取：
def logical_equiv (P Q : Prop) : Prop := (P → Q) ∧ (Q → P)
标准库中实际定义为：
structure iff (P Q : Prop) : Prop :=
(mp : P → Q)
(mpr : Q → P)
基本证明示例[编辑 | 编辑源代码]
证明命题P ∧ Q ↔ Q ∧ P（合取交换律）：
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
(assume h : P ∧ Q, show Q ∧ P, from and.intro h.right h.left)
(assume h : Q ∧ P, show P ∧ Q, from and.intro h.right h.left)
更简洁的写法：
example : P ∧ Q ↔ Q ∧ P :=
⟨λ h ↦ ⟨h.right, h.left⟩, λ h ↦ ⟨h.right, h.left⟩⟩
逻辑等价的性质[编辑 | 编辑源代码]
逻辑等价满足以下代数性质，这些性质可在Lean中验证：
自反性[编辑 | 编辑源代码]
example : P ↔ P := iff.refl P
对称性[编辑 | 编辑源代码]
example (h : P ↔ Q) : Q ↔ P := iff.symm h
传递性[编辑 | 编辑源代码]
example (h₁ : P ↔ Q) (h₂ : Q ↔ R) : P ↔ R := iff.trans h₁ h₂
常用逻辑等价定律[编辑 | 编辑源代码]
以下定律可通过Lean验证：
| 名称 | 公式 | Lean验证示例 |
|---|---|---|
| 双重否定 | example : ¬¬P ↔ P := not_not
| |
| 德摩根律 | example : ¬(P ∨ Q) ↔ ¬P ∧ ¬Q := not_or_distrib
| |
| 分配律 | example : P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R) := or_and_distrib_left
|
实际应用案例[编辑 | 编辑源代码]
条件重写[编辑 | 编辑源代码]
逻辑等价允许在证明中进行安全替换：
lemma and_comm : P ∧ Q ↔ Q ∧ P := sorry
example (h : P ∧ Q) : Q ∧ P := by rw [and_comm]; exact h
表达式简化[编辑 | 编辑源代码]
简化复杂逻辑表达式：
example : ¬(P ∨ Q) → R :=
assume h : ¬(P ∨ Q),
have ¬P ∧ ¬Q, from not_or_distrib.mp h,
-- 可继续基于德摩根律的结果进行推导
高级应用：等价关系证明[编辑 | 编辑源代码]
对于复杂等价关系，可采用结构化证明：
example : (P → Q) ↔ (¬Q → ¬P) :=
iff.intro
(assume h₁ h₂ h₃, absurd (h₁ h₃) h₂)
(assume h₁ h₂, byContradiction (λ hnQ, h₁ hnQ h₂))
常见误区与调试[编辑 | 编辑源代码]
1. 混淆相等与等价：在Lean中=表示值相等，而↔表示命题等价
2. 忽略方向性：使用rw时需注意替换方向，可用←表示反向替换
3. 隐式括号：复杂表达式建议显式添加括号，如P ∨ Q ↔ R应写为(P ∨ Q) ↔ R
练习建议[编辑 | 编辑源代码]
1. 验证其他逻辑等价定律（如吸收律、结合律）
2. 尝试用不同策略（如tauto、simp）自动证明简单等价
3. 构造非等价命题的反例证明
逻辑等价在Lean中的系统掌握为后续学习谓词逻辑和形式化验证奠定重要基础。通过交互式证明练习，开发者能深入理解逻辑结构的操作机制。