"""Claude as a pure decomposer: the model states subgoals; automated provers prove everything. The design the project set out to build. For every goal: 1. Leaf provers try it: Rocq automation, a generic induction-then-automation tactic, and CoqHammer (Vampire, E; the proof is rebuilt as a Rocq tactic). 2. If they fail, Claude proposes up to 2 alternative decompositions, each 2-4 subgoals. Claude writes NO tactics: it only states the subgoals, as Rocq propositions. 3. The leaf provers must derive the goal from the subgoals (taken as hypotheses), and then prove each subgoal, recursively (AND). Alternatives are tried in order (OR). So every proof step is found by the automated provers; the model's only contribution is the choice of intermediate statements. Proposer: Claude through isolated, stateless Claude Code calls (no tools, no files, no project memory, each from an empty folder). It sees only the vocabulary, the postulates, the lemmas proved so far for this task, and the goal -- never the repository's proofs. Statements: ../htps/heldout20.py. Logs: runs_decomp/. Proofs: proofs_decomp/. Usage: python3 pilot_decomp.py [task ...] (no argument: all twenty) """ import json, re, subprocess, sys, tempfile, time from concurrent.futures import ThreadPoolExecutor from pathlib import Path HERE = Path(__file__).resolve().parent sys.path.insert(0, str(HERE)); sys.path.insert(0, str(HERE.parent / "htps")) import pilot, heldout20 from rocq_env import HAMMER_BIN, HAMMER_ENV RUNS = HERE / "runs_decomp"; RUNS.mkdir(exist_ok=True) PROOFS = HERE / "proofs_decomp"; PROOFS.mkdir(exist_ok=True) TASKS = heldout20.TASKS MAX_DEPTH, MAX_CALLS = 4, 30 HEAD = heldout20.PREAMBLE.replace("From Stdlib Require Import Classical Relations.", "From Stdlib Require Import Classical Relations.\nFrom Hammer Require Import Hammer Tactics.") HEAD += "\nSet Hammer ATPLimit 20.\nSet Hammer ReconstrLimit 10.\n" UNF = ("unfold MP001, MP002, MP003, MP007, MP008, MP009, MP010, MP011, MP012, OP001, OP006, SP001, OfItself, " "ThroughAnother, Necessary, Possible, InUniverse, DependsOn, Independent, NonExistencePossible, AggregateOfPossibles in *") # Fixed, generic leaf tactics: the same list for every goal, written before the run. LEAF = ["intros; firstorder.", f"{UNF}; intros; firstorder.", f"{UNF}; intros; intuition eauto.", f"{UNF}; intros; apply NNPP; intro; firstorder.", # induction on a chain hypothesis, then automation (the provers cannot do induction by themselves) "intros; match goal with H : clos_trans _ _ _ _ |- _ => induction H end; firstorder eauto.", f"{UNF}; intros; match goal with H : clos_trans _ _ _ _ |- _ => induction H end; firstorder eauto.", "intros; match goal with H : clos_trans_1n _ _ _ _ |- _ => induction H end; firstorder eauto."] HAMMER = ["intros; hammer.", f"{UNF}; intros; hammer.", f"{UNF}; intros; apply NNPP; intro; hammer."] FORBID = re.compile(r"\b(Admitted|admit|Axiom|Parameter|Hypothesis|Variable|Section|End|Proof|Qed)\b") SYSTEM = ("You are an expert in the Rocq Prover (version 9, formerly Coq). You decompose goals into simpler " "subgoals for automated provers. You never write tactics. You reply with JSON only, no prose, no markdown fences.") def compile_(src, timeout): with tempfile.TemporaryDirectory() as d: f = Path(d) / "Check.v"; f.write_text(src) try: r = subprocess.run([HAMMER_BIN + "/rocq", "compile", "-q", str(f)], capture_output=True, text=True, timeout=timeout, cwd=d, env=HAMMER_ENV) return r.returncode == 0, r.stdout + r.stderr except subprocess.TimeoutExpired: return False, "TIMEOUT" class Run: def __init__(self, task): self.task, self.calls, self.counter = task, 0, 0 self.lemmas = [] # (name, statement, proof) self.log = open(RUNS / f"{task}.jsonl", "w") def record(self, **kw): kw["time"] = time.strftime("%Y-%m-%dT%H:%M:%S"); self.log.write(json.dumps(kw) + "\n"); self.log.flush() def src(self, hyps, name, stmt, proof): body = HEAD + "".join(f"\nLemma {n} : {s}.\nProof.\n{p}\nQed.\n" for n, s, p in self.lemmas) body += "".join(f"Hypothesis {h} : {s}.\n" for h, s in hyps) return body + f"\nLemma {name} : {stmt}.\nProof.\n{proof}\nQed.\n\nEnd Pilot.\n" def leaf(self, hyps, stmt, path, stage): """The automated provers only. Returns a checked tactic script, or None.""" name = f"{self.task}_try" for tac in LEAF: ok, _ = compile_(self.src(hyps, name, stmt, tac), 60) if ok: self.record(kind="leaf", stage=stage, path=path, stmt=stmt, prover="automation", proof=tac); return tac for tac in HAMMER: ok, out = compile_(self.src(hyps, name, stmt, tac), 150) m = re.search(r"Replace the hammer tactic with:\s*(.+?)\s*$", out, re.M) if ok else None if m: final = tac.replace("hammer.", m.group(1).strip().rstrip(".") + ".") ok2, _ = compile_(self.src(hyps, name, stmt, final), 150) if ok2: self.record(kind="leaf", stage=stage, path=path, stmt=stmt, prover="CoqHammer", proof=final); return final self.record(kind="leaf_failed", stage=stage, path=path, stmt=stmt) return None def ask(self, stmt): if self.calls >= MAX_CALLS: return None self.calls += 1 avail = "\n".join(f"Lemma {n} : {s}." for n, s, _ in self.lemmas) or "(none yet)" prompt = (f"Rocq context (a Section; you cannot change it):\n{heldout20.PREAMBLE}\n" f"Lemmas already proved in this section:\n{avail}\n\nGoal:\n{stmt}\n\n" "Automated provers (first-order automation, CoqHammer, and induction on a clos_trans or clos_trans_1n " "hypothesis followed by automation) could not prove this goal. Decompose it into 2 to 4 simpler " "subgoals: closed Rocq propositions over the section's vocabulary, such that the goal follows easily " "from them and each is easier to prove than the goal. Do NOT write any tactics or proofs; the " "automated provers will derive the goal from the subgoals and prove each subgoal. Propose up to 2 " 'alternative decompositions. Reply as JSON: {"decompositions": [{"subgoals": ["...", "..."]}]}') with tempfile.TemporaryDirectory() as d: # empty folder: no project, no memory t0 = time.time() try: r = subprocess.run(["claude", "-p", "--model", pilot.MODEL, "--tools", "", "--strict-mcp-config", "--setting-sources", "", "--no-session-persistence", "--system-prompt", SYSTEM, "--output-format", "json", prompt], cwd=d, capture_output=True, text=True, timeout=300) meta = json.loads(r.stdout); text = meta.get("result", ""); model = list((meta.get("modelUsage") or {}).keys()) except Exception as e: text, model = f"(call failed: {e})", [] self.record(kind="model_call", n=self.calls, model=model, seconds=round(time.time() - t0, 1), prompt=prompt, response=text) m = re.search(r"\{.*\}", text, re.S) try: return json.loads(m.group(0)) if m else None except Exception: return None def fresh(self): self.counter += 1 return f"{self.task}_L{self.counter}" def prove(self, stmt, depth, path): known = next((n for n, s, _ in self.lemmas if " ".join(s.split()) == " ".join(stmt.split())), None) if known: return known tac = self.leaf([], stmt, path, "leaf") if tac: name = self.fresh(); self.lemmas.append((name, stmt, tac)); return name if depth >= MAX_DEPTH: return None for dec in ((self.ask(stmt) or {}).get("decompositions") or [])[:2]: subs = [s for s in (dec.get("subgoals") or []) if isinstance(s, str)][:4] if not subs or any(FORBID.search(s) for s in subs): self.record(kind="rejected", reason="bad format", decomposition=dec); continue hyps = [(f"sub{i+1}", s.strip().rstrip(".")) for i, s in enumerate(subs)] # well-formed? ok, out = compile_(HEAD + "".join(f"Definition chk{i} : Prop := {s}.\n" for i, (_, s) in enumerate(hyps)) + "End Pilot.\n", 60) if not ok: self.record(kind="rejected", reason="subgoal does not typecheck", subgoals=subs, rocq=out[-400:]); continue comb = self.leaf(hyps, stmt, path, "combine") if not comb: continue names = [] for i, (_, s) in enumerate(hyps): n = self.prove(s, depth + 1, path + [i + 1]) if n is None: break names.append(n) if len(names) != len(hyps): continue proof = "".join(f"pose proof {n} as sub{i+1}. " for i, n in enumerate(names)) + comb name = self.fresh() ok, out = compile_(self.src([], name, stmt, proof), 150) self.record(kind="assembled", path=path, stmt=stmt, subgoals=[s for _, s in hyps], proof=proof, ok=ok) if ok: self.lemmas.append((name, stmt, proof)); return name return None def one(task): stmt = TASKS[task] run = Run(task); t0 = time.time() top = run.prove(stmt, 0, []) res = {"proved": top is not None, "model_calls": run.calls, "seconds": round(time.time() - t0, 1)} if top: body = HEAD for n, s, p in run.lemmas: body += f"\nLemma {n} : {s}.\nProof.\n{p}\nQed.\n" if n == top: break body += f"\nEnd Pilot.\n\nPrint Assumptions {top}.\n" (PROOFS / f"{task}.v").write_text(body) ok, out = compile_(body, 600) axioms = re.findall(r"^(\S+) :", out.split("Axioms:")[-1], re.M) if "Axioms:" in out else [] res.update(final_compiles=ok, axioms=axioms, lemmas=body.count("\nLemma ") - 0) run.record(kind="result", **res) print(task, json.dumps(res), flush=True) return task, res if __name__ == "__main__": tasks = sys.argv[1:] or list(TASKS) with ThreadPoolExecutor(4) as ex: summary = dict(ex.map(one, tasks)) (HERE / "summary_decomp.json").write_text(json.dumps(summary, indent=2)) ok = [t for t, r in summary.items() if r["proved"] and r.get("final_compiles") and set(r.get("axioms", [])) <= {"classic"}] print(f"PROVED {len(ok)} of {len(tasks)}", flush=True)