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.

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:

exact hPQ hp

Many errors come from not aligning the goal with available hypotheses.

Mistake: Using assumption Too Early

-- does not work
theorem bad_assumption
    (P Q : Prop)
    (hp : P)
    (hPQ : P -> Q) :
    Q := by
  assumption

Error: no hypothesis has type Q.

Fix:

exact hPQ hp

The tactic assumption does not apply functions.

Mistake: Wrong Rewrite Direction

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

-- fails
rw [hAB] at hb

if the needed direction is opposite.

Fix:

rw [← hAB]
exact hb

Always check which side must change.

Mistake: No Matching Rewrite

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

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

left
exact hp

Use cases only on inductive structures such as P ∨ Q, ∃ x, P x, or data types.

Mistake: Forgetting to Introduce Variables

-- fails
theorem missing_intro
    (P Q : Prop) :
    P -> Q -> P := by
  exact hp

Error: hp is not in the context.

Fix:

intro hp hq
exact hp

The goal must be transformed before using assumptions.

Mistake: Incorrect Use of apply

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

apply hPQ
exact hp

apply must match the shape of the goal.

Mistake: Forgetting a Subgoal

-- incomplete
theorem incomplete
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  constructor
  · exact hp

One goal remains: ⊢ Q.

Fix:

constructor
· exact hp
· exact hq

Lean shows remaining goals. Always resolve all of them.

Mistake: Confusing True and False

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

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

Mistake: Misusing Existentials

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

rcases h with ⟨n, hn⟩

Then use n and hn.

Mistake: Not Using Hypotheses

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

exact hPQ hp

Prefer direct use unless an intermediate result is reused.

Mistake: Overusing Automation

theorem too_much_automation
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  aesop

This works, but hides structure.

Prefer:

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.

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

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:

apply hQR
apply hPQ
exact hp

Changing perspective often reveals the issue.

Common Patterns

Match goal exactly:

exact h

Apply implication:

apply h

Rewrite:

rw [h]

Destructure:

rcases h with ⟨x, hx⟩

Split cases:

cases h

Simplify:

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.