Kevin Buzzard (Mar 25 2019 at 14:22):
In section 11.4 of TPIL they talk about quotients. The computational principle is introduced with its
theorem thm : quot.lift f h (quot.mk r a) = f a := rfl
The theorem is given the unilluminating name of
thm. I'm rolling my own quotient structure. Does this theorem have a canonical name? Furthermore, I realise that I also want a variant for my structure where f is Prop-valued and the theorem states
theorem thm' : quot.lift f h (quot.mk r a) ↔ f a
Does this theorem have a canonical name?
The question is this: In section 3.7 of the reference manual they define abstract definitional equality, and then mention (right near the end) that Lean's procedure is "more conservative". But in the formal definition of definitional equality this computational principle for
quot is never mentioned. So it seems to me that Lean's procedure is less conservative in this instance.
Chris Hughes (Mar 25 2019 at 14:26):
I think it might be called
Kevin Buzzard (Mar 25 2019 at 14:32):
Oh indeed! I just looked in core lean and lo and behold it's not called
thm after all :-) So should we call ours
lift_beta? Johan called it
lift_eq which I thought sounded much better.
Last updated: May 12 2021 at 04:19 UTC