Zulip Chat Archive

Stream: Is there code for X?

Topic: quotient.exists_rep without a typeclass instance


view this post on Zulip Eric Wieser (Dec 07 2020 at 17:32):

Is there a reason docs#quotient.exists_rep takes [s : setoid A] and not {s : setoid A}? I have a quotient constructed from a non-canonical setoid, so I don't have a global instance available.

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:33):

docs#quotient.exists_rep' ?

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:33):

no :(

Then docs#quot.exists_rep

view this post on Zulip Eric Wieser (Dec 07 2020 at 17:33):

I wonder what breaks if those arguments all become implicit...

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:34):

I don't think anything breaks. quotient.mk' is defeq to quot.mk _

view this post on Zulip Eric Wieser (Dec 07 2020 at 17:35):

Oh, the problem is this code is all in core

view this post on Zulip Eric Wieser (Dec 07 2020 at 17:35):

So changing it to take {} arguments is harder to test

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:36):

src#quotient.lift_on'

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:36):

That's from mathlib, and it looks like a few other quotient.foo' things are missing as well.

view this post on Zulip Eric Wieser (Dec 07 2020 at 17:39):

Ugh, I guess exists_rep' is difficult because the ⟦a⟧ notation used in its statement isn't available without the typeclass instance.

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:40):

It could use quotient.mk'

view this post on Zulip Adam Topaz (Dec 07 2020 at 17:42):

def quotient.exists_rep' {α : Type*} {S : setoid α} (x : quotient S) :  (a : α), quotient.mk' a = x :=
  quot.exists_rep _

view this post on Zulip Eric Wieser (Dec 07 2020 at 18:00):

Oh, which infers s from the rhs

view this post on Zulip Adam Topaz (Dec 07 2020 at 19:00):

It infers S from the type of x

view this post on Zulip Eric Wieser (Dec 07 2020 at 20:36):

Right, I mean the inferred argument to mk'

view this post on Zulip Eric Wieser (Dec 07 2020 at 22:04):

Thanks for the tip to use the quot versions anyway, that tidied up my proof nicely.

view this post on Zulip Adam Topaz (Dec 07 2020 at 22:13):

IMO the main point where quotient is useful over quot is if you have to use quotient.exact. quot.exact spits out something with eqv_gen which is annoying if you already have an equivalence relation


Last updated: May 07 2021 at 22:14 UTC