proof-failure-explainer

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:

1. Proof state:

   • Current goal(s)
   • Available hypotheses/assumptions
   • Context (definitions, lemmas in scope)

2. Error message:

   • Exact error text
   • Which tactic failed
   • Line/position of failure

3. 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?