structure Esolangs.Cornucopia.CompatibleDefs (defs : Map String Def) (fs : Map String (List ℕ → ℕ)) : Prop

• keys_fs : fs.keys = defs.keys
• get?_eq' ⦃name : String⦄ ⦃d : Def⦄ : Map.get? name defs = some d → Map.get? name fs = some (fn d.arity (d.expr.eval { defs := builtinDefs ∪ Map.ofList defs.toList } (builtinFs ∪ fs)))

structure Esolangs.Cornucopia.CompatibleDefsAlt₁ (defs : Map String Def) (fs : Map String (List ℕ → ℕ)) : Prop

• keys_fs : fs.keys = defs.keys
• eval_of_ne_arity ⦃name : String⦄ ⦃d : Def⦄ : Map.get? name defs = some d → ∀ ⦃xs : List ℕ⦄, xs.length ≠ d.arity → Map.get! name fs xs = 0
• eval_eq ⦃name : String⦄ ⦃d : Def⦄ : Map.get? name defs = some d → ∀ ⦃xs : List ℕ⦄, xs.length = d.arity → Map.get! name fs xs = d.expr.eval { defs := builtinDefs ∪ Map.ofList defs.toList } (builtinFs ∪ fs) xs

structure Esolangs.Cornucopia.WFDefs' (defs : List (String × Def)) : Prop

• nodup_names : (List.map (fun (x : String × Def) => x.1) defs).Nodup
• not_isBuiltin_of_mem ⦃name : String⦄ ⦃d : Def⦄ : (name, d) ∈ defs → ¬IsBuiltin name
• wf_main : ∃ (d : Def), (mainName, d) ∈ defs ∧ d.arity = 1
• wf_def ⦃name : String⦄ ⦃d : Def⦄ : (name, d) ∈ defs → Def.WF (Prog.ofDefs defs) d

def Esolangs.Cornucopia.CompatibleCnd (defs : List (String × Def)) (fs : Map String (List ℕ → ℕ)) : Prop

Equations

