Zulip Chat Archive

Stream: new members

Topic: How to prove equality of structure


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

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 15:21):

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

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 15:22):

but cases A; cases B will get you started.

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 15:22):

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

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

view this post on Zulip Rob Lewis (Jun 26 2020 at 15:25):

@[ext]?

view this post on Zulip Johan Commelin (Jun 26 2020 at 15:27):

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

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

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

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 15:30):

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

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

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

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

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