From ec05e83a2a4868b98a9343e64b3c0261af7a4332 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 12 Mar 2015 23:43:19 -0400 Subject: [PATCH] feat(library/data/int/div.lean): add theorems about div --- library/data/int/basic.lean | 3 + library/data/int/div.lean | 224 ++++++++++++++++++++++++++++++++---- library/data/int/order.lean | 19 +++ library/data/nat/div.lean | 40 ++++--- 4 files changed, 248 insertions(+), 38 deletions(-) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 2ef85ad1c7..93cf9ee4ee 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -789,4 +789,7 @@ have H1 : m = (#nat m - n + n), from (nat.sub_add_cancel H)⁻¹, have H2 : m = (#nat m - n) + n, from congr_arg of_nat H1, sub_eq_of_eq_add H2 +theorem neg_succ_of_nat_eq' (m : ℕ) : -[m +1] = -m - 1 := +by rewrite [neg_succ_of_nat_eq, -of_nat_add_of_nat, neg_add] + end int diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 35f39971ad..3b81cd61b0 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -1,12 +1,13 @@ /- -Copyright (c) 2014 Floris van Doorn. All rights reserved. +Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Module: data.int.div Author: Jeremy Avigad -Definitions and properties of div, mod, gcd, lcm, coprime. Following the SSReflect library -(and the SMT lib standard), we define a mod b so that 0 ≤ a mod b < |b| when b ≠ 0. +Definitions and properties of div, mod, gcd, lcm, coprime, 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. -/ import data.int.order data.nat.div @@ -34,6 +35,8 @@ 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 + /- div -/ theorem of_nat_div_of_nat (m n : nat) : m div n = of_nat (#nat m div n) := @@ -49,12 +52,33 @@ calc ... = -(m div b + 1) : by rewrite [↑divide, sign_of_pos H, one_mul] theorem div_neg (a b : ℤ) : a div -b = -(a div b) := +by rewrite [↑divide, sign_neg, neg_mul_eq_neg_mul, nat_abs_neg] + +theorem div_of_neg_of_pos {a b : ℤ} (Ha : a < 0) (Hb : b > 0) : a div b = -((-a - 1) div b + 1) := +obtain m (H1 : a = -[m +1]), from exists_eq_neg_succ_of_nat Ha, calc - a div -b = sign (-b) * _ : rfl - ... = -(sign b) * _ : sign_neg - ... = -(sign b * _) : neg_mul_eq_neg_mul - ... = -(sign b * _) : nat_abs_neg - ... = -(a div b) : rfl + a div b = -(m div b + 1) : by rewrite [H1, neg_succ_of_nat_div _ Hb] + ... = -((-a -1) div b + 1) : by rewrite [H1, neg_succ_of_nat_eq', neg_sub, sub_neg_eq_add, + add.comm 1, add_sub_cancel] + +theorem div_nonneg {a b : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) : a div b ≥ 0 := +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] + ... ≥ 0 : trivial + +theorem div_nonpos {a b : ℤ} (Ha : a ≥ 0) (Hb : b ≤ 0) : a div b ≤ 0 := +calc + a div b = -(a div -b) : by rewrite [div_neg, neg_neg] + ... ≤ 0 : neg_nonpos_of_nonneg (div_nonneg Ha (neg_nonneg_of_nonpos Hb)) + +theorem div_neg' {a b : ℤ} (Ha : a < 0) (Hb : b > 0) : a div b < 0 := +have H1 : -a - 1 ≥ 0, from le_sub_one_of_lt (neg_pos_of_neg Ha), +have H2 : (-a - 1) div b + 1 > 0, from lt_add_one_of_le (div_nonneg H1 (le_of_lt Hb)), +calc + a div b = -((-a - 1) div b + 1) : div_of_neg_of_pos Ha Hb + ... < 0 : neg_neg_of_pos H2 theorem zero_div (b : ℤ) : 0 div b = 0 := calc @@ -65,9 +89,45 @@ calc theorem div_zero (a : ℤ) : a div 0 = 0 := by rewrite [↑divide, sign_zero, zero_mul] +theorem div_one (a : ℤ) :a div 1 = a := +assert H : 1 > 0, from dec_trivial, +int.cases_on a + (take m, by rewrite [of_nat_div_of_nat, nat.div_one]) + (take m, by rewrite [!neg_succ_of_nat_div H, of_nat_div_of_nat, nat.div_one]) + theorem eq_div_mul_add_mod {a b : ℤ} : a = a div b * b + a mod b := !add.comm ▸ eq_add_of_sub_eq rfl +theorem div_eq_zero_of_lt {a b : ℤ} : 0 ≤ a → a < b → a div b = 0 := +int.cases_on a + (take m, assume H, + int.cases_on b + (take n, + assume H : m < n, + calc + m div n = #nat m div n : of_nat_div_of_nat + ... = 0 : nat.div_eq_zero_of_lt (lt_of_of_nat_lt_of_nat H)) + (take n, + assume H : m < -[ n +1], + have H1 : ¬(m < -[ n +1]), from dec_trivial, + absurd H H1)) + (take m, + assume H : 0 ≤ -[ m +1], + have H1 : ¬ (0 ≤ -[ m +1]), from dec_trivial, + absurd H H1) + +theorem div_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < abs b) : a div b = 0 := +lt.by_cases + (assume H : b < 0, + assert H3 : a < -b, from abs_of_neg H ▸ H2, + calc + a div b = - (a div -b) : by rewrite [div_neg, neg_neg] + ... = 0 : by rewrite [div_eq_zero_of_lt H1 H3, neg_zero]) + (assume H : b = 0, H⁻¹ ▸ !div_zero) + (assume H : b > 0, + 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) := @@ -109,6 +169,11 @@ 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 @@ -128,7 +193,8 @@ have H2 : a mod (abs b) ≥ 0, from int.cases_on a (take m, (of_nat_mod_abs m b)⁻¹ ▸ !of_nat_nonneg) (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)), + 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] @@ -151,17 +217,19 @@ have H2 : a mod (abs b) < abs b, from /- both div and mod -/ -private theorem add_mul_div_self_right_aux1 {a : ℤ} {k : ℕ} (n : ℕ) (H1 : a ≥ 0) (H2 : #nat k > 0) : +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 := obtain m (Hm : a = of_nat m), from exists_eq_of_nat H1, Hm⁻¹ ▸ (calc (m + n * k) div k = (#nat (m + n * k)) div k : rfl ... = (#nat (m + n * k) div k) : of_nat_div_of_nat - ... = (#nat m div k + n) : !nat.add_mul_div_self_right H2 + ... = (#nat m div k + n) : !nat.add_mul_div_self H2 ... = (#nat m div k) + n : rfl ... = m div k + n : of_nat_div_of_nat) -private theorem add_mul_div_self_right_aux2 {a : ℤ} {k : ℕ} (n : ℕ) (H1 : a < 0) (H2 : #nat k > 0) : +private theorem add_mul_div_self_aux2 {a : ℤ} {k : ℕ} (n : ℕ) + (H1 : a < 0) (H2 : #nat k > 0) : (a + n * k) div k = a div k + n := obtain m (Hm : a = -[m +1]), from exists_eq_neg_succ_of_nat H1, or.elim (nat.lt_or_ge m (#nat n * k)) @@ -189,7 +257,7 @@ or.elim (nat.lt_or_ge m (#nat n * k)) neg_succ_of_nat_div m (of_nat_lt_of_nat H2) ... = -((#nat m div k) + 1) + n : of_nat_div_of_nat ... = -((#nat (m - n * k + n * k) div k) + 1) + n : nat.sub_add_cancel nk_le_m - ... = -((#nat (m - n * k) div k + n) + 1) + n : nat.add_mul_div_self_right H2 + ... = -((#nat (m - n * k) div k + n) + 1) + n : nat.add_mul_div_self H2 ... = -((#nat m - n * k) div k + 1) : by rewrite [-of_nat_add_of_nat, *neg_add, add.right_comm, neg_add_cancel_right, of_nat_div_of_nat] @@ -201,7 +269,7 @@ or.elim (nat.lt_or_ge m (#nat n * k)) by rewrite [sub_eq_add_neg, -*add.assoc, *neg_add, neg_neg, add.right_comm] ... = (-[m +1] + n * k) div k : rfl))) -private theorem add_mul_div_self_right_aux3 (a : ℤ) {b c : ℤ} (H1 : b ≥ 0) (H2 : c > 0) : +private theorem add_mul_div_self_aux3 (a : ℤ) {b c : ℤ} (H1 : b ≥ 0) (H2 : c > 0) : (a + b * c) div c = a div c + b := obtain n (Hn : b = of_nat n), from exists_eq_of_nat H1, obtain k (Hk : c = of_nat k), from exists_eq_of_nat (le_of_lt H2), @@ -209,31 +277,143 @@ have knz : k ≠ 0, from assume kz, !lt.irrefl (kz ▸ Hk ▸ H2), have kgt0 : (#nat k > 0), from nat.pos_of_ne_zero knz, have H3 : (a + n * k) div k = a div k + n, from or.elim (lt_or_ge a 0) - (assume Ha : a < 0, add_mul_div_self_right_aux2 _ Ha kgt0) - (assume Ha : a ≥ 0, add_mul_div_self_right_aux1 _ Ha kgt0), + (assume Ha : a < 0, add_mul_div_self_aux2 _ Ha kgt0) + (assume Ha : a ≥ 0, add_mul_div_self_aux1 _ Ha kgt0), Hn⁻¹ ▸ Hk⁻¹ ▸ H3 -private theorem add_mul_div_self_right_aux4 (a b : ℤ) {c : ℤ} (H : c > 0) : +private theorem add_mul_div_self_aux4 (a b : ℤ) {c : ℤ} (H : c > 0) : (a + b * c) div c = a div c + b := or.elim (le.total 0 b) - (assume H1 : 0 ≤ b, add_mul_div_self_right_aux3 _ H1 H) + (assume H1 : 0 ≤ b, add_mul_div_self_aux3 _ H1 H) (assume H1 : 0 ≥ b, eq.symm (calc a div c + b = (a + b * c + -b * c) div c + b : by rewrite [-neg_mul_eq_neg_mul, add_neg_cancel_right] ... = (a + b * c) div c + - b + b : - add_mul_div_self_right_aux3 _ (neg_nonneg_of_nonpos H1) H + add_mul_div_self_aux3 _ (neg_nonneg_of_nonpos H1) H ... = (a + b * c) div c : neg_add_cancel_right)) -theorem add_mul_div_self_right (a b : ℤ) {c : ℤ} (H : c ≠ 0) : (a + b * c) div c = a div c + b := +theorem add_mul_div_self (a b : ℤ) {c : ℤ} (H : c ≠ 0) : (a + b * c) div c = a div c + b := lt.by_cases - (assume H1 : 0 < c, !add_mul_div_self_right_aux4 H1) + (assume H1 : 0 < c, !add_mul_div_self_aux4 H1) (assume H1 : 0 = c, absurd H1⁻¹ H) (assume H1 : 0 > c, have H2 : -c > 0, from neg_pos_of_neg H1, calc (a + b * c) div c = - ((a + -b * -c) div -c) : by rewrite [div_neg, neg_mul_neg, neg_neg] - ... = -(a div -c + -b) : !add_mul_div_self_right_aux4 H2 + ... = -(a div -c + -b) : !add_mul_div_self_aux4 H2 ... = a div c + b : by rewrite [div_neg, neg_add, *neg_neg]) +theorem add_mul_div_self_left (a : ℤ) {b : ℤ} (c : ℤ) (H : b ≠ 0) : + (a + b * c) div b = a div b + c := +!mul.comm ▸ !add_mul_div_self H + +theorem mul_div_cancel (a : ℤ) {b : ℤ} (H : b ≠ 0) : a * b div b = a := +calc + a * b div b = (0 + a * b) div b : zero_add + ... = 0 div b + a : !add_mul_div_self H + ... = a : by rewrite [zero_div, zero_add] + +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 + +theorem mod_self {a : ℤ} : a mod a = 0 := +decidable.by_cases + (assume H : a = 0, H⁻¹ ▸ !mod_zero) + (assume H : a ≠ 0, + calc + a mod a = a - a div a * a : rfl + ... = 0 : by rewrite [!div_self H, one_mul, sub_self]) + +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)) + +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)), +have H4 : a * (b mod c) < a * c, from mul_lt_mul_of_pos_left (!mod_lt_of_pos H2) H1, +have H5 : a * (b mod c) ≥ 0, from mul_nonneg (le_of_lt H1) (!mod_nonneg (ne.symm (ne_of_lt H2))), +calc + a * b div (a * c) = a * (b div c * c + b mod c) div (a * c) : eq_div_mul_add_mod + + ... = (a * (b mod c) + a * c * (b div c)) div (a * c) : + by rewrite [!add.comm, mul.left_distrib, mul.comm _ c, -!mul.assoc] + ... = a * (b mod c) div (a * c) + b div c : !add_mul_div_self_left H3 + ... = 0 + b div c : {!div_eq_zero_of_lt H5 H4} + ... = b div c : zero_add + +theorem mul_div_mul_of_pos {a : ℤ} (b c : ℤ) (H : a > 0) : a * b div (a * c) = b div c := +lt.by_cases + (assume H1 : c < 0, + have H2 : -c > 0, from neg_pos_of_neg H1, + calc + a * b div (a * c) = - (a * b div (a * -c)) : + by rewrite [!neg_mul_eq_mul_neg⁻¹, div_neg, neg_neg] + ... = - (b div -c) : mul_div_mul_of_pos_aux _ H H2 + ... = b div c : by rewrite [div_neg, neg_neg]) + (assume H1 : c = 0, + calc + a * b div (a * c) = 0 : by rewrite [H1, mul_zero, div_zero] + ... = b div c : by rewrite [H1, div_zero]) + (assume H1 : c > 0, + mul_div_mul_of_pos_aux _ H H1) + +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 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, +calc + a < a div b * b + b : iff.mp' !lt_add_iff_sub_lt_left H + ... = (a div b + 1) * b : by rewrite [mul.right_distrib, one_mul] + +theorem div_le_of_nonneg_of_nonneg {a b : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) : a div b ≤ a := +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 !nat.div_le + ... = a : Hm + +theorem abs_div_le_abs (a b : ℤ) : abs (a div b) ≤ abs a := +have H : ∀a b, b > 0 → abs (a div b) ≤ abs a, from + take a b, + assume H1 : b > 0, + or.elim (le_or_gt 0 a) + (assume H2 : 0 ≤ a, + have H3 : 0 ≤ b, from le_of_lt H1, + calc + abs (a div b) = a div b : abs_of_nonneg (div_nonneg H2 H3) + ... ≤ a : div_le_of_nonneg_of_nonneg H2 H3 + ... = abs a : abs_of_nonneg H2) + (assume H2 : a < 0, + have H3 : -a - 1 ≥ 0, from le_sub_one_of_lt (neg_pos_of_neg H2), + have H4 : (-a - 1) div b + 1 ≥ 0, from add_nonneg (div_nonneg H3 (le_of_lt H1)) trivial, + have H5 : (-a - 1) div b ≤ -a - 1, from div_le_of_nonneg_of_nonneg H3 (le_of_lt H1), + calc + abs (a div b) = abs ((-a - 1) div b + 1) : by rewrite [div_of_neg_of_pos H2 H1, abs_neg] + ... = (-a - 1) div b + 1 : abs_of_nonneg H4 + ... ≤ -a - 1 + 1 : add_le_add_right H5 _ + ... = abs a : by rewrite [sub_add_cancel, abs_of_neg H2]), +lt.by_cases + (assume H1 : b < 0, + calc + abs (a div b) = abs (a div -b) : by rewrite [div_neg, abs_neg] + ... ≤ abs a : H _ _ (neg_pos_of_neg H1)) + (assume H1 : b = 0, + calc + abs (a div b) = 0 : by rewrite [H1, div_zero, abs_zero] + ... ≤ abs a : abs_nonneg) + (assume H1 : b > 0, H _ _ H1) + +/- ltz_divLR -/ + end int diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 9514f68a2f..d3cb9a3979 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -595,6 +595,25 @@ obtain n (H1 : a + succ n = b), from lt.elim H, have H2 : a + 1 + n = b, by rewrite [-H1, add.assoc, add.comm 1], le.intro H2 +theorem lt_add_one_of_le {a b : ℤ} (H : a ≤ b) : a < b + 1 := +lt_add_of_le_of_pos H trivial + +theorem le_of_lt_add_one {a b : ℤ} (H : a < b + 1) : a ≤ b := +have H1 : a + 1 ≤ b + 1, from add_one_le_of_lt H, +le_of_add_le_add_right H1 + +theorem sub_one_le_of_lt {a b : ℤ} (H : a ≤ b) : a - 1 < b := +lt_of_add_one_le (!sub_add_cancel⁻¹ ▸ H) + +theorem lt_of_sub_one_le {a b : ℤ} (H : a - 1 < b) : a ≤ b := +!sub_add_cancel ▸ add_one_le_of_lt H + +theorem le_sub_one_of_lt {a b : ℤ} (H : a < b) : a ≤ b - 1 := +le_of_lt_add_one (!sub_add_cancel⁻¹ ▸ H) + +theorem lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) : a < b := +!sub_add_cancel ▸ (lt_add_one_of_le H) + theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 := trivial theorem of_nat_pos {n : ℕ} (Hpos : #nat n > 0) : of_nat n > 0 := diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index d54097ca53..22ef5d1486 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -42,16 +42,16 @@ divide_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l theorem div_eq_succ_sub_div {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a div b = succ ((a - b) div b) := divide_def a b ⬝ if_pos (and.intro h₁ h₂) -theorem add_div_self_right (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) := +theorem add_div_self (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) := calc (x + z) div z = if 0 < z ∧ z ≤ x + z then (x + z - z) div z + 1 else 0 : !divide_def ... = (x + z - z) div z + 1 : if_pos (and.intro H (le_add_left z x)) ... = succ (x div z) : {!add_sub_cancel} theorem add_div_self_left {x : ℕ} (z : ℕ) (H : x > 0) : (x + z) div x = succ (z div x) := -!add.comm ▸ !add_div_self_right H +!add.comm ▸ !add_div_self H -theorem add_mul_div_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y := +theorem add_mul_div_self {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y := nat.induction_on y (calc (x + zero * z) div z = (x + zero) div z : zero_mul ... = x div z : add_zero @@ -59,16 +59,16 @@ nat.induction_on y (take y, assume IH : (x + y * z) div z = x div z + y, calc (x + succ y * z) div z = (x + y * z + z) div z : by simp - ... = succ ((x + y * z) div z) : !add_div_self_right H + ... = succ ((x + y * z) div z) : !add_div_self H ... = x div z + succ y : by simp) theorem add_mul_div_self_left (x z : ℕ) {y : ℕ} (H : y > 0) : (x + y * z) div y = x div y + z := -!mul.comm ▸ add_mul_div_self_right H +!mul.comm ▸ add_mul_div_self H theorem mul_div_cancel (m : ℕ) {n : ℕ} (H : n > 0) : m * n div n = m := calc m * n div n = (0 + m * n) div n : zero_add - ... = 0 div n + m : add_mul_div_self_right H + ... = 0 div n + m : add_mul_div_self H ... = 0 + m : zero_div ... = m : zero_add @@ -97,16 +97,16 @@ modulo_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l theorem mod_eq_sub_mod {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a mod b = (a - b) mod b := modulo_def a b ⬝ if_pos (and.intro h₁ h₂) -theorem add_mod_left {x z : ℕ} (H : z > 0) : (x + z) mod z = x mod z := +theorem add_mod_self {x z : ℕ} (H : z > 0) : (x + z) mod z = x mod z := calc (x + z) mod z = if 0 < z ∧ z ≤ x + z then (x + z - z) mod z else _ : modulo_def ... = (x + z - z) mod z : if_pos (and.intro H (le_add_left z x)) ... = x mod z : add_sub_cancel -theorem add_mod_right {x z : ℕ} (H : x > 0) : (x + z) mod x = z mod x := -!add.comm ▸ add_mod_left H +theorem add_mod_self_left {x z : ℕ} (H : x > 0) : (x + z) mod x = z mod x := +!add.comm ▸ add_mod_self H -theorem add_mul_mod_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z := +theorem add_mul_mod_self {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z := nat.induction_on y (calc (x + zero * z) mod z = (x + zero) mod z : zero_mul ... = x mod z : add_zero) @@ -115,17 +115,17 @@ nat.induction_on y calc (x + succ y * z) mod z = (x + (y * z + z)) mod z : succ_mul ... = (x + y * z + z) mod z : add.assoc - ... = (x + y * z) mod z : add_mod_left H + ... = (x + y * z) mod z : add_mod_self H ... = x mod z : IH) theorem add_mul_mod_self_left {x y z : ℕ} (H : y > 0) : (x + y * z) mod y = x mod y := -!mul.comm ▸ add_mul_mod_self_right H +!mul.comm ▸ add_mul_mod_self H theorem mul_mod_left {m n : ℕ} : (m * n) mod n = 0 := by_cases_zero_pos n (by simp) (take n, assume npos : n > 0, - (by simp) ▸ (@add_mul_mod_self_right 0 m _ npos)) + (by simp) ▸ (@add_mul_mod_self 0 m _ npos)) theorem mul_mod_right {m n : ℕ} : (m * n) mod m = 0 := !mul.comm ▸ !mul_mod_left @@ -192,10 +192,10 @@ theorem eq_remainder {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2 (H3 : q1 * y + r1 = q2 * y + r2) : r1 = r2 := calc r1 = r1 mod y : by simp - ... = (r1 + q1 * y) mod y : (add_mul_mod_self_right H)⁻¹ + ... = (r1 + q1 * y) mod y : (add_mul_mod_self H)⁻¹ ... = (q1 * y + r1) mod y : add.comm ... = (r2 + q2 * y) mod y : by simp - ... = r2 mod y : add_mul_mod_self_right H + ... = r2 mod y : add_mul_mod_self H ... = r2 : by simp theorem eq_quotient {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2 : r2 < y) @@ -298,6 +298,14 @@ or.elim (eq_zero_or_pos k) ... ≤ 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, @@ -318,7 +326,7 @@ calc 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_right H4)] + by rewrite [add.comm, (add_mul_div_self H4)] ... = n - k div m - 1 : by rewrite [div_eq_zero_of_lt H6, zero_add]