Zulip Chat Archive

Stream: new members

Topic: Lean equivalence classes


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 !

view this post on Zulip 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 ;-)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 16 2020 at 21:29):

(deleted)

view this post on Zulip 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