## 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 sorrys 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: May 08 2021 at 19:11 UTC