Zulip Chat Archive

Stream: general

Topic: Using class instance definition in a proof


view this post on Zulip 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?

view this post on Zulip Alex J. Best (Sep 25 2020 at 17:09):

refl for both :smile:

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Sep 25 2020 at 17:13):

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

view this post on Zulip 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 +".

view this post on Zulip Johan Commelin (Sep 25 2020 at 17:28):

set_option pp.notation false I guess

view this post on Zulip Alex J. Best (Sep 25 2020 at 17:28):

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

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip Tomas Skrivan (Sep 25 2020 at 17:34):

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

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 17:42):

Probably it's the wrong zero :-)

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 17:43):

Try has_zero.zero :-(

view this post on Zulip 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