Lean equivalence classes

Stream: new members

[Dan Stanescu]

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]

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]

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

[Kevin Buzzard]

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

[Kyle Miller]

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]

(deleted)

[Dan Stanescu]

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-:(