Search code examples
lean

example : ((p ∨ q) → r) → (p → r) ∧ (q → r)

Section 3.6 of Theorem Proving in Lean shows the following:

example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry

Let's focus on the left-to-right direction:

example : ((p ∨ q) → r) → (p → r) ∧ (q → r) := sorry

What's a good way to structure this example?

If I go with something like this (with underscores used so that we can indicate the overall approach):

example : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
    (assume hpqr : (p ∨ q) → r,
        (assume hpq : p ∨ q,
            or.elim hpq 
                (assume hp : p,
                    show (p → r) ∧ (q → r), from and.intro _ _)
                (assume hq : q,
                    show (p → r) ∧ (q → r), from and.intro _ _)))

we get:

enter image description here

If we restructure it as:

example (hpqr : ((p ∨ q) → r)) : (p → r) ∧ (q → r) := 
    (assume hpq : p ∨ q,
        or.elim hpq 
            (assume hp : p,
                show (p → r) ∧ (q → r), from and.intro _ _)
            (assume hq : q,
                show (p → r) ∧ (q → r), from and.intro _ _))

we seem to get a little closer:

enter image description here

Chapter 3 doesn't seem to have other worked examples which involve both an ∧ and a → on the left side.

Any suggestions on how to approach this are welcome!

UPDATE

Here's an approach based on Yury's recommendation below:

example : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
    (assume hpqr : (p ∨ q) → r,
        (and.intro
            (assume hp : p, hpqr (or.inl hp))
            (assume hq : q, hpqr (or.inr hq))))

Turns out to be quite simple. :-)

UPDATE

Here's an iff version that handles both directions:

example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=

    iff.intro

        (assume hpqr : (p ∨ q) → r,
            show (p → r) ∧ (q → r), from
                (and.intro
                    (assume hp : p, hpqr (or.inl hp))
                    (assume hq : q, hpqr (or.inr hq))))

        (assume hprqr : (p → r) ∧ (q → r),
            show ((p ∨ q) → r), from
                (assume hqr : p ∨ q,
                    or.elim hqr
                        (assume hp : p, hprqr.left hp)
                        (assume hq : q, hprqr.right hq)))
Solution

  • You don't have p ∨ q in the assumptions of this example. So, you have to go from (assume hpqr, _) directly to and_intro. I mean, something like

    example (p q r : Prop) : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
assume hpqr,
and.intro (assume p, _) (assume q, _)