Skip to content

Commit d0c5117

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(L1.D): preservation_l1 body — 29/33 cases closed, 4 admits surface R-weakening gap (#161)
## Summary Inlines the per-case proof body of \`preservation_l1\` using the three swarm helpers from L1.A/B/C (all Qed): - \`value_R_G_preserving_l1\` (L1.A, PR #158) - \`region_shrink_preserves_typing_l1\` (L1.B, PR #159) - \`subst_preserves_typing_l1\` (L1.C, PR #160) After \`induction Hstep; inversion Ht; subst\` + a light automation chain (econstructor / values_dont_step / EVar-can't-step), 33 subgoals remain. This change dispatches all 33 explicitly. ## What lands **29 closed to Qed** via: - Inline inversion + T_*_L1 reconstruction (10 cases) - IH-app + reconstructor (12 congruence cases) - subst_preserves_typing_l1 (5 β-reduction cases: S_Let_Val, S_LetLin_Val, S_App_Fun, S_Case_Inl, S_Case_Inr) - region_shrink_preserves_typing_l1 (S_Region_Exit) - T_Region_Active_L1 re-application (S_Region_Enter, S_Region_Step positive) **4 explicit \`admit.\`** — all bound to the same gap class: **region-env weakening for non-values**. | Case | Pattern | |---|---| | S_StringConcat_Step2 | value v1 left, e2 steps right | | S_App_Step2 | value v1 (function) left, e2 steps right | | S_Pair_Step2 | value v1 left, e2 steps right | | S_Region_Step (¬ In r R0' branch) | outer ERegion must re-type as T_Region_L1 — body lifted R0' → r::R0' | All four reduce to: lift a typing across an R0 → R0' shift caused by inner region steps. This is the **same structural lemma** that bounds the residual admits in \`region_shrink_preserves_typing_l1_gen\` (tasks #25/#26 in the project task list). S_Region_Step's positive case (\`In r R0'\`) closes via T_Region_Active_L1 + IH — bullet-split using \`in_dec string_dec\`, leaving only the negative branch as admit. ## Net admit accounting | Item | Before | After | |---|---|---| | \`region_shrink_preserves_typing_l1_gen\` internal admits | 2 | 2 | | Axiom \`loc_retype_at_R_l1\` | 1 | 1 | | \`preservation_l1\` body admits | 0 (single Admitted) | 4 | | Lemma-level \`Admitted.\` | 2 | 2 | The Admitted at the end of \`preservation_l1\` is unchanged (already there before). The 4 new admits are **sub-cases** of the same overall Admitted — the proof body now documents exactly which sub-cases remain. ## Build \`coqc Semantics_L1.v\` clean. No new axioms; no new \`Admitted.\` markers. ## Test plan - [x] \`make\` in formal/ builds clean - [x] Counterexample.v, TypingL1.v, Semantics.v unchanged (no co-impact) - [x] No new axioms introduced ## Follow-up Once the L1.B region-env weakening lemma lands (tasks #25/#26), all four L1.D admits should discharge by the same structural argument. After that, \`preservation_l1\` closes to Qed and the file's net admit count drops to 0 (modulo the loc_retype_at_R_l1 Axiom from L1.C). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 65d665e commit d0c5117

1 file changed

Lines changed: 255 additions & 13 deletions

File tree

‎formal/Semantics_L1.v‎

Lines changed: 255 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -895,24 +895,266 @@ Qed.
895895

896896
(** ** Preservation under the L1 judgment.
897897
898-
The full case-by-case proof depends on the three Admitted helpers
899-
above. Sequenced for incremental closure across follow-up PRs (per
900-
task #19 in the project's task list).
901-
902-
The simple cases (S_StringNew, S_StringConcat, S_StringLen,
903-
S_If_True, S_If_False, S_Region_Enter, S_Drop) were verified
904-
experimentally during this file's first-pass authoring; they close
905-
using only the lemmas already Qed in TypingL1.v + this file. They
906-
are not currently inlined into the proof body because the bullet
907-
structure picks up the per-step typing-rule cross-cases (e.g.
908-
ERegion's T_Region_L1 vs T_Region_Active_L1) which doubles the
909-
subgoal count over the step rule count. The clean-bullet structure
910-
is sequenced together with the three helpers landing. *)
898+
Case-by-case inversion + reconstruction over [step]. The proof
899+
closes 29 of 33 residual subgoals (post-automation chain); the
900+
4 explicit [admit.]s all surface the same gap class — **region-env
901+
weakening for non-values**:
902+
903+
- S_StringConcat_Step2 / S_App_Step2 / S_Pair_Step2: value v1
904+
sits to the left of a stepping subexpression. After the inner
905+
step changes R0 → R0', v1's typing needs to be lifted from R0
906+
to R0'.
907+
908+
- S_Region_Step (negative branch of [In r R0']): the outer
909+
[ERegion r e'] must re-type as T_Region_L1, requiring the
910+
inner body to be lifted from R0' to (r :: R0').
911+
912+
All four reduce to: given a typing under [R0], lift it to [R0']
913+
where R0' may add or drop regions that the operational step has
914+
determined. This is the same structural gap as the residual admits
915+
in [region_shrink_preserves_typing_l1_gen] (tasks #25/#26 in the
916+
project's task list).
917+
918+
Until the weakening lemma lands, [preservation_l1] is closed with
919+
[Admitted.] but the proof body documents exactly which sub-cases
920+
remain — no other obligations are buried. *)
911921

912922
Theorem preservation_l1 :
913923
forall mu R e mu' R' e',
914924
step (mu, R, e) (mu', R', e') ->
915925
forall G T R_final G',
916926
has_type_l1 R G e T R_final G' ->
917927
has_type_l1 R' G e' T R_final G'.
928+
Proof.
929+
intros mu R e mu' R' e' Hstep.
930+
remember (mu, R, e) as cfg eqn:Hcfg.
931+
remember (mu', R', e') as cfg' eqn:Hcfg'.
932+
revert mu R e mu' R' e' Hcfg Hcfg'.
933+
induction Hstep; intros mu0 R0 e0 mu0' R0' e0' Hcfg Hcfg';
934+
inversion Hcfg; clear Hcfg; subst;
935+
inversion Hcfg'; clear Hcfg'; subst;
936+
intros G0 T0 R_final G0' Ht;
937+
inversion Ht; subst;
938+
(* Light closure pass — handles ~atomic cases and discharges
939+
value-step impossibilities. *)
940+
try solve [econstructor; eassumption];
941+
try solve [econstructor; econstructor; eassumption];
942+
try solve [exfalso; eapply values_dont_step; eassumption];
943+
try solve [exfalso; congruence];
944+
try solve [exfalso; discriminate];
945+
try solve [match goal with
946+
| [ H : (_, _, EVar _) -->> _ |- _ ] => inversion H
947+
end].
948+
(* 33 residual goals — dispatched explicitly. *)
949+
- (* 1. S_StringConcat (β): EStringConcat (ELoc l1 r) (ELoc l2 r) → ELoc l' r *)
950+
match goal with
951+
| [ H : _; _ |=L1 ELoc _ _ : _ -| _; _ |- _ ] => inversion H; subst
952+
end.
953+
match goal with
954+
| [ H : _; _ |=L1 ELoc _ _ : _ -| _; _ |- _ ] => inversion H; subst
955+
end.
956+
econstructor; assumption.
957+
- (* 2. S_StringConcat_Step1 *)
958+
eapply T_StringConcat_L1;
959+
[ eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption
960+
| eassumption ].
961+
- (* 3. S_StringConcat_Step2: value v1 left, e2 steps right.
962+
Needs region-env weakening on the value v1 (lift its typing
963+
from R to R'). Same gap class as the residual admits in
964+
[region_shrink_preserves_typing_l1_gen] (tasks #25/#26).
965+
Admit for L1.D scaffold. *)
966+
admit.
967+
- (* 4. S_StringLen (β): EStringLen (ELoc l r) → EI32 (length s) *)
968+
match goal with
969+
| [ H : _; _ |=L1 EBorrow (ELoc _ _) : _ -| _; _ |- _ ] =>
970+
let Hv := fresh in
971+
assert (Hv : is_value (EBorrow (ELoc l r))) by repeat constructor;
972+
pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ Hv H) as [HR HG];
973+
subst
974+
end.
975+
constructor.
976+
- (* 5. S_StringLen_Step: inner e steps but EBorrow e typed by either
977+
T_Borrow_L1 (e=EVar, can't step) or T_Borrow_Val_L1 (e is value,
978+
can't step). Both are vacuous. *)
979+
match goal with
980+
| [ H : _; _ |=L1 EBorrow _ : _ -| _; _ |- _ ] => inversion H; subst
981+
end.
982+
+ (* T_Borrow_L1: e = EVar i — no step rule fires on EVar *)
983+
inversion Hstep.
984+
+ (* T_Borrow_Val_L1: e is a value — values don't step *)
985+
exfalso; eapply values_dont_step; eassumption.
986+
- (* 6. S_Let_Val (β): ELet v1 e2 → subst 0 v1 e2 *)
987+
match goal with
988+
| [ Hv : is_value ?v1, Ht1 : ?R; ?G |=L1 ?v1 : _ -| _; _ |- _ ] =>
989+
pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ Hv Ht1) as [HR HG];
990+
subst
991+
end.
992+
eapply subst_preserves_typing_l1; try eassumption.
993+
- (* 7. S_Let_Step *)
994+
eapply T_Let_L1;
995+
[ eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption
996+
| eassumption ].
997+
- (* 8. S_LetLin_Val (β) *)
998+
match goal with
999+
| [ Hv : is_value ?v1, Ht1 : ?R; ?G |=L1 ?v1 : _ -| _; _ |- _ ] =>
1000+
pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ Hv Ht1) as [HR HG];
1001+
subst
1002+
end.
1003+
eapply subst_preserves_typing_l1; try eassumption.
1004+
- (* 9. S_LetLin_Step *)
1005+
eapply T_LetLin_L1;
1006+
[ eassumption
1007+
| eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption
1008+
| eassumption ].
1009+
- (* 10. S_App_Fun (β): EApp (ELam T ebody) v2 → subst 0 v2 ebody *)
1010+
match goal with
1011+
| [ H : _; _ |=L1 ELam _ _ : _ -| _; _ |- _ ] => inversion H; subst
1012+
end.
1013+
match goal with
1014+
| [ Hv : is_value ?v2, Ht2 : ?R; ?G |=L1 ?v2 : _ -| _; _ |- _ ] =>
1015+
pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ Hv Ht2) as [HR HG];
1016+
subst
1017+
end.
1018+
eapply subst_preserves_typing_l1; try eassumption.
1019+
- (* 11. S_App_Step1 *)
1020+
eapply T_App_L1;
1021+
[ eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption
1022+
| eassumption ].
1023+
- (* 12. S_App_Step2: value v1 left (function), e2 steps right.
1024+
Same region-env weakening gap as goal 3. Admit. *)
1025+
admit.
1026+
- (* 13. S_If_True *)
1027+
match goal with
1028+
| [ H : _; _ |=L1 EBool _ : _ -| _; _ |- _ ] => inversion H; subst
1029+
end.
1030+
eassumption.
1031+
- (* 14. S_If_False *)
1032+
match goal with
1033+
| [ H : _; _ |=L1 EBool _ : _ -| _; _ |- _ ] => inversion H; subst
1034+
end.
1035+
eassumption.
1036+
- (* 15. S_If_Step *)
1037+
eapply T_If_L1;
1038+
[ eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption
1039+
| eassumption
1040+
| eassumption ].
1041+
- (* 16. S_Pair_Step1 *)
1042+
eapply T_Pair_L1;
1043+
[ eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption
1044+
| eassumption ].
1045+
- (* 17. S_Pair_Step2: value v1 left, e2 steps right.
1046+
Same region-env weakening gap as goal 3. Admit. *)
1047+
admit.
1048+
- (* 18. S_Fst *)
1049+
match goal with
1050+
| [ H : _; _ |=L1 EPair _ _ : _ -| _; _ |- _ ] => inversion H; subst
1051+
end.
1052+
repeat match goal with
1053+
| [ Hv : is_value ?v, Ht : ?R; ?G |=L1 ?v : _ -| _; _ |- _ ] =>
1054+
pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ Hv Ht) as [?HR ?HG];
1055+
subst; clear Hv
1056+
end.
1057+
eassumption.
1058+
- (* 19. S_Fst_Step *)
1059+
eapply T_Fst_L1;
1060+
[ eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption
1061+
| eassumption ].
1062+
- (* 20. S_Snd *)
1063+
match goal with
1064+
| [ H : _; _ |=L1 EPair _ _ : _ -| _; _ |- _ ] => inversion H; subst
1065+
end.
1066+
repeat match goal with
1067+
| [ Hv : is_value ?v, Ht : ?R; ?G |=L1 ?v : _ -| _; _ |- _ ] =>
1068+
pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ Hv Ht) as [?HR ?HG];
1069+
subst; clear Hv
1070+
end.
1071+
eassumption.
1072+
- (* 21. S_Snd_Step *)
1073+
eapply T_Snd_L1;
1074+
[ eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption
1075+
| eassumption ].
1076+
- (* 22. S_Inl_Step *)
1077+
eapply T_Inl_L1.
1078+
eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption.
1079+
- (* 23. S_Inr_Step *)
1080+
eapply T_Inr_L1.
1081+
eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption.
1082+
- (* 24. S_Case_Inl (β): ECase (EInl T v) e1 e2 → subst 0 v e1 *)
1083+
match goal with
1084+
| [ H : _; _ |=L1 EInl _ _ : _ -| _; _ |- _ ] => inversion H; subst
1085+
end.
1086+
match goal with
1087+
| [ Hv : is_value ?v, Ht : ?R; ?G |=L1 ?v : _ -| _; _ |- _ ] =>
1088+
pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ Hv Ht) as [HR HG];
1089+
subst
1090+
end.
1091+
eapply subst_preserves_typing_l1; try eassumption.
1092+
- (* 25. S_Case_Inr (β): ECase (EInr T v) e1 e2 → subst 0 v e2 *)
1093+
match goal with
1094+
| [ H : _; _ |=L1 EInr _ _ : _ -| _; _ |- _ ] => inversion H; subst
1095+
end.
1096+
match goal with
1097+
| [ Hv : is_value ?v, Ht : ?R; ?G |=L1 ?v : _ -| _; _ |- _ ] =>
1098+
pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ Hv Ht) as [HR HG];
1099+
subst
1100+
end.
1101+
eapply subst_preserves_typing_l1; try eassumption.
1102+
- (* 26. S_Case_Step *)
1103+
eapply T_Case_L1;
1104+
[ eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption
1105+
| eassumption
1106+
| eassumption ].
1107+
- (* 27. S_Region_Enter: (mu, R, ERegion r e) → (mu, r::R, ERegion r e).
1108+
Typing came in as T_Region_L1 (since ~ In r R from the step
1109+
contradicts T_Region_Active's In r R). After the step, r IS in
1110+
r :: R, so re-type as T_Region_Active_L1. *)
1111+
eapply T_Region_Active_L1.
1112+
+ left; reflexivity.
1113+
+ assumption.
1114+
+ assumption.
1115+
+ assumption.
1116+
- (* 28. S_Region_Exit: needs region_shrink_preserves_typing_l1.
1117+
The goal's R_final = remove_first_L1 r R_body; the helper produces
1118+
remove_first r R_body. Use [remove_first_eq_l1] to convert. *)
1119+
match goal with
1120+
| [ |- _; _ |=L1 _ : _ -| remove_first_L1 ?r ?R; _ ] =>
1121+
replace (remove_first_L1 r R) with (remove_first r R)
1122+
by (symmetry; apply remove_first_eq_l1)
1123+
end.
1124+
eapply region_shrink_preserves_typing_l1; eassumption.
1125+
- (* 29. S_Region_Step: IH gives R'; G |=L1 e' : T -| R_body; G'.
1126+
Need: R'; G |=L1 ERegion r e' : T -| remove_first_L1 r R_body; G'.
1127+
Case-split on [In r R0']. The positive case applies
1128+
T_Region_Active_L1 directly. The negative case requires region-
1129+
env weakening (lifting body typing from R0' to r :: R0'); same
1130+
gap class as [region_shrink_preserves_typing_l1_gen]'s residual
1131+
admits (tasks #25/#26). *)
1132+
destruct (in_dec string_dec r R0') as [HInR' | HNotInR'].
1133+
+ (* In r R0': use T_Region_Active_L1 *)
1134+
eapply T_Region_Active_L1; try eassumption.
1135+
eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption.
1136+
+ (* ~ In r R0': would need (r :: R0'); G |- e' : T -| R_body; G'
1137+
from IH which only gives R0'; G |- e' : T -| R_body; G'.
1138+
Region-env weakening for non-values. Deferred. *)
1139+
admit.
1140+
- (* 30. S_Drop *)
1141+
match goal with
1142+
| [ H : _; _ |=L1 ELoc _ _ : _ -| _; _ |- _ ] => inversion H; subst
1143+
end.
1144+
econstructor.
1145+
- (* 31. S_Drop_Step *)
1146+
eapply T_Drop_L1;
1147+
[ eassumption
1148+
| eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption ].
1149+
- (* 32. S_Copy *)
1150+
match goal with
1151+
| [ Hv : is_value ?v, Ht : ?R; ?G |=L1 ?v : _ -| _; _ |- _ ] =>
1152+
pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ Hv Ht) as [HR HG];
1153+
subst
1154+
end.
1155+
econstructor; eassumption.
1156+
- (* 33. S_Copy_Step *)
1157+
eapply T_Copy_L1;
1158+
[ eassumption
1159+
| eapply (IHHstep _ _ _ _ _ _ eq_refl eq_refl); eassumption ].
9181160
Admitted.

0 commit comments

Comments
 (0)