Is quotient special?

Stream: new members

[Walter Moreira]

Is there something special in the quot construction in Lean kernel? I tried to reproduce my own quotient following the declarations in https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients but I don't get the same reduction as the original construction. What is it missing?

universes u v

variables α β : Type
variable  r : α → α → Prop
variable  a : α

variable f : α → β
variable h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂

-- same declarations as TPiL changing quot by my_quot
constant my_quot : Π {α : Sort u}, (α → α → Prop) → Sort u
constant my_quot.mk :
  Π {α : Sort u} (r : α → α → Prop), α → my_quot r
axiom my_quot.ind :
  ∀ {α : Sort u} {r : α → α → Prop} {β : my_quot r → Prop},
    (∀ a, β (my_quot.mk r a)) → ∀ (q : my_quot r), β q
constant my_quot.lift :
  Π {α : Sort u} {r : α → α → Prop} {β : Sort u} (f : α → β),
    (∀ a b, r a b → f a = f b) → my_quot r → β
axiom my_quot.sound :
  ∀ {α : Type u} {r : α → α → Prop} {a b : α},
    r a b → my_quot.mk r a = my_quot.mk r b

#reduce quot.lift f h (quot.mk r a)  -- f a
#reduce my_quot.lift f h (my_quot.mk r a) -- itself

[Bryan Gin-ge Chen]

Yes, it is special. It gets introduced in core Lean with a special keyword: https://github.com/leanprover-community/lean/blob/master/library/init/core.lean#L151

What you're missing is the special reduction rule mentioned there.

[Yury G. Kudryashov]

Yes, reduction rule for lift is implemented in C++.

[Walter Moreira]

So, is my mental model correct if I think on quot.lift f h (quot.mk r a) ~~> f a as an "extra" rule at the same level with the $\beta$, $\eta$, etc. reductions?

[Mario Carneiro]

yes

[Mario Carneiro]

This exact rule is mentioned at https://leanprover.github.io/reference/expressions.html#axioms

[Walter Moreira]

That was useful. Thank, folks!