Zulip Chat Archive

Stream: new members

Topic: simple structural equality


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Edward Ayers (Aug 08 2018 at 17:36):

thanks

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:36):

congr?

view this post on Zulip Edward Ayers (Aug 08 2018 at 17:36):

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

view this post on Zulip Patrick Massot (Aug 08 2018 at 17:36):

congr ; assumption instead of cc also works

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:36):

congr' too

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:36):

It's longer though

view this post on Zulip Patrick Massot (Aug 08 2018 at 17:37):

but is much longer to type

view this post on Zulip Patrick Massot (Aug 08 2018 at 17:37):

still longer

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:37):

cc is longer to run

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:37):

I suppose congr; cc works

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:37):

Can't we have congra?

view this post on Zulip Edward Ayers (Aug 08 2018 at 17:37):

by congr ; assumption fails on congr for me

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:37):

congr'

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:38):

is congra

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:38):

you have to do cases first

view this post on Zulip 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

view this post on Zulip 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