• Esolangs.Cornucopia.CompatibleCnd defs fs = (Esolangs.Cornucopia.CompatibleDefs (Map.ofList defs) fs ∧ ∀ (fs' : Map String (List ℕ → ℕ)), Esolangs.Cornucopia.CompatibleDefs (Map.ofList defs) fs' → ∀ (name : String) (d : Esolangs.Cornucopia.Def) (f : List ℕ → ℕ), (name, d) ∈ defs → Map.get? name fs' = some f → Map.get! name fs = f)

structure Esolangs.Cornucopia.WFDefs (defs : List (String × Def)) extends Esolangs.Cornucopia.WFDefs' defs : Prop

• nodup_names : (List.map (fun (x : String × Def) => x.1) defs).Nodup
• not_isBuiltin_of_mem ⦃name : String⦄ ⦃d : Def⦄ : (name, d) ∈ defs → ¬IsBuiltin name
• wf_main : ∃ (d : Def), (mainName, d) ∈ defs ∧ d.arity = 1
• wf_def ⦃name : String⦄ ⦃d : Def⦄ : (name, d) ∈ defs → Def.WF (Prog.ofDefs defs) d
• compatible : ∃ (fs : Map String (List ℕ → ℕ)), CompatibleCnd defs fs

def Esolangs.Cornucopia.isBuiltin (name : String) : Bool

Equations

• Esolangs.Cornucopia.isBuiltin name = Esolangs.Cornucopia.builtins.any fun (x : Esolangs.Cornucopia.Builtin) => decide (x.name = name)

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

Equations

• Esolangs.Cornucopia.findBuiltin name = (List.find? (fun (x : Esolangs.Cornucopia.Builtin) => decide (x.name = name)) Esolangs.Cornucopia.builtins).get!

@[irreducible]

def Esolangs.Cornucopia.Expr.decideEq : Expr → Expr → Bool

Equations

• (Esolangs.Cornucopia.Expr.arg i).decideEq (Esolangs.Cornucopia.Expr.arg j) = (i == j)
• (Esolangs.Cornucopia.Expr.call name₁ es₁).decideEq (Esolangs.Cornucopia.Expr.call name₂ es₂) = (name₁ == name₂ && decide (es₁.length = es₂.length) && (es₁.zip es₂).attach.all fun (x : { x : Esolangs.Cornucopia.Expr × Esolangs.Cornucopia.Expr // x ∈ es₁.zip es₂ }) => match x with | ⟨(x, y), _h⟩ => x.decideEq y)
• x✝¹.decideEq x✝ = false

theorem Esolangs.Cornucopia.isBuiltin_iff {name : String} : IsBuiltin name ↔ ∃ (b : Builtin), b.name = name

@[simp]

theorem Esolangs.Cornucopia.mem_builtins {b : Builtin} : b ∈ builtins

@[instance_reducible]

instance Esolangs.Cornucopia.instDecidableIsBuiltin {name : String} : Decidable (IsBuiltin name)

Equations

• Esolangs.Cornucopia.instDecidableIsBuiltin = decidable_of_bool (Esolangs.Cornucopia.isBuiltin name) ⋯

@[simp]

theorem Esolangs.Cornucopia.def_mk {defs : Map String Def} {name : String} : { defs := defs }.def name = Map.get! name defs

@[simp]

theorem Esolangs.Cornucopia.def?_mk {defs : Map String Def} {name : String} : { defs := defs }.def? name = Map.get? name defs

@[simp]

theorem Esolangs.Cornucopia.main_mk {defs : Map String Def} : { defs := defs }.main = Map.get! mainName defs

@[simp]

theorem Esolangs.Cornucopia.Prog.defs_mk {ds : Map String Def} : { defs := ds }.defs = ds

@[simp]

theorem Esolangs.Cornucopia.Builtin.arity_succ : succ.arity = 1

@[simp]

theorem Esolangs.Cornucopia.Builtin.arity_sub : sub.arity = 2

@[simp]

theorem Esolangs.Cornucopia.Prog.arity_mk {defs : Map String Def} {name : String} : { defs := defs }.arity name = (Map.get! name defs).arity

@[simp]

theorem Esolangs.Cornucopia.Prog.expr_mk {defs : Map String Def} {name : String} : { defs := defs }.expr name = (Map.get! name defs).expr

@[simp]

theorem Esolangs.Cornucopia.mem_builtinDefs {name : String} : name ∈ builtinDefs ↔ IsBuiltin name

@[simp]

theorem Esolangs.Cornucopia.mem_builtinFs {name : String} : name ∈ builtinFs ↔ IsBuiltin name

@[simp]

theorem Esolangs.Cornucopia.not_isBuiltin_mainName : ¬IsBuiltin mainName

theorem Esolangs.Cornucopia.Prog.def_ofDefs {xs : List (String × Def)} {name : String} (h : ¬IsBuiltin name) : (ofDefs xs).def name = Map.get! name (Map.ofList xs)

theorem Esolangs.Cornucopia.arity_ofDefs {defs : List (String × Def)} {name : String} (h : ¬IsBuiltin name) : (Prog.ofDefs defs).arity name = (Map.get! name (Map.ofList defs)).arity

@[simp]

theorem Esolangs.Cornucopia.BuiltinC.name_ne_mainName {name : String} [h : BuiltinC name] : name ≠ mainName

@[simp]

theorem Esolangs.Cornucopia.BuiltinC.mainName_ne_name {name : String} [h : BuiltinC name] : mainName ≠ name

@[instance_reducible]

instance Esolangs.Cornucopia.instBuiltinCName {b : Builtin} : BuiltinC b.name

Equations

• Esolangs.Cornucopia.instBuiltinCName = { b := b, name_eq := ⋯ }

@[simp]

theorem Esolangs.Cornucopia.Prog.main_ofDefs {xs : List (String × Def)} : (ofDefs xs).main = Map.get! mainName (Map.ofList xs)

@[simp]

theorem Esolangs.Cornucopia.Expr.run_arg {i : ℕ} {prog : Prog} {f : Map String (List ℕ → ℕ)} {args : List ℕ} : (arg i).eval prog f args = args[i]!

@[simp]

theorem Esolangs.Cornucopia.Expr.wf_arg {prog : Prog} {n i : ℕ} : WF prog n (arg i) ↔ i < n

@[simp]

theorem Esolangs.Cornucopia.nodup_builtins : builtins.Nodup

@[simp]

theorem Esolangs.Cornucopia.nodup_map_name_builtins : (List.map Builtin.name builtins).Nodup

@[simp]

theorem Esolangs.Cornucopia.IsBuiltin.get?_builtinDefs {name : String} [h : Cornucopia.BuiltinC name] : Map.get? name builtinDefs = some (BuiltinC.b name).def

@[simp]

theorem Esolangs.Cornucopia.Builtin.ext_name {b₁ b₂ : Builtin} : b₁.name = b₂.name ↔ b₁ = b₂

@[simp]

theorem Esolangs.Cornucopia.Builtin.arity_def {b : Builtin} : b.def.arity = b.arity

@[simp]

theorem Esolangs.Cornucopia.Builtin.expr_def {b : Builtin} : b.def.expr = b.expr

@[simp]

theorem Esolangs.Cornucopia.Builtin.ext_def {b₁ b₂ : Builtin} : b₁.def = b₂.def ↔ b₁ = b₂

@[simp]

theorem Esolangs.Cornucopia.BuiltinC_builtin_of_name {b : Builtin} [h : BuiltinC b.name] : BuiltinC.b b.name = b

@[simp]

theorem Esolangs.Cornucopia.Builtin.get!_builtinDefs {b : Builtin} : Map.get! b.name builtinDefs = b.def

theorem Esolangs.Cornucopia.def?_ofDefs_builtin_eq_of {defs : List (String × Def)} {b : Builtin} (h : ∀ d ∈ defs, ¬IsBuiltin d.1) : (Prog.ofDefs defs).def? b.name = some b.def

@[simp]

theorem Esolangs.Cornucopia.Prog.defs_ofDefs {defs : List (String × Def)} : (ofDefs defs).defs = builtinDefs ∪ Map.ofList defs

@[simp]

theorem Esolangs.Cornucopia.Prog.hasDef_ofDefs {defs : List (String × Def)} {name : String} : (ofDefs defs).HasDef name ↔ IsBuiltin name ∨ name ∈ Map.ofList defs

@[simp]

theorem Esolangs.Cornucopia.get?_builtinDefs_eq_some {name : String} {d : Def} : Map.get? name builtinDefs = some d ↔ ∃ (b : Builtin), b.name = name ∧ b.def = d

@[simp]

theorem Esolangs.Cornucopia.Builtin.wf_expr {prog : Prog} {b : Builtin} : Expr.WF prog b.arity b.expr ↔ ∃ (d : Def), prog.def? b.name = some d ∧ d.arity = b.arity

theorem Esolangs.Cornucopia.WFDefs'.builtin_not_mem {defs : List (String × Def)} {name : String} {d : Def} (H : WFDefs' defs) [h : BuiltinC name] : (name, d) ∉ defs

theorem Esolangs.Cornucopia.WFDefs'.get?_ofList_defs {defs : List (String × Def)} {name : String} {d : Def} (H : WFDefs' defs) : Map.get? name (Map.ofList defs) = some d ↔ (name, d) ∈ defs

@[simp]

theorem Esolangs.Cornucopia.Builtin.get?_namesMap {b : Builtin} : Map.get? b.name namesMap = some b

@[simp]

theorem Esolangs.Cornucopia.Builtin.get!_namesMap {b : Builtin} : Map.get! b.name namesMap = b

theorem Esolangs.Cornucopia.Builtin.builtin_get!_namesMap {name : String} [h : BuiltinC name] : (Map.get! name namesMap).name = name

theorem Esolangs.Cornucopia.WFDefs'.isBuiltin_or {defs : List (String × Def)} {name : String} {d : Def} (H : WFDefs' defs) (h : Map.get? name (builtinDefs ∪ Map.ofList defs) = some d) : IsBuiltin name ∨ (name, d) ∈ defs

theorem Esolangs.Cornucopia.WFDefs'.hasDef {defs : List (String × Def)} {name : String} {d : Def} (H : WFDefs' defs) (h : Map.get? name (builtinDefs ∪ Map.ofList defs) = some d) : (Prog.ofDefs defs).HasDef name

theorem Esolangs.Cornucopia.Prog.def_eq_get!_def? {prog : Prog} {name : String} : prog.def name = (prog.def? name).get!

theorem Esolangs.Cornucopia.Prog.def?_of_get? {defs : List (String × Def)} {name : String} {d : Def} (h : Map.get? name (builtinDefs ∪ Map.ofList defs) = some d) : (ofDefs defs).def? name = some d

theorem Esolangs.Cornucopia.Prog.def_of_get? {defs : List (String × Def)} {name : String} {d : Def} (h : Map.get? name (builtinDefs ∪ Map.ofList defs) = some d) : (ofDefs defs).def name = d

theorem Esolangs.Cornucopia.Prog.arity_of_get? {defs : List (String × Def)} {name : String} {d : Def} (h : Map.get? name (builtinDefs ∪ Map.ofList defs) = some d) : (ofDefs defs).arity name = d.arity

theorem Esolangs.Cornucopia.Prog.expr_of_get? {defs : List (String × Def)} {name : String} {d : Def} (h : Map.get? name (builtinDefs ∪ Map.ofList defs) = some d) : (ofDefs defs).expr name = d.expr

theorem Esolangs.Cornucopia.WFDefs'.not_mem_builtinDefs {defs : List (String × Def)} {name : String} {d : Def} (H : WFDefs' defs) (h : (name, d) ∈ defs) : name ∉ builtinDefs

