feat(library/data/{nat,int}/div.lean,*): improve and extend div in nat and int
This commit is contained in:
Jeremy Avigad
parent
c986ee305b
commit
b76445df39
7 changed files with 318 additions and 233 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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],
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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 _,
|
||||
|
|
|
|||
Loading…
Reference in a new issue