# Zulip Chat Archive

## Stream: new members

### Topic: Unfolding function coercion

#### 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!

#### Chris Hughes (Oct 09 2020 at 12:40):

Have you tried `unfold my_fun.f`

?

#### Chris Hughes (Oct 09 2020 at 12:40):

Actually `unfold square my_fun.f`

#### 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.

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

#### 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`

.

#### Chris Hughes (Oct 09 2020 at 12:48):

`my_fun.f`

and `Square`

are two separate arguments,

#### 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.

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