the computation principle for quotient proved via rfl?

Stream: general

[Coriver Chen]

I saw theorem thm : quot.lift f h (quot.mk r a) = f a := rfl in https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html but cannot see how it's a reflection of equality #general

[Coriver Chen]

constant quot.lift : Π {α : Sort u} {r : α → α → Prop} {β : Sort u} (f : α → β), (∀ a b, r a b → f a = f b) → quot r → β only says quot.lift f h having type quot r → β, but does not say how it's defined?

[Eric Wieser]

(deleted)

[Eric Wieser]

docs4#Quot.sound has an explanation of what's going on, for Lean 4

[Eric Wieser]

Lean 3 is similar, but I think missing the documentation: docs#quot.sound

[Coriver Chen]

Thank you. I am reading the linked docs

[Eric Wieser]

I think the summary is that the kernel itself has special support and reduction rules for those declarations, meaning you will need to look deep inside lean to find out "why" the proof you quoted works

[Reid Barton]

BTW the situation is not so different from an ordinary inductive type, it's just that Lean has hard-coded knowledge that it should add the "action on equalities" hypothesis to the type of quot.lift, which justifies the addition of the axiom quot.sound.

[Kevin Buzzard]

(deleted)

[Coriver Chen]

I still have some difficulties in understanding it. Now maybe I get the quot.sound axiom. But may I ask how is f involved in the theorem? It seems if there is some other f' satisfying f' a = f' b , is it ok taking quot.lift f h (quot.mk r a) to f' a? I have some background in programing languages like java or python, and some background in math but little in type theory and very new to lean prover. I can feel it seems different to prove 2+3=5 using reflection.

[Eric Wieser]

Where are you seeing f'?

[Eric Wieser]

It does look like the docs at Quot.sound don't actually mention that the opaque definitions satisfy lift f h (mk x) = f x, which arguably is also being added as an axiom (but not a true axiom in the keyword sense of the word)

[Coriver Chen]

Emm indeed there is no such f' mentioned. I don't have an enviroment for running codes now. What if I change the signature to constant quot.lift_f_and_f': Π {α : Sort u} {r : α → α → Prop} {β : Sort u} (f : α → β), (f': α → β), (∀ a b, r a b → f a = f b) → (∀ a b, r a b → f' a = f' b) → quot r → β ? Then we cannot give a proof for this right?

[Coriver Chen]

Anyway since I am learning lean with TPIL as a first tutorial, taking it as an axiom seems good for me. Maybe I can come back to this after being more familiar. Thank you very much Eric

[Kevin Buzzard]

The rfl behaviour of quot.liftthat you've observed is baked into Lean's kernel -- it is an axiom of the system. If you add another constant then it won't have the same behaviour.

[Rémi Bottinelli]

As an aside, something I found kind of confusing in TPIL was that they don't make explicit the fact that quot.lift and quot.ind are two constant, each with its own "baked-in" computation rule.