Tony's Wiki

Proof Engineering Lessons (Rocq wp_isorec)

3 min read

Proof Engineering Lessons — Rocq mechanization (wp_isorec / bcd-full)

Reusable lessons from mechanizing wp subtyping. Distilled from Claude Code session transcripts (2026-05-28 → 06-05).

Mathematical / proof-architecture

  1. A definition redesign can dissolve several blockers at once. Changing dpart from a propositional ∀L. dcont L S → dcont L T to an inductive relation (with a strict dpart_andL_M on left intersections) made dpart_fv, wp_weaken_fresh’s μ-case, and wp_refl_empty all close — three separate walls gone from one principled change. When a lemma keeps needing a property the current definition cannot deliver, fix the definition, not the lemma.

  2. “Splitting the target is free for soundness; positivity only governs completeness” — but only when reassembly is ≡, not <:. The forward distribution ⋀Dᵢ <: C always holds, but lifting it through μ (P<:Q ⟹ μa.P <: μa.Q) is invalid when a occurs negatively/mixed — it needs P ≡ Q. The honest design moves the soundness obligation into a checkable global ≡ premise, not a syntactic positivity test (there is no stable syntactic positivity: μa.(a→Int)&(Top→Int) ≡ μa.Top→Int looks negative but splits fine). See Distributivity Subtyping Laws, Deep Target Splitting.

  3. Source grows, never shrinks. BCD genuinely allows merge-on-the-left (wp_arr/wp_mu take part B A), so any construction may only grow the source (wp_and_source_*, wp_to_leaves) and route cross-context composition through musub_compose. Source-projection / factoring lemmas (wp_and_source_inv, cover_src_fwd-style shrinking) are false or lossy — the recurring antipattern behind the transitivity wall (wp Transitivity via Cover Routing).

  4. Polarity is a property of the whole recursion, decided globally — never per target leaf. A variable occurring even partly contravariantly cannot be climbed; it must be matched rigidly. This is why the cover carries one CLIMB/RIGID cert per entry and why a single cert cannot serve an arrow leaf whose codomain mixes variances.

  5. Records do not deep-split (no dist_rcd in BCD), unlike arrows (dist_arrow) and μ (split-or-keep). dcont_rcd_keep is atomic.

Tactic / tooling

  1. Machine-check a candidate lemma (or its negation) immediately — do not reason about it in prose. Nearly every wasted branch was an over-strong helper that turned out false: wp_weaken_var, bridge_..._both_legs, the depth-bound, cont_dpart_disj, source-and-inversion. A 2-minute counterexample search beats an hour of proof attempt.

  2. Prove a concrete example before the general lemma. Machine-verifying the cover construction on cov_example validated the shape and broke a long concede-loop. Testing a candidate admit against a known-Qed witness (cov_example) is also how a false lemma that a prover had Qed’d was caught.

  3. coq-lsp masks errors that batch coqc rejects. rocq_start/rocq_check accepted whole files that rocq_compile_file (batch) failed (folded-vs-unfolded match, unification). Always validate with rocq_compile_file + rocq_assumptions before committing.

  4. fix … N; destruct (explicit-term recursion) for list-indexed body certs — wp_ind/induction do not provide IHs for the per-entry certs and re-quantify existential witnesses, breaking the guard checker. Pass the IH as an explicit application.

  5. rocq_assumptions after every milestone is necessary but not sufficient. It tracks which admits exist, not whether they are consistent — a prover can Qed against an inconsistent admit. Pair it with witness-testing (lesson 7).

  6. Minor friction worth pre-empting: cbn (not simpl) to reduce open_tt/^^; rename binders off constructor-bound names (X→Z); fsetdec is expensive — clear irrelevant hyps first.

Driving Claude Code on Hard Proofs · wp Transitivity via Cover Routing · Split-Cover and Polarity Certificates · iso-types

Sources

Claude Code sessions a801a8e3 c41d8a99 adb148b0 (05-28→30), 25ab7e44 (05-31), 271dc5fa 1f01730a 2eecaeb4 ed9a9e97 (06-04), 11cf3241 (06-05).

Graph View

Backlinks