Proving the Distributive Law in Lean

Formal verification allows us to prove logical statements with absolute certainty. In this post, we explore a proof in the Lean 4 programming language for the distributive law of propositional logic:

p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)

Here is the complete proof script:

example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
Iff.intro
  (λ h : p ∨ (q ∧ r) =>
    Or.elim h
      (λ hp: p => And.intro (Or.intro_left q hp) (Or.intro_left r hp))
      (λ hqr : q ∧ r => And.intro (Or.intro_right p hqr.1) (Or.intro_right p hqr.2))
  )
  (λ h : (p ∨ q) ∧ (p ∨ r) =>
    Or.elim h.1
      (λ hp : p => Or.intro_left (q ∧ r) hp)
      (λ hq : q =>
        Or.elim h.2
          (λ hp : p => Or.intro_left (q ∧ r) hp)
          (λ hr : r => Or.intro_right p (And.intro hq hr)))
  )

Analyzing the Logic

The proof is constructed using Iff.intro, which splits the problem into two directions: forward (→) and backward (←).

1. Forward Direction

We assume h : p ∨ (q ∧ r) and need to prove (p ∨ q) ∧ (p ∨ r).

There are two cases based on the OR statement:

• Case 1 (Proof of p): If we have a proof of p, we can construct the proof of (p ∨ q) ∧ (p ∨ r) immediately. Since p is true, both p ∨ q and p ∨ r are true regardless of q or r.
• Case 2 (Proof of q ∧ r): If we have a proof of q ∧ r, then we have proofs for both q and r. We use q to prove the left side (p ∨ q) and r to prove the right side (p ∨ r), assuming p is false (conceptually, though in constructive logic we just use the right injection).

2. Backward Direction

We assume h : (p ∨ q) ∧ (p ∨ r) and need to prove p ∨ (q ∧ r).

Since the assumption is an AND statement, we know both p ∨ q and p ∨ r are true. We proceed by cases on the first part p ∨ q:

• If p is true, the goal p ∨ (q ∧ r) is immediately satisfied (left side of the OR).
• If q is true, we are not done yet. We need to check the second part of our initial assumption, p ∨ r.
  • If p is true here, the goal is again satisfied immediately.
  • If r is true, we now have proofs for both q and r. We can combine them to form q ∧ r, which satisfies the right side of our goal p ∨ (q ∧ r).

This nested case analysis elegantly covers all truth values, constructively building the proof object required by Lean.