Proving lemmas about structural equality

Stream: new members

[Amanda Hauer]

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]

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]

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

[Kyle Miller]

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

[Mario Carneiro]

but you also need a simp lemma for add

[Mario Carneiro]

this proof should be by ext; simp

[Reid Barton]

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

[Kyle Miller]

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]

Thank you for now!

[Adam Topaz]

Do you need the first two cases?

[Kyle Miller]

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

[Adam Topaz]

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

[Kyle Miller]

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

[Adam Topaz]

Ha! I knew I recognized your name!

[Adam Topaz]

Small world

[Kyle Miller]

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

[Kevin Buzzard]

@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