diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 0bd34368b..78161b0d9 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -120,7 +120,7 @@ section comm_semiring theorem dvd_mul_of_dvd_right {a b : A} (H : a ∣ b) (c : A) : a ∣ c * b := !mul.comm ▸ (dvd_mul_of_dvd_left H _) - theorem mul_dvd_mul {a b c d : A} (dvd_ab : (a ∣ b)) (dvd_cd : c ∣ d) : a * c ∣ b * d := + theorem mul_dvd_mul {a b c d : A} (dvd_ab : a ∣ b) (dvd_cd : c ∣ d) : a * c ∣ b * d := dvd.elim dvd_ab (take e, assume Haeb : b = a * e, dvd.elim dvd_cd diff --git a/library/data/encodable.lean b/library/data/encodable.lean index 25c4bfd0e..ef91668c4 100644 --- a/library/data/encodable.lean +++ b/library/data/encodable.lean @@ -76,7 +76,7 @@ theorem decode_encode_sum : ∀ s : sum A B, decode_sum (encode_sum s) = some s end | (sum.inr b) := assert aux₁ : 2 > 0, from dec_trivial, - assert aux₂ : 1 mod 2 = 1, by rewrite [modulo_def], + assert aux₂ : 1 mod 2 = 1, by rewrite [nat.modulo_def], assert aux₃ : 1 ≠ 0, from dec_trivial, begin esimp [encode_sum, decode_sum], diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 3d603a310..e0a786107 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -95,6 +95,9 @@ infix * := int.mul theorem of_nat.inj {m n : ℕ} (H : of_nat m = of_nat n) : m = n := by injection H; assumption +theorem of_nat_eq_of_nat (m n : ℕ) : of_nat m = of_nat n ↔ m = n := +iff.intro of_nat.inj !congr_arg + theorem neg_succ_of_nat.inj {m n : ℕ} (H : neg_succ_of_nat m = neg_succ_of_nat n) : m = n := by injection H; assumption diff --git a/library/data/int/div.lean b/library/data/int/div.lean index ed336c209..3ce85fb5e 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Jeremy Avigad -Definitions and properties of div, mod, gcd, lcm, coprime, following the SSReflect library. +Definitions and properties of div and mod, following the SSReflect library. Following SSReflect and the SMTlib standard, we define a mod b so that 0 ≤ a mod b < |b| when b ≠ 0. -/ @@ -13,8 +13,6 @@ open [declarations] nat (succ) open eq.ops notation `ℕ` := nat -set_option pp.beta true - namespace int /- definitions -/ @@ -25,14 +23,11 @@ sign b * | of_nat m := #nat m div (nat_abs b) | -[ m +1] := -[ (#nat m div (nat_abs b)) +1] end) - notation a div b := divide a b definition modulo (a b : ℤ) : ℤ := a - a div b * b - notation a mod b := modulo a b - -notation a = b [mod c] := a mod c = b mod c +notation a `≡` b `[mod`:100 c `]`:0 := a mod c = b mod c /- div -/ @@ -125,95 +120,6 @@ lt.by_cases have H3 : a < b, from abs_of_pos H ▸ H2, div_eq_zero_of_lt H1 H3) -/- mod -/ - -theorem of_nat_mod_of_nat (m n : nat) : m mod n = (#nat m mod n) := -have H : m = (#nat m mod n) + m div n * n, from calc - m = of_nat (#nat m div n * n + m mod n) : nat.eq_div_mul_add_mod - ... = (#nat m div n) * n + (#nat m mod n) : rfl - ... = m div n * n + (#nat m mod n) : of_nat_div_of_nat - ... = (#nat m mod n) + m div n * n : add.comm, -calc - m mod n = m - m div n * n : rfl - ... = (#nat m mod n) : sub_eq_of_eq_add H - -theorem neg_succ_of_nat_mod (m : ℕ) {b : ℤ} (bpos : b > 0) : - -[m +1] mod b = b - 1 - m mod b := -calc - -[m +1] mod b = -(m + 1) - -[m +1] div b * b : rfl - ... = -(m + 1) - -(m div b + 1) * b : neg_succ_of_nat_div _ bpos - ... = -m + -1 + (b + m div b * b) : - by rewrite [neg_add, -neg_mul_eq_neg_mul, sub_neg_eq_add, mul.right_distrib, - one_mul, (add.comm b)] - ... = b + -1 + (-m + m div b * b) : - by rewrite [-*add.assoc, add.comm (-m), add.right_comm (-1), (add.comm b)] - ... = b - 1 - m mod b : - by rewrite [↑modulo, *sub_eq_add_neg, neg_add, neg_neg] - -theorem mod_neg (a b : ℤ) : a mod -b = a mod b := -calc - a mod -b = a - (a div -b) * -b : rfl - ... = a - -(a div b) * -b : div_neg - ... = a - a div b * b : neg_mul_neg - ... = a mod b : rfl - -theorem mod_abs (a b : ℤ) : a mod (abs b) = a mod b := -abs.by_cases rfl !mod_neg - -theorem zero_mod (b : ℤ) : 0 mod b = 0 := -by rewrite [↑modulo, zero_div, zero_mul, sub_zero] - -theorem mod_zero (a : ℤ) : a mod 0 = a := -by rewrite [↑modulo, mul_zero, sub_zero] - -theorem mod_one (a : ℤ) : a mod 1 = 0 := -calc - a mod 1 = a - a div 1 * 1 : rfl - ... = 0 : by rewrite [mul_one, div_one, sub_self] - -private lemma of_nat_mod_abs (m : ℕ) (b : ℤ) : m mod (abs b) = (#nat m mod (nat_abs b)) := -calc - m mod (abs b) = m mod (nat_abs b) : of_nat_nat_abs - ... = (#nat m mod (nat_abs b)) : of_nat_mod_of_nat - -private lemma of_nat_mod_abs_lt (m : ℕ) {b : ℤ} (H : b ≠ 0) : m mod (abs b) < (abs b) := -have H1 : abs b > 0, from abs_pos_of_ne_zero H, -have H2 : (#nat nat_abs b > 0), from lt_of_of_nat_lt_of_nat (!of_nat_nat_abs⁻¹ ▸ H1), -calc - m mod (abs b) = (#nat m mod (nat_abs b)) : of_nat_mod_abs m b - ... < nat_abs b : of_nat_lt_of_nat_of_lt (!nat.mod_lt H2) - ... = abs b : of_nat_nat_abs _ - -theorem mod_nonneg (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b ≥ 0 := -have H1 : abs b > 0, from abs_pos_of_ne_zero H, -have H2 : a mod (abs b) ≥ 0, from - int.cases_on a - (take m, (of_nat_mod_abs m b)⁻¹ ▸ of_nat_nonneg (nat.modulo m (nat_abs b))) - (take m, - have H3 : 1 + m mod (abs b) ≤ (abs b), - from (!add.comm ▸ add_one_le_of_lt (of_nat_mod_abs_lt m H)), - calc - -[ m +1] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1 - ... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc] - ... ≥ 0 : iff.mp' !sub_nonneg_iff_le H3), -!mod_abs ▸ H2 - -theorem mod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b < (abs b) := -have H1 : abs b > 0, from abs_pos_of_ne_zero H, -have H2 : a mod (abs b) < abs b, from - int.cases_on a - (take m, of_nat_mod_abs_lt m H) - (take m, - have H3 : abs b ≠ 0, from assume H', H (eq_zero_of_abs_eq_zero H'), - have H4 : 1 + m mod (abs b) > 0, from add_pos_of_pos_of_nonneg dec_trivial (mod_nonneg _ H3), - calc - -[ m +1] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1 - ... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc] - ... < abs b : sub_lt_self _ H4), -!mod_abs ▸ H2 - -/- both div and mod -/ - private theorem add_mul_div_self_aux1 {a : ℤ} {k : ℕ} (n : ℕ) (H1 : a ≥ 0) (H2 : #nat k > 0) : (a + n * k) div k = a div k + n := @@ -233,7 +139,7 @@ or.elim (nat.lt_or_ge m (#nat n * k)) (assume m_lt_nk : #nat m < n * k, have H3 : #nat (m + 1 ≤ n * k), from nat.succ_le_of_lt m_lt_nk, have H4 : #nat m div k + 1 ≤ n, - from nat.succ_le_of_lt (nat.div_lt_of_lt_mul (!nat.mul.comm ▸ m_lt_nk)), + from nat.succ_le_of_lt (nat.div_lt_of_lt_mul m_lt_nk), Hm⁻¹ ▸ (calc (-[m +1] + n * k) div k = (n * k - (m + 1)) div k : by rewrite [add.comm, neg_succ_of_nat_eq] ... = ((#nat n * k) - (#nat m + 1)) div k : rfl @@ -314,6 +220,105 @@ calc theorem mul_div_cancel_left {a : ℤ} (b : ℤ) (H : a ≠ 0) : a * b div a = b := !mul.comm ▸ mul_div_cancel b H +theorem div_self {a : ℤ} (H : a ≠ 0) : a div a = 1 := +!mul_one ▸ !mul_div_cancel_left H + +/- mod -/ + +theorem of_nat_mod_of_nat (m n : nat) : m mod n = (#nat m mod n) := +have H : m = (#nat m mod n) + m div n * n, from calc + m = of_nat (#nat m div n * n + m mod n) : nat.eq_div_mul_add_mod + ... = (#nat m div n) * n + (#nat m mod n) : rfl + ... = m div n * n + (#nat m mod n) : of_nat_div_of_nat + ... = (#nat m mod n) + m div n * n : add.comm, +calc + m mod n = m - m div n * n : rfl + ... = (#nat m mod n) : sub_eq_of_eq_add H + +theorem neg_succ_of_nat_mod (m : ℕ) {b : ℤ} (bpos : b > 0) : + -[m +1] mod b = b - 1 - m mod b := +calc + -[m +1] mod b = -(m + 1) - -[m +1] div b * b : rfl + ... = -(m + 1) - -(m div b + 1) * b : neg_succ_of_nat_div _ bpos + ... = -m + -1 + (b + m div b * b) : + by rewrite [neg_add, -neg_mul_eq_neg_mul, sub_neg_eq_add, mul.right_distrib, + one_mul, (add.comm b)] + ... = b + -1 + (-m + m div b * b) : + by rewrite [-*add.assoc, add.comm (-m), add.right_comm (-1), (add.comm b)] + ... = b - 1 - m mod b : + by rewrite [↑modulo, *sub_eq_add_neg, neg_add, neg_neg] + +theorem mod_neg (a b : ℤ) : a mod -b = a mod b := +calc + a mod -b = a - (a div -b) * -b : rfl + ... = a - -(a div b) * -b : div_neg + ... = a - a div b * b : neg_mul_neg + ... = a mod b : rfl + +theorem mod_abs (a b : ℤ) : a mod (abs b) = a mod b := +abs.by_cases rfl !mod_neg + +theorem zero_mod (b : ℤ) : 0 mod b = 0 := +by rewrite [↑modulo, zero_div, zero_mul, sub_zero] + +theorem mod_zero (a : ℤ) : a mod 0 = a := +by rewrite [↑modulo, mul_zero, sub_zero] + +theorem mod_one (a : ℤ) : a mod 1 = 0 := +calc + a mod 1 = a - a div 1 * 1 : rfl + ... = 0 : by rewrite [mul_one, div_one, sub_self] + +private lemma of_nat_mod_abs (m : ℕ) (b : ℤ) : m mod (abs b) = (#nat m mod (nat_abs b)) := +calc + m mod (abs b) = m mod (nat_abs b) : of_nat_nat_abs + ... = (#nat m mod (nat_abs b)) : of_nat_mod_of_nat + +private lemma of_nat_mod_abs_lt (m : ℕ) {b : ℤ} (H : b ≠ 0) : m mod (abs b) < (abs b) := +have H1 : abs b > 0, from abs_pos_of_ne_zero H, +have H2 : (#nat nat_abs b > 0), from lt_of_of_nat_lt_of_nat (!of_nat_nat_abs⁻¹ ▸ H1), +calc + m mod (abs b) = (#nat m mod (nat_abs b)) : of_nat_mod_abs m b + ... < nat_abs b : of_nat_lt_of_nat_of_lt (!nat.mod_lt H2) + ... = abs b : of_nat_nat_abs _ + +theorem mod_eq_of_lt {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < b) : a mod b = a := +obtain m (Hm : a = of_nat m), from exists_eq_of_nat H1, +obtain n (Hn : b = of_nat n), from exists_eq_of_nat (le_of_lt (lt_of_le_of_lt H1 H2)), +begin + revert H2, + rewrite [Hm, Hn, of_nat_mod_of_nat, of_nat_lt_of_nat, of_nat_eq_of_nat], + apply nat.mod_eq_of_lt +end + +theorem mod_nonneg (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b ≥ 0 := +have H1 : abs b > 0, from abs_pos_of_ne_zero H, +have H2 : a mod (abs b) ≥ 0, from + int.cases_on a + (take m, (of_nat_mod_abs m b)⁻¹ ▸ of_nat_nonneg (nat.modulo m (nat_abs b))) + (take m, + have H3 : 1 + m mod (abs b) ≤ (abs b), + from (!add.comm ▸ add_one_le_of_lt (of_nat_mod_abs_lt m H)), + calc + -[ m +1] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1 + ... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc] + ... ≥ 0 : iff.mp' !sub_nonneg_iff_le H3), +!mod_abs ▸ H2 + +theorem mod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b < (abs b) := +have H1 : abs b > 0, from abs_pos_of_ne_zero H, +have H2 : a mod (abs b) < abs b, from + int.cases_on a + (take m, of_nat_mod_abs_lt m H) + (take m, + have H3 : abs b ≠ 0, from assume H', H (eq_zero_of_abs_eq_zero H'), + have H4 : 1 + m mod (abs b) > 0, from add_pos_of_pos_of_nonneg dec_trivial (mod_nonneg _ H3), + calc + -[ m +1] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1 + ... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc] + ... < abs b : sub_lt_self _ H4), +!mod_abs ▸ H2 + theorem add_mul_mod_self {a b c : ℤ} : (a + b * c) mod c = a mod c := decidable.by_cases (assume cz : c = 0, by rewrite [cz, mul_zero, add_zero]) @@ -323,15 +328,18 @@ decidable.by_cases theorem add_mul_mod_self_left (a b c : ℤ) : (a + b * c) mod b = a mod b := !mul.comm ▸ !add_mul_mod_self +theorem add_mod_self {a b : ℤ} : (a + b) mod b = a mod b := +by rewrite -(int.mul_one b) at {1}; apply add_mul_mod_self_left + +theorem add_mod_self_left {a b : ℤ} : (a + b) mod a = b mod a := +!add.comm ▸ !add_mod_self + theorem mul_mod_left (a b : ℤ) : (a * b) mod b = 0 := by rewrite [-zero_add (a * b), add_mul_mod_self, zero_mod] theorem mul_mod_right (a b : ℤ) : (a * b) mod a = 0 := !mul.comm ▸ !mul_mod_left -theorem div_self {a : ℤ} (H : a ≠ 0) : a div a = 1 := -!mul_one ▸ !mul_div_cancel_left H - theorem mod_self {a : ℤ} : a mod a = 0 := decidable.by_cases (assume H : a = 0, H⁻¹ ▸ !mod_zero) @@ -343,6 +351,8 @@ decidable.by_cases theorem mod_lt_of_pos (a : ℤ) {b : ℤ} (H : b > 0) : a mod b < b := !abs_of_pos H ▸ !mod_lt (ne.symm (ne_of_lt H)) +/- properties of div and mod -/ + theorem mul_div_mul_of_pos_aux {a : ℤ} (b : ℤ) {c : ℤ} (H1 : a > 0) (H2 : c > 0) : a * b div (a * c) = b div c := have H3 : a * c ≠ 0, from ne.symm (ne_of_lt (mul_pos H1 H2)), @@ -377,10 +387,8 @@ theorem mul_div_mul_of_pos_left (a : ℤ) {b : ℤ} (c : ℤ) (H : b > 0) : a * b div (c * b) = a div c := !mul.comm ▸ !mul.comm ▸ !mul_div_mul_of_pos H -theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a div b * b ≤ a := -calc - a = a div b * b + a mod b : eq_div_mul_add_mod - ... ≥ a div b * b : le_add_of_nonneg_right (!mod_nonneg H) +theorem mul_mod_mul_of_pos {a : ℤ} (b c : ℤ) (H : a > 0) : a * b mod (a * c) = a * (b mod c) := +by rewrite [↑modulo, !mul_div_mul_of_pos H, mul_sub_left_distrib, mul.left_comm] theorem lt_div_add_one_mul_self (a : ℤ) {b : ℤ} (H : b > 0) : a < (a div b + 1) * b := have H : a - a div b * b < b, from !mod_lt_of_pos H, @@ -393,7 +401,7 @@ obtain (m : ℕ) (Hm : a = m), from exists_eq_of_nat Ha, obtain (n : ℕ) (Hn : b = n), from exists_eq_of_nat Hb, calc a div b = #nat m div n : by rewrite [Hm, Hn, of_nat_div_of_nat] - ... ≤ m : of_nat_le_of_nat_of_le !nat.div_le + ... ≤ m : of_nat_le_of_nat_of_le !nat.div_le_self ... = a : Hm theorem abs_div_le_abs (a b : ℤ) : abs (a div b) ≤ abs a := @@ -434,7 +442,7 @@ by rewrite [eq_div_mul_add_mod a b at {2}, H, add_zero] theorem mul_div_cancel_of_mod_eq_zero {a b : ℤ} (H : a mod b = 0) : b * (a div b) = a := !mul.comm ▸ div_mul_cancel_of_mod_eq_zero H -/- divides -/ +/- dvd -/ theorem dvd_of_mod_eq_zero {a b : ℤ} (H : b mod a = 0) : a ∣ b := dvd.intro (!mul.comm ▸ div_mul_cancel_of_mod_eq_zero H) @@ -487,32 +495,82 @@ theorem eq_mul_of_div_eq_left {a b c : ℤ} (H1 : b ∣ a) (H2 : a div b = c) : a = c * b := !mul.comm ▸ !eq_mul_of_div_eq_right H1 H2 -theorem div_eq_of_eq_mul_left {a b c : ℤ} (H1 : b ≠ 0) (H2 : b ∣ a) (H3 : a = c * b) : +theorem div_eq_of_eq_mul_left {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = c * b) : a div b = c := -iff.mp' (!div_eq_iff_eq_mul_left H1 H2) H3 +div_eq_of_eq_mul_right H1 (!mul.comm ▸ H2) -theorem div_le_iff_le_mul_right {a b : ℤ} (c : ℤ) (H : b > 0) (H' : b ∣ a) : +/- div and ordering -/ + +theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a div b * b ≤ a := +calc + a = a div b * b + a mod b : eq_div_mul_add_mod + ... ≥ a div b * b : le_add_of_nonneg_right (!mod_nonneg H) + +theorem div_le_of_le_mul {a b c : ℤ} (H : c > 0) (H' : a ≤ b * c) : a div c ≤ b := +le_of_mul_le_mul_right (calc + a div c * c = a div c * c + 0 : add_zero + ... ≤ a div c * c + a mod c : add_le_add_left (!mod_nonneg (ne_of_gt H)) + ... = a : eq_div_mul_add_mod + ... ≤ b * c : H') H + +theorem div_le_self (a : ℤ) {b : ℤ} (H1 : a ≥ 0) (H2 : b ≥ 0) : a div b ≤ a := +or.elim (lt_or_eq_of_le H2) + (assume H3 : b > 0, + have H4 : b ≥ 1, from add_one_le_of_lt H3, + have H5 : a ≤ a * b, from calc + a = a * 1 : mul_one + ... ≤ a * b : !mul_le_mul_of_nonneg_left H4 H1, + div_le_of_le_mul H3 H5) + (assume H3 : 0 = b, + by rewrite [-H3, div_zero]; apply H1) + +theorem mul_le_of_le_div {a b c : ℤ} (H1 : c > 0) (H2 : a ≤ b div c) : a * c ≤ b := +calc + a * c ≤ b div c * c : !mul_le_mul_of_nonneg_right H2 (le_of_lt H1) + ... ≤ b : !div_mul_le (ne_of_gt H1) + +theorem le_div_of_mul_le {a b c : ℤ} (H1 : c > 0) (H2 : a * c ≤ b) : a ≤ b div c := +have H3 : a * c < (b div c + 1) * c, from + calc + a * c ≤ b : H2 + ... = b div c * c + b mod c : eq_div_mul_add_mod + ... < b div c * c + c : add_lt_add_left (!mod_lt_of_pos H1) + ... = (b div c + 1) * c : by rewrite [mul.right_distrib, one_mul], +le_of_lt_add_one (lt_of_mul_lt_mul_right H3 (le_of_lt H1)) + +theorem le_div_iff_mul_le {a b c : ℤ} (H : c > 0) : a ≤ b div c ↔ a * c ≤ b := +iff.intro (!mul_le_of_le_div H) (!le_div_of_mul_le H) + +theorem div_le_div {a b c : ℤ} (H : c > 0) (H' : a ≤ b) : a div c ≤ b div c := +le_div_of_mul_le H (le.trans (!div_mul_le (ne_of_gt H)) H') + +theorem div_lt_of_lt_mul {a b c : ℤ} (H : c > 0) (H' : a < b * c) : a div c < b := +lt_of_mul_lt_mul_right + (calc + a div c * c = a div c * c + 0 : add_zero + ... ≤ a div c * c + a mod c : add_le_add_left (!mod_nonneg (ne_of_gt H)) + ... = a : eq_div_mul_add_mod + ... < b * c : H') + (le_of_lt H) + +theorem lt_mul_of_div_lt {a b c : ℤ} (H1 : c > 0) (H2 : a div c < b) : a < b * c := +assert H3 : (a div c + 1) * c ≤ b * c, + from !mul_le_mul_of_nonneg_right (add_one_le_of_lt H2) (le_of_lt H1), +have H4 : a div c * c + c ≤ b * c, by rewrite [mul.right_distrib at H3, one_mul at H3]; apply H3, +calc + a = a div c * c + a mod c : eq_div_mul_add_mod + ... < a div c * c + c : add_lt_add_left (!mod_lt_of_pos H1) + ... ≤ b * c : H4 + +theorem div_lt_iff_lt_mul {a b c : ℤ} (H : c > 0) : a div c < b ↔ a < b * c := +iff.intro (!lt_mul_of_div_lt H) (!div_lt_of_lt_mul H) + +theorem div_le_iff_le_mul_of_div {a b : ℤ} (c : ℤ) (H : b > 0) (H' : b ∣ a) : a div b ≤ c ↔ a ≤ c * b := by rewrite [propext (!le_iff_mul_le_mul_right H), !div_mul_cancel H'] -theorem div_le_iff_le_mul_left {a b : ℤ} (c : ℤ) (H : b > 0) (H' : b ∣ a) : - a div b ≤ c ↔ a ≤ b * c := -!mul.comm ▸ !div_le_iff_le_mul_right H H' - -theorem eq_mul_of_div_le_right {a b c : ℤ} (H1 : b > 0) (H2 : b ∣ a) (H3 : a div b ≤ c) : +theorem le_mul_of_div_le_of_div {a b c : ℤ} (H1 : b > 0) (H2 : b ∣ a) (H3 : a div b ≤ c) : a ≤ c * b := -iff.mp (!div_le_iff_le_mul_right H1 H2) H3 - -theorem div_le_of_eq_mul_right {a b c : ℤ} (H1 : b > 0) (H2 : b ∣ a) (H3 : a ≤ c * b) : - a div b ≤ c := -iff.mp' (!div_le_iff_le_mul_right H1 H2) H3 - -theorem eq_mul_of_div_le_left {a b c : ℤ} (H1 : b > 0) (H2 : b ∣ a) (H3 : a div b ≤ c) : - a ≤ b * c := -iff.mp (!div_le_iff_le_mul_left H1 H2) H3 - -theorem div_le_of_eq_mul_left {a b c : ℤ} (H1 : b > 0) (H2 : b ∣ a) (H3 : a ≤ b * c) : - a div b ≤ c := -iff.mp' (!div_le_iff_le_mul_left H1 H2) H3 +iff.mp (!div_le_iff_le_mul_of_div H1 H2) H3 end int diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 7573deb9d..e3a476c55 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -10,7 +10,7 @@ open eq.ops well_founded decidable fake_simplifier prod namespace nat -/- div and mod -/ +/- div -/ -- auxiliary lemma used to justify div private definition div_rec_lemma {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x := @@ -20,12 +20,11 @@ private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero definition divide (x y : nat) := fix div.F x y +notation a div b := divide a b theorem divide_def (x y : nat) : divide x y = if 0 < y ∧ y ≤ x then divide (x - y) y + 1 else 0 := congr_fun (fix_eq div.F x) y -notation a div b := divide a b - theorem div_zero (a : ℕ) : a div 0 = 0 := divide_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0)) @@ -71,12 +70,14 @@ calc theorem mul_div_cancel_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n div m = n := !mul.comm ▸ !mul_div_cancel H +/- mod -/ + private definition mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x definition modulo (x y : nat) := fix mod.F x y - notation a mod b := modulo a b +notation a `≡` b `[mod`:100 c `]`:0 := a mod c = b mod c theorem modulo_def (x y : nat) : modulo x y = if 0 < y ∧ y ≤ x then modulo (x - y) y else x := congr_fun (fix_eq mod.F x) y @@ -143,7 +144,11 @@ nat.case_strong_induction_on x have H5 : succ x - y ≤ x, from le_of_lt_succ H4, show succ x mod y < y, from H3⁻¹ ▸ IH _ H5)) -/- properties of div and mod together -/ +theorem mod_one (n : ℕ) : n mod 1 = 0 := +have H1 : n mod 1 < 1, from !mod_lt !succ_pos, +eq_zero_of_le_zero (le_of_lt_succ H1) + +/- properties of div and mod -/ -- the quotient / remainder theorem theorem eq_div_mul_add_mod (x y : ℕ) : x = x div y * y + x mod y := @@ -187,12 +192,12 @@ theorem mod_le {x y : ℕ} : x mod y ≤ x := theorem eq_remainder {q1 r1 q2 r2 y : ℕ} (H1 : r1 < y) (H2 : r2 < y) (H3 : q1 * y + r1 = q2 * y + r2) : r1 = r2 := calc - r1 = r1 mod y : by simp + r1 = r1 mod y : mod_eq_of_lt H1 ... = (r1 + q1 * y) mod y : !add_mul_mod_self⁻¹ ... = (q1 * y + r1) mod y : add.comm - ... = (r2 + q2 * y) mod y : by simp + ... = (r2 + q2 * y) mod y : by rewrite [H3, add.comm] ... = r2 mod y : !add_mul_mod_self - ... = r2 : by simp + ... = r2 : mod_eq_of_lt H2 theorem eq_quotient {q1 r1 q2 r2 y : ℕ} (H1 : r1 < y) (H2 : r2 < y) (H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 := @@ -245,10 +250,6 @@ or.elim (eq_zero_or_pos z) theorem mul_mod_mul_right (x z y : ℕ) : (x * z) mod (y * z) = (x mod y) * z := mul.comm z x ▸ mul.comm z y ▸ !mul.comm ▸ !mul_mod_mul_left -theorem mod_one (n : ℕ) : n mod 1 = 0 := -have H1 : n mod 1 < 1, from !mod_lt !succ_pos, -eq_zero_of_le_zero (le_of_lt_succ H1) - theorem mod_self (n : ℕ) : n mod n = 0 := nat.cases_on n (by simp) (take n, @@ -279,60 +280,7 @@ by rewrite [eq_div_mul_add_mod m n at {2}, H, add_zero] theorem mul_div_cancel_of_mod_eq_zero {m n : ℕ} (H : m mod n = 0) : n * (m div n) = m := !mul.comm ▸ div_mul_cancel_of_mod_eq_zero H -theorem div_lt_of_lt_mul {m n k : ℕ} (H : m < k * n) : m div k < n := -lt_of_mul_lt_mul_right (calc - m div k * k ≤ m div k * k + m mod k : le_add_right - ... = m : eq_div_mul_add_mod - ... < k * n : H - ... = n * k : nat.mul.comm) - -theorem div_le_of_le_mul {m n k : ℕ} (H : m ≤ k * n) : m div k ≤ n := -or.elim (eq_zero_or_pos k) - (assume H1 : k = 0, - calc - m div k = m div 0 : H1 - ... = 0 : div_zero - ... ≤ n : zero_le) - (assume H1 : k > 0, - le_of_mul_le_mul_right (calc - m div k * k ≤ m div k * k + m mod k : le_add_right - ... = m : eq_div_mul_add_mod - ... ≤ k * n : H - ... = n * k : nat.mul.comm) H1) - -theorem div_le (m n : ℕ) : m div n ≤ m := -nat.cases_on n (!div_zero⁻¹ ▸ !zero_le) - take n, - have H : m ≤ succ n * m, from calc - m = 1 * m : one_mul - ... ≤ succ n * m : mul_le_mul_right (succ_le_succ !zero_le), - div_le_of_le_mul H - -theorem mul_sub_div_of_lt {m n k : ℕ} (H : k < m * n) : - (m * n - (k + 1)) div m = n - k div m - 1 := -have H1 : k div m < n, from div_lt_of_lt_mul H, -have H2 : n - k div m ≥ 1, from - le_sub_of_add_le (calc - 1 + k div m = succ (k div m) : add.comm - ... ≤ n : succ_le_of_lt H1), -assert H3 : n - k div m = n - k div m - 1 + 1, from (sub_add_cancel H2)⁻¹, -assert H4 : m > 0, from pos_of_ne_zero (assume H': m = 0, not_lt_zero _ (!zero_mul ▸ H' ▸ H)), -have H5 : k mod m + 1 ≤ m, from succ_le_of_lt (!mod_lt H4), -assert H6 : m - (k mod m + 1) < m, from sub_lt_self H4 !succ_pos, -calc - (m * n - (k + 1)) div m = (m * n - (k div m * m + k mod m + 1)) div m : eq_div_mul_add_mod - ... = (m * n - k div m * m - (k mod m + 1)) div m : by rewrite [*sub_sub] - ... = ((n - k div m) * m - (k mod m + 1)) div m : - by rewrite [mul.comm m, mul_sub_right_distrib] - ... = ((n - k div m - 1) * m + m - (k mod m + 1)) div m : - by rewrite [H3 at {1}, mul.right_distrib, nat.one_mul] - ... = ((n - k div m - 1) * m + (m - (k mod m + 1))) div m : {add_sub_assoc H5 _} - ... = (m - (k mod m + 1)) div m + (n - k div m - 1) : - by rewrite [add.comm, (add_mul_div_self H4)] - ... = n - k div m - 1 : - by rewrite [div_eq_zero_of_lt H6, zero_add] - -/- divides -/ +/- dvd -/ theorem dvd_of_mod_eq_zero {m n : ℕ} (H : n mod m = 0) : m ∣ n := dvd.intro (!mul.comm ▸ div_mul_cancel_of_mod_eq_zero H) @@ -362,17 +310,17 @@ have aux : m * (c₁ - c₂) = n₂, from calc ... = n₂ : add_sub_cancel_left, dvd.intro aux -theorem dvd_of_dvd_add_right {m n1 n2 : ℕ} (H : m ∣ (n1 + n2)) : m ∣ n2 → m ∣ n1 := +theorem dvd_of_dvd_add_right {m n₁ n₂ : ℕ} (H : m ∣ n₁ + n₂) : m ∣ n₂ → m ∣ n₁ := dvd_of_dvd_add_left (!add.comm ▸ H) -theorem dvd_sub {m n1 n2 : ℕ} (H1 : m ∣ n1) (H2 : m ∣ n2) : m ∣ n1 - n2 := +theorem dvd_sub {m n₁ n₂ : ℕ} (H1 : m ∣ n₁) (H2 : m ∣ n₂) : m ∣ n₁ - n₂ := by_cases - (assume H3 : n1 ≥ n2, - have H4 : n1 = n1 - n2 + n2, from (sub_add_cancel H3)⁻¹, - show m ∣ n1 - n2, from dvd_of_dvd_add_right (H4 ▸ H1) H2) - (assume H3 : ¬ (n1 ≥ n2), - have H4 : n1 - n2 = 0, from sub_eq_zero_of_le (le_of_lt (lt_of_not_ge H3)), - show m ∣ n1 - n2, from H4⁻¹ ▸ dvd_zero _) + (assume H3 : n₁ ≥ n₂, + have H4 : n₁ = n₁ - n₂ + n₂, from (sub_add_cancel H3)⁻¹, + show m ∣ n₁ - n₂, from dvd_of_dvd_add_right (H4 ▸ H1) H2) + (assume H3 : ¬ (n₁ ≥ n₂), + have H4 : n₁ - n₂ = 0, from sub_eq_zero_of_le (le_of_lt (lt_of_not_ge H3)), + show m ∣ n₁ - n₂, from H4⁻¹ ▸ dvd_zero _) theorem dvd.antisymm {m n : ℕ} : m ∣ n → n ∣ m → m = n := by_cases_zero_pos n @@ -454,28 +402,104 @@ theorem div_eq_of_eq_mul_left {m n k : ℕ} (H1 : n > 0) (H2 : m = k * n) : m div n = k := !div_eq_of_eq_mul_right H1 (!mul.comm ▸ H2) -theorem div_le_iff_le_mul_right {m n : ℕ} (k : ℕ) (H : n > 0) (H' : n ∣ m) : +/- div and ordering -/ + +theorem div_mul_le (m n : ℕ) : m div n * n ≤ m := +calc + m = m div n * n + m mod n : eq_div_mul_add_mod + ... ≥ m div n * n : le_add_right + +theorem div_le_of_le_mul {m n k : ℕ} (H : m ≤ n * k) : m div k ≤ n := +or.elim (eq_zero_or_pos k) + (assume H1 : k = 0, + calc + m div k = m div 0 : H1 + ... = 0 : div_zero + ... ≤ n : zero_le) + (assume H1 : k > 0, + le_of_mul_le_mul_right (calc + m div k * k ≤ m div k * k + m mod k : le_add_right + ... = m : eq_div_mul_add_mod + ... ≤ n * k : H) H1) + +theorem div_le_self (m n : ℕ) : m div n ≤ m := +nat.cases_on n (!div_zero⁻¹ ▸ !zero_le) + take n, + have H : m ≤ m * succ n, from calc + m = m * 1 : mul_one + ... ≤ m * succ n : !mul_le_mul_left (succ_le_succ !zero_le), + div_le_of_le_mul H + +theorem mul_le_of_le_div {m n k : ℕ} (H : m ≤ n div k) : m * k ≤ n := +calc + m * k ≤ n div k * k : !mul_le_mul_right H + ... ≤ n : div_mul_le + +theorem le_div_of_mul_le {m n k : ℕ} (H1 : k > 0) (H2 : m * k ≤ n) : m ≤ n div k := +have H3 : m * k < (succ (n div k)) * k, from + calc + m * k ≤ n : H2 + ... = n div k * k + n mod k : eq_div_mul_add_mod + ... < n div k * k + k : add_lt_add_left (!mod_lt H1) + ... = (succ (n div k)) * k : succ_mul, +lt_of_mul_lt_mul_right H3 + +theorem le_div_iff_mul_le {m n k : ℕ} (H : k > 0) : m ≤ n div k ↔ m * k ≤ n := +iff.intro !mul_le_of_le_div (!le_div_of_mul_le H) + +theorem div_le_div {m n : ℕ} (k : ℕ) (H : m ≤ n) : m div k ≤ n div k := +by_cases_zero_pos k + (by rewrite [*div_zero]) + (take k, assume H1 : k > 0, le_div_of_mul_le H1 (le.trans !div_mul_le H)) + +theorem div_lt_of_lt_mul {m n k : ℕ} (H : m < n * k) : m div k < n := +lt_of_mul_lt_mul_right (calc + m div k * k ≤ m div k * k + m mod k : le_add_right + ... = m : eq_div_mul_add_mod + ... < n * k : H) + +theorem lt_mul_of_div_lt {m n k : ℕ} (H1 : k > 0) (H2 : m div k < n) : m < n * k := +assert H3 : succ (m div k) * k ≤ n * k, from !mul_le_mul_right (succ_le_of_lt H2), +have H4 : m div k * k + k ≤ n * k, by rewrite [succ_mul at H3]; apply H3, +calc + m = m div k * k + m mod k : eq_div_mul_add_mod + ... < m div k * k + k : add_lt_add_left (!mod_lt H1) + ... ≤ n * k : H4 + +theorem div_lt_iff_lt_mul {m n k : ℕ} (H : k > 0) : m div k < n ↔ m < n * k := +iff.intro (!lt_mul_of_div_lt H) !div_lt_of_lt_mul + +theorem div_le_iff_le_mul_of_div {m n : ℕ} (k : ℕ) (H : n > 0) (H' : n ∣ m) : m div n ≤ k ↔ m ≤ k * n := by rewrite [propext (!le_iff_mul_le_mul_right H), !div_mul_cancel H'] -theorem div_le_iff_le_mul_left {m n : ℕ} (k : ℕ) (H : n > 0) (H' : n ∣ m) : - m div n ≤ k ↔ m ≤ n * k := -!mul.comm ▸ !div_le_iff_le_mul_right H H' - -theorem eq_mul_of_div_le_right {m n k : ℕ} (H1 : n > 0) (H2 : n ∣ m) (H3 : m div n ≤ k) : +theorem le_mul_of_div_le_of_div {m n k : ℕ} (H1 : n > 0) (H2 : n ∣ m) (H3 : m div n ≤ k) : m ≤ k * n := -iff.mp (!div_le_iff_le_mul_right H1 H2) H3 +iff.mp (!div_le_iff_le_mul_of_div H1 H2) H3 -theorem div_le_of_eq_mul_right {m n k : ℕ} (H1 : n > 0) (H2 : n ∣ m) (H3 : m ≤ k * n) : - m div n ≤ k := -iff.mp' (!div_le_iff_le_mul_right H1 H2) H3 - -theorem eq_mul_of_div_le_left {m n k : ℕ} (H1 : n > 0) (H2 : n ∣ m) (H3 : m div n ≤ k) : - m ≤ n * k := -iff.mp (!div_le_iff_le_mul_left H1 H2) H3 - -theorem div_le_of_eq_mul_left {m n k : ℕ} (H1 : n > 0) (H2 : n ∣ m) (H3 : m ≤ n * k) : - m div n ≤ k := -iff.mp' (!div_le_iff_le_mul_left H1 H2) H3 +-- needed for integer division +theorem mul_sub_div_of_lt {m n k : ℕ} (H : k < m * n) : + (m * n - (k + 1)) div m = n - k div m - 1 := +have H1 : k div m < n, from div_lt_of_lt_mul (!mul.comm ▸ H), +have H2 : n - k div m ≥ 1, from + le_sub_of_add_le (calc + 1 + k div m = succ (k div m) : add.comm + ... ≤ n : succ_le_of_lt H1), +assert H3 : n - k div m = n - k div m - 1 + 1, from (sub_add_cancel H2)⁻¹, +assert H4 : m > 0, from pos_of_ne_zero (assume H': m = 0, not_lt_zero _ (!zero_mul ▸ H' ▸ H)), +have H5 : k mod m + 1 ≤ m, from succ_le_of_lt (!mod_lt H4), +assert H6 : m - (k mod m + 1) < m, from sub_lt_self H4 !succ_pos, +calc + (m * n - (k + 1)) div m = (m * n - (k div m * m + k mod m + 1)) div m : eq_div_mul_add_mod + ... = (m * n - k div m * m - (k mod m + 1)) div m : by rewrite [*sub_sub] + ... = ((n - k div m) * m - (k mod m + 1)) div m : + by rewrite [mul.comm m, mul_sub_right_distrib] + ... = ((n - k div m - 1) * m + m - (k mod m + 1)) div m : + by rewrite [H3 at {1}, mul.right_distrib, nat.one_mul] + ... = ((n - k div m - 1) * m + (m - (k mod m + 1))) div m : {add_sub_assoc H5 _} + ... = (m - (k mod m + 1)) div m + (n - k div m - 1) : + by rewrite [add.comm, (add_mul_div_self H4)] + ... = n - k div m - 1 : + by rewrite [div_eq_zero_of_lt H6, zero_add] end nat diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 0cde8426a..2d4693417 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -105,20 +105,20 @@ theorem lt_add_of_pos_right {n k : ℕ} (H : k > 0) : n < n + k := /- multiplication -/ -theorem mul_le_mul_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m := +theorem mul_le_mul_left {n m : ℕ} (k : ℕ) (H : n ≤ m) : k * n ≤ k * m := obtain (l : ℕ) (Hl : n + l = m), from le.elim H, have H2 : k * n + k * l = k * m, by rewrite [-mul.left_distrib, Hl], le.intro H2 -theorem mul_le_mul_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k := -!mul.comm ▸ !mul.comm ▸ (mul_le_mul_left H k) +theorem mul_le_mul_right {n m : ℕ} (k : ℕ) (H : n ≤ m) : n * k ≤ m * k := +!mul.comm ▸ !mul.comm ▸ !mul_le_mul_left H theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l := -le.trans (mul_le_mul_right H1 m) (mul_le_mul_left H2 k) +le.trans (!mul_le_mul_right H1) (!mul_le_mul_left H2) theorem mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m := have H2 : k * n < k * n + k, from lt_add_of_pos_right Hk, -have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_mul_left (succ_le_of_lt H) k, +have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_mul_left k (succ_le_of_lt H), lt_of_lt_of_le H2 H3 theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k := @@ -170,8 +170,8 @@ section migrate_algebra add_le_add_left := @add_le_add_left, le_of_add_le_add_left := @le_of_add_le_add_left, zero_ne_one := ne.symm (succ_ne_zero zero), - mul_le_mul_of_nonneg_left := (take a b c H1 H2, mul_le_mul_left H1 c), - mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right H1 c), + mul_le_mul_of_nonneg_left := (take a b c H1 H2, mul_le_mul_left c H1), + mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right c H1), mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left, mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right ⦄ @@ -379,14 +379,14 @@ pos_of_ne_zero theorem mul_lt_mul_of_le_of_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) : n * m < k * l := -lt_of_le_of_lt (mul_le_mul_right H1 m) (mul_lt_mul_of_pos_left H2 Hk) +lt_of_le_of_lt (mul_le_mul_right m H1) (mul_lt_mul_of_pos_left H2 Hk) theorem mul_lt_mul_of_lt_of_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) : n * m < k * l := -lt_of_le_of_lt (mul_le_mul_left H2 n) (mul_lt_mul_of_pos_right H1 Hl) +lt_of_le_of_lt (mul_le_mul_left n H2) (mul_lt_mul_of_pos_right H1 Hl) theorem mul_lt_mul_of_le_of_le {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l := -have H3 : n * m ≤ k * m, from mul_le_mul_right (le_of_lt H1) m, +have H3 : n * m ≤ k * m, from mul_le_mul_right m (le_of_lt H1), have H4 : k * m < k * l, from mul_lt_mul_of_pos_left H2 (lt_of_le_of_lt !zero_le H1), lt_of_le_of_lt H3 H4 diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index a805a6adc..73f09d565 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -444,13 +444,13 @@ theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from take k l : ℕ, assume H : k ≥ l, - have H2 : m * k ≥ m * l, from mul_le_mul_left H m, + have H2 : m * k ≥ m * l, from !mul_le_mul_left H, have H3 : n * l + m * k ≥ m * l, from le.trans H2 !le_add_left, calc dist n m * dist k l = dist n m * (k - l) : dist_eq_sub_of_ge H ... = dist (n * (k - l)) (m * (k - l)) : dist_mul_right ... = dist (n * k - n * l) (m * k - m * l) : by simp - ... = dist (n * k) (m * k - m * l + n * l) : dist_sub_eq_dist_add_left (mul_le_mul_left H n) + ... = dist (n * k) (m * k - m * l + n * l) : dist_sub_eq_dist_add_left (!mul_le_mul_left H) ... = dist (n * k) (n * l + (m * k - m * l)) : add.comm ... = dist (n * k) (n * l + m * k - m * l) : add_sub_assoc H2 (n * l) ... = dist (n * k + m * l) (n * l + m * k) : dist_sub_eq_dist_add_right H3 _,