Model

Difficulty: hard — 6 definitions, 0 abbreviations, 4 lemmas, 5 theorems, 0 examples.

definition lemma theorem

legend

Arithmetic here is the semantic side of the article “Separation Logic and Non-Peano Arithmetic”, read as a theory of models rather than as a proof system.

A model is a universe of elements laid out in a line, with one demand on the layout: everything up to a given element is finite in number. Everything else is read off the order. An element is a zero when it lies below all others, a maximum when all others lie below it, and a successor of \(a\) when it is the least element strictly above \(a\). A maximum has nothing above it, so its successor is a zero instead: counting past the top wraps around to the bottom.

Peano’s postulate is the statement that a zero is the successor of nothing. Its negation is the statement that some zero is a successor. Those two split the models exactly in half. Negating the postulate is the same as the universe being finite, so the postulate itself is the same as the universe being infinite. The natural numbers satisfy it. Each universe \(\{0, \dots, n-1\}\) with addition modulo \(n\) negates it.

The axioms of a model

Structure.Arithmetic.Arith

A model of arithmetic: a universe whose elements are linearly ordered, with a least element, with at least two elements, and where everything up to a given element is finite in number.

model-of-arithmetic

structure Structure.Arithmetic.Arith.{u_1} (U : Type u_1) : Type u_1

The less-equal relation: x ≤ y

Conventions for notations in identifiers:
- The recommended spelling of ≤ in identifiers is le.
(inherited from LE)
```
le : α → α → Prop
```
The less-than relation: x < y

Conventions for notations in identifiers:
- The recommended spelling of < in identifiers is lt.
(inherited from LT)
```
lt : α → α → Prop
```
(inherited from Preorder)
```
le_refl : ∀ (a : α), a ≤ a
```

(inherited from Preorder)

le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c

(inherited from Preorder)

lt_iff_le_not_ge : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a

(inherited from PartialOrder)

le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b

Returns the lesser of its two arguments.

Conventions for notations in identifiers:
- The recommended spelling of min in identifiers is min.
- The recommended spelling of ⊓ in identifiers is inf (⊓ is the preferred notation for min when the type is not linearly ordered.).
(inherited from Min)
```
min : α → α → α
```
Returns the greater of its two arguments.

Conventions for notations in identifiers:
- The recommended spelling of max in identifiers is max.
- The recommended spelling of ⊔ in identifiers is sup (⊔ is the preferred notation for max when the type is not linearly ordered.).
(inherited from Max)
```
max : α → α → α
```
Compare two elements in α using the comparator contained in an [Ord α] instance.

(inherited from Ord)
```
compare : α → α → Ordering
```

A linear order is total.

(inherited from LinearOrder)

le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

In a linearly ordered type, we assume the order relations are all decidable.

(inherited from LinearOrder)
```
toDecidableLE : DecidableLE α
```
In a linearly ordered type, we assume the order relations are all decidable.

(inherited from LinearOrder)
```
toDecidableEq : DecidableEq α
```
In a linearly ordered type, we assume the order relations are all decidable.

(inherited from LinearOrder)
```
toDecidableLT : DecidableLT α
```
The minimum function is equivalent to the one you get from minOfLe.

(inherited from LinearOrder)
```
min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
```
The minimum function is equivalent to the one you get from maxOfLe.

(inherited from LinearOrder)
```
max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
```
Comparison via compare is equal to the canonical comparison given decidable < and =.

(inherited from LinearOrder)
```
compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
```
The bot (⊥, \bot) element

Conventions for notations in identifiers:
- The recommended spelling of ⊥ in identifiers is bot.
(inherited from Bot)
```
bot : α
```
⊥ is the least element

(inherited from OrderBot)
```
bot_le : ∀ (a : α), ⊥ ≤ a
```
In a nontrivial type, there exists a pair of distinct terms.

(inherited from Nontrivial)
```
exists_pair_ne : ∃ x y, x ≠ y
```
Everything up to \(x\) is finite in number.
```
reach : ∀ (x : U), (Set.Iic x).Finite
```

Show details

Outer dependencies: (none)

Mathlib dependencies: LinearOrder, Nontrivial, OrderBot, Set.Finite, Set.Iic

Lean core dependencies: Eq, HEq, eq_of_heq

Structure.Arithmetic.Z

\(x\) is a zero: it lies below every element.

