fix(formal): rewrite preservation proof structure for Rocq 9.1.1

Rewrote preservation with generalize dependent + induction + inversion
approach for Rocq 9.1.1 compatibility. The proof structure handles:
- T_Var_Lin/S_Var: machine-checked via env_typed
- Value reductions: match goal attempts to find sub-derivation
- Congruence: match goal attempts to apply IH

Still Admitted — the match goal patterns need interactive Coq to
debug against actual goal shapes. The proof compiles cleanly.

Current tally: 24 Qed, 4 Admitted, 7 internal admits.
All three .v files compile with zero errors on Rocq 9.1.1.

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

Author: hyperpolymath

formal/.Semantics.aux

@@ -1,72 +1,72 @@
-COQAUX1 1ab66994d3a9ac71ebd8cb394998a476 /var/mnt/eclipse/repos/ephapax/formal/Semantics.v
+COQAUX1 aa75ec5f95e6d06fec4d2f1424427fd7 /var/mnt/eclipse/repos/ephapax/formal/Semantics.v
 0 0 VernacProof "tac:no using:no"
-13140 13144 proof_build_time "0.004"
-0 0 val_to_expr_to_val "0.004"
+13140 13144 proof_build_time "0.005"
+0 0 val_to_expr_to_val "0.005"
 13127 13139 context_used ""
 13140 13144 proof_check_time "0.001"
 0 0 VernacProof "tac:no using:no"
-13581 13585 proof_build_time "0.004"
-0 0 val_to_expr_is_value "0.004"
+13581 13585 proof_build_time "0.003"
+0 0 val_to_expr_is_value "0.003"
 13568 13580 context_used ""
 13581 13585 proof_check_time "0.001"
 0 0 VernacProof "tac:no using:no"
-15167 15171 proof_build_time "0.306"
-0 0 canonical_forms_bool "0.306"
+15167 15171 proof_build_time "0.377"
+0 0 canonical_forms_bool "0.377"
 15154 15166 context_used ""
-15167 15171 proof_check_time "0.104"
+15167 15171 proof_check_time "0.118"
 0 0 VernacProof "tac:no using:no"
-15500 15504 proof_build_time "0.321"
-0 0 canonical_forms_fun "0.321"
+15500 15504 proof_build_time "0.330"
+0 0 canonical_forms_fun "0.330"
 15487 15499 context_used ""
-15500 15504 proof_check_time "0.108"
+15500 15504 proof_check_time "0.112"
 0 0 VernacProof "tac:no using:no"
-15839 15843 proof_build_time "0.288"
-0 0 canonical_forms_prod "0.288"
+15839 15843 proof_build_time "0.319"
+0 0 canonical_forms_prod "0.319"
 15826 15838 context_used ""
-15839 15843 proof_check_time "0.133"
+15839 15843 proof_check_time "0.131"
 0 0 VernacProof "tac:no using:no"
-16323 16327 proof_build_time "0.327"
-0 0 canonical_forms_sum "0.327"
+16323 16327 proof_build_time "0.388"
+0 0 canonical_forms_sum "0.388"
 16288 16322 context_used ""
-16323 16327 proof_check_time "0.133"
+16323 16327 proof_check_time "0.153"
 0 0 VernacProof "tac:no using:no"
-16640 16644 proof_build_time "0.279"
-0 0 canonical_forms_string "0.279"
+16640 16644 proof_build_time "0.317"
+0 0 canonical_forms_string "0.317"
 16627 16639 context_used ""
-16640 16644 proof_check_time "0.098"
+16640 16644 proof_check_time "0.109"
 0 0 VernacProof "tac:no using:no"
-17483 17487 proof_build_time "0.016"
-0 0 mem_free_region_correct "0.016"
+17483 17487 proof_build_time "0.018"
+0 0 mem_free_region_correct "0.018"
 17470 17482 context_used ""
 17483 17487 proof_check_time "0.002"
 0 0 VernacProof "tac:no using:no"
-17778 17782 proof_build_time "0.001"
-0 0 mem_alloc_preserves_read "0.001"
+17778 17782 proof_build_time "0.002"
+0 0 mem_alloc_preserves_read "0.002"
 17727 17777 context_used ""
-17778 17782 proof_check_time "0.000"
+17778 17782 proof_check_time "0.001"
 0 0 VernacProof "tac:no using:no"
-18178 18182 proof_build_time "0.242"
-0 0 values_dont_step "0.242"
+18178 18182 proof_build_time "0.259"
+0 0 values_dont_step "0.259"
 17979 18177 context_used ""
