Zulip Chat Archive

Stream: new members

Topic: Is quotient special?


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 03:02):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 18 2020 at 03:22):

yes

view this post on Zulip Mario Carneiro (May 18 2020 at 03:22):

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

view this post on Zulip Walter Moreira (May 18 2020 at 03:25):

That was useful. Thank, folks!


Last updated: May 14 2021 at 12:18 UTC