## Stream: new members

### Topic: equivalence classes and quotients

#### Thomas Laraia (Jul 22 2021 at 09:44):

Is there a good way to reconcile the difference of set (ℕ × ℕ) and ↥ourInt when defining pre_add? Dealing with the equivalence class of an element being in the powerset of all the elements.

import tactic

def is_refl_type {X:Type}(S: X→ X→ Prop):=
∀ a:X, S a a

def is_symm_type {X:Type}(S: X→ X→ Prop):=
∀ a b:X, S a b→ S b a

def is_trans_type {X:Type}(S:X→ X→ Prop):=
∀ a b c:X, S a b→ S b c→ S a c

def is_equiv_type {X:Type}(S:X→ X→ Prop):=
is_refl_type S ∧ is_symm_type S
∧ is_trans_type S

def equiv_class_type {X:Type}(S:X→ X→ Prop)(a:X):set X
:= {x:X | S x a}

def quotient_type {X:Type}(S:X→ X→ Prop):=
{e:set X | ∃ a:X, e=equiv_class_type S a}

def diff : ℕ × ℕ → ℕ × ℕ → Prop :=
λ a, λ b, a.fst + b.snd = a.snd + b.fst

lemma diff_is_refl : is_refl_type diff :=
begin
unfold is_refl_type, /-just for our sanity-/
intro a,
unfold diff,
end

lemma diff_is_symm : is_symm_type diff :=
begin
unfold is_symm_type, /-sanity-/
intros a b,
intro h,
unfold diff at *,
symmetry,
exact h,
end

lemma diff_is_trans : is_trans_type diff :=
begin
unfold is_trans_type,
intros a b c,
intro h1,
intro h2,
unfold diff at *,
/-have h1h2 : (a.fst + b.snd) + (b.fst + c.snd) = (a.snd + b.fst) + (b.snd + c.fst) := by add_two_eq (a.1 + b.2) (a.2 + b.1) (b.1 + c.2) (b.2 + c.1) h1 h2,-/
have h3 : a.1 + b.2 + c.2 = a.2 + b.1 + c.2,
rw h1,
rw h2 at h3,

rw add_comm b.2 c.1 at h3,

exact g,
end

lemma diff_is_equiv : is_equiv_type diff :=
begin
unfold is_equiv_type,
split,
exact diff_is_refl,
split,
exact diff_is_symm,
exact diff_is_trans,
end

lemma equiv_class_type_in_quotient_type {X : Type} (S: X → X → Prop) (a : X) :
equiv_class_type S a ∈ quotient_type S :=
begin
use a,
end

def ourInt := quotient_type diff

def pre_add : ℕ × ℕ → ℕ × ℕ → ourInt :=
λ a, λ b, equiv_class_type diff (a.1 + b.1, a.2 + b.2)


#### Anne Baanen (Jul 22 2021 at 14:58):

The error almost says the solution: you have a set (ℕ × ℕ) and you need to provide an ↥ourInt. If you unfold the definition of ↥ in this case, you'll see that it's subtype (∈ quotient_type S), i.e. the type of all elements s : set X together with a proof that s ∈ quotient_type S. Constructing an element of subtype p is done with ⟨x, hx⟩, where hx is a proof of p x.

So the first step is to replace the definition of pre_add with:

def pre_add : ℕ × ℕ → ℕ × ℕ → ourInt :=
λ a, λ b, ⟨equiv_class_type diff (a.1 + b.1, a.2 + b.2), sorry⟩


#### Thomas Laraia (Jul 22 2021 at 15:53):

How did you go about unfolding the definition of ↥ here?

#### Kevin Buzzard (Jul 22 2021 at 16:14):

you can use the infoview to figure out what these arrows mean. But in this case it's not hard -- quotient_type S is a set and this is a pretty standard coercion from set X to Type, sending the set to the corresponding subtype.

#### Thomas Laraia (Jul 22 2021 at 16:17):

Ah I'll keep messing with the infoview, with the error that came up I was unable to press on the up arrow or expand anything so I thought I'd ask.
Cheers for the help.

#### Kevin Buzzard (Jul 22 2021 at 16:21):

yeah, you need to catch it before the error :-)

#### Thomas Laraia (Jul 22 2021 at 16:24):

I guess all I have left to ask is how to get from has_coe_to_sort.S (set (set (ℕ × ℕ))) to subtype (∈ quotient_type S).

#### Yakov Pechersky (Jul 22 2021 at 17:36):

Well, do you have a proof that some s : (set (ℕ × ℕ)) satisfies quotient_type S?

#### Yakov Pechersky (Jul 22 2021 at 17:51):

def pre_add : ℕ × ℕ → ℕ × ℕ → ourInt :=
λ a b, -- we can introduce both tuples at the same time
-- we construct our term ourInt, which is a combination of data (the value)
-- and the proof that is has the property we require
⟨equiv_class_type diff (a.1 + b.1, a.2 + b.2), -- this is our data
-- now we give a proof that it satisfies our condition of
-- equiv_class_type diff (a.fst + b.fst, a.snd + b.snd) ∈ ourInt
-- but all that requires is constructing a tuple that is diff to the one we gave in the data
-- and a proof that they are diff
-- so again we provide a combination of data and proof
⟨(a.1 + b.1, a.2 + b.2), -- our compared tuple, which we can make the same for simplicity
rfl⟩⟩ -- and the proof, which is that they are the same _by definition_, which is written rfl


#### Thomas Laraia (Jul 23 2021 at 09:07):

Ah yeah sorted that part just didn't know how to apply it.

lemma equiv_class_type_in_quotient_type {X : Type} (S: X → X → Prop) (a : X) :
equiv_class_type S a ∈ quotient_type S :=
begin
use a,
end


I mean I didn't see the wording subtype (∈ quotient_type S)` in the infoview.
I've got pre_add to work now, just asking for the future where to find that type of wording or if it is concluded from something else.

Last updated: Dec 20 2023 at 11:08 UTC