pairs equal iff projections are?

Stream: new members

[Marcus Klaas]

Can anyone give me a pointer on how prove this?

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Marcus Klaas]

Thanks so much!!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Marcus Klaas]

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

[Kevin Buzzard]

(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.

[Mario Carneiro]

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

[Marcus Klaas]

You folks are amazing. Thank you.

[Kevin Buzzard]

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.