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 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: Dec 20 2023 at 11:08 UTC