feat/refactor(library/data/nat): do some housecleaning, add facts to div
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
a607e7dd57
commit
cfdaffb6f5
4 changed files with 70 additions and 6 deletions
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Reference in a new issue