def Esolangs.Cornucopia.mainName : String

Equations

• Esolangs.Cornucopia.mainName = "main"

def Esolangs.Cornucopia.succName : String

Equations

• Esolangs.Cornucopia.succName = "succ"

def Esolangs.Cornucopia.subName : String

Equations

• Esolangs.Cornucopia.subName = "sub"

inductive Esolangs.Cornucopia.Builtin : Type

• succ : Builtin
• sub : Builtin

@[instance_reducible]

instance Esolangs.Cornucopia.instInhabitedBuiltin : Inhabited Builtin

Equations

• Esolangs.Cornucopia.instInhabitedBuiltin = { default := Esolangs.Cornucopia.instInhabitedBuiltin.default }

@[instance_reducible]

instance Esolangs.Cornucopia.instFintypeBuiltin : Fintype Builtin

Equations

• Esolangs.Cornucopia.instFintypeBuiltin = { elems := { val := ↑Esolangs.Cornucopia.Builtin.enumList, nodup := Esolangs.Cornucopia.Builtin.enumList_nodup }, complete := Esolangs.Cornucopia.instFintypeBuiltin._proof_1 }

@[instance_reducible]

instance Esolangs.Cornucopia.instDecidableEqBuiltin : DecidableEq Builtin

Equations

• Esolangs.Cornucopia.instDecidableEqBuiltin x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Esolangs.Cornucopia.BuiltinInfo : Type

• name : String
• arity : ℕ
• eval : List ℕ → ℕ

theorem Esolangs.Cornucopia.BuiltinInfo.ext_iff {x y : BuiltinInfo} : x = y ↔ x.name = y.name ∧ x.arity = y.arity ∧ x.eval = y.eval

theorem Esolangs.Cornucopia.BuiltinInfo.ext {x y : BuiltinInfo} (name : x.name = y.name) (arity : x.arity = y.arity) (eval : x.eval = y.eval) : x = y

@[instance_reducible]

instance Esolangs.Cornucopia.instInhabitedBuiltinInfo : Inhabited BuiltinInfo

Equations

• Esolangs.Cornucopia.instInhabitedBuiltinInfo = { default := Esolangs.Cornucopia.instInhabitedBuiltinInfo.default }

inductive Esolangs.Cornucopia.Expr : Type

• arg : ℕ → Expr
• call : String → List Expr → Expr

@[instance_reducible]

instance Esolangs.Cornucopia.instInhabitedExpr : Inhabited Expr

Equations

• Esolangs.Cornucopia.instInhabitedExpr = { default := Esolangs.Cornucopia.instInhabitedExpr.default }

structure Esolangs.Cornucopia.Def : Type

• arity : ℕ
• expr : Expr

theorem Esolangs.Cornucopia.Def.ext_iff {x y : Def} : x = y ↔ x.arity = y.arity ∧ x.expr = y.expr

theorem Esolangs.Cornucopia.Def.ext {x y : Def} (arity : x.arity = y.arity) (expr : x.expr = y.expr) : x = y

@[instance_reducible]

instance Esolangs.Cornucopia.instInhabitedDef : Inhabited Def

Equations

• Esolangs.Cornucopia.instInhabitedDef = { default := Esolangs.Cornucopia.instInhabitedDef.default }

structure Esolangs.Cornucopia.Prog : Type

• defs : Map String Def

theorem Esolangs.Cornucopia.Prog.ext {x y : Prog} (defs : x.defs = y.defs) : x = y

theorem Esolangs.Cornucopia.Prog.ext_iff {x y : Prog} : x = y ↔ x.defs = y.defs

@[instance_reducible]

instance Esolangs.Cornucopia.instInhabitedProg : Inhabited Prog

Equations

• Esolangs.Cornucopia.instInhabitedProg = { default := Esolangs.Cornucopia.instInhabitedProg.default }

def Esolangs.Cornucopia.fn (arity : ℕ) (f : List ℕ → ℕ) (xs : List ℕ) : ℕ

Equations

• Esolangs.Cornucopia.fn arity f xs = if xs.length ≠ arity then 0 else f xs

def Esolangs.Cornucopia.builtins : List Builtin

Equations

• Esolangs.Cornucopia.builtins = [Esolangs.Cornucopia.Builtin.succ, Esolangs.Cornucopia.Builtin.sub]

