The natural numbers as a linearly ordered commutative semiring

We also have a variety of lemmas which have been deferred from Data.Nat.Basic because it is easier to prove them with this ordered semiring instance available.

TODO

Move most of the theorems to Data.Nat.Defs by modifying their proofs.

instances

instance Nat.orderBot : OrderBot ℕ

Equations

• Nat.orderBot = OrderBot.mk Nat.zero_le

instance Nat.linearOrderedCommSemiring : LinearOrderedCommSemiring ℕ

Equations

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

instance Nat.linearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero ℕ

Equations

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

Extra instances to short-circuit type class resolution and ensure computability

instance Nat.linearOrderedSemiring : LinearOrderedSemiring ℕ

Equations

• Nat.linearOrderedSemiring = inferInstance

instance Nat.strictOrderedSemiring : StrictOrderedSemiring ℕ

Equations

• Nat.strictOrderedSemiring = inferInstance

instance Nat.strictOrderedCommSemiring : StrictOrderedCommSemiring ℕ

Equations

• Nat.strictOrderedCommSemiring = inferInstance

instance Nat.orderedSemiring : OrderedSemiring ℕ

Equations

• Nat.orderedSemiring = StrictOrderedSemiring.toOrderedSemiring'

instance Nat.orderedCommSemiring : OrderedCommSemiring ℕ

Equations

• Nat.orderedCommSemiring = StrictOrderedCommSemiring.toOrderedCommSemiring'

instance Nat.linearOrderedCancelAddCommMonoid : LinearOrderedCancelAddCommMonoid ℕ

Equations

• Nat.linearOrderedCancelAddCommMonoid = inferInstance

instance Nat.canonicallyOrderedCommSemiring : CanonicallyOrderedCommSemiring ℕ

Equations

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

instance Nat.canonicallyLinearOrderedAddCommMonoid : CanonicallyLinearOrderedAddCommMonoid ℕ

Equations

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

Equalities and inequalities involving zero and one

theorem Nat.zero_eq_mul {m : ℕ} {n : ℕ} : 0 = m * n ↔ m = 0 ∨ n = 0

theorem Nat.eq_zero_of_double_le {n : ℕ} (h : 2 * n ≤ n) : n = 0

theorem Nat.eq_zero_of_mul_le {m : ℕ} {n : ℕ} (hb : 2 ≤ n) (h : n * m ≤ m) : m = 0

@[simp]

theorem Nat.min_eq_zero_iff {m : ℕ} {n : ℕ} : min m n = 0 ↔ m = 0 ∨ n = 0

@[simp]

theorem Nat.max_eq_zero_iff {m : ℕ} {n : ℕ} : max m n = 0 ↔ m = 0 ∧ n = 0

theorem Nat.add_eq_max_iff {m : ℕ} {n : ℕ} : m + n = max m n ↔ m = 0 ∨ n = 0

theorem Nat.add_eq_min_iff {m : ℕ} {n : ℕ} : m + n = min m n ↔ m = 0 ∧ n = 0

theorem Nat.one_le_of_lt {m : ℕ} {n : ℕ} (h : n < m) : 1 ≤ m

theorem Nat.eq_one_of_mul_eq_one_right {m : ℕ} {n : ℕ} (H : m * n = 1) : m = 1

theorem Nat.eq_one_of_mul_eq_one_left {m : ℕ} {n : ℕ} (H : m * n = 1) : n = 1

succ

theorem Nat.two_le_iff (n : ℕ) : 2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1

@[simp]

theorem Nat.lt_one_iff {n : ℕ} : n < 1 ↔ n = 0

add

theorem Nat.add_pos_iff_pos_or_pos (m : ℕ) (n : ℕ) : 0 < m + n ↔ 0 < m ∨ 0 < n

theorem Nat.add_eq_one_iff {m : ℕ} {n : ℕ} : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0

theorem Nat.add_eq_two_iff {m : ℕ} {n : ℕ} : m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0

theorem Nat.add_eq_three_iff {m : ℕ} {n : ℕ} : m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0

theorem Nat.le_add_one_iff {m : ℕ} {n : ℕ} : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

theorem Nat.le_and_le_add_one_iff {m : ℕ} {n : ℕ} : n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1

