Sets to types

Stream: new members

[Brandon Brown]

I'm struggling to translate basic set theory constructs into type theory. I'm trying to define disjoint but I believe in type theory all terms only belong to a single type, so generically if I have two types A and B, every a : A is not a term of B, hence they are disjoint in some sort of trivial way. I guess I want to define disjoint using equality? disjoint A B is true if forall a : A, there does not exist b : B such that a = b ?

[Mario Carneiro]

disjoint doesn't make sense as a concept in types

[Mario Carneiro]

when this happens you should #xy analyze the question

[Mario Carneiro]

what caused you to want the ability to say this?

[Brandon Brown]

I'm just trying to do basic set theory stuff in Lean but was told to not use the set type but now I dont know how to proceed

[Mario Carneiro]

that's not #xy enough. What are you trying to do and why

[Mario Carneiro]

if it's just set theory for the sake of set theory, first see whether set A is a better setting, and then ask whether it is needed at all

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/Math.20on.20lists/near/197718432

[Brandon Brown]

I guess I just need to skip these pages. I think I can understand how an equivalence relation can be defined type theoretically quite analogously to the set way. But since things like disjointedness dont make sense, I just shouldnt think in those terms. I can move on and get to defining a group

[Kevin Buzzard]

A bare type behaves exactly in the same way as a set, except that its "elements" are terms (not types, so they don't have elements themselves).

[Brandon Brown]

My goal was to do this exercise in Algebra: Chapter 0: Prove that if ~ is an equivalence relation on a set S, then the corresponding set of equivalence classes is a partition of the set S, i.e. that its elements are nonempty, disjoint and their union is S

[Kevin Buzzard]

So in fact when you learnt equivalence relations in set theory, you took elements $a,b\in X$ and asked if $a\sim b$. But you never asked what $a\cap b$ was, even though this strictly speaking makes sense because at the end of the day, $a$ and $b$ are actually sets. Because you never used this extra setty functionality for $a$ and $b$ and instead just treated them like "atoms" or "terms", this is why it all goes through immediately in type theory.

[Mario Carneiro]

A relation on a set S is a function S -> S -> Prop. It is not a type

[Kevin Buzzard]

That exercise is a joy to do in Lean. Shall we just do it now together?

[Brandon Brown]

Hah yes please

[Mario Carneiro]

It is therefore meaningful to talk about disjointness of equivalence classes (which are S -> Prop, aka set S)

[Kevin Buzzard]

import data.equiv.basic

/-

data.equiv.basic  is the import which gives you the type `equiv X Y`, the type of
bijections from X to Y.

Here's the definition of equiv from that file.

structure equiv (α : Sort*) (β : Sort*) :=
(to_fun    : α → β)
(inv_fun   : β → α)
(left_inv  : left_inverse inv_fun to_fun)
(right_inv : right_inverse inv_fun to_fun)

To make a term of type `equiv α β` you have to supply a function α → β,
a function β → α, and proofs that both composites are the identity function.

Let's see how to create the bijection ℤ → ℤ sending x to -x.
-/
-- let's prove that x ↦ -x can be extended to
example : equiv ℤ ℤ :=
{ to_fun := λ x, -x, -- this is data
  inv_fun := λ x, -x,  -- this is data
  left_inv := begin -- this is a proof
    change ∀ (x : ℤ), - -x = x, -- that's the question
    exact neg_neg, -- note: I guessed what this function was called.
                   -- If it had been called "lemma 12" I would not have been able to guess
  end,
  right_inv := neg_neg -- another proof, this time in term mode
}

/-
Q1 Define the type of partitions of a type.
A partition of X is a set of subsets of X with the property that each subset
is non-empty and each element of X is in precisely one of the subsets.
NB : this is one of the harder questions here.
-/

structure partition (X : Type*). -- remove `.`  and fill in -- look at def of equiv above

/-
Equivalence relations are in core Lean -- we don't need any imports.
Here's an example: I'll prove that the "always true" relation on a set is
an equivalence relation.

-/

def always_true (X : Type*) : X → X → Prop := λ a b, true

-- and now here's the proof that it's an equivalence relation.

theorem always_true_refl (X) : reflexive (always_true X) :=
begin
  intro x,
  trivial
end

theorem always_true_symm (X) : symmetric (always_true X) :=
begin
  intros a b H,
  trivial
end

theorem always_true_trans (X) : transitive (always_true X) :=
begin
  intros a b c Hab Hbc,
  trivial
end

-- note pointy brackets to make a term of type "A ∧ B ∧ C"
theorem always_true_equiv (X): equivalence (always_true X) :=
⟨always_true_refl X, always_true_symm X, always_true_trans X⟩
-- autocomplete made that proof really easy to type. It's really
-- lucky that I didn't call these lemmas lemma 12, lemma 13 and lemma 14.

-- if X is a type, then `setoid X` is is the type of equivalence relations on X.
-- I'll now make a term of type `setoid X` corresponding to that equivalence
-- relation above.

-- note squiggly brackets and commas at the end of each definition to make a structure
def always_true_setoid (X : Type*) : setoid X :=
{ r := always_true X,
  iseqv := always_true_equiv X }

/-
Q2 : If X is a type then `setoid X` is the type of equivalence relations on X,
and `partitions X` is the type of partitions of X. These two concepts are in
some sort of "canonical" bijection with each other (interesting exercise: make
this statement mathematically meaningful -- I know we all say it, but what
does it *mean*?).

Let's prove that these sets biject with each other by defining
a term of type equiv (setoid X) (partitions X)
-/

variable {X : Type*}

def F (S : setoid X) : partition X := sorry

/-
Q3 : now define a map the other way
-/

def G (P : partition X) : setoid X := sorry

/-
Q4 : now finally prove that the composite of maps in both directions
is the identity
-/

theorem FG_eq_id (P : partition X) : F (G P) = P := sorry
theorem GF_eq_id (S : setoid X) : G (F S) = S := sorry

/-
Q5 : now finally construct the term we seek.
-/

def partitions_biject_with_equivalence_relations :
  equiv (setoid X) (partition X) := sorry

[Kevin Buzzard]

Your move @Brandon Brown

[Reid Barton]

Kevin it seems you have played this game before

[Kevin Buzzard]

structure partition (X : Type*) :=
(ℱ : set (set X))
(disjoint : ∀ A B ∈ ℱ, A ≠ B → A ∩ B = ∅)
(cover : ∀ x : X, ∃ A ∈ ℱ, x ∈ A)
(nonempty : ∀ A ∈ ℱ, A ≠ ∅)

[Brandon Brown]

set is a function from Type u \to Type u, that's what someone was telling me earlier that set is a subset?

[Kevin Buzzard]

set X is the type of subsets of X.

[Kevin Buzzard]

A term of type set X should be thought of as a subset of X.

[Kevin Buzzard]

Don't worry about how it's implemented.

[Brandon Brown]

ok

[Kevin Buzzard]

If x : X and S : set X then x ∈ S makes sense and is a Proposition, i.e. a true/false statement.

[Kevin Buzzard]

Reid Barton said:

Kevin it seems you have played this game before

It's some partly-written teaching material.

[Brandon Brown]

Why is def F (S : setoid X) : partition X := sorry giving me an error of "type expected at partition X". An equivalence relation on X implies a partition on X. The def makes sense in english

[Reid Barton]

It makes sense to me too, so it must be for some reason we cannot see.

[Brandon Brown]

I'm reviewing how structures work

[Kevin Buzzard]

import data.equiv.basic

/-

data.equiv.basic  is the import which gives you the type `equiv X Y`, the type of
bijections from X to Y.

Here's the definition of equiv from that file.

structure equiv (α : Sort*) (β : Sort*) :=
(to_fun    : α → β)
(inv_fun   : β → α)
(left_inv  : left_inverse inv_fun to_fun)
(right_inv : right_inverse inv_fun to_fun)

To make a term of type `equiv α β` you have to supply a function α → β,
a function β → α, and proofs that both composites are the identity function.

Let's see how to create the bijection ℤ → ℤ sending x to -x.
-/
-- let's prove that x ↦ -x can be extended to
example : equiv ℤ ℤ :=
{ to_fun := λ x, -x, -- this is data
  inv_fun := λ x, -x,  -- this is data
  left_inv := begin -- this is a proof
    change ∀ (x : ℤ), - -x = x, -- that's the question
    exact neg_neg, -- note: I guessed what this function was called.
                   -- If it had been called "lemma 12" I would not have been able to guess
  end,
  right_inv := neg_neg -- another proof, this time in term mode
}

/-
Q1 Define the type of partitions of a type.
A partition of X is a set of subsets of X with the property that each subset
is non-empty and each element of X is in precisely one of the subsets.
NB : this is one of the harder questions here.
-/

structure partition (X : Type*) :=
(ℱ : set (set X))
(disjoint : ∀ A B ∈ ℱ, A ≠ B → A ∩ B = ∅)
(cover : ∀ x : X, ∃ A ∈ ℱ, x ∈ A)
(nonempty : ∀ A ∈ ℱ, A ≠ ∅)


/-
Equivalence relations are in core Lean -- we don't need any imports.
Here's an example: I'll prove that the "always true" relation on a set is
an equivalence relation.

-/

def always_true (X : Type*) : X → X → Prop := λ a b, true

-- and now here's the proof that it's an equivalence relation.

theorem always_true_refl (X) : reflexive (always_true X) :=
begin
  intro x,
  trivial
end

theorem always_true_symm (X) : symmetric (always_true X) :=
begin
  intros a b H,
  trivial
end

theorem always_true_trans (X) : transitive (always_true X) :=
begin
  intros a b c Hab Hbc,
  trivial
end

-- note pointy brackets to make a term of type "A ∧ B ∧ C"
theorem always_true_equiv (X): equivalence (always_true X) :=
⟨always_true_refl X, always_true_symm X, always_true_trans X⟩
-- autocomplete made that proof really easy to type. It's really
-- lucky that I didn't call these lemmas lemma 12, lemma 13 and lemma 14.

-- if X is a type, then `setoid X` is is the type of equivalence relations on X.
-- I'll now make a term of type `setoid X` corresponding to that equivalence
-- relation above.

-- note squiggly brackets and commas at the end of each definition to make a structure
def always_true_setoid (X : Type*) : setoid X :=
{ r := always_true X,
  iseqv := always_true_equiv X }

/-
Q2 : If X is a type then `setoid X` is the type of equivalence relations on X,
and `partitions X` is the type of partitions of X. These two concepts are in
some sort of "canonical" bijection with each other (interesting exercise: make
this statement mathematically meaningful -- I know we all say it, but what
does it *mean*?).

Let's prove that these sets biject with each other by defining
a term of type equiv (setoid X) (partitions X)
-/

variable {X : Type*}

def F (S : setoid X) : partition X := sorry

/-
Q3 : now define a map the other way
-/

def G (P : partition X) : setoid X := sorry

/-
Q4 : now finally prove that the composite of maps in both directions
is the identity
-/

theorem FG_eq_id (P : partition X) : F (G P) = P := sorry
theorem GF_eq_id (S : setoid X) : G (F S) = S := sorry

/-
Q5 : now finally construct the term we seek.
-/

def partitions_biject_with_equivalence_relations :
  equiv (setoid X) (partition X) := sorry

This file works for me.

[Kevin Buzzard]

If that exact file is giving you errors then update your Lean and mathlib.

[Brandon Brown]

Okay it's working now. I must have accidentally messed something up

[Kevin Buzzard]

Feel free to write the official solutions; I don't seem to have written them down.

[Kevin Buzzard]

I have official solutions for a completely different teaching file on the same material, with far fewer comments. If you've played the natural number game and you know how to make a term whose type is a structure (hint: write := {! !} and then click on the light bulb and select the bottom but one option, assuming some mathlib is imported).

[Brandon Brown]

I had to go through the natural number game first before attempting this. I have some unsightly proofs of G and F. Still working on proving they compose to identity.

import data.setoid
import data.equiv.basic
open set
open setoid

structure partition (X : Type*) :=
(F : set (set X))
(disjoint : ∀ A B ∈ F, A ≠ B → A ∩ B = ∅)
(cover : ∀ x : X, ∃ A ∈ F, x ∈ A)
(nonempty : ∀ A ∈ F, A ≠ ∅)

def F {X : Type*} (S : setoid X) : partition X :=
partition.mk
(
     classes S
)
( -- ⊢ (disjoint : ∀ A B ∈ ℱ, A ≠ B → A ∩ B = ∅)
  begin
    intros,
    apply eq_of_subset_of_subset,
    {
      intro x,
      intros,
      rw mem_empty_eq,
      apply a,
      cases a_1,
      --have F : set (set X), from classes S,
      apply eq_of_mem_classes,
      repeat {assumption},
    },
    {
      apply set.empty_subset,
    }
  end
)
( -- ⊢ (cover : ∀ x : X, ∃ A ∈ ℱ, x ∈ A)
  begin
    intros,
    split,
    use x,
    simp,
  end
)
( -- ⊢ (nonempty : ∀ A ∈ ℱ, A ≠ ∅)
  begin
    intros,
    intro aqn,
    apply empty_not_mem_classes,
    rwa ← aqn,
  end
)
#check F

/-
Q3 : now define a map the other way
-/

def G {X : Type*} (P : partition X) : setoid X :=
begin
    intros,
    apply setoid.setoid_of_disjoint_union,
    swap 3,
    exact P.F,
    apply eq_of_subset_of_subset,
    intro p1,
    intros,
    trivial,
    intro p1,
    intros,
    dsimp at *,
    apply P.cover,
    unfold set.pairwise_disjoint,
    unfold set.pairwise_on,
    intros,
    unfold disjoint,
    have z : x ∩ y = ∅, apply P.disjoint,
    repeat {assumption},
    finish,
end

[Kevin Buzzard]

Oh thanks! You'll need two proofs of course, one for each round trip. Then you're done

[Kevin Buzzard]

You should probably be using structure notation to make these structures though. I am busy with real life right now unfortunately

[Brandon Brown]

You made a partition structure as follows

structure partition (X : Type*) :=
(F : set (set X))
(disjoint : ∀ A B ∈ F, A ≠ B → A ∩ B = ∅)
(cover : ∀ x : X, ∃ A ∈ F, x ∈ A)
(nonempty : ∀ A ∈ F, A ≠ ∅)

To prove two partitions are equal, I assume I have to make my own .ext definition?

[Bryan Gin-ge Chen]

It'll be a lemma, but yeah.

[Bryan Gin-ge Chen]

Back in 2018, I wrote some code on partitions (with a lot of help from folks here, especially Simon Hudon, see e.g. this thread) in a "tutorials" branch: https://github.com/leanprover-fork/mathlib-backup/blob/tutorials/tutorials/partitions.lean

I think some of the code eventually made it in to data.setoid.partition but not the partition structure. The code was written when I knew a lot less about Lean, so there are probably lots of things which are done poorly. Nonetheless, I tried to write a lot of comments, so you might find it interesting.

It's based on a very old version of mathlib (using the now-ancient Lean 3.4.1!) but leanproject and elan should make it fairly easy to get it up and running (modulo some compiling time):

leanproject get https://github.com/leanprover-fork/mathlib-backup:tutorials
cd mathlib-backup_tutorials
# this is a version of mathlib from before we started uploading oleans to the cloud,
# so unfortunately you'll have to do some compiling yourself
lean --make tutorials/partitions.lean

Then you can open up mathlib-backup_tutorials/ in VS Code and then look at tutorials/partitions.lean.

[Brandon Brown]

very helpful, thank you!

[Scott Morrison]

Actually, you can just write @[ext] immediately before the structure, and you'll get an automatically generated ext lemma. It may not be the one you actually want.