04 — Disjunction (or)

The Mathematics

The disjunction P ∨ Q (read "P or Q") means that at least one of P or Q is true. Maybe both are true — that's fine too. This is the inclusive or, not the "one or the other but not both" you sometimes mean in everyday speech.

There are two sides to working with disjunction:

Proving a disjunction is like choosing a door. You pick one side and prove it:

Or.inl hp — "I'll prove the left side." Takes a proof hp : P and gives you P ∨ Q.
Or.inr hq — "I'll prove the right side." Takes a proof hq : Q and gives you P ∨ Q.

Using a disjunction hypothesis is like case analysis. If you know h : P ∨ Q, you don't know which one is true, so you have to handle both possibilities. The tactic rcases h with hp | hq splits into two goals: one where you have hp : P, and one where you have hq : Q.

The Lean Proof

Here's the pattern. Suppose we want to prove that if P is true, then P ∨ Q:

theorem or_intro_left (P Q : Prop) (hp : P) : P ∨ Q := by
  exact Or.inl hp

Simple — we have hp : P, so we inject it into the left side of the disjunction with Or.inl.

Now suppose we're given P ∨ Q and need to do something with it. We split into cases:

theorem or_elim (P Q R : Prop) (h : P ∨ Q) (hpr : P → R) (hqr : Q → R) : R := by
  rcases h with hp | hq
  · exact hpr hp
  · exact hqr hq

The rcases tactic splits h into two cases. In each case, we use the relevant implication to reach R.

Your Turn

Prove that disjunction is commutative — if P ∨ Q, then Q ∨ P. You'll need to case-split and then rebuild the disjunction with the sides swapped.

theorem or_comm (P Q : Prop) (h : P ∨ Q) : Q ∨ P := by
  sorry

Try it in Lean 4 Web. Think about it: if P is true, which side of Q ∨ P does that prove?

Hint

Start by case-splitting on h with rcases h with hp | hq. This gives you two goals.

In the first case, you have hp : P and need Q ∨ P. Since P is true, that goes on the right side — so use Or.inr.

In the second case, you have hq : Q and need Q ∨ P. Q goes on the left — use Or.inl.

Solution

theorem or_comm (P Q : Prop) (h : P ∨ Q) : Q ∨ P := by
  rcases h with hp | hq
  · exact Or.inr hp
  · exact Or.inl hq

We split h : P ∨ Q into two cases. When we have hp : P, we put it on the right of Q ∨ P with Or.inr. When we have hq : Q, we put it on the left with Or.inl. The sides swap perfectly.

← Conjunction (and) If and only if →