|
| 1 | +<!-- SPDX-License-Identifier: PMPL-1.0-or-later --> |
| 2 | +<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell --> |
| 3 | + |
| 4 | +# Design: generalising `subst_typing_gen_l1_m` to non-linear `T1` |
| 5 | + |
| 6 | +**Date**: 2026-05-28 |
| 7 | +**Author**: session 8 (Phase D slice 4 — preservation_l2 follow-on) |
| 8 | +**Status**: design only; no code lands in this doc's PR |
| 9 | + |
| 10 | +## TL;DR |
| 11 | + |
| 12 | +The β-case for `T_App_L2_Eff` in `preservation_l2` (`formal/TypingL2.v`) requires substituting a value into a lambda body when the lambda parameter type `T1` is **non-linear**. The existing substitution lemma `subst_typing_gen_l1_m` (`formal/Semantics_L1.v:1358`) carries an `is_linear_ty T1 = true` precondition that blocks this. Generalising it is more complex than a "sibling lemma with `false` instead of `true`" — it interacts with **body-R-rigidity** for non-linear `ELam` values. This document captures the analysis, identifies the sub-problems, and recommends a phased approach. |
| 13 | + |
| 14 | +## Why this matters |
| 15 | + |
| 16 | +`T_App_L2_Eff` (`formal/TypingL2.v:111`, PR #209) is the L2 elimination form for effect-typed lambdas. Closing `preservation_l2` over `has_type_l2` requires handling its β-reduction case (`S_App_Fun`). After inversion through `L2_lift_l1` + `T_Lam_L1_*_Eff` and applying `value_R_G_preserving_l1` to the argument value, the residual obligation is exactly: |
| 17 | + |
| 18 | +```coq |
| 19 | +has_type_l1 m R G v T1 R G -> |
| 20 | +has_type_l1 m R ((T1, false) :: G) ebody T2 R_out ((T1, true) :: G) -> |
| 21 | +is_value v -> |
| 22 | +has_type_l1 m R G (subst 0 v ebody) T2 R_out G |
| 23 | +``` |
| 24 | + |
| 25 | +This is the signature of `subst_typing_gen_l1_m` at `k = 0`, EXCEPT for the linearity precondition. For non-linear `T1` (any of `TUnit`, `TBool`, `TI32`, `TFun T1' T2'`, `TFunEff T1' T2' R_in' R_out'`, `TProd …` with non-linear components, `TSum …` with overall non-linear, `TRef Unr _`, `TEcho T'`), the existing lemma cannot fire. |
| 26 | + |
| 27 | +## What `subst_typing_gen_l1_m` actually does with `is_linear_ty T1 = true` |
| 28 | + |
| 29 | +Read of `Semantics_L1.v:1358-1656`. Two distinct uses of `Hlin`: |
| 30 | + |
| 31 | +### Use A: `linear_value_is_loc_l1` to extract canonical location form |
| 32 | + |
| 33 | +In ~20 of the proof's 28 cases, the tactic pattern is: |
| 34 | + |
| 35 | +```coq |
| 36 | +destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) |
| 37 | + as [lv [rv [-> [-> Hregv]]]]. |
| 38 | +``` |
| 39 | + |
| 40 | +`linear_value_is_loc_l1` requires `is_linear_ty T = true` to conclude `v = ELoc l r ∧ T = TString r ∧ In r R`. This canonical form lets subsequent reasoning: |
| 41 | +- Treat `v` as a location (so substitution into typing positions becomes "introduce a location at the right region"). |
| 42 | +- Use `loc_retype_at_R_l1_m` to lift the location's typing across R-shifts within `ebody`'s recursion. |
| 43 | + |
| 44 | +For non-linear values, this canonical-form extraction has no analogue: |
| 45 | +- `EUnit` / `EBool` / `EI32` have trivial R-irrelevance (T_Unit_L1 / T_Bool_L1 / T_I32_L1 type them at any R). |
| 46 | +- `ELam` has body-R-rigidity (the lambda's body is typed at a fixed R determined at lambda formation). |
| 47 | +- `EPair` / `EInl` / `EInr` are R-relevant if any sub-component is R-relevant. |
| 48 | +- `EBorrow` of a location is R-relevant. |
| 49 | + |
| 50 | +### Use B: contradiction discharge in `T_Var_Unr_L1` |
| 51 | + |
| 52 | +`Semantics_L1.v:1409`: |
| 53 | +```coq |
| 54 | +exfalso. unfold ctx_lookup in H. rewrite Hk_in in H. |
| 55 | +injection H as <- <-. rewrite Hlin in H0. discriminate. |
| 56 | +``` |
| 57 | + |
| 58 | +When the substituted variable position `k0` is the same as the variable being typed AND the variable is typed via T_Var_Unr_L1 (unrestricted), the rule's `is_linear_ty T = false` premise contradicts `Hlin : is_linear_ty T1 = true` (since they refer to the same type). The case is vacuous. |
| 59 | + |
| 60 | +For non-linear `T1`, this case is **not vacuous** — it's the actual substitution case: substituting an unrestricted value into an unrestricted variable position. The proof structure must handle it constructively rather than discharge by contradiction. |
| 61 | + |
| 62 | +## The body-R-rigidity issue (the real obstacle) |
| 63 | + |
| 64 | +For the recursive cases in `subst_typing_gen_l1_m` (e.g. `T_App_L1`, `T_Pair_L1`, `T_Let_L1`), the IH on each sub-expression needs `Hv_type` at the **sub-expression's** input R, which may differ from the outer R due to region operations inside `ebody`. |
| 65 | + |
| 66 | +For linear values (locations), the existing proof lifts `Hv_type` across R-shifts via: |
| 67 | +```coq |
| 68 | +apply loc_retype_at_R_l1_m. eapply region_liveness_at_split_l1_gen; ... |
| 69 | +``` |
| 70 | +or |
| 71 | +```coq |
| 72 | +apply loc_retype_at_R_l1_m. right; exact Hregv. |
| 73 | +``` |
| 74 | + |
| 75 | +The `loc_retype_at_R_l1_m` lemma re-types an `ELoc` at any `R` that contains the location's region. The corresponding non-linear-value retype lemma is more nuanced: |
| 76 | + |
| 77 | +| Value | Retype across R-shift `R → R'`? | |
| 78 | +|---|---| |
| 79 | +| `EUnit` / `EBool` / `EI32` | ✅ Trivial (R-irrelevant) | |
| 80 | +| `ELoc l r` | ❌ Always linear; outside non-linear scope | |
| 81 | +| `ELam T e` (TFun T1 T2) | ❌ Body typed at fixed R; retype requires body-R-shift | |
| 82 | +| `ELam T e` (TFunEff T1 T2 R_in R_out) | ⚠️ Body typed at R_in (independent of outer R); retype works if R' still satisfies `forall r, In r R' -> In r R_in` | |
| 83 | +| `EPair v1 v2` | ⚠️ Inherits from components | |
| 84 | +| `EInl T v` / `EInr T v` | ⚠️ Inherits from `v` | |
| 85 | +| `EBorrow (ELoc l r)` | ❌ Inherits R-dependence from `ELoc` | |
| 86 | +| `EEcho T v` | ⚠️ Inherits from `v` | |
| 87 | + |
| 88 | +The ❌ rows mean a fully general `nonlinear_value_retype_at_R_l1_m` lemma is **false** in the unrestricted case — specifically, `TFun` lambdas have body-R-rigidity (the same gap that blocks legacy `preservation_l1` per `Semantics_L1.v:1708-1713`). |
| 89 | + |
| 90 | +## What this means for the lemma's scope |
| 91 | + |
| 92 | +The clean non-linear substitution lemma cannot cover all non-linear `T1`. The categories that **do** admit a clean lemma: |
| 93 | + |
| 94 | +1. **Ground non-linear values** (`EUnit`, `EBool`, `EI32`): trivially R-irrelevant. A retype lemma `ground_nonlinear_retype_l1_m` is Qed-able in ~10 lines. |
| 95 | + |
| 96 | +2. **TFunEff lambdas** (`ELam T e` typed at `TFunEff T1 T2 R_in R_out`): R'-retype works under the side condition `forall r, In r R' -> In r R_in`. The lambda value's typing rule `T_Lam_L1_*_Eff` already requires this side condition at formation; preserving it across retype is a one-line obligation. |
| 97 | + |
| 98 | +The categories that **do not** admit a clean lemma: |
| 99 | + |
| 100 | +3. **TFun lambdas** (legacy `T_Lam_L1_Linear` / `T_Lam_L1_Affine`): body-R-rigid. Same gap as legacy `preservation_l1` slice 4b. |
| 101 | + |
| 102 | +4. **EBorrow of a location**: inherits linear R-dependence; the borrow doesn't reduce R-dependence. |
| 103 | + |
| 104 | +5. **Compound values with R-dependent sub-components**: inherit from sub-components. |
| 105 | + |
| 106 | +## Recommended phasing |
| 107 | + |
| 108 | +### Phase 1 (next session): ship `ground_nonlinear_retype_l1_m` |
| 109 | + |
| 110 | +A 10-line lemma covering `EUnit` / `EBool` / `EI32`. Qed-able trivially. Useful in its own right (any β-reduction with `T1 ∈ {TUnit, TBool, TI32}` becomes closeable). |
| 111 | + |
| 112 | +```coq |
| 113 | +Lemma ground_nonlinear_retype_l1_m : |
| 114 | + forall m R R' G v T, |
| 115 | + is_value v -> |
| 116 | + is_ground_nonlinear_ty T = true -> (* new predicate; TUnit/TBool/TI32 only *) |
| 117 | + has_type_l1 m R G v T R G -> |
| 118 | + has_type_l1 m R' G v T R' G. |
| 119 | +``` |
| 120 | + |
| 121 | +Where `is_ground_nonlinear_ty` is a new predicate: |
| 122 | +```coq |
| 123 | +Definition is_ground_nonlinear_ty (T : ty) : bool := |
| 124 | + match T with |
| 125 | + | TUnit | TBool | TI32 => true |
| 126 | + | _ => false |
| 127 | + end. |
| 128 | +``` |
| 129 | + |
| 130 | +### Phase 2: ship `subst_typing_gen_l1_m_ground_nonlinear` |
| 131 | + |
| 132 | +A parallel substitution lemma for ground non-linear types. Uses `ground_nonlinear_retype_l1_m` in place of `loc_retype_at_R_l1_m` in the cases that need R-shift retyping. |
| 133 | + |
| 134 | +Structure mirrors `subst_typing_gen_l1_m`'s 28 cases. Crucially: |
| 135 | +- `T_Var_Lin_L1` with `i = k0`: **exfalso** via `is_linear_ty T1 = false` vs T_Var_Lin_L1's `is_linear_ty T = true` premise. |
| 136 | +- `T_Var_Unr_L1` with `i = k0`: **constructive**; apply `Hv_type` directly. |
| 137 | +- Compound cases: use `ground_nonlinear_retype_l1_m` for R-shift retypes. |
| 138 | + |
| 139 | +Estimated ~250-300 lines, paralleling the existing proof. |
| 140 | + |
| 141 | +### Phase 3: ship `tfuneff_lambda_retype_l1_m` + extend substitution |
| 142 | + |
| 143 | +Add a retype lemma for TFunEff lambdas (under R' ⊆ R_in side condition). Extend the substitution lemma to cover `T1 = TFunEff …` lambdas as substituends. This is the case actually needed for higher-order β-reductions where the lambda parameter is itself a function type. |
| 144 | + |
| 145 | +### Phase 4: close `preservation_l2` β-case using Phases 1-3 |
| 146 | + |
| 147 | +With the substitution machinery in place, the T_App_L2_Eff β-case in `preservation_l2` closes by: |
| 148 | +1. Inversion on the L2 derivation → L1 derivation of `T_Lam_L1_*_Eff`. |
| 149 | +2. Inversion on the L1 derivation → body typing at R_in + side condition. |
| 150 | +3. Apply `value_R_G_preserving_l1` to argument value → R_in = R, G'' = G. |
| 151 | +4. Case-split on `is_linear_ty T1`: |
| 152 | + - Linear: use existing `subst_typing_gen_l1_m`. |
| 153 | + - Ground non-linear: use Phase 2 lemma. |
| 154 | + - TFunEff non-linear: use Phase 3 lemma. |
| 155 | + - Other non-linear: deferred (compound values; see Phase 5). |
| 156 | +5. `L2_lift_l1` wrap. |
| 157 | + |
| 158 | +### Phase 5 (deferred): compound non-linear values |
| 159 | + |
| 160 | +`EPair` / `EInl` / `EInr` / `EEcho` of non-linear components. Sub-component analysis. May require additional retype machinery. Realistically multiple sessions of work. |
| 161 | + |
| 162 | +## What this session ships |
| 163 | + |
| 164 | +This design document only. No code changes. STATE.a2ml shifts `next_action` to "Phase 1: implement `ground_nonlinear_retype_l1_m` per `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`". |
| 165 | + |
| 166 | +## Owner-directive compliance check |
| 167 | + |
| 168 | +Per `CLAUDE.md` 2026-05-27: |
| 169 | + |
| 170 | +- ✅ Does not propose closing legacy `preservation` in `Semantics.v` (provably false). |
| 171 | +- ✅ Does not extend `Semantics.v` with closure-support lemmas. |
| 172 | +- ✅ Does not close residual `Semantics_L1.v` axioms via proof tricks — Phase 1-2 add NEW infrastructure to `Semantics_L1.v` orthogonal to legacy admits. |
| 173 | +- ✅ Does not follow pre-2026-05-26 closure plans. |
| 174 | +- ✅ Does not patch legacy `Typing.v`. |
| 175 | +- ✅ Reads `PRESERVATION-DESIGN.md` first (specifically §5.1 lines 468-474 — the L1-intro / L2-elim design vision endorsing T_App_L2_Eff at L2). |
| 176 | +- ✅ Works per-layer (L1 infrastructure → L2 preservation closure). |
| 177 | +- ✅ Escalates before patching (this design doc IS the escalation). |
| 178 | + |
| 179 | +Anti-pattern detector (per `CLAUDE.md` §"Anti-pattern detector"): |
| 180 | + |
| 181 | +- ✅ No sibling-region-disjointness side conditions proposed. |
| 182 | +- ✅ No region-weakening predicates indexed on syntactic shape (the proposed retype lemmas are indexed on TYPE shape, not syntactic shape — `is_ground_nonlinear_ty` is a type predicate). |
| 183 | +- ✅ No admit-shuffling between `Semantics.v` and a new lemma. |
| 184 | +- ✅ No proposal to close `Theorem preservation` in `Semantics.v` to `Qed.`. |
| 185 | +- ✅ No new `Axiom` declarations. |
| 186 | + |
| 187 | +## Open design questions for owner |
| 188 | + |
| 189 | +1. **`is_ground_nonlinear_ty` predicate placement**: `Syntax.v` (near `is_linear_ty`) or `Semantics_L1.v` (near the lemma that uses it)? Recommendation: `Syntax.v` for symmetry with `is_linear_ty`. |
| 190 | + |
| 191 | +2. **Phase 3 scope**: TFunEff lambdas only, or also TFun lambdas with the body-R-rigidity gap honestly admitted? Recommendation: TFunEff only (TFun is the legacy slice 4b debt; not in scope for this initiative). |
| 192 | + |
| 193 | +3. **Phase 5 priority**: should compound non-linear values block `preservation_l2` closure, or can `preservation_l2` Qed with the compound-value case admitted? Recommendation: defer Phase 5; `preservation_l2` can close conditionally on a `nonlinear_compound_substitutable T` predicate that returns true for ground + TFunEff and false otherwise. The predicate's `true` cases let preservation_l2 fire; the `false` cases vacuously discharge or admit at the predicate-false branch. |
| 194 | + |
| 195 | +4. **Sibling vs case-split**: Phase 2 ships as a parallel lemma (`subst_typing_gen_l1_m_ground_nonlinear`) rather than folding case-split into the existing lemma. Avoids breaking ~30 Qed downstreams of `subst_typing_gen_l1_m`. Confirmed. |
| 196 | + |
| 197 | +## References |
| 198 | + |
| 199 | +- `formal/Semantics_L1.v:1358-1656` — `subst_typing_gen_l1_m` proof body. |
| 200 | +- `formal/Semantics_L1.v:916-933` — `linear_value_is_loc_l1` canonical-form extractor. |
| 201 | +- `formal/Semantics_L1.v:1168-1235` — `loc_retype_at_R_l1_m` (the lemma to parallel for non-linear values). |
| 202 | +- `formal/Semantics_L1.v:1708-1713` — body-R-rigidity comment in preservation_l1. |
| 203 | +- `formal/TypingL1.v:221-229` — `T_Lam_L1_Linear_Eff` / `T_Lam_L1_Affine_Eff` (TFunEff lambdas with R_in side condition). |
| 204 | +- `formal/TypingL2.v` post-PR #211 — `preservation_l2_via_l1` + doc block stating the full preservation_l2 goal. |
| 205 | +- `formal/PRESERVATION-DESIGN.md` §5.1 lines 468-474 — load-bearing design quote. |
| 206 | +- `CLAUDE.md` owner directive 2026-05-27 — preservation-work boundaries. |
| 207 | +- PR #209 — T_App_L2_Eff constructor. |
| 208 | +- PR #211 — preservation_l2_via_l1. |
| 209 | +- PR #212 — STATE shift after PR #211. |
0 commit comments