## Stream: new members

### Topic: simple structural equality

#### Edward Ayers (Aug 08 2018 at 17:28):

How would I prove this?

structure mystr :=
(A : ℕ)
(B : bool)
(p : A > 10)

def mystr_eq (x y : mystr) (A_eq : x.A = y.A) (B_eq : x.B = y.B) : x = y
:= by sorry


#### Patrick Massot (Aug 08 2018 at 17:35):

def mystr_eq (x y : mystr) (A_eq : x.A = y.A) (B_eq : x.B = y.B) : x = y
:= by cases x ; cases y ; cc


thanks

#### Mario Carneiro (Aug 08 2018 at 17:36):

congr?

#### Edward Ayers (Aug 08 2018 at 17:36):

next question: how to prove it without tactics? Just a proof term.

#### Patrick Massot (Aug 08 2018 at 17:36):

congr ; assumption instead of cc also works

#### Mario Carneiro (Aug 08 2018 at 17:36):

congr' too

#### Johan Commelin (Aug 08 2018 at 17:36):

It's longer though

#### Patrick Massot (Aug 08 2018 at 17:37):

but is much longer to type

still longer

#### Mario Carneiro (Aug 08 2018 at 17:37):

cc is longer to run

#### Johan Commelin (Aug 08 2018 at 17:37):

I suppose congr; cc works

#### Johan Commelin (Aug 08 2018 at 17:37):

Can't we have congra?

#### Edward Ayers (Aug 08 2018 at 17:37):

by congr ; assumption fails on congr for me

#### Mario Carneiro (Aug 08 2018 at 17:37):

congr'

#### Mario Carneiro (Aug 08 2018 at 17:38):

is congra

#### Mario Carneiro (Aug 08 2018 at 17:38):

you have to do cases first

#### Mario Carneiro (Aug 08 2018 at 17:40):

term proof:

theorem mystr_eq : ∀ (x y : mystr) (A_eq : x.A = y.A) (B_eq : x.B = y.B), x = y
| ⟨xA, xB, xp⟩ ⟨_, _, _⟩ rfl rfl := rfl


#### Kevin Buzzard (Aug 08 2018 at 17:45):

I was about to post that term proof but Mario just beat me to it. When I was a beginner I found those sorts of proofs miraculous; that's why I thought it was worth mentioning. The equation compiler is so clever.

Last updated: May 11 2021 at 22:14 UTC