Zulip Chat Archive

Stream: new members

Topic: eliminating self coercion


view this post on Zulip Duckki Oe (Oct 31 2020 at 18:21):

How can I reduce (@coe _ _ lift_self x) to x?

variables {A : Type}

-- I can do it with `cast`
example (x : A) : (cast rfl x) = x
:= begin
    refl,
end

lemma lift_self: has_lift_t A A := by split; tautology

example (x : A) : (@coe _ _ lift_self x) = x
:= begin
    sorry,
end

view this post on Zulip Bryan Gin-ge Chen (Oct 31 2020 at 18:25):

I'm not sure what you mean. In your examples, you postulate a term x of type A, (written (x : A) for short). What exactly do you want to reduce x to?

view this post on Zulip Duckki Oe (Oct 31 2020 at 18:27):

Sorry for confusion. I wrote (x : A) as a shorthand for (@coe _ _ lift_self x). I'd like to reduce it to x.

view this post on Zulip Reid Barton (Oct 31 2020 at 18:29):

Don't use lemma for lift_self, use def instead

view this post on Zulip Duckki Oe (Oct 31 2020 at 18:29):

Thanks, @Reid Barton . That was it.

view this post on Zulip Bryan Gin-ge Chen (Oct 31 2020 at 18:32):

We have a linter that warns you if lemmas should be defs and vice versa. Unfortunately, it has to be called manually at the moment:

import tactic

variables {A : Type}
lemma lift_self: has_lift_t A A := by split; tautology
#lint
/-
/- Checking 1 declarations (plus 0 automatically generated ones) in the current file -/

/- The `def_lemma` linter reports: -/
/- INCORRECT DEF/LEMMA: -/
#print lift_self /- is a lemma/theorem, should be a def -/
-/

view this post on Zulip Duckki Oe (Oct 31 2020 at 18:42):

I see. Thanks! @Bryan Gin-ge Chen


Last updated: May 08 2021 at 10:12 UTC