def Esolangs.Cornucopia.Builtin.info (b : Builtin) : BuiltinInfo

Equations

• Esolangs.Cornucopia.Builtin.succ.info = { name := Esolangs.Cornucopia.succName, arity := 1, eval := fun (xs : List ℕ) => xs[0]! + 1 }
• Esolangs.Cornucopia.Builtin.sub.info = { name := Esolangs.Cornucopia.subName, arity := 2, eval := fun (xs : List ℕ) => xs[0]! - xs[1]! }

def Esolangs.Cornucopia.Builtin.name (b : Builtin) : String

Equations

• b.name = b.info.name

def Esolangs.Cornucopia.Builtin.arity (b : Builtin) : ℕ

Equations

• b.arity = b.info.arity

def Esolangs.Cornucopia.Builtin.eval (b : Builtin) : List ℕ → ℕ

Equations

• b.eval = Esolangs.Cornucopia.fn b.arity b.info.eval

def Esolangs.Cornucopia.Builtin.expr (b : Builtin) : Expr

Equations

• b.expr = Esolangs.Cornucopia.Expr.call b.name (mkList b.arity Esolangs.Cornucopia.Expr.arg)

def Esolangs.Cornucopia.Builtin.def (b : Builtin) : Def

Equations

• b.def = { arity := b.arity, expr := b.expr }

def Esolangs.Cornucopia.Builtin.namesMap : Map String Builtin

Equations

• Esolangs.Cornucopia.Builtin.namesMap = Map.ofList (List.map (fun (b : Esolangs.Cornucopia.Builtin) => (b.name, b)) Esolangs.Cornucopia.builtins)

class Esolangs.Cornucopia.IsBuiltin (name : String) : Prop

• h : ∃ (b : Builtin), b.name = name

class Esolangs.Cornucopia.BuiltinC (name : String) : Type

• b : Builtin
• name_eq : (b name).name = name

def Esolangs.Cornucopia.Prog.def? (prog : Prog) (name : String) : Option Def

Equations

• prog.def? name = Map.get? name prog.defs

def Esolangs.Cornucopia.Prog.def (prog : Prog) (name : String) : Def

Equations

• prog.def name = Map.get! name prog.defs

def Esolangs.Cornucopia.builtinDefs : Map String Def

Equations

• Esolangs.Cornucopia.builtinDefs = Map.ofList (List.map (fun (b : Esolangs.Cornucopia.Builtin) => (b.name, b.def)) Esolangs.Cornucopia.builtins)

def Esolangs.Cornucopia.builtinFs : Map String (List ℕ → ℕ)

Equations

• Esolangs.Cornucopia.builtinFs = Map.ofList (List.map (fun (b : Esolangs.Cornucopia.Builtin) => (b.name, b.eval)) Esolangs.Cornucopia.builtins)

def Esolangs.Cornucopia.Prog.ofDefs (defs : List (String × Def)) : Prog

Equations

• Esolangs.Cornucopia.Prog.ofDefs defs = { defs := Esolangs.Cornucopia.builtinDefs ∪ Map.ofList defs }

def Esolangs.Cornucopia.Prog.main (prog : Prog) : Def

Equations

• prog.main = prog.def Esolangs.Cornucopia.mainName

def Esolangs.Cornucopia.Prog.HasDef (prog : Prog) (name : String) : Prop

Equations

• prog.HasDef name = (name ∈ prog.defs)

def Esolangs.Cornucopia.Prog.arity (prog : Prog) (name : String) : ℕ

Equations

• prog.arity name = (prog.def name).arity

def Esolangs.Cornucopia.Prog.expr (prog : Prog) (name : String) : Expr

Equations

• prog.expr name = (prog.def name).expr

@[irreducible]

def Esolangs.Cornucopia.Expr.WF (prog : Prog) (arity : ℕ) (e : Expr) : Prop

Equations

• Esolangs.Cornucopia.Expr.WF prog arity (Esolangs.Cornucopia.Expr.arg i) = (i < arity)
• Esolangs.Cornucopia.Expr.WF prog arity (Esolangs.Cornucopia.Expr.call t args) = (prog.HasDef t ∧ args.length = prog.arity t ∧ ∀ e ∈ args, Esolangs.Cornucopia.Expr.WF prog arity e)

def Esolangs.Cornucopia.Def.WF (prog : Prog) (d : Def) : Prop

