Zulip Chat Archive

Stream: new members

Topic: Proving lemmas about structural equality


view this post on Zulip Amanda Hauer (Aug 15 2020 at 00:42):

I'm having trouble proving statements about structure equality. Here's an MWE of the type of problem I run into.

structure point :=
(a : )
(b : )

def pt_add : point  point  point := λ x y, x.1 + y.1, x.2 + y.2

instance : has_add point := pt_add

lemma pt_add_comm :  a b : point, a + b = b + a :=
begin
intros a b,
cases a,
cases b,
{sorry}
end

The goal contains curly brackets. I have no idea how to go about reaching this goal.

{a := a_a, b := a_b} + {a := b_a, b := b_b} = {a := b_a, b := b_b} + {a := a_a, b := a_b}

view this post on Zulip Adam Topaz (Aug 15 2020 at 00:44):

I think congr will help here. But I think the "correct" way to do this is to define and use an extensionality lemma

view this post on Zulip Mario Carneiro (Aug 15 2020 at 00:46):

You can put @[ext] on the structure to do that automatically

view this post on Zulip Kyle Miller (Aug 15 2020 at 00:46):

I probably would try dsimp [has_add.add, pt_add] as a start.

view this post on Zulip Mario Carneiro (Aug 15 2020 at 00:46):

but you also need a simp lemma for add

view this post on Zulip Mario Carneiro (Aug 15 2020 at 00:47):

this proof should be by ext; simp

view this post on Zulip Reid Barton (Aug 15 2020 at 00:51):

you can put @[simps] on pt_add :sunglasses:

view this post on Zulip Kyle Miller (Aug 15 2020 at 00:54):

Here's one way using only the @[ext] annotation:

import tactic

@[ext]
structure point :=
(a : )
(b : )

def pt_add : point  point  point := λ x y, x.1 + y.1, x.2 + y.2

instance : has_add point := pt_add

lemma pt_add_comm (a b : point) : a + b = b + a :=
begin
  cases a,
  cases b,
  ext; dsimp only [has_add.add, pt_add]; exact add_comm _ _,
end

view this post on Zulip Amanda Hauer (Aug 15 2020 at 00:58):

Thank you for now!

view this post on Zulip Adam Topaz (Aug 15 2020 at 01:04):

Do you need the first two cases?

view this post on Zulip Kyle Miller (Aug 15 2020 at 01:07):

@Adam Topaz You're right, the vestigial cases can be removed :smile:

view this post on Zulip Adam Topaz (Aug 15 2020 at 01:09):

@Kyle Miller did you ever take a commutative algebra class at Berkeley?

view this post on Zulip Kyle Miller (Aug 15 2020 at 01:09):

I've been meaning to say "hi" for a while. I took 250B with you.

view this post on Zulip Adam Topaz (Aug 15 2020 at 01:10):

Ha! I knew I recognized your name!

view this post on Zulip Adam Topaz (Aug 15 2020 at 01:10):

Small world

view this post on Zulip Kyle Miller (Aug 15 2020 at 01:13):

It was a good diet of category theory and homological algebra you fed us back then!

view this post on Zulip Kevin Buzzard (Aug 15 2020 at 09:52):

@Amanda Hauer you could look at the complex number game https://github.com/ImperialCollegeLondon/complex-number-game . A complex number is two real numbers, and assuming everything about real numbers I prove that addition commutes in the complex numbers in a hopefully comprehensive way in the first level


Last updated: May 14 2021 at 21:11 UTC