## Stream: new members

### Topic: Proving lemmas about structural equality

#### 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⟩

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}


#### 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

#### Mario Carneiro (Aug 15 2020 at 00:46):

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

#### Kyle Miller (Aug 15 2020 at 00:46):

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

#### Mario Carneiro (Aug 15 2020 at 00:46):

but you also need a simp lemma for add

#### Mario Carneiro (Aug 15 2020 at 00:47):

this proof should be by ext; simp

#### Reid Barton (Aug 15 2020 at 00:51):

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

#### 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⟩

lemma pt_add_comm (a b : point) : a + b = b + a :=
begin
cases a,
cases b,
end


#### Amanda Hauer (Aug 15 2020 at 00:58):

Thank you for now!

#### Adam Topaz (Aug 15 2020 at 01:04):

Do you need the first two cases?

#### Kyle Miller (Aug 15 2020 at 01:07):

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

#### Adam Topaz (Aug 15 2020 at 01:09):

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

#### Kyle Miller (Aug 15 2020 at 01:09):

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

#### Adam Topaz (Aug 15 2020 at 01:10):

Ha! I knew I recognized your name!

Small world

#### Kyle Miller (Aug 15 2020 at 01:13):

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

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