theorem Esolangs.Cornucopia.WFDefs'.not_mem_builtinFs {defs : List (String × Def)} {name : String} {d : Def} (H : WFDefs' defs) (h : (name, d) ∈ defs) : name ∉ builtinFs

theorem Esolangs.Cornucopia.WFDefs'.get?_builtin {defs : List (String × Def)} {b : Builtin} (H : WFDefs' defs) : Map.get? b.name (builtinDefs ∪ Map.ofList defs) = some b.def

theorem Esolangs.Cornucopia.WFDefs'.get?_of_mem_defs {defs : List (String × Def)} (H : WFDefs' defs) {name : String} {d : Def} (h : (name, d) ∈ defs) : Map.get? name (builtinDefs ∪ Map.ofList defs) = some d

theorem Esolangs.Cornucopia.WFDefs'.def?_builtin {defs : List (String × Def)} {b : Builtin} (H : WFDefs' defs) : (Prog.ofDefs defs).def? b.name = some b.def

theorem Esolangs.Cornucopia.WFDefs'.def_builtin {defs : List (String × Def)} {b : Builtin} (H : WFDefs' defs) : (Prog.ofDefs defs).def b.name = b.def

theorem Esolangs.Cornucopia.WFDefs'.arity_builtin {defs : List (String × Def)} {b : Builtin} (H : WFDefs' defs) : (Prog.ofDefs defs).arity b.name = b.arity

theorem Esolangs.Cornucopia.WFDefs'.expr_builtin {defs : List (String × Def)} {b : Builtin} (H : WFDefs' defs) : (Prog.ofDefs defs).expr b.name = b.expr

