simple structural equality

Stream: new members

[Edward Ayers]

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]

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

[Edward Ayers]

thanks

[Mario Carneiro]

congr?

[Edward Ayers]

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

[Patrick Massot]

congr ; assumption instead of cc also works

[Mario Carneiro]

congr' too

[Johan Commelin]

It's longer though

[Patrick Massot]

but is much longer to type

[Patrick Massot]

still longer

[Mario Carneiro]

cc is longer to run

[Johan Commelin]

I suppose congr; cc works

[Johan Commelin]

Can't we have congra?

[Edward Ayers]

by congr ; assumption fails on congr for me

[Mario Carneiro]

congr'

[Mario Carneiro]

is congra

[Mario Carneiro]

you have to do cases first

[Mario Carneiro]

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]

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.