Skip to content

Commit 4bb8c2a

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
wip(L1): Phase 3b Stage 1b prerequisite — expr_closed_below + closure helpers (Syntax.v)
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) <noreply@anthropic.com>
1 parent 7c4c3f5 commit 4bb8c2a

1 file changed

Lines changed: 196 additions & 0 deletions

File tree

‎formal/Syntax.v‎

Lines changed: 196 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
Require Import Coq.Lists.List.
1616
Require Import Coq.Arith.Arith.
1717
Require Import Coq.Strings.String.
18+
Require Import Lia.
1819
Import ListNotations.
1920

2021
(** ** Variables and Names *)
@@ -553,6 +554,55 @@ Fixpoint tfuneff_lambda_free (e : expr) : bool :=
553554
| ELam _ _ => false
554555
end.
555556

557+
(** Syntactic closure predicate: [expr_closed_below k e] holds when [e]
558+
contains no free de Bruijn variable ≥ [k]. Variables < [k] are bound
559+
by lambda/let/case binders introduced *above* the term.
560+
561+
Used by Phase 3b Stage 1b's TFunEff substitution lemma to permit
562+
G-polymorphic retype of the substituent v: for [expr_closed_below 0
563+
v] terms, the body of any TFunEff value [v = ELam T0 ebody] is
564+
[expr_closed_below 1] — i.e., references only position 0 (the bound
565+
variable). Outer context positions ≥ 1 are inert, which discharges
566+
the G-mismatch in compound-rule cases of the substitution lemma.
567+
568+
Binder structure (mirrors [shift] / [subst] at lines 542-606):
569+
- [ELam _ e0]: e0 at S k (one binder).
570+
- [ELet e1 e2]: e1 at k, e2 at S k.
571+
- [ELetLin e1 e2]: e1 at k, e2 at S k.
572+
- [ECase e0 e1 e2]: e0 at k, e1 and e2 each at S k.
573+
- All other forms: same k across sub-expressions.
574+
575+
[bool] target per Phase D's post-redesign style ([is_linear_ty],
576+
[is_ground_nonlinear_ty], [tfuneff_lambda_free] are all bool). The
577+
legacy [expr_free_of_region] / [expr_strictly_free_of_region] Prop
578+
predicates are pre-redesign artefacts.
579+
580+
Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 3b Stage 1b
581+
and ephapax issue #249. *)
582+
Fixpoint expr_closed_below (k : nat) (e : expr) : bool :=
583+
match e with
584+
| EUnit | EBool _ | EI32 _ => true
585+
| EVar i => Nat.ltb i k
586+
| EStringNew _ _ | ELoc _ _ => true
587+
| EStringConcat e1 e2 | EApp e1 e2 | EPair e1 e2 =>
588+
andb (expr_closed_below k e1) (expr_closed_below k e2)
589+
| ELet e1 e2 | ELetLin e1 e2 =>
590+
andb (expr_closed_below k e1) (expr_closed_below (S k) e2)
591+
| EStringLen e' | EFst e' | ESnd e'
592+
| EBorrow e' | EDeref e' | EDrop e' | ECopy e' | EObserve e' =>
593+
expr_closed_below k e'
594+
| EInl _ e' | EInr _ e' | EEcho _ e' | ERegion _ e' =>
595+
expr_closed_below k e'
596+
| EIf e1 e2 e3 =>
597+
andb (andb (expr_closed_below k e1) (expr_closed_below k e2))
598+
(expr_closed_below k e3)
599+
| ECase e0 e1 e2 =>
600+
andb (andb (expr_closed_below k e0)
601+
(expr_closed_below (S k) e1))
602+
(expr_closed_below (S k) e2)
603+
| ELam _ e' => expr_closed_below (S k) e'
604+
end.
605+
556606
(** Check if all linear variables in context have been used *)
557607
Fixpoint ctx_all_linear_used (G : ctx) : Prop :=
558608
match G with
@@ -649,6 +699,152 @@ Proof.
649699
intros c d v Hv. induction Hv; simpl; try constructor; auto.
650700
Qed.
651701

