Lean布尔逻辑
Lean布尔逻辑是Lean定理证明器中处理命题逻辑的基础模块，它基于布尔代数的经典规则，允许用户形式化并验证逻辑命题的正确性。本章将系统介绍Lean中布尔逻辑的核心概念、语法和实际应用方法。
核心概念[编辑 | 编辑源代码]
布尔逻辑在Lean中通过以下基础构件实现：
- 命题（Proposition）：可被判定真（`true`）或假（`false`）的陈述，对应Lean类型`Prop`。
- 逻辑联结词：包括否定（`¬`）、合取（`∧`）、析取（`∨`）、蕴含（`→`）和等价（`↔`）。
- 常量：`true`和`false`。
数学表达示例：（排中律）。
语法与示例[编辑 | 编辑源代码]
基础命题定义[编辑 | 编辑源代码]
-- 定义两个命题变量
variables (p q : Prop)
-- 命题示例：合取（AND）
example : p ∧ q → q ∧ p :=
fun h : p ∧ q => ⟨h.right, h.left⟩
输出说明：此证明展示合取交换律，输入假设`h : p ∧ q`时，通过解构`h`并重组顺序得到`q ∧ p`。
真值表验证[编辑 | 编辑源代码]
使用`#check`命令验证命题有效性：
#check true ∧ false -- 输出: false
#check ¬(true ∨ false) -- 输出: false
高级应用[编辑 | 编辑源代码]
条件证明[编辑 | 编辑源代码]
theorem impl_trans (p q r : Prop) : (p → q) → (q → r) → (p → r) :=
fun h₁ h₂ h₃ => h₂ (h₁ h₃)
解释：该定理证明蕴含的传递性，通过函数组合实现逻辑推理。
经典逻辑 vs 构造逻辑[编辑 | 编辑源代码]
Lean默认使用构造逻辑，但可显式启用经典推理：
open classical
example (p : Prop) : p ∨ ¬p :=
em p
实际案例[编辑 | 编辑源代码]
电路设计验证[编辑 | 编辑源代码]
验证与门的逻辑行为：
def and_gate (a b : bool) : bool :=
a && b
lemma and_gate_correct : ∀ a b, and_gate a b ↔ a = tt ∧ b = tt :=
by cases a; cases b; simp [and_gate]
决策系统[编辑 | 编辑源代码]
编码简单的访问控制规则：
def has_access (is_admin has_permission : bool) : bool :=
is_admin ∨ has_permission
可视化逻辑结构[编辑 | 编辑源代码]
说明：图示展示合取命题的解构与析取命题的案例分析。
常见错误与调试[编辑 | 编辑源代码]
- 构造性限制：未启用`classical`时无法直接使用排中律。
- 类型混淆：混淆`Bool`（计算布尔值）与`Prop`（逻辑命题）类型。
- 隐式转换失败：`example : true := trivial`正确，但`example : 1 = 1 := trivial`会报错。
练习建议[编辑 | 编辑源代码]
1. 证明德摩根定律：
example : ¬(p ∧ q) ↔ ¬p ∨ ¬q
2. 实现异或（XOR）运算符并验证其性质。