Zulip Chat Archive

Stream: new members

Topic: pairs equal iff projections are?


view this post on Zulip Marcus Klaas (Dec 02 2018 at 12:50):

Can anyone give me a pointer on how prove this?

example {α β} {a c : α} {b d : β} (h: (a, b) = (c, d)) : a = c := sorry

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 12:51):

example {α β} {a c : α} {b d : β} (h: (a, b) = (c, d)) : a = c :=
begin
  cases h,
  refl,
end

view this post on Zulip Patrick Massot (Dec 02 2018 at 12:54):

The state after cases is a bit weird. You can also directly provide the proof term (prod.mk.inj h).left

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 12:54):

example {α β} {a c : α} {b d : β} (h: (a, b) = (c, d)) : a = c :=
(prod.mk.inj h).1

view this post on Zulip Marcus Klaas (Dec 02 2018 at 12:54):

Thanks so much!!

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 12:55):

example {α β} :  {a c : α} {b d : β} (h: (a, b) = (c, d)), a = c
| a c b d rfl := rfl

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 12:56):

So that's a tactic mode proof, a term mode proof, and a proof using the equation compiler.

view this post on Zulip Marcus Klaas (Dec 02 2018 at 12:58):

Haha, that's great :D - I'm not quite sure how the equation compiler does it tho ;p

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 13:00):

(a, b) has type prod \alpha \beta, an inductive type, so you need tools to deal with terms of this type. When the inductive type prod is defined, Lean creates with it its recursor prod.rec, which is the universal way to define a map from prod \alpha \beta to anywhere. Lean then creates a bunch of other useful functions automatically, you can see what they are by typing #print prefix prod. There's usually something called X.mk.inj in there for an inductive type X, so that's what I was looking for. That's how I found the term proof. For the tactic mode proof, cases is a great tactic for any inductive type, it takes the type to pieces.

For the equation compiler proof, we make Lean do the work. I had to move things to the other side of the colon. The point is that I can tell Lean that without loss of generality h must be rfl. I still don't really understand how the equation compiler actually works, but I have sort-of got the hang of how to use it in practice. Your question is a great basic example of how to use its power.

view this post on Zulip Mario Carneiro (Dec 02 2018 at 13:02):

it uses prod.no_confusion under the hood, which is basically the same as prod.inj

view this post on Zulip Marcus Klaas (Dec 02 2018 at 13:03):

You folks are amazing. Thank you.

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 13:04):

Just to be clear -- moving stuff to before or after the colon doesn't change the proposition, it's just a trick for controlling whether or not you have to give the inputs yourself in the "first line" of your proof.


Last updated: May 11 2021 at 14:11 UTC