Some basic Propositional Logic Proofs in Lean

Question

I just read though the documentation of Lean, and try to do the 3.7. Exercises,
didn't finish all of them yet, but here are the first four exercises (without classical reasoning):

variables p q r : Prop

-- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p := sorry
example : p ∨ q ↔ q ∨ p := sorry

-- associativity of ∧ and ∨
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry

Here is what I did for that first four exercises:

variables p q r : Prop

-- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p := 
iff.intro
  (assume h : p ∧ q,
    show q ∧ p, from and.intro (and.right h) (and.left h))
  (assume h : q ∧ p,
    show p ∧ q, from and.intro (and.right h) (and.left h))

example : p ∨ q ↔ q ∨ p :=
iff.intro
  (assume h : p ∨ q,
  show q ∨ p, from 
  or.elim h
     (assume hp : p,
       show q ∨ p, from or.intro_right q hp)
     (assume hq : q,
       show q ∨ p, from or.intro_left p hq))
  (assume h : q ∨ p,
  show p ∨ q, from 
  or.elim h
     (assume hq : q,
       show p ∨ q, from or.intro_right p hq)
     (assume hp : p,
       show p ∨ q, from or.intro_left q hp))

-- associativity of ∧ and ∨
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := 
iff.intro
  (assume h: (p ∧ q) ∧ r,
    have hpq : p ∧ q, from and.elim_left h,
    have hqr : q ∧ r, from and.intro (and.right hpq) (and.right h),
    show p ∧ (q ∧ r), from and.intro (and.left hpq) (hqr))
  (assume h: p ∧ (q ∧ r),
    have hqr : q ∧ r, from and.elim_right h,
    have hpq : p ∧ q, from and.intro (and.left h) (and.left hqr),
    show (p ∧ q) ∧ r, from and.intro (hpq) (and.right hqr))

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
iff.intro
  (assume hpqr : (p ∨ q) ∨ r, 
    show p ∨ (q ∨ r), from or.elim hpqr
      (assume hpq : p ∨ q,
        show p ∨ (q ∨ r), from or.elim hpq
          (assume hp : p,
            show p ∨ (q ∨ r), from or.intro_left (q ∨ r) hp)
          (assume hq : q,
            have hqr : q ∨ r, from or.intro_left r hq,
            show p ∨ (q ∨ r), from or.intro_right p hqr))
      (assume hr : r,
        have hqr : q ∨ r, from or.intro_right q hr,
        show p ∨ (q ∨ r), from or.intro_right p hqr))
  (assume hpqr : p ∨ (q ∨ r),
    show (p ∨ q) ∨ r, from or.elim hpqr
    (assume hp : p,
      have hpq : (p ∨ q), from or.intro_left q hp,
      show (p ∨ q) ∨ r, from or.intro_left r hpq)
    (assume hqr : (q ∨ r),
      show (p ∨ q) ∨ r, from or.elim hqr
        (assume hq : q,
          have hpq : (p ∨ q), from or.intro_right p hq,
          show (p ∨ q) ∨ r, from or.intro_left r hpq)
        (assume hr : r,
          show (p ∨ q) ∨ r, from or.intro_right (p ∨ q) hr)))

I think this is valid, but it's quite long, Is this the best we can do, or are there better ways to write those proofs in Lean, any suggestions would be appreciated.

Answer 1

Just another idea. For me (also a beginner with LEAN) it is easier to read through the proofs if I break them down in smaller pieces. The code fragment below is a proof of the second commutativity property written with tactics in a few steps.

--- 2) Prove p ∨ q ↔ q ∨ p
-- Easier if using these results first:
theorem LR2_11 : p → p ∨ q :=
begin
    intros hp,
    exact or.intro_left q hp
end
#check LR2_11 
theorem LR2_12 : p → q ∨ p :=
begin
    intros hp,
    exact or.intro_right q hp
end
#check LR2_12 
theorem LR2_2 : p ∨ q → q ∨ p :=
begin
    intros p_or_q, 
    exact or.elim p_or_q (LR2_12 p q) (LR2_11 q p)
end
theorem Comm2_2 : p ∨ q ↔ q ∨ p :=
begin
    exact iff.intro (LR2_2 p q) (LR2_2 q p)
end
#check Comm2_2

Answer 2

If you import Lean's math's library then the tactic by tauto! should solve all of these. Additionally these are all already library theorems with names like and_comm.

I don't think there are any shorter proofs of these statements from first principles. The only way you can shorten some of the proofs is by removing the haves and shows and making them less readable. Here's my proof of or_assoc, which is essentially the same as yours, but without the haves and shows.

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
iff.intro 
  (λ h, or.elim h (λ hpq, or.elim hpq or.inl (λ hq, or.inr (or.inl hq))) (λ hr, or.inr (or.inr hr)))
  (λ h, or.elim h (λ hp, (or.inl (or.inl hp))) (λ hqr, or.elim hqr (λ hq, or.inl (or.inr hq)) or.inr))