ed636a1aa2
GolangLean/Core/Preservation.lean:
theorem preservation:
HasType Γ e T -> HasTypeH ht h -> HasTypeEnv ht env Γ ->
BigStep h env e v h' ->
∃ ht', HeapTy.extends ht ht' /\ HasTypeH ht' h' /\
HasTypeV ht' v T /\ HasTypeEnv ht' env Γ
The standard big-step type-soundness result: well-typed terminating
programs produce well-typed values, with heap conformance preserved.
Proof is by induction on the big-step derivation, fourteen cases.
Supporting infrastructure:
HeapTy.extends_push - heap-typing extends across a push
HasTypeH.push - heap conformance preserved by push
HasTypeH.setIfInBounds - heap conformance preserved by in-bounds update
binop_apply_sound - operator typing matches operator semantics
The closure case (appR) uses the mutual HasTypeV/HasTypeEnv weakening
lemmas from TypeSoundness to thread heap-typings across the three
sub-derivations. The assign case (assignR) uses the heap-update
lemma to preserve conformance. The if-cases collapse the cross-rule
(ifT vs ifF) ambiguity via Bool.noConfusion on the condition's IH.
Zero sorries / axioms / admits across the project. Full lake build clean.
20 lines
550 B
Text
20 lines
550 B
Text
import GolangLean.Error
|
|
import GolangLean.Token
|
|
import GolangLean.AST
|
|
import GolangLean.Value
|
|
import GolangLean.Env
|
|
import GolangLean.Scanner
|
|
import GolangLean.Parser
|
|
import GolangLean.Eval
|
|
import GolangLean.Builtins
|
|
import GolangLean.REPL
|
|
import GolangLean.PureEval
|
|
import GolangLean.BigStep
|
|
import GolangLean.ValueEquiv
|
|
import GolangLean.Core.Syntax
|
|
import GolangLean.Core.Semantics
|
|
import GolangLean.Core.Determinism
|
|
import GolangLean.Core.Eval
|
|
import GolangLean.Core.Types
|
|
import GolangLean.Core.TypeSoundness
|
|
import GolangLean.Core.Preservation
|