Zulip Chat Archive

Stream: new members

Topic: How does quot work?


view this post on Zulip Julian Gilbey (Dec 14 2019 at 18:29):

I'm struggling to understand how quot actually works. We have the definitions of quot.mk and quot.ind (in the core, they also appear as a comment in init/core.lean), namely

constant quot.mk {α : Sort u} (r : α  α  Prop) (a : α) : quot r

constant quot.lift {α : Sort u} {r : α  α  Prop} {β : Sort v} (f : α  β) :
  ( a b : α, r a b  eq (f a) (f b))  quot r  β

But from there, in init/data/quot.lean, we have the lemma:

protected lemma lift_beta {α : Sort u} {r : α  α  Prop} {β : Sort v} (f : α  β) (c :  a b, r a b  f a = f b) (a : α) : lift f c (quot.mk r a) = f a :=
rfl

So it seems as though Lean can deduce that quot.lift does exactly what we want it to. Yet the definition only seems to specify the type of quot.lift as quot r → β but without specifying the behaviour on things of type quot r. My guess is that the only possible meaning that could be given to the function is the one we expect, rather than something like a constant function. But I'm clearly missing something here, yet I don't even know what I don't understand. Help please?

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 18:30):

Did you look at the relevant section of Theorem Proving in Lean?

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 18:30):

I implemented quotients myself as equivalence classes and this exercise taught me a lot about what was going on

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 18:32):

axiom quot.sound :
   {α : Type u} {r : α  α  Prop} {a b : α},
    r a b  quot.mk r a = quot.mk r b

is the axiom which tells you that quot.mk is what you think it should be

view this post on Zulip Reid Barton (Dec 14 2019 at 18:32):

The thing that makes lift_beta work is called the computation rule for quot and it's also magically added by init_quotient

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 18:33):

For me, part of the problem was that the names of the functions in Lean are very unlike the ones which I would use. For example quot.lift doesn't lift a map from the quotient to a map on the original type, it descends a map on the type which plays well with the equivalence relation to a map on the quotient.

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 18:33):

Another thing that helped was working out one explicit example, which I did here: https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 18:52):

(deleted)

view this post on Zulip Bryan Gin-ge Chen (Dec 14 2019 at 19:08):

(deleted)

view this post on Zulip Julian Gilbey (Dec 14 2019 at 21:23):

The thing that makes lift_beta work is called the computation rule for quot and it's also magically added by init_quotient

Thanks @Reid Barton - that makes a lot of sense. The relevant section of Theorem Proving in Lean doesn't explain this point, though I've just found that in the reference manual, it says explicitly: quot.mk and quot.lift satisfy the following computation rule:

quot.lift f h (quot.mk r a) = f a

So this interpretation does seem to be built into the core (though I couldn't locate the actual code which does so).

view this post on Zulip Bryan Gin-ge Chen (Dec 14 2019 at 21:53):

The Lean code is here, but as you can see that just calls a special init_quotient function which eventually calls this C++ function.

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 22:13):

Yes the computation rule is a definitional equality by Leo's clever definition of rfl. This is precisely what falls if you roll your own

view this post on Zulip Julian Gilbey (Dec 14 2019 at 22:19):

Yes, I found that C++ function, but I don't understand how the computation rule was implied by it :-( Anyway, knowing that it is definitionally built into Lean means I can stop worrying about it ;-)

view this post on Zulip Mario Carneiro (Dec 14 2019 at 23:10):

The computation rule comes from the implementation of quotient_normalizer_extension::operator() in the same file

view this post on Zulip Mario Carneiro (Dec 14 2019 at 23:11):

it is an extension to the whnf function that checks if the target has the form @quot.lift α r β f h (@quot.mk α r a) and replaces it with f a

view this post on Zulip Mario Carneiro (Dec 14 2019 at 23:14):

It also reduces @quot.ind α r β f (@quot.mk α r a) to f a, even though this is mostly unnecessary because of proof irrelevance

view this post on Zulip Julian Gilbey (Dec 15 2019 at 07:31):

Wow, thanks @Mario Carneiro! I certainly didn't understand that function first time round, not knowing the internals of the source code! It is also necessary for things to work correctly, as the following throws an error:

universes u v

constant myquot {α : Sort u} (r : α  α  Prop) : Sort u

constant myquot.mk {α : Sort u} (r : α  α  Prop) (a : α) : myquot r

constant myquot.lift {α : Sort u} {r : α  α  Prop} {β : Sort v} (f : α  β) :
  ( a b : α, r a b  eq (f a) (f b))  myquot r  β

lemma mylift_beta {α : Sort u} {r : α  α  Prop} {β : Sort v} (f : α  β) (c :  a b, r a b  f a = f b) (a : α) : myquot.lift f c (myquot.mk r a) = f a :=
rfl

I haven't tried to see whether changing mylift_beta into an axiom would make other proofs work, but that's not something I'm particularly interested in doing.

view this post on Zulip Mario Carneiro (Dec 15 2019 at 07:32):

It would not be the same

view this post on Zulip Mario Carneiro (Dec 15 2019 at 07:32):

You can prove the existence of constants satisfying everything except the computation rule without any extensions

view this post on Zulip Mario Carneiro (Dec 15 2019 at 07:33):

using set-quotients as in regular math


Last updated: May 14 2021 at 06:16 UTC