prove that option coercion of value equals (some value)

Stream: new members

[Kevin Kappelmann]

Is there any "pretty" proof that coercing a value to an option type equals (some value)? For example, is there a more elegant way to prove the following example?

example {α: Type*} (val: α) : (λ (x: option α), x) val = (some val) :=
by simp [coe, lift_t, has_lift_t.lift, coe_t, has_coe_t.coe]

[Kevin Buzzard]

example {α: Type*} (val: α) : (λ (x: option α), x) val = (some val) := rfl

[Kevin Kappelmann]

that is indeed more elegant ;D thank you!

[Kevin Buzzard]

My thought process:

example {α: Type*} (val: α) : (λ (x: option α), x) val = (some val) :=
begin
 -- not sure how to proceed, so let's start to unfold
 unfold coe,
 unfold lift_t,
 unfold has_lift_t.lift,
 unfold coe_t,
 unfold has_coe_t.coe,
 -- hey, the goal automatically got solved!
 -- And "unfold" didn't really do anything apart from changing things
 -- to definitionally equal things.
 -- So maybe `rfl` worked right from the start!
end

[Kevin Buzzard]

I should probably not confess this, but I often write code like this.

[Kevin Buzzard]

When I'm not entirely sure how coercions are defined, I just unfold them manually like this

[Kevin Buzzard]

and then when I've got to the actual definition, I look at the goal, copy it, write change [insert goal here] and then delete all the unfolds.

[Kevin Buzzard]

change (and show, they do the same thing) changes the goal to something definitionally equal.

[Kevin Kappelmann]

Ah, I did not know about the change keyword. Nice to know :)

[Johan Commelin]

There is unfold_coes. Maybe if would have done all those unfolds in one go.

[Kevin Kappelmann]

That also works, cheers!

[Kevin Buzzard]

PS you can write (λ (x: option α), x) val as (val : option α)

[Kevin Kappelmann]

Oh, I knew that one can do that, but for some reason, I did not use it here. Thanks again Kevin! :)