theorem Esolangs.Cornucopia.WFDefs'.def?_of_mem_defs {defs : List (String × Def)} {name : String} {d : Def} (H : WFDefs' defs) (h : (name, d) ∈ defs) : (Prog.ofDefs defs).def? name = some d

theorem Esolangs.Cornucopia.WFDefs'.def_of_mem_defs {defs : List (String × Def)} {name : String} {d : Def} (H : WFDefs' defs) (h : (name, d) ∈ defs) : (Prog.ofDefs defs).def name = d

theorem Esolangs.Cornucopia.WFDefs'.arity_of_mem_defs {defs : List (String × Def)} {name : String} {d : Def} (H : WFDefs' defs) (h : (name, d) ∈ defs) : (Prog.ofDefs defs).arity name = d.arity

theorem Esolangs.Cornucopia.WFDefs'.expr_of_mem_defs {defs : List (String × Def)} {name : String} {d : Def} (H : WFDefs' defs) (h : (name, d) ∈ defs) : (Prog.ofDefs defs).expr name = d.expr

@[simp]

theorem Esolangs.Cornucopia.mem_builtinFS {name : String} : name ∈ builtinFs ↔ IsBuiltin name

theorem Esolangs.Cornucopia.WFDefs'.builtin_not_mem_defs {defs : List (String × Def)} {b : Builtin} {d : Def} (H : WFDefs' defs) : (b.name, d) ∉ defs

theorem Esolangs.Cornucopia.Builtin.eval_of_ne_arity {b : Builtin} {xs : List ℕ} (h : xs.length ≠ b.arity) : b.eval xs = 0

theorem Esolangs.Cornucopia.compatibleDefs_iff_alt₁ {defs : Map String Def} {fs : Map String (List ℕ → ℕ)} : CompatibleDefs defs fs ↔ CompatibleDefsAlt₁ defs fs

theorem Esolangs.Cornucopia.CompatibleDefs.alt₁ {defs : Map String Def} {fs : Map String (List ℕ → ℕ)} (h : CompatibleDefs defs fs) : CompatibleDefsAlt₁ defs fs

@[simp]

theorem Esolangs.Cornucopia.Builtin.get?_builtinFs {name : String} [h : BuiltinC name] : Map.get? name builtinFs = some (BuiltinC.b name).eval

@[simp]

theorem Esolangs.Cornucopia.Builtin.get!_builtinFs {name : String} [h : BuiltinC name] : Map.get! name builtinFs = (BuiltinC.b name).eval

theorem Esolangs.Cornucopia.CompatibleDefs.get?_builtin {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} {name : String} [H₀ : BuiltinC name] (H : WFDefs' defs) (H₁ : CompatibleDefs (Map.ofList defs) fs) : Map.get? name (builtinFs ∪ fs) = some (BuiltinC.b name).eval

theorem Esolangs.Cornucopia.CompatibleDefs.get!_builtin {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} {name : String} [H₀ : BuiltinC name] (H : WFDefs' defs) (H₁ : CompatibleDefs (Map.ofList defs) fs) : Map.get! name (builtinFs ∪ fs) = (BuiltinC.b name).eval

@[simp]

theorem Esolangs.Cornucopia.Builtin.eval_mkList {b : Builtin} {xs : List ℕ} : b.eval (mkList b.arity fun (x : ℕ) => xs[x]!) = b.info.eval xs

@[simp]

theorem Esolangs.Cornucopia.get?_builtinFs_eq_some {name : String} {f : List ℕ → ℕ} : Map.get? name builtinFs = some f ↔ ∃ (b : Builtin), b.name = name ∧ b.eval = f

theorem Esolangs.Cornucopia.Prog.WF.def_builtin {prog : Prog} {b : Builtin} [H : prog.WF] : prog.def b.name = b.def

theorem Esolangs.Cornucopia.Prog.Compatible.builtinFs_union {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} (H : (ofDefs defs).Compatible fs) : fs ∪ builtinFs = fs

theorem Esolangs.Cornucopia.WFDefs'.get?_fs_of_mem_defs {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} {name : String} {d : Def} (H : WFDefs' defs) (h : (name, d) ∈ defs) : Map.get? name (builtinFs ∪ fs) = Map.get? name fs

theorem Esolangs.Cornucopia.WFDefs'.get!_fs_of_mem_defs {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} {name : String} {d : Def} (H : WFDefs' defs) (h : (name, d) ∈ defs) : Map.get! name (builtinFs ∪ fs) = Map.get! name fs

theorem Esolangs.Cornucopia.WFDefs'.get?_of_mem_defs' {defs : List (String × Def)} (H : WFDefs' defs) {name : String} {d : Def} (h : (name, d) ∈ defs) : Map.get? name (Map.ofList defs) = some d

theorem Esolangs.Cornucopia.WFDefs'.toList_defs {defs : List (String × Def)} (H : WFDefs' defs) : (Map.ofList defs).toList = defs.mergeSort fun (x1 x2 : String × Def) => decide (x1.1 ≤ x2.1)

theorem Esolangs.Cornucopia.Prog.Compatible.union_builtinFs {prog : Prog} {fs : Map String (List ℕ → ℕ)} (H : prog.Compatible fs) : fs ∪ builtinFs = fs

