2.4 Disjunction

Disjunction represents “or”. A proof of P ∨ Q contains one piece of evidence: either a proof of P or a proof of Q, tagged with the side from which it came. In Lean, disjunction behaves like a sum type for propositions.

Problem

You want to prove or use a statement of the form:

P ∨ Q

To prove it, you must choose one side and provide a proof of that side. To use it, you must handle both possible cases.

Solution

Use left to prove the left side of a disjunction.

theorem make_left_disjunction (P Q : Prop) : P -> P ∨ Q := by
  intro hp
  left
  exact hp

Use right to prove the right side.

theorem make_right_disjunction (P Q : Prop) : Q -> P ∨ Q := by
  intro hq
  right
  exact hq

After left, the goal changes from:

⊢ P ∨ Q

to:

⊢ P

After right, the goal changes from:

⊢ P ∨ Q

to:

⊢ Q

Discussion

A conjunction requires both sides. A disjunction requires one side. This makes introduction easy and elimination more careful.

If you have a hypothesis:

h : P ∨ Q

you cannot simply extract P or Q. The proof may have come from either side. To use h, you must perform case analysis.

theorem disjunction_comm (P Q : Prop) : P ∨ Q -> Q ∨ P := by
  intro h
  cases h with
  | inl hp =>
    right
    exact hp
  | inr hq =>
    left
    exact hq

There are two cases.

In the first case, Lean gives:

hp : P
⊢ Q ∨ P

So the proof chooses the right side.

In the second case, Lean gives:

hq : Q
⊢ Q ∨ P

So the proof chooses the left side.

Constructors

The two constructors for disjunction are Or.inl and Or.inr.

theorem disjunction_left_term (P Q : Prop) : P -> P ∨ Q :=
  fun hp => Or.inl hp

theorem disjunction_right_term (P Q : Prop) : Q -> P ∨ Q :=
  fun hq => Or.inr hq

The constructor names mean “inject left” and “inject right”.

Their shapes are:

Or.inl : P -> P ∨ Q
Or.inr : Q -> P ∨ Q

The tactics left and right are tactic-mode wrappers around these constructors.

Eliminating a Disjunction

To prove a result R from P ∨ Q, prove R in both cases.

theorem disjunction_elim
    (P Q R : Prop) :
    (P -> R) -> (Q -> R) -> P ∨ Q -> R := by
  intro hpr
  intro hqr
  intro hpq
  cases hpq with
  | inl hp =>
    exact hpr hp
  | inr hq =>
    exact hqr hq

The structure is important. A disjunction gives alternatives. To obtain a single conclusion from alternatives, both alternatives must lead to that conclusion.

Nested Disjunctions

Nested disjunctions require nested case analysis.

theorem disjunction_assoc
    (P Q R : Prop) :
    (P ∨ Q) ∨ R -> P ∨ (Q ∨ R) := by
  intro h
  cases h with
  | inl hpq =>
    cases hpq with
    | inl hp =>
      left
      exact hp
    | inr hq =>
      right
      left
      exact hq
  | inr hr =>
    right
    right
    exact hr

The hypothesis has type:

h : (P ∨ Q) ∨ R

The outer disjunction first splits into:

hpq : P ∨ Q

or:

hr : R

The hpq case must then be split again.

Pattern Matching in intro

You can destruct a disjunction when it is introduced.

theorem disjunction_comm_intro_pattern
    (P Q : Prop) :
    P ∨ Q -> Q ∨ P := by
  intro h
  rcases h with hp | hq
  · right
    exact hp
  · left
    exact hq

The rcases tactic is often convenient for destructuring disjunctions, conjunctions, existentials, and nested combinations of them.

For simple beginner proofs, cases is usually clearer because it directly displays the constructors.

Disjunction with Existing Implications

A common pattern is to combine disjunction elimination with implication application.

theorem disjunction_map
    (P Q R S : Prop) :
    (P -> R) -> (Q -> S) -> P ∨ Q -> R ∨ S := by
  intro hpr
  intro hqs
  intro hpq
  cases hpq with
  | inl hp =>
    left
    exact hpr hp
  | inr hq =>
    right
    exact hqs hq

The proof says: if the disjunction was proved from P, map that proof to R; if it was proved from Q, map that proof to S.

Choosing the Correct Side

Lean does not choose a side of a disjunction automatically unless automation has enough information.

theorem choose_right
    (P Q : Prop)
    (hq : Q) :
    P ∨ Q := by
  right
  exact hq

Trying left here would leave the goal:

⊢ P

but the context only contains:

hq : Q

So the proof would fail unless you also had a proof of P.

Disjunction and False

False is the empty proposition. A disjunction with False can often be simplified by case analysis.

theorem false_or (P : Prop) : False ∨ P -> P := by
  intro h
  cases h with
  | inl hf =>
    cases hf
  | inr hp =>
    exact hp

In the left case, hf : False. Since False has no constructors, cases hf closes the goal.

theorem or_false (P : Prop) : P ∨ False -> P := by
  intro h
  cases h with
  | inl hp =>
    exact hp
  | inr hf =>
    cases hf

Common Patterns

To prove:

⊢ P ∨ Q

use one of:

left

or:

right

then prove the selected side.

To use:

h : P ∨ Q

use:

cases h with
| inl hp => ...
| inr hq => ...

To map a disjunction through implications, split it into cases and rebuild the target disjunction.

Common Pitfalls

Do not try to extract both sides from a disjunction. A proof of P ∨ Q contains one side, not both.

Do not choose left or right before checking which proof is available. The chosen side becomes the new goal.

Do not forget to handle both cases when using a disjunction hypothesis. A proof that only handles one case is incomplete.

Do not confuse P ∨ Q with boolean or. A proof of P ∨ Q carries evidence for one side.

Takeaway

A disjunction is a tagged proof of one side. To prove P ∨ Q, choose P or choose Q. To use P ∨ Q, split into cases and prove the desired result in each case. This explains left, right, Or.inl, Or.inr, and case analysis on disjunctions.