From c1aaf6ec0518722f3b107f1e4b2d9af864811ebb Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 15:44:03 +0100 Subject: [PATCH] =?UTF-8?q?feat(L2):=20Phase=20D=20slice=204=20Phase=204b?= =?UTF-8?q?=20=E2=80=94=20preservation=5Fl2=5Fapp=5Feff=5Fbeta=5Fground=5F?= =?UTF-8?q?nonlinear?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Phase 4 continuation following PR #228's Phase 4a (linear T1). Closes the T_App_L2_Eff β-case (S_App_Fun step) for ground-non-linear T1 ∈ { TBase TUnit, TBase TBool, TBase TI32 } via Phase 2's subst_typing_gen_l1_m_ground_nonlinear (PR #220). Two lemmas, mirroring #228's Linear pattern: - preservation_l2_app_eff_beta_ground_nonlinear_l1 — L1-level kernel. Inversion on the lambda forces T_Lam_L1_*_Eff (TFun cases discriminate); value_R_G_preserving_l1 on the argument collapses R_in/G'' to R/G. The Linear case discharges the |=L1 (Linear) Hv_type premise directly with Harg; the Affine case bridges via ground_nonlinear_retype_l1_m (cross-modality, same R) since Phase 2's Hv_type premise uses the Linear-only |=L1 shorthand. - preservation_l2_app_eff_beta_ground_nonlinear — L2 wrapper. Inverts both has_type_l2 hypotheses through L2_lift_l1 (T_App_L2_Eff discriminates: lambda's head is ELam not EApp; argument is a value). Defers to the L1 kernel and re-lifts via L2_lift_l1. Combined with PR #228's Phase 4a, this closes T_App_L2_Eff β for T1 ∈ { linear, ground-non-linear }. Phase 4c (TFunEff T1) remains blocked on Phase 3b (ephapax issue #225). Phase 4d (compound) remains deferred to Phase 5. Build + assumption audit: - coqc 8.18 / Rocq 9.1.1 clean rebuild across all 10 .v files. - Print Assumptions preservation_l2_app_eff_beta_ground_nonlinear shows only pre-existing axioms inherited transitively via subst_typing_gen_l1_m_ground_nonlinear (which Print Assumptions shows is closed under the global context per PR #220's audit). No new admits, no new axioms. Owner-directive compliance (CLAUDE.md 2026-05-27): - Does NOT close Theorem preservation in formal/Semantics.v. - Does NOT extend Semantics.v / Typing.v / Counterexample.v. - Does NOT close any residual Semantics_L1.v admit. - Works per-layer: L1 kernel + L2 wrapper, both at the post-redesign m-indexed has_type_l1 judgment. - Reads PRESERVATION-DESIGN.md / SUBST-LEMMA-GENERALIZATION-DESIGN.md. - No new Axiom or Admitted markers. Refs: - PR #220 — Phase 2 (subst_typing_gen_l1_m_ground_nonlinear) - PR #228 — Phase 4a (linear T1 sibling) - ephapax#225 — Phase 4c gating issue - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 4 - formal/PRESERVATION-DESIGN.md §5.1 Co-Authored-By: Claude Opus 4.7 (1M context) --- formal/TypingL2.v | 83 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/formal/TypingL2.v b/formal/TypingL2.v index 8c578bc..5c5250c 100644 --- a/formal/TypingL2.v +++ b/formal/TypingL2.v @@ -491,3 +491,86 @@ Proof. into the Type-sorted has_type_l2 goal is allowed. *) exfalso. inversion Hval. Qed. + +(** Phase D slice 4 Phase 4b — preservation_l2 β-case closure for + ground-non-linear T1. + + Mirrors [preservation_l2_app_eff_beta_linear] (PR #228) but uses + Phase 2's [Semantics_L1.subst_typing_gen_l1_m_ground_nonlinear] + for the L1 substitution step. Covers T1 ∈ { TBase TUnit, + TBase TBool, TBase TI32 } — ground values whose typing is + R-irrelevant and modality-polymorphic, so they bridge across the + Linear-only [|=L1] premise of the Phase 2 lemma via + [ground_nonlinear_retype_l1_m] (Phase 1). + + Combined with PR #228's [preservation_l2_app_eff_beta_linear], + this closes the [T_App_L2_Eff] β-case for T1 ∈ { linear, + ground-non-linear }. Phase 4c (TFunEff T1) and Phase 4d + (compound non-linear) remain open — see issue #225 / Phase 5 + respectively. + + Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 4, + [PRESERVATION-DESIGN.md §5.1]. *) + +Lemma preservation_l2_app_eff_beta_ground_nonlinear_l1 : + forall m R R1 G G' G'' v2 T1 T2 R_in R_out ebody, + is_value v2 -> + is_ground_nonlinear_ty T1 = true -> + TypingL1.has_type_l1 m R G (ELam T1 ebody) + (TFunEff T1 T2 R_in R_out) R1 G' -> + TypingL1.has_type_l1 m R1 G' v2 T1 R_in G'' -> + TypingL1.has_type_l1 m R G (subst 0 v2 ebody) T2 R_out G''. +Proof. + intros m R R1 G G' G'' v2 T1 T2 R_in R_out ebody Hval Hgrd Hlam Harg. + inversion Hlam; subst. + - (* T_Lam_L1_Linear_Eff: m = Linear; body at R_in / (T1,false)::G'' → + R_out / (T1,true)::G''. Harg : has_type_l1 Linear R G v2 T1 R G + (after value_R_G_preserving_l1). Matches Phase 2's [|=L1] + premise directly. *) + destruct (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hval Harg) as [<- <-]. + eapply subst_typing_gen_l1_m_ground_nonlinear with + (k := 0) (u_in := false) + (Gin := (T1, false) :: G'') + (Gout := (T1, true) :: G''). + + unfold ctx_extend in *. eassumption. + + reflexivity. + + exact Hval. + + exact Hgrd. + + exact Harg. + + reflexivity. + - (* T_Lam_L1_Affine_Eff: m = Affine; bridge Harg (Affine) to Linear + via [ground_nonlinear_retype_l1_m] (cross-modality at same R). *) + destruct (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hval Harg) as [<- <-]. + eapply subst_typing_gen_l1_m_ground_nonlinear with + (k := 0) (u_in := false) + (Gin := (T1, false) :: G'') + (Gout := (T1, _) :: G''). + + unfold ctx_extend in *. eassumption. + + reflexivity. + + exact Hval. + + exact Hgrd. + + eapply ground_nonlinear_retype_l1_m; + [exact Hval | exact Hgrd | exact Harg]. + + reflexivity. +Qed. + +Lemma preservation_l2_app_eff_beta_ground_nonlinear : + forall m R R1 G G' G'' v2 T1 T2 R_in R_out ebody, + is_value v2 -> + is_ground_nonlinear_ty T1 = true -> + has_type_l2 m R G (ELam T1 ebody) + (TFunEff T1 T2 R_in R_out) R1 G' -> + has_type_l2 m R1 G' v2 T1 R_in G'' -> + has_type_l2 m R G (subst 0 v2 ebody) T2 R_out G''. +Proof. + intros m R R1 G G' G'' v2 T1 T2 R_in R_out ebody Hval Hgrd Hlam Harg. + (* Lambda inversion: only [L2_lift_l1] survives ([T_App_L2_Eff]'s + expression is [EApp _ _], not [ELam _ _]). *) + inversion Hlam as [m0 R0 G0 e0 T0 R0' G0' Hlam_l1 | ]; subst. + (* Argument inversion: [v2] is a value, so the [T_App_L2_Eff] case + would force [v2 = EApp _ _], contradicting [Hval]. *) + inversion Harg as [m0' R0'' G0'' e0' T0' R0''' G0''' Harg_l1 | ]; subst. + - apply L2_lift_l1. + eapply preservation_l2_app_eff_beta_ground_nonlinear_l1; eassumption. + - exfalso. inversion Hval. +Qed.