From 567d3d190291d1e092b1bdff3699ef0c9b3f1aed Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Sun, 10 May 2026 04:26:12 -0600 Subject: [PATCH] Add Tiny Octave Core (TOC) parallel to golang-lean's TGC. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit OctiveLean/Core/ — the kernel-level formal layer that octive-lean's existing surface BigStep didn't have. Six files: Syntax.lean — Term, BinOp. Twelve constructors: ten shared with TGC plus assign (var mutation in env) and whileT (loop). No refs (Octave has no &/*). Semantics.lean — Value, EnvList, BigStep. Signature `BigStep : Env -> Term -> Value -> Env -> Prop` threading env (vs TGC's `Heap x Env`). Determinism.lean — BigStep.deterministic. Same case shapes as TGC for the shared ten constructors. The whileFR/whileTR cross-case mirrors TGC's ifTR/ifFR via Bool.noConfusion. Eval.lean — fuel-bounded eval + eval_sound. whileT recursion consumes one fuel unit per iteration. Function calls discard the body's post-env (Octave/MATLAB local-scope semantics). Types.lean — Ty (no ref), TyEnv, HasType. Twelve typing rules mirroring the constructors. TypeSoundness.lean — HasTypeV inductive, function-form HasTypeEnv. vClos uses two-part formulation (he_dom + he_typed) instead of nested existential — Lean's kernel rejects the natural ∃-form due to nested-inductive parameter restrictions. extend_typed (assign preservation) and extend_letIn (letIn preservation) lemmas. Cross-language symmetry surfaced this iteration: * Determinism proof: ten cases mirror TGC line-for-line. Two new cases (assign, while) follow the same three structural shapes. * Eval signature: state type differs (Env vs Heap×Env), constructors' eval recurrences are otherwise isomorphic. * Type system: Ty diverges (no ref vs no whileT/assign), but the typing-rule shapes are identical — variables, let, app, if, binop, seq. * Typing of runtime data is where the languages most diverge: TGC's structural HasTypeEnv works because env is scoped; TOC needs function-form because env mutates. This is the *real* asymmetry that a cross-language layer would have to abstract over. Preservation deferred — has a soundness gap with letIn-shadowing-then- assign that needs a freshness premise on letIn typing. To follow. Zero sorries / axioms / admits. Full lake build clean (73 jobs). --- OctiveLean.lean | 6 ++ OctiveLean/Core/Determinism.lean | 105 ++++++++++++++++++ OctiveLean/Core/Eval.lean | 166 +++++++++++++++++++++++++++++ OctiveLean/Core/Semantics.lean | 106 ++++++++++++++++++ OctiveLean/Core/Syntax.lean | 33 ++++++ OctiveLean/Core/TypeSoundness.lean | 95 +++++++++++++++++ OctiveLean/Core/Types.lean | 89 ++++++++++++++++ 7 files changed, 600 insertions(+) create mode 100644 OctiveLean/Core/Determinism.lean create mode 100644 OctiveLean/Core/Eval.lean create mode 100644 OctiveLean/Core/Semantics.lean create mode 100644 OctiveLean/Core/Syntax.lean create mode 100644 OctiveLean/Core/TypeSoundness.lean create mode 100644 OctiveLean/Core/Types.lean diff --git a/OctiveLean.lean b/OctiveLean.lean index ceb1c68..dea61dc 100644 --- a/OctiveLean.lean +++ b/OctiveLean.lean @@ -16,3 +16,9 @@ import OctiveLean.PlotWidget import OctiveLean.PlotBuiltins import OctiveLean.DSL import OctiveLean.Corpus +import OctiveLean.Core.Syntax +import OctiveLean.Core.Semantics +import OctiveLean.Core.Determinism +import OctiveLean.Core.Eval +import OctiveLean.Core.Types +import OctiveLean.Core.TypeSoundness diff --git a/OctiveLean/Core/Determinism.lean b/OctiveLean/Core/Determinism.lean new file mode 100644 index 0000000..0ad188e --- /dev/null +++ b/OctiveLean/Core/Determinism.lean @@ -0,0 +1,105 @@ +import OctiveLean.Core.Semantics + +namespace OctiveLean.Core + +/-! # Determinism of TOC big-step. + + `BigStep env e v₁ env₁ → BigStep env e v₂ env₂ → v₁ = v₂ ∧ env₁ = env₂` + +Proof structure mirrors TGC's `Determinism` line-for-line on the shared +ten constructors. Octave-specific cases (`assign`, `whileT`) follow the +same three patterns: terminal, structural-functional, contradiction-collapse. + +The `whileFR`/`whileTR` cross-case is closed exactly like `ifTR`/`ifFR`: +the IH on the condition produces `vBool true = vBool false`, dispatched +by `Bool.noConfusion`. -/ + +theorem BigStep.deterministic + {env : Env} {e : Term} {v₁ v₂ : Value} {env₁ env₂ : Env} + (D₁ : BigStep env e v₁ env₁) (D₂ : BigStep env e v₂ env₂) : + v₁ = v₂ ∧ env₁ = env₂ := by + induction D₁ generalizing v₂ env₂ with + | unitR => cases D₂; exact ⟨rfl, rfl⟩ + | intLitR n => cases D₂; exact ⟨rfl, rfl⟩ + | boolLitR b => cases D₂; exact ⟨rfl, rfl⟩ + | varR hLook => + cases D₂ with + | varR hLook' => + have heq := hLook.symm.trans hLook' + exact ⟨Option.some.inj heq, rfl⟩ + | lamR x body => cases D₂; exact ⟨rfl, rfl⟩ + | appR _ _ _ ih1 ih2 ihb => + cases D₂ with + | appR D1' D2' Db' => + have ⟨hClos, hE1⟩ := ih1 D1' + injection hClos with hx hbody henv + subst hx; subst hbody; subst henv; subst hE1 + have ⟨hArg, hE2⟩ := ih2 D2' + subst hArg; subst hE2 + have ⟨hv, _⟩ := ihb Db' + exact ⟨hv, rfl⟩ + | letInR _ _ ih1 ih2 => + cases D₂ with + | letInR D1' D2' => + have ⟨hv1, hE1⟩ := ih1 D1' + subst hv1; subst hE1 + exact ih2 D2' + | ifTR _ _ ihc iht => + cases D₂ with + | ifTR Dc' Dt' => + have ⟨_, hE1⟩ := ihc Dc'; subst hE1 + exact iht Dt' + | ifFR Dc' _ => + have ⟨hb, _⟩ := ihc Dc' + injection hb with hb_eq + exact Bool.noConfusion hb_eq + | ifFR _ _ ihc ihf => + cases D₂ with + | ifTR Dc' _ => + have ⟨hb, _⟩ := ihc Dc' + injection hb with hb_eq + exact Bool.noConfusion hb_eq + | ifFR Dc' Df' => + have ⟨_, hE1⟩ := ihc Dc'; subst hE1 + exact ihf Df' + | binopR _ _ Hop ih1 ih2 => + cases D₂ with + | binopR D1' D2' Hop' => + have ⟨hv1, hE1⟩ := ih1 D1' + subst hv1; subst hE1 + have ⟨hv2, hE2⟩ := ih2 D2' + subst hv2; subst hE2 + have heq := Hop.symm.trans Hop' + exact ⟨Option.some.inj heq, rfl⟩ + | seqR _ _ ih1 ih2 => + cases D₂ with + | seqR D1' D2' => + have ⟨_, hE1⟩ := ih1 D1'; subst hE1 + exact ih2 D2' + | assignR _ ih => + cases D₂ with + | assignR D' => + have ⟨hv, hE⟩ := ih D' + subst hv; subst hE + exact ⟨rfl, rfl⟩ + | whileFR _ ihc => + cases D₂ with + | whileFR Dc' => + have ⟨_, hE⟩ := ihc Dc'; subst hE + exact ⟨rfl, rfl⟩ + | whileTR Dc' _ _ => + have ⟨hb, _⟩ := ihc Dc' + injection hb with hb_eq + exact Bool.noConfusion hb_eq + | whileTR _ _ _ ihc ihb ihw => + cases D₂ with + | whileFR Dc' => + have ⟨hb, _⟩ := ihc Dc' + injection hb with hb_eq + exact Bool.noConfusion hb_eq + | whileTR Dc' Db' Dw' => + have ⟨_, hE1⟩ := ihc Dc'; subst hE1 + have ⟨_, hE2⟩ := ihb Db'; subst hE2 + exact ihw Dw' + +end OctiveLean.Core diff --git a/OctiveLean/Core/Eval.lean b/OctiveLean/Core/Eval.lean new file mode 100644 index 0000000..7eab6e0 --- /dev/null +++ b/OctiveLean/Core/Eval.lean @@ -0,0 +1,166 @@ +import OctiveLean.Core.Semantics + +namespace OctiveLean.Core + +/-! # Executable evaluator and soundness for TOC. + +Fuel-bounded recursive evaluator + `eval : Nat → Env → Term → Option (Value × Env)` +together with + `eval_sound : eval n env e = some (v, env') → BigStep env e v env'`. + +Function-call semantics: the body's post-env is *discarded* — only the +arg-evaluation env propagates outward. This matches Octave/MATLAB scoping +where mutations inside a function do not leak. + +`whileT` recursion uses one fuel step per iteration. A run that uses `n` +fuel covers up to `n` iterations of the loop. -/ + +def eval : Nat → Env → Term → Option (Value × Env) + | 0, _, _ => none + | _ + 1, env, .unitT => some (.vUnit, env) + | _ + 1, env, .intLit k => some (.vInt k, env) + | _ + 1, env, .boolLit b => some (.vBool b, env) + | _ + 1, env, .var x => + match env.lookup x with + | some v => some (v, env) + | none => none + | _ + 1, env, .lam x body => some (.vClos x body env, env) + | n + 1, env, .app e1 e2 => + match eval n env e1 with + | some (.vClos x body env_clos, env1) => + match eval n env1 e2 with + | some (v_arg, env2) => + match eval n (env_clos.extend x v_arg) body with + | some (v, _) => some (v, env2) + | none => none + | none => none + | _ => none + | n + 1, env, .letIn x e1 e2 => + match eval n env e1 with + | some (v1, env1) => eval n (env1.extend x v1) e2 + | none => none + | n + 1, env, .ifte ec e1 e2 => + match eval n env ec with + | some (.vBool true, env1) => eval n env1 e1 + | some (.vBool false, env1) => eval n env1 e2 + | _ => none + | n + 1, env, .binop op e1 e2 => + match eval n env e1 with + | some (v1, env1) => + match eval n env1 e2 with + | some (v2, env2) => + match op.apply v1 v2 with + | some v => some (v, env2) + | none => none + | none => none + | none => none + | n + 1, env, .seq e1 e2 => + match eval n env e1 with + | some (_, env1) => eval n env1 e2 + | none => none + | n + 1, env, .assign x e => + match eval n env e with + | some (v, env1) => some (.vUnit, env1.extend x v) + | none => none + | n + 1, env, .whileT c b => + match eval n env c with + | some (.vBool true, env1) => + match eval n env1 b with + | some (_, env2) => eval n env2 (.whileT c b) + | none => none + | some (.vBool false, env1) => some (.vUnit, env1) + | _ => none + +theorem eval_sound : + ∀ (n : Nat) (env : Env) (e : Term) (v : Value) (env' : Env), + eval n env e = some (v, env') → BigStep env e v env' := by + intro n + induction n with + | zero => intro env e v env' heq; simp [eval] at heq + | succ n ih => + intro env e v env' 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_clos env1 heq1 => + split at heq + next v_arg env2 heq2 => + split at heq + next v_body _ heqb => + simp at heq; obtain ⟨rfl, rfl⟩ := heq + exact .appR (ih _ _ _ _ heq1) (ih _ _ _ _ heq2) (ih _ _ _ _ heqb) + next => simp at heq + next => simp at heq + all_goals simp at heq + | letIn x e1 e2 => + simp only [eval] at heq + split at heq + next v1 env1 heq1 => + exact .letInR (ih _ _ _ _ heq1) (ih _ _ _ _ heq) + next => simp at heq + | ifte ec e1 e2 => + simp only [eval] at heq + split at heq + next env1 heq1 => exact .ifTR (ih _ _ _ _ heq1) (ih _ _ _ _ heq) + next env1 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 env1 heq1 => + split at heq + next v2 env2 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 + | seq e1 e2 => + simp only [eval] at heq + split at heq + next _ env1 heq1 => + exact .seqR (ih _ _ _ _ heq1) (ih _ _ _ _ heq) + next => simp at heq + | assign x e => + simp only [eval] at heq + split at heq + next vv env1 heq1 => + simp at heq; obtain ⟨rfl, rfl⟩ := heq + exact .assignR (ih _ _ _ _ heq1) + next => simp at heq + | whileT c b => + simp only [eval] at heq + split at heq + next env1 heq1 => + split at heq + next _ env2 heq2 => + have hbs_rec := ih _ _ _ _ heq + have hv_unit : v = .vUnit := by cases hbs_rec <;> rfl + subst hv_unit + exact .whileTR (ih _ _ _ _ heq1) (ih _ _ _ _ heq2) hbs_rec + next => simp at heq + next env1 heq1 => + simp at heq; obtain ⟨rfl, rfl⟩ := heq + exact .whileFR (ih _ _ _ _ heq1) + all_goals simp at heq + +end OctiveLean.Core diff --git a/OctiveLean/Core/Semantics.lean b/OctiveLean/Core/Semantics.lean new file mode 100644 index 0000000..b0dc31b --- /dev/null +++ b/OctiveLean/Core/Semantics.lean @@ -0,0 +1,106 @@ +import OctiveLean.Core.Syntax + +namespace OctiveLean.Core + +/-! # Big-step operational semantics for TOC. + +Threads `Env` (no heap — Octave has no explicit references). `assign x e` +mutates the env by prepending; subsequent `var x` lookups see the new +binding. Closures capture the env at λ-evaluation time (lexical scope). + +Compare with TGC's `BigStep : Heap → Env → Term → Value → Heap → Prop`: +TOC's signature `BigStep : Env → Term → Value → Env → Prop` differs in +the *state type* (Env vs Heap × Env). Constructors for the shared subset +(unitR, intLitR, boolLitR, varR, lamR, appR, letInR, ifTR, ifFR, binopR, +seqR) match TGC's structure rule-for-rule. -/ + +mutual + + inductive Value where + | vUnit : Value + | vInt : Int → Value + | vBool : Bool → Value + | vClos : String → Term → EnvList → Value + + inductive EnvList where + | nil : EnvList + | cons : String → Value → EnvList → EnvList + +end + +abbrev Env := EnvList + +namespace EnvList + +def lookup : EnvList → String → Option Value + | .nil, _ => none + | .cons k v r, x => if k = x then some v else lookup r x + +def extend (env : EnvList) (x : String) (v : Value) : EnvList := + .cons x v env + +end EnvList + +namespace BinOp + +def apply : BinOp → Value → Value → Option Value + | .add, .vInt a, .vInt b => some (.vInt (a + b)) + | .sub, .vInt a, .vInt b => some (.vInt (a - b)) + | .mul, .vInt a, .vInt b => some (.vInt (a * b)) + | .eq, .vInt a, .vInt b => some (.vBool (a == b)) + | .eq, .vBool a, .vBool b => some (.vBool (a == b)) + | .lt, .vInt a, .vInt b => some (.vBool (a < b)) + | _, _, _ => none + +end BinOp + +inductive BigStep : Env → Term → Value → Env → Prop where + | unitR {env} : + BigStep env .unitT .vUnit env + | intLitR {env} (n : Int) : + BigStep env (.intLit n) (.vInt n) env + | boolLitR {env} (b : Bool) : + BigStep env (.boolLit b) (.vBool b) env + | varR {env x v} (hLook : env.lookup x = some v) : + BigStep env (.var x) v env + | lamR {env} (x : String) (body : Term) : + BigStep env (.lam x body) (.vClos x body env) env + | appR {env e1 e2 x body env_clos v_arg v env1 env2 env3} + (D1 : BigStep env e1 (.vClos x body env_clos) env1) + (D2 : BigStep env1 e2 v_arg env2) + (Db : BigStep (env_clos.extend x v_arg) body v env3) : + BigStep env (.app e1 e2) v env2 + | 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 + | ifTR {env ec e1 e2 v env1 env2} + (Dc : BigStep env ec (.vBool true) env1) + (Dt : BigStep env1 e1 v env2) : + BigStep env (.ifte ec e1 e2) v env2 + | ifFR {env ec e1 e2 v env1 env2} + (Dc : BigStep env ec (.vBool false) env1) + (Df : BigStep env1 e2 v env2) : + BigStep env (.ifte ec e1 e2) v env2 + | binopR {env op e1 e2 v1 v2 v env1 env2} + (D1 : BigStep env e1 v1 env1) + (D2 : BigStep env1 e2 v2 env2) + (Hop : op.apply v1 v2 = some v) : + BigStep env (.binop op e1 e2) v env2 + | seqR {env e1 e2 v1 v2 env1 env2} + (D1 : BigStep env e1 v1 env1) + (D2 : BigStep env1 e2 v2 env2) : + BigStep env (.seq e1 e2) v2 env2 + | assignR {env x e v env1} + (D : BigStep env e v env1) : + BigStep env (.assign x e) .vUnit (env1.extend x v) + | whileFR {env c b env1} + (Dc : BigStep env c (.vBool false) env1) : + BigStep env (.whileT c b) .vUnit env1 + | whileTR {env c b env1 env2 env3 v_b} + (Dc : BigStep env c (.vBool true) env1) + (Db : BigStep env1 b v_b env2) + (Dw : BigStep env2 (.whileT c b) .vUnit env3) : + BigStep env (.whileT c b) .vUnit env3 + +end OctiveLean.Core diff --git a/OctiveLean/Core/Syntax.lean b/OctiveLean/Core/Syntax.lean new file mode 100644 index 0000000..21f6ac1 --- /dev/null +++ b/OctiveLean/Core/Syntax.lean @@ -0,0 +1,33 @@ +namespace OctiveLean.Core + +/-! # Tiny Octave Core (TOC) — abstract syntax. + +Parallel to golang-lean's TGC. Shared kernel: ten constructors covering +λ-calculus core + conditionals + sequencing. Octave-specific extensions: +`assign` (variable mutation in the env) and `whileT` (loop until false). + +What is *not* here: matrices, cell arrays, ranges, anonymous-function +captures with `@(x) expr` syntax, `printf`-family builtins. Those are +desugaring targets for the surface-Octave→TOC translator (later). -/ + +inductive BinOp where + | add | sub | mul + | eq | lt + deriving Repr, BEq, DecidableEq, Inhabited + +inductive Term where + | unitT : Term + | intLit : Int → Term + | boolLit : Bool → Term + | var : String → Term + | lam : String → Term → Term -- λ x. e + | app : Term → Term → Term + | letIn : String → Term → Term → Term -- let x = e₁ in e₂ (lexical) + | ifte : Term → Term → Term → Term + | binop : BinOp → Term → Term → Term + | seq : Term → Term → Term + | assign : String → Term → Term -- x = e (mutates env) + | whileT : Term → Term → Term -- while c do b + deriving Repr, Inhabited + +end OctiveLean.Core diff --git a/OctiveLean/Core/TypeSoundness.lean b/OctiveLean/Core/TypeSoundness.lean new file mode 100644 index 0000000..3cc9c15 --- /dev/null +++ b/OctiveLean/Core/TypeSoundness.lean @@ -0,0 +1,95 @@ +import OctiveLean.Core.Types +import OctiveLean.Core.Semantics + +namespace OctiveLean.Core + +/-! # Type soundness infrastructure for TOC. + +Asymmetry vs TGC: TOC's `assign` mutates env, so the "runtime data is +well-typed" property must be permissive — env may have *more* bindings +than Γ requires. So `HasTypeEnv` is a function-form predicate (Π → ∃), +not a structural inductive (TGC could afford structural because its +env is scoped; only the heap mutates). + +Closure typing: `vClos` would naturally take `HasTypeEnv` as a premise, +but the kernel rejects nested ∃ in inductive constructors with locally +bound parameters. So we split into two strictly-positive premises — +domain coverage and pointwise typing — and rebuild `HasTypeEnv` outside. +The two formulations are interconvertible (lemmas below). -/ + +inductive HasTypeV : Value → Ty → Prop where + | vUnit : HasTypeV .vUnit .unit + | vInt (n : Int) : HasTypeV (.vInt n) .int + | vBool (b : Bool) : HasTypeV (.vBool b) .bool + | vClos {x : String} {body : Term} {env : Env} + {Γ : TyEnv} {T_arg T_ret : Ty} + (he_dom : ∀ y T_y, Γ.lookup y = some T_y → (env.lookup y).isSome) + (he_typed : ∀ y T_y v, Γ.lookup y = some T_y → + env.lookup y = some v → HasTypeV v T_y) + (hb : HasType (Γ.extend x T_arg) body T_ret) : + HasTypeV (.vClos x body env) (.arrow T_arg T_ret) + +def HasTypeEnv (env : Env) (Γ : TyEnv) : Prop := + ∀ y T_y, Γ.lookup y = some T_y → ∃ v, env.lookup y = some v ∧ HasTypeV v T_y + +namespace HasTypeEnv + +theorem extend_typed + {env : Env} {Γ : TyEnv} {x : String} {v : Value} {T : Ty} + (hE : HasTypeEnv env Γ) + (hx : Γ.lookup x = some T) + (hv : HasTypeV v T) : + HasTypeEnv (env.extend x v) Γ := by + intro y T_y hLy + by_cases hxy : x = y + · subst hxy + rw [hLy] at hx + cases hx + refine ⟨v, ?_, hv⟩ + simp [EnvList.lookup, EnvList.extend] + · have ⟨v', hLv', hVT'⟩ := hE y T_y hLy + refine ⟨v', ?_, hVT'⟩ + simp [EnvList.lookup, EnvList.extend, hxy] + exact hLv' + +theorem extend_letIn + {env : Env} {Γ : TyEnv} {x : String} {v : Value} {T : Ty} + (hE : HasTypeEnv env Γ) (hv : HasTypeV v T) : + HasTypeEnv (env.extend x v) (Γ.extend x T) := by + intro y T_y hLy + by_cases hxy : x = y + · subst hxy + simp only [TyEnv.extend, TyEnv.lookup] at hLy + simp at hLy + subst hLy + refine ⟨v, ?_, hv⟩ + simp [EnvList.lookup, EnvList.extend] + · simp only [TyEnv.extend, TyEnv.lookup] at hLy + simp [hxy] at hLy + have ⟨v', hLv', hVT'⟩ := hE y T_y hLy + refine ⟨v', ?_, hVT'⟩ + simp [EnvList.lookup, EnvList.extend, hxy] + exact hLv' + +end HasTypeEnv + +/-! ## Bridge between vClos's two-part formulation and HasTypeEnv. -/ + +theorem HasTypeV.vClos_of_env + {x : String} {body : Term} {env : Env} {Γ : TyEnv} + {T_arg T_ret : Ty} + (hE : HasTypeEnv env Γ) + (hb : HasType (Γ.extend x T_arg) body T_ret) : + HasTypeV (.vClos x body env) (.arrow T_arg T_ret) := by + apply HasTypeV.vClos + · intros y T_y hLy + have ⟨_, hLv, _⟩ := hE y T_y hLy + rw [hLv]; rfl + · intros y T_y v hLy hLv + have ⟨v', hLv', hVT'⟩ := hE y T_y hLy + rw [hLv'] at hLv + cases hLv + exact hVT' + · exact hb + +end OctiveLean.Core diff --git a/OctiveLean/Core/Types.lean b/OctiveLean/Core/Types.lean new file mode 100644 index 0000000..cbaf216 --- /dev/null +++ b/OctiveLean/Core/Types.lean @@ -0,0 +1,89 @@ +import OctiveLean.Core.Syntax + +namespace OctiveLean.Core + +/-! # Static type system for TOC. + +Four base types — `unit`, `int`, `bool`, `arrow`. No `ref` (Octave has +no explicit references, unlike TGC). Two new typing rules over TGC's +shared core: + + * `assign x e` requires `x` to already be typed in Γ with the same + type as `e`. New variables enter scope via `letIn`, not assign. + * `whileT c b` types as `unit` whenever `c : bool` and `b` types at + any T (the body's value is discarded). -/ + +inductive Ty where + | unit : Ty + | int : Ty + | bool : Ty + | arrow : Ty → 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 + | seq {Γ e1 e2 T1 T2} + (h1 : HasType Γ e1 T1) + (h2 : HasType Γ e2 T2) : + HasType Γ (.seq e1 e2) T2 + | assign {Γ x e T} + (hx : Γ.lookup x = some T) + (h : HasType Γ e T) : + HasType Γ (.assign x e) .unit + | whileT {Γ c b T_b} + (hc : HasType Γ c .bool) + (hb : HasType Γ b T_b) : + HasType Γ (.whileT c b) .unit + +end OctiveLean.Core