Stream: new members

Topic: How to prove equality of structure

Keyao Peng (Jun 26 2020 at 15:20):

For example

variable (α : Type)
structure pair α  :=
(x : α)
(y : α)

def foo:  pair α -> pair α ->pair α :=
λ a b , {x := fx a.x b.x ,y := fy a.y b.y}


now I want to prove something like for some A B C : pair α

lemma bar: foo A B = C


which tactics I can use to reduce the goal to, {x := fx A.x B.x ,y := fy A.y B.y}={x :=C.x,y :=C.y}  and finally become fx A.x B.x =C.x ∧ fy A.y B.y =C.y?

Kevin Buzzard (Jun 26 2020 at 15:21):

This question would be much easier to work with if what you posted compiled.

Kevin Buzzard (Jun 26 2020 at 15:22):

but cases A; cases B will get you started.

Kevin Buzzard (Jun 26 2020 at 15:22):

In general you should probably prove an ext lemma before you embark on proving bar

Kevin Buzzard (Jun 26 2020 at 15:24):

There's a way of getting the derive handler to derive ext but I can never remember how to do it and I don't know how to look it up :-(

Rob Lewis (Jun 26 2020 at 15:25):

@[ext]?

Johan Commelin (Jun 26 2020 at 15:27):

@Keyao Peng You are looking for cases A, cases B, cases C, congr,

Keyao Peng (Jun 26 2020 at 15:30):

Kevin Buzzard said:

but cases A; cases B will get you started.

when use cases A; cases B;cases C it just becomes foo {x := A.x , y:=A.y} {x := B.x , y:=B.y} = {x := C.x , y:=C.y}, but I want {x := fx A.x B.x ,y := fy A.y B.y}={x :=C.x,y :=C.y}

Kevin Buzzard (Jun 26 2020 at 15:30):

import tactic

variable {α : Type}

@[ext] structure pair (α : Type) :=
(x : α)
(y : α)

def foo (fx fy : α → α → α):  pair α -> pair α ->pair α :=
λ a b, {x := fx a.x b.x ,y := fy a.y b.y}

lemma bar (fx fy : α → α → α) (A B C : pair α):
foo fx fy A B = C :=
begin
ext,
/-
2 goals
α : Type,
fx fy : α → α → α,
A B C : pair α
⊢ (foo fx fy A B).x = C.x

α : Type,
fx fy : α → α → α,
A B C : pair α
⊢ (foo fx fy A B).y = C.y
-/
cases A, cases B, cases C, all_goals {dsimp [foo]},
/-
α : Type,
fx fy : α → α → α,
A_x A_y B_x B_y C_x C_y : α
⊢ fx A_x B_x = C_x

α : Type,
fx fy : α → α → α,
A B C : pair α
⊢ fy A.y B.y = C.y
-/
sorry, sorry
end


Kevin Buzzard (Jun 26 2020 at 15:30):

that non-ascii comma in the original post threw me for a while

ROCKY KAMEN-RUBIO (Jun 28 2020 at 02:28):

Kevin's twitch stream about the complex number game gives an overview of this using a locally defined complex number structure as an example.
Edit: I'm having trouble finding it on twitch and am only seeing this clip. Does anyone know what happened to it?
https://www.twitch.tv/kbuzzard/clip/CrepuscularSmoggyCroissantPeanutButterJellyTime

Kevin Buzzard (Jun 28 2020 at 04:28):

Try the Xena project YouTube channel. NB if anyone has any ideas about how to set up a YouTube channel I'd be interested to hear them

Jalex Stark (Jun 28 2020 at 05:29):

@Kevin Buzzard if you kick twitch \$5/month, they'll keep your videos for 90 days instead of 14 days (I don't have advice about youtube, but this will buy some time so that getting the details of the youtube channel correct isn't critical right now)

ROCKY KAMEN-RUBIO (Jun 30 2020 at 18:05):

The channel seems to be stable and have the complete stream. Here's a link if anyone's interested https://www.youtube.com/watch?v=OEZCp63GES8

Last updated: May 10 2021 at 00:31 UTC