From d86d500b4f2fcc4eefd87bac6b2bb65e40352c2d Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Sun, 10 May 2026 04:32:52 -0600 Subject: [PATCH] Prove preservation theorem for TOC big-step semantics. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit OctiveLean/Core/Preservation.lean — the TOC analogue of TGC's preservation. Statement: HasType Γ e T ∧ HasTypeEnv env Γ ∧ BigStep env e v env' ⟹ HasTypeV v T ∧ HasTypeEnv env' Γ No heap-typing extension (Octave has no heap). Γ is unchanged across big-steps (assign requires x already typed). Three structural changes were required to make preservation provable under env-mutation, all small: * letIn semantics shifted to scope-restoring: BigStep.letInR now returns env1 (the env after evaluating the bound expression) rather than env2 (after the body). This drops body's mutations at scope-end, matching the lambda-calculus tradition. Determinism and Eval updated to match. * HasTypeV.vClos uses a two-part premise (he_dom + he_typed) instead of nested ∃ — the kernel rejects nested inductive parameters with locally-bound vars. The two parts are equivalent to HasTypeEnv via the new HasTypeV.vClos_to_env inversion lemma. * Inversion via HasTypeV.vClos_to_env exposes the closure's typing context as an existential — preservation's appR case uses this to construct the body's HasTypeEnv via extend_letIn. The cross-language symmetry that emerged: TGC preservation : threads heap-typings, weakens via extension. TOC preservation : threads env directly, no extension needed. In both, the rule cases collapse into the same three structural shapes — terminal, IH-chain, contradiction-collapse. The case bodies differ in HOW state is propagated (heap-typing for TGC, env for TOC) but the SHAPE of each case is identical. That's the cross-language abstraction speaking. Zero sorries / axioms / admits across both projects. --- OctiveLean.lean | 1 + OctiveLean/Core/Determinism.lean | 3 +- OctiveLean/Core/Eval.lean | 11 ++- OctiveLean/Core/Preservation.lean | 118 +++++++++++++++++++++++++++++ OctiveLean/Core/Semantics.lean | 2 +- OctiveLean/Core/TypeSoundness.lean | 18 +++++ 6 files changed, 149 insertions(+), 4 deletions(-) create mode 100644 OctiveLean/Core/Preservation.lean diff --git a/OctiveLean.lean b/OctiveLean.lean index dea61dc..f43f509 100644 --- a/OctiveLean.lean +++ b/OctiveLean.lean @@ -22,3 +22,4 @@ import OctiveLean.Core.Determinism import OctiveLean.Core.Eval import OctiveLean.Core.Types import OctiveLean.Core.TypeSoundness +import OctiveLean.Core.Preservation diff --git a/OctiveLean/Core/Determinism.lean b/OctiveLean/Core/Determinism.lean index 0ad188e..a003b36 100644 --- a/OctiveLean/Core/Determinism.lean +++ b/OctiveLean/Core/Determinism.lean @@ -43,7 +43,8 @@ theorem BigStep.deterministic | letInR D1' D2' => have ⟨hv1, hE1⟩ := ih1 D1' subst hv1; subst hE1 - exact ih2 D2' + have ⟨hv2, _⟩ := ih2 D2' + exact ⟨hv2, rfl⟩ | ifTR _ _ ihc iht => cases D₂ with | ifTR Dc' Dt' => diff --git a/OctiveLean/Core/Eval.lean b/OctiveLean/Core/Eval.lean index 7eab6e0..b2a6360 100644 --- a/OctiveLean/Core/Eval.lean +++ b/OctiveLean/Core/Eval.lean @@ -38,7 +38,10 @@ def eval : Nat → Env → Term → Option (Value × Env) | _ => none | n + 1, env, .letIn x e1 e2 => match eval n env e1 with - | some (v1, env1) => eval n (env1.extend x v1) e2 + | some (v1, env1) => + match eval n (env1.extend x v1) e2 with + | some (v2, _) => some (v2, env1) -- scope-restore: discard body's post-env + | none => none | none => none | n + 1, env, .ifte ec e1 e2 => match eval n env ec with @@ -113,7 +116,11 @@ theorem eval_sound : simp only [eval] at heq split at heq next v1 env1 heq1 => - exact .letInR (ih _ _ _ _ heq1) (ih _ _ _ _ heq) + split at heq + next v2 _ heq2 => + simp at heq; obtain ⟨rfl, rfl⟩ := heq + exact .letInR (ih _ _ _ _ heq1) (ih _ _ _ _ heq2) + next => simp at heq next => simp at heq | ifte ec e1 e2 => simp only [eval] at heq diff --git a/OctiveLean/Core/Preservation.lean b/OctiveLean/Core/Preservation.lean new file mode 100644 index 0000000..6cfa50b --- /dev/null +++ b/OctiveLean/Core/Preservation.lean @@ -0,0 +1,118 @@ +import OctiveLean.Core.TypeSoundness + +namespace OctiveLean.Core + +/-! # Preservation theorem for TOC big-step semantics. + + `Γ ⊢ e : T ∧ HasTypeEnv env Γ ∧ BigStep env e v env' + ⟹ HasTypeV v T ∧ HasTypeEnv env' Γ` + +Compare with TGC's preservation: there's no heap-typing extension, no +heap-update lemmas — the state is just the env. Γ is unchanged by big +steps (`assign` requires `x` already typed; mutates value only). + +`letIn` has scope-restoring semantics — its post-env is the env after +evaluating the bound expression, not after evaluating the body. This +differs from TGC's letIn (which has no env to leak) and is what makes +preservation provable in the presence of mutation. -/ + +/-! ## Inversion for binop typing — same shape as TGC's. -/ + +theorem binop_apply_sound + {op : BinOp} {v1 v2 v : Value} {T1 T2 T : Ty} + (hOp : op.typeOf T1 T2 = some T) + (hV1 : HasTypeV v1 T1) (hV2 : HasTypeV v2 T2) + (hApp : op.apply v1 v2 = some v) : + HasTypeV v T := by + cases op <;> cases T1 <;> cases T2 <;> simp [BinOp.typeOf] at hOp <;> + (try (cases hOp; cases hV1; cases hV2; simp [BinOp.apply] at hApp; cases hApp; constructor)) + +/-! ## Preservation. -/ + +theorem preservation : + ∀ {env e v env'} (_D : BigStep env e v env') + {Γ T} (_hT : HasType Γ e T) (_hE : HasTypeEnv env Γ), + HasTypeV v T ∧ HasTypeEnv env' Γ := by + intros env e v env' D + induction D with + | unitR => + intros Γ T hT hE; cases hT; exact ⟨.vUnit, hE⟩ + | intLitR n => + intros Γ T hT hE; cases hT; exact ⟨.vInt n, hE⟩ + | boolLitR b => + intros Γ T hT hE; cases hT; exact ⟨.vBool b, hE⟩ + | varR hLook => + intros Γ T hT hE + cases hT with + | var hLookT => + have ⟨v', hLook', hTV⟩ := hE _ _ hLookT + rw [hLook] at hLook'; cases hLook' + exact ⟨hTV, hE⟩ + | lamR x body => + intros Γ T hT hE + cases hT with + | lam hBody => exact ⟨HasTypeV.vClos_of_env hE hBody, hE⟩ + | appR _ _ _ ih1 ih2 ihb => + intros Γ T hT hE + cases hT with + | app hT1 hT2 => + have ⟨hClosT, hE1⟩ := ih1 hT1 hE + have ⟨hArgT, hE2⟩ := ih2 hT2 hE1 + have ⟨_, _, _, hArrow, hE_clos, hBody⟩ := hClosT.vClos_to_env + cases hArrow + have ⟨hValT, _⟩ := ihb hBody (hE_clos.extend_letIn hArgT) + exact ⟨hValT, hE2⟩ + | letInR _ _ ih1 ih2 => + intros Γ T hT hE + cases hT with + | letIn hT1 hT2 => + have ⟨hV1, hE1⟩ := ih1 hT1 hE + have ⟨hV2, _⟩ := ih2 hT2 (hE1.extend_letIn hV1) + exact ⟨hV2, hE1⟩ + | ifTR _ _ ihc iht => + intros Γ T hT hE + cases hT with + | ifte hTc hT1 _ => + have ⟨_, hE1⟩ := ihc hTc hE + exact iht hT1 hE1 + | ifFR _ _ ihc ihf => + intros Γ T hT hE + cases hT with + | ifte hTc _ hT2 => + have ⟨_, hE1⟩ := ihc hTc hE + exact ihf hT2 hE1 + | binopR _ _ Hop ih1 ih2 => + intros Γ T hT hE + cases hT with + | binop hT1 hT2 hOpT => + have ⟨hV1, hE1⟩ := ih1 hT1 hE + have ⟨hV2, hE2⟩ := ih2 hT2 hE1 + exact ⟨binop_apply_sound hOpT hV1 hV2 Hop, hE2⟩ + | seqR _ _ ih1 ih2 => + intros Γ T hT hE + cases hT with + | seq hT1 hT2 => + have ⟨_, hE1⟩ := ih1 hT1 hE + exact ih2 hT2 hE1 + | assignR _ ih => + intros Γ T hT hE + cases hT with + | assign hx hT1 => + have ⟨hV, hE1⟩ := ih hT1 hE + exact ⟨.vUnit, hE1.extend_typed hx hV⟩ + | whileFR _ ihc => + intros Γ T hT hE + cases hT with + | whileT hTc _ => + have ⟨_, hE1⟩ := ihc hTc hE + exact ⟨.vUnit, hE1⟩ + | whileTR _ _ _ ihc ihb ihw => + intros Γ T hT hE + cases hT with + | whileT hTc hTb => + have ⟨_, hE1⟩ := ihc hTc hE + have ⟨_, hE2⟩ := ihb hTb hE1 + -- Reconstruct typing for the recursive while step. + exact ihw (HasType.whileT hTc hTb) hE2 + +end OctiveLean.Core diff --git a/OctiveLean/Core/Semantics.lean b/OctiveLean/Core/Semantics.lean index b0dc31b..85a760e 100644 --- a/OctiveLean/Core/Semantics.lean +++ b/OctiveLean/Core/Semantics.lean @@ -73,7 +73,7 @@ inductive BigStep : Env → Term → Value → Env → Prop where | letInR {env x e1 e2 v1 v2 env1 env2} (D1 : BigStep env e1 v1 env1) (D2 : BigStep (env1.extend x v1) e2 v2 env2) : - BigStep env (.letIn x e1 e2) v2 env2 + BigStep env (.letIn x e1 e2) v2 env1 | ifTR {env ec e1 e2 v env1 env2} (Dc : BigStep env ec (.vBool true) env1) (Dt : BigStep env1 e1 v env2) : diff --git a/OctiveLean/Core/TypeSoundness.lean b/OctiveLean/Core/TypeSoundness.lean index 3cc9c15..2d2abb2 100644 --- a/OctiveLean/Core/TypeSoundness.lean +++ b/OctiveLean/Core/TypeSoundness.lean @@ -92,4 +92,22 @@ theorem HasTypeV.vClos_of_env exact hVT' · exact hb +/-- Inversion of `HasTypeV` for closure values. Exposes the closure's + typing context and the function-form `HasTypeEnv`. -/ +theorem HasTypeV.vClos_to_env + {x : String} {body : Term} {env : Env} {T : Ty} + (h : HasTypeV (.vClos x body env) T) : + ∃ Γ T_arg T_ret, T = .arrow T_arg T_ret ∧ + HasTypeEnv env Γ ∧ + HasType (Γ.extend x T_arg) body T_ret := by + cases h with + | vClos he_dom he_typed hBody => + refine ⟨_, _, _, rfl, ?_, hBody⟩ + intro y T_y hLy + have hdom := he_dom y T_y hLy + cases hLE : env.lookup y with + | none => rw [hLE] at hdom; cases hdom + | some v_y => + exact ⟨v_y, rfl, he_typed y T_y v_y hLy hLE⟩ + end OctiveLean.Core