# Zulip Chat Archive

## 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 *,
rw [add_comm, add_comm y.snd _],
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.

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

(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