equivalence classes and quotients

Stream: new members

[Thomas Laraia]

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,
  rw add_comm,
end

lemma diff_is_symm : is_symm_type diff :=
begin
  unfold is_symm_type, /-sanity-/
  intros a b,
  intro h,
  unfold diff at *,
  symmetry,
  rw add_comm,
  rw add_comm b.fst,
  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 add_assoc a.2 at h3,
  rw h2 at h3,

  rw add_comm at h3,
  rw add_comm b.2 c.1 at h3,
  rw ← add_assoc at h3,
  rw ← add_assoc at h3,

  have g := add_right_cancel h3,
  rw add_comm,
  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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Thomas Laraia]

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]

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

[Yakov Pechersky]

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]

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.