zero

def Structure.Arithmetic.Z.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (x : U) : Prop

Show details

| Structure.Arithmetic.Z x = ∀ (y : U), x ≤ y

Complexity: 47 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Structure.Arithmetic.M

\(a\) is a maximum: every element lies below it.

def Structure.Arithmetic.M.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (a : U) : Prop

Show details

| Structure.Arithmetic.M a = ∀ (y : U), y ≤ a

Complexity: 47 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Used by: Structure.Arithmetic.S, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.S_lt, Structure.Arithmetic.S_unique, Structure.Arithmetic.exists_S_of_not_Z, Structure.Arithmetic.instDefS, Structure.Arithmetic.instPeanoNat, Structure.Arithmetic.lt_succ, Structure.Arithmetic.ultrafinitism

Structure.Arithmetic.S

\(v\) is a successor of \(a\): it lies strictly above \(a\), and it is the least such element. A maximum has nothing strictly above it, so a maximum has a zero for its successor: counting past the top wraps around to the bottom.

successor

def Structure.Arithmetic.S.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (a v : U) : Prop

Show details

| Structure.Arithmetic.S a v =
  ((a < v ∧ ∀ (z : U), a < z → v ≤ z) ∨ Structure.Arithmetic.M a ∧ Structure.Arithmetic.Z v)

Complexity: 147 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.M, Structure.Arithmetic.Z

Lean core dependencies: And, Or

Peano’s postulate and the natural numbers

Structure.Arithmetic.Peano

A model where a zero is the successor of nothing.

peano-postulate

structure Structure.Arithmetic.Peano.{u_2} (U : Type u_2) : Type u_2

The less-equal relation: x ≤ y

Conventions for notations in identifiers:
- The recommended spelling of ≤ in identifiers is le.
(inherited from LE)
```
le : α → α → Prop
```
The less-than relation: x < y

Conventions for notations in identifiers:
- The recommended spelling of < in identifiers is lt.
(inherited from LT)
```
lt : α → α → Prop
```
(inherited from Preorder)
```
le_refl : ∀ (a : α), a ≤ a
```

(inherited from Preorder)

le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c

(inherited from Preorder)

lt_iff_le_not_ge : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a

(inherited from PartialOrder)

le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b

Returns the lesser of its two arguments.

Conventions for notations in identifiers:
- The recommended spelling of min in identifiers is min.
- The recommended spelling of ⊓ in identifiers is inf (⊓ is the preferred notation for min when the type is not linearly ordered.).
(inherited from Min)
```
min : α → α → α
```
Returns the greater of its two arguments.

Conventions for notations in identifiers:
- The recommended spelling of max in identifiers is max.
- The recommended spelling of ⊔ in identifiers is sup (⊔ is the preferred notation for max when the type is not linearly ordered.).
(inherited from Max)
```
max : α → α → α
```
Compare two elements in α using the comparator contained in an [Ord α] instance.

(inherited from Ord)
```
compare : α → α → Ordering
```

A linear order is total.

(inherited from LinearOrder)

le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

In a linearly ordered type, we assume the order relations are all decidable.

(inherited from LinearOrder)
```
toDecidableLE : DecidableLE α
```
In a linearly ordered type, we assume the order relations are all decidable.

(inherited from LinearOrder)
```
toDecidableEq : DecidableEq α
```
In a linearly ordered type, we assume the order relations are all decidable.

(inherited from LinearOrder)
```
toDecidableLT : DecidableLT α
```
The minimum function is equivalent to the one you get from minOfLe.

(inherited from LinearOrder)
```
min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
```
The minimum function is equivalent to the one you get from maxOfLe.

(inherited from LinearOrder)
```
max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
```
Comparison via compare is equal to the canonical comparison given decidable < and =.

(inherited from LinearOrder)
```
compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
```
The bot (⊥, \bot) element

Conventions for notations in identifiers:
- The recommended spelling of ⊥ in identifiers is bot.
(inherited from Bot)
```
bot : α
```
⊥ is the least element

(inherited from OrderBot)
```
bot_le : ∀ (a : α), ⊥ ≤ a
```
In a nontrivial type, there exists a pair of distinct terms.

(inherited from Nontrivial)
```
exists_pair_ne : ∃ x y, x ≠ y
```
Everything up to \(x\) is finite in number.

