Skip to content

Commit f499c82

Browse files
claudeclaude
committed
proof(coq): step_preserves_type clone-out — 8 more cases (12 of 35 remain)
Mechanical clone-out of step_preserves_type tactics for the single-pattern cases. Closes: Cluster B (congruence) via direct IH: - S_Inl_Step, S_Inr_Step (TSum T1 T2) - S_Drop_Step (vacuous-via-IH; outer T = TBase TUnit) - S_Copy_Step (TProd T T symmetric) - S_Fst_Step, S_Snd_Step (IH gives TProd alignment; injection extracts the relevant component) - S_Borrow_Step (vacuous via inversion chain — EVar/value can't step) Atomic / region: - S_Region_Enter (4-sub-goal inversion + type_determinacy on inner expression e at common (r :: R) context) Open (12 of 35): | Category | Cases | Blocker | |----------|-------|---------| | Pair / App / StringConcat second-child / Step1 | 4 | IH + type_determinacy on unchanged sibling for BOTH T1 AND T2 components | | Let / LetLin / Case | 3 | ctx_extend-with-unfixed-T1 needs explicit binder consistency | | If_Step | 1 | branch ctx_types_agree composition | | Copy atomic (EPair v v) | 1 | is_linear_ty premise discharge | | Fst / Snd atomic | 2 | pattern-var binding through nested match | | Region_Exit | 1 | as documented | | Region_Step (Phase 3) | 1 | region-env weakening blocker | Each remaining case is tractable with a bespoke tactic — the patterns are documented in the comment block; the work is purely case-specific Coq tactic engineering rather than research-level proof discovery. Build: coqc 8.18.0 green. Admitted: 3 (step_preserves_type, step_output_context_eq, preservation). Session progress recap: - 12 commits to PR #124. - Lemma B: 28 of 35 (80%) — every closable case closed. - step_preserves_type: 23 of 35 (66%) — IH-driven recipe proven viable, mass clone-out done. - Helpers Qed: output_ctx_det, subst_preserves_typing_strong, ctx_types_agree_sym, ctx_types_agree_trans.
1 parent cf058e3 commit f499c82

1 file changed

Lines changed: 369 additions & 7 deletions

File tree

‎formal/Semantics.v‎

Lines changed: 369 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3710,13 +3710,375 @@ Proof.
37103710
end
37113711
end
37123712
].
3713-
(* ~20 cases remain in step_preserves_type. Closed via the new
3714-
IH-driven recipe: S_StringConcat_Step1, S_App_Step1/Step2,
3715-
S_Let_Val, S_LetLin_Val, S_App_Fun, S_Case_Inl/Inr (and the
3716-
atomic-axiom group from the initial tactic). Remaining cases
3717-
would follow the same recipe + variations for second-child,
3718-
unary, and ternary congruence shapes. The structural template
3719-
is in place; finishing is purely mechanical clone work. *)
3713+
(* ===== Second-child congruences (inner step on e2, v1 value) ===== *)
3714+
(* S_StringConcat_Step2 *)
3715+
all: try solve [
3716+
match goal with
3717+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3718+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3719+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3720+
Hv : is_value ?v1,
3721+
Hte : has_type _ _ (EStringConcat ?v1 _) _ _,
3722+
Hte' : has_type _ _ (EStringConcat ?v1 _) _ _ |- _ ] =>
3723+
inversion Hte; subst;
3724+
inversion Hte'; subst;
3725+
match goal with
3726+
| [ H2 : has_type ?R ?Gmid ?e2 (TString ?r) ?Ga,
3727+
H2' : has_type ?R' ?Gmid' ?e2' (TString ?r') ?Gb |- _ ] =>
3728+
pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2 _ _ H2') as Hteq;
3729+
inversion Hteq; reflexivity
3730+
end
3731+
end
3732+
].
3733+
(* S_App_Step2 *)
3734+
all: try solve [
3735+
match goal with
3736+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3737+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3738+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3739+
Hv : is_value ?v1,
3740+
Hte : has_type _ _ (EApp ?v1 _) _ _,
3741+
Hte' : has_type _ _ (EApp ?v1 _) _ _ |- _ ] =>
3742+
inversion Hte; subst;
3743+
inversion Hte'; subst;
3744+
match goal with
3745+
| [ H1 : has_type ?R ?G ?v1 (TFun ?T1a ?T2a) ?Gmid,
3746+
H2 : has_type ?R ?Gmid ?e2 ?T1a ?Ga,
3747+
H1' : has_type ?R' ?G ?v1 (TFun ?T1b ?T2b) ?Gmid',
3748+
H2' : has_type ?R' ?Gmid' ?e2' ?T1b ?Gb |- _ ] =>
3749+
(* Align v1's TFun types via type_determinacy. *)
3750+
assert (HGm : Gmid = G) by
3751+
(eapply value_context_unchanged; eassumption);
3752+
subst Gmid;
3753+
assert (HGm' : Gmid' = G) by
3754+
(eapply value_context_unchanged; eassumption);
3755+
subst Gmid';
3756+
assert (HTfun : TFun T1a T2a = TFun T1b T2b)
3757+
by (eapply type_determinacy;
3758+
[exact H1 | exact H1' | apply ctx_types_agree_refl]);
3759+
inversion HTfun; subst;
3760+
pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2 _ _ H2') as Hteq;
3761+
exact Hteq
3762+
end
3763+
end
3764+
].
3765+
(* S_Pair_Step1, S_Pair_Step2: TProd T1 T2 outer constraints both children. *)
3766+
all: try solve [
3767+
match goal with
3768+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3769+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3770+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3771+
Hte : has_type _ _ (EPair _ _) _ _,
3772+
Hte' : has_type _ _ (EPair _ _) _ _ |- _ ] =>
3773+
inversion Hte; subst;
3774+
inversion Hte'; subst;
3775+
match goal with
3776+
| [ H1 : has_type ?R ?G ?e1 ?T1 ?Gmid,
3777+
H1' : has_type ?R' ?G ?e1' ?T1' ?Gmid' |- _ ] =>
3778+
pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 _ _ H1') as Hteq;
3779+
subst T1'; reflexivity
3780+
end
3781+
end
3782+
].
3783+
(* ===== Unary congruences (single child) ===== *)
3784+
(* S_Inl_Step: TSum T1 T2; outer T = TSum T1 T2 constrains T1. *)
3785+
all: try solve [
3786+
match goal with
3787+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3788+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3789+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3790+
Hte : has_type _ _ (EInl _ _) _ _,
3791+
Hte' : has_type _ _ (EInl _ _) _ _ |- _ ] =>
3792+
inversion Hte; subst;
3793+
inversion Hte'; subst;
3794+
match goal with
3795+
| [ H1 : has_type ?R ?G ?e ?T1 ?Ga,
3796+
H1' : has_type ?R' ?G ?e' ?T1' ?Gb |- _ ] =>
3797+
pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 _ _ H1') as Hteq;
3798+
subst T1'; reflexivity
3799+
end
3800+
end
3801+
].
3802+
(* S_Inr_Step: symmetric. *)
3803+
all: try solve [
3804+
match goal with
3805+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3806+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3807+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3808+
Hte : has_type _ _ (EInr _ _) _ _,
3809+
Hte' : has_type _ _ (EInr _ _) _ _ |- _ ] =>
3810+
inversion Hte; subst;
3811+
inversion Hte'; subst;
3812+
match goal with
3813+
| [ H1 : has_type ?R ?G ?e ?T2 ?Ga,
3814+
H1' : has_type ?R' ?G ?e' ?T2' ?Gb |- _ ] =>
3815+
pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 _ _ H1') as Hteq;
3816+
subst T2'; reflexivity
3817+
end
3818+
end
3819+
].
3820+
(* S_Borrow_Step: T_Borrow forces e = EVar (no step), T_Borrow_Val
3821+
forces e is value (no step). Vacuous. *)
3822+
all: try solve [
3823+
match goal with
3824+
| [ Hin : (_, _, _) -->> (_, _, _),
3825+
Hte : has_type _ _ (EBorrow _) _ _ |- _ ] =>
3826+
inversion Hte; subst;
3827+
[ inversion Hin
3828+
| exfalso;
3829+
match goal with
3830+
| [ Hv : is_value ?v |- _ ] =>
3831+
eapply values_dont_step; [exact Hv | exact Hin]
3832+
end
3833+
]
3834+
end
3835+
].
3836+
(* S_Drop_Step: T_Drop's inner type is independent; use sibling-
3837+
less approach via IH directly (the inner step's IH provides
3838+
type-equality even though outer T is fixed at TBase TUnit). *)
3839+
all: try solve [
3840+
match goal with
3841+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3842+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3843+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3844+
Hte : has_type _ _ (EDrop _) _ _,
3845+
Hte' : has_type _ _ (EDrop _) _ _ |- _ ] =>
3846+
inversion Hte; subst;
3847+
inversion Hte'; subst;
3848+
reflexivity
3849+
end
3850+
].
3851+
(* S_Copy_Step: T_Copy outputs TProd T T — symmetric. *)
3852+
all: try solve [
3853+
match goal with
3854+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3855+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3856+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3857+
Hte : has_type _ _ (ECopy _) _ _,
3858+
Hte' : has_type _ _ (ECopy _) _ _ |- _ ] =>
3859+
inversion Hte; subst;
3860+
inversion Hte'; subst;
3861+
match goal with
3862+
| [ H1 : has_type ?R ?G ?e ?Ta ?Ga,
3863+
H1' : has_type ?R' ?G ?e' ?Tb ?Gb |- _ ] =>
3864+
pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 _ _ H1') as Hteq;
3865+
subst Tb; reflexivity
3866+
end
3867+
end
3868+
].
3869+
(* S_If_Step: cond at TBase TBool, branches at outer T. *)
3870+
all: try solve [
3871+
match goal with
3872+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3873+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3874+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3875+
Hte : has_type _ _ (EIf _ _ _) _ _,
3876+
Hte' : has_type _ _ (EIf _ _ _) _ _ |- _ ] =>
3877+
inversion Hte; subst;
3878+
inversion Hte'; subst;
3879+
match goal with
3880+
| [ H2 : has_type ?R ?Gmid ?e2 ?T ?Ga,
3881+
H2' : has_type ?R' ?Gmid' ?e2 ?T' ?Gb |- _ ] =>
3882+
assert (HagrMid : ctx_types_agree Gmid Gmid')
3883+
by (apply (ctx_types_agree_trans _ _ _);
3884+
[ eapply typing_types_agree; eassumption
3885+
| apply ctx_types_agree_sym;
3886+
eapply typing_types_agree; eassumption ]);
3887+
eapply type_determinacy;
3888+
[ exact H2 | exact H2' | exact HagrMid ]
3889+
end
3890+
end
3891+
].
3892+
(* S_Fst_Step: T_Fst's T2 independent. Use IH directly — IH on
3893+
the inner step preserves type, so e and e' have same TProd type.
3894+
Output's T1 component (= outer T) follows. *)
3895+
all: try solve [
3896+
match goal with
3897+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3898+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3899+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3900+
Hte : has_type _ _ (EFst _) _ _,
3901+
Hte' : has_type _ _ (EFst _) _ _ |- _ ] =>
3902+
inversion Hte; subst;
3903+
inversion Hte'; subst;
3904+
match goal with
3905+
| [ H1 : has_type ?R ?G ?e (TProd ?Ta1 ?Ta2) ?Ga,
3906+
H1' : has_type ?R' ?G ?e' (TProd ?Tb1 ?Tb2) ?Gb |- _ ] =>
3907+
pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 _ _ H1') as Hteq;
3908+
inversion Hteq; reflexivity
3909+
end
3910+
end
3911+
].
3912+
(* S_Snd_Step: T_Snd's T1 independent. Symmetric. *)
3913+
all: try solve [
3914+
match goal with
3915+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3916+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3917+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3918+
Hte : has_type _ _ (ESnd _) _ _,
3919+
Hte' : has_type _ _ (ESnd _) _ _ |- _ ] =>
3920+
inversion Hte; subst;
3921+
inversion Hte'; subst;
3922+
match goal with
3923+
| [ H1 : has_type ?R ?G ?e (TProd ?Ta1 ?Ta2) ?Ga,
3924+
H1' : has_type ?R' ?G ?e' (TProd ?Tb1 ?Tb2) ?Gb |- _ ] =>
3925+
pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 _ _ H1') as Hteq;
3926+
inversion Hteq; reflexivity
3927+
end
3928+
end
3929+
].
3930+
(* S_Case_Step: scrutinee steps. Outer T comes from branches; IH
3931+
gives TSum T1 T2 alignment. *)
3932+
all: try solve [
3933+
match goal with
3934+
| [ IH : forall (_:mem) (_:region_env) (_:expr) (_:mem) (_:region_env) (_:expr),
3935+
_ = _ -> _ = _ -> forall (_:ctx) (_:ty) (_:ctx),
3936+
_ -> forall (_:ty) (_:ctx), _ -> _ = _,
3937+
Hte : has_type _ _ (ECase _ _ _) _ _,
3938+
Hte' : has_type _ _ (ECase _ _ _) _ _ |- _ ] =>
3939+
inversion Hte; subst;
3940+
inversion Hte'; subst;
3941+
match goal with
3942+
| [ Hs : has_type ?R ?G ?e (TSum ?Ta1 ?Ta2) ?Gmid,
3943+
Hb1 : has_type ?R (ctx_extend ?Gmid ?Ta1) ?eb1 ?T
3944+
((?Ta1, true) :: ?Gfin),
3945+
Hs' : has_type ?R' ?G ?e' (TSum ?Tb1 ?Tb2) ?Gmid',
3946+
Hb1' : has_type ?R' (ctx_extend ?Gmid' ?Tb1) ?eb1 ?T'
3947+
((?Tb1, true) :: ?Gfin') |- _ ] =>
3948+
pose proof (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ Hs _ _ Hs') as Hsum;
3949+
inversion Hsum; subst;
3950+
(* Now Ta1 = Tb1 and Ta2 = Tb2. Apply type_determinacy on
3951+
branch eb1 (same expression in agreeing contexts). *)
3952+
assert (HagrMid : ctx_types_agree Gmid Gmid')
3953+
by (apply (ctx_types_agree_trans _ _ _);
3954+
[ eapply typing_types_agree; eassumption
3955+
| apply ctx_types_agree_sym;
3956+
eapply typing_types_agree; eassumption ]);
3957+
assert (HagrExt : ctx_types_agree
3958+
(ctx_extend Gmid Ta1) (ctx_extend Gmid' Ta1))
3959+
by (apply ctx_extend_types_agree; assumption);
3960+
eapply type_determinacy;
3961+
[ exact Hb1 | exact Hb1' | exact HagrExt ]
3962+
end
3963+
end
3964+
].
3965+
(* ===== Atomic compound-value cases (post = some value form) ===== *)
3966+
(* S_Copy: ECopy v -> EPair v v. Hte (T_Copy) gives outer TProd T T;
3967+
Hte' (T_Pair) gives outer TProd Ta1 Ta2. By T_Copy structure,
3968+
Ta1 = Ta2 = v's type. *)
3969+
all: try solve [
3970+
match goal with
3971+
| [ Hv : is_value ?v,
3972+
Hte : has_type _ _ (ECopy _) _ _,
3973+
Hte' : has_type _ _ (EPair _ _) _ _ |- _ ] =>
3974+
inversion Hte; subst;
3975+
inversion Hte'; subst;
3976+
match goal with
3977+
| [ H1 : has_type ?R ?G ?v ?Ta ?Ga,
3978+
H1' : has_type ?R ?G ?v ?Tb ?Gmid |- _ ] =>
3979+
assert (HTeq : Ta = Tb)
3980+
by (eapply type_determinacy;
3981+
[ exact H1 | exact H1' | apply ctx_types_agree_refl ]);
3982+
subst Tb; reflexivity
3983+
end
3984+
end
3985+
].
3986+
(* S_Fst: EFst (EPair v1 v2) -> v1. *)
3987+
all: try solve [
3988+
match goal with
3989+
| [ Hv1 : is_value ?v1, Hv2 : is_value ?v2,
3990+
Hte : has_type _ _ (EFst (EPair ?v1 ?v2)) _ _,
3991+
Hte' : has_type _ _ ?v1 _ _ |- _ ] =>
3992+
inversion Hte; subst;
3993+
match goal with
3994+
| [ Hp : has_type ?R ?G (EPair ?v1 ?v2) (TProd ?T1 ?T2) ?Gpost |- _ ] =>
3995+
inversion Hp; subst;
3996+
match goal with
3997+
| [ Hv1t : has_type ?R ?G ?v1 ?T1 ?Gmid |- _ ] =>
3998+
assert (HTeq : T1 = _)
3999+
by (eapply type_determinacy;
4000+
[ exact Hv1t | exact Hte' | apply ctx_types_agree_refl ]);
4001+
exact HTeq
4002+
end
4003+
end
4004+
end
4005+
].
4006+
(* S_Snd: ESnd (EPair v1 v2) -> v2. *)
4007+
all: try solve [
4008+
match goal with
4009+
| [ Hv1 : is_value ?v1, Hv2 : is_value ?v2,
4010+
Hte : has_type _ _ (ESnd (EPair ?v1 ?v2)) _ _,
4011+
Hte' : has_type _ _ ?v2 _ _ |- _ ] =>
4012+
inversion Hte; subst;
4013+
match goal with
4014+
| [ Hp : has_type ?R ?G (EPair ?v1 ?v2) (TProd ?T1 ?T2) ?Gpost |- _ ] =>
4015+
inversion Hp; subst;
4016+
match goal with
4017+
| [ Hv2t : has_type _ _ ?v2 ?T2 _ |- _ ] =>
4018+
assert (HTeq : T2 = _)
4019+
by (eapply type_determinacy;
4020+
[ exact Hv2t | exact Hte' | apply ctx_types_agree_refl ]);
4021+
exact HTeq
4022+
end
4023+
end
4024+
end
4025+
].
4026+
(* S_Region_Exit: ERegion r v -> v (R becomes remove_first r R).
4027+
Hte is T_Region_Active; Hte' types v at T'. *)
4028+
all: try solve [
4029+
match goal with
4030+
| [ Hv : is_value ?v,
4031+
Hte : has_type _ _ (ERegion _ _) ?T _,
4032+
Hte' : has_type _ _ ?v ?T' _ |- ?T = ?T' ] =>
4033+
inversion Hte; subst;
4034+
match goal with
4035+
| [ Hvt : has_type ?R ?G ?v ?T ?Gmid |- _ ] =>
4036+
eapply type_determinacy;
4037+
[ exact Hvt | exact Hte' | apply ctx_types_agree_refl ]
4038+
end
4039+
end
4040+
].
4041+
(* S_Region_Enter: ERegion r e (under R) -> ERegion r e (under r::R).
4042+
Both Hte and Hte' invert to give inner e's typing under (r :: R).
4043+
The 4 inversion sub-goals split by T_Region / T_Region_Active. *)
4044+
all: try solve [
4045+
match goal with
4046+
| [ Hn : ~ In ?r _,
4047+
Hte : has_type _ _ (ERegion ?r ?e) ?T _,
4048+
Hte' : has_type _ _ (ERegion ?r ?e) ?T' _ |- ?T = ?T' ] =>
4049+
inversion Hte; subst;
4050+
inversion Hte'; subst;
4051+
first
4052+
[ exfalso; tauto
4053+
| exfalso;
4054+
match goal with
4055+
| [ H : ~ In ?r (?r :: _) |- _ ] =>
4056+
apply H; left; reflexivity
4057+
end
4058+
| match goal with
4059+
| [ H1 : has_type ?R ?G ?e ?T ?Ga,
4060+
H2 : has_type ?R ?G ?e ?T' ?Gb |- ?T = ?T' ] =>
4061+
eapply type_determinacy;
4062+
[ exact H1 | exact H2 | apply ctx_types_agree_refl ]
4063+
end ]
4064+
end
4065+
].
4066+
(* 12 cases remain. Each requires per-case adjustment beyond the
4067+
mass clone-out:
4068+
- S_Pair_Step1/2, S_App_Step2: need IH on stepping child +
4069+
type_determinacy on unchanged sibling to align BOTH outer
4070+
type components.
4071+
- S_StringConcat_Step2: similar to App_Step2.
4072+
- S_Let_Step, S_LetLin_Step, S_Case_Step: ctx_extend-with-
4073+
unfixed-T1 inversion needs explicit binder names that don't
4074+
match Coq's auto-renaming consistently.
4075+
- S_If_Step: inner step on cond e1 (TBase TBool); the e2/e3
4076+
branches need ctx_types_agree composition.
4077+
- S_Copy atomic (EPair v v from ECopy v): need extra
4078+
is_linear_ty premise discharge.
4079+
- S_Fst, S_Snd atomic: pattern var bind to outer goal's T
4080+
doesn't propagate through nested match cleanly.
4081+
- S_Region_Exit, S_Region_Step: as documented. *)
37204082
all: admit.
37214083
Admitted.
37224084

0 commit comments

Comments
 (0)