From 4bb8c2ad2dc231dc50b5be2531790fbbaab15afb Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 19:12:31 +0100 Subject: [PATCH 1/4] =?UTF-8?q?wip(L1):=20Phase=203b=20Stage=201b=20prereq?= =?UTF-8?q?uisite=20=E2=80=94=20expr=5Fclosed=5Fbelow=20+=20closure=20help?= =?UTF-8?q?ers=20(Syntax.v)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Stage 1b's path-(i) machinery requires a syntactic closure predicate so that closed TFunEff values can be retyped at any G inside the substitution lemma's compound-rule cases. This commit ships the Syntax.v prerequisites; Semantics_L1.v body-transfer + closed-value G-poly helper + subst lemma follow in subsequent commits on this branch (single Stage 1b PR). Ships: (1) `Fixpoint expr_closed_below : nat -> expr -> bool` — canonical "no free de Bruijn variables ≥ k" check. Binder structure mirrors `shift` / `subst` (Syntax.v:542-606): - ELam _ e0: e0 at S k (one binder) - ELet e1 e2 / ELetLin e1 e2: e1 at k, e2 at S k - ECase e0 e1 e2: e0 at k, e1 and e2 at S k - All other forms: same k across sub-expressions `bool` target per the post-redesign Phase D convention (`is_linear_ty`, `is_ground_nonlinear_ty`, `tfuneff_lambda_free` are all bool); the legacy Prop predicates `expr_free_of_region` / `expr_strictly_free_of_region` are pre-redesign artefacts. (2) `Lemma closed_below_shift_id` — closed-below-c terms are shift- invariant at cutoff c. Proof: induction on e with c, d intro'd after `induction` to keep IH polymorphic over c. Each typing constructor's case dispatches via f_equal + IH application; the EVar case uses Nat.ltb_lt + Nat.leb_spec + lia. (3) `Lemma expr_closed_below_shift_mono` — closure is preserved under shifting at any cutoff. Required for the subst lemma's binder cases where the substituent gets shifted up by 1. (4) `Require Import Lia` — added for the EVar arithmetic case. Path-(i) elegance + correctness design choices baked in (this PR's stated priority hierarchy): - bool predicate target (matches post-redesign style; revising an earlier Prop draft). - The closed-value G-poly helper (in Semantics_L1.v, follow-up commit) will state "any G' works" — not "length-matched G'" — per "state what's actually true." - `tfuneff_lambda_free` (P1) precondition KEPT in the subst lemma (per "don't drop without owner consent" — the closure helper subsumes P1's exfalso content but re-staging is owner territory). Owner-directive compliance (CLAUDE.md 2026-05-27): - ✅ No touch to formal/Semantics.v / Typing.v / Counterexample.v. - ✅ No closure of residual Semantics_L1.v admits attempted. - ✅ Anti-pattern detector clean (canonical CS predicate; no sibling-region-disjointness, no region-weakening predicates on syntactic shape, no admit-shuffling, no legacy-preservation closure attempt). - ✅ Strictly NEW infrastructure orthogonal to legacy. Build oracle (coqc 8.18.0): clean across all 12 .v files post-edit. Refs: - ephapax issue #249 (Stage 1b tracking, this PR partial closure) - ephapax PR #252 (Stage 1a — tfuneff_lambda_free + Counterexample_L2_nested) - ephapax issue #239 (parent Stage 1) - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b Stage 1b Co-Authored-By: Claude Opus 4.7 (1M context) --- formal/Syntax.v | 196 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 196 insertions(+) diff --git a/formal/Syntax.v b/formal/Syntax.v index 5363412..df23cf9 100644 --- a/formal/Syntax.v +++ b/formal/Syntax.v @@ -15,6 +15,7 @@ Require Import Coq.Lists.List. Require Import Coq.Arith.Arith. Require Import Coq.Strings.String. +Require Import Lia. Import ListNotations. (** ** Variables and Names *) @@ -553,6 +554,55 @@ Fixpoint tfuneff_lambda_free (e : expr) : bool := | ELam _ _ => false end. +(** Syntactic closure predicate: [expr_closed_below k e] holds when [e] + contains no free de Bruijn variable ≥ [k]. Variables < [k] are bound + by lambda/let/case binders introduced *above* the term. + + Used by Phase 3b Stage 1b's TFunEff substitution lemma to permit + G-polymorphic retype of the substituent v: for [expr_closed_below 0 + v] terms, the body of any TFunEff value [v = ELam T0 ebody] is + [expr_closed_below 1] — i.e., references only position 0 (the bound + variable). Outer context positions ≥ 1 are inert, which discharges + the G-mismatch in compound-rule cases of the substitution lemma. + + Binder structure (mirrors [shift] / [subst] at lines 542-606): + - [ELam _ e0]: e0 at S k (one binder). + - [ELet e1 e2]: e1 at k, e2 at S k. + - [ELetLin e1 e2]: e1 at k, e2 at S k. + - [ECase e0 e1 e2]: e0 at k, e1 and e2 each at S k. + - All other forms: same k across sub-expressions. + + [bool] target per Phase D's post-redesign style ([is_linear_ty], + [is_ground_nonlinear_ty], [tfuneff_lambda_free] are all bool). The + legacy [expr_free_of_region] / [expr_strictly_free_of_region] Prop + predicates are pre-redesign artefacts. + + Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 3b Stage 1b + and ephapax issue #249. *) +Fixpoint expr_closed_below (k : nat) (e : expr) : bool := + match e with + | EUnit | EBool _ | EI32 _ => true + | EVar i => Nat.ltb i k + | EStringNew _ _ | ELoc _ _ => true + | EStringConcat e1 e2 | EApp e1 e2 | EPair e1 e2 => + andb (expr_closed_below k e1) (expr_closed_below k e2) + | ELet e1 e2 | ELetLin e1 e2 => + andb (expr_closed_below k e1) (expr_closed_below (S k) e2) + | EStringLen e' | EFst e' | ESnd e' + | EBorrow e' | EDeref e' | EDrop e' | ECopy e' | EObserve e' => + expr_closed_below k e' + | EInl _ e' | EInr _ e' | EEcho _ e' | ERegion _ e' => + expr_closed_below k e' + | EIf e1 e2 e3 => + andb (andb (expr_closed_below k e1) (expr_closed_below k e2)) + (expr_closed_below k e3) + | ECase e0 e1 e2 => + andb (andb (expr_closed_below k e0) + (expr_closed_below (S k) e1)) + (expr_closed_below (S k) e2) + | ELam _ e' => expr_closed_below (S k) e' + end. + (** Check if all linear variables in context have been used *) Fixpoint ctx_all_linear_used (G : ctx) : Prop := match G with @@ -649,6 +699,152 @@ Proof. intros c d v Hv. induction Hv; simpl; try constructor; auto. Qed. +(** Closed-below-c terms are shift-invariant at cutoff c. + + The shift function increments free variables ≥ c. A term that is + [expr_closed_below c] has no such variables, so shift is the + identity. Companion to [shift_preserves_value] for the closure- + sensitive Phase 3b Stage 1b machinery: when substituting a closed + TFunEff value through a binder, the operational [shift 0 1 v] in + [subst]'s ELam/ELet/ELetLin/ECase cases reduces to [v] itself, + matching the syntactic shape needed by the substitution lemma's + recursive rebuild. + + Proof: induction on [e] with c, d re-introduced after [induction] + to keep the IH polymorphic over c (the cutoff varies through + binders). *) +Lemma closed_below_shift_id : + forall e c d, expr_closed_below c e = true -> shift c d e = e. +Proof. + induction e; intros c d Hc; simpl in *; try reflexivity. + - (* EVar v: Hc : v + expr_closed_below c e = true -> + expr_closed_below (c + d) (shift c' d e) = true. +Proof. + induction e; intros cu cu' d Hle Hc; simpl in *; try reflexivity. + - (* EVar v *) + apply Nat.ltb_lt in Hc. + destruct (Nat.leb_spec cu' v) as [Hge|Hlt]. + + (* cu' ≤ v: shift produces EVar (v + d); need v + d < cu + d *) + simpl. apply Nat.ltb_lt. lia. + + (* v < cu': shift unchanged; v < cu ≤ cu + d *) + simpl. apply Nat.ltb_lt. lia. + - (* EStringConcat *) + apply andb_prop in Hc as [H1 H2]. simpl. + rewrite IHe1 by assumption. rewrite IHe2 by assumption. reflexivity. + - (* EStringLen *) + apply IHe; assumption. + - (* ELet — e2 at S cu, with the shift cutoff also at S cu' *) + apply andb_prop in Hc as [H1 H2]. simpl. + rewrite IHe1 by assumption. + replace (S (cu + d)) with (S cu + d) by lia. + rewrite IHe2; [reflexivity | lia | assumption]. + - (* ELetLin *) + apply andb_prop in Hc as [H1 H2]. simpl. + rewrite IHe1 by assumption. + replace (S (cu + d)) with (S cu + d) by lia. + rewrite IHe2; [reflexivity | lia | assumption]. + - (* EIf *) + apply andb_prop in Hc as [H12 H3]. + apply andb_prop in H12 as [H1 H2]. simpl. + rewrite IHe1, IHe2, IHe3 by assumption. reflexivity. + - (* ELam — e' at S cu *) + simpl. + replace (S (cu + d)) with (S cu + d) by lia. + apply IHe; [lia | assumption]. + - (* EApp *) + apply andb_prop in Hc as [H1 H2]. simpl. + rewrite IHe1, IHe2 by assumption. reflexivity. + - (* EPair *) + apply andb_prop in Hc as [H1 H2]. simpl. + rewrite IHe1, IHe2 by assumption. reflexivity. + - (* EFst *) apply IHe; assumption. + - (* ESnd *) apply IHe; assumption. + - (* EInl *) apply IHe; assumption. + - (* EInr *) apply IHe; assumption. + - (* ECase *) + apply andb_prop in Hc as [H01 H2]. + apply andb_prop in H01 as [H0 H1]. simpl. + rewrite IHe1 by assumption. + replace (S (cu + d)) with (S cu + d) by lia. + rewrite IHe2; [|lia|assumption]. + rewrite IHe3; [reflexivity|lia|assumption]. + - (* ERegion *) apply IHe; assumption. + - (* EBorrow *) apply IHe; assumption. + - (* EDeref *) apply IHe; assumption. + - (* EDrop *) apply IHe; assumption. + - (* ECopy *) apply IHe; assumption. + - (* EEcho *) apply IHe; assumption. + - (* EObserve *) apply IHe; assumption. +Qed. + (** ** Region Environment *) Definition region_env := list region_name. From e2e56e4ab71ce0e385d95e6168c487d7bed7bf57 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 19:49:58 +0100 Subject: [PATCH 2/4] =?UTF-8?q?wip(L1):=20Phase=203b=20Stage=201b=20?= =?UTF-8?q?=E2=80=94=20body-transfer=20+=20closed-value=20G-poly=20helpers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Path-(i) machinery for the elegance-first Stage 1b. Closed TFunEff values are typed at ANY G — for closed values, G is genuinely irrelevant. The substitution lemma's compound-rule cases (next commit) consume this fact to discharge the G-mismatch gap that blocks `tfuneff_lambda_retype_l1_m` (G-preserving) from playing the same role Phase 2's `ground_nonlinear_retype_l1_m` plays for ground non-linear values. Ships: (1) `ctx_mark_used_app_lt` in Syntax.v — [ctx_mark_used] commutes with context append when the marked position lies within the head. Required by body-transfer's T_Var_Lin_L1 case (the only typing rule that changes G's flags). (2) `closed_below_k_typing_outer_tail_irrelevant_l1_m` in Semantics_L1.v — the body-transfer core. Structural induction on the typing derivation across 28+ rule cases. Statement: forall m R G e T R' G_out, has_type_l1 m R G e T R' G_out -> forall k G_head G_tail, G = G_head ++ G_tail -> length G_head = k -> expr_closed_below k e = true -> exists G_head_out, G_out = G_head_out ++ G_tail /\ length G_head_out = k /\ forall G_tail_new, has_type_l1 m R (G_head ++ G_tail_new) e T R' (G_head_out ++ G_tail_new). "Closed below k terms' typing depends only on G's first k positions; the outer tail is structurally irrelevant." Each typing-rule case threads (k, G_head, G_tail) through its sub-derivations and reconstructs the rule at the alternate tail. Binder rules (T_Let / T_LetLin / T_Lam_* / T_Case_*) apply IH at k+1 with the binder type cons'd onto G_head; Case rules cross-check branch agreement via `app_inv_tail`. (3) `closed_value_typing_G_poly_l1_m` in Semantics_L1.v — the consumer-facing helper. Statement (any-G' form per elegance-first decision: state what's actually true, not what fell out of the proof induction): is_value v -> expr_closed_below 0 v = true -> has_type_l1 m R G v (TFunEff T1 T2 R_in R_out) R G -> has_type_l1 m R G' v (TFunEff T1 T2 R_in R_out) R G'. Proof: invert is_value + has_type_l1 to T_Lam_L1_*_Eff cases; apply body-transfer at k=1, G_head=[(T1,false)], G_tail=G. (4) `closed_value_shift_id_l1_m` in Semantics_L1.v — companion: closed values' [shift 0 d] is identity. Specialises [Syntax.closed_below_shift_id] for the subst lemma's binder cases where [shift 0 1 v] must reduce to [v] for the typing reconstruction to fire. Owner-directive compliance (CLAUDE.md 2026-05-27): - ✅ No touch to formal/Semantics.v / Typing.v / Counterexample.v. - ✅ No closure of residual Semantics_L1.v admits attempted. - ✅ Anti-pattern detector clean (canonical CS infrastructure; no sibling-region-disjointness, no region-weakening predicates on syntactic shape, no admit-shuffling, no legacy-preservation closure attempt). - ✅ Strictly NEW infrastructure orthogonal to legacy. Build oracle (coqc 8.18.0): clean across all 12 .v files post-edit. Next commit on this branch: `subst_typing_gen_l1_m_tfuneff` Qed (~300 lines mirroring Phase 2 with the closed-value G-poly helper replacing `ground_nonlinear_retype_l1_m` where G-poly retype is needed). Then `preservation_l2_app_eff_beta_tfuneff_l1` + L2 wrapper in TypingL2.v. Refs: - ephapax issue #249 (Stage 1b tracking, this commit partial) - ephapax PR #252 (Stage 1a prerequisite — tfuneff_lambda_free + Counterexample_L2_nested) - ephapax issue #239 (parent Stage 1) - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b Stage 1b Co-Authored-By: Claude Opus 4.7 (1M context) --- formal/Semantics_L1.v | 490 ++++++++++++++++++++++++++++++++++++++++++ formal/Syntax.v | 16 ++ 2 files changed, 506 insertions(+) diff --git a/formal/Semantics_L1.v b/formal/Semantics_L1.v index 4691184..06462a8 100644 --- a/formal/Semantics_L1.v +++ b/formal/Semantics_L1.v @@ -1308,6 +1308,496 @@ Proof. inversion Ht; subst; try discriminate Hgrd; reflexivity. Qed. +(** ===== Phase 3b Stage 1b — closed-value G-polymorphism machinery ===== + + Phase 2's [ground_nonlinear_retype_l1_m] gives a fully (R, G)-poly + retype for ground non-linear values because such values contain no + de Bruijn indices — their typing is structurally independent of G. + + Phase 3b's [tfuneff_lambda_retype_l1_m] (PR #224) handles TFunEff + lambda values but is R-polymorphic AND G-preserving (the body's + typing may legitimately reference outer G). This leaves a G-mismatch + gap when the substitution lemma's compound-rule cases need to retype + the substituent at a post-e1 G. + + Resolution (path (i), elegance + correctness > workload): for + *closed* substituent values, G is genuinely irrelevant — the + lambda's body contains no free variables that reach into the outer + G beyond position 0 (the bound variable). The body-transfer lemma + below makes this structural fact mechanised; the closed-value + G-poly helper uses it via inversion on [T_Lam_L1_*_Eff]. + + Lemmas (in order): + - [closed_below_k_typing_outer_tail_irrelevant_l1_m] — the + body-transfer core: closed-below-k terms' typing depends only on + G's first k positions, with the outer tail entirely irrelevant. + Structural induction on the typing derivation; ~25 typing-rule + cases. + - [closed_value_typing_G_poly_l1_m] — the consumer-facing helper: + closed TFunEff values retype at ANY G (per "state what's + actually true"). + - [closed_value_shift_id_l1_m] — companion: closed values' shift + is identity. Specializes [closed_below_shift_id] from Syntax.v + for the value-shaped callers in the subst lemma's binder + cases. + + Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 3b + Stage 1b, ephapax issue #249. *) + +(** Body-transfer core: for terms closed below depth k, the typing + derivation depends only on the first k positions of the input + context. Splitting G as [G_head ++ G_tail] with [length G_head = k], + the tail is structurally irrelevant — the term re-types under any + [G_tail_new], producing an output of the same split shape with the + head transformed identically and the tail copied through. *) +Lemma closed_below_k_typing_outer_tail_irrelevant_l1_m : + forall m R G e T R' G_out, + has_type_l1 m R G e T R' G_out -> + forall k G_head G_tail, + G = G_head ++ G_tail -> + length G_head = k -> + expr_closed_below k e = true -> + exists G_head_out, + G_out = G_head_out ++ G_tail /\ + length G_head_out = k /\ + forall G_tail_new, + has_type_l1 m R (G_head ++ G_tail_new) e T R' (G_head_out ++ G_tail_new). +Proof. + intros m R G e T R' G_out Htype. + induction Htype; intros k G_head G_tail Hsplit Hlen Hc; subst G. + + - (* T_Unit_L1 *) + exists G_head. split; [reflexivity | split; [exact Hlen | intros; constructor]]. + + - (* T_Bool_L1 *) + exists G_head. split; [reflexivity | split; [exact Hlen | intros; constructor]]. + + - (* T_I32_L1 *) + exists G_head. split; [reflexivity | split; [exact Hlen | intros; constructor]]. + + - (* T_Var_Lin_L1: ctx_lookup G i = Some (T, false), output ctx_mark_used G i. *) + simpl in Hc. apply Nat.ltb_lt in Hc. rewrite <- Hlen in Hc. + exists (ctx_mark_used G_head i). split; [|split]. + + apply ctx_mark_used_app_lt. lia. + + rewrite ctx_mark_used_length. exact Hlen. + + intros G_tail_new. + rewrite <- (ctx_mark_used_app_lt G_head G_tail_new i ltac:(lia)). + eapply T_Var_Lin_L1; [|exact H0]. + unfold ctx_lookup in *. + rewrite nth_error_app1 by lia. + rewrite nth_error_app1 in H by lia. + exact H. + + - (* T_Var_Unr_L1: G unchanged. *) + simpl in Hc. apply Nat.ltb_lt in Hc. + exists G_head. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_Var_Unr_L1; [|exact H0]. + unfold ctx_lookup in *. + rewrite nth_error_app1 by lia. + rewrite nth_error_app1 in H by lia. + exact H. + + - (* T_Loc_L1: G unchanged, no var ref. *) + exists G_head. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros. eapply T_Loc_L1. exact H. + + - (* T_StringNew_L1 *) + exists G_head. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros. eapply T_StringNew_L1. exact H. + + - (* T_StringConcat_L1: e1 then e2, both at depth k. *) + simpl in Hc. apply andb_prop in Hc as [H1 H2]. + destruct (IHHtype1 k G_head G_tail eq_refl Hlen H1) as [G_mid_h [-> [Hlen_mid IH1]]]. + destruct (IHHtype2 k G_mid_h G_tail eq_refl Hlen_mid H2) as [G_out_h [-> [Hlen_out IH2]]]. + exists G_out_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_StringConcat_L1. + + apply IH1. + + apply IH2. + + - (* T_StringLen_L1: single sub-derivation on EBorrow e. *) + simpl in Hc. + assert (Hbe : expr_closed_below k (EBorrow e) = true) by exact Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hbe) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_StringLen_L1. apply IH1. + + - (* T_Let_L1: e1 at depth k, e2 at depth S k (binder). *) + simpl in Hc. apply andb_prop in Hc as [H1 H2]. + destruct (IHHtype1 k G_head G_tail eq_refl Hlen H1) as [G_mid_h [-> [Hlen_mid IH1]]]. + assert (Hsplit2 : ctx_extend (G_mid_h ++ G_tail) T1 = ((T1, false) :: G_mid_h) ++ G_tail). + { unfold ctx_extend. reflexivity. } + assert (Hlen2 : length ((T1, false) :: G_mid_h) = S k) by (simpl; lia). + destruct (IHHtype2 (S k) ((T1, false) :: G_mid_h) G_tail Hsplit2 Hlen2 H2) + as [G_e2h [Heq2 [Hlen_e2 IH2]]]. + (* G_e2h has length S k and prepended at the conclusion equals (T1, true) :: G''. + So G_e2h = (T1, true) :: tail of G_e2h. *) + destruct G_e2h as [|[T1' u_e2] G_e2h_tl]; [simpl in Hlen_e2; lia|]. + simpl in Heq2. inversion Heq2; subst. + exists G_e2h_tl. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_Let_L1; [apply IH1 | unfold ctx_extend; apply (IH2 G_tail_new)]. + + - (* T_LetLin_L1: same shape as T_Let_L1 + is_linear_ty T1 = true. *) + simpl in Hc. apply andb_prop in Hc as [H1 H2]. + destruct (IHHtype1 k G_head G_tail eq_refl Hlen H1) as [G_mid_h [-> [Hlen_mid IH1]]]. + assert (Hsplit2 : ctx_extend (G_mid_h ++ G_tail) T1 = ((T1, false) :: G_mid_h) ++ G_tail). + { unfold ctx_extend. reflexivity. } + assert (Hlen2 : length ((T1, false) :: G_mid_h) = S k) by (simpl; lia). + destruct (IHHtype2 (S k) ((T1, false) :: G_mid_h) G_tail Hsplit2 Hlen2 H2) + as [G_e2h [Heq2 [Hlen_e2 IH2]]]. + destruct G_e2h as [|[T1' u_e2] G_e2h_tl]; [simpl in Hlen_e2; lia|]. + simpl in Heq2. inversion Heq2; subst. + exists G_e2h_tl. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_LetLin_L1; [exact H | apply IH1 | unfold ctx_extend; apply (IH2 G_tail_new)]. + + - (* T_Lam_L1_Linear: body at S k, conclusion preserves outer G. *) + simpl in Hc. + assert (Hsplit_b : ctx_extend (G_head ++ G_tail) T1 = ((T1, false) :: G_head) ++ G_tail). + { unfold ctx_extend. reflexivity. } + assert (Hlen_b : length ((T1, false) :: G_head) = S k) by (simpl; lia). + destruct (IHHtype (S k) ((T1, false) :: G_head) G_tail Hsplit_b Hlen_b Hc) + as [G_bh [Heq_b [Hlen_bh IH_b]]]. + destruct G_bh as [|[T1' u_b] G_bh_tl]; [simpl in Hlen_bh; lia|]. + simpl in Heq_b. + injection Heq_b as Heq_T Heq_u Heq_tail. + apply app_inv_tail in Heq_tail. subst T1' u_b G_bh_tl. + exists G_head. split; [reflexivity | split; [exact Hlen |]]. + intros G_tail_new. + eapply T_Lam_L1_Linear. unfold ctx_extend. apply IH_b. + + - (* T_Lam_L1_Affine: same as Linear with flexible u. *) + simpl in Hc. + assert (Hsplit_b : ctx_extend (G_head ++ G_tail) T1 = ((T1, false) :: G_head) ++ G_tail). + { unfold ctx_extend. reflexivity. } + assert (Hlen_b : length ((T1, false) :: G_head) = S k) by (simpl; lia). + destruct (IHHtype (S k) ((T1, false) :: G_head) G_tail Hsplit_b Hlen_b Hc) + as [G_bh [Heq_b [Hlen_bh IH_b]]]. + destruct G_bh as [|[T1' u_b] G_bh_tl]; [simpl in Hlen_bh; lia|]. + simpl in Heq_b. + injection Heq_b as Heq_T Heq_u Heq_tail. + apply app_inv_tail in Heq_tail. subst T1' u_b G_bh_tl. + exists G_head. split; [reflexivity | split; [exact Hlen |]]. + intros G_tail_new. + eapply T_Lam_L1_Affine. unfold ctx_extend. apply IH_b. + + - (* T_Lam_L1_Linear_Eff: body at R_in / S k, side condition forall r in R, r in R_in. *) + simpl in Hc. + assert (Hsplit_b : ctx_extend (G_head ++ G_tail) T1 = ((T1, false) :: G_head) ++ G_tail). + { unfold ctx_extend. reflexivity. } + assert (Hlen_b : length ((T1, false) :: G_head) = S k) by (simpl; lia). + destruct (IHHtype (S k) ((T1, false) :: G_head) G_tail Hsplit_b Hlen_b Hc) + as [G_bh [Heq_b [Hlen_bh IH_b]]]. + destruct G_bh as [|[T1' u_b] G_bh_tl]; [simpl in Hlen_bh; lia|]. + simpl in Heq_b. + injection Heq_b as Heq_T Heq_u Heq_tail. + apply app_inv_tail in Heq_tail. subst T1' u_b G_bh_tl. + exists G_head. split; [reflexivity | split; [exact Hlen |]]. + intros G_tail_new. + eapply T_Lam_L1_Linear_Eff; [exact H | unfold ctx_extend; apply IH_b]. + + - (* T_Lam_L1_Affine_Eff: same as Linear_Eff with flexible u. *) + simpl in Hc. + assert (Hsplit_b : ctx_extend (G_head ++ G_tail) T1 = ((T1, false) :: G_head) ++ G_tail). + { unfold ctx_extend. reflexivity. } + assert (Hlen_b : length ((T1, false) :: G_head) = S k) by (simpl; lia). + destruct (IHHtype (S k) ((T1, false) :: G_head) G_tail Hsplit_b Hlen_b Hc) + as [G_bh [Heq_b [Hlen_bh IH_b]]]. + destruct G_bh as [|[T1' u_b] G_bh_tl]; [simpl in Hlen_bh; lia|]. + simpl in Heq_b. + injection Heq_b as Heq_T Heq_u Heq_tail. + apply app_inv_tail in Heq_tail. subst T1' u_b G_bh_tl. + exists G_head. split; [reflexivity | split; [exact Hlen |]]. + intros G_tail_new. + eapply T_Lam_L1_Affine_Eff; [exact H | unfold ctx_extend; apply IH_b]. + + - (* T_App_L1: two sub-derivations e1, e2 at depth k. *) + simpl in Hc. apply andb_prop in Hc as [H1 H2]. + destruct (IHHtype1 k G_head G_tail eq_refl Hlen H1) as [G_mid_h [-> [Hlen_mid IH1]]]. + destruct (IHHtype2 k G_mid_h G_tail eq_refl Hlen_mid H2) as [G_out_h [-> [Hlen_out IH2]]]. + exists G_out_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_App_L1; [apply IH1 | apply IH2]. + + - (* T_Pair_L1 *) + simpl in Hc. apply andb_prop in Hc as [H1 H2]. + destruct (IHHtype1 k G_head G_tail eq_refl Hlen H1) as [G_mid_h [-> [Hlen_mid IH1]]]. + destruct (IHHtype2 k G_mid_h G_tail eq_refl Hlen_mid H2) as [G_out_h [-> [Hlen_out IH2]]]. + exists G_out_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_Pair_L1; [apply IH1 | apply IH2]. + + - (* T_Fst_L1 *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Fst_L1; [apply IH1 | exact H]. + + - (* T_Snd_L1 *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Snd_L1; [apply IH1 | exact H]. + + - (* T_Inl_L1 *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Inl_L1. apply IH1. + + - (* T_Inr_L1 *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Inr_L1. apply IH1. + + - (* T_Case_L1_Linear: scrutinee at k, both branches at S k, must agree on G_final. *) + simpl in Hc. apply andb_prop in Hc as [Hc01 Hc2]. + apply andb_prop in Hc01 as [Hc0 Hc1]. + destruct (IHHtype1 k G_head G_tail eq_refl Hlen Hc0) as [G'h [-> [Hlen' IH0]]]. + assert (Hsplit_e1 : ctx_extend (G'h ++ G_tail) T1 = ((T1, false) :: G'h) ++ G_tail). + { unfold ctx_extend. reflexivity. } + assert (Hsplit_e2 : ctx_extend (G'h ++ G_tail) T2 = ((T2, false) :: G'h) ++ G_tail). + { unfold ctx_extend. reflexivity. } + assert (Hlen_e : length ((T1, false) :: G'h) = S k) by (simpl; lia). + assert (Hlen_e2 : length ((T2, false) :: G'h) = S k) by (simpl; lia). + destruct (IHHtype2 (S k) ((T1, false) :: G'h) G_tail Hsplit_e1 Hlen_e Hc1) + as [G_e1h [Heq_e1 [Hlen_e1h IH1]]]. + destruct (IHHtype3 (S k) ((T2, false) :: G'h) G_tail Hsplit_e2 Hlen_e2 Hc2) + as [G_e2h [Heq_e2 [Hlen_e2h IH2]]]. + destruct G_e1h as [|[T1' u1] G_e1h_tl]; [simpl in Hlen_e1h; lia|]. + destruct G_e2h as [|[T2' u2] G_e2h_tl]; [simpl in Hlen_e2h; lia|]. + simpl in Heq_e1, Heq_e2. + injection Heq_e1 as Heq_T1 Heq_u1 Heq_final1. + injection Heq_e2 as Heq_T2 Heq_u2 Heq_final2. + subst T1' u1 T2' u2. + (* Both branches forced G_final_outer = G_e1h_tl ++ G_tail = G_e2h_tl ++ G_tail. + By app injectivity on equal-length tails, G_e1h_tl = G_e2h_tl. *) + assert (Hlen_inner_eq : length G_e1h_tl = length G_e2h_tl) + by (simpl in Hlen_e1h, Hlen_e2h; lia). + pose proof (app_inv_tail _ G_e1h_tl G_e2h_tl + (eq_trans (eq_sym Heq_final1) Heq_final2)) as Heq_tl. + subst G_e2h_tl. rewrite Heq_final1. + exists G_e1h_tl. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_Case_L1_Linear. + * apply (IH0 G_tail_new). + * unfold ctx_extend. apply (IH1 G_tail_new). + * unfold ctx_extend. apply (IH2 G_tail_new). + + - (* T_Case_L1_Affine: same structure with flexible u1, u2. *) + simpl in Hc. apply andb_prop in Hc as [Hc01 Hc2]. + apply andb_prop in Hc01 as [Hc0 Hc1]. + destruct (IHHtype1 k G_head G_tail eq_refl Hlen Hc0) as [G'h [-> [Hlen' IH0]]]. + assert (Hsplit_e1 : ctx_extend (G'h ++ G_tail) T1 = ((T1, false) :: G'h) ++ G_tail). + { unfold ctx_extend. reflexivity. } + assert (Hsplit_e2 : ctx_extend (G'h ++ G_tail) T2 = ((T2, false) :: G'h) ++ G_tail). + { unfold ctx_extend. reflexivity. } + assert (Hlen_e : length ((T1, false) :: G'h) = S k) by (simpl; lia). + assert (Hlen_e2 : length ((T2, false) :: G'h) = S k) by (simpl; lia). + destruct (IHHtype2 (S k) ((T1, false) :: G'h) G_tail Hsplit_e1 Hlen_e Hc1) + as [G_e1h [Heq_e1 [Hlen_e1h IH1]]]. + destruct (IHHtype3 (S k) ((T2, false) :: G'h) G_tail Hsplit_e2 Hlen_e2 Hc2) + as [G_e2h [Heq_e2 [Hlen_e2h IH2]]]. + destruct G_e1h as [|[T1' u1'] G_e1h_tl]; [simpl in Hlen_e1h; lia|]. + destruct G_e2h as [|[T2' u2'] G_e2h_tl]; [simpl in Hlen_e2h; lia|]. + simpl in Heq_e1, Heq_e2. + injection Heq_e1 as Heq_T1 Heq_u1 Heq_final1. + injection Heq_e2 as Heq_T2 Heq_u2 Heq_final2. + subst T1' u1' T2' u2'. + assert (Hlen_inner_eq : length G_e1h_tl = length G_e2h_tl) + by (simpl in Hlen_e1h, Hlen_e2h; lia). + pose proof (app_inv_tail _ G_e1h_tl G_e2h_tl + (eq_trans (eq_sym Heq_final1) Heq_final2)) as Heq_tl. + subst G_e2h_tl. rewrite Heq_final1. + exists G_e1h_tl. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_Case_L1_Affine. + * apply (IH0 G_tail_new). + * unfold ctx_extend. apply (IH1 G_tail_new). + * unfold ctx_extend. apply (IH2 G_tail_new). + + - (* T_If_L1_Linear: e1, e2, e3 all at depth k (no binders). *) + simpl in Hc. apply andb_prop in Hc as [Hc12 Hc3]. + apply andb_prop in Hc12 as [Hc1 Hc2]. + destruct (IHHtype1 k G_head G_tail eq_refl Hlen Hc1) as [G_mid_h [-> [Hlen_mid IH1]]]. + destruct (IHHtype2 k G_mid_h G_tail eq_refl Hlen_mid Hc2) as [G_out_h [-> [Hlen_out IH2]]]. + destruct (IHHtype3 k G_mid_h G_tail eq_refl Hlen_mid Hc3) + as [G_out_h3 [Heq3 [Hlen_out3 IH3]]]. + assert (Hlen_eq : length G_out_h = length G_out_h3) by lia. + pose proof (app_inv_tail _ G_out_h G_out_h3 Heq3) as Heq_h. + subst G_out_h3. + exists G_out_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_If_L1_Linear; [apply IH1 | apply IH2 | apply IH3]. + + - (* T_If_L1_Affine *) + simpl in Hc. apply andb_prop in Hc as [Hc12 Hc3]. + apply andb_prop in Hc12 as [Hc1 Hc2]. + destruct (IHHtype1 k G_head G_tail eq_refl Hlen Hc1) as [G_mid_h [-> [Hlen_mid IH1]]]. + destruct (IHHtype2 k G_mid_h G_tail eq_refl Hlen_mid Hc2) as [G_out_h [-> [Hlen_out IH2]]]. + destruct (IHHtype3 k G_mid_h G_tail eq_refl Hlen_mid Hc3) + as [G_out_h3 [Heq3 [Hlen_out3 IH3]]]. + assert (Hlen_eq : length G_out_h = length G_out_h3) by lia. + pose proof (app_inv_tail _ G_out_h G_out_h3 Heq3) as Heq_h. + subst G_out_h3. + exists G_out_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_If_L1_Affine; [apply IH1 | apply IH2 | apply IH3]. + + - (* T_Region_L1: body at r::R / G, side conditions ~In r R / ~In r free_regions T / In r R_body. *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Region_L1; eauto. + + - (* T_Region_Active_L1 *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Region_Active_L1; eauto. + + - (* T_Region_L1_Echo *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Region_L1_Echo; eauto. + + - (* T_Region_Active_L1_Echo *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Region_Active_L1_Echo; eauto. + + - (* T_Borrow_L1: EBorrow (EVar i), G unchanged. *) + simpl in Hc. apply Nat.ltb_lt in Hc. + exists G_head. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_Borrow_L1. + unfold ctx_lookup in *. + rewrite nth_error_app1 by lia. + rewrite nth_error_app1 in H by lia. + exact H. + + - (* T_Borrow_Val_L1: v value, G unchanged. IH gives v at G — G unchanged means G_h = G_head. *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [Heq_h [Hlen_h IH1]]]. + (* The rule's input = output = G_head ++ G_tail. So G_h ++ G_tail = G_head ++ G_tail. *) + pose proof (app_inv_tail _ G_h G_head (eq_sym Heq_h)) as ->. + exists G_head. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_Borrow_Val_L1; [exact H | apply IH1]. + + - (* T_Drop_L1 *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Drop_L1; [exact H | apply IH1]. + + - (* T_Drop_L1_Echo *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Drop_L1_Echo; [exact H | apply IH1]. + + - (* T_Copy_L1 *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Copy_L1; [exact H | apply IH1]. + + - (* T_Echo_L1: v value, G unchanged. *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [Heq_h [Hlen_h IH1]]]. + pose proof (app_inv_tail _ G_h G_head (eq_sym Heq_h)) as ->. + exists G_head. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. + eapply T_Echo_L1; [exact H | apply IH1]. + + - (* T_Observe_L1 *) + simpl in Hc. + destruct (IHHtype k G_head G_tail eq_refl Hlen Hc) as [G_h [-> [Hlen_h IH1]]]. + exists G_h. split; [reflexivity | split; [solve [exact Hlen | exact Hlen_h | exact Hlen_mid | exact Hlen_out | exact Hlen' | simpl in *; lia] |]]. + intros G_tail_new. eapply T_Observe_L1; apply IH1. +Qed. + +(** Closed TFunEff lambda values type at ANY G — for closed values, G + is genuinely irrelevant (not "G of matching length / matching + types" — actually irrelevant). + + Used by Phase 3b Stage 1b's substitution lemma's compound-rule + cases (T_Let_L1, T_LetLin_L1, T_StringConcat_L1, T_App_L1, + T_Pair_L1, T_Case_L1_x, T_If_L1_x, T_Region_x) where the + substituent's required typing context shifts as the sub-derivations + progress. For closed v = ELam T0 ebody, the body's typing references + only position 0 (the bound variable); G's tail is structurally + inert via [closed_below_k_typing_outer_tail_irrelevant_l1_m] at + k=1, G_head = [(T0, false)], G_tail = G. + + Stage 4 (#242) replaces the syntactic [expr_closed_below 0 v] + precondition with a typing-derived closure invariant; the proof + content of this lemma is reused as Stage 4's closure-discharge + kernel. *) +Lemma closed_value_typing_G_poly_l1_m : + forall m R G G' v T1 T2 R_in R_out, + is_value v -> + expr_closed_below 0 v = true -> + has_type_l1 m R G v (TFunEff T1 T2 R_in R_out) R G -> + has_type_l1 m R G' v (TFunEff T1 T2 R_in R_out) R G'. +Proof. + intros m R G G' v T1 T2 R_in R_out Hval Hclos Ht. + destruct Hval as + [ | b | n + | T0 e0 | v1 v2 Hv1 Hv2 + | T0 v0 Hv0 | T0 v0 Hv0 + | l r + | v0 Hv0 + | T0 v0 Hv0 ]; + inversion Ht; subst. + - (* v = ELam T0 e0, T_Lam_L1_Linear_Eff *) + simpl in Hclos. + assert (Hbody : has_type_l1 Linear R_in (ctx_extend G T1) e0 T2 R_out ((T1, true) :: G)) + by eassumption. + pose proof (closed_below_k_typing_outer_tail_irrelevant_l1_m + Linear R_in (ctx_extend G T1) e0 T2 R_out ((T1, true) :: G) Hbody + 1 [(T1, false)] G eq_refl eq_refl Hclos) as + [G_bh [Heq_b [Hlen_b IH_b]]]. + destruct G_bh as [|[T1' u_b] [|x rest]]; simpl in Hlen_b; try lia. + simpl in Heq_b. inversion Heq_b; subst. + eapply T_Lam_L1_Linear_Eff; [eassumption | unfold ctx_extend; apply (IH_b G')]. + - (* v = ELam T0 e0, T_Lam_L1_Affine_Eff *) + simpl in Hclos. + assert (Hbody : has_type_l1 Affine R_in (ctx_extend G T1) e0 T2 R_out ((T1, u) :: G)) + by eassumption. + pose proof (closed_below_k_typing_outer_tail_irrelevant_l1_m + Affine R_in (ctx_extend G T1) e0 T2 R_out ((T1, u) :: G) Hbody + 1 [(T1, false)] G eq_refl eq_refl Hclos) as + [G_bh [Heq_b [Hlen_b IH_b]]]. + destruct G_bh as [|[T1' u_b] [|x rest]]; simpl in Hlen_b; try lia. + simpl in Heq_b. inversion Heq_b; subst. + eapply T_Lam_L1_Affine_Eff; [eassumption | unfold ctx_extend; apply (IH_b G')]. +Qed. + +(** Closed values are shift-invariant at cutoff 0. + + Specialisation of [Syntax.closed_below_shift_id] for the + substitution lemma's binder cases (T_Let_L1, T_LetLin_L1, ELam, + T_Case_L1_x) where the operational [shift 0 d v] in [subst] must + reduce to [v] for the typing reconstruction to fire. [is_value] + is not used in the proof — closure is purely syntactic — but is + threaded in the signature to match the calling convention of + Phase 2's [ground_nonlinear_value_shift_id_l1]. *) +Lemma closed_value_shift_id_l1_m : + forall v d, + expr_closed_below 0 v = true -> + shift 0 d v = v. +Proof. + intros v d Hclos. + apply closed_below_shift_id. exact Hclos. +Qed. + (** Narrower axiom (region-liveness at compound-rule split points). Given a well-typed sub-derivation [R; G |=L1 e1 : T1 -| R1; G'] diff --git a/formal/Syntax.v b/formal/Syntax.v index df23cf9..5b9b9cb 100644 --- a/formal/Syntax.v +++ b/formal/Syntax.v @@ -427,6 +427,22 @@ Proof. + apply IH. intro H. apply Hne. f_equal. exact H. Qed. +(** [ctx_mark_used] commutes with context append when the marked + position lies within the head. Required by Phase 3b Stage 1b's + body-transfer lemma for the [T_Var_Lin_L1] case (the only typing + rule that changes G's flags). *) +Lemma ctx_mark_used_app_lt : + forall (G_head G_tail : ctx) (i : nat), + i < List.length G_head -> + ctx_mark_used (G_head ++ G_tail) i = ctx_mark_used G_head i ++ G_tail. +Proof. + induction G_head as [|[T0 u0] G_head' IH]; intros G_tail i Hlt; simpl in *. + - lia. + - destruct i. + + reflexivity. + + simpl. f_equal. apply IH. lia. +Qed. + (** flags_only_increase via projection: if flag is false in output, it was false in input *) (** Direct contradiction for the T_Let/T_LetLin/T_Case idx=0 case. Uses functional extraction to avoid option-pair discrimination. *) From 491ff146304b9ea7c863fb729c3f95d59c63b726 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 20:13:29 +0100 Subject: [PATCH 3/4] =?UTF-8?q?feat(L1):=20Phase=203b=20Stage=201b=20?= =?UTF-8?q?=E2=80=94=20subst=5Ftyping=5Fgen=5Fl1=5Fm=5Ftfuneff=20Qed=20(ze?= =?UTF-8?q?ro=20axioms)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ships the substitution-lemma half of Stage 1b. Closed TFunEff values can now be substituted at depth k into leaf-only outer expressions with full L1-typing preservation. Lemma signature: forall m R Gin e T R' Gout, has_type_l1 m R Gin e T R' Gout -> forall k Ta Tb R_in_v R_out_v v u_in, nth_error Gin k = Some (TFunEff Ta Tb R_in_v R_out_v, u_in) -> is_value v -> tfuneff_lambda_free e = true -> (P1) (forall r, In r (regions_introduced_by e) -> In r R_in_v) -> (P2) expr_closed_below 0 v = true -> (P3) has_type_l1 m R (remove_at k Gin) v (TFunEff Ta Tb R_in_v R_out_v) R (remove_at k Gin) -> forall u_out, nth_error Gout k = Some (TFunEff Ta Tb R_in_v R_out_v, u_out) -> has_type_l1 m R (remove_at k Gin) (subst k v e) T R' (remove_at k Gout). Mirrors Phase 2's [subst_typing_gen_l1_m_ground_nonlinear] structurally with two swaps: - Phase 2's [ground_nonlinear_retype_l1_m] (R, G-poly retype for ground non-linear values, no side conditions) is replaced by [closed_value_typing_RG_poly_l1_m] (closed TFunEff value RG-poly retype, requires R' ⊆ R_in side condition). The side condition is discharged at each compound-rule call site via [sub_R_in_R_in_via_value_l1_m]: chain (sub-derivation R' ⊆ outer R via count_occ_le_l1_m) + (outer R ⊆ R_in_v via the substituent's T_Lam_L1_*_Eff formation side condition, extracted by value_TFunEff_R_subset_R_in_l1_m). - Phase 2's [ground_nonlinear_value_shift_id_l1] is replaced by [closed_value_shift_id_l1_m] for binder-traversal shift-identity. Inner T_Lam_L1_* / T_Lam_L1_*_Eff cases discharge via [discriminate] on P1 (tfuneff_lambda_free (ELam _ _) = false). Two new supporting lemmas in Semantics_L1.v: - [closed_value_typing_RG_poly_l1_m] — combined RG-poly retype chaining [closed_value_typing_G_poly_l1_m] with [tfuneff_lambda_retype_l1_m] (PR #224). - [value_TFunEff_R_subset_R_in_l1_m] — extracts the lambda-formation side condition R ⊆ R_in from any TFunEff value typing. Trivial inversion proof. - [sub_R_in_R_in_via_value_l1_m] — packages the R-subset chain used at every compound-rule call site in subst_typing_gen_l1_m_tfuneff. Print Assumptions verdict on all four new lemmas: - subst_typing_gen_l1_m_tfuneff: Closed under the global context - closed_value_typing_G_poly_l1_m: Closed under the global context - closed_value_typing_RG_poly_l1_m: Closed under the global context - closed_below_k_typing_outer_tail_irrelevant_l1_m: Closed under the global context Zero new axioms. Zero new admits. Stage 1b's L1-level deliverable is complete; the L2 β-wrapper [preservation_l2_app_eff_beta_tfuneff_l1] + L2-judgment surface lemma ship next on this branch. Owner-directive compliance (CLAUDE.md 2026-05-27): - ✅ No touch to formal/Semantics.v / Typing.v / Counterexample.v. - ✅ No closure of residual Semantics_L1.v admits attempted. - ✅ Anti-pattern detector clean across all four stages of the 4-stage Phase 3b plan (#235 → #239 / #240 / #241 / #242). - ✅ Strictly NEW infrastructure orthogonal to legacy. Build oracle (coqc 8.18.0): clean across all 12 .v files. Refs: - ephapax issue #249 (Stage 1b tracking; this commit is the L1 half). - ephapax PR #252 (Stage 1a prerequisite — tfuneff_lambda_free + Counterexample_L2_nested + design doc). - ephapax issue #239 (parent Stage 1). - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b Stage 1b. Co-Authored-By: Claude Opus 4.7 (1M context) --- formal/Semantics_L1.v | 480 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 480 insertions(+) diff --git a/formal/Semantics_L1.v b/formal/Semantics_L1.v index 06462a8..6f72b83 100644 --- a/formal/Semantics_L1.v +++ b/formal/Semantics_L1.v @@ -1798,6 +1798,91 @@ Proof. apply closed_below_shift_id. exact Hclos. Qed. +(** Combined R + G poly retype for closed TFunEff lambda values. + + Mirrors Phase 2's [ground_nonlinear_retype_l1_m] (full (R, G) + polymorphism) for the closed TFunEff substituent of Phase 3b + Stage 1b. The R-component requires the side condition + [(forall r, In r R' -> In r R_in)] mirroring + [tfuneff_lambda_retype_l1_m]'s constraint — closed TFunEff + values' typing demands the new R fit within the lambda's + declared input env. + + Used by [subst_typing_gen_l1_m_tfuneff]'s compound-rule cases + where the substituent must retype at a sub-derivation's (R, G) + pair (e.g., post-e1 R1 / G_mid in [T_Let_L1] / [T_StringConcat_L1] / + [T_App_L1] / etc.). The R' ⊆ R_in obligation is derivable at + the call site from [count_occ_le_l1_m] (sub-derivation's R is + a subset of the outer R) chained with the lambda formation + rule's own R ⊆ R_in side condition (extracted from the original + [Hv_type] via [value_TFunEff_R_subset_R_in_l1_m]). *) +Lemma closed_value_typing_RG_poly_l1_m : + forall m R R' G G' v T1 T2 R_in R_out, + is_value v -> + expr_closed_below 0 v = true -> + has_type_l1 m R G v (TFunEff T1 T2 R_in R_out) R G -> + (forall r, In r R' -> In r R_in) -> + has_type_l1 m R' G' v (TFunEff T1 T2 R_in R_out) R' G'. +Proof. + intros m R R' G G' v T1 T2 R_in R_out Hval Hclos Ht HR'. + (* First retype at any G' with the original R. *) + pose proof (closed_value_typing_G_poly_l1_m _ _ _ G' _ _ _ _ _ Hval Hclos Ht) as Ht'. + (* Then retype the R via tfuneff_lambda_retype_l1_m. *) + eapply tfuneff_lambda_retype_l1_m; eassumption. +Qed. + +(** Extract [R ⊆ R_in] from a TFunEff value's typing. + + A TFunEff lambda value's typing fires via [T_Lam_L1_Linear_Eff] + or [T_Lam_L1_Affine_Eff], both of which carry the formation + side condition [(forall r, In r R -> In r R_in)]. This lemma + surfaces that side condition from any TFunEff value typing, + enabling the [closed_value_typing_RG_poly_l1_m] R-discharge + at call sites. *) +Lemma value_TFunEff_R_subset_R_in_l1_m : + forall m R G v T1 T2 R_in R_out, + is_value v -> + has_type_l1 m R G v (TFunEff T1 T2 R_in R_out) R G -> + forall r, In r R -> In r R_in. +Proof. + intros m R G v T1 T2 R_in R_out Hval Ht. + destruct Hval as + [ | b | n + | T0 e0 | v1 v2 Hv1 Hv2 + | T0 v0 Hv0 | T0 v0 Hv0 + | l r0 + | v0 Hv0 + | T0 v0 Hv0 ]; + inversion Ht; subst; assumption. +Qed. + +(** Chained helper: a sub-derivation's threaded R is contained in + the substituent value's declared input env [R_in]. + + Packages the chain (sub-derivation R ⊆ outer R) + (outer R ⊆ + R_in via the substituent's formation side condition) used at + every compound-rule call site of [subst_typing_gen_l1_m_tfuneff]. + + The substituent [v] is a TFunEff value typed at outer R; the + sub-derivation [He] threads R → R1 inside the outer expression + [e]. By [count_occ_le_l1_m] R1 ⊆ R; by + [value_TFunEff_R_subset_R_in_l1_m] R ⊆ R_in; transitively + R1 ⊆ R_in. *) +Lemma sub_R_in_R_in_via_value_l1_m : + forall m R G_e e T R1 G_e' G_v v T1 T2 R_in R_out, + has_type_l1 m R G_e e T R1 G_e' -> + is_value v -> + has_type_l1 m R G_v v (TFunEff T1 T2 R_in R_out) R G_v -> + forall r, In r R1 -> In r R_in. +Proof. + intros m R G_e e T R1 G_e' G_v v T1 T2 R_in R_out He Hval Hv r Hr. + eapply value_TFunEff_R_subset_R_in_l1_m; [exact Hval | exact Hv |]. + apply (count_occ_In string_dec). + pose proof (count_occ_le_l1_m _ _ _ _ _ _ _ He r) as Hle. + apply (count_occ_In string_dec) in Hr. + unfold cnt in Hle. lia. +Qed. + (** Narrower axiom (region-liveness at compound-rule split points). Given a well-typed sub-derivation [R; G |=L1 e1 : T1 -| R1; G'] @@ -2562,6 +2647,401 @@ Proof. - eapply T_Observe_L1. eapply IHHtype; eassumption. Qed. +(** ===== Phase 3b Stage 1b — substitution lemma for closed TFunEff + substituents in leaf-only outer expressions ===== + + Mirrors [subst_typing_gen_l1_m_ground_nonlinear] (Phase 2, + lines 1812-2073 above) with two structural swaps: + + - Phase 2's [ground_nonlinear_retype_l1_m] (full (R, G)-poly + retype for ground non-linear values) is replaced by + [closed_value_typing_G_poly_l1_m] (G-poly retype for closed + TFunEff lambda values). The R parameter stays fixed at the + substitutent's R; only G changes through compound rule + threading. The R-restriction is acceptable because at the + call site [preservation_l2_app_eff_beta_tfuneff_l1] the + [value_R_G_preserving_l1] collapse forces R_in = R1 = R. + + - Phase 2's [ground_nonlinear_value_shift_id_l1] is replaced + by [closed_value_shift_id_l1_m]. Both reduce [shift 0 d v] + to [v]: Phase 2 via the typing witness of ground-non-linear + shape; Phase 3b via the syntactic closure check. + + Three additional preconditions threaded through the induction: + + - [tfuneff_lambda_free e = true] (P1): the OUTER expression is + leaf-only with respect to TFunEff-typed lambdas. Inner + [T_Lam_L1_*] cases [discriminate] off this; inner + [T_Lam_L1_*_Eff] cases likewise. Compound rules andb-split + the predicate across sub-derivations. + + - [(forall r, In r (regions_introduced_by e) -> In r R_in_v)] + (P2): every region introduced syntactically in [e] is + visible in the substituent's declared input env. Per + [regions_introduced_by]'s monotonicity through compound + forms, P2 propagates to sub-derivations via list-append + reasoning. + + - [expr_closed_below 0 v = true] (P3): the substituent is + closed. Powers both the G-poly retype and the shift-identity + lemma above. Naturally satisfied at the + [preservation_l2_app_eff_beta_tfuneff_l1] call site (v is + the operational β-redex argument, typed at the lambda's + formation context). + + Inner [T_Lam_L1_*_Eff] cases discharge via P1 ([tfuneff_lambda_free + (ELam _ _) = false]); the non-effect [T_Lam_L1_Linear] / + [T_Lam_L1_Affine] cases discharge identically. + + Stage 1 of the four-stage Phase 3b resolution plan (#235): + issue #239 (Stage 1) / #240 (Stage 2 ELam annotation) / #241 + (Stage 3 relaxed Phase 3b + CPS) / #242 (Stage 4 unconditional + preservation_l2). Stage 2-4 progressively remove preconditions + P1, P2, P3; Stage 1 ships the leaf-only with-closure variant. + + Owner-directive compliance (CLAUDE.md 2026-05-27): + - ✅ Strictly NEW infrastructure orthogonal to legacy. + - ✅ No touch to Semantics.v / Typing.v / Counterexample.v. + - ✅ No new Axiom / Admitted; no closure of residual + Semantics_L1.v admits. + + Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 3b + Stage 1b, ephapax issue #249. *) +Lemma subst_typing_gen_l1_m_tfuneff : + forall m R Gin e T R' Gout, + has_type_l1 m R Gin e T R' Gout -> + forall k Ta Tb R_in_v R_out_v v u_in, + nth_error Gin k = Some (TFunEff Ta Tb R_in_v R_out_v, u_in) -> + is_value v -> + tfuneff_lambda_free e = true -> + (forall r, In r (regions_introduced_by e) -> In r R_in_v) -> + expr_closed_below 0 v = true -> + has_type_l1 m R (remove_at k Gin) v + (TFunEff Ta Tb R_in_v R_out_v) R (remove_at k Gin) -> + forall u_out, + nth_error Gout k = Some (TFunEff Ta Tb R_in_v R_out_v, u_out) -> + has_type_l1 m R (remove_at k Gin) (subst k v e) T R' (remove_at k Gout). +Proof. + intros m R Gin e T R' Gout Htype. + induction Htype; intros k0 Ta Tb R_in_v R_out_v vv u_in + Hk_in Hval Hflam Hreg Hclos Hv_type u_out Hk_out; simpl in *. + + (* T_Unit_L1, T_Bool_L1, T_I32_L1 *) + 1-3: (assert (u_out = u_in) by congruence; subst; constructor). + + (* T_Var_Lin_L1 *) + - destruct (Nat.eq_dec i k0) as [->|Hne]. + + (* i = k0: rule's [is_linear_ty T = true] contradicts + [is_linear_ty (TFunEff ...) = false] *) + exfalso. + assert (T = TFunEff Ta Tb R_in_v R_out_v) + by (unfold ctx_lookup in H; congruence). + subst T. simpl in H0. discriminate H0. + + rewrite (proj2 (Nat.eqb_neq i k0) Hne). + destruct (Nat.ltb_spec k0 i) as [Hlt|Hge]. + * assert (Hrw: remove_at k0 (ctx_mark_used G i) = + ctx_mark_used (remove_at k0 G) (i - 1)). + { replace i with (S (i - 1)) at 1 by lia. + apply remove_at_ctx_mark_used_gt. lia. } + rewrite Hrw. + eapply T_Var_Lin_L1. + -- unfold ctx_lookup. rewrite nth_error_remove_at_ge by lia. + replace (S (i - 1)) with i by lia. + unfold ctx_lookup in H. exact H. + -- exact H0. + * assert (i < k0) by lia. + rewrite remove_at_ctx_mark_used_lt by lia. + eapply T_Var_Lin_L1. + -- unfold ctx_lookup. rewrite nth_error_remove_at_lt by lia. + unfold ctx_lookup in H. exact H. + -- exact H0. + + (* T_Var_Unr_L1 *) + - destruct (Nat.eq_dec i k0) as [->|Hne]. + + (* i = k0: CONSTRUCTIVE case. Substituent's TFunEff typing is + re-derived at the rule's output context = G via + closed_value_typing_G_poly_l1_m. *) + rewrite Nat.eqb_refl. + assert (T = TFunEff Ta Tb R_in_v R_out_v) + by (unfold ctx_lookup in H; congruence). + subst T. + assert (u_out = u_in) by congruence; subst u_out. + exact Hv_type. + + rewrite (proj2 (Nat.eqb_neq i k0) Hne). + destruct (Nat.ltb_spec k0 i) as [Hlt|Hge]. + * eapply T_Var_Unr_L1. + -- unfold ctx_lookup. rewrite nth_error_remove_at_ge by lia. + replace (S (i - 1)) with i by lia. + unfold ctx_lookup in H. exact H. + -- exact H0. + * assert (i < k0) by lia. eapply T_Var_Unr_L1. + -- unfold ctx_lookup. rewrite nth_error_remove_at_lt by lia. + unfold ctx_lookup in H. exact H. + -- exact H0. + + (* T_Loc_L1 *) + - assert (u_out = u_in) by congruence; subst. constructor. assumption. + (* T_StringNew_L1 *) + - assert (u_out = u_in) by congruence; subst. constructor. assumption. + + (* T_StringConcat_L1 *) + - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + apply andb_prop in Hflam as [Hf1 Hf2]. + eapply T_StringConcat_L1. + + eapply IHHtype1; try eassumption. + intros rr Hrr. apply Hreg. apply in_app_iff. left. exact Hrr. + + eapply IHHtype2; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + (* T_StringLen_L1 *) + - eapply T_StringLen_L1. eapply IHHtype; eassumption. + + (* T_Let_L1 *) + - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + apply andb_prop in Hflam as [Hf1 Hf2]. + eapply T_Let_L1. + + eapply IHHtype1; try eassumption. + intros rr Hrr. apply Hreg. apply in_app_iff. left. exact Hrr. + + rewrite (closed_value_shift_id_l1_m vv 1 Hclos). + eapply (IHHtype2 (S k0) Ta Tb R_in_v R_out_v vv u_mid); + simpl; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + (* T_LetLin_L1 *) + - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + apply andb_prop in Hflam as [Hf1 Hf2]. + eapply T_LetLin_L1; [exact H | |]. + + eapply IHHtype1; try eassumption. + intros rr Hrr. apply Hreg. apply in_app_iff. left. exact Hrr. + + rewrite (closed_value_shift_id_l1_m vv 1 Hclos). + eapply (IHHtype2 (S k0) Ta Tb R_in_v R_out_v vv u_mid); + simpl; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + (* T_Lam_L1_Linear: P1 excludes — tfuneff_lambda_free (ELam _ _) = false. *) + - discriminate Hflam. + + (* T_Lam_L1_Affine: same *) + - discriminate Hflam. + + (* T_Lam_L1_Linear_Eff: same *) + - discriminate Hflam. + + (* T_Lam_L1_Affine_Eff: same *) + - discriminate Hflam. + + (* T_App_L1 *) + - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + apply andb_prop in Hflam as [Hf1 Hf2]. + eapply T_App_L1. + + eapply IHHtype1; try eassumption. + intros rr Hrr. apply Hreg. apply in_app_iff. left. exact Hrr. + + eapply IHHtype2; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + (* T_Pair_L1 *) + - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + apply andb_prop in Hflam as [Hf1 Hf2]. + eapply T_Pair_L1. + + eapply IHHtype1; try eassumption. + intros rr Hrr. apply Hreg. apply in_app_iff. left. exact Hrr. + + eapply IHHtype2; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + (* T_Fst_L1 *) + - eapply T_Fst_L1; [eapply IHHtype; eassumption | assumption]. + + (* T_Snd_L1 *) + - eapply T_Snd_L1; [eapply IHHtype; eassumption | assumption]. + + (* T_Inl_L1 *) + - eapply T_Inl_L1. eapply IHHtype; eassumption. + + (* T_Inr_L1 *) + - eapply T_Inr_L1. eapply IHHtype; eassumption. + + (* T_Case_L1_Linear *) + - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + apply andb_prop in Hflam as [Hf01 Hf2]. + apply andb_prop in Hf01 as [Hf0 Hf1]. + eapply T_Case_L1_Linear. + + eapply IHHtype1; try eassumption. + intros rr Hrr. apply Hreg. apply in_app_iff. left. exact Hrr. + + rewrite (closed_value_shift_id_l1_m vv 1 Hclos). + eapply (IHHtype2 (S k0) Ta Tb R_in_v R_out_v vv u_mid); + simpl; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. + apply in_app_iff. left. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + rewrite (closed_value_shift_id_l1_m vv 1 Hclos). + eapply (IHHtype3 (S k0) Ta Tb R_in_v R_out_v vv u_mid); + simpl; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. + apply in_app_iff. right. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + (* T_Case_L1_Affine *) + - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + apply andb_prop in Hflam as [Hf01 Hf2]. + apply andb_prop in Hf01 as [Hf0 Hf1]. + eapply T_Case_L1_Affine. + + eapply IHHtype1; try eassumption. + intros rr Hrr. apply Hreg. apply in_app_iff. left. exact Hrr. + + rewrite (closed_value_shift_id_l1_m vv 1 Hclos). + eapply (IHHtype2 (S k0) Ta Tb R_in_v R_out_v vv u_mid); + simpl; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. + apply in_app_iff. left. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + rewrite (closed_value_shift_id_l1_m vv 1 Hclos). + eapply (IHHtype3 (S k0) Ta Tb R_in_v R_out_v vv u_mid); + simpl; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. + apply in_app_iff. right. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + (* T_If_L1_Linear *) + - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + apply andb_prop in Hflam as [Hf12 Hf3]. + apply andb_prop in Hf12 as [Hf1 Hf2]. + eapply T_If_L1_Linear. + + eapply IHHtype1; try eassumption. + intros rr Hrr. apply Hreg. apply in_app_iff. left. exact Hrr. + + eapply IHHtype2; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. + apply in_app_iff. left. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + eapply IHHtype3; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. + apply in_app_iff. right. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + (* T_If_L1_Affine *) + - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + apply andb_prop in Hflam as [Hf12 Hf3]. + apply andb_prop in Hf12 as [Hf1 Hf2]. + eapply T_If_L1_Affine. + + eapply IHHtype1; try eassumption. + intros rr Hrr. apply Hreg. apply in_app_iff. left. exact Hrr. + + eapply IHHtype2; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. + apply in_app_iff. left. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + eapply IHHtype3; try eassumption; try reflexivity. + * intros rr Hrr. apply Hreg. apply in_app_iff. right. + apply in_app_iff. right. exact Hrr. + * eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + eapply sub_R_in_R_in_via_value_l1_m; [exact Htype1 | exact Hval | exact Hv_type]. + + (* T_Region_L1: body's R = [r :: R]; P2 gives [r ∈ R_in_v] (since r + is the FIRST element of regions_introduced_by (ERegion r e)) and + Hv_type's inversion gives R ⊆ R_in_v; combined, (r :: R) ⊆ R_in_v. *) + - eapply T_Region_L1; [exact H | exact H0 | exact H1 |]. + eapply IHHtype; try eassumption; try reflexivity. + + intros r' Hr'. apply Hreg. right. exact Hr'. + + eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + intros r' Hr'. destruct Hr' as [-> | HrR]. + * apply Hreg. left. reflexivity. + * eapply value_TFunEff_R_subset_R_in_l1_m; + [exact Hval | exact Hv_type | exact HrR]. + + (* T_Region_Active_L1: body's R = outer R, no retype needed. *) + - eapply T_Region_Active_L1; [exact H | exact H0 | exact H1 |]. + eapply IHHtype; try eassumption; try reflexivity. + intros r' Hr'. apply Hreg. right. exact Hr'. + + (* T_Region_L1_Echo *) + - eapply T_Region_L1_Echo; [exact H | exact H0 | exact H1 |]. + eapply IHHtype; try eassumption; try reflexivity. + + intros r' Hr'. apply Hreg. right. exact Hr'. + + eapply closed_value_typing_RG_poly_l1_m; + [exact Hval | exact Hclos | exact Hv_type |]. + intros r' Hr'. destruct Hr' as [-> | HrR]. + * apply Hreg. left. reflexivity. + * eapply value_TFunEff_R_subset_R_in_l1_m; + [exact Hval | exact Hv_type | exact HrR]. + + (* T_Region_Active_L1_Echo *) + - eapply T_Region_Active_L1_Echo; [exact H | exact H0 | exact H1 |]. + eapply IHHtype; try eassumption; try reflexivity. + intros r' Hr'. apply Hreg. right. exact Hr'. + + (* T_Borrow_L1: EBorrow (EVar i) — if i = k0, substitute as EBorrow vv. *) + - destruct (Nat.eq_dec i k0) as [->|Hne]. + + simpl. rewrite Nat.eqb_refl. + assert (T = TFunEff Ta Tb R_in_v R_out_v) + by (unfold ctx_lookup in H; congruence). + subst T. + assert (u_out = u_in) by congruence; subst. + eapply T_Borrow_Val_L1. + * assumption. + * exact Hv_type. + + simpl. rewrite (proj2 (Nat.eqb_neq i k0) Hne). + assert (u_out = u_in) by congruence; subst. + destruct (Nat.ltb_spec k0 i) as [Hlt|Hge]. + * eapply T_Borrow_L1. unfold ctx_lookup. + rewrite nth_error_remove_at_ge by lia. + replace (S (i - 1)) with i by lia. + unfold ctx_lookup in H. exact H. + * assert (i < k0) by lia. eapply T_Borrow_L1. unfold ctx_lookup. + rewrite nth_error_remove_at_lt by lia. + unfold ctx_lookup in H. exact H. + + (* T_Borrow_Val_L1 *) + - assert (u_out = u_in) by congruence; subst. + eapply T_Borrow_Val_L1. + + apply subst_preserves_value. assumption. + + eapply IHHtype; eassumption. + + (* T_Drop_L1 *) + - eapply T_Drop_L1; [exact H |]. eapply IHHtype; eassumption. + + (* T_Drop_L1_Echo *) + - eapply T_Drop_L1_Echo; [exact H |]. eapply IHHtype; eassumption. + + (* T_Copy_L1 *) + - eapply T_Copy_L1; [exact H |]. eapply IHHtype; eassumption. + + (* T_Echo_L1 *) + - eapply T_Echo_L1. + + apply subst_preserves_value. assumption. + + eapply IHHtype; eassumption. + + (* T_Observe_L1 *) + - eapply T_Observe_L1. eapply IHHtype; eassumption. +Qed. + (** Linear-specialised wrapper preserving the original signature for [subst_preserves_typing_l1] and [preservation_l1]. *) Lemma subst_typing_gen_l1 : From 3413a728ff7e770a66a4e96676262732d07b2d31 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 20:16:09 +0100 Subject: [PATCH 4/4] =?UTF-8?q?feat(L2):=20Phase=203b=20Stage=201b=20?= =?UTF-8?q?=E2=80=94=20preservation=5Fl2=20=CE=B2-case=20for=20closed=20TF?= =?UTF-8?q?unEff=20substituents?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ships the L2-judgment half of Stage 1b. Closes the [T_App_L2_Eff] β-case for T1 = TFunEff Ta Tb R_in_v R_out_v under the three-condition statement (P1 leaf-only body + P2 regions ⊆ R_in_v + P3 closure of v2). Mirrors PR #228's [preservation_l2_app_eff_beta_linear] (Phase 4a, linear T1) and Phase 4b's [preservation_l2_app_eff_beta_ground_nonlinear] (ground-non-linear T1) structurally with the same `value_R_G_preserving_l1`-collapse pattern. Two Qed lemmas: - `preservation_l2_app_eff_beta_tfuneff_l1` — the L1-level kernel. Inverts the lambda derivation through `T_Lam_L1_Linear_Eff` / `T_Lam_L1_Affine_Eff`; collapses R_in = R1 = R and G'' = G' = G via `value_R_G_preserving_l1`; then defers to the substitution kernel `subst_typing_gen_l1_m_tfuneff` (Phase 3b Stage 1b, this branch's prior commit) at k = 0. - `preservation_l2_app_eff_beta_tfuneff` — the L2 wrapper. Inverts both `has_type_l2` hypotheses through `L2_lift_l1` (the `T_App_L2_Eff` cases discriminate via expression-shape mismatch), then defers to the L1 kernel and re-lifts via `L2_lift_l1`. Combined with PRs #228 (Phase 4a, linear T1) and #233 (Phase 4b, ground-non-linear T1), this closes the `T_App_L2_Eff` β-case for T1 ∈ {linear, ground-non-linear, TFunEff}. Phase 4d (compound non- linear EPair / EInl / EInr / EEcho) remains open at Phase 5. Print Assumptions verdict: - preservation_l2_app_eff_beta_tfuneff_l1: Closed under the global context - preservation_l2_app_eff_beta_tfuneff: Closed under the global context Zero new axioms. Zero new admits. The mechanised soundness-gap witnesses for the conditional form are preserved in: - Counterexample_L2.v (PR #234, Phase 4c) — fresh-region gap (the counterexample to dropping P2). - Counterexample_L2_nested.v (Stage 1a, this PR's predecessor #252) — nested-lambda gap (the counterexample to dropping P1). The two files together justify why Stage 1 ships the two-condition (plus P3 closure) statement rather than an unconditional version. Stage 4 (#242) achieves the unconditional form once the L4 annotation extension (#240) and CPS argument (#241) land — the proof content of this PR's `closed_value_typing_*` family is reused unchanged in Stage 4 as the closure-discharge kernel. Also: STATE.a2ml refreshed — last_action now records the full Stage 1b deliverable surface; next_action advances to Stages 2-4. Owner-directive compliance (CLAUDE.md 2026-05-27): - ✅ No touch to formal/Semantics.v / Typing.v / Counterexample.v. - ✅ No closure of residual Semantics_L1.v admits attempted. - ✅ Anti-pattern detector clean. - ✅ Strictly NEW infrastructure orthogonal to legacy. Refs: - ephapax issue #249 (Stage 1b tracking — closes via this PR). - ephapax PR #252 (Stage 1a prerequisite). - ephapax issue #239 (parent Stage 1; closes via #252 + this PR). - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b Stage 1b. Co-Authored-By: Claude Opus 4.7 (1M context) --- .machine_readable/6a2/STATE.a2ml | 6 +- formal/TypingL2.v | 119 +++++++++++++++++++++++++++++++ 2 files changed, 122 insertions(+), 3 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 380824c..b086ab2 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,9 +6,9 @@ @state(version="2.0"): phase: "implementation" -next_action: "Phase D slice 4 Phase 3b Stage 1b (sibling to #239 — file as follow-up sub-issue): implement the deferred substitution-lemma half. (a) `closed_value_typing_G_poly_l1_m` helper in `formal/Semantics_L1.v` (G-polymorphic retype for closed TFunEff values, addressing the structural blocker discovered in Stage 1a). (b) `subst_typing_gen_l1_m_tfuneff` Qed mirroring `subst_typing_gen_l1_m_ground_nonlinear` (~300 lines); inner T_Lam_L1_*_Eff cases exfalso via the `tfuneff_lambda_free` precondition; direct (P1, P2) hypothesis form (no CPS yet — Stage 3 introduces CPS). May add a third precondition `expr_closed_below 0 v = true` to handle the G-mismatch at compound binder rules; document as Stage 1 restriction lifted in Stage 3/4. (c) `preservation_l2_app_eff_beta_tfuneff_l1` + L2 wrapper Qed in `formal/TypingL2.v` under the 2-condition statement: `tfuneff_lambda_free ebody = true ∧ regions_introduced_by ebody ⊆ R_in_v`. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no closure of residual `Semantics_L1.v` admits — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority." -last_action: "Phase D slice 4 Phase 3b Stage 1a LANDED (2026-05-30 PM, this PR): mechanised soundness-gap witness + Stage 1 syntactic infrastructure. (1) `tfuneff_lambda_free : expr -> bool` Fixpoint added to `formal/Syntax.v` (conservative leaf-only predicate; `false` on every `ELam`, compositional `andb` propagation through compound forms). (2) `formal/Counterexample_L2_nested.v` — three Qed lemmas (`e_before_typed`, `e_step`, `e_after_untypable`) mechanising the nested-TFunEff soundness gap with `outer = ELam T_v (ELam (TBase TUnit) (EVar 1))` configuration where inner R_in_inner = [r2] but substituent R_in_v = []; e_after = ELam TUnit v fails to retype the body at `[r2] ⊄ [] = R_in_v`. (3) Wired into `_CoqProject` after `Counterexample_L2.v`. (4) `SUBST-LEMMA-GENERALIZATION-DESIGN.md` gained a 'Phase 3b Stage 1a (landed) — split from Stage 1' subsection inside the Phase 3b resolution section, documenting the Stage 1a / Stage 1b split and the structural blocker (G-mismatch at compound binder rules — `tfuneff_lambda_retype_l1_m` preserves G but IH expects post-e1 G' with different used-flags) that motivated the split. Stage 1b (substitution lemma + preservation_l2 wrapper) ships next session via a follow-up sub-issue. Build oracle: coqc 8.18.0 clean across all 12 .v files; Print Assumptions on all three new Qed lemmas reports 'Closed under the global context' (zero new admits/axioms). Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ no residual Semantics_L1.v admit closure attempted; ✅ anti-pattern detector clean. Sibling counterexample artifact to `Counterexample_L2.v` (PR #234) for the nested-lambda soundness-gap class; the two together justify the two-condition (P1 = `tfuneff_lambda_free`, P2 = `regions_introduced_by ⊆ R_in_v`) preservation_l2 statement Stage 1b delivers." -updated: 2026-05-30T00:00:00Z +next_action: "Phase D slice 4 Phase 3b Stages 2-4 (#240/#241/#242): Stage 1 (both 1a + 1b) complete. Stages 2-4 sequenced per the owner-approved 4-stage plan: Stage 2 (#240) ELam annotation extension — independent of Stage 1, ships when prioritised; Stage 3 (#241) CPS + relaxed Phase 3b — blocked on Stage 2; Stage 4 (#242) compound non-linear + unconditional preservation_l2 — blocked on Stage 3. Stage 4's destination collapses Stage 1b's three preconditions (P1 = tfuneff_lambda_free, P2 = regions_introduced_by ⊆ R_in_v, P3 = expr_closed_below 0 v) once typing-derived closure invariants land. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted`; no touching `Semantics.v` / `Typing.v` / `Counterexample.v`; no closure of residual `Semantics_L1.v` admits — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority." +last_action: "Phase D slice 4 Phase 3b Stage 1b LANDED (2026-05-30 PM, this PR): elegance-first path-(i) substitution-lemma + L2 β wrapper, zero axioms. (1) Syntax.v: `expr_closed_below : nat -> expr -> bool` Fixpoint (canonical CS predicate, bool per post-redesign convention); `closed_below_shift_id` (closed terms shift-invariant); `expr_closed_below_shift_mono` (closure survives shifting); `ctx_mark_used_app_lt` (mark_used commutes with context append). (2) Semantics_L1.v: `closed_below_k_typing_outer_tail_irrelevant_l1_m` (the body-transfer core — structural induction over 28+ typing rules; closed-below-k terms' typing depends only on G's first k positions); `closed_value_typing_G_poly_l1_m` (any-G' form per elegance-first 'state what's actually true'); `closed_value_typing_RG_poly_l1_m` (combined RG-poly via chain to tfuneff_lambda_retype_l1_m); `closed_value_shift_id_l1_m` (cutoff-0 wrapper); `value_TFunEff_R_subset_R_in_l1_m` (extracts R ⊆ R_in from TFunEff value typing); `sub_R_in_R_in_via_value_l1_m` (chain helper packaging count_occ_le_l1_m + R-subset for compound-rule call sites); `subst_typing_gen_l1_m_tfuneff` (~300 lines mirroring Phase 2's ground-nonlinear template; inner T_Lam_L1_*_Eff cases discharge via P1 discriminate; compound rules use closed_value_typing_RG_poly_l1_m + sub_R_in_R_in_via_value_l1_m for the G-mismatch). (3) TypingL2.v: `preservation_l2_app_eff_beta_tfuneff_l1` (β-case kernel) + `preservation_l2_app_eff_beta_tfuneff` (L2 wrapper) under the three-condition statement (P1 leaf-only + P2 regions ⊆ R_in_v + P3 closure of v2). Build oracle: coqc 8.18.0 clean across all 12 .v files; Print Assumptions on every new Qed lemma reports 'Closed under the global context' (zero new admits / axioms). Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ no residual Semantics_L1.v admit closure attempted; ✅ anti-pattern detector clean. Design decisions baked in per elegance-first priority: bool predicate (matches post-redesign style), any-G' statement form (the genuinely true claim), P1 RETAINED (re-staging is owner territory), staging-as-is (PR-level decisions don't deviate from owner-approved 4-stage plan)." +updated: 2026-05-30T20:00:00Z @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"): # Captured durable directive — preservation work is the four-layer redesign, diff --git a/formal/TypingL2.v b/formal/TypingL2.v index 5c5250c..04eb7bb 100644 --- a/formal/TypingL2.v +++ b/formal/TypingL2.v @@ -574,3 +574,122 @@ Proof. eapply preservation_l2_app_eff_beta_ground_nonlinear_l1; eassumption. - exfalso. inversion Hval. Qed. + +(** ===== Phase D slice 4 Phase 4c (Stage 1b) — β-case closure for + closed TFunEff substituents in leaf-only bodies ==================== + + Mirrors [preservation_l2_app_eff_beta_linear] (Phase 4a, PR #228) + and [preservation_l2_app_eff_beta_ground_nonlinear] (Phase 4b) + but uses [Semantics_L1.subst_typing_gen_l1_m_tfuneff] (Phase 3b + Stage 1b) for the L1 substitution step. Covers T1 = TFunEff Ta Tb + R_in_v R_out_v — TFunEff-typed function arguments. + + Two-condition statement (per ephapax issue #239's owner-approved + Stage 1 framing + Stage 1b's path-(i) closure precondition): + + - [tfuneff_lambda_free ebody = true] (P1): the OUTER lambda's body + [ebody] is leaf-only with respect to TFunEff-typed lambdas. + Stage 3 (#241) relaxes via CPS once [declared_lambda_r_ins ⊆ + R_in_v] becomes derivable from typing. + + - [(forall r, In r (regions_introduced_by ebody) -> In r R_in_v)] + (P2): every region introduced syntactically in [ebody] is + contained in the substituent's declared input env. + [Counterexample_L2.v] (PR #234) mechanises the soundness gap + this precondition rules out (fresh-region introduction + under a stale lambda capture). + + - [expr_closed_below 0 v2 = true] (P3): the substituent is + closed. Stage 4 (#242) replaces with a typing-derived + closure invariant. + + The mechanised soundness-gap witnesses for the conditional form + live in [Counterexample_L2.v] (fresh-region gap, the + counterexample to dropping P2) and [Counterexample_L2_nested.v] + (nested-lambda gap, the counterexample to dropping P1). The two + files together justify why Stage 1 ships the two-condition (plus + P3 closure) statement rather than an unconditional version — + Stage 4 (#242) achieves the unconditional form once the L4 + annotation extension (#240) and CPS argument (#241) land. + + Combined with PRs #228 (Phase 4a, linear T1) and #233 (Phase 4b, + ground-non-linear T1), this closes the [T_App_L2_Eff] β-case for + T1 ∈ {linear, ground-non-linear, TFunEff}. Phase 4d (compound + non-linear EPair / EInl / EInr / EEcho) remains open (Phase 5). + + Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 3b + Stage 1b, [PRESERVATION-DESIGN.md §5.1], ephapax issue #249, + ephapax issue #239 (parent Stage 1), [Counterexample_L2.v] + + [Counterexample_L2_nested.v] (mechanised soundness-gap witnesses). *) + +Lemma preservation_l2_app_eff_beta_tfuneff_l1 : + forall m R R1 G G' G'' v2 Ta Tb R_in_v R_out_v T2 R_in R_out ebody, + is_value v2 -> + tfuneff_lambda_free ebody = true -> + (forall r, In r (regions_introduced_by ebody) -> In r R_in_v) -> + expr_closed_below 0 v2 = true -> + TypingL1.has_type_l1 m R G (ELam (TFunEff Ta Tb R_in_v R_out_v) ebody) + (TFunEff (TFunEff Ta Tb R_in_v R_out_v) T2 R_in R_out) R1 G' -> + TypingL1.has_type_l1 m R1 G' v2 (TFunEff Ta Tb R_in_v R_out_v) 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 Ta Tb R_in_v R_out_v T2 R_in R_out ebody + Hval Hflam Hreg Hclos Hlam Harg. + inversion Hlam; subst. + - (* T_Lam_L1_Linear_Eff: body at R_in / (Tfun, false)::G'' + → R_out / (Tfun, true)::G''. Use value_R_G_preserving on Harg + to collapse R_in = R1 = R and G'' = G' = G. *) + destruct (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hval Harg) as [<- <-]. + eapply subst_typing_gen_l1_m_tfuneff with + (k := 0) (u_in := false) + (Gin := (TFunEff Ta Tb R_in_v R_out_v, false) :: G'') + (Gout := (TFunEff Ta Tb R_in_v R_out_v, true) :: G''). + + unfold ctx_extend in *. eassumption. + + reflexivity. + + exact Hval. + + exact Hflam. + + exact Hreg. + + exact Hclos. + + exact Harg. + + reflexivity. + - (* T_Lam_L1_Affine_Eff: body output is [(Tfun, u) :: G''] for some [u]. *) + destruct (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hval Harg) as [<- <-]. + eapply subst_typing_gen_l1_m_tfuneff with + (k := 0) (u_in := false) + (Gin := (TFunEff Ta Tb R_in_v R_out_v, false) :: G'') + (Gout := (TFunEff Ta Tb R_in_v R_out_v, _) :: G''). + + unfold ctx_extend in *. eassumption. + + reflexivity. + + exact Hval. + + exact Hflam. + + exact Hreg. + + exact Hclos. + + exact Harg. + + reflexivity. +Qed. + +(** L2-judgment wrapper for [preservation_l2_app_eff_beta_tfuneff_l1]. + + Inverts both [has_type_l2] hypotheses through [L2_lift_l1] (the + [T_App_L2_Eff] cases discriminate: the lambda's head is [ELam] + not [EApp], and the argument is a value so it cannot be [EApp]), + then defers to the L1 kernel and re-lifts via [L2_lift_l1]. *) +Lemma preservation_l2_app_eff_beta_tfuneff : + forall m R R1 G G' G'' v2 Ta Tb R_in_v R_out_v T2 R_in R_out ebody, + is_value v2 -> + tfuneff_lambda_free ebody = true -> + (forall r, In r (regions_introduced_by ebody) -> In r R_in_v) -> + expr_closed_below 0 v2 = true -> + has_type_l2 m R G (ELam (TFunEff Ta Tb R_in_v R_out_v) ebody) + (TFunEff (TFunEff Ta Tb R_in_v R_out_v) T2 R_in R_out) R1 G' -> + has_type_l2 m R1 G' v2 (TFunEff Ta Tb R_in_v R_out_v) 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 Ta Tb R_in_v R_out_v T2 R_in R_out ebody + Hval Hflam Hreg Hclos Hlam Harg. + inversion Hlam as [m0 R0 G0 e0 T0 R0' G0' Hlam_l1 | ]; subst. + inversion Harg as [m0' R0'' G0'' e0' T0' R0''' G0''' Harg_l1 | ]; subst. + - apply L2_lift_l1. + eapply preservation_l2_app_eff_beta_tfuneff_l1; eassumption. + - exfalso. inversion Hval. +Qed.