(inherited from Structure.Arithmetic.Arith)
```
reach : ∀ (x : U), (Set.Iic x).Finite
```

No element has a zero for its successor.

peano : ∀ (x y : U), ¬(Structure.Arithmetic.Z y ∧ Structure.Arithmetic.S x y)

Show details

Outer dependencies: (none)

Inner dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.S, Structure.Arithmetic.Z

Lean core dependencies: And, Eq, HEq, Not, eq_of_heq

Used by: Structure.Arithmetic.Tower.instPeanoColimit, Structure.Arithmetic.count, Structure.Arithmetic.count_strictMono, Structure.Arithmetic.count_succ, Structure.Arithmetic.count_surjective, Structure.Arithmetic.eq_succ_of_S, Structure.Arithmetic.instPeanoNat, Structure.Arithmetic.instPeanoStandard, Structure.Arithmetic.lt_succ, Structure.Arithmetic.peanoOrderIso

Structure.Arithmetic.instArithNat

The natural numbers form a model: everything up to \(x\) lies among the finitely many numbers \(0, \dots, x\).

instance Structure.Arithmetic.instArithNat : Structure.Arithmetic.Arith ℕ

Show details

| Structure.Arithmetic.instArithNat =
  { toLinearOrder := Nat.instLinearOrder, toOrderBot := Nat.instOrderBot,
    toNontrivial := Nat.instNontrivial, reach := Structure.Arithmetic.instArithNat._proof_1 }

Complexity: 11 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Mathlib dependencies: Set.finite_Iic

Lean core dependencies: Nat

Used by: Structure.Arithmetic.S_iff_succ, Structure.Arithmetic.Z_iff_zero, Structure.Arithmetic.instPeanoNat

Structure.Arithmetic.instPeanoNat

The natural numbers satisfy Peano’s postulate: \(0\) is a successor of nothing, since there is no greatest number to wrap around.

instance Structure.Arithmetic.instPeanoNat : Structure.Arithmetic.Peano ℕ

Show details

| Structure.Arithmetic.instPeanoNat =
  { toArith := Structure.Arithmetic.instArithNat,
    peano := Structure.Arithmetic.instPeanoNat._proof_3 }

Complexity: 7 (size of the value term)

Outer dependencies: Structure.Arithmetic.Peano

Inner dependencies: Structure.Arithmetic.M, Structure.Arithmetic.S, Structure.Arithmetic.Z, Structure.Arithmetic.instArithNat

Lean core dependencies: And, Bool, Decidable.decide, Eq, Eq.symm, Eq.trans, False, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.natCast_nonneg, Int.sub_eq_zero_of_eq, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.le_zero, absurd, id, le_of_le_of_eq, of_decide_eq_true

Used by: (none)

Structure.Arithmetic.Z_iff_zero

Among the natural numbers, the zero is \(0\).

theorem Structure.Arithmetic.Z_iff_zero (x : ℕ) : Structure.Arithmetic.Z x ↔ x = 0

Show details

fun x =>
  { mp := fun h => Nat.le_zero.mp (h 0),
    mpr := fun h y =>
      Decidable.byContradiction fun a => Structure.Arithmetic.Z_iff_zero._proof_1_1 x h y a }

Complexity: 201 (size of the value term)

Dependencies: Structure.Arithmetic.Z, Structure.Arithmetic.instArithNat

Lean core dependencies: Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.symm, Eq.trans, Iff, Int, Int.add_one_le_of_lt, Int.natCast_nonneg, Int.sub_eq_zero_of_eq, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_congr, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.le_zero, Nat.lt_of_not_le, Not, id, le_of_le_of_eq, of_decide_eq_true

Used by: (none)

Structure.Arithmetic.S_iff_succ

Among the natural numbers, the successor of \(a\) is \(a + 1\), and it never wraps around.

theorem Structure.Arithmetic.S_iff_succ (a v : ℕ) : Structure.Arithmetic.S a v ↔ v = a + 1

Show details

