dependent-type - 在精益中使用集合

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 的消除规则，所以我只是不知道如何使用它们。

1. 如何证明引理？

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

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

如何将上述示例分解为更简单的依赖/归纳类型概念？

Answer 1

该模块使用某种类型 α 上的谓词来标识集合(α 通常称为“宇宙”):

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

如果你有一个集合 s : set α 并且对于某些 x : α 你可以证明 s a，这被解释为 'x属于 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

这就像基本集合论中这些属性通常的“有意义的”证明。

关于你关于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))