How does quot work?

Stream: new members

[Julian Gilbey]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

(deleted)

[Bryan Gin-ge Chen]

(deleted)

[Julian Gilbey]

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).

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

[Julian Gilbey]

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 ;-)

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Julian Gilbey]

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.

[Mario Carneiro]

It would not be the same

[Mario Carneiro]

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

[Mario Carneiro]

using set-quotients as in regular math