fun a v =>
  id
    {
      mp := fun a_1 =>
        Or.casesOn a_1
          (fun h =>
            And.casesOn h fun h1 h2 =>
              have this :=
                h2 (a + 1)
                  (Decidable.byContradiction fun a_2 =>
                    Structure.Arithmetic.S_iff_succ._proof_1_4 a v a_2);
              Decidable.byContradiction fun a_2 =>
                Structure.Arithmetic.S_iff_succ._proof_1_5 a v h1 this a_2)
          fun h =>
          And.casesOn h fun h1 right =>
            have this := h1 (a + 1);
            Decidable.byContradiction fun a_2 => Structure.Arithmetic.S_iff_succ._proof_1_6 a this,
      mpr := fun a_1 =>
        Eq.symm a_1 ▸
          Or.inl
            ⟨Decidable.byContradiction fun a_2 => Structure.Arithmetic.S_iff_succ._proof_1_7 a a_2,
              fun z hz =>
              Decidable.byContradiction fun a_2 =>
                Structure.Arithmetic.S_iff_succ._proof_1_8 a z hz a_2⟩ }

Complexity: 3461 (size of the value term)

Dependencies: Structure.Arithmetic.S, Structure.Arithmetic.instArithNat

Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.symm, Eq.trans, False, GT.gt, Iff, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.le_of_not_lt, Nat.lt_of_not_le, Nat.lt_or_gt_of_ne, Not, Or, Or.elim, id, le_of_le_of_eq, of_decide_eq_true

Used by: (none)

Negating the postulate, and the finite models

A model has at least two elements, so the finite models are the universes \(\{0, \dots, n-1\}\) with \(2 \le n\). Their arithmetic is arithmetic modulo \(n\).

Structure.Arithmetic.NonPeano

A model where some zero is a successor.

structure Structure.Arithmetic.NonPeano.{u_2} (U : Type u_2) : Type u_2

The less-equal relation: x ≤ y

Conventions for notations in identifiers:
- The recommended spelling of ≤ in identifiers is le.
(inherited from LE)
```
le : α → α → Prop
```
The less-than relation: x < y

Conventions for notations in identifiers:
- The recommended spelling of < in identifiers is lt.
(inherited from LT)
```
lt : α → α → Prop
```
(inherited from Preorder)
```
le_refl : ∀ (a : α), a ≤ a
```

(inherited from Preorder)

le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c

(inherited from Preorder)

lt_iff_le_not_ge : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a

(inherited from PartialOrder)

le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b

Returns the lesser of its two arguments.

Conventions for notations in identifiers:
- The recommended spelling of min in identifiers is min.
- The recommended spelling of ⊓ in identifiers is inf (⊓ is the preferred notation for min when the type is not linearly ordered.).
(inherited from Min)
```
min : α → α → α
```
Returns the greater of its two arguments.

Conventions for notations in identifiers:
- The recommended spelling of max in identifiers is max.
- The recommended spelling of ⊔ in identifiers is sup (⊔ is the preferred notation for max when the type is not linearly ordered.).
(inherited from Max)
```
max : α → α → α
```
Compare two elements in α using the comparator contained in an [Ord α] instance.

(inherited from Ord)
```
compare : α → α → Ordering
```

A linear order is total.

(inherited from LinearOrder)

le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

In a linearly ordered type, we assume the order relations are all decidable.

(inherited from LinearOrder)
```
toDecidableLE : DecidableLE α
```
In a linearly ordered type, we assume the order relations are all decidable.

(inherited from LinearOrder)
```
toDecidableEq : DecidableEq α
```
In a linearly ordered type, we assume the order relations are all decidable.

(inherited from LinearOrder)
```
toDecidableLT : DecidableLT α
```
The minimum function is equivalent to the one you get from minOfLe.

(inherited from LinearOrder)
```
min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
```
The minimum function is equivalent to the one you get from maxOfLe.

(inherited from LinearOrder)
```
max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
```
Comparison via compare is equal to the canonical comparison given decidable < and =.

(inherited from LinearOrder)
```
compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
```
The bot (⊥, \bot) element

Conventions for notations in identifiers:
- The recommended spelling of ⊥ in identifiers is bot.
(inherited from Bot)
```
bot : α
```
⊥ is the least element

(inherited from OrderBot)
```
bot_le : ∀ (a : α), ⊥ ≤ a
```
In a nontrivial type, there exists a pair of distinct terms.

(inherited from Nontrivial)
```
exists_pair_ne : ∃ x y, x ≠ y
```
Everything up to \(x\) is finite in number.

(inherited from Structure.Arithmetic.Arith)
```
reach : ∀ (x : U), (Set.Iic x).Finite
```

Some element has a zero for its successor.

