# Zulip Chat Archive

## Stream: general

### Topic: Using class instance definition in a proof

#### Tomas Skrivan (Sep 25 2020 at 17:06):

If a type `Y`

has zero or addition, then we can naturally extend zero and addition to the type `X -> Y`

. Naturally, the zero of `X -> Y`

should evaluate to zero for every input and function evaluation should distribute over addition in `X -> Y`

. I'm having hard time proving this when I define zero and addition with typeclasses. The code:

```
instance fspace.has_zero {X Y : Type} [has_zero Y] : has_zero (X → Y) := has_zero.mk (λ x, 0)
instance fspace.has_add {X Y : Type} [has_add Y] : has_add (X → Y) := has_add.mk (λ f g, λ x, (f x) + (g x))
lemma eval_zero_is_zero {X Y : Type} [has_zero Y] {f : X → Y} : (f = 0) → (∀ (x : X), f x = 0) :=
begin
intros H x,
rewrite H,
sorry
end
lemma add_on_vals {X Y : Type} [has_add Y] {f g : X → Y} {x : X} : (f + g) x = (f x) + (g x) :=
begin
sorry,
end
```

Is there a way to use the definition of zero and addition in the proof?

It is likely, that I'm asking for something that cannot be done. How else can I define zero and addition on types `X -> Y`

such that I can prove those lemmas?

#### Alex J. Best (Sep 25 2020 at 17:09):

`refl`

for both :smile:

#### Alex J. Best (Sep 25 2020 at 17:11):

You've already got both `sorry`

s to the point where it is true by definition, and thats what the `refl`

tactic will prove for you.

#### Rob Lewis (Sep 25 2020 at 17:13):

BTW, these instances are defined already if you `import algebra.group.pi`

#### Tomas Skrivan (Sep 25 2020 at 17:27):

Ohh, I didn't realize that the proof is done :D. Now, I can do the more complicated case I was originally struggling with.

Is there a way to monetarily turn off the `+`

and `0`

notation? So I can see the actual definition? Something like `"unfold +"`

.

#### Johan Commelin (Sep 25 2020 at 17:28):

`set_option pp.notation false`

I guess

#### Alex J. Best (Sep 25 2020 at 17:28):

`simp only [(+)]`

is what I normally do to actually unfold the definition.

#### Tomas Skrivan (Sep 25 2020 at 17:28):

Rob Lewis said:

BTW, these instances are defined already if you

`import algebra.group.pi`

Good to know, thanks!

#### Tomas Skrivan (Sep 25 2020 at 17:33):

Alex J. Best said:

`simp only [(+)]`

is what I normally do to actually unfold the definition.

This works perfectly!

#### Tomas Skrivan (Sep 25 2020 at 17:34):

Hmm but `simp only [(0)]`

does not work.

#### Kevin Buzzard (Sep 25 2020 at 17:42):

Probably it's the wrong zero :-)

#### Kevin Buzzard (Sep 25 2020 at 17:43):

Try `has_zero.zero`

:-(

#### Kevin Buzzard (Sep 25 2020 at 17:44):

Oh, replace `(0)`

with `(0 : X)`

and you might be ok

Last updated: Dec 20 2023 at 11:08 UTC