Zulip Chat Archive

Stream: new members

Topic: Unfolding function coercion


view this post on Zulip Jean-Philippe Burelle (Oct 09 2020 at 12:38):

I've been scratching my head over this simple problem :
If I define a structure and give it a coercion to functions, like this :

structure my_fun :=
    (f :    )

instance : has_coe_to_fun (my_fun) :=
_, λ fct, fct.f 

and then define an instance

def square : my_fun :={
    f := λ u, u*u,
}

I don't know what the right way to unfold these definitions is in a proof. In the interactive prover, when I try to prove this lemma :

lemma test : square 1 = 1 :=
begin
end

I can use unfold_coes to turn ⇑square 1 into square.f 1, but I don't know how to unfold this function. If I try unfold square.f I get square.f does not have equational lemmas nor is a projection.

I have found that if I use rw square, after unfolding the function coercion, the goal becomes ⇑{f := λ (u : ℝ), u * u} 1 = 1, which I also don't know how to unfold, but simp will complete the goal. Even more confusingly, if I don't unfold the function coercion and directly use rw square on ⇑square 1, the goal becomes identical ⇑{f := λ (u : ℝ), u * u} 1 = 1, but now simp doesn't close it!

view this post on Zulip Chris Hughes (Oct 09 2020 at 12:40):

Have you tried unfold my_fun.f?

view this post on Zulip Chris Hughes (Oct 09 2020 at 12:40):

Actually unfold square my_fun.f

view this post on Zulip Jean-Philippe Burelle (Oct 09 2020 at 12:43):

Thank you! This works, and unfold my_fun.f square does the same thing. I would have thought square.f was short for my_fun.f square but apparently not.

view this post on Zulip Chris Hughes (Oct 09 2020 at 12:44):

It is short for my_fun.f square, but you can only unfold declarations, and my_fun.f square is not a declaration, but both square and my_Fun.f are

view this post on Zulip Chris Hughes (Oct 09 2020 at 12:47):

I see where you misunderstood unfold my_fun.f square is like unfold my_fun.f, unfold square.

view this post on Zulip Chris Hughes (Oct 09 2020 at 12:48):

my_fun.f and Square are two separate arguments,

view this post on Zulip Jean-Philippe Burelle (Oct 09 2020 at 12:57):

How should I think of the expression square.f ? Its type is ℝ → ℝ but unfold gives an error.

view this post on Zulip Reid Barton (Oct 09 2020 at 13:02):

I'm not sure what to add to what Chris already wrote. unfold doesn't take an expression, it takes a list of constants.


Last updated: May 18 2021 at 16:25 UTC