theorem Esolangs.Cornucopia.Prog.Compatible.fs_eq_union {prog : Prog} {fs : Map String (List ℕ → ℕ)} (H : prog.Compatible fs) : ∃ (fs' : Map String (List ℕ → ℕ)), fs = builtinFs ∪ fs' ∧ ∀ (b : Builtin), b.name ∉ fs'

theorem Esolangs.Cornucopia.CompatibleDefs.builtin_not_mem {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} (H : WFDefs' defs) (H₁ : CompatibleDefs (Map.ofList defs) fs) (b : Builtin) : b.name ∉ fs

@[simp]

theorem Esolangs.Cornucopia.Builtin.eval_succ : succ.eval = fn 1 fun (x : List ℕ) => x[0]! + 1

@[simp]

theorem Esolangs.Cornucopia.Builtin.eval_sub : sub.eval = fn 2 fun (xs : List ℕ) => xs[0]! - xs[1]!

theorem Esolangs.Cornucopia.WFDefs'.compatible_fs_aux₁ {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} (H : WFDefs' defs) (H₁ : CompatibleDefs (Map.ofList defs) fs) : (Prog.ofDefs defs).Compatible (builtinFs ∪ fs)

theorem Esolangs.Cornucopia.WFDefs'.compatible_fs_aux₂ {defs : List (String × Def)} {fs' : Map String (List ℕ → ℕ)} (H : WFDefs' defs) (H₂ : (Prog.ofDefs defs).Compatible (builtinFs ∪ fs')) (h : ∀ (b : Builtin), b.name ∉ fs') : CompatibleDefs (Map.ofList defs) fs'

theorem Esolangs.Cornucopia.CompatibleDefs.exi_mem_defs_of_get? {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} {name : String} {f : List ℕ → ℕ} (H : CompatibleDefs (Map.ofList defs) fs) (h : Map.get? name fs = some f) : ∃ (d : Def), (name, d) ∈ defs

theorem Esolangs.Cornucopia.CompatibleDefs.exi_get?_defs_of_get? {defs : Map String Def} {fs : Map String (List ℕ → ℕ)} {name : String} {f : List ℕ → ℕ} (H : CompatibleDefs defs fs) (h : Map.get? name fs = some f) : ∃ (d : Def), Map.get? name defs = some d

theorem Esolangs.Cornucopia.WFDefs.exiu_compatible {defs : List (String × Def)} (H : WFDefs defs) : ∃! fs : Map String (List ℕ → ℕ), CompatibleDefs (Map.ofList defs) fs

theorem Esolangs.Cornucopia.WFDefs.compatible_fs {defs : List (String × Def)} (H : WFDefs defs) : ∃! fs : Map String (List ℕ → ℕ), (Prog.ofDefs defs).Compatible fs

@[simp]

theorem Esolangs.Cornucopia.IsBuiltin.name_findBuiltin {name : String} [h : IsBuiltin name] : (findBuiltin name).name = name

@[simp]

instance Esolangs.Cornucopia.BuiltinC.isBuiltin {name : String} [h : BuiltinC name] : IsBuiltin name

@[instance_reducible]

instance Esolangs.Cornucopia.IsBuiltin.BuiltinC {name : String} [h : IsBuiltin name] : Cornucopia.BuiltinC name

Equations

• Esolangs.Cornucopia.IsBuiltin.BuiltinC = { b := Esolangs.Cornucopia.findBuiltin name, name_eq := ⋯ }

theorem Esolangs.Cornucopia.WFDefs'.wf' {defs : List (String × Def)} (H : WFDefs' defs) : (Prog.ofDefs defs).WF'

theorem Esolangs.Cornucopia.WFDefs.wf {defs : List (String × Def)} (H : WFDefs defs) : (Prog.ofDefs defs).WF

@[simp]

theorem Esolangs.Cornucopia.Expr.run_call {prog : Prog} {fs : Map String (List ℕ → ℕ)} {args : List ℕ} {t : String} {xs : List Expr} : (call t xs).eval prog fs args = Map.get! t fs (List.map (fun (x : Expr) => x.eval prog fs args) xs)

@[simp]

theorem Esolangs.Cornucopia.Prog.compatible_fs {prog : Prog} [H : prog.WF] : prog.Compatible prog.fs

@[simp]

theorem Esolangs.Cornucopia.Expr.wf_call {prog : Prog} {t : String} {args : List Expr} {n : ℕ} : WF prog n (call t args) ↔ prog.HasDef t ∧ args.length = prog.arity t ∧ ∀ e ∈ args, WF prog n e

theorem Esolangs.Cornucopia.Prog.fs_eq_of_compatible {prog : Prog} {fs : Map String (List ℕ → ℕ)} [hp : prog.WF] (h : prog.Compatible fs) : prog.fs = fs

@[instance_reducible]

instance Esolangs.Cornucopia.instDecidableHasDef {prog : Prog} {i : String} : Decidable (prog.HasDef i)

Equations

• Esolangs.Cornucopia.instDecidableHasDef = id inferInstance

@[instance_reducible]

instance Esolangs.Cornucopia.instDecidableHasDef_1 {prog : Prog} {t : String} : Decidable (prog.HasDef t)

Equations

• Esolangs.Cornucopia.instDecidableHasDef_1 = id inferInstance

@[simp]

theorem Esolangs.Cornucopia.fn_eq_fn_iff {n : ℕ} {f g : List ℕ → ℕ} : fn n f = fn n g ↔ ∀ (xs : List ℕ), xs.length = n → f xs = g xs

theorem Esolangs.Cornucopia.CompatibleDefs.eval_eq {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} {name : String} {d : Def} (H : CompatibleDefs (Map.ofList defs) fs) (h : (name, d) ∈ defs) (hh : (List.map (fun (x : String × Def) => x.1) defs).Nodup := by simp) : Map.get? name fs = some (fn d.arity (d.expr.eval { defs := builtinDefs ∪ Map.ofList defs } (builtinFs ∪ fs)))

theorem Esolangs.Cornucopia.WFDefs'.compatible {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} (H : WFDefs' defs) (H₁ : CompatibleDefs (Map.ofList defs) fs) : (Prog.ofDefs defs).Compatible (builtinFs ∪ fs)

theorem Esolangs.Cornucopia.WFDefs'.wfDefs {defs : List (String × Def)} (H : WFDefs' defs) (h : ∃ (fs : Map String (List ℕ → ℕ)), CompatibleCnd defs fs) : WFDefs defs

