or distrib over and golf

Stream: general

[Kevin Buzzard]

A student just asked me this:

example (P Q R : Prop) : P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R) := sorry

They proved it in 60 lines :-) I said that there were probably quicker proofs. How quick can we get it?

[Chris Hughes]

by finish

[Sebastien Gouezel]

by tauto (one letter less)

[Kevin Buzzard]

I couldn't get finish to work :-/

[Kevin Buzzard]

But I got or_and_distrib_left to work :-)

[Rob Lewis]

finish doesn't work for me, but split; finish does.

[Chris Hughes]

example (P Q R : Prop) : P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R) :=
⟨λ h, h.elim (λ h, ⟨or.inl h, or.inl h⟩) (λ h, ⟨or.inr h.1, or.inr h.2⟩),
  λ h, h.1.elim or.inl (λ hQ, h.2.elim or.inl (λ hR, or.inr ⟨hQ, hR⟩))

[Scott Olson]

If one didn't want to use a high level tactic, I'm fond of pattern matching for this style of "take it apart and put it back together in another shape" proof:

lemma ltr {P Q R : Prop} : P ∨ (Q ∧ R) → (P ∨ Q) ∧ (P ∨ R)
| (or.inl hp) := ⟨or.inl hp, or.inl hp⟩
| (or.inr ⟨hq, hr⟩) := ⟨or.inr hq, or.inr hr⟩

lemma rtl {P Q R : Prop} : (P ∨ Q) ∧ (P ∨ R) → P ∨ (Q ∧ R)
| ⟨or.inl hp, _⟩ := or.inl hp
| ⟨_, or.inl hp⟩ := or.inl hp
| ⟨or.inr hq, or.inr hr⟩ := or.inr ⟨hq, hr⟩

example {P Q R : Prop} : P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R) :=
iff.intro ltr rtl

[Scott Olson]

This isn't exactly golfing it, but I find it really clear for proofs that are merely reorganizing "data"

[Kevin Buzzard]

Thanks for all of these -- I believe the student is a learner and is reading the answers so it's great to see the options which are available