Zulip Chat Archive

Stream: general

Topic: name for, and question about, computational principle

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 rfl proof.

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 quot.lift_beta

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: Aug 03 2023 at 10:10 UTC