max/crosslang
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add Tiny Octave Core (TOC) parallel to golang-lean's TGC.

Browse source 
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).
This commit is contained in:
Maximus Gorog 2026-05-10 04:26:12 -06:00
parent 23162fb93a
commit 567d3d1902
7 changed files with 600 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
OctiveLean.lean
View file

@ -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

105
OctiveLean/Core/Determinism.lean Normal file
View file

@ -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

166
OctiveLean/Core/Eval.lean Normal file
View file

@ -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

106
OctiveLean/Core/Semantics.lean Normal file
View file

@ -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

33
OctiveLean/Core/Syntax.lean Normal file
View file

@ -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

95
OctiveLean/Core/TypeSoundness.lean Normal file
View file

@ -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

89
OctiveLean/Core/Types.lean Normal file
View file

@ -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