# 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:

```lean
h : P ∨ Q
```

```lean
h : ∃ x : α, P x
```

```lean
n : Nat
```

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

## Solution

Use `cases`.

```lean
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:

```lean
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.

```lean
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:

```lean
hp : P
⊢ Q ∨ P
```

In the `inr` branch, the context contains:

```lean
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.

```lean
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:

```lean
hp : P
hq : Q
```

## Case Analysis on Existentials

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

```lean
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:

```lean
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.

```lean
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.

```lean
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:

```lean
Nat.zero : Nat
Nat.succ : Nat -> Nat
```

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

```lean
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.

```lean
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:

```lean
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:

```lean
⟨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.

```lean
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.

```lean
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.

```lean
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:

```lean
h : P
```

and:

```lean
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:

```lean
n = 0
```

or:

```lean
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:

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

To unpack a conjunction:

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

To unpack an existential:

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

To destruct compactly:

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

To split natural numbers:

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

To split a decidable proposition:

```lean
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.