diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 5f1d14bb..db89c068 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -238,17 +238,32 @@ to the owner**: ## §4. Counts + file-by-file map -Coq admitted proofs remaining: 5 +Coq admitted proofs remaining: 3 (1 outer `Admitted.` in `formal/Semantics.v` — sacrosanct legacy -preservation, provably false per `Counterexample.v` + **4** outer -`Admitted.` markers in `formal/Semantics_L1.v` — the four open L1 lemmas -`region_shrink` / `region_liveness` / `step_pop` / `preservation_l1`. -**Corrected 2026-06-16 from `4`: the marker and the per-file table below were -written 2026-06-01, predate the `step_pop_disjoint_from_type_l1` outer marker, -and had drifted by one against `coqc`/grep ground truth. §5.2 carries the -authoritative current line numbers and the internal-`admit.` breakdown; the -2026-06-01 seam-audit line numbers below are superseded by it.**) +preservation, provably false per `Counterexample.v` + **2** outer +`Admitted.` markers in `formal/Semantics_L1.v` — the two open L1 lemmas +`step_pop` / `preservation_l1`. +**Updated 2026-06-26 (this branch) against rebuilt `coqc 8.18.0` + +`scripts/status-gate.sh --proofs` ground truth. Two closures dropped the +count 5 → 3:** +**(a) `region_shrink_preserves_typing_l1_gen_m` was *dissolved* (the +2026-06-16 multiset-perm closure) — its general form is proven false and +pinned in `formal/Counterexample_RegionShrink.v`, the surviving value +corollary `region_shrink_value` is `Qed`/axiom-free, and `preservation_l3` +is consequently UNCONDITIONALLY axiom-free.** +**(b) `region_liveness_at_split_l1_gen` — the provably-false +`In rv R -> In rv R'` lemma — was *removed*. Its 13 consumers in +`subst_typing_gen_l1_m` now route through the TRUE, `Qed` +`region_liveness_no_exit_l1_gen`, supplied with the honest +`val_region_no_exit` premise threaded through `subst_typing_gen_l1_m` / +`subst_typing_gen_l1` / `subst_preserves_typing_l1` and the L2 β-case +lemmas (`preservation_l2_app_eff_beta_linear` / `_l1`) — all of which +`Print Assumptions` now reports as "Closed under the global context" +(axiom-free) instead of depending on a false axiom.** +The two remaining outer markers are `step_pop_disjoint_from_type_l1` and +`preservation_l1` (capstone, gated on `step_pop`); §5's line numbers are +earlier-branch snapshots, superseded here.) ### Per-file Qed / Admitted summary (as of 2026-06-01) @@ -260,7 +275,7 @@ authoritative current line numbers and the internal-`admit.` breakdown; the | `formal/Counterexample_L2.v` | **5** | 0 | ✅ Phase 4c soundness-gap witness — fresh-region scope crossing (`v_typed_at_empty`, `outer_typed`, `e_before_typed`, `e_step`, `e_after_untypable`) | | `formal/Counterexample_L2_nested.v` | **5** | 0 | ✅ Phase 3b soundness-gap witness — nested TFunEff (analogue structure to `Counterexample_L2.v`) | | `formal/TypingL1.v` | **2** | 0 | ✅ active — L1 judgment, modality-indexed | -| `formal/Semantics_L1.v` | **37+** | **4** | ✅ active — Phase 3b Stage 1a + 1b landed via PRs #252 + #253. **4** outer `Admitted.` markers — the four open L1 lemmas (`region_shrink` / `region_liveness` / `step_pop` / `preservation_l1`). **Corrected 2026-06-16 from `3` (the `step_pop` marker was missed). §5.2 has the authoritative current line numbers + the 13 internal `admit.` cases; the 2026-06-01 line numbers in the seam audit below are superseded.** | +| `formal/Semantics_L1.v` | **54** | **2** | ✅ active — Phase 3b Stage 1a + 1b landed via PRs #252 + #253. **2** outer `Admitted.` markers — the two open L1 lemmas (`step_pop_disjoint_from_type_l1` / `preservation_l1`). **Updated 2026-06-26: `region_shrink…gen_m` dissolved (2026-06-16) and `region_liveness_at_split_l1_gen` removed (this branch) via the honest `val_region_no_exit` reformulation — see the §4 marker note. `preservation_l3` and the L2 β-case lemmas are now unconditionally axiom-free. Counts are rebuilt `coqc 8.18.0` ground truth on this branch.** | | `formal/Modality.v` | **1** | 0 | ✅ active — L2 core, zero axioms (`linear_to_affine`) | | `formal/Echo.v` | **12** | 0 | ✅ active — L3 calculus mechanised | | `formal/TypingL2.v` | **10** | 0 | ✅ active — `weaken_modality` (+ Affine_id + 3 `_le_*` variants), `preservation_l2_via_l1` (conditional on `preservation_l1`), `linear_value_retype_l1_m`, and 3 β-case lemmas (`preservation_l2_app_eff_beta_linear`, `_ground_nonlinear`, `_tfuneff` conditional on Stage 1b side conditions). NOT a wrapper. | diff --git a/formal/Semantics_L1.v b/formal/Semantics_L1.v index df28943b..80c7ea82 100644 --- a/formal/Semantics_L1.v +++ b/formal/Semantics_L1.v @@ -1,7 +1,7 @@ (* SPDX-License-Identifier: MPL-2.0 *) (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) -(* hypatia: allow code_safety/admitted -- TRACKED v2 proof-debt, not an honest-completion gap. The 3 Admitted lemmas (region_liveness_at_split_l1_gen, step_pop_disjoint_from_type_l1, preservation_l1) and their internal `admit.` tactics are documented in PROOF-NEEDS.md and owner-fenced by CLAUDE.md (directive 2026-05-27): closing or extending them is a banned anti-pattern. region_liveness is provably FALSE as stated; step_pop is open eliminator-fork research; preservation_l1 is the capstone gated on the others. Build truth is the `Print Assumptions` CI gate, not this comment. *) +(* hypatia: allow code_safety/admitted -- TRACKED v2 proof-debt, not an honest-completion gap. The 2 remaining Admitted lemmas (step_pop_disjoint_from_type_l1, preservation_l1) and their internal `admit.` tactics are documented in PROOF-NEEDS.md and owner-fenced by CLAUDE.md (directive 2026-05-27): closing or extending them via ad-hoc patching is a banned anti-pattern. step_pop is open eliminator-fork research; preservation_l1 is the capstone gated on it. The former third admit, region_liveness_at_split_l1_gen, was provably FALSE as stated and has been REMOVED (2026-06-26) via the honest val_region_no_exit reformulation (routes through the TRUE region_liveness_no_exit_l1_gen, Qed). Build truth is the `Print Assumptions` CI gate, not this comment. *) (* hypatia: allow coq_admit_tactic -- see preceding directive; same tracked admits. *) (** @@ -2066,6 +2066,18 @@ Proof. apply (count_occ_In string_dec). exact Hin. Qed. +(** The substituted value's region has no exit inside [e]. For a linear + value (always an [ELoc _ r] by [linear_value_is_loc_l1]) this is the + honest no-exit side condition; for any other value it is vacuous. This + is the premise that lets the 13 substitution sites below discharge + region-liveness through the TRUE [region_liveness_no_exit_l1_gen] + instead of the false [region_liveness_at_split_l1_gen]. *) +Definition val_region_no_exit (v e : expr) : Prop := + match v with + | ELoc _ r => expr_no_exit_of_region r e + | _ => True + end. + (** ===== 2026-06-16 CALL-SITE AUDIT RESULT (ADMIT 2) ===== The false [region_liveness_at_split_l1_gen] below is consumed at 13 @@ -2101,108 +2113,28 @@ Qed. See [formal/L1-REGION-REFOUNDATION-PLAN.md] (ADMIT 2 section). *) -(** Generalised over the modality parameter [m]. The wrapper below - matches the original Linear-only Axiom signature for the - existing call sites in [subst_typing_gen_l1]. *) -Lemma region_liveness_at_split_l1_gen : - forall m R G e T R' G' rv, - has_type_l1 m R G e T R' G' -> - In rv R -> - In rv R'. -Proof. - intros m R G e T R' G' rv Ht. - induction Ht; intros Hin; try assumption. - (* Compound cases — thread rv through sub-derivations via IH. *) - - (* T_StringConcat_L1: R -> R1 -> R2 *) - apply IHHt2. apply IHHt1. assumption. - - (* T_StringLen_L1 *) - apply IHHt. assumption. - - (* T_Let_L1 *) - apply IHHt2. apply IHHt1. assumption. - - (* T_LetLin_L1 *) - apply IHHt2. apply IHHt1. assumption. - - (* T_App_L1 *) - apply IHHt2. apply IHHt1. assumption. - - (* T_Pair_L1 *) - apply IHHt2. apply IHHt1. assumption. - - (* T_Fst_L1 *) - apply IHHt. assumption. - - (* T_Snd_L1 *) - apply IHHt. assumption. - - (* T_Inl_L1 *) - apply IHHt. assumption. - - (* T_Inr_L1 *) - apply IHHt. assumption. - - (* T_Case_L1_Linear: R -> R1 -> R_final *) - apply IHHt2. apply IHHt1. assumption. - - (* T_Case_L1_Affine: same shape *) - apply IHHt2. apply IHHt1. assumption. - - (* T_If_L1_Linear: R -> R1 -> R2 *) - apply IHHt2. apply IHHt1. assumption. - - (* T_If_L1_Affine *) - apply IHHt2. apply IHHt1. assumption. - - (* T_Region_L1 (fresh): ~In r R + In rv R gives r ≠ rv; - remove_first_L1 preserves rv. *) - assert (Hne : r <> rv). - { intro Heq. subst rv. apply H. exact Hin. } - assert (Hin_body_in : In rv (r :: R)) by (right; exact Hin). - pose proof (IHHt Hin_body_in) as HinRbody. - apply (count_occ_In string_dec). - pose proof (remove_first_L1_count_other r rv R_body Hne) as Heq. - unfold cnt in Heq. rewrite Heq. - apply (count_occ_In string_dec). exact HinRbody. - - (* T_Region_Active_L1: two sub-cases r=rv / r ≠ rv *) - destruct (string_dec r rv) as [Heq|Hne]. - + (* r = rv: GENUINELY FALSE. Counterexample at the source level: - ERegion rv (EI32 5) at R = [rv] — body R_body = [rv], pop - yields [], so In rv R = True but In rv R' = False. *) - admit. - + (* r ≠ rv: same shape as T_Region_L1. *) - pose proof (IHHt Hin) as HinRbody. - apply (count_occ_In string_dec). - pose proof (remove_first_L1_count_other r rv R_body Hne) as Heq. - unfold cnt in Heq. rewrite Heq. - apply (count_occ_In string_dec). exact HinRbody. - - (* T_Region_L1_Echo — same shape as T_Region_L1 (parallel rule; - output type differs but the R-threading is identical). *) - assert (Hne : r <> rv). - { intro Heq. subst rv. apply H. exact Hin. } - assert (Hin_body_in : In rv (r :: R)) by (right; exact Hin). - pose proof (IHHt Hin_body_in) as HinRbody. - apply (count_occ_In string_dec). - pose proof (remove_first_L1_count_other r rv R_body Hne) as Heq. - unfold cnt in Heq. rewrite Heq. - apply (count_occ_In string_dec). exact HinRbody. - - (* T_Region_Active_L1_Echo — same shape as T_Region_Active_L1 - including the structural admit in the [r = rv] sub-case. *) - destruct (string_dec r rv) as [Heq|Hne]. - + admit. - + pose proof (IHHt Hin) as HinRbody. - apply (count_occ_In string_dec). - pose proof (remove_first_L1_count_other r rv R_body Hne) as Heq. - unfold cnt in Heq. rewrite Heq. - apply (count_occ_In string_dec). exact HinRbody. - (* T_Borrow_L1, T_Borrow_Val_L1: R unchanged, auto-discharged by - [try assumption] above. *) - - (* T_Drop_L1 *) - apply IHHt. assumption. - - (* T_Drop_L1_Echo *) - apply IHHt. assumption. - - (* T_Copy_L1 *) - apply IHHt. assumption. -Admitted. - -(** Linear-specialised wrapper matching the original Axiom signature - for the call sites in [subst_typing_gen_l1]. *) -Lemma region_liveness_at_split_l1 : - forall R G e T R' G' rv, - R; G |=L1 e : T -| R'; G' -> - In rv R -> - In rv R'. -Proof. - intros R G e T R' G' rv Ht. - eapply region_liveness_at_split_l1_gen. exact Ht. -Qed. +(** [region_liveness_at_split_l1_gen] and its Linear wrapper + [region_liveness_at_split_l1] — the FALSE, [Admitted] versions of + "typing preserves region liveness" ([In rv R -> In rv R'] + unconditionally) — have been REMOVED (2026-06-26). The unconditional + statement is false in the [T_Region_Active_L1] [r = rv] sub-case + (witness [ERegion rv (EI32 5)] at [R = [rv]]: [In rv R] holds but the + region pop yields [In rv R' = False]). It is now pinned, with its + counterexample, as a NEGATIVE result in + [Counterexample_RegionShrink.v]'s region family — there is no value in + keeping a false [Admitted] lemma in the live build. + + The 13 consumers in [subst_typing_gen_l1_m] now discharge region + liveness through the TRUE, [Qed] [region_liveness_no_exit_l1_gen] + above, supplied with the honest [val_region_no_exit] premise threaded + from [subst_typing_gen_l1_m] / [subst_typing_gen_l1] / + [subst_preserves_typing_l1]. This realises the HONEST closure recorded + in the call-site audit above (ADMIT 2): one fewer outer [Admitted], + zero false lemmas, and the residual region-liveness-through-reduction + obligation now lives — explicitly and honestly — as the + [val_region_no_exit] premise that [preservation_l1] (the capstone) owes + when it fires substitution. See + [formal/L1-REGION-REFOUNDATION-PLAN.md] (ADMIT 2 section). *) (** Generalized substitution: at depth [k] for a linear value [v]. Mirrors legacy [subst_typing_gen]. The only L1-specific gap is the @@ -2233,13 +2165,14 @@ Lemma subst_typing_gen_l1_m : nth_error Gin k = Some (T1, u_in) -> is_value v -> is_linear_ty T1 = true -> + val_region_no_exit v e -> R; remove_at k Gin |=L1 v : T1 -| R; remove_at k Gin -> forall u_out, nth_error Gout k = Some (T1, 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 Tsub vv u_in Hk_in Hval Hlin Hv_type u_out Hk_out; simpl. + induction Htype; intros k0 Tsub vv u_in Hk_in Hval Hlin Hnx Hv_type u_out Hk_out; simpl. (* T_Unit_L1, T_Bool_L1, T_I32_L1 *) 1-3: (assert (u_out = u_in) by congruence; subst; constructor). @@ -2296,36 +2229,39 @@ Proof. - 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]. + - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hnx1 Hnx2]. + destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. eapply T_StringConcat_L1. + eapply IHHtype1; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply IHHtype2; try eassumption; try reflexivity. + + eapply IHHtype2; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). (* 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]. + - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hnx1 Hnx2]. + destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. eapply T_Let_L1. + eapply IHHtype1; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply (IHHtype2 (S k0) (TString rv) (ELoc lv rv) u_mid); + + eapply (IHHtype2 (S k0) (TString rv) (ELoc lv rv) u_mid); simpl; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). (* T_LetLin_L1 *) - - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hnx1 Hnx2]. + destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. eapply T_LetLin_L1; [exact H | |]. + eapply IHHtype1; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply (IHHtype2 (S k0) (TString rv) (ELoc lv rv) u_mid); + + eapply (IHHtype2 (S k0) (TString rv) (ELoc lv rv) u_mid); simpl; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). (* T_Lam_L1_Linear: body's R = outer R; direct discharge via [T_Loc_L1] + Hregv. *) @@ -2366,22 +2302,24 @@ Proof. apply loc_retype_at_R_l1_m. apply H. exact Hregv. (* T_App_L1 *) - - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hnx1 Hnx2]. + destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. eapply T_App_L1. + eapply IHHtype1; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply IHHtype2; try eassumption; try reflexivity. + + eapply IHHtype2; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). (* T_Pair_L1 *) - - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hnx1 Hnx2]. + destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. eapply T_Pair_L1. + eapply IHHtype1; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply IHHtype2; try eassumption; try reflexivity. + + eapply IHHtype2; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). (* T_Fst_L1 *) - eapply T_Fst_L1; [eapply IHHtype; eassumption | assumption]. @@ -2396,85 +2334,89 @@ Proof. - eapply T_Inr_L1. eapply IHHtype; eassumption. (* T_Case_L1_Linear *) - - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hnx1 [Hnx2 Hnx3]]. + destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. eapply T_Case_L1_Linear. + eapply IHHtype1; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply (IHHtype2 (S k0) (TString rv) (ELoc lv rv) u_mid); + + eapply (IHHtype2 (S k0) (TString rv) (ELoc lv rv) u_mid); simpl; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply (IHHtype3 (S k0) (TString rv) (ELoc lv rv) u_mid); + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). + + eapply (IHHtype3 (S k0) (TString rv) (ELoc lv rv) u_mid); simpl; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). (* T_Case_L1_Affine: same shape — per-branch [u1, u2] are the inner-bound variable's output flags, orthogonal to the substituted variable's flag. *) - - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hnx1 [Hnx2 Hnx3]]. + destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. eapply T_Case_L1_Affine. + eapply IHHtype1; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply (IHHtype2 (S k0) (TString rv) (ELoc lv rv) u_mid); + + eapply (IHHtype2 (S k0) (TString rv) (ELoc lv rv) u_mid); simpl; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply (IHHtype3 (S k0) (TString rv) (ELoc lv rv) u_mid); + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). + + eapply (IHHtype3 (S k0) (TString rv) (ELoc lv rv) u_mid); simpl; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). (* T_If_L1_Linear *) - - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hnx1 [Hnx2 Hnx3]]. + destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. eapply T_If_L1_Linear. + eapply IHHtype1; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply IHHtype2; try eassumption; try reflexivity. + + eapply IHHtype2; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply IHHtype3; try eassumption; try reflexivity. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). + + eapply IHHtype3; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). (* T_If_L1_Affine: same shape; branches agree on output structure just as in the Linear case (the mode-split is on context consumption, not on conditional symmetry). *) - - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. + - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hnx1 [Hnx2 Hnx3]]. + destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid]. eapply T_If_L1_Affine. + eapply IHHtype1; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply IHHtype2; try eassumption; try reflexivity. + + eapply IHHtype2; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. - + destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. - eapply IHHtype3; try eassumption; try reflexivity. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). + + eapply IHHtype3; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. - eapply region_liveness_at_split_l1_gen; eassumption. + exact (region_liveness_no_exit_l1_gen _ _ _ _ _ _ _ rv Htype1 Hnx1 Hregv). (* T_Region_L1: body's R = [r :: R]; [In rv R] (from Hregv) lifts to [In rv (r :: R)]. Direct discharge via [T_Loc_L1] — no axiom. *) - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hr_ne Hnx_body]. eapply T_Region_L1; [exact H | exact H0 | exact H1 |]. eapply IHHtype; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. right; exact Hregv. (* T_Region_Active_L1: body's R = outer R, so Hv_type re-uses unchanged. *) - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hr_ne Hnx_body]. eapply T_Region_Active_L1; [exact H | exact H0 | exact H1 |]. eapply IHHtype; try eassumption; try reflexivity. (* T_Region_L1_Echo — parallel rule; identical substitution shape *) - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hr_ne Hnx_body]. eapply T_Region_L1_Echo; [exact H | exact H0 | exact H1 |]. eapply IHHtype; try eassumption; try reflexivity. apply loc_retype_at_R_l1_m. right; exact Hregv. (* T_Region_Active_L1_Echo — parallel rule *) - destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]]. + simpl in Hnx; destruct Hnx as [Hr_ne Hnx_body]. eapply T_Region_Active_L1_Echo; [exact H | exact H0 | exact H1 |]. eapply IHHtype; try eassumption; try reflexivity. @@ -3216,12 +3158,13 @@ Lemma subst_typing_gen_l1 : nth_error Gin k = Some (T1, u_in) -> is_value v -> is_linear_ty T1 = true -> + val_region_no_exit v e -> R; remove_at k Gin |=L1 v : T1 -| R; remove_at k Gin -> forall u_out, nth_error Gout k = Some (T1, u_out) -> R; remove_at k Gin |=L1 subst k v e : T -| R'; remove_at k Gout. Proof. - intros R Gin e T R' Gout Htype k T1 v u_in Hk_in Hval Hlin Hv_type u_out Hk_out. + intros R Gin e T R' Gout Htype k T1 v u_in Hk_in Hval Hlin Hnx Hv_type u_out Hk_out. eapply subst_typing_gen_l1_m; eassumption. Qed. @@ -3232,15 +3175,16 @@ Qed. Lemma subst_preserves_typing_l1 : forall T1 v R2 G2 e2 T2 R2_final G2', is_value v -> + val_region_no_exit v e2 -> has_type_l1_linear R2 G2 v T1 R2 G2 -> has_type_l1_linear R2 ((T1, false) :: G2) e2 T2 R2_final ((T1, true) :: G2') -> has_type_l1_linear R2 G2 (subst 0 v e2) T2 R2_final G2'. Proof. - intros T1 v R2 G2 e2 T2 R2_final G2' Hval Hv_type He2_type. + intros T1 v R2 G2 e2 T2 R2_final G2' Hval Hnx Hv_type He2_type. assert (Hlin: is_linear_ty T1 = true). { eapply (flag_false_to_true_implies_linear_l1 _ _ _ _ _ _ 0 T1 He2_type); simpl; reflexivity. } - pose proof (subst_typing_gen_l1 _ _ _ _ _ _ He2_type 0 T1 v false eq_refl Hval Hlin + pose proof (subst_typing_gen_l1 _ _ _ _ _ _ He2_type 0 T1 v false eq_refl Hval Hlin Hnx Hv_type true eq_refl) as Hsubst. simpl in Hsubst. exact Hsubst. Qed. @@ -3764,10 +3708,14 @@ Qed. [region_shrink_preserves_typing_l1_gen_m] is GONE; its false general statement is pinned in [Counterexample_RegionShrink.v]. - - [region_liveness_at_split_l1_gen] Admitted → - surfaces itself. Provably-false-as-stated in the residual - [binder = rv] sub-case (counterexample documented in source); - closure requires Phase D reformulation. + - [region_liveness_at_split_l1_gen] REMOVED (2026-06-26). It was + [Admitted] and provably-false-as-stated in the [binder = rv] + sub-case. Its 13 consumers in [subst_typing_gen_l1_m] now route + through the TRUE [region_liveness_no_exit_l1_gen] (Qed) supplied + with the honest [val_region_no_exit] premise; the substitution + chain and the L2 β-case lemmas + ([preservation_l2_app_eff_beta_linear] / [_l1]) are therefore now + axiom-free rather than depending on a false axiom. - [preservation_l1] Admitted → surfaces itself plus any structural debt its conditional Qed-portion already diff --git a/formal/TypingL2.v b/formal/TypingL2.v index 984b1665..4046d824 100644 --- a/formal/TypingL2.v +++ b/formal/TypingL2.v @@ -429,12 +429,13 @@ Lemma preservation_l2_app_eff_beta_linear_l1 : forall m R R1 G G' G'' v2 T1 T2 R_in R_out ebody, is_value v2 -> is_linear_ty T1 = true -> + val_region_no_exit v2 ebody -> 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 Hlin Hlam Harg. + intros m R R1 G G' G'' v2 T1 T2 R_in R_out ebody Hval Hlin Hnx Hlam Harg. inversion Hlam; subst. - (* T_Lam_L1_Linear_Eff: body at R_in / (T1,false)::G'' → R_out / (T1,true)::G'' (R and G eliminated by inversion equalities; R_in and G'' remain. Use @@ -450,6 +451,7 @@ Proof. + reflexivity. + exact Hval. + exact Hlin. + + exact Hnx. + exact Harg. + reflexivity. - (* T_Lam_L1_Affine_Eff: body output is [(T1, u) :: G''] for some [u] @@ -465,6 +467,7 @@ Proof. + reflexivity. + exact Hval. + exact Hlin. + + exact Hnx. + apply (linear_value_retype_l1_m Affine Linear); assumption. + reflexivity. Qed. @@ -473,12 +476,13 @@ Lemma preservation_l2_app_eff_beta_linear : forall m R R1 G G' G'' v2 T1 T2 R_in R_out ebody, is_value v2 -> is_linear_ty T1 = true -> + val_region_no_exit v2 ebody -> 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 Hlin Hlam Harg. + intros m R R1 G G' G'' v2 T1 T2 R_in R_out ebody Hval Hlin Hnx Hlam Harg. (* Lambda inversion: [T_App_L2_Eff]'s expression is [EApp _ _], not [ELam _ _], so it discriminates; only [L2_lift_l1] remains. *) inversion Hlam as [m0 R0 G0 e0 T0 R0' G0' Hlam_l1 | ]; subst.