fix(coq/cno): Stage 1 - Coq 8.18 build repair, nop_is_cno Admitted

Three systemic blockers in CNO.v under Coq 8.18 are fixed in this commit;
the file now compiles cleanly with one Admitted (nop_is_cno) and four
Axioms unchanged. Theorem statements are preserved.

Fixes:

1. Auto-naming clobber: extract eval_nil_inv + eval_cons_inv helpers so
   eval_app no longer relies on the fragile [H3] identifier produced by
   [inversion ...; subst.]. Both directions of eval_app rewritten to use
   the helpers; the <- direction's intros pattern is also fixed
   ([intros s sm Hp1 s' Hp2] instead of the wrong-order
   [intros s sm s' Hp1 Hp2]).

2. [repeat split.] + bullets fails 8.18 name hygiene at every site that
   the prior file used it inside a multi-goal proof body. Restructured
   eval_app, state_eq_refl, state_eq_trans, state_eq_sym, cno_composition,
   empty_is_cno, and cno_eval_on_equal_states to use [split. { ... }]
   blocks. The { } blocks reset the name table; bullets do not.

3. cno_equiv_sym used the generic [symmetry.] tactic for =st=, which 8.18
   rejects because state_eq is not a declared symmetric relation.
   Moved the theorem after state_eq_sym is defined and replaced
   [symmetry.] with [apply state_eq_sym.] + an explicit
   [apply H with (s := s)] to unify the universally-quantified [s].

4. cno_eval_on_equal_states: original [exists s'.] left a goal that
   eval_respects_state_eq_left could not discharge. Fixed to
   [exists sx.] so the axiom unifies (theorem statement unchanged).

5. nop_is_cno: theorem statement preserved, proof body replaced with
   Admitted. The Identity clause is unprovable under the strict 4-clause
   state_eq because Nop increments state_pc. Stage 2 relaxes state_eq
   (per owner ruling on standards#157) and discharges this Admitted.

Verification: coqc -R common CNO common/CNO.v exits 0.

Refs hyperpolymath/standards#124
Refs hyperpolymath/standards#157

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/coq/common/CNO.v

@@ -246,6 +246,31 @@ Qed.
 (** Sequential composition of programs *)
 Definition seq_comp (p1 p2 : Program) : Program := p1 ++ p2.
 
+(** Inversion helpers for the eval relation.
+
+    Coq 8.18's [inversion ...; subst.] tactic auto-names hypotheses
+    differently from older versions, which breaks proofs that referenced
+    fragile names like [H3]. Extracting these helpers gives us stable,
+    name-free destructuring. *)
+
+Lemma eval_nil_inv :
+  forall s s', eval [] s s' -> s = s'.
+Proof.
+  intros s s' H.
+  inversion H.
+  reflexivity.
+Qed.
+
+Lemma eval_cons_inv :
+  forall i is s s',
+    eval (i :: is) s s' ->
+    exists s2, step s i s2 /\ eval is s2 s'.
+Proof.
+  intros i is s s' H.
+  inversion H; subst.
+  eexists. split; eassumption.
+Qed.
+
 (** Key lemma: evaluation of concatenated programs *)
 Lemma eval_app :
   forall p1 p2 s s',
@@ -267,37 +292,44 @@ Proof.
       * assumption.   (* H : eval p2 s s' *)
     + (* p1 = i :: p1' *)
       simpl in H.
-      inversion H; subst.
-      apply IH in H3.
-      destruct H3 as [sm [H3a H3b]].
+      apply eval_cons_inv in H.
+      destruct H as [s2 [Hstep Hrest]].
+      apply IH in Hrest.
+      destruct Hrest as [sm [Hsm_p1 Hsm_p2]].
       exists sm.
       split; try assumption.
       eapply eval_step; eassumption.
   - (* <- direction *)
-    intros [sm [H1 H2]].
+    intros [sm [Hp1 Hp2]].
     generalize dependent s'.
     generalize dependent sm.
     generalize dependent s.
-    induction p1 as [| i p1' IH]; intros s sm s' H1 H2.
+    induction p1 as [| i p1' IH]; intros s sm Hp1 s' Hp2.
     + (* p1 = [] *)
       simpl.
-      inversion H1; subst.
+      apply eval_nil_inv in Hp1. subst.
       assumption.
     + (* p1 = i :: p1' *)
       simpl.
-      inversion H1; subst.
+      apply eval_cons_inv in Hp1.
+      destruct Hp1 as [s2 [Hstep Hrest]].
       eapply eval_step.
       * eassumption.
-      * apply IH; eassumption.
+      * eapply IH; eassumption.
 Qed.
 
 (** State equality is reflexive *)
 Lemma state_eq_refl : forall s, s =st= s.
 Proof.
   intros s.
-  unfold state_eq.
-  repeat split; try reflexivity.
-  unfold mem_eq. reflexivity.
+  unfold state_eq, mem_eq.
+  split.
+  { intros addr. reflexivity. }
+  split.
+  { reflexivity. }
+  split.
+  { reflexivity. }
+  reflexivity.
 Qed.
 
 (** State equality is transitive *)
@@ -306,17 +338,22 @@ Lemma state_eq_trans :
 Proof.
   intros s1 s2 s3 [Hm1 [Hr1 [Hi1 Hp1]]] [Hm2 [Hr2 [Hi2 Hp2]]].
   unfold state_eq.
-  repeat split.
-  - (* Memory *)
+  split.
+  { (* Memory *)
     unfold mem_eq in *.
     intros addr.
     transitivity (s2.(state_memory) addr); auto.
-  - (* Registers *)
+  }
+  split.
+  { (* Registers *)
     transitivity (s2.(state_registers)); auto.
-  - (* I/O *)
+  }
+  split.
+  { (* I/O *)
     transitivity (s2.(state_io)); auto.
-  - (* PC *)
-    transitivity (s2.(state_pc)); auto.
+  }
+  (* PC *)
+  transitivity (s2.(state_pc)); auto.
 Qed.
 
 (** Purity is transitive *)
@@ -342,8 +379,8 @@ Proof.
   unfold is_CNO in *.
   destruct H1 as [T1 [I1 [P1 R1]]].
   destruct H2 as [T2 [I2 [P2 R2]]].
-  repeat split.
-  - (* Termination *)
+  split.
+  { (* Termination *)
     intros s.
     unfold terminates in *.
     destruct (T1 s) as [s1 E1].
@@ -353,7 +390,9 @@ Proof.
     apply eval_app.
     exists s1.
     split; assumption.
-  - (* Identity *)
+  }
+  split.
+  { (* Identity *)
     intros s s' Heval.
     unfold seq_comp in Heval.
     apply eval_app in Heval.
@@ -363,18 +402,21 @@ Proof.
     apply I1 in E1.
     apply I2 in E2.
     eapply state_eq_trans; eassumption.
-  - (* Purity *)
+  }
+  split.
+  { (* Purity *)
     intros s s' Heval.
     unfold seq_comp in Heval.
     apply eval_app in Heval.
     destruct Heval as [sm [E1 E2]].
     apply P1 in E1.
     apply P2 in E2.
     eapply pure_trans; eassumption.
-  - (* Thermodynamic reversibility *)
-    unfold thermodynamically_reversible, energy_dissipated in *.
-    intros s1 s2 Heval.
-    reflexivity.
+  }
+  (* Thermodynamic reversibility *)
+  unfold thermodynamically_reversible, energy_dissipated in *.
+  intros s1 s2 Heval.
+  reflexivity.
 Qed.
 
 (** ** The Simplest CNO: Empty Program *)
@@ -383,61 +425,45 @@ Qed.
 Theorem empty_is_cno : is_CNO [].
 Proof.
   unfold is_CNO.
-  repeat split.
-  - (* Termination *)
+  split.
+  { (* Termination *)
     intros s.
     exists s.
     constructor.
-  - (* Identity *)
+  }
+  split.
+  { (* Identity *)
     intros s s' Heval.
-    inversion Heval; subst.
-    unfold state_eq.
-    repeat split; try reflexivity.
-    unfold mem_eq. reflexivity.
-  - (* Purity *)
+    apply eval_nil_inv in Heval. subst.
+    apply state_eq_refl.
+  }
+  split.
+  { (* Purity *)
     intros s s' Heval.
-    inversion Heval; subst.
-    unfold pure, no_io, no_memory_alloc.
-    split; try reflexivity.
-    unfold mem_eq. reflexivity.
-  - (* Thermodynamic reversibility *)
-    unfold thermodynamically_reversible.
-    intros s1 s2 Heval.
-    reflexivity.
+    apply eval_nil_inv in Heval. subst.
+    unfold pure, no_io, no_memory_alloc, mem_eq.
+    split.
+    { reflexivity. }
+    intros addr. reflexivity.
+  }
+  (* Thermodynamic reversibility *)
+  unfold thermodynamically_reversible.
+  intros s1 s2 Heval.
+  reflexivity.
 Qed.
 
 (** ** The Canonical CNO: Single Nop *)
 
-(** A single Nop instruction is a CNO *)
+(** A single Nop instruction is a CNO.
+
+    Under the strict 4-clause [state_eq] (with pc-equality) this theorem
+    is FALSE: Nop increments the program counter, so the post-state
+    differs from the pre-state on the [state_pc] field. The proof is
+    discharged in Stage 2 once [state_eq] is relaxed to ignore [state_pc].
+    See [hyperpolymath/standards#157] Stage 2. *)
 Theorem nop_is_cno : is_CNO [Nop].
 Proof.
-  unfold is_CNO.
-  repeat split.
-  - (* Termination *)
-    intros s.
-    exists (mkState s.(state_memory) s.(state_registers) s.(state_io) (S s.(state_pc))).
-    apply eval_step with (s2 := mkState s.(state_memory) s.(state_registers) s.(state_io) (S s.(state_pc))).
-    + constructor.
-    + constructor.
-  - (* Identity - modulo PC increment *)
-    intros s s' Heval.
-    inversion Heval; subst.
-    inversion H; subst.
-    inversion H0; subst.
-    unfold state_eq.
-    repeat split; try reflexivity.
-    unfold mem_eq. reflexivity.
-  - (* Purity *)
-    intros s s' Heval.
-    inversion Heval; subst.
-    inversion H; subst.
-    unfold pure, no_io, no_memory_alloc.
-    split; reflexivity.
-  - (* Thermodynamic reversibility *)
-    unfold thermodynamically_reversible.
-    intros s1 s2 Heval.
-    reflexivity.
-Qed.
+Admitted.
 
 (** ** CNO Equivalence *)
 
@@ -465,21 +491,26 @@ Proof.
   apply eval_deterministic with (p := p) (s := s); assumption.
 Qed.
 
-Theorem cno_equiv_sym : forall p1 p2, cno_equiv p1 p2 -> cno_equiv p2 p1.
-Proof.
-  unfold cno_equiv.
-  intros p1 p2 H s s1 s2 H1 H2.
-  symmetry.
-  apply H; assumption.
-Qed.
-
 (** State equality is symmetric *)
 Lemma state_eq_sym : forall s1 s2, s1 =st= s2 -> s2 =st= s1.
 Proof.
   intros s1 s2 [Hm [Hr [Hi Hp]]].
   unfold state_eq, mem_eq in *.
-  repeat split; auto.
-  intros addr. symmetry. apply Hm.
+  split.
+  { intros addr. symmetry. apply Hm. }
+  split.
+  { symmetry. assumption. }
+  split.
+  { symmetry. assumption. }
+  symmetry. assumption.
+Qed.
+
+Theorem cno_equiv_sym : forall p1 p2, cno_equiv p1 p2 -> cno_equiv p2 p1.
+Proof.
+  unfold cno_equiv.
+  intros p1 p2 H s s1 s2 H1 H2.
+  apply state_eq_sym.
+  apply H with (s := s); assumption.
 Qed.
 
 Theorem cno_equiv_trans :
@@ -612,16 +643,18 @@ Lemma cno_eval_on_equal_states :
     (exists s1, eval p s s1) <-> (exists s2, eval p s' s2).
 Proof.
   intros p s s' H_cno H_eq.
-  split; intros [sx H_eval].
-  - (* Forward direction *)
-    exists s'.
-    eapply eval_respects_state_eq_left.
-    + eassumption.
-    + assumption.
-  - (* Backward direction *)
-    exists s.
-    eapply eval_respects_state_eq_left.
-    + eassumption.
-    + apply state_eq_sym. assumption.
+  split.
+  { (* Forward direction *)
+    intros [sx H_eval].
+    exists sx.
+    eapply eval_respects_state_eq_left;
+      [ eassumption | assumption ].
+  }
+  { (* Backward direction *)
+    intros [sx H_eval].
+    exists sx.
+    eapply eval_respects_state_eq_left;
+      [ eassumption | apply state_eq_sym; assumption ].
+  }
 Qed.