theorem Nat.add_succ_lt_add {m : ℕ} {n : ℕ} {k : ℕ} {l : ℕ} (hab : m < n) (hcd : k < l) : m + k + 1 < n + l

pred

theorem Nat.pred_le_iff {m : ℕ} {n : ℕ} : Nat.pred m ≤ n ↔ m ≤ Nat.succ n

sub

Most lemmas come from the OrderedSub instance on ℕ.

instance Nat.instOrderedSubNatInstLENatInstAddNatInstSubNat : OrderedSub ℕ

Equations

• Nat.instOrderedSubNatInstLENatInstAddNatInstSubNat = (_ : OrderedSub ℕ)

theorem Nat.lt_pred_iff {m : ℕ} {n : ℕ} : n < Nat.pred m ↔ Nat.succ n < m

theorem Nat.lt_of_lt_pred {m : ℕ} {n : ℕ} (h : m < n - 1) : m < n

theorem Nat.le_or_le_of_add_eq_add_pred {m : ℕ} {n : ℕ} {k : ℕ} {l : ℕ} (h : k + l = m + n - 1) : m ≤ k ∨ n ≤ l

theorem Nat.sub_succ' (m : ℕ) (n : ℕ) : m - Nat.succ n = m - n - 1

A version of Nat.sub_succ in the form _ - 1 instead of Nat.pred _.

mul

theorem Nat.succ_mul_pos {n : ℕ} (m : ℕ) (hn : 0 < n) : 0 < Nat.succ m * n

theorem Nat.mul_self_le_mul_self {m : ℕ} {n : ℕ} (h : m ≤ n) : m * m ≤ n * n

theorem Nat.mul_self_lt_mul_self {m : ℕ} {n : ℕ} : m < n → m * m < n * n

theorem Nat.mul_self_le_mul_self_iff {m : ℕ} {n : ℕ} : m ≤ n ↔ m * m ≤ n * n

theorem Nat.mul_self_lt_mul_self_iff {m : ℕ} {n : ℕ} : m < n ↔ m * m < n * n

theorem Nat.le_mul_self (n : ℕ) : n ≤ n * n

theorem Nat.mul_self_inj {m : ℕ} {n : ℕ} : m * m = n * n ↔ m = n

theorem Nat.le_add_pred_of_pos (n : ℕ) {i : ℕ} (hi : i ≠ 0) : n ≤ i + (n - 1)

@[simp]

theorem Nat.lt_mul_self_iff {n : ℕ} : n < n * n ↔ 1 < n

theorem Nat.add_sub_one_le_mul {m : ℕ} {n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : m + n - 1 ≤ m * n

Recursion and induction principles

This section is here due to dependencies -- the lemmas here require some of the lemmas proved above, and some of the results in later sections depend on the definitions in this section.

theorem Nat.diag_induction (P : ℕ → ℕ → Prop) (ha : ∀ (a : ℕ), P (a + 1) (a + 1)) (hb : ∀ (b : ℕ), P 0 (b + 1)) (hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)) (a : ℕ) (b : ℕ) : a < b → P a b

Given a predicate on two naturals P : ℕ → ℕ → Prop, P a b is true for all a < b if P (a + 1) (a + 1) is true for all a, P 0 (b + 1) is true for all b and for all a < b, P (a + 1) b is true and P a (b + 1) is true implies P (a + 1) (b + 1) is true.

theorem Nat.set_induction_bounded {n : ℕ} {k : ℕ} {S : Set ℕ} (hk : k ∈ S) (h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S) (hnk : k ≤ n) : n ∈ S

A subset of ℕ containing k : ℕ and closed under Nat.succ contains every n ≥ k.

theorem Nat.set_induction {S : Set ℕ} (hb : 0 ∈ S) (h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S) (n : ℕ) : n ∈ S

A subset of ℕ containing zero and closed under Nat.succ contains all of ℕ.

div

theorem Nat.div_le_of_le_mul' {m : ℕ} {n : ℕ} {k : ℕ} (h : m ≤ k * n) : m / k ≤ n

theorem Nat.div_le_self' (m : ℕ) (n : ℕ) : m / n ≤ m

theorem Nat.div_lt_of_lt_mul {m : ℕ} {n : ℕ} {k : ℕ} (h : m < n * k) : m / n < k

