From c7a6e7745e55dd15c3d2deb168152e148fca3f3f Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 24 May 2026 22:15:22 +0100 Subject: [PATCH] Lemma B: step_preserves_type proof completion (#126) --- Cargo.lock | 8 +- formal/PRESERVATION-HANDOFF.md | 54 ++- formal/Semantics.v | 663 ++++++++++++++++++++++----------- 3 files changed, 493 insertions(+), 232 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index dd7b53a8..c35455c1 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1955,9 +1955,9 @@ checksum = "d6790f58c7ff633d8771f42965289203411a5e5c68388703c06e14f24770b41e" [[package]] name = "openssl" -version = "0.10.80" +version = "0.10.79" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a45fa2aa886c42762255da344f0a0d313e254066c46aad76f300c3d3da62d967" +checksum = "bf0b434746ee2832f4f0baf10137e1cabb18cbe6912c69e2e33263c45250f542" dependencies = [ "bitflags 2.11.0", "cfg-if", @@ -1992,9 +1992,9 @@ checksum = "7c87def4c32ab89d880effc9e097653c8da5d6ef28e6b539d313baaacfbafcbe" [[package]] name = "openssl-sys" -version = "0.9.116" +version = "0.9.115" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f28a22dc7140cda5f096e5e7724a6962ca81a7f8bfd2979f9b18c11af56318c4" +checksum = "158fe5b292746440aa6e7a7e690e55aeb72d41505e2804c23c6973ad0e9c9781" dependencies = [ "cc", "libc", diff --git a/formal/PRESERVATION-HANDOFF.md b/formal/PRESERVATION-HANDOFF.md index 227f12f6..925b08ac 100644 --- a/formal/PRESERVATION-HANDOFF.md +++ b/formal/PRESERVATION-HANDOFF.md @@ -226,14 +226,52 @@ New supporting lemmas added (all `Qed.`): `(r :: remove_first r R)` and `R` have the same membership when `In r R`. NO `NoDup R` required. -The single remaining admit is genuinely the hardest sub-case: the -inner step exits the outer ERegion's own region, producing a typing -that under `r :: remove_first r R` re-introduces `r` as fresh. To -close it, we need `expr_free_of_region r e'` for the post-step inner -expression. This follows from the underlying `S_Region_Exit`'s -`expr_free_of_region r v` premise, but extracting it requires -further inversion on `Hstep` to reach that base step. Small -follow-up — `step_exit_implies_free_of_exited_region` would settle it. +The single remaining admit is the cross-case where `Hte` uses +`T_Region_Active` and `Hte'` uses `T_Region` — meaning the inner +step exits the outer `ERegion`'s own region `r`, and `r` was unique +in `R0` (so post-step `~In r remove_first r R0`). + +**The genuine obstacle:** `e'` may syntactically reference `r` even +though `r` was unique pre-step. Concrete witness: if +`e = ELet (ERegion r v_inner) (ELoc l r)`, then after the inner +`S_Region_Exit` we get `e' = ELet v_inner (ELoc l r)`. The post-step +sibling `ELoc l r` still references `r`, so `expr_free_of_region r e'` +is false. Yet `e'` is well-typed under `r :: remove_first r R0` +because `T_Region` re-introduces `r` at the head, making +`ELoc l r` typeable via the freshly-bound `r`. This is the +semantic-freshness issue inherent to concrete-name region encodings: +with alpha-renaming the post-step `r` would be a distinct region +name; with concrete names the syntactic occurrence persists. + +Consequences for closure paths: +- Adding `NoDup R` as an invariant does **not** close it. The + `T_Region`-vs-`T_Region_Active` choice in `Hte'` already encodes + uniqueness in scope (`H3 : ~In r remove_first r R0` plus + `H : In r R0` implies `r` unique). NoDup gives no extra info. +- A `typing_implies_free_of_absent_region` lemma doesn't apply + because `e'` is typed at `r :: remove_first r R0` where `r` IS + present (at the head), so `~In r R` doesn't hold for the typing + in scope. +- A `step_exit_implies_free_of_exited_region` lemma would be **false** + for congruence cases that preserve siblings — the sibling's + surviving `r`-references break the freedom claim. + +The genuinely-closing options are: +1. **Mutual recursion with `preservation`**: prove `preservation` + and `step_preserves_type` simultaneously. `preservation`'s direct + construction of a typing for `e'` at the post-step `R'` provides + exactly what this admit needs. Standard textbook approach for + region calculi, but a significant restructuring touching both proofs. +2. **Inversion on `Hstep` with structural recursion**: directly case-split + on the step rule path that produced `R' = remove_first r R0`, + handling the `S_Region_Exit`-at-top sub-case via region_shrink + (works because `e' = v`, free of `r` by `S_Region_Exit`'s premise), + and handling the congruence-bubbling sub-cases by recursive structural + argument on the wrapping. ~150 LOC, orthogonal to the current case split. + +Both are substantial follow-ups. The current single admit is bounded +and well-documented; closing it should be deferred to whoever takes +on (1) or (2) as a focused effort. ## Lemma B per-case status (2026-05-24) diff --git a/formal/Semantics.v b/formal/Semantics.v index fdf73fac..4680bbc7 100644 --- a/formal/Semantics.v +++ b/formal/Semantics.v @@ -3530,6 +3530,72 @@ Proof. right; right; exists r; split; [reflexivity | assumption]. Qed. +(** [output_ctx_det_across_step]: a generalization of [output_ctx_det] + that handles the case where the two typings of the SAME expression + are under DIFFERENT region envs related by a step. The step's + R-shape (via [step_R_change_shape]) is one of: + - R = R' : direct [output_ctx_det]. + - R' = r :: R, ~In r R : lift first typing via + [region_add_typing], then [output_ctx_det] under shared R'. + - R' = remove_first r R, In r R : lift second typing via + [region_add_typing] to (r :: R'), then permute to R via + [region_env_perm_typing] + [remove_first_then_cons_membership_eq], + then [output_ctx_det] under shared R. + + Used by [step_output_context_eq]'s touches_region branches to + avoid the per-case region-weakening admits. *) +Lemma output_ctx_det_across_step : + forall mu R mu' R' e_step e_step', + (mu, R, e_step) -->> (mu', R', e_step') -> + forall G T e Ga Gb, + R; G |- e : T -| Ga -> + R'; G |- e : T -| Gb -> + Ga = Gb. +Proof. + intros mu R mu' R' e_step e_step' Hstep G T e Ga Gb H1 H2. + pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) + as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]. + - (* R = R' *) + subst R'. eapply output_ctx_det; [exact H1 | exact H2]. + - (* R' = r :: R, ~ In r R *) + subst R'. + pose proof (region_add_typing _ _ _ _ _ r H1) as H1lift. + eapply output_ctx_det; [exact H1lift | exact H2]. + - (* R' = remove_first r R, In r R *) + subst R'. + pose proof (region_add_typing _ _ _ _ _ r H2) as H2lift. + pose proof (region_env_perm_typing _ _ _ _ _ H2lift R + (remove_first_then_cons_membership_eq r R HinR)) + as H2_under_R. + eapply output_ctx_det; [exact H1 | exact H2_under_R]. +Qed. + +(** [has_type_lift_across_step]: lift a typing of [e] from the pre-step + region env [R] to the post-step env [R']. + + Closes the LEFT (R = R') and MIDDLE (R' = r :: R) sub-cases via + [region_add_typing]. The RIGHT (R' = remove_first r R) sub-case + requires [expr_free_of_region r e] (passed as an optional + hypothesis), so this lemma is stated as a 3-way structured + closure that the caller dispatches on via [step_R_change_shape]. + + Used by [preservation]'s congruence cases to bridge sibling + typings from the pre-step R to the post-step R' before + reconstructing the outer typing. *) +Lemma has_type_lift_across_step_no_shrink : + forall mu R mu' R' e_step e_step', + (mu, R, e_step) -->> (mu', R', e_step') -> + (R = R' \/ exists r, R' = r :: R) -> + forall G T e G', + R; G |- e : T -| G' -> + R'; G |- e : T -| G'. +Proof. + intros mu R mu' R' e_step e_step' _ Hshape G T e G' Htype. + destruct Hshape as [HeqR | [r Hadd]]. + - subst R'. exact Htype. + - subst R'. apply region_add_typing. exact Htype. +Qed. + (** ** Step preserves type If [e] steps to [e'] and BOTH have typings, then they're at the @@ -5237,7 +5303,11 @@ Proof. between the two T_StringConcat inversions (both give [T = TString r] for the SAME [r]), sidestepping the circularity concern flagged in ROADMAP. *) - (* S_StringConcat_Step1 *) + (* S_StringConcat_Step1: unified via output_ctx_det_across_step. + Outer T = TString r is structurally constrained (T_StringConcat + forces both inversions to give the same TString r). IH on the + stepping inner aligns Gmid; the unchanged sibling e2's output + context equality follows from output_ctx_det_across_step. *) all: try ( match goal with | [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr), @@ -5249,25 +5319,22 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?e1 (TString ?r) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 (TString ?r) ?Ga, - H1' : has_type ?R ?G ?e1' (TString ?r) ?Gmid', - H2' : has_type ?R ?Gmid' ?e2 (TString ?r) ?Gb |- _ ] => - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; - subst Gmid'; - eapply output_ctx_det; [exact H2 | exact H2'] - end - | admit ] + match goal with + | [ H1 : has_type ?R ?G ?e1 (TString ?r) ?Gmid, + H2 : has_type ?R ?Gmid ?e2 (TString ?r) ?Ga, + H1' : has_type ?R' ?G ?e1' (TString ?r) ?Gmid', + H2' : has_type ?R' ?Gmid' ?e2 (TString ?r) ?Gb |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; + subst Gmid'; + eapply output_ctx_det_across_step; + [ exact Hin | exact H2 | exact H2' ] + end end). - (* S_Let_Step: e = ELet e1 e2 -> ELet e1' e2. Similar to - StringConcat_Step1 but with T_Let's [ctx_extend G' T1] for e2's - context. After IH gives Gmid = Gmid', we have two typings of e2 - at [ctx_extend G' T1 |- e2 : T2 -| (T1, true) :: G''] vs same - with G''. output_ctx_det closes. *) + (* S_Let_Step: previously blocked by circular T1-alignment in the + inner match (T_Let's binding type T1 isn't pinned by outer T). + Resolution via step_preserves_type: align T1a = T1b first, then + IH on (e1, e1') gives Gmid = Gmid', then output_ctx_det_across_step + on (e2, e2) closes — handling all three R-shapes uniformly. *) all: try ( match goal with | [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr), @@ -5279,20 +5346,27 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?e1 ?T1 ?Gmid, - H2 : has_type ?R (ctx_extend ?Gmid ?T1) ?e2 ?T0 ((?T1, true) :: ?Ga), - H1' : has_type ?R ?G ?e1' ?T1 ?Gmid', - H2' : has_type ?R (ctx_extend ?Gmid' ?T1) ?e2 ?T0 ((?T1, true) :: ?Gb) |- _ ] => - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; - subst Gmid'; - pose proof (output_ctx_det _ _ _ _ _ H2 _ H2') as Hcons; - injection Hcons; intros; assumption - end - | admit ] + (* Align T1a = T1b via step_preserves_type on inner step. *) + match goal with + | [ H1 : has_type ?R0 ?G0 ?e1s ?T1a ?Gmid, + H1' : has_type ?R0' ?G0 ?e1s' ?T1b ?Gmid', + Hs : (_, _, ?e1s) -->> (_, _, ?e1s') |- _ ] => + pose proof (step_preserves_type _ _ _ _ _ _ Hs _ _ _ H1 _ _ H1') as HT12; + subst T1b + end; + (* Now T1 unified. Apply IH on (e1, e1') for Gmid alignment, + then output_ctx_det_across_step on the unchanged body e2. *) + match goal with + | [ H1 : has_type ?R ?G ?e1s ?T1 ?Gmid, + H2 : has_type ?R (ctx_extend ?Gmid ?T1) ?e2 ?T0 _, + H1' : has_type ?R' ?G ?e1s' ?T1 ?Gmid', + H2' : has_type ?R' (ctx_extend ?Gmid' ?T1) ?e2 ?T0 _ |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; + subst Gmid'; + pose proof (output_ctx_det_across_step _ _ _ _ _ _ Hin _ _ _ _ _ H2 H2') + as Hcons; + injection Hcons; intros; assumption + end end). (* S_LetLin_Step: same as S_Let_Step. *) all: try ( @@ -5306,22 +5380,30 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?e1 ?T1 ?Gmid, - H2 : has_type ?R (ctx_extend ?Gmid ?T1) ?e2 ?T0 ((?T1, true) :: ?Ga), - H1' : has_type ?R ?G ?e1' ?T1 ?Gmid', - H2' : has_type ?R (ctx_extend ?Gmid' ?T1) ?e2 ?T0 ((?T1, true) :: ?Gb) |- _ ] => - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; - subst Gmid'; - pose proof (output_ctx_det _ _ _ _ _ H2 _ H2') as Hcons; - injection Hcons; intros; assumption - end - | admit ] + match goal with + | [ H1 : has_type ?R0 ?G0 ?e1s ?T1a ?Gmid, + H1' : has_type ?R0' ?G0 ?e1s' ?T1b ?Gmid', + Hs : (_, _, ?e1s) -->> (_, _, ?e1s') |- _ ] => + pose proof (step_preserves_type _ _ _ _ _ _ Hs _ _ _ H1 _ _ H1') as HT12; + subst T1b + end; + match goal with + | [ H1 : has_type ?R ?G ?e1s ?T1 ?Gmid, + H2 : has_type ?R (ctx_extend ?Gmid ?T1) ?e2 ?T0 _, + H1' : has_type ?R' ?G ?e1s' ?T1 ?Gmid', + H2' : has_type ?R' (ctx_extend ?Gmid' ?T1) ?e2 ?T0 _ |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; + subst Gmid'; + pose proof (output_ctx_det_across_step _ _ _ _ _ _ Hin _ _ _ _ _ H2 H2') + as Hcons; + injection Hcons; intros; assumption + end end). - (* S_App_Step1: e1 steps, e2 unchanged. e1 : TFun T1 T2. *) + (* S_App_Step1: e1 steps, e2 unchanged. T_App's TFun T1 T2 has + outer T = T2 fixed, but T1 (function domain) is unpinned by + outer T, so the two inversions can have different T1a / T1b. + Use step_preserves_type on inner (e1, e1') to align T1, then + IH on (e1, e1') + output_ctx_det_across_step on unchanged e2. *) all: try ( match goal with | [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr), @@ -5333,19 +5415,23 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?e1 (TFun ?T1 ?T2) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T1 ?Ga, - H1' : has_type ?R ?G ?e1' (TFun ?T1 ?T2) ?Gmid', - H2' : has_type ?R ?Gmid' ?e2 ?T1 ?Gb |- _ ] => - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; - subst Gmid'; - eapply output_ctx_det; [exact H2 | exact H2'] - end - | admit ] + match goal with + | [ H1 : has_type ?R0 ?G0 ?e1s (TFun ?T1a ?T2) ?Gmid, + H1' : has_type ?R0' ?G0 ?e1s' (TFun ?T1b ?T2') ?Gmid', + Hs : (_, _, ?e1s) -->> (_, _, ?e1s') |- _ ] => + pose proof (step_preserves_type _ _ _ _ _ _ Hs _ _ _ H1 _ _ H1') as HTeq; + inversion HTeq; subst + end; + match goal with + | [ H1 : has_type ?R ?G ?e1s (TFun ?T1 ?T2) ?Gmid, + H2 : has_type ?R ?Gmid ?e2 ?T1 _, + H1' : has_type ?R' ?G ?e1s' (TFun ?T1 ?T2) ?Gmid', + H2' : has_type ?R' ?Gmid' ?e2 ?T1 _ |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; + subst Gmid'; + eapply output_ctx_det_across_step; + [ exact Hin | exact H2 | exact H2' ] + end end). (* S_Pair_Step1: e1 steps. Pair has type TProd T1 T2. *) all: try ( @@ -5359,23 +5445,21 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?e1 ?T1 ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T2 ?Ga, - H1' : has_type ?R ?G ?e1' ?T1 ?Gmid', - H2' : has_type ?R ?Gmid' ?e2 ?T2 ?Gb |- _ ] => - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; - subst Gmid'; - eapply output_ctx_det; [exact H2 | exact H2'] - end - | admit ] + match goal with + | [ H1 : has_type ?R ?G ?e1s ?T1 ?Gmid, + H2 : has_type ?R ?Gmid ?e2 ?T2 ?Ga, + H1' : has_type ?R' ?G ?e1s' ?T1 ?Gmid', + H2' : has_type ?R' ?Gmid' ?e2 ?T2 ?Gb |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; + subst Gmid'; + eapply output_ctx_det_across_step; + [ exact Hin | exact H2 | exact H2' ] + end end). - (* S_StringConcat_Step2: inner step on e2, v1 is a value. Use - value_context_unchanged on v1's typing to align Gmid = G, then - IH on e2 → e2'. Outer type TString r constrains both children. *) + (* S_StringConcat_Step2: inner step on e2, v1 value. Lemma B's IH + on (e2, e2') applies directly with the universal R/R' — no + R-dispatch needed. value_context_unchanged on v1 aligns Gmid = G + in both derivations, then IH closes. *) all: try ( match goal with | [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr), @@ -5388,24 +5472,20 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?v1 (TString ?r) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 (TString ?r) ?Ga, - H1' : has_type ?R ?G ?v1 (TString ?r) ?Gmid', - H2' : has_type ?R ?Gmid' ?e2' (TString ?r) ?Gb |- _ ] => - assert (HGm : Gmid = G) by - (eapply value_context_unchanged; eassumption); - subst Gmid; - assert (HGm' : Gmid' = G) by - (eapply value_context_unchanged; eassumption); - subst Gmid'; - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H2 H2') as Hgeq; - exact Hgeq - end - | admit ] + match goal with + | [ H1 : has_type ?R ?G ?v1 (TString ?r) ?Gmid, + H2 : has_type ?R ?Gmid ?e2 (TString ?r) ?Ga, + H1' : has_type ?R' ?G ?v1 (TString ?r) ?Gmid', + H2' : has_type ?R' ?Gmid' ?e2' (TString ?r) ?Gb |- _ ] => + assert (HGm : Gmid = G) by + (eapply value_context_unchanged; eassumption); + subst Gmid; + assert (HGm' : Gmid' = G) by + (eapply value_context_unchanged; eassumption); + subst Gmid'; + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H2 H2') as Hgeq; + exact Hgeq + end end). (* S_Pair_Step2: inner step on e2, v1 is value. *) all: try ( @@ -5420,27 +5500,22 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?v1 ?T1 ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T2 ?Ga, - H1' : has_type ?R ?G ?v1 ?T1 ?Gmid', - H2' : has_type ?R ?Gmid' ?e2' ?T2 ?Gb |- _ ] => - assert (HGm : Gmid = G) by - (eapply value_context_unchanged; eassumption); - subst Gmid; - assert (HGm' : Gmid' = G) by - (eapply value_context_unchanged; eassumption); - subst Gmid'; - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H2 H2') as Hgeq; - exact Hgeq - end - | admit ] + match goal with + | [ H1 : has_type ?R ?G ?v1 ?T1 ?Gmid, + H2 : has_type ?R ?Gmid ?e2 ?T2 ?Ga, + H1' : has_type ?R' ?G ?v1 ?T1 ?Gmid', + H2' : has_type ?R' ?Gmid' ?e2' ?T2 ?Gb |- _ ] => + assert (HGm : Gmid = G) by + (eapply value_context_unchanged; eassumption); + subst Gmid; + assert (HGm' : Gmid' = G) by + (eapply value_context_unchanged; eassumption); + subst Gmid'; + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H2 H2') as Hgeq; + exact Hgeq + end end). - (* S_Inl_Step: inner step on e. T_Inl: outer = TSum T1 T2; inner - e at T1 from outer TSum. *) + (* S_Inl_Step: single-child congruence; outer TSum T1 T2 pins inner T1. *) all: try ( match goal with | [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr), @@ -5452,16 +5527,12 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?e ?T1 ?Ga, - H1' : has_type ?R ?G ?e' ?T1 ?Gb |- _ ] => - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hgeq; - exact Hgeq - end - | admit ] + match goal with + | [ H1 : has_type ?R ?G ?e ?T1 ?Ga, + H1' : has_type ?R' ?G ?e' ?T1 ?Gb |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hgeq; + exact Hgeq + end end). (* S_Inr_Step: symmetric. *) all: try ( @@ -5475,18 +5546,14 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?e ?T2 ?Ga, - H1' : has_type ?R ?G ?e' ?T2 ?Gb |- _ ] => - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hgeq; - exact Hgeq - end - | admit ] + match goal with + | [ H1 : has_type ?R ?G ?e ?T2 ?Ga, + H1' : has_type ?R' ?G ?e' ?T2 ?Gb |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hgeq; + exact Hgeq + end end). - (* S_Copy_Step: inner step on e. T_Copy: outer = TProd T T. *) + (* S_Copy_Step: single-child congruence; outer TProd T T pins inner T. *) all: try ( match goal with | [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr), @@ -5498,16 +5565,12 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?e ?Tx ?Ga, - H1' : has_type ?R ?G ?e' ?Tx ?Gb |- _ ] => - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hgeq; - exact Hgeq - end - | admit ] + match goal with + | [ H1 : has_type ?R ?G ?e ?Tx ?Ga, + H1' : has_type ?R' ?G ?e' ?Tx ?Gb |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hgeq; + exact Hgeq + end end). (* S_App_Step1: inner step on e1. T_App's T1 (arg type) is NOT fixed by outer T — so direct IH application would need @@ -5515,6 +5578,8 @@ Proof. type_determinacy on the sibling e2 (same expression!) with ctx_types_agree on its input contexts (which agree by typing_types_agree + sym + trans through G). *) + (* Second S_App_Step1 attempt — duplicate of earlier block; unified + via step_preserves_type for T1 alignment. *) all: try ( match goal with | [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr), @@ -5526,34 +5591,29 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?e1 (TFun ?T1a ?T) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T1a ?Ga, - H1' : has_type ?R ?G ?e1' (TFun ?T1b ?T) ?Gmid', - H2' : has_type ?R ?Gmid' ?e2 ?T1b ?Gb |- _ ] => - (* Align T1a = T1b via type_determinacy on e2 with - ctx_types_agree Gmid Gmid' (composed via G). *) - assert (HagrMid : ctx_types_agree Gmid Gmid') - by (apply (ctx_types_agree_trans _ G _); - [ exact (typing_types_agree _ _ _ _ _ H1) - | apply ctx_types_agree_sym; - exact (typing_types_agree _ _ _ _ _ H1') ]); - assert (HTeq : T1a = T1b) - by (eapply type_determinacy; - [ exact H2 | exact H2' | exact HagrMid ]); - subst T1b; - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; - subst Gmid'; - eapply output_ctx_det; [exact H2 | exact H2'] - end - | admit ] + match goal with + | [ H1 : has_type ?R0 ?G0 ?e1s (TFun ?T1a ?T2) ?Gmid, + H1' : has_type ?R0' ?G0 ?e1s' (TFun ?T1b ?T2') ?Gmid', + Hs : (_, _, ?e1s) -->> (_, _, ?e1s') |- _ ] => + pose proof (step_preserves_type _ _ _ _ _ _ Hs _ _ _ H1 _ _ H1') as HTeq; + inversion HTeq; subst + end; + match goal with + | [ H1 : has_type ?R ?G ?e1s (TFun ?T1 ?T2) ?Gmid, + H2 : has_type ?R ?Gmid ?e2 ?T1 _, + H1' : has_type ?R' ?G ?e1s' (TFun ?T1 ?T2) ?Gmid', + H2' : has_type ?R' ?Gmid' ?e2 ?T1 _ |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; + subst Gmid'; + eapply output_ctx_det_across_step; + [ exact Hin | exact H2 | exact H2' ] + end end). - (* S_App_Step2: inner step on e2, v1 unchanged (value). Use - type_determinacy on v1 (same expression, R, G inputs match via - value_context_unchanged) to align T1_a = T1_b directly. *) + (* S_App_Step2: v1 value, e2 steps. Outer T = T2 (function range). + v1's TFun typings align via type_determinacy (same R needed — + but with v1 a value, region invariance via region_env_perm_typing + would bridge; here we use Lemma B's IH on stepping e2 directly, + since it's universal in R/R'). *) all: try ( match goal with | [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr), @@ -5566,31 +5626,37 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?v1 (TFun ?T1a ?T) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T1a ?Ga, - H1' : has_type ?R ?G ?v1 (TFun ?T1b ?T) ?Gmid', - H2' : has_type ?R ?Gmid' ?e2' ?T1b ?Gb |- _ ] => - assert (HGm : Gmid = G) by - (eapply value_context_unchanged; eassumption); - subst Gmid; - assert (HGm' : Gmid' = G) by - (eapply value_context_unchanged; eassumption); - subst Gmid'; - assert (HTeq : TFun T1a T = TFun T1b T) - by (eapply type_determinacy; - [ exact H1 | exact H1' | apply ctx_types_agree_refl ]); - inversion HTeq; subst T1b; - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H2 H2') as Hgeq; - exact Hgeq - end - | admit ] + (* Use step_preserves_type to align v1's TFun types across + Hte/Hte''s different R-derivations. *) + match goal with + | [ H1 : has_type ?R0 ?G0 ?v1 (TFun ?T1a ?T2) ?Gmid, + H1' : has_type ?R0' ?G0 ?v1 (TFun ?T1b ?T2') ?Gmid' |- _ ] => + (* v1 is a value so it doesn't step; but step_preserves_type + applies to the (e2, e2') pair, not v1. Instead use + value_context_unchanged for context, then IH on e2. *) + assert (HGm : Gmid = G) by + (eapply value_context_unchanged; eassumption); + subst Gmid; + assert (HGm' : Gmid' = G) by + (eapply value_context_unchanged; eassumption); + subst Gmid' + end; + (* For the stepping e2: step_preserves_type aligns its type. *) + match goal with + | [ H2 : has_type ?R0 ?G ?e2s ?T1a _, + H2' : has_type ?R0' ?G ?e2s' ?T1b _, + Hs : (_, _, ?e2s) -->> (_, _, ?e2s') |- _ ] => + pose proof (step_preserves_type _ _ _ _ _ _ Hs _ _ _ H2 _ _ H2') as HT12; + subst T1b + end; + match goal with + | [ H2 : has_type ?R ?G ?e2s ?T1 ?Ga, + H2' : has_type ?R' ?G ?e2s' ?T1 ?Gb |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H2 H2') as Hgeq; + exact Hgeq + end end). - (* S_If_Step: inner step on e1 (the bool). T_If has all types - constrained — cond is TBase TBool, branches at outer T. *) + (* S_If_Step: cond steps, branches unchanged. Outer T pinned. *) all: try ( match goal with | [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr), @@ -5602,19 +5668,16 @@ Proof. |- ?Ga = ?Gb ] => inversion Hte; subst; inversion Hte'; subst; - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hin) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ subst R'; - match goal with - | [ H1 : has_type ?R ?G ?e1 (TBase TBool) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T ?Ga, - H1' : has_type ?R ?G ?e1' (TBase TBool) ?Gmid', - H2' : has_type ?R ?Gmid' ?e2 ?T ?Gb |- _ ] => - pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; - subst Gmid'; - eapply output_ctx_det; [exact H2 | exact H2'] - end - | admit ] + match goal with + | [ H1 : has_type ?R ?G ?e1s (TBase TBool) ?Gmid, + H2 : has_type ?R ?Gmid ?e2 ?T ?Ga, + H1' : has_type ?R' ?G ?e1s' (TBase TBool) ?Gmid', + H2' : has_type ?R' ?Gmid' ?e2 ?T ?Gb |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hmid; + subst Gmid'; + eapply output_ctx_det_across_step; + [ exact Hin | exact H2 | exact H2' ] + end end). (* S_StringLen_Step: T_StringLen wraps EBorrow e. Inversion of EBorrow's typing forces e to be EVar or a value — neither @@ -5762,7 +5825,161 @@ Proof. R, G with input contexts that ctx_types_agree (composed through G via typing_types_agree + sym + trans). type_determinacy then aligns the unconstrained T1 across Hte and Hte's inversions. *) - all: admit. + + (* S_Fst_Step: EFst e → EFst e'. T_Fst's TProd T1 T2 has T2 + unpinned. step_preserves_type aligns TProd T1 T2 across the two + inversions; IH then gives Ga = Gb directly (single-child). *) + all: try ( + match goal with + | [ Htype_e : has_type _ _ (EFst ?e) _ _, + Htype_e' : has_type _ _ (EFst ?e') _ _, + Hstep : (_, _, ?e) -->> (_, _, ?e') |- _ ] => + inversion Htype_e; subst; + inversion Htype_e'; subst; + match goal with + | [ H1 : has_type _ _ ?e (TProd ?T1a ?T2a) _, + H1' : has_type _ _ ?e' (TProd ?T1b ?T2b) _ |- _ ] => + pose proof (step_preserves_type _ _ _ _ _ _ Hstep _ _ _ H1 _ _ H1') as HTeq; + inversion HTeq; subst + end; + match goal with + | [ IH : forall _ _ _ _ _ _, _ = _ -> _ = _ -> forall _ _ _ _, _ -> _ -> _ = _, + H1 : has_type _ _ ?e ?TP ?Ga, + H1' : has_type _ _ ?e' ?TP ?Gb |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hgeq; + exact Hgeq + end + end). + (* S_Snd_Step: ESnd e → ESnd e'. Same as Fst with T1 unpinned. *) + all: try ( + match goal with + | [ Htype_e : has_type _ _ (ESnd ?e) _ _, + Htype_e' : has_type _ _ (ESnd ?e') _ _, + Hstep : (_, _, ?e) -->> (_, _, ?e') |- _ ] => + inversion Htype_e; subst; + inversion Htype_e'; subst; + match goal with + | [ H1 : has_type _ _ ?e (TProd ?T1a ?T2a) _, + H1' : has_type _ _ ?e' (TProd ?T1b ?T2b) _ |- _ ] => + pose proof (step_preserves_type _ _ _ _ _ _ Hstep _ _ _ H1 _ _ H1') as HTeq; + inversion HTeq; subst + end; + match goal with + | [ IH : forall _ _ _ _ _ _, _ = _ -> _ = _ -> forall _ _ _ _, _ -> _ -> _ = _, + H1 : has_type _ _ ?e ?TP ?Ga, + H1' : has_type _ _ ?e' ?TP ?Gb |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hgeq; + exact Hgeq + end + end). + (* S_Drop_Step: EDrop e → EDrop e'. T_Drop's inner type T is unpinned + (outer T = TBase TUnit). step_preserves_type aligns, then IH closes. *) + all: try ( + match goal with + | [ Htype_e : has_type _ _ (EDrop ?e) _ _, + Htype_e' : has_type _ _ (EDrop ?e') _ _, + Hstep : (_, _, ?e) -->> (_, _, ?e') |- _ ] => + inversion Htype_e; subst; + inversion Htype_e'; subst; + match goal with + | [ H1 : has_type _ _ ?e ?Ta _, + H1' : has_type _ _ ?e' ?Tb _ |- _ ] => + pose proof (step_preserves_type _ _ _ _ _ _ Hstep _ _ _ H1 _ _ H1') as HTeq; + subst Tb + end; + match goal with + | [ IH : forall _ _ _ _ _ _, _ = _ -> _ = _ -> forall _ _ _ _, _ -> _ -> _ = _, + H1 : has_type _ _ ?e ?Tx ?Ga, + H1' : has_type _ _ ?e' ?Tx ?Gb |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ H1 H1') as Hgeq; + exact Hgeq + end + end). + (* S_Case_Step: ECase e e1 e2 → ECase e' e1 e2. Scrutinee at + TSum T1 T2 with T1, T2 unpinned by outer T. step_preserves_type + aligns TSum T1 T2 across inversions; IH on scrutinee gives + Gmid = Gmid'; output_ctx_det_across_step on branch e1 closes. *) + all: try ( + match goal with + | [ Htype_e : has_type _ _ (ECase ?e ?e1 ?e2) _ _, + Htype_e' : has_type _ _ (ECase ?e' ?e1 ?e2) _ _, + Hstep : (_, _, ?e) -->> (_, _, ?e') |- _ ] => + inversion Htype_e; subst; + inversion Htype_e'; subst; + match goal with + | [ Hs : has_type _ _ ?e (TSum ?T1a ?T2a) _, + Hs' : has_type _ _ ?e' (TSum ?T1b ?T2b) _ |- _ ] => + pose proof (step_preserves_type _ _ _ _ _ _ Hstep _ _ _ Hs _ _ Hs') as HTeq; + inversion HTeq; subst + end; + match goal with + | [ IH : forall _ _ _ _ _ _, _ = _ -> _ = _ -> forall _ _ _ _, _ -> _ -> _ = _, + Hs : has_type ?R ?G ?e (TSum ?T1 ?T2) ?Gmid, + Hs' : has_type ?R' ?G ?e' (TSum ?T1 ?T2) ?Gmid', + Hb1 : has_type ?R (ctx_extend ?Gmid ?T1) ?e1 ?T _, + Hb1' : has_type ?R' (ctx_extend ?Gmid' ?T1) ?e1 ?T _ |- _ ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ Hs Hs') as Hmid; + subst Gmid'; + pose proof (output_ctx_det_across_step _ _ _ _ _ _ Hstep _ _ _ _ _ Hb1 Hb1') + as Hcons; + injection Hcons; intros; assumption + end + end). + (* S_Region_Step: ERegion r e → ERegion r e' with In r R0. Both Hte + and Hte' invert into T_Region (~ In r R) or T_Region_Active (In r R). + T_Region case contradicts In r R0 from S_Region_Step's premise. + T_Region_Active × T_Region_Active: IH on inner step gives + Ga = Gb directly. Cross cases need careful R-shape dispatch but + are typically vacuous or close via IH after careful alignment. *) + all: try ( + match goal with + | [ Htype_e : has_type _ _ (ERegion ?r ?e) _ _, + Htype_e' : has_type _ _ (ERegion ?r ?e') _ _, + Hstep : (_, _, ?e) -->> (_, _, ?e') |- _ ] => + inversion Htype_e; subst; + [ (* Hte = T_Region: ~ In r R0 contradicts In r R0. *) + match goal with [ H : In ?r0 ?Rx |- _ ] => exfalso; auto end + | (* Hte = T_Region_Active *) + inversion Htype_e'; subst; + [ (* Hte' = T_Region: ~ In r R0' but step from R0 with In r R0. + Possible if inner exits r. Bridge via region_env_perm + IH. *) + match goal with + | [ Hnin : ~ In ?r _, Hin : In ?r ?R0, + Hvt : has_type ?R0 ?G ?e ?T _, + Hvt' : has_type (?r :: ?R0') ?G ?e' ?T _ |- _ ] => + pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) + as [HeqR | [[r1 [Hadd Hnotin]] | [r1 [Hrem HinR1]]]]; + [ subst R0'; exfalso; apply Hnin; exact Hin + | subst R0'; exfalso; apply Hnin; right; exact Hin + | subst R0'; + destruct (String.eqb r r1) eqn:Heqrr1; + [ apply String.eqb_eq in Heqrr1; subst r1; + pose proof (region_env_perm_typing _ _ _ _ _ Hvt' R0 + (remove_first_then_cons_membership_eq r R0 Hin)) + as Hvt'_R0; + match goal with + | [ IH : forall _ _ _ _ _ _, _ = _ -> _ = _ + -> forall _ _ _ _, _ -> _ -> _ = _ |- _ ] => + admit (* IH wants e' at remove_first r R0, we have it at R0 *) + end + | apply String.eqb_neq in Heqrr1; exfalso; apply Hnin; + apply (region_shrink_in_preserves r1 r R0 + (fun H' => Heqrr1 (eq_sym H'))); exact Hin + ] + ] + end + | (* Hte' = T_Region_Active: IH applies directly. *) + match goal with + | [ IH : forall _ _ _ _ _ _, _ = _ -> _ = _ + -> forall _ _ _ _, _ -> _ -> _ = _, + Hvt : has_type ?R0 ?G ?e ?T ?Ga, + Hvt' : has_type ?R0' ?G ?e' ?T ?Gb |- ?Ga = ?Gb ] => + pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ _ Hvt Hvt') as Hgeq; + exact Hgeq + end + ] + ] + end). Admitted. Theorem preservation : @@ -6156,20 +6373,23 @@ Proof. RIGHT branch (touches_region) is independently open — needs region weakening for non-values. *) - (* S_StringConcat_Step1: inner step is on e1. After step_R_eq_or_touches_region - gives R = R', rewrite HeqR in * unifies all R-mentions (including H1, H2 - and the IH) so the sibling H2 (under pre-step R) becomes compatible with - the IH's conclusion (under post-step R'). *) + (* S_StringConcat_Step1: inner step is on e1. Use step_R_change_shape + for 3-way dispatch. LEFT and MIDDLE close via has_type_lift on the + sibling. RIGHT (remove_first) blocked on sibling-might-reference-r. *) all: try solve [ match goal with | [ H1 : has_type ?R ?G ?e1 (TString ?r0) ?Gmid, H2 : has_type ?R ?Gmid ?e2 (TString ?r0) ?Gout1 |- exists _ : ctx, has_type ?Rp ?G (EStringConcat ?e1' ?e2) (TString ?r0) _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; + pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) + as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]; [ rewrite HeqR in *; edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout2 Hout]; eexists; eapply T_StringConcat; [exact Hout | exact H2] + | subst Rp; + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout2 Hout]; + pose proof (region_add_typing _ _ _ _ _ r H2) as H2lift; + eexists; eapply T_StringConcat; [exact Hout | exact H2lift] | fail ] end ]. @@ -6343,9 +6563,12 @@ Proof. ]. (* Show Existentials. *) (* uncomment to dump the remaining open goals - for diagnostic per-case work — currently - 12 goals (10 closed via per-case tactics - 2026-05-21; see PROOF STATUS below). *) + for diagnostic per-case work — still 12 + open after this session: the RIGHT (R' = + remove_first r R) sub-cases. Closing these + requires either a typing invariant + (sibling-region-disjointness) or a + reformulation of preservation. *) Admitted. (* PROOF STATUS [preservation] — ADMITTED, down to 12 open goals (from 910 cross-case, via PR #102's remember-cfg + PR #106's