Equations

• Esolangs.Cornucopia.Def.WF prog d = Esolangs.Cornucopia.Expr.WF prog d.arity d.expr

@[irreducible]

def Esolangs.Cornucopia.Expr.eval (e : Expr) (prog : Prog) (fs : Map String (List ℕ → ℕ)) (args : List ℕ) : ℕ

Equations

• (Esolangs.Cornucopia.Expr.arg i).eval prog fs args = args[i]!
• (Esolangs.Cornucopia.Expr.call t args_1).eval prog fs args = Map.get! t fs (List.map (fun (x : Esolangs.Cornucopia.Expr) => x.eval prog fs args) args_1)

structure Esolangs.Cornucopia.Prog.Compatible (prog : Prog) (fs : Map String (List ℕ → ℕ)) : Prop

• keys_fs : fs.keys = prog.defs.keys
• get?_builtin' ⦃b : Builtin⦄ : Map.get? b.name fs = some b.eval
• eval_of_ne_arity ⦃name : String⦄ : prog.HasDef name → ∀ ⦃xs : List ℕ⦄, xs.length ≠ prog.arity name → Map.get! name fs xs = 0
• eval_eq ⦃name : String⦄ : prog.HasDef name → ∀ ⦃xs : List ℕ⦄, xs.length = prog.arity name → Map.get! name fs xs = (prog.expr name).eval prog fs xs

class Esolangs.Cornucopia.Prog.WFBuiltins (prog : Prog) : Prop

• def?_builtin ⦃b : Builtin⦄ : prog.def? b.name = some b.def

class Esolangs.Cornucopia.Prog.WF' (prog : Prog) extends prog.WFBuiltins : Prop

• def?_builtin ⦃b : Builtin⦄ : prog.def? b.name = some b.def
• has_main : prog.HasDef mainName
• arity_main : prog.main.arity = 1
• wf_def ⦃name : String⦄ ⦃d : Def⦄ : prog.def? name = some d → Def.WF prog d

class Esolangs.Cornucopia.Prog.WF (prog : Prog) extends prog.WF' : Prop

• def?_builtin ⦃b : Builtin⦄ : prog.def? b.name = some b.def
• has_main : prog.HasDef mainName
• arity_main : prog.main.arity = 1
• wf_def ⦃name : String⦄ ⦃d : Def⦄ : prog.def? name = some d → Def.WF prog d
• exiu_compatible : ∃! fs : Map String (List ℕ → ℕ), prog.Compatible fs

class Esolangs.Cornucopia.Prog.WFWoutModel (prog : Prog) extends prog.WF' : Prop

• def?_builtin ⦃b : Builtin⦄ : prog.def? b.name = some b.def
• has_main : prog.HasDef mainName
• arity_main : prog.main.arity = 1
• wf_def ⦃name : String⦄ ⦃d : Def⦄ : prog.def? name = some d → Def.WF prog d
• not_compatible ⦃fs : Map String (List ℕ → ℕ)⦄ : ¬prog.Compatible fs

class Esolangs.Cornucopia.Prog.WFWoutUnique (prog : Prog) extends prog.WF' : Prop

• def?_builtin ⦃b : Builtin⦄ : prog.def? b.name = some b.def
• has_main : prog.HasDef mainName
• arity_main : prog.main.arity = 1
• wf_def ⦃name : String⦄ ⦃d : Def⦄ : prog.def? name = some d → Def.WF prog d
• exi_two : ∃ (fs₁ : Map String (List ℕ → ℕ)) (fs₂ : Map String (List ℕ → ℕ)), fs₁ ≠ fs₂ ∧ prog.Compatible fs₁ ∧ prog.Compatible fs₂

noncomputable def Esolangs.Cornucopia.Prog.fs (prog : Prog) : Map String (List ℕ → ℕ)

Equations

• prog.fs = Classical.epsilon fun (fs : Map String (List ℕ → ℕ)) => prog.Compatible fs

noncomputable def Esolangs.Cornucopia.Prog.eval (prog : Prog) (name : String) (xs : List ℕ) : ℕ

Equations

• prog.eval name xs = Map.get! name prog.fs xs

noncomputable def Esolangs.Cornucopia.Prog.run (prog : Prog) (n : ℕ) : ℕ

Equations

• prog.run n = prog.eval Esolangs.Cornucopia.mainName [n]