-18178 18182 proof_check_time "0.116"
+18178 18182 proof_check_time "0.108"
 0 0 VernacProof "tac:no using:no"
-18755 18759 proof_build_time "0.009"
-0 0 mem_write_preserves_read "0.009"
+18755 18759 proof_build_time "0.012"
+0 0 mem_write_preserves_read "0.012"
 18750 18754 context_used ""
-18755 18759 proof_check_time "0.003"
+18755 18759 proof_check_time "0.004"
 0 0 VernacProof "tac:no using:no"
-18911 18915 proof_build_time "0.002"
-0 0 eregion_not_value "0.002"
+18911 18915 proof_build_time "0.003"
+0 0 eregion_not_value "0.003"
 18895 18910 context_used ""
 18911 18915 proof_check_time "0.002"
 0 0 VernacProof "tac:no using:no"
-19333 19337 proof_build_time "0.015"
-0 0 value_multi_step_refl "0.015"
+19333 19337 proof_build_time "0.019"
+0 0 value_multi_step_refl "0.019"
 19301 19332 context_used ""
-19333 19337 proof_check_time "0.005"
+19333 19337 proof_check_time "0.007"
 0 0 VernacProof "tac:no using:no"
-19659 19663 proof_build_time "0.004"
-0 0 mem_free_region_length "0.004"
+19659 19663 proof_build_time "0.005"
+0 0 mem_free_region_length "0.005"
 19649 19658 context_used ""
 19659 19663 proof_check_time "0.001"
 0 0 VernacProof "tac:no using:no"
@@ -75,18 +75,18 @@ COQAUX1 1ab66994d3a9ac71ebd8cb394998a476 /var/mnt/eclipse/repos/ephapax/formal/S
 19822 19834 context_used ""
 19835 19839 proof_check_time "0.000"
 0 0 VernacProof "tac:no using:no"
-20908 20912 proof_build_time "0.021"
-0 0 ctx_lookup_mark_used "0.021"
+20908 20912 proof_build_time "0.026"
+0 0 ctx_lookup_mark_used "0.026"
 20897 20907 context_used ""
-20908 20912 proof_check_time "0.003"
+20908 20912 proof_check_time "0.004"
 0 0 VernacProof "tac:no using:no"
 21266 21270 proof_build_time "0.001"
 0 0 env_consistent_mark_used "0.001"
 21242 21265 context_used ""
 21266 21270 proof_check_time "0.000"
 0 0 VernacProof "tac:no using:no"
-21862 21866 proof_build_time "0.001"
-0 0 env_consistent_weaken "0.001"
+21862 21866 proof_build_time "0.002"
+0 0 env_consistent_weaken "0.002"
 21832 21861 context_used ""
 21862 21866 proof_check_time "0.001"
 0 0 VernacProof "tac:no using:no"
@@ -100,29 +100,39 @@ COQAUX1 1ab66994d3a9ac71ebd8cb394998a476 /var/mnt/eclipse/repos/ephapax/formal/S
 22641 22655 context_used ""
 22656 22660 proof_check_time "0.001"
 0 0 VernacProof "tac:no using:no"
-29443 29452 proof_build_time "0.040"
-0 0 typing_preserves_domain "0.040"
+29443 29452 proof_build_time "0.046"
+0 0 typing_preserves_domain "0.046"
 29443 29452 proof_check_time "0.000"
 0 0 VernacProof "tac:no using:no"
-30537 30541 proof_build_time "0.052"
-0 0 step_eregion_cases "0.052"
+30537 30541 proof_build_time "0.055"
+0 0 step_eregion_cases "0.055"
 30524 30536 context_used ""
-30537 30541 proof_check_time "0.041"
+30537 30541 proof_check_time "0.040"
 0 0 VernacProof "tac:no using:no"
-31861 31865 proof_build_time "0.020"
-0 0 region_exit_mem_free "0.020"
+31861 31865 proof_build_time "0.019"
+0 0 region_exit_mem_free "0.019"
 31848 31860 context_used ""
-31861 31865 proof_check_time "0.010"
+31861 31865 proof_check_time "0.009"
 0 0 VernacProof "tac:no using:no"
 32719 32723 proof_build_time "0.002"
 0 0 no_leaks "0.002"
 32680 32718 context_used ""
 32719 32723 proof_check_time "0.001"
 0 0 VernacProof "tac:no using:no"
-34060 34064 proof_build_time "0.005"
-0 0 expr_to_val_locs_valid "0.005"
+34060 34064 proof_build_time "0.006"
+0 0 expr_to_val_locs_valid "0.006"
 34046 34059 context_used ""
