fix: make Semantics.v compile with Rocq 9.1.1 (-R . "")

The file was broken by Rocq 9.1.1 auto-naming changes (H5→different
names from inversion). Fixed the typing_types_agree proof to use
match-goal patterns instead of fragile auto-generated names.

Also restructured no_consumption_at_true_linear to use automated
tactic dispatch for compound cases via typing_preserves_types_agree
and flags_monotone.

Status: 28 Qed, 4 Admitted (unchanged count).
The 4 Admitted are:
  1. no_consumption_at_true_linear — compound/binding cases
  2. typing_ctx_transfer — T_Case/T_If + consumption tracking
  3. subst_preserves_typing — binding cases at depth k
  4. preservation — depends on #2 and #3

Root cause of remaining admits: compound cases need IH threading
through intermediate contexts, but induction-generated IH names
are fragile across Rocq versions. Proper fix: refactor all
induction calls to use explicit `as [IH1 IH2]` naming.

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

Author: hyperpolymath

formal/Semantics.v

@@ -903,15 +903,35 @@ Proof.
   (* T_Loc *) - inversion H2; subst. exact HiG2.
   (* T_StringNew *) - inversion H2; subst. exact HiG2.
 
-  (* T_StringConcat *)
-  - inversion H2; subst. admit. (* compound chain — needs correct IH names *)
-
-  (* Remaining compound/binding cases: same pattern — inversion on H2,
-     thread IH through sub-derivations with typing_preserves_types_agree
-     and flags_monotone. Admit for now — correct structure shown in
-     T_StringConcat above, just needs correct IH names from induction. *)
-  all: try (inversion H2; subst; admit).
+  (* Remaining compound/binding cases: thread IH through sub-derivations.
+     The pattern is: inversion H2 gives sub-typing derivations that
+     match the IHs from induction on H1. For each sub-derivation,
+     the IH gives us the false-preservation at position i. *)
+
+  (* Generic tactic: for compound cases, inversion on H2 and use available IHs *)
   all: try (inversion H2; subst; exact HiG2).
+  all: try (inversion H2; subst;
+    match goal with
+    | [ IH : forall _ _, ctx_types_agree _ _ -> _ -> _ -> _ ; _ |- _ : _ -| _ -> _
+        |- ctx_lookup _ _ = Some (_, false) ] =>
+        eapply IH; try eassumption;
+        try (eapply typing_preserves_types_agree; eassumption);
+        try (eapply flags_monotone; eassumption)
+    end).
+  (* Remaining cases: try threading IH1 through IH2 for chain types *)
+  all: try (inversion H2; subst;
+    match goal with
+    | [ IH1 : forall _ _, ctx_types_agree _ _ -> _ -> _ -> _ ; _ |- _ : _ -| _ -> _,
+        IH2 : forall _ _, ctx_types_agree _ _ -> _ -> _ -> _ ; _ |- _ : _ -| _ -> _,
+        Htyp_sub : _ ; _ |- _ : _ -| ?Gmid |- _ ] =>
+        eapply IH1; try eassumption;
+        try (eapply typing_preserves_types_agree; eassumption);
+        try (eapply flags_monotone; eassumption);
+        try (eapply IH2; try eassumption;
+             try (eapply typing_preserves_types_agree; eassumption);
+             try (eapply flags_monotone; eassumption))
+    end).
+  all: try (inversion H2; subst; eauto using typing_preserves_types_agree, flags_monotone).
   all: admit.
 Admitted.