2.15 Case Analysis

Case analysis is the proof pattern for using data that has more than one possible constructor. In logic, it appears most often with disjunctions, existentials, booleans, natural numbers, and inductive propositions. The basic rule is simple: if a hypothesis could have been built in several ways, prove the goal for each possible way.

Problem

You have a hypothesis whose type has constructors, and you want to use the information inside it.

Typical examples are:

h : P ∨ Q

h : ∃ x : α, P x

n : Nat

To use such a hypothesis, split it into its possible cases.

Solution

Use cases.

theorem or_case_analysis
    (P Q R : Prop)
    (h : P ∨ Q)
    (hp : P -> R)
    (hq : Q -> R) :
    R := by
  cases h with
  | inl hp_proof =>
    exact hp hp_proof
  | inr hq_proof =>
    exact hq hq_proof

The hypothesis h : P ∨ Q has two possible constructors:

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

So cases h creates two branches. In the first branch, Lean gives a proof of P. In the second branch, Lean gives a proof of Q.

Case Analysis on Disjunction

Disjunction is the most common logical example.

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

In the inl branch, the original proof came from the left side, so the context contains:

hp : P
⊢ Q ∨ P

In the inr branch, the context contains:

hq : Q
⊢ Q ∨ P

Each branch must independently prove the same target.

Case Analysis on Conjunction

A conjunction has only one constructor, but cases is still useful because it exposes the two fields.

theorem and_case_analysis
    (P Q : Prop) :
    P ∧ Q -> Q ∧ P := by
  intro h
  cases h with
  | intro hp hq =>
    constructor
    · exact hq
    · exact hp

Here there is only one branch, because And.intro is the only constructor of conjunction. The branch receives both components:

hp : P
hq : Q

Case Analysis on Existentials

An existential also has one constructor. Case analysis exposes the witness and the proof.

theorem exists_case_analysis
    (P : Nat -> Prop)
    (h : ∃ n : Nat, P n) :
    ∃ m : Nat, P m := by
  cases h with
  | intro n hn =>
    use n
    exact hn

The case gives:

n  : Nat
hn : P n

The witness is now available as an ordinary local variable.

Case Analysis on False

False has no constructors, so case analysis closes the goal.

theorem false_cases
    (P : Prop)
    (h : False) :
    P := by
  cases h

There are no branches to prove. This is why contradiction can prove anything.

Case Analysis on True

True has one constructor and no useful fields.

theorem true_cases
    (P : Prop)
    (h : True)
    (hp : P) :
    P := by
  cases h
  exact hp

The proof still has to prove P. The hypothesis h : True provides no useful data.

Case Analysis on Natural Numbers

Natural numbers have two constructors:

Nat.zero : Nat
Nat.succ : Nat -> Nat

So case analysis on n : Nat creates a zero case and a successor case.

theorem nat_cases_example
    (n : Nat) :
    n = 0 ∨ ∃ k : Nat, n = k + 1 := by
  cases n with
  | zero =>
    left
    rfl
  | succ k =>
    right
    use k

In the zero branch, n is replaced by 0. In the successor branch, n is replaced by Nat.succ k.

Case Analysis with rcases

The rcases tactic gives compact patterns for destructuring hypotheses.

theorem rcases_or
    (P Q R : Prop)
    (h : P ∨ Q)
    (hp : P -> R)
    (hq : Q -> R) :
    R := by
  rcases h with hp_proof | hq_proof
  · exact hp hp_proof
  · exact hq hq_proof

For conjunctions and existentials:

theorem rcases_exists_and
    (P Q : Nat -> Prop)
    (h : ∃ n : Nat, P n ∧ Q n) :
    ∃ n : Nat, Q n ∧ P n := by
  rcases h with ⟨n, hp, hq⟩
  use n
  constructor
  · exact hq
  · exact hp

The pattern:

⟨n, hp, hq⟩

unpacks the existential witness and the two conjunction components.

Case Analysis with match

The same reasoning can be written in term mode with pattern matching.

theorem or_comm_match
    (P Q : Prop) :
    P ∨ Q -> Q ∨ P :=
  fun h =>
    match h with
    | Or.inl hp => Or.inr hp
    | Or.inr hq => Or.inl hq

This makes the constructors explicit. Tactic-mode cases and term-mode match perform the same logical split.

Preserving Names

When cases replaces a variable, names can become hard to read. Use branch names and field names intentionally.

theorem nat_cases_named
    (n : Nat) :
    n = 0 ∨ ∃ k : Nat, n = Nat.succ k := by
  cases n with
  | zero =>
    left
    rfl
  | succ k =>
    right
    use k

The name k makes the successor predecessor explicit.

Case Analysis on Decidable Propositions

Classical logic provides case analysis on arbitrary propositions.

open Classical

theorem proposition_cases
    (P Q : Prop)
    (hp : P -> Q)
    (hnp : ¬ P -> Q) :
    Q := by
  by_cases h : P
  · exact hp h
  · exact hnp h

The tactic by_cases h : P creates two branches:

h : P

and:

h : ¬ P

This is different from cases h. The proposition P is not being destructed. Instead, classical excluded middle is being used to split on whether P holds.

Case Analysis vs Induction

Case analysis splits only the outer constructor. Induction gives an additional induction hypothesis for recursive data.

For example, case analysis on n : Nat gives:

n = 0

or:

n = Nat.succ k

but no statement about k.

Induction on n gives a successor branch with an induction hypothesis about k.

Use cases when the immediate shape is enough. Use induction when proving a property for all recursive values.

Common Patterns

To split a disjunction:

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

To unpack a conjunction:

cases h with
| intro hp hq => ...

To unpack an existential:

cases h with
| intro x hx => ...

To destruct compactly:

rcases h with ⟨x, hx₁, hx₂⟩

To split natural numbers:

cases n with
| zero => ...
| succ k => ...

To split a decidable proposition:

by_cases h : P

Common Pitfalls

Do not use case analysis when induction is required. If the property must be proved recursively, use induction.

Do not forget that every branch must prove the same final goal.

Do not assume a disjunction gives both sides. Case analysis gives one side in each branch.

Do not confuse cases h with by_cases h : P. The first destructs existing evidence. The second creates a logical split.

Takeaway

Case analysis uses the constructors of a type or proposition. Each constructor gives one proof branch. In each branch, Lean exposes the data carried by that constructor, and the goal must be proved under those assumptions. This pattern is the basis for working with disjunctions, existentials, booleans, natural numbers, and inductive proofs.