LeanPool.FormalizationOfBoundedArithmetic.LanguageZambella

inductive FirstOrder.Language.ZambellaFunc : ℕ → Type u

Function symbols for the two-sorted Zambella language.

• zero : ZambellaFunc 0
• one : ZambellaFunc 0
• empty : ZambellaFunc 0
• len : ZambellaFunc 1
• add : ZambellaFunc 2
• mul : ZambellaFunc 2

@[implicit_reducible]

instance FirstOrder.Language.instDecidableEqZambellaFunc {a✝ : ℕ} : DecidableEq (ZambellaFunc a✝)

Equations

• FirstOrder.Language.instDecidableEqZambellaFunc = FirstOrder.Language.instDecidableEqZambellaFunc.decEq

def FirstOrder.Language.instDecidableEqZambellaFunc.decEq {a✝ : ℕ} (x✝ x✝¹ : ZambellaFunc a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

inductive FirstOrder.Language.ZambellaRel : ℕ → Type u

Relation symbols for the two-sorted Zambella language.

• isnum : ZambellaRel 1
• isstr : ZambellaRel 1
• leq : ZambellaRel 2
• mem : ZambellaRel 2

@[implicit_reducible]

instance FirstOrder.Language.instDecidableEqZambellaRel {a✝ : ℕ} : DecidableEq (ZambellaRel a✝)

Equations

• FirstOrder.Language.instDecidableEqZambellaRel = FirstOrder.Language.instDecidableEqZambellaRel.decEq

def FirstOrder.Language.instDecidableEqZambellaRel.decEq {a✝ : ℕ} (x✝ x✝¹ : ZambellaRel a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.zambella : Language

The two-sorted language for bounded arithmetic.

Equations

• FirstOrder.Language.zambella = { Functions := FirstOrder.Language.ZambellaFunc, Relations := FirstOrder.Language.ZambellaRel }

@[implicit_reducible]

instance FirstOrder.Language.instIsOrderedZambella : zambella.IsOrdered

Equations

• FirstOrder.Language.instIsOrderedZambella = { leSymb := FirstOrder.Language.ZambellaRel.leq }

@[implicit_reducible]

instance FirstOrder.Language.instZeroTermZambella {a : Type u} : Zero (zambella.Term a)

Equations

• FirstOrder.Language.instZeroTermZambella = { zero := FirstOrder.Language.Constants.term FirstOrder.Language.ZambellaFunc.zero }

@[implicit_reducible]

instance FirstOrder.Language.instOneTermZambella {a : Type u} : One (zambella.Term a)

Equations

• FirstOrder.Language.instOneTermZambella = { one := FirstOrder.Language.Constants.term FirstOrder.Language.ZambellaFunc.one }

class FirstOrder.Language.HasEmptySet (α : Type u_1) : Type u_1

Types with a distinguished empty set or string element.

• empty : α

  The distinguished empty element.

@[implicit_reducible]

instance FirstOrder.Language.instHasEmptySetTermZambella {a : Type u} : HasEmptySet (zambella.Term a)

Equations

• FirstOrder.Language.instHasEmptySetTermZambella = { empty := FirstOrder.Language.Constants.term FirstOrder.Language.ZambellaFunc.empty }

class FirstOrder.Language.HasLen (α : Type u) (β : Type v) : Type (max u v)

Types with a length map into another type.

• len : α → β

  Length of an object.

@[implicit_reducible]

instance FirstOrder.Language.instHasLenTermZambella {a : Type u} : HasLen (zambella.Term a) (zambella.Term a)

Equations

• FirstOrder.Language.instHasLenTermZambella = { len := FirstOrder.Language.Functions.apply₁ FirstOrder.Language.ZambellaFunc.len }

@[implicit_reducible]

instance FirstOrder.Language.instAddTermZambella {a : Type u} : Add (zambella.Term a)

Equations

• FirstOrder.Language.instAddTermZambella = { add := FirstOrder.Language.Functions.apply₂ FirstOrder.Language.ZambellaFunc.add }

@[implicit_reducible]

instance FirstOrder.Language.instMulTermZambella {a : Type u} : Mul (zambella.Term a)

Equations

• FirstOrder.Language.instMulTermZambella = { mul := FirstOrder.Language.Functions.apply₂ FirstOrder.Language.ZambellaFunc.mul }

class FirstOrder.Language.HasTypesIs (α : Type u_1) : Type u_1

Predicate interface for values that are either numbers or strings.

• int : α → Prop

  The value is a number.

• str : α → Prop

  The value is a string.

• dec (x : α) : int x ∨ str x
• excl (x : α) : (int x → ¬str x) ∧ (str x → ¬int x)

@[implicit_reducible]

instance FirstOrder.Language.instZeroOfStructureZambella {M : Type u_1} [h : zambella.Structure M] : Zero M

Equations

• FirstOrder.Language.instZeroOfStructureZambella = { zero := FirstOrder.Language.Structure.funMap FirstOrder.Language.ZambellaFunc.zero ![] }

@[implicit_reducible]

instance FirstOrder.Language.instOneOfStructureZambella {M : Type u_1} [h : zambella.Structure M] : One M

Equations

• FirstOrder.Language.instOneOfStructureZambella = { one := FirstOrder.Language.Structure.funMap FirstOrder.Language.ZambellaFunc.one ![] }

@[implicit_reducible]

instance FirstOrder.Language.instAddOfStructureZambella {M : Type u_1} [h : zambella.Structure M] : Add M

Equations

• FirstOrder.Language.instAddOfStructureZambella = { add := fun (x y : M) => FirstOrder.Language.Structure.funMap FirstOrder.Language.ZambellaFunc.add ![x, y] }

@[implicit_reducible]

instance FirstOrder.Language.instMulOfStructureZambella {M : Type u_1} [h : zambella.Structure M] : Mul M

Equations

• FirstOrder.Language.instMulOfStructureZambella = { mul := fun (x y : M) => FirstOrder.Language.Structure.funMap FirstOrder.Language.ZambellaFunc.mul ![x, y] }

@[implicit_reducible]

instance FirstOrder.Language.instLEOfStructureZambella {M : Type u_1} [h : zambella.Structure M] : LE M

Equations

• FirstOrder.Language.instLEOfStructureZambella = { le := fun (x y : M) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.ZambellaRel.leq ![x, y] }

@[implicit_reducible]

instance FirstOrder.Language.instHasEmptySetOfStructureZambella {M : Type u_1} [h : zambella.Structure M] : HasEmptySet M

Equations

• FirstOrder.Language.instHasEmptySetOfStructureZambella = { empty := FirstOrder.Language.Structure.funMap FirstOrder.Language.ZambellaFunc.empty ![] }

@[implicit_reducible]

instance FirstOrder.Language.instHasLenOfStructureZambella {M : Type u_1} [h : zambella.Structure M] : HasLen M M

Equations

• FirstOrder.Language.instHasLenOfStructureZambella = { len := fun (x : M) => FirstOrder.Language.Structure.funMap FirstOrder.Language.ZambellaFunc.len ![x] }

@[implicit_reducible]

instance FirstOrder.Language.instMembershipOfStructureZambella {M : Type u_1} [h : zambella.Structure M] : Membership M M

Equations

• FirstOrder.Language.instMembershipOfStructureZambella = { mem := fun (x y : M) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.ZambellaRel.mem ![x, y] }

@[implicit_reducible]

instance FirstOrder.Language.instStructurePeanoOfZambella {M : Type u_1} [h : zambella.Structure M] : peano.Structure M

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance FirstOrder.Language.instOfNatOfStructureZambella {M : Type u_1} [h : zambella.Structure M] (n : ℕ) : OfNat M n

Equations

• FirstOrder.Language.instOfNatOfStructureZambella n = { ofNat := FirstOrder.Language.instOfNatOfStructureZambella.aux n }

def FirstOrder.Language.instOfNatOfStructureZambella.aux {M : Type u_1} [h : zambella.Structure M] : ℕ → M

Equations

• FirstOrder.Language.instOfNatOfStructureZambella.aux 0 = Zero.zero
• FirstOrder.Language.instOfNatOfStructureZambella.aux 1 = One.one
• FirstOrder.Language.instOfNatOfStructureZambella.aux n.succ = FirstOrder.Language.instOfNatOfStructureZambella.aux n + One.one

@[simp]

theorem FirstOrder.Language.realize_zero_to_zero {M : Type u_1} [zambella.Structure M] {a : Type u_4} {env : a → M} : Term.realize env 0 = 0

@[simp]

theorem FirstOrder.Language.realize_one_to_one {M : Type u_1} [zambella.Structure M] {a : Type u_4} {env : a → M} : Term.realize env 1 = 1

@[simp]

theorem FirstOrder.Language.realize_add_to_add {M : Type u_1} [h : zambella.Structure M] {a : Type u_4} {env : a → M} (t u : zambella.Term a) : Term.realize env (t + u) = Term.realize env t + Term.realize env u

@[simp]

theorem FirstOrder.Language.realize_mul_to_mul {M : Type u_1} [zambella.Structure M] {a : Type u_4} {env : a → M} (t u : zambella.Term a) : Term.realize env (t * u) = Term.realize env t * Term.realize env u

theorem FirstOrder.Language.realize_leq_to_leq {M : Type u_1} [h : zambella.Structure M] {a : Type u_4} {env : a → M} {k : ℕ} (t u : zambella.Term (a ⊕ Fin k)) {xs : Fin k → M} : (t.le u).Realize env xs = (Term.realize (Sum.elim env xs) t ≤ Term.realize (Sum.elim env xs) u)

@[simp]

theorem FirstOrder.Language.realize_leq_to_leq' {M : Type u_1} [h : zambella.Structure M] {a : Type u_4} {env : a → M} {k : ℕ} (t u : zambella.Term (a ⊕ Fin k)) {xs : Fin k → M} : (BoundedFormula.rel ZambellaRel.leq ![t, u]).Realize env xs = (Term.realize (Sum.elim env xs) t ≤ Term.realize (Sum.elim env xs) u)

@[simp]

theorem FirstOrder.Language.realize_leq_to_leq'' {M : Type u_1} [h : zambella.Structure M] {a : Type u_4} {env : a → M} {k : ℕ} (t u : zambella.Term (a ⊕ Fin k)) {xs : Fin k → M} : Structure.RelMap ZambellaRel.leq ![Term.realize (Sum.elim env xs) t, Term.realize (Sum.elim env xs) u] ↔ Term.realize (Sum.elim env xs) t ≤ Term.realize (Sum.elim env xs) u

def FirstOrder.Language.Term.IsNum {a : Type u} (t : zambella.Term (a ⊕ Fin 0)) : zambella.Formula a

Formula asserting that a term denotes a number.

Equations

• t.IsNum = FirstOrder.Language.Relations.boundedFormula₁ FirstOrder.Language.ZambellaRel.isnum t

def FirstOrder.Language.Term.IsStr {a : Type u} (t : zambella.Term (a ⊕ Fin 0)) : zambella.Formula a

Formula asserting that a term denotes a string.

Equations

• t.IsStr = FirstOrder.Language.Relations.boundedFormula₁ FirstOrder.Language.ZambellaRel.isstr t

def FirstOrder.Language.Formula.IsNum {n : FvName} (phi : zambella.Formula (Vars1 n)) : zambella.BoundedFormula (Vars1 n) 0

Guard a formula by asserting that its displayed variable is a number.

Equations

• phi.IsNum = FirstOrder.Language.BoundedFormula.imp (FirstOrder.Language.var (Sum.inl Vars1.fv1)).IsNum phi

def FirstOrder.Term.in {a : Type u} {n : ℕ} (t1 t2 : Language.zambella.Term (a ⊕ Fin n)) : Language.zambella.BoundedFormula a n

The membership relation of two terms as a bounded formula

Equations

• FirstOrder.Term.in t1 t2 = FirstOrder.Language.Relations.boundedFormula₂ FirstOrder.Language.ZambellaRel.mem t2 t1

def FirstOrder.Language.«term_∈'_» : Lean.TrailingParserDescr

The membership relation of two terms as a bounded formula

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Term.notin {a : Type u} {n : ℕ} (t1 t2 : Language.zambella.Term (a ⊕ Fin n)) : Language.zambella.BoundedFormula a n

The not-mem relation of two terms as a bounded formula

Equations

• FirstOrder.Term.notin t1 t2 = (FirstOrder.Term.in t1 t2).not

def FirstOrder.Language.«term_∉'_» : Lean.TrailingParserDescr

The not-mem relation of two terms as a bounded formula

Equations

• One or more equations did not get rendered due to their size.

class FirstOrder.Language.ZambellaModel (num str : Type u') extends FirstOrder.Language.zambella.Structure (num ⊕ str), Preorder (num ⊕ str), FirstOrder.Language.zambella.OrderedStructure (num ⊕ str) : Type (max u' u_1)

Two-sorted structures satisfying the intended Zambella typing axioms.

• funMap {n : ℕ} : zambella.Functions n → (Fin n → num ⊕ str) → num ⊕ str
• RelMap {n : ℕ} : zambella.Relations n → (Fin n → num ⊕ str) → Prop
• le : num ⊕ str → num ⊕ str → Prop
• lt : num ⊕ str → num ⊕ str → Prop
• le_refl (a : num ⊕ str) : a ≤ a
• le_trans (a b c : num ⊕ str) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : num ⊕ str) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• relMap_leSymb (x : Fin 2 → num ⊕ str) : Structure.RelMap leSymb x ↔ x 0 ≤ x 1
• ax_realize_isnum {a : Type} {t : zambella.Term (a ⊕ Fin 0)} {v : a → num ⊕ str} : t.IsNum.Realize v ↔ (Term.realize (Sum.elim v Fin.elim0) t).isLeft = true
• ax_realize_isstr {a : Type} {v : a → num ⊕ str} {t : zambella.Term (a ⊕ Fin 0)} : t.IsStr.Realize v ↔ (Term.realize (Sum.elim v Fin.elim0) t).isRight = true
• ax_realize_in {a : Type} {n : ℕ} {t1 t2 : zambella.Term (a ⊕ Fin n)} {v : a → num ⊕ str} {xs : Fin n → num ⊕ str} : (Term.in t1 t2).Realize v xs ↔ Term.realize (Sum.elim v xs) t1 ∈ Term.realize (Sum.elim v xs) t2

def FirstOrder.Language.peanoToZambella : peano →ᴸ zambella

Language homomorphism embedding Peano arithmetic into the Zambella language.

Equations

• One or more equations did not get rendered due to their size.