CODEWITHSUNDEEP
functional-programmingtheorem-provinglean
Vox
Vox

Reputation: 323

How to prove distributivity (propositional validity property 6) in LEAN?

Having gone through most exercises and also solved/proved in LEAN the first five propositional validities/properties at the end of chapter 3 in the LEAN manual, I still have trouble with the following implication (one of the implications needed for the proof of property 6):

theorem Distr_or_L (p q r : Prop) : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
begin
    intros pqpr, 
    have porq : p ∨ q, from pqpr.left,
    have porr : p ∨ r, from pqpr.right,
    sorry
end

The difficulty I face is mainly due to the case when p is not true, as I don't know how to combine, using LEAN tools, the two sides of the and in the hypothesis to obtain the fact that both q and r must hold under that scenario. I would greatly appreciate any help here; please help me understand how to construct this proof in the above setting without importing any other tactics except those in standard LEAN. For completeness, here is my proof of the other direction:

theorem Distr_or_R (p q r : Prop) : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) :=
begin
    intros pqr,
    exact or.elim pqr 
    ( assume hp: p, show (p ∨ q) ∧ (p ∨ r), from 
        and.intro (or.intro_left q hp) (or.intro_left r hp) ) 
    ( assume hqr : (q ∧ r), show (p ∨ q) ∧ (p ∨ r), from 
        and.intro (or.intro_right p hqr.left) (or.intro_right p hqr.right) ) 
end

Upvotes: 1

Views: 402

Answers (2)

Jorge M
Jorge M

Reputation: 11

Here is an asnwer for say problem without using cases. (explained later in tbe mentioned book)

example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
Iff.intro
 (fun hpqr => Or.elim hpqr
 (fun hp: p => 
 show (p ∨ q) ∧ (p ∨ r) from And.intro (Or.inl hp) (Or.inl hp))
 (fun hqr: q ∧ r => 
 show (p ∨ q) ∧ (p ∨ r) from And.intro (Or.inr hqr.left) (Or.inr hqr.right)))
(fun hpqpr: (p ∨ q) ∧ (p ∨ r) => 
 have hpq: (p ∨ q) := hpqpr.left;
 have hpr: (p ∨ r) := hpqpr.right;
   Or.elim hpq
    (fun hp: p => show p ∨ (q ∧ r) from Or.inl hp)
    (fun hq: q => Or.elim hpr 
       (fun hp: p => show p ∨ (q ∧ r) from Or.inl hp)
       (fun hr: r => show p ∨ (q ∧ r) from Or.inr (And.intro hq hr))))

You're using the information in the right part of the conjunction, otherwise, the left part doesn't give any info regarding r.

Upvotes: 1

Christopher Hughes
Christopher Hughes

Reputation: 1129

Hint. Try case splitting on both porq and porr.

Here's a solution

theorem Distr_or_L (p q r : Prop) : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
begin
    intros pqpr, 
    have porq : p ∨ q, from pqpr.left,
    have porr : p ∨ r, from pqpr.right,
    { cases porq with hp hq,
      { exact or.inl hp },
      { cases porr with hp hr,
        { exact or.inl hp },
        { exact or.inr ⟨hq, hr⟩ } } }
end

Upvotes: 1

Related Questions