From cfdaffb6f5f8a19b51053dca18ad104e4899ee62 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Wed, 25 Feb 2015 13:32:50 -0500 Subject: [PATCH] feat/refactor(library/data/nat): do some housecleaning, add facts to div --- library/data/nat/basic.lean | 4 ++-- library/data/nat/div.lean | 45 +++++++++++++++++++++++++++++++++++++ library/data/nat/order.lean | 8 +++---- library/data/nat/sub.lean | 19 ++++++++++++++++ 4 files changed, 70 insertions(+), 6 deletions(-) diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index a4a6a8306..c4766d311 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -133,7 +133,7 @@ nat.induction_on m ... = succ (k + n) : IH ... = succ k + n : add.succ_left) -theorem succ_add_eq_add_succ (n m : ℕ) : succ n + m = n + succ m := +theorem succ_add_eq_succ_add (n m : ℕ) : succ n + m = n + succ m := !add.succ_left ⬝ !add_succ⁻¹ theorem add.assoc (n m k : ℕ) : (n + m) + k = n + (m + k) := @@ -215,7 +215,7 @@ nat.induction_on m ... = n * k + k + succ n : IH ... = n * k + (k + succ n) : add.assoc ... = n * k + (succ n + k) : add.comm - ... = n * k + (n + succ k) : succ_add_eq_add_succ + ... = n * k + (n + succ k) : succ_add_eq_succ_add ... = n * k + n + succ k : add.assoc ... = n * succ k + succ k : mul_succ) diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 50036c3fc..37f451971 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -277,6 +277,51 @@ theorem div_mul_cancel_of_mod_eq_zero {m n : ℕ} (H : m mod n = 0) : m div n * 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 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), +have H3 [visible] : n - k div m = n - k div m - 1 + 1, from (sub_add_cancel H2)⁻¹, +have H4 [visible] : 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), +have H6 [visible] : 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_right H4)] + ... = n - k div m - 1 : + by rewrite [(div_eq_zero_of_lt H6), zero_add] + /- divides -/ theorem dvd_of_mod_eq_zero {m n : ℕ} (H : n mod m = 0) : m | n := diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 9d4b7d9ad..fcae31778 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -269,7 +269,7 @@ theorem lt_elim {n m : ℕ} (H : n < m) : ∃k, succ n + k = m := le.elim (succ_le_of_lt H) theorem lt_add_succ (n m : ℕ) : n < n + succ m := -lt_intro !succ_add_eq_add_succ +lt_intro !succ_add_eq_succ_add theorem eq_zero_of_le_zero {n : ℕ} (H : n ≤ 0) : n = 0 := obtain (k : ℕ) (Hk : n + k = 0), from le.elim H, @@ -355,7 +355,7 @@ discriminate (take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero) (take (l : ℕ) (Hm : m = succ l), exists.intro l Hm) -theorem self_lt_succ (n : ℕ) : n < succ n := +theorem lt_succ_self (n : ℕ) : n < succ n := lt.base n theorem le_of_lt_succ {n m : ℕ} (H : n < succ m) : n ≤ m := @@ -378,7 +378,7 @@ have H1 : ∀ {n m : nat}, m < n → P m, from or.elim (lt_or_eq_of_le (le_of_lt_succ H3)) (assume H4: m < n', IH H4) (assume H4: m = n', H4⁻¹ ▸ H2)), -H1 !self_lt_succ +H1 !lt_succ_self protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0) (Hind : ∀(n : nat), (∀m, m ≤ n → P m) → P (succ n)) : P a := @@ -459,7 +459,7 @@ or.elim (le_or_gt n 1) (assume H5 : n > 1, have H6 : n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt H4), have H7 : 1 ≥ 2, from !mul_one ▸ H ▸ H6, - absurd !self_lt_succ (not_lt_of_le H7)) + absurd !lt_succ_self (not_lt_of_le H7)) theorem eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : m = 1 := eq_one_of_mul_eq_one_right (!mul.comm ▸ H) diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 74cbd9226..459f422cc 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -325,6 +325,25 @@ sub.cases have H2 : n - k = mn + km, from sub_eq_of_add_eq H, H2 ▸ !le.refl)) +theorem sub_lt_self {m n : ℕ} (H1 : m > 0) (H2 : n > 0) : m - n < m := +calc + m - n = succ (pred m) - n : succ_pred_of_pos H1 + ... = succ (pred m) - succ (pred n) : succ_pred_of_pos H2 + ... = pred m - pred n : succ_sub_succ + ... ≤ pred m : sub_le + ... < succ (pred m) : lt_succ_self + ... = m : succ_pred_of_pos H1 + +theorem le_sub_of_add_le {m n k : ℕ} (H : m + k ≤ n) : m ≤ n - k := +calc + m = m + k - k : add_sub_cancel + ... ≤ n - k : sub_le_sub_right H k + +theorem lt_sub_of_add_lt {m n k : ℕ} (H : m + k < n) (H2 : k ≤ n) : m < n - k := +lt_of_succ_le (le_sub_of_add_le (calc + succ m + k = succ (m + k) : succ_add_eq_succ_add + ... ≤ n : succ_le_of_lt H)) + /- distance -/ definition dist [reducible] (n m : ℕ) := (n - m) + (m - n)