Unfolding function coercion

Stream: new members

[Jean-Philippe Burelle]

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!

[Chris Hughes]

Have you tried unfold my_fun.f?

[Chris Hughes]

Actually unfold square my_fun.f

[Jean-Philippe Burelle]

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.

[Chris Hughes]

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

[Chris Hughes]

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

[Chris Hughes]

my_fun.f and Square are two separate arguments,

[Jean-Philippe Burelle]

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

[Reid Barton]

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