More set theoretic proofs in Lean
We’ve seen an example where the goal is to give a proof of an equality of sets. Both in Lean and with pen-and-paper, to show two sets are equal X=Y
we use set extensionality to reduce to establishing ∀ x, x ∈ X ↔ x ∈ Y
. We then take some x ∈ U
, prove one direction x ∈ X → x ∈ Y
, and then the other x ∈ Y → x ∈ X
.
While for pen-and-paper everyone can just do this conversion “in their head”, in Lean we need to step the computer through each time. This can be tedious so we automate it. For that, we can use a tactic called set_extensionality
.
variable (U : Type)
variable (X Y : Set U)
example : X = Y :=
set_extensionality x
-- we now have x:U
-- and two goals x ∈ X → x ∈ Y and x ∈ X → x ∈ Y
-- we sorry these goals because we cannot prove two sets are
-- equal in general
. sorry
. sorry
set_extensionality
helps us when proving a goal of the form X=Y
. What if we have a hypothesis of set equality?
variable (x:U)
variable (X Y Z : Set U)
example (h: X = Y) : X ∪ Z = Y ∪ Z := by
rewrite [h]
rfl
Rewriting the goal with the assumption X=Y
produces a new goal X ∪ Z = X ∪ Z
. Recall the tactic rfl
solves goals of the form t = t
. We can also use rw
in place of rewrite
and rfl
as rw
does a rewrite and then calls rfl
.
Let’s see another one.
variable (U : Type)
variable (X Y : Set U)
example (h : X ⊆ Y) : Z \ Y ⊆ Z \ X := by
intro (x:U) (g : x ∈ Z \ Y)
have : x ∉ X := sorry
exact ⟨g.left,this⟩
The only thing left is to fill in the sorry
. Knowing that if X ⊆ Y
and x ∉ Y
, then x ∉ X
seems like a useful result itself. We give it a name and then use it. (Remember that given h : A ∧ B
we can access a proof of A
using h.left
and a proof of B
using h.right
.)
variable (U : Type)
variable (X Y : Set U)
theorem sub_comp_super (h : X ⊆ Y) : Yᶜ ⊆ Xᶜ := by
intro (x : U) (g : x ∈ Yᶜ) (n : l ∈ X)
exact g (h x l)
example (h : X ⊆ Y) : Z \ Y ⊆ Z \ X := by
intro (x:U) (g : x ∈ Z \ Y)
have : x ∉ X := sub_comp_super h x g.right
exact ⟨g.left,this⟩
Next we look at the distributivity of intersection over unions.
variable (U : Type)
variable (X Y Z : Set U)
theorem dist_inter_union : X ∩ (Y ∪ Z) = (X ∩ Y) ∪ (X ∩ Z) := by
set_extensionality x
· intro (h : x ∈ X ∩ (Y ∪ Z))
cases h.right with
| inl (g : x ∈ Y) => exact Or.inl ⟨h.left,g⟩
| inr (g : x ∈ Z) => exact Or.inr ⟨h.left,g⟩
· intro (h : x ∈ (X ∪ Y) ∩ (X ∩ Z))
cases h with
| inl (g : X ∩ Y) => exact ⟨g.left,Or.inl g.right⟩
| inr (g : X ∩ Z) => exact ⟨g.left,Or.inr g.right⟩
In place of an apply Or.elim
, we have used the cases
tactic. This tactic creates different proof goals for each way there is to build the term. In our case, h.right : x ∈ Y ∪ Z
which is definitionally equivalent to x ∈ Y ∨ x ∈ Z
. There are two ways to make a proof of an or-statement: either you have a proof of the left and use .inl
or you have a proof the right and use .inr
. These constructors are the labels for the two branches of the cases. Note that cases
comes with additional syntax: with
and the |
to label the branches.
Here is an example with the use of cases
for the existential quantifer.
variable (I U : Type)
variable (X Y : I → Set U)
example (h : ∃ (i:I), X i ∩ Y i = ∅) : BigInter X ∩ BigInter Y = ∅ := by
set_extensionality x
· intro (g : x ∈ BigInter X ∩ BigInter Y)
cases h with
| intro (i : I) (g₁ : X i ∩ Y i = ∅) =>
have g₂ : x ∈ X i := g.left i
have g₃ : x ∈ Y i := g.right i
have g₄ : x ∉ X i ∩ Y i := by
rw [g₁]
exact fun h => False.elim h
exact g₄ ⟨g₂,g₃⟩
· exact fun h => False.elim h