nonPeano : ∃ x y, Structure.Arithmetic.Z y ∧ Structure.Arithmetic.S x y

Show details

Outer dependencies: (none)

Inner dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.S, Structure.Arithmetic.Z

Lean core dependencies: And, Eq, Exists, HEq, eq_of_heq

Used by: Structure.Arithmetic.Tower.instPeanoColimit, Structure.Arithmetic.instNonPeanoFin, Structure.Arithmetic.ultrafinitism

Structure.Arithmetic.ultrafinitism

Ultrafinitism: negating Peano’s postulate is exactly finiteness. A zero that is a successor is a successor by wrap-around, so the element it succeeds is a maximum, and everything up to a maximum is everything and finite in number. Conversely a finite universe has a greatest element, whose successor wraps around to the zero.

ultrafinitism

theorem Structure.Arithmetic.ultrafinitism.{u_2} {U : Type u_2} [inst : Structure.Arithmetic.Arith U] :
  Nonempty (Structure.Arithmetic.NonPeano U) ↔ Finite U

Show details

fun {U} [inst : Structure.Arithmetic.Arith U] =>
  {
    mp := fun a =>
      Nonempty.casesOn a fun h =>
        Exists.casesOn Structure.Arithmetic.NonPeano.nonPeano fun x h_1 =>
          Exists.casesOn h_1 fun y h_2 =>
            And.casesOn h_2 fun hy right =>
              Or.casesOn right
                (fun h_3 => And.casesOn h_3 fun hlt right => absurd (hy x) (not_le.mpr hlt))
                fun h_3 =>
                And.casesOn h_3 fun hx right =>
                  Set.finite_univ_iff.mp
                    ((Set.eq_univ_of_forall fun y => hx y) ▸ Structure.Arithmetic.Arith.reach x),
    mpr := fun a =>
      Exists.casesOn (Finite.exists_max id) fun m hm =>
        Nonempty.intro
          { toArith := inst,
            nonPeano :=
              Exists.intro m
                (Exists.intro ⊥ ⟨fun x => bot_le, Or.inr ⟨fun y => hm y, fun x => bot_le⟩⟩) } }

Complexity: 2250 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.NonPeano

Proof dependencies: Structure.Arithmetic.M, Structure.Arithmetic.S, Structure.Arithmetic.Z

Mathlib dependencies: Finite, Finite.exists_max, Set, Set.Finite, Set.eq_univ_of_forall, Set.finite_univ_iff, Set.univ, bot_le, not_le

Lean core dependencies: And, Eq, Exists, Iff, Nonempty, Not, absurd, id

Used by: Structure.Arithmetic.Tower.instPeanoColimit, Structure.Arithmetic.instNonPeanoFin

Structure.Arithmetic.instNeZeroNat_structure

instance Structure.Arithmetic.instNeZeroNat_structure {n : ℕ} [n.AtLeastTwo] : NeZero n

Show details

fun {n} [n.AtLeastTwo] =>
  {
    out :=
      have this := Nat.AtLeastTwo.prop;
      fun a => Structure.Arithmetic.instNeZeroNat_structure._proof_1 this a }

Complexity: 70 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: Nat.AtLeastTwo

Used by: Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.Z_iff_zero_fin, Structure.Arithmetic.instArithFin

Structure.Arithmetic.instArithFin

A universe of \(n\) elements is a model: all of its collections are finite in number, and \(0\) differs from \(1\) as soon as it holds at least two elements.

instance Structure.Arithmetic.instArithFin {n : ℕ} [n.AtLeastTwo] : Structure.Arithmetic.Arith (Fin n)

Show details

| Structure.Arithmetic.instArithFin =
  { toLinearOrder := Fin.instLinearOrder, toOrderBot := Fin.instHeytingAlgebra.toOrderBot,
    toNontrivial := ⋯, reach := ⋯ }

Complexity: 41 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.instNeZeroNat_structure

Mathlib dependencies: Nat.AtLeastTwo, Set, Set.Iic, Set.toFinite

Lean core dependencies: Eq, Eq.trans, Exists, False, Fin, Fin.ext_iff, Nat, Nat.mod_eq_of_lt, Ne, Not, True, congrArg, not_false_eq_true, of_eq_true

Used by: Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.Z_iff_zero_fin, Structure.Arithmetic.finTower, Structure.Arithmetic.instNonPeanoFin

