Zulip Chat Archive

Stream: new members

Topic: prove that option coercion of value equals (some value)


Kevin Kappelmann (Apr 15 2019 at 11:22):

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 (Apr 15 2019 at 11:23):

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

Kevin Kappelmann (Apr 15 2019 at 11:24):

that is indeed more elegant ;D thank you!

Kevin Buzzard (Apr 15 2019 at 11:25):

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 (Apr 15 2019 at 11:26):

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

Kevin Buzzard (Apr 15 2019 at 11:26):

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

Kevin Buzzard (Apr 15 2019 at 11:27):

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 (Apr 15 2019 at 11:27):

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

Kevin Kappelmann (Apr 15 2019 at 11:29):

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

Johan Commelin (Apr 15 2019 at 11:36):

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

Kevin Kappelmann (Apr 15 2019 at 11:42):

That also works, cheers!

Kevin Buzzard (Apr 15 2019 at 14:29):

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

Kevin Kappelmann (Apr 15 2019 at 14:48):

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


Last updated: Dec 20 2023 at 11:08 UTC