-34060 34064 proof_check_time "0.001"
+34060 34064 proof_check_time "0.002"
 0 0 VernacProof "tac:no using:no"
-37516 37520 proof_build_time "0.751"
-0 0 memory_safety "0.751"
+37516 37525 proof_build_time "0.864"
+0 0 memory_safety "0.864"
+37516 37525 proof_check_time "0.000"
+0 0 VernacProof "tac:no using:no"
+45980 45989 proof_build_time "0.704"
+0 0 progress "0.704"
+45980 45989 proof_check_time "0.000"
+0 0 VernacProof "tac:no using:no"
+50327 50336 proof_build_time "1.118"
+0 0 preservation "1.118"
+50327 50336 proof_check_time "0.000"
+0 0 vo_compile_time "6.675"

formal/Semantics.v

@@ -1217,24 +1217,61 @@ Theorem preservation :
     exists G'' G_out, R; G'' |- e' : T -| G_out.
 Proof.
   intros R G e T G' mu rho mu' rho' e' Htype Hstep Henv.
-  (* By induction on the typing derivation, inverting the step for
-     each expression form *)
-  induction Htype; inversion Hstep; subst.
+  (* Induction on typing, inversion on step.
+     The weakened statement (exists G'' G_out) makes most cases straightforward:
+     - Value reductions: the result is typed by a sub-derivation
+     - Congruence: IH gives typed sub-result, reconstruct outer rule
+     We use generalize dependent to handle Rocq 9.1.1 variable renaming. *)
+  generalize dependent e'.
+  generalize dependent rho'.
+  generalize dependent mu'.
+  generalize dependent mu.
+  generalize dependent rho.
+  induction Htype; intros rho Henv mu mu' rho' e' Hstep;
+    inversion Hstep; subst.
 
-  (* All preservation cases — use match goal for Rocq 9.1.1 compatibility *)
   (* T_Var_Lin, S_Var *)
-  - destruct (Henv x T false H eq_refl) as [v' [Hlookup' Htyped]].
+  - destruct (Henv x T false H eq_refl) as [v' [Hlk Hty]].
     match goal with
-    | [ Hlk : env_lookup _ _ = Some ?V |- _ ] =>
-        rewrite Hlk in Hlookup'; injection Hlookup'; intros; subst;
-        exists G, G; apply Htyped
+    | [ Heq : env_lookup _ _ = Some _ |- _ ] =>
+        rewrite Heq in Hlk; injection Hlk; intros; subst;
+        exists G, G; apply Hty
     end.
 
-  (* T_Var_Unr, S_Var *)
-  - admit. (* needs env_typed to cover unrestricted used vars *)
+  (* T_Var_Unr, S_Var — env_typed only covers u=false, but u could be true.
+     For unrestricted types, the variable may be reused. We need env_typed
+     to also cover used unrestricted variables. Deferred. *)
+  - admit.
 
-  (* All remaining cases *)
-  all: admit. (* remaining cases need IH threading + context reconstruction *)
+  (* For all remaining cases, the key patterns are:
+     1. Sub-expression typing directly gives the result (value reductions)
+     2. IH on sub-step + reconstruct outer typing rule (congruence)
+     3. Region changes (deferred — requires region weakening)
+
+     We handle the value reduction cases first, then try IH for congruence. *)
+
+  (* Value reduction cases: the result is already typed by a sub-derivation *)
+  (* T_Let, S_Let_Val: result is e2, typed by Htype2 *)
+  all: try (match goal with
+    | [ Hty2 : _; ctx_extend ?G' ?X ?T1 |- ?E2 : ?T2 -| _ |- _ ] =>
+        exists (ctx_extend G' X T1), _; exact Hty2
+    end).
+
+  (* T_If, S_If_True/False: result is e2 or e3, typed directly *)
+  all: try (match goal with
+    | [ Hty : _; ?G |- ?E : ?T -| ?G' |- context[?E] ] =>
+        exists G, G'; exact Hty
+    end).
+
+  (* Congruence: IH gives sub-result, reconstruct *)
+  all: try (match goal with
+    | [ IH : forall _ _, env_typed _ _ _ -> forall _ _ _ _, _ -> exists _ _, _ |- _ ] =>
+        edestruct IH as [?G'' [?Gout ?Hty']]; try eassumption;
+        eexists _, _; econstructor; eassumption
+    end).
+
+  (* Anything remaining *)
+  all: admit.
 Admitted.
 (* DUST NOTE: Preservation proof outline is complete for the key cases:
    - S_Var: uses env_typed to get well-typed val_to_expr ✓