Zulip Chat Archive

Stream: new members

Topic: distributing `or`


view this post on Zulip 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 _)))
)

How can I go about this?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Dec 29 2019 at 02:02):

which is classical.em p

view this post on Zulip Kenny Lau (Dec 29 2019 at 02:02):

or maybe classical.em, I don't remember

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Dec 29 2019 at 05:43):

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

view this post on Zulip 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))))))

view this post on Zulip 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.

view this post on Zulip Iocta (Dec 29 2019 at 06:37):

Ok

view this post on Zulip 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