在精益中使用集合

Question

我想使用精益做一些拓扑学方面的工作。

作为一个好的开始，我想证明一些关于 sets in lean 的简单引理。

例如

def inter_to_union (H : a ∈ set.inter A B) : a ∈ set.union A B :=
    sorry

或

def set_deMorgan : a ∈ set.inter A B → a ∈ set.compl (set.union (set.compl A) (set.compl B)) :=
sorry

或者，也许更有趣

def set_deMorgan2 : set.inter A B = set.compl (set.union (set.compl A) (set.compl B)) :=
sorry

但是我在任何地方都找不到 set.union 或 set.inter 的消除规则，所以我不知道如何使用它们。

如何证明引理？

此外，查看definition of sets in lean，我可以看到一些语法，看起来很像纸上数学，但我在依赖类型理论层面上看不懂，例如：

protected def sep (p : α → Prop) (s : set α) : set α :=
{a | a ∈ s ∧ p a}

如何将上述示例分解为更简单的 dependent/inductive 类型概念？

Answer 1

该模块用某种类型的谓词识别集合 α（α 通常称为 'the universe'）：

def set (α : Type u) := α → Prop

如果你有一个集合s : set α并且对于一些x : α你可以证明s a，这被解释为'x belongs to s'。

在这种情况下，x ∈ A 是 set.mem x A 的一种表示法（让我们暂时不考虑类型类），其定义如下：

protected def mem (a : α) (s : set α) :=
s a

上面解释了为什么空集表示为谓词总是返回false:

instance : has_emptyc (set α) :=
⟨λ a, false⟩

此外，宇宙毫不奇怪地表示为：

def univ : set α :=
λ a, true

我将展示如何证明第一个引理：

def inter_to_union {α : Type} {A B : set α} {a : α} : A ∩ B ⊆ A ∪ B :=
  assume (x : α) (xinAB : x ∈ A ∩ B),        -- unfold the definition of `subset`
  have xinA : x ∈ A, from and.left xinAB,
  @or.inl _ (x ∈ B) xinA

这与基本集合论中这些属性的常见 "pointful" 证明完全一样。

关于你关于 sep 的问题——你可以通过这样的符号来理解：

set_option pp.notation false
#print set.sep

这是输出：

protected def set.sep : Π {α : Type u}, (α → Prop) → set α → set α :=
λ {α : Type u} (p : α → Prop) (s : set α),
  set_of (λ (a : α), and (has_mem.mem a s) (p a))

在精益中使用集合

Using sets in lean

formal-verification

dependent-type

lean