Zulip Chat Archive

Stream: Is there code for X?

Topic: quot.lift₂


view this post on Zulip Bhavik Mehta (May 23 2020 at 19:06):

There's quotient.lift₂ but I can't see a quot version - does this indicate I should be using quotient instead of quot in my definitions?

view this post on Zulip Kevin Buzzard (May 23 2020 at 19:41):

You should be using quotient' ;-) except that you can't have the notation with that

view this post on Zulip Bhavik Mehta (May 23 2020 at 19:43):

Where's quotient'?

view this post on Zulip Chris Hughes (May 23 2020 at 19:46):

I think quot.lift2 isn't even true. I remember thinking about this once. quotient.lift' and variants use implicit brackets for the setoid argument.

view this post on Zulip Mario Carneiro (May 23 2020 at 19:58):

In case it wasn't obvious, you can always define a binary function on quotients by iterated quot.lift, but you get different proof obligations than the hypothetical quot.lift2.

view this post on Zulip Mario Carneiro (May 23 2020 at 19:59):

You should generally use quotient instead of quot if your relation is in fact an equivalence relation

view this post on Zulip Bhavik Mehta (May 23 2020 at 20:00):

Mario Carneiro said:

In case it wasn't obvious, you can always define a binary function on quotients by iterated quot.lift, but you get different proof obligations than the hypothetical quot.lift2.

Yeah this was why I was initially surprised by not having quot.lift2

view this post on Zulip Bhavik Mehta (May 23 2020 at 20:00):

Mario Carneiro said:

You should generally use quotient instead of quot if your relation is in fact an equivalence relation

Is there a particular reason for this?

view this post on Zulip Mario Carneiro (May 23 2020 at 20:04):

there are better lemmas, like quotient.sound

view this post on Zulip Mario Carneiro (May 23 2020 at 20:04):

and quotient.lift2 for that matter

view this post on Zulip Bhavik Mehta (May 23 2020 at 20:05):

Alright, I was refactoring some definitions code where I used quotient so was thinking about if this would be better - i'll keep the quotients as they are then!

view this post on Zulip Yury G. Kudryashov (May 23 2020 at 21:29):

If you use quotient or quotient', then you tell Lean that your relation is already already an equivalence relation, and later you (and Lean) can use this information to use a simpler reasoning.


Last updated: May 17 2021 at 15:13 UTC