[P2] absolute-zero/proofs/coq: full rebuild on Coq 8.18 (split from standards#133 Coq half) #157

Background

Filed as a properly-scoped successor to the Coq half of standards#133 (Lean half done in absolute-zero#23).

standards#133's body said "finish Lean CNO cons-case + Coq tier-0 rebuild" with a P2 label and OWED scope of "discharge 4 axioms". A build attempt (Coq 8.18.0) shows that framing under-specified the actual state by a wide margin. The file doesn't compile at all, and at least one theorem is false under the current definitions.

Actual state of proofs/coq/common/CNO.v on Coq 8.18

A. Build-blocking incompatibilities (≥ 3 systemic)

1. inversion ... ; subst. auto-naming clobber. The original eval_app proof at -> direction, cons case references H3, generated by inversion H; subst.. Coq 8.18's inversion uses different positional auto-naming and H3 doesn't exist. Same pattern repeats elsewhere.
2. Wrong-order intros pattern in eval_app <- direction. After three generalize dependent calls and induction p1, the goal binders are in the order forall s sm, eval [] s sm -> forall s', eval p2 sm s' -> .... The code uses intros s sm s' Hp1 Hp2. which silently mis-binds s' to the eval [] s sm premise and Hp1 to the actual s', making subsequent inversion Hp1; subst. produce the famous error context s' : eval [] s sm, Hp1 : ProgramState, Hp2 : eval p2 sm Hp1. Correct order: intros s sm Hp1 s' Hp2.
3. repeat split + bullets + cross-bullet identifier reuse. Coq 8.18 enforces stricter name hygiene: once intros s runs in one bullet, the name s is "reserved" and a sibling bullet's intros s s' Heval. fails with "s is already used". Fix is to convert each affected proof from repeat split. + - bullets to split; { ... } + braces (which create a name scope reset). Affected: at least cno_composition, empty_is_cno, nop_is_cno, plus 5+ more theorems following the same pattern. Total repeat split count in this file: 9.

B. Soundness defect (design decision required)

4. nop_is_cno : is_CNO [Nop] is false under the current state_eq. is_CNO's second clause requires eval p s s' -> s =st= s', and state_eq requires state_pc s1 = state_pc s2. But step s Nop = mkState s.(memory) s.(registers) s.(io) (S s.(state_pc)) — Nop bumps PC. So Nop changes state under state_eq, and nop_is_cno is unprovable. The original proof used inversion Heval; subst. inversion H; subst. inversion H0; subst. unfold state_eq. repeat split; try reflexivity. unfold mem_eq. reflexivity. — which only works if the underlying inversion silently absorbs the PC delta, which it doesn't on Coq 8.18 with strict checking. Two viable resolutions, owner-gated:

   • (a) Drop nop_is_cno — Nop is not a CNO under the strict pc-equality state_eq. The intuition that "Nop does nothing" only holds modulo PC, which is a different equivalence.
   • (b) Redefine state_eq to ignore PC. Then nop_is_cno is true and the file's CNO discourse becomes pc-agnostic. This is a bigger change because every theorem using state_eq re-checks under the relaxed definition.

   Either way, no purely-mechanical fix to nop_is_cno's proof works. This is a design call, not a proof debt.

C. Existing 4 axioms (the original OWED)

These are the Axiom declarations standards#133's body actually referenced:

• eval_deterministic (L445) — eval-relation is deterministic; proof comment says "TODO: Prove this axiom by induction on eval structure".
• cno_decidable (L523) — {is_CNO p} + {~ is_CNO p}. Decidability is non-trivial because is_CNO quantifies over all states.
• eval_respects_state_eq_right (L589) / eval_respects_state_eq_left (L601) — eval respects state-equality on both sides. Per the echo-types Agda↔Coq↔Lean4 correspondence (echo-types PR #64), these are precisely the 3 axioms that --safe --without-K (Agda) and Lean's no-axiom posture both forbid; they exist in Coq specifically to paper over the relational eval model's inability to derive determinism by direct case-splitting on a Fixpoint.

The deeper fix is to either (i) re-route through a Functional.eval Fixpoint formulation matching Agda + Lean (Route A in the echo-types correspondence appendix), at which point all four axioms reduce to refl, or (ii) discharge each axiom in place by induction on the eval inductive — the comments claim this is "straightforward" but until A/B/C above are fixed, the file doesn't even compile so the proofs can't be checked.

Recommended scope for this issue

Tier-0 in standards#133's sense ("zero axioms") is achievable but is not a P2 fixup. Proposed staged plan:

• Stage 1 — Coq 8.18 build repair. Convert all 9 repeat split. + bullet sites to split; { ... } blocks; fix the eval_app <- intros order; extract eval_nil_inv + eval_cons_inv helper lemmas to isolate inversion noise. File compiles modulo whatever resolution is chosen for nop_is_cno.
• Stage 2 — nop_is_cno design call. Owner picks (a) drop or (b) relax state_eq. Apply the picked path.
• Stage 3 — Tier-0 axiom discharge. Either rewrite eval as a Fixpoint (Route A — affects every eval-using theorem) or prove each of the 4 axioms by induction (Route B — incremental). The echo-types correspondence appendix lays out the precise blockers.

Each stage is its own PR. Stage 1 is mechanical and high-value (currently CI can't even build this tree on 8.18). Stage 2 is a 30-minute decision + 1h application. Stage 3 is the real proof work.

Sub-issue of #124. PRs Refs hyperpolymath/standards#124. Joint-close only on explicit agreement.

🤖 Generated with Claude Code