702+
(** Closed-below-c terms are shift-invariant at cutoff c.
703+
704+
The shift function increments free variables ≥ c. A term that is
705+
[expr_closed_below c] has no such variables, so shift is the
706+
identity. Companion to [shift_preserves_value] for the closure-
707+
sensitive Phase 3b Stage 1b machinery: when substituting a closed
708+
TFunEff value through a binder, the operational [shift 0 1 v] in
709+
[subst]'s ELam/ELet/ELetLin/ECase cases reduces to [v] itself,
710+
matching the syntactic shape needed by the substitution lemma's
711+
recursive rebuild.
712+
713+
Proof: induction on [e] with c, d re-introduced after [induction]
714+
to keep the IH polymorphic over c (the cutoff varies through
715+
binders). *)
716+
Lemma closed_below_shift_id :
717+
forall e c d, expr_closed_below c e = true -> shift c d e = e.
718+
Proof.
719+
induction e; intros c d Hc; simpl in *; try reflexivity.
720+
- (* EVar v: Hc : v <? c = true, so leb c v = false, shift returns
721+
EVar v unchanged. *)
722+
apply Nat.ltb_lt in Hc.
723+
destruct (Nat.leb_spec c v) as [Hle|Hlt]; [lia | reflexivity].
724+
- (* EStringConcat e1 e2 *)
725+
apply andb_prop in Hc as [H1 H2].
726+
f_equal; [apply IHe1 | apply IHe2]; assumption.
727+
- (* EStringLen e' *)
728+
f_equal. apply IHe. assumption.
729+
- (* ELet e1 e2 — e1 at c, e2 at S c *)
730+
apply andb_prop in Hc as [H1 H2].
731+
f_equal; [apply IHe1 | apply IHe2]; assumption.
732+
- (* ELetLin e1 e2 *)
733+
apply andb_prop in Hc as [H1 H2].
734+
f_equal; [apply IHe1 | apply IHe2]; assumption.
735+
- (* EIf e1 e2 e3 *)
736+
apply andb_prop in Hc as [H12 H3].
737+
apply andb_prop in H12 as [H1 H2].
738+
f_equal; [apply IHe1 | apply IHe2 | apply IHe3]; assumption.
739+
- (* ELam T e' — e' at S c *)
740+
f_equal. apply IHe. assumption.
741+
- (* EApp e1 e2 *)
742+
apply andb_prop in Hc as [H1 H2].
743+
f_equal; [apply IHe1 | apply IHe2]; assumption.
744+
- (* EPair e1 e2 *)
745+
apply andb_prop in Hc as [H1 H2].
746+
f_equal; [apply IHe1 | apply IHe2]; assumption.
747+
- (* EFst *)
748+
f_equal. apply IHe. assumption.
749+
- (* ESnd *)
750+
f_equal. apply IHe. assumption.
751+
- (* EInl T e' *)
752+
f_equal. apply IHe. assumption.
753+
- (* EInr T e' *)
754+
f_equal. apply IHe. assumption.
755+
- (* ECase e0 e1 e2 — e0 at c, e1 and e2 at S c *)
756+
apply andb_prop in Hc as [H01 H2].
757+
apply andb_prop in H01 as [H0 H1].
758+
f_equal; [apply IHe1 | apply IHe2 | apply IHe3]; assumption.
759+
- (* ERegion *)
760+
f_equal. apply IHe. assumption.
761+
- (* EBorrow *)
762+
f_equal. apply IHe. assumption.
763+
- (* EDeref *)
764+
f_equal. apply IHe. assumption.
765+
- (* EDrop *)
766+
f_equal. apply IHe. assumption.
767+
- (* ECopy *)
768+
f_equal. apply IHe. assumption.
769+
- (* EEcho T e' *)
770+
f_equal. apply IHe. assumption.
771+
- (* EObserve *)
772+
f_equal. apply IHe. assumption.
773+
Qed.
774+
775+
(** Closure is preserved under shifting at any cutoff.
776+
777+
A term [e] that is closed below cutoff [c] remains closed below
778+
cutoff [c + d] after shifting by d at any cutoff ≤ c. Useful when
779+
propagating closure through binder traversals in the substitution
780+
lemma's recursive calls.
781+
782+
Proof: induction on [e] with all parameters generalised. The
783+
EVar case is the only non-trivial one — the others propagate
784+
through structural recursion. *)
785+
Lemma expr_closed_below_shift_mono :
786+
forall e c c' d,
787+
c' <= c ->
788+
expr_closed_below c e = true ->
789+
expr_closed_below (c + d) (shift c' d e) = true.
790+
Proof.
791+
induction e; intros cu cu' d Hle Hc; simpl in *; try reflexivity.
792+
- (* EVar v *)
793+
apply Nat.ltb_lt in Hc.
794+
destruct (Nat.leb_spec cu' v) as [Hge|Hlt].
795+
+ (* cu' ≤ v: shift produces EVar (v + d); need v + d < cu + d *)
796+
simpl. apply Nat.ltb_lt. lia.
797+
+ (* v < cu': shift unchanged; v < cu ≤ cu + d *)
798+
simpl. apply Nat.ltb_lt. lia.
799+
- (* EStringConcat *)
800+
apply andb_prop in Hc as [H1 H2]. simpl.
801+
rewrite IHe1 by assumption. rewrite IHe2 by assumption. reflexivity.
802+
- (* EStringLen *)
803+
apply IHe; assumption.
804+
- (* ELet — e2 at S cu, with the shift cutoff also at S cu' *)
805+
apply andb_prop in Hc as [H1 H2]. simpl.
806+
rewrite IHe1 by assumption.
807+
replace (S (cu + d)) with (S cu + d) by lia.
808+
rewrite IHe2; [reflexivity | lia | assumption].
809+
- (* ELetLin *)
810+
apply andb_prop in Hc as [H1 H2]. simpl.
811+
rewrite IHe1 by assumption.
812+
replace (S (cu + d)) with (S cu + d) by lia.
813+
rewrite IHe2; [reflexivity | lia | assumption].
814+
- (* EIf *)
815+
apply andb_prop in Hc as [H12 H3].
816+
apply andb_prop in H12 as [H1 H2]. simpl.
817+
rewrite IHe1, IHe2, IHe3 by assumption. reflexivity.
818+
- (* ELam — e' at S cu *)
819+
simpl.
820+
replace (S (cu + d)) with (S cu + d) by lia.
821+
apply IHe; [lia | assumption].
822+
- (* EApp *)
823+
apply andb_prop in Hc as [H1 H2]. simpl.
824+
rewrite IHe1, IHe2 by assumption. reflexivity.
825+
- (* EPair *)
826+
apply andb_prop in Hc as [H1 H2]. simpl.
827+
rewrite IHe1, IHe2 by assumption. reflexivity.
828+
- (* EFst *) apply IHe; assumption.
829+
- (* ESnd *) apply IHe; assumption.
830+
- (* EInl *) apply IHe; assumption.
831+
- (* EInr *) apply IHe; assumption.
832+
- (* ECase *)
833+
apply andb_prop in Hc as [H01 H2].
834+
apply andb_prop in H01 as [H0 H1]. simpl.
835+
rewrite IHe1 by assumption.
836+
replace (S (cu + d)) with (S cu + d) by lia.
837+
rewrite IHe2; [|lia|assumption].
838+
rewrite IHe3; [reflexivity|lia|assumption].
839+
- (* ERegion *) apply IHe; assumption.
840+
- (* EBorrow *) apply IHe; assumption.
841+
- (* EDeref *) apply IHe; assumption.
842+
- (* EDrop *) apply IHe; assumption.
843+
- (* ECopy *) apply IHe; assumption.
844+
- (* EEcho *) apply IHe; assumption.
845+
- (* EObserve *) apply IHe; assumption.
846+
Qed.
847+
652848
(** ** Region Environment *)
653849

654850
Definition region_env := list region_name.

0 commit comments

Comments
 (0)