Lean集合
Lean集合[编辑 | 编辑源代码]
Lean集合是Lean定理证明器中的基础数据结构之一，用于存储唯一元素的容器。它基于数学中的集合理论，支持常见的集合操作，如并集、交集、差集等。本章节将详细介绍Lean集合的定义、基本操作、实际应用以及高级特性。
介绍[编辑 | 编辑源代码]
在Lean中，集合（`Set`）是一种表示数学集合的数据结构。它类似于列表，但集合中的元素是唯一的，且不保证顺序。Lean的`Set`类型定义在标准库`Mathlib`中，依赖于谓词逻辑来表示集合成员关系。
集合的核心特征是：
- 唯一性：集合中的元素不会重复。
- 无序性：元素的存储顺序无关紧要。
- 动态性：集合可以动态增删元素。
数学上，集合 可以表示为： 其中 是一个谓词，描述元素 是否属于集合 。
基本操作[编辑 | 编辑源代码]
创建集合[编辑 | 编辑源代码]
在Lean中，可以通过`Set`构造函数或字面量语法创建集合：
-- 使用Set构造函数
def mySet : Set Nat := {1, 2, 3}
-- 使用谓词定义集合
def evenNumbers : Set Nat := {n | n % 2 = 0}
成员检查[编辑 | 编辑源代码]
检查元素是否属于集合：
#eval 1 ∈ mySet -- 输出: true
#eval 4 ∈ mySet -- 输出: false
集合运算[编辑 | 编辑源代码]
Lean支持常见的集合运算：
def setA : Set Nat := {1, 2, 3}
def setB : Set Nat := {3, 4, 5}
-- 并集
#eval setA ∪ setB -- 输出: {1, 2, 3, 4, 5}
-- 交集
#eval setA ∩ setB -- 输出: {3}
-- 差集
#eval setA \ setB -- 输出: {1, 2}
高级特性[编辑 | 编辑源代码]
集合的证明[编辑 | 编辑源代码]
Lean的集合与定理证明紧密结合。例如，可以证明两个集合相等：
example : {1, 2, 3} = {3, 2, 1} := by
simp only [Set.insert_empty_eq_singleton, Set.singleton_union]
有限与无限集合[编辑 | 编辑源代码]
Lean区分有限集合（`Finset`）和无限集合（`Set`）。`Finset`提供了更高效的运算：
import Mathlib.Data.Finset.Basic
def finiteSet : Finset Nat := {1, 2, 3}
#eval finiteSet.card -- 输出: 3
实际案例[编辑 | 编辑源代码]
案例1：过滤唯一元素[编辑 | 编辑源代码]
假设我们需要从一个列表中提取唯一元素：
def uniqueElements (lst : List Nat) : Set Nat := lst.toSet
#eval uniqueElements [1, 2, 2, 3] -- 输出: {1, 2, 3}
案例2：集合覆盖问题[编辑 | 编辑源代码]
解决一个简单的集合覆盖问题：
def universe : Set Nat := {1, 2, 3, 4, 5}
def subsets : List (Set Nat) := [{1, 2}, {3, 4}, {4, 5}]
-- 检查是否覆盖全集
def isCovered : Bool := subsets.foldl (· ∪ ·) ∅ = universe
#eval isCovered -- 输出: false
可视化[编辑 | 编辑源代码]
使用Mermaid展示集合关系：
总结[编辑 | 编辑源代码]
Lean集合是功能强大的数据结构，适用于数学证明和编程任务。通过本章的学习，您应掌握：
- 集合的基本定义与操作。
- 如何用Lean进行集合运算和证明。
- 实际场景中集合的应用方法。