Structure.Arithmetic.instNonPeanoFin

Every finite model negates Peano’s postulate, by ultrafinitism.

instance Structure.Arithmetic.instNonPeanoFin {n : ℕ} [n.AtLeastTwo] : Structure.Arithmetic.NonPeano (Fin n)

Show details

| Structure.Arithmetic.instNonPeanoFin = ⋯.some

Complexity: 19 (size of the value term)

Outer dependencies: Structure.Arithmetic.NonPeano

Inner dependencies: Structure.Arithmetic.instArithFin, Structure.Arithmetic.ultrafinitism

Mathlib dependencies: Finite, Nat.AtLeastTwo, Nonempty.some

Lean core dependencies: Fin, Nat, Nonempty, inferInstance

Used by: (none)

Structure.Arithmetic.Z_iff_zero_fin

In a universe of \(n\) elements, the zero is \(0\).

theorem Structure.Arithmetic.Z_iff_zero_fin {n : ℕ} [n.AtLeastTwo] (x : Fin n) :
  Structure.Arithmetic.Z x ↔ x = 0

Show details

fun {n} [n.AtLeastTwo] x =>
  { mp := fun h => le_antisymm (h 0) (Fin.zero_le x), mpr := fun h y => Eq.symm h ▸ Fin.zero_le y }

Complexity: 325 (size of the value term)

Dependencies: Structure.Arithmetic.Z, Structure.Arithmetic.instArithFin, Structure.Arithmetic.instNeZeroNat_structure

Mathlib dependencies: Nat.AtLeastTwo, le_antisymm

Lean core dependencies: Eq, Eq.symm, Fin, Fin.zero_le, Iff, Nat

Used by: (none)

Structure.Arithmetic.S_iff_add_one

In a universe of \(n\) elements, the successor of \(a\) is \(a + 1\) modulo \(n\), wrap-around included.

theorem Structure.Arithmetic.S_iff_add_one {n : ℕ} [n.AtLeastTwo] (a v : Fin n) :
  Structure.Arithmetic.S a v ↔ v = a + 1

Show details

