Lean逻辑连接词

逻辑连接词是命题逻辑中的基本构建块，用于组合简单命题形成复杂命题。在Lean定理证明器中，逻辑连接词是形式化数学和编程验证的核心工具。本文将全面介绍Lean中五种主要逻辑连接词：合取（∧）、析取（∨）、蕴含（→）、否定（¬）和等价（↔）。

逻辑连接词概述[编辑 | 编辑源代码]

在Lean中，逻辑连接词被定义为归纳类型或常量，其行为遵循构造演算的规则。以下是基础连接词的类型签名：

解析失败 (语法错误): {\displaystyle \begin{align*} &\wedge\ :\ Prop\ \to\ Prop\ \to\ Prop \\ &\vee\ :\ Prop\ \to\ Prop\ \to\ Prop \\ &\to\ :\ Prop\ \to\ Prop\ \to\ Prop \\ &\neg\ :\ Prop\ \to\ Prop \\ &\leftrightarrow\ :\ Prop\ \to\ Prop\ \to\ Prop \end{align*}}

合取（Conjunction, ∧）[编辑 | 编辑源代码]

合取表示"且"关系，要求两个命题同时为真。

语法与构造[编辑 | 编辑源代码]

-- 构造合取命题
example : 2 + 2 = 4 ∧ 3 + 3 = 6 := 
  ⟨by norm_num, by norm_num⟩

输出结果：

⊢ 2 + 2 = 4 ∧ 3 + 3 = 6

分解使用[编辑 | 编辑源代码]

example (h : p ∧ q) : p := h.left
example (h : p ∧ q) : q := h.right

析取（Disjunction, ∨）[编辑 | 编辑源代码]

析取表示"或"关系，至少一个命题为真即可。

基本用法[编辑 | 编辑源代码]

-- 从左构造析取
example : 2 + 2 = 4 ∨ 1 = 0 := Or.inl (by norm_num)
-- 从右构造析取
example : 1 = 0 ∨ 3 = 3 := Or.inr (by norm_num)

案例分析[编辑 | 编辑源代码]

蕴含（Implication, →）[编辑 | 编辑源代码]

蕴含表示"如果...那么..."关系，是Lean中最常用的连接词。

函数对应[编辑 | 编辑源代码]

在Curry-Howard同构下，蕴含对应函数类型：

example (h : p → q) (hp : p) : q := h hp

证明策略[编辑 | 编辑源代码]

使用intro策略处理假设：

example : p → p := by
  intro h
  exact h

否定（Negation, ¬）[编辑 | 编辑源代码]

否定实际上是蕴含的特殊形式： $\neg p \equiv p \to False$

典型证明[编辑 | 编辑源代码]

example (h : p ∧ ¬p) : False := h.right h.left

等价（Equivalence, ↔）[编辑 | 编辑源代码]

等价是双向蕴含，定义为合取两个方向的蕴含。

构造示例[编辑 | 编辑源代码]

example : p ↔ p := 
  ⟨fun h => h, fun h => h⟩

优先级规则[编辑 | 编辑源代码]

Lean中逻辑连接词的优先级（从高到低）：

¬
∧, ∨
→
↔

实际应用案例[编辑 | 编辑源代码]

软件规范验证：验证排序算法的前后条件

theorem sort_correct (arr : Array α) :
  (is_sorted (sort arr)) ∧ (arr.toList.Perm (sort arr).toList) := by
  apply And.intro
  · -- 证明排序后有序
  · -- 证明结果是排列

练习建议[编辑 | 编辑源代码]

1. 证明交换律：p ∧ q ↔ q ∧ p 2. 构造德摩根定律：¬(p ∨ q) ↔ ¬p ∧ ¬q 3. 实现蕴含传递性：(p → q) → (q → r) → (p → r)

高级主题[编辑 | 编辑源代码]

对于有经验的用户，可以探讨：

连接词的计算行为差异
经典逻辑与直觉主义逻辑的区别
连接词在依赖类型中的扩展应用

通过掌握这些逻辑连接词，用户将能够构建复杂的逻辑陈述并在Lean中进行形式化验证。