theorem Nat.eq_zero_of_le_div {m : ℕ} {n : ℕ} (hn : 2 ≤ n) (h : m ≤ m / n) : m = 0

theorem Nat.div_mul_div_le_div (m : ℕ) (n : ℕ) (k : ℕ) : m / k * n / m ≤ n / k

theorem Nat.eq_zero_of_le_half {n : ℕ} (h : n ≤ n / 2) : n = 0

theorem Nat.mul_div_mul_comm_of_dvd_dvd {m : ℕ} {n : ℕ} {k : ℕ} {l : ℕ} (hmk : k ∣ m) (hnl : l ∣ n) : m * n / (k * l) = m / k * (n / l)

theorem Nat.le_half_of_half_lt_sub {a : ℕ} {b : ℕ} (h : a / 2 < a - b) : b ≤ a / 2

theorem Nat.half_le_of_sub_le_half {a : ℕ} {b : ℕ} (h : a - b ≤ a / 2) : a / 2 ≤ b

mod, dvd

theorem Nat.two_mul_odd_div_two {n : ℕ} (hn : n % 2 = 1) : 2 * (n / 2) = n - 1

theorem Nat.div_dvd_of_dvd {m : ℕ} {n : ℕ} (h : n ∣ m) : m / n ∣ m

theorem Nat.div_div_self {m : ℕ} {n : ℕ} (h : n ∣ m) (hm : m ≠ 0) : m / (m / n) = n

theorem Nat.mod_mul_right_div_self (m : ℕ) (n : ℕ) (k : ℕ) : m % (n * k) / n = m / n % k

theorem Nat.mod_mul_left_div_self (m : ℕ) (n : ℕ) (k : ℕ) : m % (k * n) / n = m / n % k