fun {n} [n.AtLeastTwo] a v =>
  have hn := Nat.AtLeastTwo.prop;
  have hlast := fun b =>
    have hb := b.isLt;
    Eq.mpr (id (congrArg (fun _a => _a = if ↑b = n - 1 then 0 else ↑b + 1) (Fin.val_add b 1)))
      (Eq.mpr
        (id
          (congrArg (fun _a => (↑b + _a) % n = if ↑b = n - 1 then 0 else ↑b + 1) (Fin.val_one' n)))
        (Eq.mpr
          (id
            (congrArg (fun _a => (↑b + _a) % n = if ↑b = n - 1 then 0 else ↑b + 1)
              (Nat.mod_eq_of_lt hn)))
          (Decidable.casesOn (instDecidableEqNat (↑b) (n - 1))
            (fun h =>
              Eq.mpr (id (congrArg (Eq ((↑b + 1) % n)) (if_neg h)))
                (Nat.mod_eq_of_lt
                  (Decidable.byContradiction fun a =>
                    Structure.Arithmetic.S_iff_add_one._proof_1_2 hn b hb h a)))
            fun h =>
            Eq.mpr (id (congrArg (Eq ((↑b + 1) % n)) (if_pos h)))
              (Eq.mpr
                (id
                  (congrArg (fun _a => _a % n = 0)
                    (have this :=
                      Decidable.byContradiction fun a =>
                        Structure.Arithmetic.S_iff_add_one._proof_1_1 hn b hb h a;
                    this)))
                (Eq.mpr (id (congrArg (fun _a => _a = 0) (Nat.mod_self n))) (Eq.refl 0))))));
  have ha := a.isLt;
  have hv := v.isLt;
  Eq.mpr
    (id
      (congr
        (congrArg Iff
          (congr
            (congrArg Or
              (congr (congrArg And Structure.Arithmetic.S_iff_add_one._simp_1_6)
                (forall_congr fun z =>
                  implies_congr Structure.Arithmetic.S_iff_add_one._simp_1_6
                    Structure.Arithmetic.S_iff_add_one._simp_1_7)))
            (congr
              (congrArg And (forall_congr fun y => Structure.Arithmetic.S_iff_add_one._simp_1_7))
              (forall_congr fun y => Structure.Arithmetic.S_iff_add_one._simp_1_7))))
        (Eq.trans Structure.Arithmetic.instArithFin._simp_1
          (congrArg (Eq ↑v) ((fun b => hlast b) a)))))
    {
      mp := fun a_1 =>
        Or.casesOn a_1
          (fun h =>
            And.casesOn h fun h1 h2 =>
              have h3 :=
                h2
                  ⟨↑a + 1,
                    Decidable.byContradiction fun a_2 =>
                      Structure.Arithmetic.S_iff_add_one._proof_1_8 a v ha hv h1 a_2⟩
                  (of_eq_true
                    (Eq.trans (lt_add_iff_pos_right._simp_1 ↑a)
                      (Eq.trans Order.lt_one_iff._simp_1 (eq_self 0))));
              Decidable.casesOn (instDecidableEqNat (↑a) (n - 1))
                (fun h =>
                  Eq.mpr (id (congrArg (Eq ↑v) (if_neg h)))
                    (Decidable.byContradiction fun a_2 =>
                      Structure.Arithmetic.S_iff_add_one._proof_1_10 a v h1 h3 a_2))
                fun h =>
                Eq.mpr (id (congrArg (Eq ↑v) (if_pos h)))
                  (Decidable.byContradiction fun a_2 =>
                    Structure.Arithmetic.S_iff_add_one._proof_1_9 a v hn hv h1 h3 h a_2))
          fun h =>
          And.casesOn h fun h1 h2 =>
            have h3 :=
              h1
                ⟨n - 1,
                  Decidable.byContradiction fun a_2 =>
                    Structure.Arithmetic.S_iff_add_one._proof_1_11 a v hn a_2⟩;
            have h4 :=
              h2
                ⟨0,
                  Decidable.byContradiction fun a_2 =>
                    Structure.Arithmetic.S_iff_add_one._proof_1_12 a v hn a_2⟩;
            Decidable.casesOn (instDecidableEqNat (↑a) (n - 1))
              (fun h =>
                Eq.mpr (id (congrArg (Eq ↑v) (if_neg h)))
                  (Decidable.byContradiction fun a_2 =>
                    Structure.Arithmetic.S_iff_add_one._proof_1_14 a v hn ha h3 h4 h a_2))
              fun h =>
              Eq.mpr (id (congrArg (Eq ↑v) (if_pos h)))
                (Decidable.byContradiction fun a_2 =>
                  Structure.Arithmetic.S_iff_add_one._proof_1_13 a v h4 a_2),
      mpr := fun h =>
        if hc : ↑a = n - 1 then
          Or.inr
            ⟨fun y =>
              have this := y.isLt;
              Decidable.byContradiction fun a_1 =>
                Structure.Arithmetic.S_iff_add_one._proof_1_15 a v hn hc y this a_1,
              fun y =>
              of_eq_true
                (Eq.trans
                  (congrFun'
                    (congrArg LE.le
                      (congrArg Fin.val
                        (Eq.mp
                          (Eq.trans
                            (congrArg (Eq ↑v)
                              (ite_cond_eq_true 0 (↑a + 1)
                                (Eq.trans (congrFun' (congrArg Eq hc) (n - 1)) (eq_self (n - 1)))))
                            Fin.val_eq_zero_iff._simp_1)
                          h)))
                    ↑y)
                  zero_le._simp_1)⟩
        else
          Or.inl
            ⟨Decidable.byContradiction fun a_1 =>
                Structure.Arithmetic.S_iff_add_one._proof_1_16 a v
                  (Eq.mp (congrArg (Eq ↑v) (ite_cond_eq_false 0 (↑a + 1) (eq_false hc))) h) a_1,
              fun z x =>
              Decidable.byContradiction fun a_1 =>
                Structure.Arithmetic.S_iff_add_one._proof_1_17 a v
                  (Eq.mp (congrArg (Eq ↑v) (ite_cond_eq_false 0 (↑a + 1) (eq_false hc))) h) z x
                  a_1⟩ }

Complexity: 17339 (size of the value term)

Dependencies: Structure.Arithmetic.S, Structure.Arithmetic.instArithFin, Structure.Arithmetic.instNeZeroNat_structure

Proof dependencies: Structure.Arithmetic.M, Structure.Arithmetic.Z

Mathlib dependencies: Fin.val_one', Nat.AtLeastTwo

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency

legend