Strategy: Case analysis

Pattern recognition

When you see: a hypothesis of the form h : P ∨ Q

Strategy: Consider each case separately. Prove the goal assuming P, then prove it again assuming Q.

Tactic: rcases h with hp | hq

A disjunction P ∨ Q tells you one of two things is true, but not which. To use it, you must handle both possibilities. This creates two subgoals with the same target but different hypotheses.

This is Velleman's "proof by cases" — when your information branches, your proof must branch too.

Watch the strategy in action

The rule

Hypothesis:  h : P ∨ Q
Action:      rcases h with hp | hq
Effect:      Two subgoals created:
             Case 1: hp : P, prove the goal
             Case 2: hq : Q, prove the goal
Think:       "Either P or Q is true. Handle both."

Your turn

Prove that Or is associative (one direction): if (P ∨ Q) ∨ R then P ∨ (Q ∨ R).

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

Hint

Case split on h first to get P ∨ Q vs R. Then case split again on the P ∨ Q case. Use Or.inl and Or.inr to build the result.

Solution

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

← Split the goal Contradiction →