Looking for Explicit Axiom for Simplification in Quot

Stream: lean4

[Lingwei Peng (彭灵伟)]

I find that the example in the tutorial (https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#quotients):

example (a : Nat) : Quot.lift f f_respects (Quot.mk mod7Rel a) = f a :=
  rfl

uses the feature that the kernel automatically simplifies Quot.lift f f_respects (Quot.mk mod7Rel a) into f a. Is there an explicit axiom for the Quot type that justifies this simplification behavior? Specifically, I am looking for an explicit axiom that connects Quot.lift and Quot.mk in this manner, instead of relying on the kernel’s implicit behavior.

[Kyle Miller]

There's no axiom in the axiom sense at least.

You should take a look at the docstrings in the Prelude: https://github.com/leanprover/lean4/blob/e9f2e1861e746c2aba134215e56fcd6e7eb62d50/src/Init/Prelude.lean#L382-L440

These are all part of the definition of quotients. You should think of it as being why inductive recursors have simplification rules too. Their definitional equality properties are part of the theory.

[Kyle Miller]

(When I skimmed it, I didn't find the reduction rule at first, but rereading I see it's on the Quot.lift docstring in words.)

[Kyle Miller]

If you want the justification for this rule, a way to think about it is that Quot X is "X with a different Eq". That's to say, Quot X can be represented as X itself, but (1) you're allowed to prove that more things are Eq than there "really" are (using the relation), and (2) if you have a function f : X -> Y with the property that f x = f y whenever x is related to y, then it's safe to make a function Quot X -> Y that evaluates f on the underlying X element of the Quot X element. That is, we can have a reduction rule where Quot.lift f pf (Quot.mk R x) evaluates to f x.

[Lingwei Peng (彭灵伟)]

Thanks