# 2.25 Common Proof Mistakes and Debugging Lean proofs fail in predictable ways. The error messages often indicate a mismatch between the goal and the available assumptions, or a misuse of tactics. Effective debugging is a disciplined process: inspect the goal, inspect the context, and identify the exact mismatch. ## Problem A proof does not compile. Typical symptoms: * `tactic failed, no goals solved` * `type mismatch` * `unknown identifier` * `failed to unify` You need a systematic way to locate and fix the issue. ## Read the Goal and Context Always start by inspecting the proof state. ```lean P Q R : Prop hp : P hPQ : P -> Q ⊢ Q ``` If the goal is `Q` and you have `hPQ : P -> Q`, then Lean expects a proof of `P`. If you already have `hp : P`, the fix is immediate: ```lean exact hPQ hp ``` Many errors come from not aligning the goal with available hypotheses. ## Mistake: Using `assumption` Too Early ```lean -- does not work theorem bad_assumption (P Q : Prop) (hp : P) (hPQ : P -> Q) : Q := by assumption ``` Error: no hypothesis has type `Q`. Fix: ```lean exact hPQ hp ``` The tactic `assumption` does not apply functions. ## Mistake: Wrong Rewrite Direction ```lean -- fails theorem bad_rw (a b : Nat) (hAB : a = b) (hb : b + 1 = 5) : a + 1 = 5 := by rw [hAB] exact hb ``` After `rw [hAB]`, the goal becomes `b + 1 = 5`, but `hb` already has that type. This case actually works. The real failure happens when direction is reversed incorrectly. Example: ```lean -- fails rw [hAB] at hb ``` if the needed direction is opposite. Fix: ```lean rw [← hAB] exact hb ``` Always check which side must change. ## Mistake: No Matching Rewrite ```lean -- fails theorem rw_no_match (a b c : Nat) (hAB : a = b) : c + 1 = c + 1 := by rw [hAB] ``` There is no occurrence of `a` in the goal. Fix: do nothing, or use `rfl`. ## Mistake: Misusing `cases` ```lean -- incorrect idea theorem bad_cases (P Q : Prop) (hp : P) : P ∨ Q := by cases hp ``` `hp : P` is not an inductive type with multiple constructors. There is nothing to split. Fix: ```lean left exact hp ``` Use `cases` only on inductive structures such as `P ∨ Q`, `∃ x, P x`, or data types. ## Mistake: Forgetting to Introduce Variables ```lean -- fails theorem missing_intro (P Q : Prop) : P -> Q -> P := by exact hp ``` Error: `hp` is not in the context. Fix: ```lean intro hp hq exact hp ``` The goal must be transformed before using assumptions. ## Mistake: Incorrect Use of `apply` ```lean -- fails theorem bad_apply (P Q : Prop) (hp : P) (hPQ : P -> Q) : Q := by apply hp ``` `apply hp` expects `hp` to have type `A -> goal`. It does not. Fix: ```lean apply hPQ exact hp ``` `apply` must match the shape of the goal. ## Mistake: Forgetting a Subgoal ```lean -- incomplete theorem incomplete (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by constructor · exact hp ``` One goal remains: `⊢ Q`. Fix: ```lean constructor · exact hp · exact hq ``` Lean shows remaining goals. Always resolve all of them. ## Mistake: Confusing `True` and `False` ```lean -- incorrect reasoning theorem bad_true_false (P : Prop) (h : True) : P := by cases h ``` This does not work. `True` gives no information. Fix: you cannot derive `P` from `True` alone. Correct pattern: ```lean theorem false_case (P : Prop) (h : False) : P := by cases h ``` ## Mistake: Misusing Existentials ```lean -- fails theorem bad_exists (P : Nat -> Prop) (h : ∃ n, P n) : P 0 := by exact ? ``` You do not know that the witness is `0`. Fix: ```lean rcases h with ⟨n, hn⟩ ``` Then use `n` and `hn`. ## Mistake: Not Using Hypotheses ```lean -- overly complex theorem unused_hyp (P Q : Prop) (hp : P) (hPQ : P -> Q) : Q := by have : Q := by apply hPQ exact hp exact this ``` This works, but is unnecessarily indirect. Better: ```lean exact hPQ hp ``` Prefer direct use unless an intermediate result is reused. ## Mistake: Overusing Automation ```lean theorem too_much_automation (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by aesop ``` This works, but hides structure. Prefer: ```lean constructor · exact hp · exact hq ``` Use automation when structure is irrelevant. ## Debugging Strategy 1. Read the goal 2. Check if any hypothesis matches it exactly 3. If not, check for implications that produce it 4. If still not, inspect structure (∧, ∨, ∃, ∀) 5. Decide: introduce, destructure, or apply 6. If rewriting is needed, check direction and location ## Use `#check` and Hover Lean allows inspection of terms. ```lean #check hPQ #check hp ``` This shows types and helps align reasoning. In editors, hovering over identifiers shows their types. ## Use `simp?` and Error Messages `simp?` suggests simplifications. Error messages often indicate the mismatch: * `type mismatch` means wrong type used * `failed to unify` means goal and term differ structurally * `unknown identifier` means missing name Do not ignore error messages. They describe the failure precisely. ## Reduce the Problem If a proof is complex, isolate the failing part. ```lean have hq : Q := by -- debug here ``` Work inside the smaller goal. Once fixed, return to the full proof. ## Check Direction of Reasoning If forward reasoning fails, try backward reasoning. If `exact hQR (hPQ hp)` is unclear, rewrite as: ```lean apply hQR apply hPQ exact hp ``` Changing perspective often reveals the issue. ## Common Patterns Match goal exactly: ```lean exact h ``` Apply implication: ```lean apply h ``` Rewrite: ```lean rw [h] ``` Destructure: ```lean rcases h with ⟨x, hx⟩ ``` Split cases: ```lean cases h ``` Simplify: ```lean simp ``` ## Common Pitfalls Do not guess tactics blindly. Each step should match the goal shape. Do not ignore the goal state after each tactic. Do not assume Lean infers missing steps. Do not mix forward and backward reasoning without tracking intermediate goals. Do not let the context grow without purpose. ## Takeaway Debugging is alignment. The goal must match the output of some assumption or construction. When a proof fails, inspect the goal, inspect the context, and identify the mismatch. Then fix it by introducing variables, applying functions, rewriting equalities, or destructuring data.