eliminating self coercion

Stream: new members

[Duckki Oe]

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

[Bryan Gin-ge Chen]

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?

[Duckki Oe]

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

[Reid Barton]

Don't use lemma for lift_self, use def instead

[Duckki Oe]

Thanks, @Reid Barton . That was it.

[Bryan Gin-ge Chen]

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 -/
-/

[Duckki Oe]

I see. Thanks! @Bryan Gin-ge Chen