在精益中使用集合

Question

我想用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. 我该如何证明这些引理？

此外，在精益集的定义中，我可以看到一些语法，它们看起来非常像纸数学，但是我不理解依赖类型理论的层次，例如：

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

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

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

这是输出：

受保护的def set.sep :Π{α: Type u}，(α→Prop)→setα→αλ{α: Type u} (p :α→Prop) (s : setα)，set_of (λ(a :α)和(has_mem.mem a s) (p ))