Analyze and explain why Isabelle or Coq proofs fail, identifying the root cause such as type mismatches, missing assumptions, incorrect goals, unification failures, or inapplicable tactics. Use when the user encounters proof failures, error messages in formal verification, stuck proof states, or asks why their Isabelle/Coq proof doesn't work.
Analyze and explain why Isabelle or Coq proofs fail, identifying the root cause such as type mismatches, missing assumptions, incorrect goals, unification failures, or inapplicable tactics. Use when the user encounters proof failures, error messages in formal verification, stuck proof states, or asks why their Isabelle/Coq proof doesn't work.
Proof Failure Explainer
Overview
Diagnose and explain proof failures in Isabelle and Coq by analyzing proof states, error messages, and goal structures. This skill helps identify root causes and suggests fixes for common proof problems.
Analysis Workflow
Step 1: Gather Context
Collect information about the failure:
Proof state:
Current goal(s)
Available hypotheses/assumptions
Context (definitions, lemmas in scope)
Error message:
Exact error text
Which tactic failed
Line/position of failure
Proof attempt:
What tactics were tried
What was expected to happen
Where the proof got stuck
Step 2: Identify Failure Category
Classify the type of failure:
Type Errors:
Type mismatch in expressions
Wrong function argument types
Incompatible type unification
Unification Failures:
Cannot unify terms
Existential variables not instantiated
Pattern matching failures
Missing Assumptions:
Unprovable without additional hypotheses
Missing preconditions
Insufficient context
Incorrect Goals:
Goal statement is false
Goal too strong or too weak
Wrong quantifier order
Tactic Failures:
Tactic not applicable to goal
Wrong tactic for goal structure
Induction hypothesis too weak
Scope Issues:
Variables not in scope
Shadowed variables
Context problems
Step 3: Analyze Root Cause
Examine the specific failure:
For Type Errors:
Check each term's type:
- What type does the term have?
- What type is expected?
- Where does the mismatch occur?
For Unification Failures:
Compare terms that should unify:
- Are they syntactically equal?
- What substitution would make them equal?
- Is that substitution possible?
For Missing Assumptions:
Identify what's needed:
- What fact would make the goal provable?
- Is it missing from hypotheses?
- Should it be a precondition?
For Incorrect Goals:
Verify goal correctness:
- Is the statement actually true?
- Can you find a counterexample?
- Is it too strong/weak?
Lemma comm_fail : forall x y z : nat, x + y = y + z.
Proof.
intros. reflexivity.
Qed.
Error:
Unable to unify "x + y" with "y + z".
Explanation:
The proof fails because:
reflexivity requires both sides to be syntactically equal
x + y and y + z are not equal without knowing x = z
You're trying to prove something that's not true in general
Solution:
Either fix the goal or add the necessary assumption:
(* Option 1: Fix the goal to something true *)
Lemma comm_correct : forall x y : nat, x + y = y + x.
Proof.
intros. lia.
Qed.
(* Option 2: Add assumption *)
Lemma comm_with_assumption : forall x y z : nat, x = z -> x + y = y + z.
Proof.
intros. rewrite H. reflexivity.
Qed.
Example 3: Missing Assumption
User's Failing Proof (Isabelle):
lemma "x > 0 ⟹ x + y > y"
by simp
Error:
Failed to apply initial proof method
Explanation:
The proof fails because:
For integers, x + y > y requires x > 0
The assumption is stated, but simp alone is insufficient
Need arithmetic reasoning, not just simplification
Solution:
lemma "x > (0::int) ⟹ x + y > y"
by arith
Or in Coq:
Lemma add_positive : forall x y : nat, x > 0 -> x + y > y.
Proof.
intros. lia.
Qed.
Example 4: Wrong Tactic
User's Failing Proof (Coq):
Lemma or_intro : forall P Q : Prop, P -> P \/ Q.
Proof.
intros. split.
Qed.
Error:
Unable to unify "?P /\ ?Q" with "P \/ Q".
Explanation:
The proof fails because:
split is for conjunction (/\), not disjunction (\/)
The goal is P \/ Q (disjunction)
You need left or right for disjunction
Solution:
Lemma or_intro : forall P Q : Prop, P -> P \/ Q.
Proof.
intros. left. assumption.
Qed.
