# Zulip Chat Archive

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

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

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

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

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: May 14 2021 at 21:11 UTC