## Stream: new members

### Topic: distributing or

#### Iocta (Dec 29 2019 at 01:36):

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 _)))
)


#### Kenny Lau (Dec 29 2019 at 02:02):

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

#### Kenny Lau (Dec 29 2019 at 02:02):

which is classical.em p

#### Kenny Lau (Dec 29 2019 at 02:02):

or maybe classical.em, I don't remember

#### Iocta (Dec 29 2019 at 05:24):

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 (Dec 29 2019 at 05:42):

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 (Dec 29 2019 at 05:43):

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

#### Iocta (Dec 29 2019 at 06:12):

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 (Dec 29 2019 at 06:14):

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

Ok

#### Luis O'Shea (Jan 04 2020 at 15:28):

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⟩))


Last updated: May 11 2021 at 14:11 UTC