Basic lemmas about natural numbers

The primary purpose of the lemmas in this file is to assist with reasoning about sizes of objects, array indices and such. For a more thorough development of the theory of natural numbers, we recommend using Mathlib.

rec/cases

@[simp]

theorem Nat.recAux_zero {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) : Nat.recAux zero succ 0 = zero

theorem Nat.recAux_succ {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (n : Nat) : Nat.recAux zero succ (n + 1) = succ n (Nat.recAux zero succ n)

@[simp]

theorem Nat.recAuxOn_zero {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) : Nat.recAuxOn 0 zero succ = zero

theorem Nat.recAuxOn_succ {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (n : Nat) : Nat.recAuxOn (n + 1) zero succ = succ n (Nat.recAuxOn n zero succ)

@[simp]

theorem Nat.casesAuxOn_zero {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) : Nat.casesAuxOn 0 zero succ = zero

theorem Nat.casesAuxOn_succ {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) (n : Nat) : Nat.casesAuxOn (n + 1) zero succ = succ n

theorem Nat.strongRec_eq {motive : Nat → Sort u_1} (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) (t : Nat) : Nat.strongRec ind t = ind t fun (m : Nat) (x : m < t) => Nat.strongRec ind m

theorem Nat.strongRecOn_eq {motive : Nat → Sort u_1} (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) (t : Nat) : Nat.strongRecOn t ind = ind t fun (m : Nat) (x : m < t) => Nat.strongRecOn m ind

@[simp]

theorem Nat.recDiagAux_zero_left {motive : Nat → Nat → Sort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (n : Nat) : Nat.recDiagAux zero_left zero_right succ_succ 0 n = zero_left n

@[simp]

theorem Nat.recDiagAux_zero_right {motive : Nat → Nat → Sort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (h : zero_left 0 = zero_right 0 := by first | assumption | trivial) : Nat.recDiagAux zero_left zero_right succ_succ m 0 = zero_right m

theorem Nat.recDiagAux_succ_succ {motive : Nat → Nat → Sort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m n : Nat) : Nat.recDiagAux zero_left zero_right succ_succ (m + 1) (n + 1) = succ_succ m n (Nat.recDiagAux zero_left zero_right succ_succ m n)

@[simp]

theorem Nat.recDiag_zero_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 0 = zero_zero

theorem Nat.recDiag_zero_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (n : Nat) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 (n + 1) = zero_succ n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 n)

theorem Nat.recDiag_succ_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) 0 = succ_zero m (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m 0)

theorem Nat.recDiag_succ_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m n : Nat) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) (n + 1) = succ_succ m n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m n)

@[simp]

theorem Nat.recDiagOn_zero_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) : Nat.recDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero

theorem Nat.recDiagOn_zero_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (n : Nat) : Nat.recDiagOn 0 (n + 1) zero_zero zero_succ succ_zero succ_succ = zero_succ n (Nat.recDiagOn 0 n zero_zero zero_succ succ_zero succ_succ)

theorem Nat.recDiagOn_succ_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) : Nat.recDiagOn (m + 1) 0 zero_zero zero_succ succ_zero succ_succ = succ_zero m (Nat.recDiagOn m 0 zero_zero zero_succ succ_zero succ_succ)

theorem Nat.recDiagOn_succ_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m n : Nat) : Nat.recDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n (Nat.recDiagOn m n zero_zero zero_succ succ_zero succ_succ)

@[simp]

theorem Nat.casesDiagOn_zero_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) : Nat.casesDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero

@[simp]

theorem Nat.casesDiagOn_zero_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) (n : Nat) : Nat.casesDiagOn 0 (n + 1) zero_zero zero_succ succ_zero succ_succ = zero_succ n

@[simp]

theorem Nat.casesDiagOn_succ_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) (m : Nat) : Nat.casesDiagOn (m + 1) 0 zero_zero zero_succ succ_zero succ_succ = succ_zero m

@[simp]

theorem Nat.casesDiagOn_succ_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) (m n : Nat) : Nat.casesDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n

strong case

def Nat.lt_sum_ge (a b : Nat) : a < b ⊕' b ≤ a

Strong case analysis on a < b ∨ b ≤ a

Equations

• a.lt_sum_ge b = if h : a < b then PSum.inl h else PSum.inr ⋯

def Nat.sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a

Strong case analysis on a < b ∨ a = b ∨ b < a

Equations

• a.sum_trichotomy b = match h : compare a b with | Ordering.lt => PSum.inl ⋯ | Ordering.eq => PSum.inr (PSum.inl ⋯) | Ordering.gt => PSum.inr (PSum.inr ⋯)

div/mod

sum

@[simp]

theorem Nat.sum_append {l₁ l₂ : List Nat} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum

ofBits

@[simp]

theorem Nat.ofBits_zero (f : Fin 0 → Bool) : ofBits f = 0

theorem Nat.ofBits_succ {n : Nat} (f : Fin (n + 1) → Bool) : ofBits f = 2 * ofBits (f ∘ Fin.succ) + (f 0).toNat

theorem Nat.ofBits_lt_two_pow {n : Nat} (f : Fin n → Bool) : ofBits f < 2 ^ n

@[simp]

theorem Nat.testBit_ofBits_lt {n : Nat} (f : Fin n → Bool) (i : Nat) (h : i < n) : (ofBits f).testBit i = f ⟨i, h⟩

@[simp]

theorem Nat.testBit_ofBits_ge {n : Nat} (f : Fin n → Bool) (i : Nat) (h : n ≤ i) : (ofBits f).testBit i = false

theorem Nat.testBit_ofBits {n i : Nat} (f : Fin n → Bool) : (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else false