theorem Esolangs.Cornucopia.WFDefs'.wf {defs : List (String × Def)} (H : WFDefs' defs) (h : ∃ (fs : Map String (List ℕ → ℕ)), CompatibleCnd defs fs) : (Prog.ofDefs defs).WF

@[instance_reducible]

instance Esolangs.Cornucopia.BuiltinC.succ : BuiltinC succName

Equations

• Esolangs.Cornucopia.BuiltinC.succ = { b := Esolangs.Cornucopia.Builtin.succ, name_eq := Esolangs.Cornucopia.BuiltinC.succ._proof_1 }

@[instance_reducible]

instance Esolangs.Cornucopia.BuiltinC.sub : BuiltinC subName

Equations

• Esolangs.Cornucopia.BuiltinC.sub = { b := Esolangs.Cornucopia.Builtin.sub, name_eq := Esolangs.Cornucopia.BuiltinC.sub._proof_1 }

@[instance_reducible]

instance Esolangs.Cornucopia.BuiltinC.succ_lit : BuiltinC "succ"

Equations

• Esolangs.Cornucopia.BuiltinC.succ_lit = { b := Esolangs.Cornucopia.Builtin.succ, name_eq := Esolangs.Cornucopia.BuiltinC.succ._proof_1 }

@[instance_reducible]

instance Esolangs.Cornucopia.BuiltinC.sub_lit : BuiltinC "sub"

Equations

• Esolangs.Cornucopia.BuiltinC.sub_lit = { b := Esolangs.Cornucopia.Builtin.sub, name_eq := Esolangs.Cornucopia.BuiltinC.sub._proof_1 }

@[simp]

theorem Esolangs.Cornucopia.BuiltinC.b_succ [h : BuiltinC succName] : b succName = Builtin.succ

@[simp]

theorem Esolangs.Cornucopia.BuiltinC.b_sub [h : BuiltinC subName] : b subName = Builtin.sub

@[simp]

theorem Esolangs.Cornucopia.BuiltinC.b_succ_lit [h : BuiltinC "succ"] : b "succ" = Builtin.succ

@[simp]

theorem Esolangs.Cornucopia.BuiltinC.b_sub_lit [h : BuiltinC "sub"] : b "sub" = Builtin.sub

@[simp]

theorem Esolangs.Cornucopia.BuiltinC.exi_eq_name {name : String} [h : BuiltinC name] : ∃ (b : Builtin), b.name = name

@[simp]

theorem Esolangs.Cornucopia.BuiltinC.not_forall_ne_name {name : String} [h : BuiltinC name] : ¬∀ (b : Builtin), b.name ≠ name

@[simp]

theorem Esolangs.Cornucopia.Builtin.name_succ : succ.name = succName

@[simp]

theorem Esolangs.Cornucopia.Builtin.name_sub : sub.name = subName

@[simp]

theorem Esolangs.Cornucopia.subName_ne_succName : subName ≠ succName

@[simp]

theorem Esolangs.Cornucopia.succName_ne_subName : succName ≠ subName

@[simp]

theorem Esolangs.Cornucopia.Builtin.name_eq_succName {b : Builtin} : b.name = succName ↔ b = succ

@[simp]

theorem Esolangs.Cornucopia.Builtin.name_eq_subName {b : Builtin} : b.name = subName ↔ b = sub

@[simp]

theorem Esolangs.Cornucopia.BuiltinC.builtin_succName [h : BuiltinC succName] : b succName = Builtin.succ

@[simp]

theorem Esolangs.Cornucopia.BuiltinC.builtin_subName [h : BuiltinC subName] : b subName = Builtin.sub

@[simp]

theorem Esolangs.Cornucopia.get?_succName_builtinDefs : Map.get? succName builtinDefs = some Builtin.succ.def

@[simp]

