## Stream: new members

### Topic: Is quotient special?

#### Walter Moreira (May 18 2020 at 02:59):

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 (May 18 2020 at 03:02):

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 (May 18 2020 at 03:02):

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

#### Walter Moreira (May 18 2020 at 03:13):

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?

yes

#### Mario Carneiro (May 18 2020 at 03:22):

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

#### Walter Moreira (May 18 2020 at 03:25):

That was useful. Thank, folks!

Last updated: May 14 2021 at 12:18 UTC