Add executable evaluator (Phase A) and type system + soundness infra (Phase B).
Phase A — GolangLean/Core/Eval.lean:
def eval : Nat -> Heap -> Env -> Term -> Option (Value x Heap)
Fuel-bounded recursive evaluator, total over the fuel.
theorem eval_sound: eval succeeds => BigStep holds.
Bridges executable computation to inductive specification.
Phase B — GolangLean/Core/Types.lean:
inductive Ty {unit, int, bool, arrow, ref}
TyEnv := List (String x Ty); BinOp.typeOf
inductive HasType : TyEnv -> Term -> Ty -> Prop
Standard simply-typed lambda calculus + ML-style references.
Phase B — GolangLean/Core/TypeSoundness.lean:
abbrev HeapTy := Array Ty
mutual inductive HasTypeV / HasTypeEnv (value & env typing under heap-typing)
def HasTypeH (heap conforms to heap-typing)
def HeapTy.extends (prefix-extension of heap-typings)
thm HeapTy.extends_refl, extends_trans
thm HasTypeV.weaken, HasTypeEnv.weaken (mutual; under heap-typing extension)
thm HasTypeEnv.lookup_correspondence (well-typed env yields well-typed values)
The preservation theorem itself
HasType /\ HasTypeH /\ HasTypeEnv /\ BigStep
==> ∃ ht', extends /\ HasTypeH' /\ HasTypeV' /\ HasTypeEnv'
is the next deliverable; the infrastructure here is what its proof
case-analysis depends on.
Zero sorries / axioms / admits across the project. Full lake build clean.
This commit is contained in:
Maximus Gorog
parent
878a84e072
commit
3174918193
4 changed files with 384 additions and 0 deletions
|
|
@ -14,3 +14,6 @@ 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
|
||||
|
|
|
|||
190
GolangLean/Core/Eval.lean
Normal file
190
GolangLean/Core/Eval.lean
Normal file
|
|
@ -0,0 +1,190 @@
|
|||
import GolangLean.Core.Semantics
|
||||
|
||||
namespace GolangLean.Core
|
||||
|
||||
/-! # Executable evaluator and soundness.
|
||||
|
||||
A fuel-bounded recursive evaluator
|
||||
`eval : Nat → Heap → Env → Term → Option (Value × Heap)`
|
||||
together with the soundness theorem
|
||||
`eval n h env e = some (v, h') → BigStep h env e v h'`.
|
||||
|
||||
Soundness is the bridge that makes the inductive specification *runnable*.
|
||||
For any closed TGC term you can write a Lean theorem of the form
|
||||
`BigStep h env e v h'`
|
||||
and prove it by `decide`-style execution: run `eval`, then apply
|
||||
`eval_sound` to the equation. -/
|
||||
|
||||
def eval : Nat → Heap → Env → Term → Option (Value × Heap)
|
||||
| 0, _, _, _ => none
|
||||
| _ + 1, h, _, .unitT => some (.vUnit, h)
|
||||
| _ + 1, h, _, .intLit k => some (.vInt k, h)
|
||||
| _ + 1, h, _, .boolLit b => some (.vBool b, h)
|
||||
| _ + 1, h, env, .var x =>
|
||||
match env.lookup x with
|
||||
| some v => some (v, h)
|
||||
| none => none
|
||||
| _ + 1, h, env, .lam x body => some (.vClos x body env, h)
|
||||
| n + 1, h, env, .app e1 e2 =>
|
||||
match eval n h env e1 with
|
||||
| some (.vClos x body env', h1) =>
|
||||
match eval n h1 env e2 with
|
||||
| some (v2, h2) => eval n h2 (env'.extend x v2) body
|
||||
| none => none
|
||||
| _ => none
|
||||
| n + 1, h, env, .letIn x e1 e2 =>
|
||||
match eval n h env e1 with
|
||||
| some (v1, h1) => eval n h1 (env.extend x v1) e2
|
||||
| none => none
|
||||
| n + 1, h, env, .ifte ec e1 e2 =>
|
||||
match eval n h env ec with
|
||||
| some (.vBool true, h1) => eval n h1 env e1
|
||||
| some (.vBool false, h1) => eval n h1 env e2
|
||||
| _ => none
|
||||
| n + 1, h, env, .binop op e1 e2 =>
|
||||
match eval n h env e1 with
|
||||
| some (v1, h1) =>
|
||||
match eval n h1 env e2 with
|
||||
| some (v2, h2) =>
|
||||
match op.apply v1 v2 with
|
||||
| some v => some (v, h2)
|
||||
| none => none
|
||||
| none => none
|
||||
| none => none
|
||||
| n + 1, h, env, .refMk e =>
|
||||
match eval n h env e with
|
||||
| some (v, h1) => some (.vLoc h1.size, h1.push v)
|
||||
| none => none
|
||||
| n + 1, h, env, .deref e =>
|
||||
match eval n h env e with
|
||||
| some (.vLoc loc, h1) =>
|
||||
match h1[loc]? with
|
||||
| some v => some (v, h1)
|
||||
| none => none
|
||||
| _ => none
|
||||
| n + 1, h, env, .assign e1 e2 =>
|
||||
match eval n h env e1 with
|
||||
| some (.vLoc loc, h1) =>
|
||||
match eval n h1 env e2 with
|
||||
| some (v2, h2) =>
|
||||
if loc < h2.size then some (.vUnit, h2.set! loc v2) else none
|
||||
| none => none
|
||||
| _ => none
|
||||
| n + 1, h, env, .seq e1 e2 =>
|
||||
match eval n h env e1 with
|
||||
| some (_, h1) => eval n h1 env e2
|
||||
| none => none
|
||||
|
||||
theorem eval_sound :
|
||||
∀ (n : Nat) (h : Heap) (env : Env) (e : Term) (v : Value) (h' : Heap),
|
||||
eval n h env e = some (v, h') → BigStep h env e v h' := by
|
||||
intro n
|
||||
induction n with
|
||||
| zero =>
|
||||
intro h env e v h' heq
|
||||
simp [eval] at heq
|
||||
| succ n ih =>
|
||||
intro h env e v h' heq
|
||||
cases e with
|
||||
| unitT =>
|
||||
simp [eval] at heq
|
||||
obtain ⟨rfl, rfl⟩ := heq
|
||||
exact .unitR
|
||||
| intLit k =>
|
||||
simp [eval] at heq
|
||||
obtain ⟨rfl, rfl⟩ := heq
|
||||
exact .intLitR k
|
||||
| boolLit b =>
|
||||
simp [eval] at heq
|
||||
obtain ⟨rfl, rfl⟩ := heq
|
||||
exact .boolLitR b
|
||||
| var x =>
|
||||
simp only [eval] at heq
|
||||
split at heq
|
||||
next vv hL =>
|
||||
simp at heq
|
||||
obtain ⟨rfl, rfl⟩ := heq
|
||||
exact .varR hL
|
||||
next => simp at heq
|
||||
| lam x body =>
|
||||
simp [eval] at heq
|
||||
obtain ⟨rfl, rfl⟩ := heq
|
||||
exact .lamR x body
|
||||
| app e1 e2 =>
|
||||
simp only [eval] at heq
|
||||
split at heq
|
||||
next x body env' h1 heq1 =>
|
||||
split at heq
|
||||
next v2 h2 heq2 =>
|
||||
exact .appR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq2) (ih _ _ _ _ _ heq)
|
||||
next => simp at heq
|
||||
all_goals simp at heq
|
||||
| letIn x e1 e2 =>
|
||||
simp only [eval] at heq
|
||||
split at heq
|
||||
next v1 h1 heq1 =>
|
||||
exact .letInR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq)
|
||||
next => simp at heq
|
||||
| ifte ec e1 e2 =>
|
||||
simp only [eval] at heq
|
||||
split at heq
|
||||
next h1 heq1 =>
|
||||
exact .ifTR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq)
|
||||
next h1 heq1 =>
|
||||
exact .ifFR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq)
|
||||
all_goals simp at heq
|
||||
| binop op e1 e2 =>
|
||||
simp only [eval] at heq
|
||||
split at heq
|
||||
next v1 h1 heq1 =>
|
||||
split at heq
|
||||
next v2 h2 heq2 =>
|
||||
split at heq
|
||||
next vv heqop =>
|
||||
simp at heq
|
||||
obtain ⟨rfl, rfl⟩ := heq
|
||||
exact .binopR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq2) heqop
|
||||
next => simp at heq
|
||||
next => simp at heq
|
||||
next => simp at heq
|
||||
| refMk e =>
|
||||
simp only [eval] at heq
|
||||
split at heq
|
||||
next vv h1 heq1 =>
|
||||
simp at heq
|
||||
obtain ⟨rfl, rfl⟩ := heq
|
||||
exact .refMkR (ih _ _ _ _ _ heq1)
|
||||
next => simp at heq
|
||||
| deref e =>
|
||||
simp only [eval] at heq
|
||||
split at heq
|
||||
next loc h1 heq1 =>
|
||||
split at heq
|
||||
next vv hget =>
|
||||
simp at heq
|
||||
obtain ⟨rfl, rfl⟩ := heq
|
||||
exact .derefR (ih _ _ _ _ _ heq1) hget
|
||||
next => simp at heq
|
||||
all_goals simp at heq
|
||||
| assign e1 e2 =>
|
||||
simp only [eval] at heq
|
||||
split at heq
|
||||
next loc h1 heq1 =>
|
||||
split at heq
|
||||
next v2 h2 heq2 =>
|
||||
split at heq
|
||||
next hb =>
|
||||
simp at heq
|
||||
obtain ⟨rfl, rfl⟩ := heq
|
||||
exact .assignR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq2) hb
|
||||
next => simp at heq
|
||||
next => simp at heq
|
||||
all_goals simp at heq
|
||||
| seq e1 e2 =>
|
||||
simp only [eval] at heq
|
||||
split at heq
|
||||
next _ h1 heq1 =>
|
||||
exact .seqR (ih _ _ _ _ _ heq1) (ih _ _ _ _ _ heq)
|
||||
next => simp at heq
|
||||
|
||||
end GolangLean.Core
|
||||
101
GolangLean/Core/TypeSoundness.lean
Normal file
101
GolangLean/Core/TypeSoundness.lean
Normal file
|
|
@ -0,0 +1,101 @@
|
|||
import GolangLean.Core.Types
|
||||
import GolangLean.Core.Semantics
|
||||
|
||||
namespace GolangLean.Core
|
||||
|
||||
/-! # Type soundness for TGC.
|
||||
|
||||
Big-step preservation: if `Γ ⊢ e : T` and `BigStep h env e v h'` under
|
||||
compatible heap/env typings, then there exists an extended heap-typing
|
||||
under which `v : T` and the new heap is well-typed. There is no
|
||||
small-step "progress" analogue — big-step proves "if it terminates, the
|
||||
result has the expected type". -/
|
||||
|
||||
abbrev HeapTy := Array Ty
|
||||
|
||||
mutual
|
||||
|
||||
inductive HasTypeV : HeapTy → Value → Ty → Prop where
|
||||
| vUnit {ht} : HasTypeV ht .vUnit .unit
|
||||
| vInt {ht} (n : Int) : HasTypeV ht (.vInt n) .int
|
||||
| vBool {ht} (b : Bool) : HasTypeV ht (.vBool b) .bool
|
||||
| vLoc {ht loc T} (h : (ht[loc]? : Option Ty) = some T) :
|
||||
HasTypeV ht (.vLoc loc) (.ref T)
|
||||
| vClos {ht x body env Γ T_arg T_ret}
|
||||
(he : HasTypeEnv ht env Γ)
|
||||
(hb : HasType (Γ.extend x T_arg) body T_ret) :
|
||||
HasTypeV ht (.vClos x body env) (.arrow T_arg T_ret)
|
||||
|
||||
inductive HasTypeEnv : HeapTy → Env → TyEnv → Prop where
|
||||
| nil {ht} : HasTypeEnv ht .nil []
|
||||
| cons {ht x v T env Γ}
|
||||
(hv : HasTypeV ht v T)
|
||||
(he : HasTypeEnv ht env Γ) :
|
||||
HasTypeEnv ht (.cons x v env) ((x, T) :: Γ)
|
||||
|
||||
end
|
||||
|
||||
def HasTypeH (ht : HeapTy) (h : Heap) : Prop :=
|
||||
ht.size = h.size ∧
|
||||
∀ (i : Nat) (T : Ty), (ht[i]? : Option Ty) = some T →
|
||||
∃ v, (h[i]? : Option Value) = some v ∧ HasTypeV ht v T
|
||||
|
||||
def HeapTy.extends (ht ht' : HeapTy) : Prop :=
|
||||
ht.size ≤ ht'.size ∧
|
||||
∀ (i : Nat) (T : Ty), (ht[i]? : Option Ty) = some T → (ht'[i]? : Option Ty) = some T
|
||||
|
||||
namespace HeapTy
|
||||
|
||||
theorem extends_refl (ht : HeapTy) : ht.extends ht :=
|
||||
⟨Nat.le_refl _, fun _ _ h => h⟩
|
||||
|
||||
theorem extends_trans {ht₁ ht₂ ht₃ : HeapTy}
|
||||
(h₁ : ht₁.extends ht₂) (h₂ : ht₂.extends ht₃) : ht₁.extends ht₃ :=
|
||||
⟨Nat.le_trans h₁.1 h₂.1, fun i T h => h₂.2 i T (h₁.2 i T h)⟩
|
||||
|
||||
end HeapTy
|
||||
|
||||
/-! ## Weakening under heap-typing extension. -/
|
||||
|
||||
mutual
|
||||
|
||||
theorem HasTypeV.weaken {ht ht' v T}
|
||||
(h : HasTypeV ht v T) (ext : HeapTy.extends ht ht') :
|
||||
HasTypeV ht' v T := by
|
||||
cases h with
|
||||
| vUnit => exact .vUnit
|
||||
| vInt n => exact .vInt n
|
||||
| vBool b => exact .vBool b
|
||||
| vLoc hLoc => exact .vLoc (ext.2 _ _ hLoc)
|
||||
| vClos he hb => exact .vClos (HasTypeEnv.weaken he ext) hb
|
||||
|
||||
theorem HasTypeEnv.weaken {ht ht' env Γ}
|
||||
(h : HasTypeEnv ht env Γ) (ext : HeapTy.extends ht ht') :
|
||||
HasTypeEnv ht' env Γ := by
|
||||
cases h with
|
||||
| nil => exact .nil
|
||||
| cons hv he => exact .cons (HasTypeV.weaken hv ext) (HasTypeEnv.weaken he ext)
|
||||
|
||||
end
|
||||
|
||||
/-! ## Lookup correspondence: well-typed env produces well-typed values. -/
|
||||
|
||||
theorem HasTypeEnv.lookup_correspondence :
|
||||
∀ {ht env Γ x T},
|
||||
HasTypeEnv ht env Γ → Γ.lookup x = some T →
|
||||
∃ v, env.lookup x = some v ∧ HasTypeV ht v T
|
||||
| _, _, _, _, _, .nil, hL => by simp [TyEnv.lookup] at hL
|
||||
| _, _, _, x, _, @HasTypeEnv.cons _ x' v' T' env' Γ' hv he, hL => by
|
||||
by_cases hx : x' = x
|
||||
· subst hx
|
||||
simp only [TyEnv.lookup] at hL
|
||||
simp at hL
|
||||
cases hL
|
||||
refine ⟨v', ?_, hv⟩
|
||||
simp [EnvList.lookup]
|
||||
· simp only [TyEnv.lookup, if_neg hx] at hL
|
||||
have ⟨v, hLv, hTv⟩ := lookup_correspondence he hL
|
||||
refine ⟨v, ?_, hTv⟩
|
||||
simp [EnvList.lookup, hx, hLv]
|
||||
|
||||
end GolangLean.Core
|
||||
90
GolangLean/Core/Types.lean
Normal file
90
GolangLean/Core/Types.lean
Normal file
|
|
@ -0,0 +1,90 @@
|
|||
import GolangLean.Core.Syntax
|
||||
|
||||
namespace GolangLean.Core
|
||||
|
||||
/-! # Static type system for TGC.
|
||||
|
||||
Five base types: `unit`, `int`, `bool`, `arrow τ₁ τ₂`, `ref τ`. Typing
|
||||
context `TyEnv` is a list of (name, type) bindings — innermost-first to
|
||||
match `Env`.
|
||||
|
||||
Typing rules `HasType : TyEnv → Term → Ty → Prop` follow the standard
|
||||
simply-typed lambda calculus + ML-style references discipline. -/
|
||||
|
||||
inductive Ty where
|
||||
| unit : Ty
|
||||
| int : Ty
|
||||
| bool : Ty
|
||||
| arrow : Ty → Ty → Ty
|
||||
| ref : Ty → Ty
|
||||
deriving Repr, BEq, DecidableEq, Inhabited
|
||||
|
||||
abbrev TyEnv := List (String × Ty)
|
||||
|
||||
namespace TyEnv
|
||||
|
||||
def lookup : TyEnv → String → Option Ty
|
||||
| [], _ => none
|
||||
| (k, T) :: rs, x => if k = x then some T else lookup rs x
|
||||
|
||||
def extend (Γ : TyEnv) (x : String) (T : Ty) : TyEnv :=
|
||||
(x, T) :: Γ
|
||||
|
||||
end TyEnv
|
||||
|
||||
namespace BinOp
|
||||
|
||||
def typeOf : BinOp → Ty → Ty → Option Ty
|
||||
| .add, .int, .int => some .int
|
||||
| .sub, .int, .int => some .int
|
||||
| .mul, .int, .int => some .int
|
||||
| .eq, .int, .int => some .bool
|
||||
| .eq, .bool, .bool => some .bool
|
||||
| .lt, .int, .int => some .bool
|
||||
| _, _, _ => none
|
||||
|
||||
end BinOp
|
||||
|
||||
inductive HasType : TyEnv → Term → Ty → Prop where
|
||||
| unitT {Γ} : HasType Γ .unitT .unit
|
||||
| intLit {Γ} (n : Int) : HasType Γ (.intLit n) .int
|
||||
| boolLit {Γ} (b : Bool) : HasType Γ (.boolLit b) .bool
|
||||
| var {Γ x T} (h : Γ.lookup x = some T) :
|
||||
HasType Γ (.var x) T
|
||||
| lam {Γ x body T_arg T_ret}
|
||||
(h : HasType (Γ.extend x T_arg) body T_ret) :
|
||||
HasType Γ (.lam x body) (.arrow T_arg T_ret)
|
||||
| app {Γ e1 e2 T_arg T_ret}
|
||||
(h1 : HasType Γ e1 (.arrow T_arg T_ret))
|
||||
(h2 : HasType Γ e2 T_arg) :
|
||||
HasType Γ (.app e1 e2) T_ret
|
||||
| letIn {Γ x e1 e2 T1 T2}
|
||||
(h1 : HasType Γ e1 T1)
|
||||
(h2 : HasType (Γ.extend x T1) e2 T2) :
|
||||
HasType Γ (.letIn x e1 e2) T2
|
||||
| ifte {Γ ec e1 e2 T}
|
||||
(hc : HasType Γ ec .bool)
|
||||
(h1 : HasType Γ e1 T)
|
||||
(h2 : HasType Γ e2 T) :
|
||||
HasType Γ (.ifte ec e1 e2) T
|
||||
| binop {Γ op e1 e2 T1 T2 T}
|
||||
(h1 : HasType Γ e1 T1)
|
||||
(h2 : HasType Γ e2 T2)
|
||||
(hOp : op.typeOf T1 T2 = some T) :
|
||||
HasType Γ (.binop op e1 e2) T
|
||||
| refMk {Γ e T}
|
||||
(h : HasType Γ e T) :
|
||||
HasType Γ (.refMk e) (.ref T)
|
||||
| deref {Γ e T}
|
||||
(h : HasType Γ e (.ref T)) :
|
||||
HasType Γ (.deref e) T
|
||||
| assign {Γ e1 e2 T}
|
||||
(h1 : HasType Γ e1 (.ref T))
|
||||
(h2 : HasType Γ e2 T) :
|
||||
HasType Γ (.assign e1 e2) .unit
|
||||
| seq {Γ e1 e2 T1 T2}
|
||||
(h1 : HasType Γ e1 T1)
|
||||
(h2 : HasType Γ e2 T2) :
|
||||
HasType Γ (.seq e1 e2) T2
|
||||
|
||||
end GolangLean.Core
|
||||
Loading…
Add table
Reference in a new issue