## Stream: new members

### Topic: Lean equivalence classes

#### Dan Stanescu (Jul 16 2020 at 15:51):

Working through this textbook example while trying to get used to Lean's interface. Is my goal in the example at the bottom stated correctly? If so, can it be solved with only what I have available or do I need more API for natnat?

import tactic

namespace test

--construct the integers from the natural numbers
@[ext] structure natnat :=
( fst : ℕ )
( snd : ℕ )

namespace natnat

notation ℕ2 := natnat

def ℕ2_zero : ℕ2 := ⟨ 0, 0 ⟩
def ℕ2_another_zero : ℕ2 := ⟨ 3, 3 ⟩
instance : has_zero ℕ2 := ⟨ ℕ2_zero ⟩

def same (a b : ℕ2) : Prop := a.1 + b.2 = a.2 + b.1
instance : has_equiv ℕ2 := ⟨ same ⟩    -- equivalence relation on ℕ2
theorem same_equiv : equivalence same :=
begin
split,
{ -- reflexive:
intros x, unfold same, rw add_comm, },
split,
{ -- symmetric
intros x y hxy, unfold same at *,
exact hxy.symm, },
{ -- transitive
intros x y z H G,
unfold same at *, linarith, }
end

instance : setoid ℕ2 :=
{
r := same,
iseqv := same_equiv }

end natnat

notation myℤ := quotient natnat.setoid

-- def zero : myℤ := ⟦0⟧
def zero : myℤ := ⟦ natnat.ℕ2_zero ⟧
def another_zero : myℤ := ⟦ natnat.ℕ2_another_zero ⟧
example : zero = another_zero := sorry

end test


#### Kevin Buzzard (Jul 16 2020 at 21:12):

open natnat

example : zero = another_zero :=
begin
apply quot.sound,
-- ⊢ setoid.r ℕ2_zero ℕ2_another_zero
-- simp only [setoid.r] is helpful with a goal like this
show natnat.same natnat.ℕ2_zero natnat.ℕ2_another_zero,
show 0 + 3 = 3 + 0,
norm_num
end


#### Dan Stanescu (Jul 16 2020 at 21:24):

I explored the various variants of quotient.lift_on, but it was quot.sound that I missed! Thank you @Kevin Buzzard !

#### Kevin Buzzard (Jul 16 2020 at 21:27):

I am absolutely rubbish at the quotient API -- I will confess that I found it with suggest ;-)

#### Kyle Miller (Jul 16 2020 at 21:27):

Since you're working with quotient, you might also consider quotient.sound, which gives a ≈ b → ⟦a⟧ = ⟦b⟧. This can be convenient since it puts it in terms of your equivalence relation.

(deleted)

#### Dan Stanescu (Jul 16 2020 at 21:32):

Kevin Buzzard said:

I am absolutely rubbish at the quotient API -- I will confess that I found it with suggest ;-)

I also confess that (apparently) I completely forgot about suggest and library_search and was just reading through quot.lean instead. The idea that suggest could find something like this just didn't cross my mind-:(

Last updated: May 15 2021 at 22:14 UTC