Using class instance definition in a proof

Stream: general

[Tomas Skrivan]

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]

refl for both :smile:

[Alex J. Best]

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]

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

[Tomas Skrivan]

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]

set_option pp.notation false I guess

[Alex J. Best]

simp only [(+)] is what I normally do to actually unfold the definition.

[Tomas Skrivan]

Rob Lewis said:

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

Good to know, thanks!

[Tomas Skrivan]

Alex J. Best said:

simp only [(+)] is what I normally do to actually unfold the definition.

This works perfectly!

[Tomas Skrivan]

Hmm but simp only [(0)] does not work.

[Kevin Buzzard]

Probably it's the wrong zero :-)

[Kevin Buzzard]

Try has_zero.zero :-(

[Kevin Buzzard]

Oh, replace (0) with (0 : X) and you might be ok