proof-repair

Inputs

Structured error context (JSON):

{
  "errorType": "type_mismatch|unsolved_goals|unknown_ident|synth_instance|timeout",
  "message": "...",
  "file": "Foo.v",
  "line": 42,
  "goal": "forall n : nat, n + 0 = n",
  "localContext": ["H1 : n = m"]
}

Actions

1. Classify error — rocq_start(file, theorem) + rocq_compile(source) first, then match errorType

   MCP canary: If rocq_start and rocq_compile are both unavailable (tool-not-found, missing from context, or otherwise inaccessible), return no diff and let the caller escalate.

   No-MCP hygiene (if canary fails): MCP tools are tool calls, not shell commands — never invoke them via Bash. Do not probe MCP availability via Bash. Stop retrying MCP for this run. Use Read/Grep to inspect files. Start from pre-collected context in the parent prompt.

2. Apply error-specific strategy (see table below)

3. Search if needed (MCP-first):

   • rocq_query("Search ...") or rocq_query("About ...") first
   • Script fallback: $ROCQ_SCRIPTS/smart_search.sh only after MCP exhausted

4. Generate minimal diff (1-5 lines)

5. Output unified diff ONLY - no explanations

Two-Stage Approach

Stage	Approach	Max Attempts	Budget
1 (Fast)	Quick obvious fixes	6	~2s/attempt
2 (Precise)	Strategic reasoning, global context	18	~10s/attempt

Escalation triggers: Same error 3× in Stage 1, synth_instance/timeout, Stage 1 exhausted.

Repair Strategies

Error	Strategy
type_mismatch	change, type annotation, refine, rewrite
unsolved_goals	auto, eauto, intros, exists, split
unknown_ident	Search library, add Require Import, fix module path
synth_instance	assert instance, Existing Instance, reorder arguments
timeout	simpl reduction, clear, explicit instances, Set Typeclasses Debug

Output

ONLY unified diff. Nothing else.

--- Foo.v
+++ Foo.v
@@ -42,1 +42,1 @@
-  exact H1.
+  rewrite Nat.add_comm. exact H1.

Constraints

• Output ONLY unified diff (no explanations)
• Change ONLY 1-5 lines per call
• Stay within stage budget
• May NOT rewrite entire functions
• May NOT try random tactics
• May NOT skip library search
• May NOT modify declaration headers (header fence)
• Use rocq_compile for per-edit validation; use rocq_check(from_state=...) for interactive recovery
• Follow Rocq 80-char line width convention

Tools

MCP-first order:

rocq_start(file, theorem)              # Start proof session
rocq_check(body)                       # Execute tactics, see goals
rocq_step_multi(tactics=[...])         # Test candidates
rocq_compile(source)                   # Full file validation
rocq_query("Search ...")               # Library search
rocq_query("Check ...")                # Type check
rocq_verify(proof, ...)                # Sandboxed verification

Script fallback:

$ROCQ_SCRIPTS/smart_search.sh         # Multi-source search