LeanPool.FormalizationOfBoundedArithmetic.V0

class V0Model (num : Type) (str : outParam Type) extends FirstOrder.Language.HasLen str num, Membership num str, BASICModel num : Type u_1

Two-sorted V0-style models used by this development.

This is a strengthened bundled API: besides the finite V0 comprehension axioms, it includes induction, order, and algebraic laws as fields so later files can build the string-addition theory over a compact typeclass interface.

• len : str → num
• mem : str → num → Prop
• funMap {n : ℕ} : peano.Functions n → (Fin n → num) → num
• RelMap {n : ℕ} : peano.Relations n → (Fin n → num) → Prop
• B1 {x : num} : x + 1 ≠ 0
• B2 (x y : num) : x + 1 = y + 1 → x = y
• B3 (x : num) : x + 0 = x
• B4 {x y : num} : x + (y + 1) = x + y + 1
• B5 {x : num} : x * 0 = 0
• B6 {x y : num} : x * (y + 1) = x * y + x
• B7 {x y : num} : x ≤ y → y ≤ x → x = y
• B8 {x y : num} : x ≤ x + y
• B9 (x : num) : 0 ≤ x
• B10 (x y : num) : x ≤ y ∨ y ≤ x
• B11 (x y : num) : x ≤ y ↔ x < y + 1
• B12 {x : num} : x ≠ 0 → ∃ y ≤ x, y + 1 = x
• L1 {X : str} {y : num} : y ∈ X → y < FirstOrder.Language.HasLen.len X
• L2 {X : str} {y : num} : y + 1 = FirstOrder.Language.HasLen.len X → y ∈ X
• SE {X Y : str} : FirstOrder.Language.HasLen.len X = FirstOrder.Language.HasLen.len Y → (∀ y < FirstOrder.Language.HasLen.len X, y ∈ X ↔ y ∈ Y) → X = Y
• comp1 (b1 b2 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨b1,b2⟩ ∧ ∀ x1 < b1, ∀ x2 < b2, ⟨x1,x2⟩ ∈ Y ↔ x1 = x2
• comp2 (b1 b2 b3 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨⟨b1,b2⟩,b3⟩ ∧ ∀ x1 < b1, ∀ x2 < b2, ∀ x3 < b3, ⟨⟨x1,x2⟩,x3⟩ ∈ Y ↔ x3 = x1
• comp3 (b1 b2 b3 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨⟨b1,b2⟩,b3⟩ ∧ ∀ x1 < b1, ∀ x2 < b2, ∀ x3 < b3, ⟨⟨x1,x2⟩,x3⟩ ∈ Y ↔ x3 = x2
• comp4 (Q1 Q2 : str) (b1 b2 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨b1,b2⟩ ∧ ∀ x1 < b1, ∀ x2 < b2, ⟨x1,x2⟩ ∈ Y ↔ ∃ y ≤ x1, ⟨x1,y⟩ ∈ Q1 ∧ ⟨y,x2⟩ ∈ Q2
• comp5 (a b1 b2 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨b1,b2⟩ ∧ ∀ x < b1, ∀ y < b2, ⟨x,y⟩ ∈ Y ↔ y = a
• comp6 (Q1 Q2 : str) (b1 b2 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨b1,b2⟩ ∧ ∀ x < b1, ∀ y < b2, ⟨x,y⟩ ∈ Y ↔ ∃ z1 ≤ y, ∃ z2 ≤ y, ⟨x,z1⟩ ∈ Q1 ∧ ⟨x,z2⟩ ∈ Q2 ∧ y = z1 + z2
• comp7 (Q1 Q2 : str) (b1 b2 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨b1,b2⟩ ∧ ∀ x < b1, ∀ y < b2, ⟨x,y⟩ ∈ Y ↔ ∃ z1 ≤ y, ∃ z2 ≤ y, ⟨x,z1⟩ ∈ Q1 ∧ ⟨x,z2⟩ ∈ Q2 ∧ y = z1 * z2
• comp8 (Q1 Q2 : str) (c b : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ b ∧ ∀ x < b, x ∈ Y ↔ ∃ y1 ≤ c, ∃ y2 ≤ c, ⟨x,y1⟩ ∈ Q1 ∧ ⟨x,y2⟩ ∈ Q2 ∧ y1 ≤ y2
• comp9 (X Q : str) (c b : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ b ∧ ∀ x < b, x ∈ Y ↔ ∃ y ≤ c, ⟨x,y⟩ ∈ Q ∧ y ∈ X
• comp10 (Q : str) (b : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ b ∧ ∀ x < b, x ∈ Y ↔ x ∉ Q
• comp11 (Q1 Q2 : str) (b : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ b ∧ ∀ x < b, x ∈ Y ↔ x ∈ Q1 ∧ x ∈ Q2
• comp12 (Q : str) (c b : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ b ∧ ∀ x < b, x ∈ Y ↔ ∀ y ≤ c, ⟨x,y⟩ ∈ Q
• xmin_comp_ax (X : str) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ FirstOrder.Language.HasLen.len X ∧ ∀ z < FirstOrder.Language.HasLen.len X, z ∈ Y ↔ ∀ y ≤ z, y ∉ X
• comp_xind_ax (X : str) (z : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ z + 1 ∧ ∀ y < z + 1, y ∈ Y ↔ y ∉ X
• prop_induction_ax (P : num → Prop) : P 0 → (∀ (i : num), P i → P (i + 1)) → ∀ (i : num), P i
• open_induction_ax {n : FvName} {a : Type} [IsEnum a] (phi : FirstOrder.Language.peano.BoundedFormula (Vars1 n ⊕ a) 0) : phi.IsOpen → num ⊨ mkInductionSentence phi
• delta0_induction_ax {n : FvName} {a : Type} [IsEnum a] (phi : FirstOrder.Language.peano.BoundedFormula (Vars1 n ⊕ a) 0) : phi.IsDelta0 → num ⊨ mkInductionSentence phi
• le_trans (x y z : num) : x ≤ y → y ≤ z → x ≤ z
• zero_add (x : num) : 0 + x = x
• add_left_cancel (x : num) : IsAddLeftRegular x
• add_right_cancel (x : num) : IsAddRightRegular x
• add_assoc (x y z : num) : x + y + z = x + (y + z)
• le_total (a b : num) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE num

  Decidability of the order relation on numbers.

• exists_add_of_le {a b : num} : a ≤ b → ∃ (c : num), b = a + c
• add_le_add_left (a b : num) : a ≤ b → ∀ (c : num), c + a ≤ c + b
• le_antisymm (a b : num) : a ≤ b → b ≤ a → a = b
• add_comm (a b : num) : a + b = b + a

@[implicit_reducible]

instance V0Model.instPartialOrder {num str : Type} [M : V0Model num str] : PartialOrder num

Equations

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

@[implicit_reducible]

instance V0Model.instAddZeroClass {num str : Type} [M : V0Model num str] : AddZeroClass num

Equations

• V0Model.instAddZeroClass = { toZero := FirstOrder.Language.peano.instZeroOfStructure, toAdd := FirstOrder.Language.peano.instAddOfStructure, zero_add := ⋯, add_zero := ⋯ }

instance V0Model.instIsLeftCancelAdd {num str : Type} [M : V0Model num str] : IsLeftCancelAdd num

instance V0Model.instIsRightCancelAdd {num str : Type} [M : V0Model num str] : IsRightCancelAdd num

@[implicit_reducible]

instance V0Model.instAddMonoid {num str : Type} [M : V0Model num str] : AddMonoid num

Equations

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

@[implicit_reducible]

instance V0Model.instLinearOrder {num str : Type} [M : V0Model num str] : LinearOrder num

Equations

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

instance V0Model.instCanonicallyOrderedAdd {num str : Type} [M : V0Model num str] : CanonicallyOrderedAdd num

@[implicit_reducible]

instance V0Model.instAddCommMonoid {num str : Type} [M : V0Model num str] : AddCommMonoid num

Equations

• V0Model.instAddCommMonoid = { toAddMonoid := V0Model.instAddMonoid, add_comm := ⋯ }

@[implicit_reducible]

instance V0Model.instPartialOrder_1 {num str : Type} [M : V0Model num str] : PartialOrder num

Equations

• V0Model.instPartialOrder_1 = { toPreorder := V0Model.instPartialOrder.toPreorder, le_antisymm := ⋯ }

instance V0Model.instIsOrderedAddMonoid {num str : Type} [M : V0Model num str] : IsOrderedAddMonoid num

theorem V0Model.xmin_comp {num str : Type} [M : V0Model num str] (X : str) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ FirstOrder.Language.HasLen.len X ∧ ∀ z < FirstOrder.Language.HasLen.len X, z ∈ Y ↔ ∀ y ≤ z, y ∉ X

theorem V0Model.ex_elt_of_len_pos {num str : Type} [M : V0Model num str] {X : str} : 0 < FirstOrder.Language.HasLen.len X → ∃ x ∈ X, x + 1 = FirstOrder.Language.HasLen.len X

theorem V0Model.lt_succ {num str : Type} [M : V0Model num str] (x : num) : x < x + 1

theorem V0Model.len_not_in {num str : Type} [M : V0Model num str] {X : str} : FirstOrder.Language.HasLen.len X ∉ X

theorem V0Model.not_lt_zero {num str : Type} [M : V0Model num str] {x : num} : ¬x < 0

instance V0Model.instCanonicallyOrderedAdd_1 {num str : Type} [M : V0Model num str] : CanonicallyOrderedAdd num

theorem V0Model.xmin {num str : Type} [M : V0Model num str] {X : str} : 0 < FirstOrder.Language.HasLen.len X → ∃ x < FirstOrder.Language.HasLen.len X, x ∈ X ∧ ∀ y < x, y ∉ X

theorem V0Model.comp_xind {num str : Type} [M : V0Model num str] (X : str) (z : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ z + 1 ∧ ∀ y < z + 1, y ∈ Y ↔ y ∉ X

theorem V0Model.len_ne_zero_of_in {num str : Type} [M : V0Model num str] {x : num} {X : str} : x ∈ X → FirstOrder.Language.HasLen.len X ≠ 0

theorem V0Model.xind {num str : Type} [M : V0Model num str] {X : str} {z : num} : 0 ∈ X → (∀ y < z, y ∈ X → y + 1 ∈ X) → z ∈ X

theorem V0Model.ind_of_comp {num str : Type} [M : V0Model num str] (P : num → Prop) : (∀ (y : num), ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ y ∧ ∀ z < y, z ∈ Y ↔ P z) → P 0 → (∀ (x : num), P x → P (x + 1)) → ∀ (x : num), P x

theorem V0Model.ind_strengthened_v0 {num str : Type} [M : V0Model num str] (P : num → Prop) : (∀ (y : num), ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ y ∧ ∀ z < y, z ∈ Y ↔ P z) → P 0 → (∀ (x : num), P x → P (x + 1)) → ∀ (x : num), P x

Named alias emphasizing that this induction theorem uses the strengthened V0Model bundle.

@[implicit_reducible]

instance V0Model.instIDelta0Model {num str : Type} [M : V0Model num str] : IDelta0Model num

Equations

• V0Model.instIDelta0Model = { toBASICModel := M.toBASICModel, open_induction := ⋯, delta0_induction := ⋯ }

class HasSucc (α : Type u_1) : Type u_1

Types equipped with a successor operation.

• succ : α → α

  Successor operation.

def Carry {num str : Type} [V0Model num str] (i : num) (X Y : str) : Prop

Carry predicate for binary string addition below position i.

Equations

• Carry i X Y = ∃ k < i, k ∈ X ∧ k ∈ Y ∧ ∀ j < i, k < j → j ∈ X ∨ j ∈ Y

class V0ExtModel (num : Type) (str : outParam Type) extends Zero str, HasSucc str, Add str, V0Model num str : Type u_1

Extension of V0 with string successor and string addition.

• zero : str
• succ : str → str
• add : str → str → str
• len : str → num
• mem : str → num → Prop
• funMap {n : ℕ} : peano.Functions n → (Fin n → num) → num
• RelMap {n : ℕ} : peano.Relations n → (Fin n → num) → Prop
• B1 {x : num} : x + 1 ≠ 0
• B2 (x y : num) : x + 1 = y + 1 → x = y
• B3 (x : num) : x + 0 = x
• B4 {x y : num} : x + (y + 1) = x + y + 1
• B5 {x : num} : x * 0 = 0
• B6 {x y : num} : x * (y + 1) = x * y + x
• B7 {x y : num} : x ≤ y → y ≤ x → x = y
• B8 {x y : num} : x ≤ x + y
• B9 (x : num) : 0 ≤ x
• B10 (x y : num) : x ≤ y ∨ y ≤ x
• B11 (x y : num) : x ≤ y ↔ x < y + 1
• B12 {x : num} : x ≠ 0 → ∃ y ≤ x, y + 1 = x
• L1 {X : str} {y : num} : y ∈ X → y < FirstOrder.Language.HasLen.len X
• L2 {X : str} {y : num} : y + 1 = FirstOrder.Language.HasLen.len X → y ∈ X
• SE {X Y : str} : FirstOrder.Language.HasLen.len X = FirstOrder.Language.HasLen.len Y → (∀ y < FirstOrder.Language.HasLen.len X, y ∈ X ↔ y ∈ Y) → X = Y
• comp1 (b1 b2 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨b1,b2⟩ ∧ ∀ x1 < b1, ∀ x2 < b2, ⟨x1,x2⟩ ∈ Y ↔ x1 = x2
• comp2 (b1 b2 b3 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨⟨b1,b2⟩,b3⟩ ∧ ∀ x1 < b1, ∀ x2 < b2, ∀ x3 < b3, ⟨⟨x1,x2⟩,x3⟩ ∈ Y ↔ x3 = x1
• comp3 (b1 b2 b3 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨⟨b1,b2⟩,b3⟩ ∧ ∀ x1 < b1, ∀ x2 < b2, ∀ x3 < b3, ⟨⟨x1,x2⟩,x3⟩ ∈ Y ↔ x3 = x2
• comp4 (Q1 Q2 : str) (b1 b2 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨b1,b2⟩ ∧ ∀ x1 < b1, ∀ x2 < b2, ⟨x1,x2⟩ ∈ Y ↔ ∃ y ≤ x1, ⟨x1,y⟩ ∈ Q1 ∧ ⟨y,x2⟩ ∈ Q2
• comp5 (a b1 b2 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨b1,b2⟩ ∧ ∀ x < b1, ∀ y < b2, ⟨x,y⟩ ∈ Y ↔ y = a
• comp6 (Q1 Q2 : str) (b1 b2 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨b1,b2⟩ ∧ ∀ x < b1, ∀ y < b2, ⟨x,y⟩ ∈ Y ↔ ∃ z1 ≤ y, ∃ z2 ≤ y, ⟨x,z1⟩ ∈ Q1 ∧ ⟨x,z2⟩ ∈ Q2 ∧ y = z1 + z2
• comp7 (Q1 Q2 : str) (b1 b2 : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ ⟨b1,b2⟩ ∧ ∀ x < b1, ∀ y < b2, ⟨x,y⟩ ∈ Y ↔ ∃ z1 ≤ y, ∃ z2 ≤ y, ⟨x,z1⟩ ∈ Q1 ∧ ⟨x,z2⟩ ∈ Q2 ∧ y = z1 * z2
• comp8 (Q1 Q2 : str) (c b : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ b ∧ ∀ x < b, x ∈ Y ↔ ∃ y1 ≤ c, ∃ y2 ≤ c, ⟨x,y1⟩ ∈ Q1 ∧ ⟨x,y2⟩ ∈ Q2 ∧ y1 ≤ y2
• comp9 (X Q : str) (c b : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ b ∧ ∀ x < b, x ∈ Y ↔ ∃ y ≤ c, ⟨x,y⟩ ∈ Q ∧ y ∈ X
• comp10 (Q : str) (b : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ b ∧ ∀ x < b, x ∈ Y ↔ x ∉ Q
• comp11 (Q1 Q2 : str) (b : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ b ∧ ∀ x < b, x ∈ Y ↔ x ∈ Q1 ∧ x ∈ Q2
• comp12 (Q : str) (c b : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ b ∧ ∀ x < b, x ∈ Y ↔ ∀ y ≤ c, ⟨x,y⟩ ∈ Q
• xmin_comp_ax (X : str) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ FirstOrder.Language.HasLen.len X ∧ ∀ z < FirstOrder.Language.HasLen.len X, z ∈ Y ↔ ∀ y ≤ z, y ∉ X
• comp_xind_ax (X : str) (z : num) : ∃ (Y : str), FirstOrder.Language.HasLen.len Y ≤ z + 1 ∧ ∀ y < z + 1, y ∈ Y ↔ y ∉ X
• prop_induction_ax (P : num → Prop) : P 0 → (∀ (i : num), P i → P (i + 1)) → ∀ (i : num), P i
• open_induction_ax {n : FvName} {a : Type} [IsEnum a] (phi : FirstOrder.Language.peano.BoundedFormula (Vars1 n ⊕ a) 0) : phi.IsOpen → num ⊨ mkInductionSentence phi
• delta0_induction_ax {n : FvName} {a : Type} [IsEnum a] (phi : FirstOrder.Language.peano.BoundedFormula (Vars1 n ⊕ a) 0) : phi.IsDelta0 → num ⊨ mkInductionSentence phi
• le_trans (x y z : num) : x ≤ y → y ≤ z → x ≤ z
• zero_add (x : num) : 0 + x = x
• add_left_cancel (x : num) : IsAddLeftRegular x
• add_right_cancel (x : num) : IsAddRightRegular x
• add_assoc (x y z : num) : x + y + z = x + (y + z)
• le_total (a b : num) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE num
• exists_add_of_le {a b : num} : a ≤ b → ∃ (c : num), b = a + c
• add_le_add_left (a b : num) : a ≤ b → ∀ (c : num), c + a ≤ c + b
• le_antisymm (a b : num) : a ≤ b → b ≤ a → a = b
• add_comm (a b : num) : a + b = b + a
• ax_empty {z : num} : z ∈ 0 ↔ z < 0
• ax_succ {X : str} {i : num} : i ∈ HasSucc.succ X ↔ i ≤ FirstOrder.Language.HasLen.len X ∧ ((i ∈ X ∧ ∃ j < i, j ∉ X) ∨ i ∉ X ∧ ∀ j < i, j ∈ X)
• ax_add {X Y : str} {i : num} : i ∈ X + Y ↔ i < FirstOrder.Language.HasLen.len X + FirstOrder.Language.HasLen.len Y ∧ Xor (Xor (i ∈ X) (i ∈ Y)) (Carry i X Y)

theorem len_empty {num str : Type} [M : V0ExtModel num str] : FirstOrder.Language.HasLen.len 0 = 0

def Maj (P Q R : Prop) : Prop

Majority predicate on three propositions.

Equations

• Maj P Q R = (P ∧ Q ∧ ¬R ∨ P ∧ ¬Q ∧ R ∨ ¬P ∧ Q ∧ R ∨ P ∧ Q ∧ R)

theorem Maj_true2 {P Q R : Prop} : Q → (Maj P Q R ↔ P ∨ R)

theorem Maj_true3 {P Q R : Prop} : R → (Maj P Q R ↔ P ∨ Q)

theorem carry_rec1 {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : Carry i X Y → i ∈ X ∨ i ∈ Y → Carry (i + 1) X Y

theorem not_lt_self {num str : Type} [M : V0ExtModel num str] (i : num) : ¬i < i

theorem carry_rec2 {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : i ∈ X ∧ i ∈ Y → Carry (i + 1) X Y

theorem carry_rec {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : ¬Carry 0 X Y ∧ (Carry (i + 1) X Y ↔ Maj (Carry i X Y) (i ∈ X) (i ∈ Y))

theorem exists_of_len_lt {num str : Type} [M : V0ExtModel num str] {X Y : str} : FirstOrder.Language.HasLen.len X < FirstOrder.Language.HasLen.len Y → ∃ z ∈ Y, z ∉ X ∧ z + 1 = FirstOrder.Language.HasLen.len Y

theorem exists_of_len_lt' {num str : Type} [M : V0ExtModel num str] {X : str} {i : num} : i < FirstOrder.Language.HasLen.len X → ∃ z ∈ X, i ≤ z ∧ z + 1 = FirstOrder.Language.HasLen.len X

theorem len_pos_of_exists {num str : Type} [M : V0ExtModel num str] {i : num} {X : str} : i ∈ X → FirstOrder.Language.HasLen.len X > 0

theorem lt_add_right_of_mem_left {num str : Type} [M : V0ExtModel num str] {X : str} {b i : num} (h : i ∈ X) : i < FirstOrder.Language.HasLen.len X + b

A position belonging to X lies below len X + b for any bound b.

theorem lt_add_left_of_mem_right {num str : Type} [M : V0ExtModel num str] {Y : str} {a i : num} (h : i ∈ Y) : i < a + FirstOrder.Language.HasLen.len Y

A position belonging to Y lies below a + len Y for any bound a.

theorem xor3_split {P Q R : Prop} : Xor (Xor P Q) R ↔ P ∧ ¬Q ∧ ¬R ∨ ¬P ∧ Q ∧ ¬R ∨ ¬P ∧ ¬Q ∧ R ∨ P ∧ Q ∧ R

theorem carry_lt_add_len {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : Carry i X Y → i < FirstOrder.Language.HasLen.len X + FirstOrder.Language.HasLen.len Y

theorem str_eq_of_mem_iff {num str : Type} [M : V0ExtModel num str] {X Y : str} : (∀ (y : num), y ∈ X ↔ y ∈ Y) → X = Y