distributing `or`

Stream: new members

[Iocta]

This clearly isn't on the right track,

def factor_or : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
  (λ h,
  or.elim (and.left h)
  -- p is true.
  or.inl
  -- If p is false, q and r are true.
  -- But we don't really know that p is false.
  (λ z, (or.inr (and.intro z _)))
)

but lean doesn't like or.elim (p \or \not p) either.

def factor_or : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
  (λ h,
  or.elim (p ∨ ¬p)
  -- p is true.
  or.inl
  -- p is false, so q and r are true.
  (λ z, (or.inr (and.intro z _)))
)

How can I go about this?

[Kenny Lau]

the p or not p needs to be replaced with a proof of p or not p

[Kenny Lau]

which is classical.em p

[Kenny Lau]

or maybe classical.em, I don't remember

[Iocta]

This is in the section of the exercises that I think isn't supposed to require classical. Is there a way to do it without?

[Joe]

lemma factor_or : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
  λh, or.elim h.left or.inl $ λhq, or.elim h.right or.inl $ λhr, or.inr $ and.intro hq hr

[Yury G. Kudryashov]

Try to do or.elim on both and.left h and and.right h.

[Iocta]

Got it, thanks.

def factor_or : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
(λ h,
  (or.elim h.left or.inl
    (λ qq, or.elim h.right or.inl
      (λ rr, (or.inr (and.intro qq rr))))))

[Yury G. Kudryashov]

BTW, it makes sense to use theorem/lemma in this case because the conclusion is a proposition, not a Type.

[Iocta]

Ok

[Luis O'Shea]

Below is the same proof written in a slightly different way. It illustrates

• Using dot syntax to deal with and followed by or: h.left.elim and h.right.elim
• Letting Lean infer the and constructor by using angle brackets: ⟨hq,hr⟩

I'm not saying it's stylistically better (it's just an example of some Lean syntax which may be of interest).

example (h: (p ∨ q) ∧ (p ∨ r)) : p ∨ (q ∧ r) :=
h.left.elim
    or.inl
    (assume hq, h.right.elim
        or.inl
        (assume hr, or.inr ⟨hq,hr⟩))