编辑“︁Lean逻辑等价”︁

{{DISPLAYTITLE:Lean逻辑等价}}

'''逻辑等价'''是命题逻辑中的核心概念，指两个命题在所有可能情况下具有相同的真值。在Lean定理证明器中，逻辑等价不仅作为理论概念存在，更通过可操作的证明机制实现形式化验证。本文将系统讲解逻辑等价在Lean中的表示、证明方法及实际应用。

== 逻辑等价的基本定义 ==
在命题逻辑中，两个命题<math>P</math>和<math>Q</math>称为'''逻辑等价'''（记作<math>P \leftrightarrow Q</math>或<math>P \equiv Q</math>），当且仅当它们在所有真值赋值下具有相同的真值。其真值表如下：

<mermaid>
truthTable
    title 逻辑等价真值表
    headers "P", "Q", "P ↔ Q"
    row "T", "T", "T"
    row "T", "F", "F"
    row "F", "T", "F"
    row "F", "F", "T"
</mermaid>

在Lean中，逻辑等价通过双条件语句<code>↔</code>（Unicode符号，可输入为<code>\iff</code>或<code>\lr</code>）表示，实际是<code>iff</code>类型的语法糖。

== Lean中的逻辑等价表示 ==
Lean将逻辑等价定义为双向蕴涵的合取：
<syntaxhighlight lang="lean">
def logical_equiv (P Q : Prop) : Prop := (P → Q) ∧ (Q → P)
</syntaxhighlight>

标准库中实际定义为：
<syntaxhighlight lang="lean">
structure iff (P Q : Prop) : Prop :=
  (mp : P → Q)
  (mpr : Q → P)
</syntaxhighlight>

=== 基本证明示例 ===
证明命题<code>P ∧ Q ↔ Q ∧ P</code>（合取交换律）：
<syntaxhighlight lang="lean">
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)
</syntaxhighlight>

更简洁的写法：
<syntaxhighlight lang="lean">
example : P ∧ Q ↔ Q ∧ P :=
⟨λ h ↦ ⟨h.right, h.left⟩, λ h ↦ ⟨h.right, h.left⟩⟩
</syntaxhighlight>

== 逻辑等价的性质 ==
逻辑等价满足以下代数性质，这些性质可在Lean中验证：

=== 自反性 ===
<syntaxhighlight lang="lean">
example : P ↔ P := iff.refl P
</syntaxhighlight>

=== 对称性 ===
<syntaxhighlight lang="lean">
example (h : P ↔ Q) : Q ↔ P := iff.symm h
</syntaxhighlight>

=== 传递性 ===
<syntaxhighlight lang="lean">
example (h₁ : P ↔ Q) (h₂ : Q ↔ R) : P ↔ R := iff.trans h₁ h₂
</syntaxhighlight>

== 常用逻辑等价定律 ==
以下定律可通过Lean验证：

{| class="wikitable"
! 名称 !! 公式 !! Lean验证示例
|-
| 双重否定 || <math>\neg \neg P \leftrightarrow P</math> || <code>example : ¬¬P ↔ P := not_not</code>
|-
| 德摩根律 || <math>\neg(P \lor Q) \leftrightarrow \neg P \land \neg Q</math> || <code>example : ¬(P ∨ Q) ↔ ¬P ∧ ¬Q := not_or_distrib</code>
|-
| 分配律 || <math>P \lor (Q \land R) \leftrightarrow (P \lor Q) \land (P \lor R)</math> || <code>example : P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R) := or_and_distrib_left</code>
|}

== 实际应用案例 ==
=== 条件重写 ===
逻辑等价允许在证明中进行安全替换：
<syntaxhighlight lang="lean">
lemma and_comm : P ∧ Q ↔ Q ∧ P := sorry
example (h : P ∧ Q) : Q ∧ P := by rw [and_comm]; exact h
</syntaxhighlight>

=== 表达式简化 ===
简化复杂逻辑表达式：
<syntaxhighlight lang="lean">
example : ¬(P ∨ Q) → R :=
assume h : ¬(P ∨ Q),
have ¬P ∧ ¬Q, from not_or_distrib.mp h,
-- 可继续基于德摩根律的结果进行推导
</syntaxhighlight>

== 高级应用：等价关系证明 ==
对于复杂等价关系，可采用结构化证明：
<syntaxhighlight lang="lean">
example : (P → Q) ↔ (¬Q → ¬P) :=
iff.intro
  (assume h₁ h₂ h₃, absurd (h₁ h₃) h₂)
  (assume h₁ h₂, byContradiction (λ hnQ, h₁ hnQ h₂))
</syntaxhighlight>

== 常见误区与调试 ==
1. '''混淆相等与等价'''：在Lean中<code>=</code>表示值相等，而<code>↔</code>表示命题等价
2. '''忽略方向性'''：使用<code>rw</code>时需注意替换方向，可用<code>←</code>表示反向替换
3. '''隐式括号'''：复杂表达式建议显式添加括号，如<code>P ∨ Q ↔ R</code>应写为<code>(P ∨ Q) ↔ R</code>

== 练习建议 ==
1. 验证其他逻辑等价定律（如吸收律、结合律）
2. 尝试用不同策略（如<code>tauto</code>、<code>simp</code>）自动证明简单等价
3. 构造非等价命题的反例证明

逻辑等价在Lean中的系统掌握为后续学习谓词逻辑和形式化验证奠定重要基础。通过交互式证明练习，开发者能深入理解逻辑结构的操作机制。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean命题逻辑]]