theorem Esolangs.Cornucopia.get?_subName_builtinDefs : Map.get? subName builtinDefs = some Builtin.sub.def

@[simp]

theorem Esolangs.Cornucopia.get!_succName_builtinDefs : Map.get! succName builtinDefs = Builtin.succ.def

@[simp]

theorem Esolangs.Cornucopia.get!_subName_builtinDefs : Map.get! subName builtinDefs = Builtin.sub.def

@[simp]

theorem Esolangs.Cornucopia.Prog.arity_main {prog : Prog} [H : prog.WF'] : prog.main.arity = 1

@[simp]

theorem Esolangs.Cornucopia.Prog.arity_mainName {prog : Prog} [H : prog.WF'] : prog.arity mainName = 1

@[simp]

theorem Esolangs.Cornucopia.Prog.hasDef_mainName {prog : Prog} [H : prog.WF'] : prog.HasDef mainName

@[simp]

theorem Esolangs.Cornucopia.Prog.Compatible.get?_builtin {prog : Prog} {fs : Map String (List ℕ → ℕ)} {name : String} [h : BuiltinC name] (H : prog.Compatible fs) : Map.get? name fs = some (BuiltinC.b name).eval

@[simp]

theorem Esolangs.Cornucopia.Prog.Compatible.get!_builtin {prog : Prog} {fs : Map String (List ℕ → ℕ)} {name : String} [h : BuiltinC name] (H : prog.Compatible fs) : Map.get! name fs = (BuiltinC.b name).eval

theorem Esolangs.Cornucopia.Prog.wfBuiltins_ofDefs {defs : List (String × Def)} (h : (defs.all fun (x : String × Def) => decide (x.1 ∉ List.map (fun (x : Builtin) => x.name) builtins)) = true) : (ofDefs defs).WFBuiltins

@[simp]

theorem Esolangs.Cornucopia.Prog.WFBuiltins.hasDef_builtin {prog : Prog} {name : String} [h₁ : prog.WFBuiltins] [h₂ : BuiltinC name] : prog.HasDef name

@[simp]

theorem Esolangs.Cornucopia.Prog.WFBuiltins.mem_defs_builtin {prog : Prog} {name : String} [h₁ : prog.WFBuiltins] [h₂ : BuiltinC name] : name ∈ prog.defs

@[simp]

theorem Esolangs.Cornucopia.Prog.WFBuiltins.def?_builtin_eq {prog : Prog} {name : String} [h₁ : prog.WFBuiltins] [h₂ : BuiltinC name] : prog.def? name = some (BuiltinC.b name).def

@[simp]

theorem Esolangs.Cornucopia.Prog.WFBuiltins.def_builtin_eq {prog : Prog} {name : String} [h₁ : prog.WFBuiltins] [h₂ : BuiltinC name] : prog.def name = (BuiltinC.b name).def

@[simp]

theorem Esolangs.Cornucopia.Prog.WFBuiltins.arity_builtin_eq {prog : Prog} {name : String} [h₁ : prog.WFBuiltins] [h₂ : BuiltinC name] : prog.arity name = (BuiltinC.b name).arity

@[simp]

theorem Esolangs.Cornucopia.Prog.WFBuiltins.expr_builtin_eq {prog : Prog} {name : String} [h₁ : prog.WFBuiltins] [h₂ : BuiltinC name] : prog.expr name = (BuiltinC.b name).expr

theorem Esolangs.Cornucopia.Prog.mem_defs_of_def? {prog : Prog} {name : String} {d : Def} (h : prog.def? name = some d) : name ∈ prog.defs

theorem Esolangs.Cornucopia.Prog.hasDef_of_def? {prog : Prog} {name : String} {d : Def} (h : prog.def? name = some d) : prog.HasDef name

theorem Esolangs.Cornucopia.Prog.def_of_def? {prog : Prog} {name : String} {d : Def} (h : prog.def? name = some d) : prog.def name = d

theorem Esolangs.Cornucopia.Prog.arity_of_def? {prog : Prog} {name : String} {d : Def} (h : prog.def? name = some d) : prog.arity name = d.arity

theorem Esolangs.Cornucopia.Prog.expr_of_def? {prog : Prog} {name : String} {d : Def} (h : prog.def? name = some d) : prog.expr name = d.expr

theorem Esolangs.Cornucopia.Expr.ind {p : Expr → Prop} (h₁ : ∀ (i : ℕ), p (arg i)) (h₂ : ∀ (name : String) (es : List Expr), (∀ e ∈ es, p e) → p (call name es)) (e : Expr) : p e

theorem Esolangs.Cornucopia.Expr.eq_iff_decideEq {a b : Expr} : a = b ↔ a.decideEq b = true

@[instance_reducible]

instance Esolangs.Cornucopia.instDecidableEqExpr : DecidableEq Expr

Equations

• Esolangs.Cornucopia.instDecidableEqExpr x✝¹ x✝ = decidable_of_bool (x✝¹.decideEq x✝) ⋯

def Esolangs.Cornucopia.instDecidableEqDef.decEq (x✝ x✝¹ : Def) : Decidable (x✝ = x✝¹)

Equations

• Esolangs.Cornucopia.instDecidableEqDef.decEq { arity := a, expr := a_1 } { arity := b, expr := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Esolangs.Cornucopia.instDecidableEqDef : DecidableEq Def

Equations

• Esolangs.Cornucopia.instDecidableEqDef = Esolangs.Cornucopia.instDecidableEqDef.decEq

@[instance_reducible]

instance Esolangs.Cornucopia.instDecidableEqProg : DecidableEq Prog

Equations

• Esolangs.Cornucopia.instDecidableEqProg = Esolangs.Cornucopia.instDecidableEqProg.decEq

def Esolangs.Cornucopia.instDecidableEqProg.decEq (x✝ x✝¹ : Prog) : Decidable (x✝ = x✝¹)

Equations

• Esolangs.Cornucopia.instDecidableEqProg.decEq { defs := a } { defs := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

theorem Esolangs.Cornucopia.Builtin.all {p : Builtin → Prop} : (∀ (b : Builtin), p b) ↔ p succ ∧ p sub

theorem Esolangs.Cornucopia.Builtin.exi {p : Builtin → Prop} : (∃ (b : Builtin), p b) ↔ p succ ∨ p sub

theorem Esolangs.Cornucopia.Prog.def?_ofDefs {defs : List (String × Def)} {name : String} (h : (List.map (fun (x : String × Def) => x.1) defs).Nodup) : (ofDefs defs).def? name = (Option.map Prod.snd (List.find? (fun (x : String × Def) => decide (x.1 = name)) defs)).or (Option.map Builtin.def (List.find? (fun (x : Builtin) => decide (x.name = name)) builtins))

theorem Esolangs.Cornucopia.Prog.eq_ofDefs {defs : List (String × Def)} : { defs := builtinDefs ∪ Map.ofList (Map.ofList defs).toList } = ofDefs defs

theorem Esolangs.Cornucopia.CompatibleDefs.get?_fs {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} {name : String} {f : List ℕ → ℕ} (H : WFDefs' defs) (H₁ : CompatibleDefs (Map.ofList defs) fs) (h : Map.get? name fs = some f) : Map.get? name (builtinFs ∪ fs) = if IsBuiltin name then Map.get? name builtinFs else Map.get? name fs

theorem Esolangs.Cornucopia.CompatibleDefs.get!_fs {defs : List (String × Def)} {fs : Map String (List ℕ → ℕ)} {name : String} {f : List ℕ → ℕ} (H : WFDefs' defs) (H₁ : CompatibleDefs (Map.ofList defs) fs) (h : Map.get? name fs = some f) : Map.get! name (builtinFs ∪ fs) = if IsBuiltin name then Map.get! name builtinFs else Map.get! name fs

@[simp]

theorem Esolangs.Cornucopia.sort_map_builtins : ((List.map (fun (x : Builtin) => x.name) builtins).mergeSort fun (a b : String) => decide (a ≤ b)) = [subName, succName]

@[simp]

theorem Esolangs.Cornucopia.keys_builtinDefs : builtinDefs.keys = [subName, succName]

@[simp]

theorem Esolangs.Cornucopia.keys_builtinFs : builtinFs.keys = [subName, succName]

@[simp]

theorem Esolangs.Cornucopia.fn_eq_fn_iff' {n : ℕ} {f g : List ℕ → ℕ} {xs : List ℕ} : fn n f xs = fn n g xs ↔ xs.length = n → f xs = g xs

theorem Esolangs.Cornucopia.Expr.wf_of_le {prog : Prog} {e : Expr} {k n : ℕ} (h₁ : WF prog k e) (h₂ : k ≤ n) : WF prog n e

theorem Esolangs.Cornucopia.isBuiltin_lit {name : String} : IsBuiltin name ↔ name = "succ" ∨ name = "sub"

theorem Esolangs.Cornucopia.isBuiltin_iff_decide {name : String} : IsBuiltin name ↔ isBuiltin name = true

theorem Esolangs.Cornucopia.imp_fs_and_of {fs : Map String (List ℕ → ℕ)} {name : String} {y z : List ℕ → ℕ} {p : List ℕ → Prop} {n : ℕ} (h₁ : Map.get? name fs = some (fn n y)) (h₂ : ∀ (xs : List ℕ), xs.length = n → z xs = y xs) (h₃ : Map.get! name (builtinFs ∪ fs) = fn n z → ∀ (xs : List ℕ), p xs) (h₀ : ¬IsBuiltin name := by decide) (xs : List ℕ) : (xs.length = n → Map.get? name fs = some (fn n y) → y xs = z xs) ∧ p xs

@[simp]

theorem Esolangs.Cornucopia.Builtin.forall_imp_iff {p : String → Prop} : (∀ (name : String), IsBuiltin name → p name) ↔ ∀ (b : Builtin), p b.name

@[simp]

theorem Esolangs.Cornucopia.Builtin.exists_and_iff {p : String → Prop} : (∃ (name : String), IsBuiltin name ∧ p name) ↔ ∃ (b : Builtin), p b.name

@[simp]

theorem Esolangs.Cornucopia.fn_fn_same {f : List ℕ → ℕ} {n : ℕ} : fn n (fn n f) = fn n f