Debug proof failures using counterexamples from Nitpick (Isabelle) or QuickChick (Coq) to identify specification errors, missing preconditions, and proof strategy issues. Use when: (1) A proof attempt fails and you need to understand why, (2) Counterexamples are generated by Nitpick or QuickChick, (3) Specifications may be incorrect or incomplete, (4) Theorems need validation before proving, (5) Missing preconditions or lemmas need identification, or (6) Proof failures need explanation and correction suggestions. Supports both Isabelle/HOL and Coq equally.
Debug proof failures using counterexamples from Nitpick (Isabelle) or QuickChick (Coq) to identify specification errors, missing preconditions, and proof strategy issues. Use when: (1) A proof attempt fails and you need to understand why, (2) Counterexamples are generated by Nitpick or QuickChick, (3) Specifications may be incorrect or incomplete, (4) Theorems need validation before proving, (5) Missing preconditions or lemmas need identification, or (6) Proof failures need explanation and correction suggestions. Supports both Isabelle/HOL and Coq equally.
Counterexample-Guided Proof Debugger
Analyze counterexamples from Nitpick or QuickChick to explain proof failures and suggest corrections to specifications or proofs.
Workflow
1. Receive Counterexample Information
Identify what information is provided:
Counterexample output: From Nitpick or QuickChick
Failed theorem: The statement that couldn't be proven
Proof attempt: Any partial proof or tactics tried
Context: Definitions and lemmas involved
2. Choose Target System
Determine which proof assistant is being used:
Isabelle/HOL with Nitpick: Finite model finder
Coq with QuickChick: Property-based testing
Both: Provide analysis for both systems
3. Analyze the Counterexample
Examine the counterexample systematically:
Verify the counterexample:
Manually compute the result for the given values
Confirm it actually violates the theorem
Check if it's a genuine counterexample or tool limitation
Identify the violation:
Which part of the theorem fails?
What values cause the failure?
Is it an edge case or fundamental issue?
Determine the root cause:
Missing precondition?
Incorrect specification?
Wrong quantifier order?
Implementation bug?
Off-by-one error?
Type constraint issue?
4. Explain the Failure
Provide clear explanation:
What went wrong:
Describe why the counterexample violates the theorem
Show the computation step-by-step
Highlight the specific point of failure
Why it happened:
Explain the underlying cause
Identify the conceptual error
Note any common patterns (empty list, boundary values, etc.)
Impact assessment:
Is the theorem fundamentally wrong?
Does it need preconditions?
Is the specification incomplete?
5. Suggest Corrections
Provide actionable fixes based on the root cause:
For missing preconditions:
(* Before *)
lemma "hd xs ∈ set xs"
(* After *)
lemma "xs ≠ [] ⟹ hd xs ∈ set xs"
For incorrect specifications:
(* Before: uses < instead of <= *)
x < y && is_sorted (y :: ys)
(* After *)
x <= y && is_sorted (y :: ys)
For quantifier order:
(* Before *)
"∃y. ∀x. P x y"
(* After *)
"∀x. ∃y. P x y"
For incomplete specifications:
(* Before: only checks sortedness *)
is_sorted (sort l)
(* After: also checks permutation *)
is_sorted (sort l) && permutation l (sort l)
6. Recommend Next Steps
Guide the user on what to do:
Retest with fix:
Run Nitpick/QuickChick again
Verify no counterexample found
Check if fix is sufficient
Identify additional issues:
Are there other edge cases?
Do other lemmas need fixing?
Is the specification now complete?
Proceed with proof:
If no counterexample, attempt proof
Suggest proof strategy
Identify needed helper lemmas
Counterexample Analysis Patterns
Pattern 1: Empty Structures
Symptom: Counterexample is [], {}, or None
Common causes:
Missing non-empty precondition
Undefined behavior on empty input
Base case not handled
Fix: Add precondition or handle empty case explicitly
Pattern 2: Boundary Values
Symptom: Counterexample is 0, 1, or type limits
Common causes:
Off-by-one errors
Boundary condition not considered
Edge case in arithmetic
Fix: Adjust bounds or add special case handling
Pattern 3: Duplicate Elements
Symptom: Counterexample has repeated values like [0, 0]
Common causes:
Using < instead of ≤
Assuming distinctness
Set vs. multiset confusion
Fix: Use appropriate comparison or add distinctness assumption
Pattern 4: Small Counterexamples
Symptom: Very small counterexample (1-2 elements)
Common causes:
Fundamental specification error
Wrong base case
Incorrect inductive step
Fix: Review base definitions and inductive structure