theorem Nat.not_dvd_of_pos_of_lt {m : ℕ} {n : ℕ} (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n

theorem Nat.sub_mod_eq_zero_of_mod_eq {m : ℕ} {n : ℕ} {k : ℕ} (h : m % k = n % k) : (m - n) % k = 0

If m and n are equal mod k, m - n is zero mod k.

@[simp]

theorem Nat.one_mod (n : ℕ) : 1 % (n + 2) = 1

theorem Nat.one_mod_of_ne_one {n : ℕ} : n ≠ 1 → 1 % n = 1

theorem Nat.dvd_sub_mod {n : ℕ} (k : ℕ) : n ∣ k - k % n

theorem Nat.add_mod_eq_ite {m : ℕ} {n : ℕ} {k : ℕ} : (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k

theorem Nat.div_eq_self {m : ℕ} {n : ℕ} : m / n = m ↔ m = 0 ∨ n = 1

theorem Nat.div_eq_sub_mod_div {m : ℕ} {n : ℕ} : m / n = (m - m % n) / n

theorem Nat.not_dvd_of_between_consec_multiples {m : ℕ} {n : ℕ} {k : ℕ} (h1 : n * k < m) (h2 : m < n * (k + 1)) : ¬n ∣ m

m is not divisible by n if it is between n * k and n * (k + 1) for some k.

find

theorem Nat.find_pos {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) : 0 < Nat.find h ↔ ¬p 0

theorem Nat.find_add {n : ℕ} {p : ℕ → Prop} [DecidablePred p] {hₘ : ∃ (m : ℕ), p (m + n)} {hₙ : ∃ (n : ℕ), p n} (hn : n ≤ Nat.find hₙ) : Nat.find hₘ + n = Nat.find hₙ

find_greatest

theorem Nat.findGreatest_eq_iff {m : ℕ} {k : ℕ} {P : ℕ → Prop} [DecidablePred P] : Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n

theorem Nat.findGreatest_eq_zero_iff {k : ℕ} {P : ℕ → Prop} [DecidablePred P] : Nat.findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n

@[simp]

theorem Nat.findGreatest_pos {k : ℕ} {P : ℕ → Prop} [DecidablePred P] : 0 < Nat.findGreatest P k ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n

theorem Nat.findGreatest_spec {m : ℕ} {n : ℕ} {P : ℕ → Prop} [DecidablePred P] (hmb : m ≤ n) (hm : P m) : P (Nat.findGreatest P n)

theorem Nat.findGreatest_le {P : ℕ → Prop} [DecidablePred P] (n : ℕ) : Nat.findGreatest P n ≤ n

theorem Nat.le_findGreatest {m : ℕ} {n : ℕ} {P : ℕ → Prop} [DecidablePred P] (hmb : m ≤ n) (hm : P m) : m ≤ Nat.findGreatest P n

theorem Nat.findGreatest_mono_right (P : ℕ → Prop) [DecidablePred P] : Monotone (Nat.findGreatest P)

theorem Nat.findGreatest_mono_left {P : ℕ → Prop} {Q : ℕ → Prop} [DecidablePred P] [DecidablePred Q] (hPQ : P ≤ Q) : Nat.findGreatest P ≤ Nat.findGreatest Q

theorem Nat.findGreatest_mono {m : ℕ} {n : ℕ} {P : ℕ → Prop} {Q : ℕ → Prop} [DecidablePred P] [DecidablePred Q] (hPQ : P ≤ Q) (hmn : m ≤ n) : Nat.findGreatest P m ≤ Nat.findGreatest Q n

theorem Nat.findGreatest_is_greatest {n : ℕ} {k : ℕ} {P : ℕ → Prop} [DecidablePred P] (hk : Nat.findGreatest P n < k) (hkb : k ≤ n) : ¬P k

theorem Nat.findGreatest_of_ne_zero {m : ℕ} {n : ℕ} {P : ℕ → Prop} [DecidablePred P] (h : Nat.findGreatest P n = m) (h0 : m ≠ 0) : P m

bit0 and bit1

theorem Nat.bit0_le {n : ℕ} {m : ℕ} (h : n ≤ m) : bit0 n ≤ bit0 m

theorem Nat.bit1_le {n : ℕ} {m : ℕ} (h : n ≤ m) : bit1 n ≤ bit1 m

theorem Nat.bit_le (b : Bool) {m : ℕ} {n : ℕ} : m ≤ n → Nat.bit b m ≤ Nat.bit b n

theorem Nat.bit0_le_bit (b : Bool) {m : ℕ} {n : ℕ} : m ≤ n → bit0 m ≤ Nat.bit b n

theorem Nat.bit_le_bit1 (b : Bool) {m : ℕ} {n : ℕ} : m ≤ n → Nat.bit b m ≤ bit1 n

theorem Nat.bit_lt_bit0 (b : Bool) {m : ℕ} {n : ℕ} : m < n → Nat.bit b m < bit0 n

theorem Nat.bit_lt_bit {m : ℕ} {n : ℕ} (a : Bool) (b : Bool) (h : m < n) : Nat.bit a m < Nat.bit b n

@[simp]

theorem Nat.bit0_le_bit1_iff {m : ℕ} {n : ℕ} : bit0 m ≤ bit1 n ↔ m ≤ n

@[simp]

theorem Nat.bit0_lt_bit1_iff {m : ℕ} {n : ℕ} : bit0 m < bit1 n ↔ m ≤ n

@[simp]

theorem Nat.bit1_le_bit0_iff {m : ℕ} {n : ℕ} : bit1 m ≤ bit0 n ↔ m < n

@[simp]

theorem Nat.bit1_lt_bit0_iff {m : ℕ} {n : ℕ} : bit1 m < bit0 n ↔ m < n

decidability of predicates

instance Nat.decidableLoHi (lo : ℕ) (hi : ℕ) (P : ℕ → Prop) [H : DecidablePred P] : Decidable (∀ (x : ℕ), lo ≤ x → x < hi → P x)

Equations

• Nat.decidableLoHi lo hi P = decidable_of_iff (∀ (x : ℕ), x < hi - lo → P (lo + x)) (_ : (∀ (x : ℕ), x < hi - lo → P (lo + x)) ↔ ∀ (x : ℕ), lo ≤ x → x < hi → P x)

instance Nat.decidableLoHiLe (lo : ℕ) (hi : ℕ) (P : ℕ → Prop) [DecidablePred P] : Decidable (∀ (x : ℕ), lo ≤ x → x ≤ hi → P x)

Equations

• Nat.decidableLoHiLe lo hi P = decidable_of_iff (∀ (x : ℕ), lo ≤ x → x < hi + 1 → P x) (_ : (∀ (x : ℕ), lo ≤ x → x < hi + 1 → P x) ↔ ∀ (x : ℕ), lo ≤ x → x ≤ hi → P x)