diff --git a/library/data/encodable.lean b/library/data/encodable.lean index 6cfa61072f..6ae21c5d52 100644 --- a/library/data/encodable.lean +++ b/library/data/encodable.lean @@ -6,7 +6,8 @@ Author: Leonardo de Moura Type class for encodable types. Note that every encodable type is countable. -/ -import data.fintype data.list data.list.sort data.sum data.nat.div data.countable data.equiv data.finset +import data.fintype data.list data.list.sort data.sum data.nat.div data.countable data.equiv +import data.finset open option list nat function algebra structure encodable [class] (A : Type) := @@ -22,7 +23,8 @@ have injective encode, from by rewrite [*encodek at this]; injection this; assumption, exists.intro encode this -definition encodable_fintype [instance] {A : Type} [h₁ : fintype A] [h₂ : decidable_eq A] : encodable A := +definition encodable_fintype [instance] {A : Type} [h₁ : fintype A] [h₂ : decidable_eq A] : + encodable A := encodable.mk (λ a, find a (elements_of A)) (λ n, nth (elements_of A) n) @@ -72,7 +74,8 @@ private theorem decode_encode_sum : ∀ s : sum A B, decode_sum (encode_sum s) = assert aux : 2 > (0:nat), from dec_trivial, begin esimp [encode_sum, decode_sum], - rewrite [mul_mod_right, if_pos (eq.refl (0 : nat)), mul_div_cancel_left _ aux, encodable.encodek] + rewrite [mul_mod_right, if_pos (eq.refl (0 : nat)), nat.mul_div_cancel_left _ aux, + encodable.encodek] end | (sum.inr b) := assert aux₁ : 2 > (0:nat), from dec_trivial, @@ -80,8 +83,8 @@ private theorem decode_encode_sum : ∀ s : sum A B, decode_sum (encode_sum s) = assert aux₃ : 1 ≠ (0:nat), from dec_trivial, begin esimp [encode_sum, decode_sum], - rewrite [add.comm, add_mul_mod_self_left, aux₂, if_neg aux₃, add_sub_cancel_left, - mul_div_cancel_left _ aux₁, encodable.encodek] + rewrite [add.comm, add_mul_mod_self_left, aux₂, if_neg aux₃, nat.add_sub_cancel_left, + nat.mul_div_cancel_left _ aux₁, encodable.encodek] end definition encodable_sum [instance] : encodable (sum A B) := diff --git a/library/data/equiv.lean b/library/data/equiv.lean index ef53dede1c..b4c5ff1dce 100644 --- a/library/data/equiv.lean +++ b/library/data/equiv.lean @@ -267,18 +267,20 @@ mk (λ s, match s with inl n := 2*n | inr n := 2*n+1 end) (λ s, begin have two_gt_0 : 2 > zero, from dec_trivial, cases s, - {esimp, rewrite [if_pos (even_two_mul _), mul_div_cancel_left _ two_gt_0]}, - {esimp, rewrite [if_neg (not_even_two_mul_plus_one _), add_sub_cancel, mul_div_cancel_left _ two_gt_0]} + {esimp, rewrite [if_pos (even_two_mul _), nat.mul_div_cancel_left _ two_gt_0]}, + {esimp, rewrite [if_neg (not_even_two_mul_plus_one _), nat.add_sub_cancel, + nat.mul_div_cancel_left _ two_gt_0]} end) (λ n, by_cases - (λ h : even n, begin rewrite [if_pos h], esimp, rewrite [mul_div_cancel' (dvd_of_even h)] end) + (λ h : even n, + by rewrite [if_pos h]; esimp; rewrite [nat.mul_div_cancel' (dvd_of_even h)]) (λ h : ¬ even n, begin rewrite [if_neg h], esimp, cases n, {exact absurd even_zero h}, - {rewrite [-(add_one a), add_sub_cancel, - mul_div_cancel' (dvd_of_even (even_of_odd_succ (odd_of_not_even h)))]} + {rewrite [-(add_one a), nat.add_sub_cancel, + nat.mul_div_cancel' (dvd_of_even (even_of_odd_succ (odd_of_not_even h)))]} end)) definition prod_equiv_of_equiv_nat {A : Type} : A ≃ nat → (A × A) ≃ A := diff --git a/library/data/fin.lean b/library/data/fin.lean index ed361ea662..9a72d7ed99 100644 --- a/library/data/fin.lean +++ b/library/data/fin.lean @@ -257,7 +257,7 @@ by apply eq_of_veq; rewrite [*val_madd, mod_add_mod, add_mod_mod, add.assoc (val lemma madd_left_inv : ∀ i : fin (succ n), madd (minv i) i = fin.zero n | (mk iv ilt) := eq_of_veq (by - rewrite [val_madd, ↑minv, ↑fin.zero, mod_add_mod, sub_add_cancel (le_of_lt ilt), mod_self]) + rewrite [val_madd, ↑minv, ↑fin.zero, mod_add_mod, nat.sub_add_cancel (le_of_lt ilt), mod_self]) open algebra @@ -420,7 +420,7 @@ assert aux₁ : ∀ {v}, v < m → (v + n) < (n + m), from end, inv_fun := λ f : fin (n + m), match f with - | mk v hlt := if h : v < n then sum.inl (mk v h) else sum.inr (mk (v-n) (sub_lt_of_lt_add hlt (le_of_not_gt h))) + | mk v hlt := if h : v < n then sum.inl (mk v h) else sum.inr (mk (v-n) (nat.sub_lt_of_lt_add hlt (le_of_not_gt h))) end, left_inv := begin intro s, cases s with f₁ f₂, @@ -428,15 +428,15 @@ assert aux₁ : ∀ {v}, v < m → (v + n) < (n + m), from { cases f₂ with v hlt, esimp, have ¬ v + n < n, from suppose v + n < n, - assert v < n - n, from lt_sub_of_add_lt this !le.refl, - have v < 0, by rewrite [sub_self at this]; exact this, + assert v < n - n, from nat.lt_sub_of_add_lt this !le.refl, + have v < 0, by rewrite [nat.sub_self at this]; exact this, absurd this !not_lt_zero, - rewrite [dif_neg this], congruence, congruence, rewrite [add_sub_cancel] } + rewrite [dif_neg this], congruence, congruence, rewrite [nat.add_sub_cancel] } end, right_inv := begin intro f, cases f with v hlt, esimp, apply @by_cases (v < n), { intro h₁, rewrite [dif_pos h₁] }, - { intro h₁, rewrite [dif_neg h₁], esimp, congruence, rewrite [sub_add_cancel (le_of_not_gt h₁)] } + { intro h₁, rewrite [dif_neg h₁], esimp, congruence, rewrite [nat.sub_add_cancel (le_of_not_gt h₁)] } end ⦄ @@ -453,7 +453,7 @@ assert aux₁ : ∀ {v₁ v₂}, v₁ < n → v₂ < m → v₁ + v₂ * n < n*m assert aux₂ : ∀ v, v mod n < n, from take v, mod_lt _ `n > 0`, assert aux₃ : ∀ {v}, v < n * m → v div n < m, from - take v, assume h, by rewrite mul.comm at h; exact div_lt_of_lt_mul h, + take v, assume h, by rewrite mul.comm at h; exact nat.div_lt_of_lt_mul h, ⦃ equiv, to_fun := λ p : (fin n × fin m), match p with (mk v₁ hlt₁, mk v₂ hlt₂) := mk (v₁ + v₂ * n) (aux₁ hlt₁ hlt₂) end, inv_fun := λ f : fin (n*m), match f with (mk v hlt) := (mk (v mod n) (aux₂ v), mk (v div n) (aux₃ hlt)) end, diff --git a/library/data/finset/equiv.lean b/library/data/finset/equiv.lean index 8a98dece4f..620d7074c3 100644 --- a/library/data/finset/equiv.lean +++ b/library/data/finset/equiv.lean @@ -49,16 +49,16 @@ private lemma succ_mem_of_nat (n : nat) (s : nat) : succ n ∈ of_nat s ↔ n iff.intro (suppose succ n ∈ of_nat s, assert odd (s div 2^(succ n)), from odd_of_mem_of_nat this, - have odd ((s div 2) div (2 ^ n)), by rewrite [pow_succ' at this, div_div_eq_div_mul, mul.comm]; assumption, + have odd ((s div 2) div (2 ^ n)), by rewrite [pow_succ' at this, nat.div_div_eq_div_mul, mul.comm]; assumption, show n ∈ of_nat (s div 2), from mem_of_nat_of_odd this) (suppose n ∈ of_nat (s div 2), assert odd ((s div 2) div (2 ^ n)), from odd_of_mem_of_nat this, - assert odd (s div 2^(succ n)), by rewrite [pow_succ', mul.comm, -div_div_eq_div_mul]; assumption, + assert odd (s div 2^(succ n)), by rewrite [pow_succ', mul.comm, -nat.div_div_eq_div_mul]; assumption, show succ n ∈ of_nat s, from mem_of_nat_of_odd this) private lemma odd_of_zero_mem (s : nat) : 0 ∈ of_nat s ↔ odd s := begin - unfold of_nat, rewrite [mem_sep_eq, pow_zero, div_one, mem_upto_eq], + unfold of_nat, rewrite [mem_sep_eq, pow_zero, nat.div_one, mem_upto_eq], show 0 < succ s ∧ odd s ↔ odd s, from iff.intro (assume h, and.right h) @@ -127,7 +127,7 @@ begin assert aux : _, from calc succ m ∈ of_nat (2 * w + 1) ↔ m ∈ of_nat ((2*w+1) div 2) : succ_mem_of_nat ... ↔ m ∈ of_nat w : by rewrite [add.comm, add_mul_div_self_left _ _ (dec_trivial : 2 > 0), d₁, zero_add] - ... ↔ m ∈ of_nat (2*w div 2) : by rewrite [mul.comm, mul_div_cancel _ (dec_trivial : 2 > 0)] + ... ↔ m ∈ of_nat (2*w div 2) : by rewrite [mul.comm, nat.mul_div_cancel _ (dec_trivial : 2 > 0)] ... ↔ succ m ∈ of_nat (2*w) : succ_mem_of_nat, iff.intro (λ hl, finset.mem_insert_of_mem _ (iff.mp aux hl)) @@ -256,7 +256,7 @@ begin have d₁ : 1 div 2 = (0:nat), from dec_trivial, show 2 * w div 2 = (1 + 2 * w) div 2, by rewrite [add_mul_div_self_left _ _ (dec_trivial : 2 > 0), mul.comm, - mul_div_cancel _ (dec_trivial : 2 > 0), d₁, zero_add] + nat.mul_div_cancel _ (dec_trivial : 2 > 0), d₁, zero_add] end }, { have a ∉ predimage s, from suppose a ∈ predimage s, absurd (succ_mem_of_mem_predimage this) nains, rewrite [predimage_insert_succ, to_nat_insert nains, pow_succ', add.comm, diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 9c3c2db2d1..ee9651a155 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -145,7 +145,7 @@ show sub_nat_nat m n = nat.cases_on 0 (m -[nat] n) _, from (sub_eq_zero_of_le H) section local attribute sub_nat_nat [reducible] theorem sub_nat_nat_of_lt {m n : ℕ} (H : m < n) : sub_nat_nat m n = -[1+ pred (n - m)] := -have H1 : n - m = succ (pred (n - m)), from eq.symm (succ_pred_of_pos (sub_pos_of_lt H)), +have H1 : n - m = succ (pred (n - m)), from eq.symm (succ_pred_of_pos (nat.sub_pos_of_lt H)), show sub_nat_nat m n = nat.cases_on (succ (nat.pred (n - m))) (m -[nat] n) _, from H1 ▸ rfl end @@ -224,11 +224,11 @@ theorem repr_sub_nat_nat (m n : ℕ) : repr (sub_nat_nat m n) ≡ (m, n) := nat.lt_ge_by_cases (take H : m < n, have H1 : repr (sub_nat_nat m n) = (0, n - m), by - rewrite [sub_nat_nat_of_lt H, -(succ_pred_of_pos (sub_pos_of_lt H))], - H1⁻¹ ▸ (!zero_add ⬝ (sub_add_cancel (le_of_lt H))⁻¹)) + rewrite [sub_nat_nat_of_lt H, -(succ_pred_of_pos (nat.sub_pos_of_lt H))], + H1⁻¹ ▸ (!zero_add ⬝ (nat.sub_add_cancel (le_of_lt H))⁻¹)) (take H : m ≥ n, have H1 : repr (sub_nat_nat m n) = (m - n, 0), from sub_nat_nat_of_ge H ▸ rfl, - H1⁻¹ ▸ ((sub_add_cancel H) ⬝ !zero_add⁻¹)) + H1⁻¹ ▸ ((nat.sub_add_cancel H) ⬝ !zero_add⁻¹)) theorem repr_abstr (p : ℕ × ℕ) : repr (abstr p) ≡ p := !prod.eta ▸ !repr_sub_nat_nat @@ -238,20 +238,20 @@ or.elim (int.equiv_cases Hequiv) (and.rec (assume (Hp : pr1 p ≥ pr2 p) (Hq : pr1 q ≥ pr2 q), have H : pr1 p - pr2 p = pr1 q - pr2 q, from calc pr1 p - pr2 p - = pr1 p + pr2 q - pr2 q - pr2 p : by rewrite add_sub_cancel + = pr1 p + pr2 q - pr2 q - pr2 p : by rewrite nat.add_sub_cancel ... = pr2 p + pr1 q - pr2 q - pr2 p : Hequiv - ... = pr2 p + (pr1 q - pr2 q) - pr2 p : add_sub_assoc Hq + ... = pr2 p + (pr1 q - pr2 q) - pr2 p : nat.add_sub_assoc Hq ... = pr1 q - pr2 q + pr2 p - pr2 p : by rewrite add.comm - ... = pr1 q - pr2 q : by rewrite add_sub_cancel, + ... = pr1 q - pr2 q : by rewrite nat.add_sub_cancel, abstr_of_ge Hp ⬝ (H ▸ rfl) ⬝ (abstr_of_ge Hq)⁻¹)) (and.rec (assume (Hp : pr1 p < pr2 p) (Hq : pr1 q < pr2 q), have H : pr2 p - pr1 p = pr2 q - pr1 q, from calc pr2 p - pr1 p - = pr2 p + pr1 q - pr1 q - pr1 p : by rewrite add_sub_cancel + = pr2 p + pr1 q - pr1 q - pr1 p : by rewrite nat.add_sub_cancel ... = pr1 p + pr2 q - pr1 q - pr1 p : Hequiv - ... = pr1 p + (pr2 q - pr1 q) - pr1 p : add_sub_assoc (le_of_lt Hq) + ... = pr1 p + (pr2 q - pr1 q) - pr1 p : nat.add_sub_assoc (le_of_lt Hq) ... = pr2 q - pr1 q + pr1 p - pr1 p : by rewrite add.comm - ... = pr2 q - pr1 q : by rewrite add_sub_cancel, + ... = pr2 q - pr1 q : by rewrite nat.add_sub_cancel, abstr_of_lt Hp ⬝ (H ▸ rfl) ⬝ (abstr_of_lt Hq)⁻¹)) theorem equiv_iff (p q : ℕ × ℕ) : (p ≡ q) ↔ (abstr p = abstr q) := @@ -275,7 +275,7 @@ theorem nat_abs_abstr : Π (p : ℕ × ℕ), nat_abs (abstr p) = dist (pr1 p) (p (assume H : m < n, calc nat_abs (abstr (m, n)) = nat_abs (-[1+ pred (n - m)]) : int.abstr_of_lt H - ... = n - m : succ_pred_of_pos (sub_pos_of_lt H) + ... = n - m : succ_pred_of_pos (nat.sub_pos_of_lt H) ... = dist m n : dist_eq_sub_of_le (le_of_lt H)) (assume H : m ≥ n, (abstr_of_ge H)⁻¹ ▸ (dist_eq_sub_of_ge H)⁻¹) end diff --git a/library/data/int/div.lean b/library/data/int/div.lean index f510739b09..6246ff9942 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -66,7 +66,7 @@ calc ... = -[1+(m div (nat_abs b))] : by rewrite [sign_of_pos H, one_mul] ... = -(m div b + 1) : by rewrite [of_nat_div_eq, sign_of_pos H, one_mul] -theorem div_neg (a b : ℤ) : a div -b = -(a div b) := +protected theorem div_neg (a b : ℤ) : a div -b = -(a div b) := begin induction a, rewrite [*of_nat_div_eq, sign_neg, neg_mul_eq_neg_mul, nat_abs_neg], @@ -80,32 +80,32 @@ calc ... = -((-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 := +protected 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 = m div n : by rewrite [Hm, Hn] ... ≥ 0 : by rewrite -of_nat_div; apply trivial -theorem div_nonpos {a b : ℤ} (Ha : a ≥ 0) (Hb : b ≤ 0) : a div b ≤ 0 := +protected 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)) + a div b = -(a div -b) : by rewrite [int.div_neg, neg_neg] + ... ≤ 0 : neg_nonpos_of_nonneg (int.div_nonneg Ha (neg_nonneg_of_nonpos Hb)) theorem div_neg' {a b : ℤ} (Ha : a < 0) (Hb : b > 0) : a div b < 0 := have -a - 1 ≥ 0, from le_sub_one_of_lt (neg_pos_of_neg Ha), -have (-a - 1) div b + 1 > 0, from lt_add_one_of_le (div_nonneg this (le_of_lt Hb)), +have (-a - 1) div b + 1 > 0, from lt_add_one_of_le (int.div_nonneg this (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 this -theorem zero_div (b : ℤ) : 0 div b = 0 := +protected theorem zero_div (b : ℤ) : 0 div b = 0 := by rewrite [of_nat_div_eq, nat.zero_div, of_nat_zero, mul_zero] -theorem div_zero (a : ℤ) : a div 0 = 0 := +protected theorem div_zero (a : ℤ) : a div 0 = 0 := by rewrite [divide.def, sign_zero, zero_mul] -theorem div_one (a : ℤ) : a div 1 = a := +protected theorem div_one (a : ℤ) : a div 1 = a := assert (1 : int) > 0, from dec_trivial, int.cases_on a (take m : nat, by rewrite [-of_nat_one, -of_nat_div, nat.div_one]) @@ -136,9 +136,9 @@ lt.by_cases (suppose b < 0, assert a < -b, from abs_of_neg this ▸ H2, calc - a div b = - (a div -b) : by rewrite [div_neg, neg_neg] + a div b = - (a div -b) : by rewrite [int.div_neg, neg_neg] ... = 0 : by rewrite [div_eq_zero_of_lt H1 this, neg_zero]) - (suppose b = 0, this⁻¹ ▸ !div_zero) + (suppose b = 0, this⁻¹ ▸ !int.div_zero) (suppose b > 0, have a < b, from abs_of_pos this ▸ H2, div_eq_zero_of_lt H1 this) @@ -214,32 +214,33 @@ or.elim (le.total 0 b) 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 (a b : ℤ) {c : ℤ} (H : c ≠ 0) : (a + b * c) div c = a div c + b := +protected 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_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 + b * c) div c = - ((a + -b * -c) div -c) : by rewrite [int.div_neg, neg_mul_neg, neg_neg] ... = -(a div -c + -b) : !add_mul_div_self_aux4 H2 - ... = a div c + b : by rewrite [div_neg, neg_add, *neg_neg]) + ... = a div c + b : by rewrite [int.div_neg, neg_add, *neg_neg]) -theorem add_mul_div_self_left (a : ℤ) {b : ℤ} (c : ℤ) (H : b ≠ 0) : +protected 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 +!mul.comm ▸ !int.add_mul_div_self H -theorem mul_div_cancel (a : ℤ) {b : ℤ} (H : b ≠ 0) : a * b div b = a := +protected theorem mul_div_cancel (a : ℤ) {b : ℤ} (H : b ≠ 0) : a * b div b = a := calc - a * b div b = (0 + a * b) div b : algebra.zero_add - ... = 0 div b + a : !add_mul_div_self H - ... = a : by rewrite [zero_div, zero_add] + a * b div b = (0 + a * b) div b : zero_add + ... = 0 div b + a : !int.add_mul_div_self H + ... = a : by rewrite [int.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 +protected theorem mul_div_cancel_left {a : ℤ} (b : ℤ) (H : a ≠ 0) : a * b div a = b := +!mul.comm ▸ int.mul_div_cancel b H -theorem div_self {a : ℤ} (H : a ≠ 0) : a div a = 1 := -!mul_one ▸ !mul_div_cancel_left H +protected theorem div_self {a : ℤ} (H : a ≠ 0) : a div a = 1 := +!mul_one ▸ !int.mul_div_cancel_left H /- mod -/ @@ -269,7 +270,7 @@ calc 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 : int.div_neg ... = a - a div b * b : neg_mul_neg ... = a mod b : rfl @@ -277,7 +278,7 @@ 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.def), zero_div, zero_mul, sub_zero] +by rewrite [(modulo.def), int.zero_div, zero_mul, sub_zero] theorem mod_zero (a : ℤ) : a mod 0 = a := by rewrite [(modulo.def), mul_zero, sub_zero] @@ -285,7 +286,7 @@ by rewrite [(modulo.def), 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] + ... = 0 : by rewrite [mul_one, int.div_one, sub_self] private lemma of_nat_mod_abs (m : ℕ) (b : ℤ) : m mod (abs b) = of_nat (m mod (nat_abs b)) := calc @@ -341,7 +342,7 @@ have H2 : a mod (abs b) < abs b, from 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]) - (assume cnz, by rewrite [(modulo.def), !add_mul_div_self cnz, right_distrib, + (assume cnz, by rewrite [(modulo.def), !int.add_mul_div_self cnz, right_distrib, sub_add_eq_sub_sub_swap, add_sub_cancel]) theorem add_mul_mod_self_left (a b c : ℤ) : (a + b * c) mod b = a mod b := @@ -389,7 +390,7 @@ decidable.by_cases (assume H : a ≠ 0, calc a mod a = a - a div a * a : rfl - ... = 0 : by rewrite [!div_self H, one_mul, sub_self]) + ... = 0 : by rewrite [!int.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)) @@ -406,7 +407,7 @@ calc ... = (a * (b mod c) + a * c * (b div c)) div (a * c) : by rewrite [!add.comm, int.mul_left_distrib, mul.comm _ c, -!mul.assoc] - ... = a * (b mod c) div (a * c) + b div c : !add_mul_div_self_left H3 + ... = a * (b mod c) div (a * c) + b div c : !int.add_mul_div_self_left H3 ... = 0 + b div c : {!div_eq_zero_of_lt H5 H4} ... = b div c : zero_add @@ -416,13 +417,13 @@ lt.by_cases 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] + by rewrite [-neg_mul_eq_mul_neg, int.div_neg, neg_neg] ... = - (b div -c) : mul_div_mul_of_pos_aux _ H H2 - ... = b div c : by rewrite [div_neg, neg_neg]) + ... = b div c : by rewrite [int.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]) + a * b div (a * c) = 0 : by rewrite [H1, mul_zero, int.div_zero] + ... = b div c : by rewrite [H1, int.div_zero]) (assume H1 : c > 0, mul_div_mul_of_pos_aux _ H H1) @@ -456,13 +457,13 @@ have H : ∀a b, b > 0 → abs (a div b) ≤ abs a, from (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) + abs (a div b) = a div b : abs_of_nonneg (int.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)) (of_nat_le_of_nat_of_le !nat.zero_le), + from add_nonneg (int.div_nonneg H3 (le_of_lt H1)) (of_nat_le_of_nat_of_le !nat.zero_le), 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] @@ -472,11 +473,11 @@ have H : ∀a b, b > 0 → abs (a div b) ≤ abs a, from lt.by_cases (assume H1 : b < 0, calc - abs (a div b) = abs (a div -b) : by rewrite [div_neg, abs_neg] + abs (a div b) = abs (a div -b) : by rewrite [int.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 div b) = 0 : by rewrite [H1, int.div_zero, abs_zero] ... ≤ abs a : abs_nonneg) (assume H1 : b > 0, H _ _ H1) @@ -530,74 +531,74 @@ iff.intro mod_eq_zero_of_dvd dvd_of_mod_eq_zero definition dvd.decidable_rel [instance] : decidable_rel dvd := take a n, decidable_of_decidable_of_iff _ (iff.symm !dvd_iff_mod_eq_zero) -theorem div_mul_cancel {a b : ℤ} (H : b ∣ a) : a div b * b = a := +protected theorem div_mul_cancel {a b : ℤ} (H : b ∣ a) : a div b * b = a := div_mul_cancel_of_mod_eq_zero (mod_eq_zero_of_dvd H) -theorem mul_div_cancel' {a b : ℤ} (H : a ∣ b) : a * (b div a) = b := -!mul.comm ▸ !div_mul_cancel H +protected theorem mul_div_cancel' {a b : ℤ} (H : a ∣ b) : a * (b div a) = b := +!mul.comm ▸ !int.div_mul_cancel H -theorem mul_div_assoc (a : ℤ) {b c : ℤ} (H : c ∣ b) : (a * b) div c = a * (b div c) := +protected theorem mul_div_assoc (a : ℤ) {b c : ℤ} (H : c ∣ b) : (a * b) div c = a * (b div c) := decidable.by_cases - (assume cz : c = 0, by rewrite [cz, *div_zero, mul_zero]) + (assume cz : c = 0, by rewrite [cz, *int.div_zero, mul_zero]) (assume cnz : c ≠ 0, obtain d (H' : b = d * c), from exists_eq_mul_left_of_dvd H, - by rewrite [H', -mul.assoc, *(!mul_div_cancel cnz)]) + by rewrite [H', -mul.assoc, *(!int.mul_div_cancel cnz)]) theorem div_dvd_div {a b c : ℤ} (H1 : a ∣ b) (H2 : b ∣ c) : b div a ∣ c div a := -have H3 : b = b div a * a, from (div_mul_cancel H1)⁻¹, -have H4 : c = c div a * a, from (div_mul_cancel (dvd.trans H1 H2))⁻¹, +have H3 : b = b div a * a, from (int.div_mul_cancel H1)⁻¹, +have H4 : c = c div a * a, from (int.div_mul_cancel (dvd.trans H1 H2))⁻¹, decidable.by_cases (assume H5 : a = 0, - have H6: c div a = 0, from (congr_arg _ H5 ⬝ !div_zero), + have H6: c div a = 0, from (congr_arg _ H5 ⬝ !int.div_zero), H6⁻¹ ▸ !dvd_zero) (assume H5 : a ≠ 0, dvd_of_mul_dvd_mul_right H5 (H3 ▸ H4 ▸ H2)) -theorem div_eq_iff_eq_mul_right {a b : ℤ} (c : ℤ) (H : b ≠ 0) (H' : b ∣ a) : +protected theorem div_eq_iff_eq_mul_right {a b : ℤ} (c : ℤ) (H : b ≠ 0) (H' : b ∣ a) : a div b = c ↔ a = b * c := iff.intro - (assume H1, by rewrite [-H1, mul_div_cancel' H']) - (assume H1, by rewrite [H1, !mul_div_cancel_left H]) + (assume H1, by rewrite [-H1, int.mul_div_cancel' H']) + (assume H1, by rewrite [H1, !int.mul_div_cancel_left H]) -theorem div_eq_iff_eq_mul_left {a b : ℤ} (c : ℤ) (H : b ≠ 0) (H' : b ∣ a) : +protected theorem div_eq_iff_eq_mul_left {a b : ℤ} (c : ℤ) (H : b ≠ 0) (H' : b ∣ a) : a div b = c ↔ a = c * b := -!mul.comm ▸ !div_eq_iff_eq_mul_right H H' +!mul.comm ▸ !int.div_eq_iff_eq_mul_right H H' -theorem eq_mul_of_div_eq_right {a b c : ℤ} (H1 : b ∣ a) (H2 : a div b = c) : +protected theorem eq_mul_of_div_eq_right {a b c : ℤ} (H1 : b ∣ a) (H2 : a div b = c) : a = b * c := calc - a = b * (a div b) : mul_div_cancel' H1 + a = b * (a div b) : int.mul_div_cancel' H1 ... = b * c : H2 -theorem div_eq_of_eq_mul_right {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = b * c) : +protected theorem div_eq_of_eq_mul_right {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = b * c) : a div b = c := calc a div b = b * c div b : H2 - ... = c : !mul_div_cancel_left H1 + ... = c : !int.mul_div_cancel_left H1 -theorem eq_mul_of_div_eq_left {a b c : ℤ} (H1 : b ∣ a) (H2 : a div b = c) : +protected 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 +!mul.comm ▸ !int.eq_mul_of_div_eq_right H1 H2 -theorem div_eq_of_eq_mul_left {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = c * b) : +protected theorem div_eq_of_eq_mul_left {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = c * b) : a div b = c := -div_eq_of_eq_mul_right H1 (!mul.comm ▸ H2) +int.div_eq_of_eq_mul_right H1 (!mul.comm ▸ H2) theorem neg_div_of_dvd {a b : ℤ} (H : b ∣ a) : -a div b = -(a div b) := decidable.by_cases - (assume H1 : b = 0, by rewrite [H1, *div_zero, neg_zero]) + (assume H1 : b = 0, by rewrite [H1, *int.div_zero, neg_zero]) (assume H1 : b ≠ 0, dvd.elim H (take c, assume H' : a = b * c, - by rewrite [H', neg_mul_eq_mul_neg, *!mul_div_cancel_left H1])) + by rewrite [H', neg_mul_eq_mul_neg, *!int.mul_div_cancel_left H1])) -theorem sign_eq_div_abs (a : ℤ) : sign a = a div (abs a) := +protected theorem sign_eq_div_abs (a : ℤ) : sign a = a div (abs a) := decidable.by_cases (suppose a = 0, by subst a) (suppose a ≠ 0, have abs a ≠ 0, from assume H, this (eq_zero_of_abs_eq_zero H), have abs a ∣ a, from abs_dvd_of_dvd !dvd.refl, - eq.symm (iff.mpr (!div_eq_iff_eq_mul_left `abs a ≠ 0` this) !eq_sign_mul_abs)) + eq.symm (iff.mpr (!int.div_eq_iff_eq_mul_left `abs a ≠ 0` this) !eq_sign_mul_abs)) theorem le_of_dvd {a b : ℤ} (bpos : b > 0) (H : a ∣ b) : a ≤ b := or.elim !le_or_gt @@ -613,35 +614,35 @@ or.elim !le_or_gt /- div and ordering -/ -theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a div b * b ≤ a := +protected 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 := +protected 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 := +protected 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) + int.div_le_of_le_mul H3 H5) (assume H3 : 0 = b, - by rewrite [-H3, div_zero]; apply H1) + by rewrite [-H3, int.div_zero]; apply H1) -theorem mul_le_of_le_div {a b c : ℤ} (H1 : c > 0) (H2 : a ≤ b div c) : a * c ≤ b := +protected 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) + ... ≤ b : !int.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 := +protected 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 @@ -650,13 +651,13 @@ have H3 : a * c < (b div c + 1) * c, from ... = (b div c + 1) * c : by rewrite [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) +protected theorem le_div_iff_mul_le {a b c : ℤ} (H : c > 0) : a ≤ b div c ↔ a * c ≤ b := +iff.intro (!int.mul_le_of_le_div H) (!int.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') +protected theorem div_le_div {a b c : ℤ} (H : c > 0) (H' : a ≤ b) : a div c ≤ b div c := +int.le_div_of_mul_le H (le.trans (!int.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 := +protected 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 @@ -665,7 +666,7 @@ lt_of_mul_lt_mul_right ... < 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 := +protected 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 [right_distrib at H3, one_mul at H3]; apply H3, @@ -674,33 +675,33 @@ calc ... < 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) +protected theorem div_lt_iff_lt_mul {a b c : ℤ} (H : c > 0) : a div c < b ↔ a < b * c := +iff.intro (!int.lt_mul_of_div_lt H) (!int.div_lt_of_lt_mul H) -theorem div_le_iff_le_mul_of_div {a b : ℤ} (c : ℤ) (H : b > 0) (H' : b ∣ a) : +protected 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'] +by rewrite [propext (!le_iff_mul_le_mul_right H), !int.div_mul_cancel H'] -theorem le_mul_of_div_le_of_div {a b c : ℤ} (H1 : b > 0) (H2 : b ∣ a) (H3 : a div b ≤ c) : +protected 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_of_div H1 H2) H3 +iff.mp (!int.div_le_iff_le_mul_of_div H1 H2) H3 theorem div_pos_of_pos_of_dvd {a b : ℤ} (H1 : a > 0) (H2 : b ≥ 0) (H3 : b ∣ a) : a div b > 0 := have H4 : b ≠ 0, from (assume H5 : b = 0, have H6 : a = 0, from eq_zero_of_zero_dvd (H5 ▸ H3), ne_of_gt H1 H6), -have H6 : (a div b) * b > 0, by rewrite (div_mul_cancel H3); apply H1, +have H6 : (a div b) * b > 0, by rewrite (int.div_mul_cancel H3); apply H1, pos_of_mul_pos_right H6 H2 theorem div_eq_div_of_dvd_of_dvd {a b c d : ℤ} (H1 : b ∣ a) (H2 : d ∣ c) (H3 : b ≠ 0) (H4 : d ≠ 0) (H5 : a * d = b * c) : a div b = c div d := begin - apply div_eq_of_eq_mul_right H3, - rewrite [-!mul_div_assoc H2], + apply int.div_eq_of_eq_mul_right H3, + rewrite [-!int.mul_div_assoc H2], apply eq.symm, - apply div_eq_of_eq_mul_left H4, + apply int.div_eq_of_eq_mul_left H4, apply eq.symm H5 end diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean index 46237898c4..0037f5f294 100644 --- a/library/data/int/gcd.lean +++ b/library/data/int/gcd.lean @@ -118,17 +118,17 @@ theorem gcd_div {a b c : ℤ} (H1 : c ∣ a) (H2 : c ∣ b) : decidable.by_cases (suppose c = 0, calc - gcd (a div c) (b div c) = gcd 0 0 : by subst c; rewrite *div_zero + gcd (a div c) (b div c) = gcd 0 0 : by subst c; rewrite *int.div_zero ... = 0 : gcd_zero_left - ... = gcd a b div 0 : div_zero + ... = gcd a b div 0 : int.div_zero ... = gcd a b div (abs c) : by subst c) (suppose c ≠ 0, have abs c ≠ 0, from assume H', this (eq_zero_of_abs_eq_zero H'), - eq.symm (div_eq_of_eq_mul_left this + eq.symm (int.div_eq_of_eq_mul_left this (eq.symm (calc gcd (a div c) (b div c) * abs c = gcd (a div c * c) (b div c * c) : gcd_mul_right - ... = gcd a (b div c * c) : div_mul_cancel H1 - ... = gcd a b : div_mul_cancel H2)))) + ... = gcd a (b div c * c) : int.div_mul_cancel H1 + ... = gcd a b : int.div_mul_cancel H2)))) theorem gcd_dvd_gcd_mul_left (a b c : ℤ) : gcd a b ∣ gcd (c * a) b := dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right @@ -287,7 +287,7 @@ theorem coprime_div_gcd_div_gcd {a b : ℤ} (H : gcd a b ≠ 0) : calc gcd (a div gcd a b) (b div gcd a b) = gcd a b div abs (gcd a b) : gcd_div !gcd_dvd_left !gcd_dvd_right - ... = 1 : by rewrite [abs_of_nonneg !gcd_nonneg, div_self H] + ... = 1 : by rewrite [abs_of_nonneg !gcd_nonneg, int.div_self H] theorem not_coprime_of_dvd_of_dvd {m n d : ℤ} (dgt1 : d > 1) (Hm : d ∣ m) (Hn : d ∣ n) : ¬ coprime m n := @@ -299,8 +299,8 @@ show false, from not_lt_of_ge `d ≤ 1` `d > 1` theorem exists_coprime {a b : ℤ} (H : gcd a b ≠ 0) : exists a' b', coprime a' b' ∧ a = a' * gcd a b ∧ b = b' * gcd a b := -have H1 : a = (a div gcd a b) * gcd a b, from (div_mul_cancel !gcd_dvd_left)⁻¹, -have H2 : b = (b div gcd a b) * gcd a b, from (div_mul_cancel !gcd_dvd_right)⁻¹, +have H1 : a = (a div gcd a b) * gcd a b, from (int.div_mul_cancel !gcd_dvd_left)⁻¹, +have H2 : b = (b div gcd a b) * gcd a b, from (int.div_mul_cancel !gcd_dvd_right)⁻¹, exists.intro _ (exists.intro _ (and.intro (coprime_div_gcd_div_gcd H) (and.intro H1 H2))) theorem coprime_mul {a b c : ℤ} (H1 : coprime a c) (H2 : coprime b c) : coprime (a * b) c := @@ -340,12 +340,12 @@ decidable.by_cases have H4 : (a * b) div gcd c a = (a div gcd c a) * b, from calc a * b div gcd c a = b * a div gcd c a : mul.comm - ... = b * (a div gcd c a) : !mul_div_assoc !gcd_dvd_right + ... = b * (a div gcd c a) : !int.mul_div_assoc !gcd_dvd_right ... = a div gcd c a * b : mul.comm, have H5 : c div gcd c a ∣ (a div gcd c a) * b, from H4 ▸ H3, have H6 : coprime (c div gcd c a) (a div gcd c a), from coprime_div_gcd_div_gcd `gcd c a ≠ 0`, have H7 : c div gcd c a ∣ b, from dvd_of_coprime_of_dvd_mul_left H6 H5, - have H8 : c = gcd c a * (c div gcd c a), from (mul_div_cancel' `gcd c a ∣ c`)⁻¹, + have H8 : c = gcd c a * (c div gcd c a), from (int.mul_div_cancel' `gcd c a ∣ c`)⁻¹, exists.intro _ (exists.intro _ (and.intro H8 (and.intro !gcd_dvd_right H7)))) end int diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 64f3ea8acd..6c37a83a49 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -28,13 +28,13 @@ has_divide.mk nat.divide 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 -theorem div_zero (a : ℕ) : a div 0 = 0 := +protected theorem div_zero (a : ℕ) : a div 0 = 0 := divide_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0)) theorem div_eq_zero_of_lt {a b : ℕ} (h : a < b) : a div b = 0 := divide_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_gt h)) -theorem zero_div (b : ℕ) : 0 div b = 0 := +protected theorem zero_div (b : ℕ) : 0 div b = 0 := divide_def 0 b ⬝ if_neg (and.rec not_le_of_gt) theorem div_eq_succ_sub_div {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a div b = succ ((a - b) div b) := @@ -44,7 +44,7 @@ theorem add_div_self (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) div z = succ (x d 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} + ... = succ (x div z) : {!nat.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 H @@ -64,15 +64,15 @@ nat.induction_on y 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 H -theorem mul_div_cancel (m : ℕ) {n : ℕ} (H : n > 0) : m * n div n = m := +protected 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 H - ... = 0 + m : zero_div + ... = 0 + m : nat.zero_div ... = m : zero_add -theorem mul_div_cancel_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n div m = n := -!mul.comm ▸ !mul_div_cancel H +protected theorem mul_div_cancel_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n div m = n := +!mul.comm ▸ !nat.mul_div_cancel H /- mod -/ @@ -108,7 +108,7 @@ by_cases_zero_pos 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) + ... = x mod z : nat.add_sub_cancel) theorem add_mod_self_left (x z : ℕ) : (x + z) mod x = z mod x := !add.comm ▸ !add_mod_self @@ -170,7 +170,7 @@ begin show x = x div y * y + x mod y, begin eapply nat.case_strong_induction_on x, - show 0 = (0 div y) * y + 0 mod y, by rewrite [zero_mod, add_zero, zero_div, zero_mul], + show 0 = (0 div y) * y + 0 mod y, by rewrite [zero_mod, add_zero, nat.zero_div, zero_mul], intro x IH, show succ x = succ x div y * y + succ x mod y, from if H1 : succ x < y then @@ -190,12 +190,12 @@ begin ... = ((succ x - y) div y) * y + y + (succ x - y) mod y : by rewrite H4 ... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add.right_comm ... = succ x - y + y : by rewrite -(IH _ H6) - ... = succ x : sub_add_cancel H2)⁻¹ + ... = succ x : nat.sub_add_cancel H2)⁻¹ end end theorem mod_eq_sub_div_mul (x y : ℕ) : x mod y = x - x div y * y := -eq_sub_of_add_eq (!add.comm ▸ !eq_div_mul_add_mod)⁻¹ +nat.eq_sub_of_add_eq (!add.comm ▸ !eq_div_mul_add_mod)⁻¹ theorem mod_add_mod (m n k : ℕ) : (m mod n + k) mod n = (m + k) mod n := by rewrite [eq_div_mul_add_mod m n at {2}, add.assoc, add.comm (m div n * n), add_mul_mod_self] @@ -251,23 +251,24 @@ have H5 : q1 * y = q2 * y, from add.right_cancel H4, have H6 : y > 0, from lt_of_le_of_lt !zero_le H1, show q1 = q2, from eq_of_mul_eq_mul_right H6 H5 -theorem mul_div_mul_left {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) div (z * y) = x div y := +protected theorem mul_div_mul_left {z : ℕ} (x y : ℕ) (zpos : z > 0) : + (z * x) div (z * y) = x div y := if H : y = 0 then - by rewrite [H, mul_zero, *div_zero] + by rewrite [H, mul_zero, *nat.div_zero] else - have ypos : y > 0, from pos_of_ne_zero H, - have zypos : z * y > 0, from mul_pos zpos ypos, - have H1 : (z * x) mod (z * y) < z * y, from !mod_lt zypos, - have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (!mod_lt ypos) zpos, - eq_quotient H1 H2 - (calc - ((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : eq_div_mul_add_mod - ... = z * (x div y * y + x mod y) : eq_div_mul_add_mod - ... = z * (x div y * y) + z * (x mod y) : left_distrib - ... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm) + have ypos : y > 0, from pos_of_ne_zero H, + have zypos : z * y > 0, from mul_pos zpos ypos, + have H1 : (z * x) mod (z * y) < z * y, from !mod_lt zypos, + have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (!mod_lt ypos) zpos, + eq_quotient H1 H2 + (calc + ((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : eq_div_mul_add_mod + ... = z * (x div y * y + x mod y) : eq_div_mul_add_mod + ... = z * (x div y * y) + z * (x mod y) : left_distrib + ... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm) -theorem mul_div_mul_right {x z y : ℕ} (zpos : z > 0) : (x * z) div (y * z) = x div y := -!mul.comm ▸ !mul.comm ▸ !mul_div_mul_left zpos +protected theorem mul_div_mul_right {x z y : ℕ} (zpos : z > 0) : (x * z) div (y * z) = x div y := +!mul.comm ▸ !mul.comm ▸ !nat.mul_div_mul_left zpos theorem mul_mod_mul_left (z x y : ℕ) : (z * x) mod (z * y) = z * (x mod y) := or.elim (eq_zero_or_pos z) @@ -305,13 +306,13 @@ calc theorem mul_mod_eq_mul_mod_mod (m n k : nat) : (m * n) mod k = (m * (n mod k)) mod k := !mul.comm ▸ !mul.comm ▸ !mul_mod_eq_mod_mul_mod -theorem div_one (n : ℕ) : n div 1 = n := +protected theorem div_one (n : ℕ) : n div 1 = n := assert n div 1 * 1 + n mod 1 = n, from !eq_div_mul_add_mod⁻¹, begin rewrite [-this at {2}, mul_one, mod_one] end -theorem div_self {n : ℕ} (H : n > 0) : n div n = 1 := -assert (n * 1) div (n * 1) = 1 div 1, from !mul_div_mul_left H, -by rewrite [div_one at this, -this, *mul_one] +protected theorem div_self {n : ℕ} (H : n > 0) : n div n = 1 := +assert (n * 1) div (n * 1) = 1 div 1, from !nat.mul_div_mul_left H, +by rewrite [nat.div_one at this, -this, *mul_one] theorem div_mul_cancel_of_mod_eq_zero {m n : ℕ} (H : m mod n = 0) : m div n * n = m := by rewrite [eq_div_mul_add_mod m n at {2}, H, add_zero] @@ -333,30 +334,30 @@ iff.intro mod_eq_zero_of_dvd dvd_of_mod_eq_zero definition dvd.decidable_rel [instance] : decidable_rel dvd := take m n, decidable_of_decidable_of_iff _ (iff.symm !dvd_iff_mod_eq_zero) -theorem div_mul_cancel {m n : ℕ} (H : n ∣ m) : m div n * n = m := +protected theorem div_mul_cancel {m n : ℕ} (H : n ∣ m) : m div n * n = m := div_mul_cancel_of_mod_eq_zero (mod_eq_zero_of_dvd H) -theorem mul_div_cancel' {m n : ℕ} (H : n ∣ m) : n * (m div n) = m := -!mul.comm ▸ div_mul_cancel H +protected theorem mul_div_cancel' {m n : ℕ} (H : n ∣ m) : n * (m div n) = m := +!mul.comm ▸ nat.div_mul_cancel H theorem dvd_of_dvd_add_left {m n₁ n₂ : ℕ} (H₁ : m ∣ n₁ + n₂) (H₂ : m ∣ n₁) : m ∣ n₂ := obtain (c₁ : nat) (Hc₁ : n₁ + n₂ = m * c₁), from H₁, obtain (c₂ : nat) (Hc₂ : n₁ = m * c₂), from H₂, have aux : m * (c₁ - c₂) = n₂, from calc - m * (c₁ - c₂) = m * c₁ - m * c₂ : mul_sub_left_distrib + m * (c₁ - c₂) = m * c₁ - m * c₂ : nat.mul_sub_left_distrib ... = n₁ + n₂ - m * c₂ : Hc₁ ... = n₁ + n₂ - n₁ : Hc₂ - ... = n₂ : add_sub_cancel_left, + ... = n₂ : nat.add_sub_cancel_left, dvd.intro aux 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) +nat.dvd_of_dvd_add_left (!add.comm ▸ H) theorem dvd_sub {m n₁ n₂ : ℕ} (H1 : m ∣ n₁) (H2 : m ∣ n₂) : m ∣ n₁ - n₂ := by_cases (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) + have H4 : n₁ = n₁ - n₂ + n₂, from (nat.sub_add_cancel H3)⁻¹, + show m ∣ n₁ - n₂, from nat.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 _) @@ -375,21 +376,21 @@ by_cases_zero_pos n have k = 1, from eq_one_of_mul_eq_one_left this, show m = n, from (mul_one m)⁻¹ ⬝ (this ▸ Hk⁻¹)) -theorem mul_div_assoc (m : ℕ) {n k : ℕ} (H : k ∣ n) : m * n div k = m * (n div k) := +protected theorem mul_div_assoc (m : ℕ) {n k : ℕ} (H : k ∣ n) : m * n div k = m * (n div k) := or.elim (eq_zero_or_pos k) (assume H1 : k = 0, calc m * n div k = m * n div 0 : H1 - ... = 0 : div_zero + ... = 0 : nat.div_zero ... = m * 0 : mul_zero m - ... = m * (n div 0) : div_zero + ... = m * (n div 0) : nat.div_zero ... = m * (n div k) : H1) (assume H1 : k > 0, - have H2 : n = n div k * k, from (div_mul_cancel H)⁻¹, + have H2 : n = n div k * k, from (nat.div_mul_cancel H)⁻¹, calc m * n div k = m * (n div k * k) div k : H2 ... = m * (n div k) * k div k : mul.assoc - ... = m * (n div k) : mul_div_cancel _ H1) + ... = m * (n div k) : nat.mul_div_cancel _ H1) theorem dvd_of_mul_dvd_mul_left {m n k : ℕ} (kpos : k > 0) (H : k * m ∣ k * n) : m ∣ n := dvd.elim H @@ -399,50 +400,50 @@ dvd.elim H dvd.intro H2⁻¹) theorem dvd_of_mul_dvd_mul_right {m n k : ℕ} (kpos : k > 0) (H : m * k ∣ n * k) : m ∣ n := -dvd_of_mul_dvd_mul_left kpos (!mul.comm ▸ !mul.comm ▸ H) +nat.dvd_of_mul_dvd_mul_left kpos (!mul.comm ▸ !mul.comm ▸ H) lemma dvd_of_eq_mul (i j n : nat) : n = j*i → j ∣ n := begin intros, subst n, apply dvd_mul_right end theorem div_dvd_div {k m n : ℕ} (H1 : k ∣ m) (H2 : m ∣ n) : m div k ∣ n div k := -have H3 : m = m div k * k, from (div_mul_cancel H1)⁻¹, -have H4 : n = n div k * k, from (div_mul_cancel (dvd.trans H1 H2))⁻¹, +have H3 : m = m div k * k, from (nat.div_mul_cancel H1)⁻¹, +have H4 : n = n div k * k, from (nat.div_mul_cancel (dvd.trans H1 H2))⁻¹, or.elim (eq_zero_or_pos k) (assume H5 : k = 0, - have H6: n div k = 0, from (congr_arg _ H5 ⬝ !div_zero), + have H6: n div k = 0, from (congr_arg _ H5 ⬝ !nat.div_zero), H6⁻¹ ▸ !dvd_zero) (assume H5 : k > 0, - dvd_of_mul_dvd_mul_right H5 (H3 ▸ H4 ▸ H2)) + nat.dvd_of_mul_dvd_mul_right H5 (H3 ▸ H4 ▸ H2)) -theorem div_eq_iff_eq_mul_right {m n : ℕ} (k : ℕ) (H : n > 0) (H' : n ∣ m) : +protected theorem div_eq_iff_eq_mul_right {m n : ℕ} (k : ℕ) (H : n > 0) (H' : n ∣ m) : m div n = k ↔ m = n * k := iff.intro - (assume H1, by rewrite [-H1, mul_div_cancel' H']) - (assume H1, by rewrite [H1, !mul_div_cancel_left H]) + (assume H1, by rewrite [-H1, nat.mul_div_cancel' H']) + (assume H1, by rewrite [H1, !nat.mul_div_cancel_left H]) -theorem div_eq_iff_eq_mul_left {m n : ℕ} (k : ℕ) (H : n > 0) (H' : n ∣ m) : +protected theorem div_eq_iff_eq_mul_left {m n : ℕ} (k : ℕ) (H : n > 0) (H' : n ∣ m) : m div n = k ↔ m = k * n := -!mul.comm ▸ !div_eq_iff_eq_mul_right H H' +!mul.comm ▸ !nat.div_eq_iff_eq_mul_right H H' -theorem eq_mul_of_div_eq_right {m n k : ℕ} (H1 : n ∣ m) (H2 : m div n = k) : +protected theorem eq_mul_of_div_eq_right {m n k : ℕ} (H1 : n ∣ m) (H2 : m div n = k) : m = n * k := calc - m = n * (m div n) : mul_div_cancel' H1 + m = n * (m div n) : nat.mul_div_cancel' H1 ... = n * k : H2 -theorem div_eq_of_eq_mul_right {m n k : ℕ} (H1 : n > 0) (H2 : m = n * k) : +protected theorem div_eq_of_eq_mul_right {m n k : ℕ} (H1 : n > 0) (H2 : m = n * k) : m div n = k := calc m div n = n * k div n : H2 - ... = k : !mul_div_cancel_left H1 + ... = k : !nat.mul_div_cancel_left H1 -theorem eq_mul_of_div_eq_left {m n k : ℕ} (H1 : n ∣ m) (H2 : m div n = k) : +protected theorem eq_mul_of_div_eq_left {m n k : ℕ} (H1 : n ∣ m) (H2 : m div n = k) : m = k * n := -!mul.comm ▸ !eq_mul_of_div_eq_right H1 H2 +!mul.comm ▸ !nat.eq_mul_of_div_eq_right H1 H2 -theorem div_eq_of_eq_mul_left {m n k : ℕ} (H1 : n > 0) (H2 : m = k * n) : +protected 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) +!nat.div_eq_of_eq_mul_right H1 (!mul.comm ▸ H2) lemma add_mod_eq_of_dvd (i j n : nat) : n ∣ j → (i + j) mod n = i mod n := assume h, @@ -471,12 +472,12 @@ 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 := +protected 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 + ... = 0 : nat.div_zero ... ≤ n : zero_le) (assume H1 : k > 0, le_of_mul_le_mul_right (calc @@ -484,20 +485,20 @@ or.elim (eq_zero_or_pos k) ... = 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) +protected theorem div_le_self (m n : ℕ) : m div n ≤ m := +nat.cases_on n (!nat.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 + nat.div_le_of_le_mul H -theorem mul_le_of_le_div {m n k : ℕ} (H : m ≤ n div k) : m * k ≤ n := +protected 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 := +protected 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 @@ -506,21 +507,21 @@ have H3 : m * k < (succ (n div k)) * k, from ... = (succ (n div k)) * k : succ_mul, le_of_lt_succ (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) +protected theorem le_div_iff_mul_le {m n k : ℕ} (H : k > 0) : m ≤ n div k ↔ m * k ≤ n := +iff.intro !nat.mul_le_of_le_div (!nat.le_div_of_mul_le H) -theorem div_le_div {m n : ℕ} (k : ℕ) (H : m ≤ n) : m div k ≤ n div k := +protected 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)) + (by rewrite [*nat.div_zero]) + (take k, assume H1 : k > 0, nat.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 := +protected 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 := +protected 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 @@ -528,38 +529,38 @@ calc ... < 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 +protected theorem div_lt_iff_lt_mul {m n k : ℕ} (H : k > 0) : m div k < n ↔ m < n * k := +iff.intro (!nat.lt_mul_of_div_lt H) !nat.div_lt_of_lt_mul -theorem div_le_iff_le_mul_of_div {m n : ℕ} (k : ℕ) (H : n > 0) (H' : n ∣ m) : +protected 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'] +by rewrite [propext (!le_iff_mul_le_mul_right H), !nat.div_mul_cancel H'] -theorem le_mul_of_div_le_of_div {m n k : ℕ} (H1 : n > 0) (H2 : n ∣ m) (H3 : m div n ≤ k) : +protected 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_of_div H1 H2) H3 +iff.mp (!nat.div_le_iff_le_mul_of_div 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 := begin - have H1 : k div m < n, from div_lt_of_lt_mul (!mul.comm ▸ H), + have H1 : k div m < n, from nat.div_lt_of_lt_mul (!mul.comm ▸ H), have H2 : n - k div m ≥ 1, from - le_sub_of_add_le (calc + nat.le_sub_of_add_le (calc 1 + k div m = succ (k div m) : add.comm ... ≤ n : succ_le_of_lt H1), - have H3 : n - k div m = n - k div m - 1 + 1, from (sub_add_cancel H2)⁻¹, + have H3 : n - k div m = n - k div m - 1 + 1, from (nat.sub_add_cancel H2)⁻¹, have H4 : m > 0, from pos_of_ne_zero (assume H': m = 0, not_lt_zero k (begin rewrite [H' at H, zero_mul at H], exact H end)), have H5 : k mod m + 1 ≤ m, from succ_le_of_lt (!mod_lt H4), - have H6 : m - (k mod m + 1) < m, from sub_lt_self H4 !succ_pos, + have H6 : m - (k mod m + 1) < m, from nat.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] + ... = (m * n - k div m * m - (k mod m + 1)) div m : by rewrite [*nat.sub_sub] ... = ((n - k div m) * m - (k mod m + 1)) div m : - by rewrite [mul.comm m, mul_sub_right_distrib] + by rewrite [mul.comm m, nat.mul_sub_right_distrib] ... = ((n - k div m - 1) * m + m - (k mod m + 1)) div m : by rewrite [H3 at {1}, right_distrib, nat.one_mul] - ... = ((n - k div m - 1) * m + (m - (k mod m + 1))) div m : {add_sub_assoc H5 _} + ... = ((n - k div m - 1) * m + (m - (k mod m + 1))) div m : {nat.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 : @@ -579,7 +580,7 @@ nat.strong_induction_on a (suppose k₂ = a, assert i₁ : a < b * c, by rewrite -this; assumption, assert k₁ = 0, from div_eq_zero_of_lt i₁, - assert a div b < c, by rewrite [mul.comm at i₁]; exact div_lt_of_lt_mul i₁, + assert a div b < c, by rewrite [mul.comm at i₁]; exact nat.div_lt_of_lt_mul i₁, begin rewrite [`k₁ = 0`], show (a div b) div c = 0, from div_eq_zero_of_lt `a div b < c` @@ -596,12 +597,12 @@ nat.strong_induction_on a assert (k₂ div b) div c = 0, by rewrite [e₂, e₃], show (a div b) div c = k₁, by rewrite [e₁, this])) -lemma div_div_eq_div_mul (a b c : nat) : (a div b) div c = a div (b * c) := +protected lemma div_div_eq_div_mul (a b c : nat) : (a div b) div c = a div (b * c) := begin cases b with b, - rewrite [zero_mul, *div_zero, zero_div], + rewrite [zero_mul, *nat.div_zero, nat.zero_div], cases c with c, - rewrite [mul_zero, *div_zero], + rewrite [mul_zero, *nat.div_zero], apply div_div_aux a (succ b) (succ c) dec_trivial dec_trivial end @@ -609,7 +610,7 @@ lemma div_lt_of_ne_zero : ∀ {n : nat}, n ≠ 0 → n div 2 < n | 0 h := absurd rfl h | (succ n) h := begin - apply div_lt_of_lt_mul, + apply nat.div_lt_of_lt_mul, rewrite [-add_one, right_distrib], change n + 1 < (n * 1 + n) + (1 + 1), rewrite [mul_one, -add.assoc], diff --git a/library/data/nat/examples/partial_sum.lean b/library/data/nat/examples/partial_sum.lean index 9e31389421..f8b02c638d 100644 --- a/library/data/nat/examples/partial_sum.lean +++ b/library/data/nat/examples/partial_sum.lean @@ -30,4 +30,4 @@ theorem partial_sum_eq : ∀ n, partial_sum n = ((n + 1) * n) div 2 := take n, assert h₁ : (2 * partial_sum n) div 2 = ((succ n) * n) div 2, by rewrite two_mul_partial_sum_eq, assert h₂ : (2:nat) > 0, from dec_trivial, -by rewrite [mul_div_cancel_left _ h₂ at h₁]; exact h₁ +by rewrite [nat.mul_div_cancel_left _ h₂ at h₁]; exact h₁ diff --git a/library/data/nat/gcd.lean b/library/data/nat/gcd.lean index feb37cb797..6f17e39875 100644 --- a/library/data/nat/gcd.lean +++ b/library/data/nat/gcd.lean @@ -94,7 +94,7 @@ gcd.induction m n (take m, imp.intro) (IH : k ∣ n → k ∣ m mod n → k ∣ gcd n (m mod n)) (H1 : k ∣ m) (H2 : k ∣ n), have H3 : k ∣ m div n * n + m mod n, from !eq_div_mul_add_mod ▸ H1, - have H4 : k ∣ m mod n, from dvd_of_dvd_add_left H3 (dvd.trans H2 !dvd_mul_left), + have H4 : k ∣ m mod n, from nat.dvd_of_dvd_add_left H3 (dvd.trans H2 !dvd_mul_left), !gcd_rec⁻¹ ▸ IH H2 H4) theorem gcd.comm (m n : ℕ) : gcd m n = gcd n m := @@ -150,10 +150,10 @@ eq_zero_of_gcd_eq_zero_left (!gcd.comm ▸ H) theorem gcd_div {m n k : ℕ} (H1 : k ∣ m) (H2 : k ∣ n) : gcd (m div k) (n div k) = gcd m n div k := or.elim (eq_zero_or_pos k) - (assume H3 : k = 0, by subst k; rewrite *div_zero) - (assume H3 : k > 0, (div_eq_of_eq_mul_left H3 (calc - gcd m n = gcd m (n div k * k) : div_mul_cancel H2 - ... = gcd (m div k * k) (n div k * k) : div_mul_cancel H1 + (assume H3 : k = 0, by subst k; rewrite *nat.div_zero) + (assume H3 : k > 0, (nat.div_eq_of_eq_mul_left H3 (calc + gcd m n = gcd m (n div k * k) : nat.div_mul_cancel H2 + ... = gcd (m div k * k) (n div k * k) : nat.div_mul_cancel H1 ... = gcd (m div k) (n div k) * k : gcd_mul_right))⁻¹) theorem gcd_dvd_gcd_mul_left (m n k : ℕ) : gcd m n ∣ gcd (k * m) n := @@ -183,7 +183,7 @@ theorem lcm_zero_left (m : ℕ) : lcm 0 m = 0 := calc lcm 0 m = 0 * m div gcd 0 m : rfl ... = 0 div gcd 0 m : zero_mul - ... = 0 : zero_div + ... = 0 : nat.zero_div theorem lcm_zero_right (m : ℕ) : lcm m 0 = 0 := !lcm.comm ▸ !lcm_zero_left @@ -192,27 +192,27 @@ calc lcm 1 m = 1 * m div gcd 1 m : rfl ... = m div gcd 1 m : one_mul ... = m div 1 : gcd_one_left - ... = m : div_one + ... = m : nat.div_one theorem lcm_one_right (m : ℕ) : lcm m 1 = m := !lcm.comm ▸ !lcm_one_left theorem lcm_self (m : ℕ) : lcm m m = m := have H : m * m div m = m, from - by_cases_zero_pos m !div_zero (take m, assume H1 : m > 0, !mul_div_cancel H1), + by_cases_zero_pos m !nat.div_zero (take m, assume H1 : m > 0, !nat.mul_div_cancel H1), calc lcm m m = m * m div gcd m m : rfl ... = m * m div m : gcd_self ... = m : H theorem dvd_lcm_left (m n : ℕ) : m ∣ lcm m n := -have H : lcm m n = m * (n div gcd m n), from mul_div_assoc _ !gcd_dvd_right, +have H : lcm m n = m * (n div gcd m n), from nat.mul_div_assoc _ !gcd_dvd_right, dvd.intro H⁻¹ theorem dvd_lcm_right (m n : ℕ) : n ∣ lcm m n := !lcm.comm ▸ !dvd_lcm_left theorem gcd_mul_lcm (m n : ℕ) : gcd m n * lcm m n = m * n := -eq.symm (eq_mul_of_div_eq_right (dvd.trans !gcd_dvd_left !dvd_mul_right) rfl) +eq.symm (nat.eq_mul_of_div_eq_right (dvd.trans !gcd_dvd_left !dvd_mul_right) rfl) theorem lcm_dvd {m n k : ℕ} (H1 : m ∣ k) (H2 : n ∣ k) : lcm m n ∣ k := or.elim (eq_zero_or_pos k) @@ -302,7 +302,7 @@ theorem coprime_div_gcd_div_gcd {m n : ℕ} (H : gcd m n > 0) : coprime (m div gcd m n) (n div gcd m n) := calc gcd (m div gcd m n) (n div gcd m n) = gcd m n div gcd m n : gcd_div !gcd_dvd_left !gcd_dvd_right - ... = 1 : div_self H + ... = 1 : nat.div_self H theorem not_coprime_of_dvd_of_dvd {m n d : ℕ} (dgt1 : d > 1) (Hm : d ∣ m) (Hn : d ∣ n) : ¬ coprime m n := @@ -314,8 +314,8 @@ show false, from not_lt_of_ge `d ≤ 1` `d > 1` theorem exists_coprime {m n : ℕ} (H : gcd m n > 0) : exists m' n', coprime m' n' ∧ m = m' * gcd m n ∧ n = n' * gcd m n := -have H1 : m = (m div gcd m n) * gcd m n, from (div_mul_cancel !gcd_dvd_left)⁻¹, -have H2 : n = (n div gcd m n) * gcd m n, from (div_mul_cancel !gcd_dvd_right)⁻¹, +have H1 : m = (m div gcd m n) * gcd m n, from (nat.div_mul_cancel !gcd_dvd_left)⁻¹, +have H2 : n = (n div gcd m n) * gcd m n, from (nat.div_mul_cancel !gcd_dvd_right)⁻¹, exists.intro _ (exists.intro _ (and.intro (coprime_div_gcd_div_gcd H) (and.intro H1 H2))) theorem coprime_mul {m n k : ℕ} (H1 : coprime m k) (H2 : coprime n k) : coprime (m * n) k := @@ -357,16 +357,16 @@ or.elim (eq_zero_or_pos (gcd k m)) exists.intro _ (exists.intro _ (and.intro H4 (and.intro H5 H6)))) (assume H1 : gcd k m > 0, have H2 : gcd k m ∣ k, from !gcd_dvd_left, - have H3 : k div gcd k m ∣ (m * n) div gcd k m, from div_dvd_div H2 H, + have H3 : k div gcd k m ∣ (m * n) div gcd k m, from nat.div_dvd_div H2 H, have H4 : (m * n) div gcd k m = (m div gcd k m) * n, from calc m * n div gcd k m = n * m div gcd k m : mul.comm - ... = n * (m div gcd k m) : !mul_div_assoc !gcd_dvd_right + ... = n * (m div gcd k m) : !nat.mul_div_assoc !gcd_dvd_right ... = m div gcd k m * n : mul.comm, have H5 : k div gcd k m ∣ (m div gcd k m) * n, from H4 ▸ H3, have H6 : coprime (k div gcd k m) (m div gcd k m), from coprime_div_gcd_div_gcd H1, have H7 : k div gcd k m ∣ n, from dvd_of_coprime_of_dvd_mul_left H6 H5, - have H8 : k = gcd k m * (k div gcd k m), from (mul_div_cancel' H2)⁻¹, + have H8 : k = gcd k m * (k div gcd k m), from (nat.mul_div_cancel' H2)⁻¹, exists.intro _ (exists.intro _ (and.intro H8 (and.intro !gcd_dvd_right H7)))) end nat diff --git a/library/data/nat/pairing.lean b/library/data/nat/pairing.lean index e2c2b805c1..5befe9ef77 100644 --- a/library/data/nat/pairing.lean +++ b/library/data/nat/pairing.lean @@ -30,21 +30,22 @@ by_cases (suppose h₁ : ¬ n - s*s < s, have s ≤ n - s*s, from le_of_not_gt h₁, assert s + s*s ≤ n - s*s + s*s, from add_le_add_right this (s*s), - assert s*s + s ≤ n, by rewrite [sub_add_cancel (sqrt_lower n) at this, add.comm at this]; assumption, + assert s*s + s ≤ n, by rewrite [nat.sub_add_cancel (sqrt_lower n) at this, + add.comm at this]; assumption, have n ≤ s*s + s + s, from sqrt_upper n, have n - s*s ≤ s + s, from calc - n - s*s ≤ (s*s + s + s) - s*s : sub_le_sub_right this (s*s) + n - s*s ≤ (s*s + s + s) - s*s : nat.sub_le_sub_right this (s*s) ... = (s*s + (s+s)) - s*s : by rewrite add.assoc - ... = s + s : by rewrite add_sub_cancel_left, + ... = s + s : by rewrite nat.add_sub_cancel_left, have n - s*s - s ≤ s, from calc - n - s*s - s ≤ (s + s) - s : sub_le_sub_right this s - ... = s : by rewrite add_sub_cancel_left, + n - s*s - s ≤ (s + s) - s : nat.sub_le_sub_right this s + ... = s : by rewrite nat.add_sub_cancel_left, assert h₂ : ¬ s < n - s*s - s, from not_lt_of_ge this, begin esimp [unpair], rewrite [if_neg h₁], esimp, esimp [mkpair], - rewrite [if_neg h₂, sub_sub, add_sub_of_le `s*s + s ≤ n`], + rewrite [if_neg h₂, nat.sub_sub, add_sub_of_le `s*s + s ≤ n`], end) theorem unpair_mkpair (a b : nat) : unpair (mkpair a b) = (a, b) := @@ -57,7 +58,7 @@ by_cases esimp [mkpair], rewrite [if_pos `a < b`], esimp [unpair], - rewrite [sqrt_offset_eq `a ≤ b + b`, add_sub_cancel_left, if_pos `a < b`] + rewrite [sqrt_offset_eq `a ≤ b + b`, nat.add_sub_cancel_left, if_pos `a < b`] end) (suppose ¬ a < b, have b ≤ a, from le_of_not_gt this, @@ -68,7 +69,8 @@ by_cases esimp [mkpair], rewrite [if_neg `¬ a < b`], esimp [unpair], - rewrite [add.assoc (a * a) a b, sqrt_offset_eq `a + b ≤ a + a`, *add_sub_cancel_left, if_neg `¬ a + b < a`] + rewrite [add.assoc (a * a) a b, sqrt_offset_eq `a + b ≤ a + a`, *nat.add_sub_cancel_left, + if_neg `¬ a + b < a`] end) open prod.ops diff --git a/library/data/nat/parity.lean b/library/data/nat/parity.lean index 34b90d6358..01a440e954 100644 --- a/library/data/nat/parity.lean +++ b/library/data/nat/parity.lean @@ -268,7 +268,7 @@ assume h₁ h₂, obtain w₂ (hw₂ : m = 2*w₂), from exists_of_even `even m`, begin substvars, rewrite [mul.comm 2 w₁ at h₁, mul.comm 2 w₂ at h₁, - *mul_div_cancel _ (dec_trivial : 2 > 0) at h₁, h₁] + *nat.mul_div_cancel _ (dec_trivial : 2 > 0) at h₁, h₁] end) (suppose odd m, absurd `odd m` (not_odd_of_even (iff.mp h₂ `even n`)))) (suppose odd n, or.elim (em (even m)) diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean index f2ed5eff08..2944e38693 100644 --- a/library/data/nat/power.lean +++ b/library/data/nat/power.lean @@ -72,8 +72,8 @@ theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → a^b = a^c → b = c by rewrite [pow_cancel_left h₁ this] theorem pow_div_cancel : ∀ {a b : nat}, a ≠ 0 → (a ^ succ b) div a = a ^ b -| a 0 h := by rewrite [pow_succ, pow_zero, mul_one, div_self (pos_of_ne_zero h)] -| a (succ b) h := by rewrite [pow_succ, mul_div_cancel_left _ (pos_of_ne_zero h)] +| a 0 h := by rewrite [pow_succ, pow_zero, mul_one, nat.div_self (pos_of_ne_zero h)] +| a (succ b) h := by rewrite [pow_succ, nat.mul_div_cancel_left _ (pos_of_ne_zero h)] lemma dvd_pow : ∀ (i : nat) {n : nat}, n > 0 → i ∣ i^n | i 0 h := absurd h !lt.irrefl @@ -88,12 +88,13 @@ iff.mp !dvd_iff_mod_eq_zero (dvd_pow i h) lemma pow_dvd_of_pow_succ_dvd {p i n : nat} : p^(succ i) ∣ n → p^i ∣ n := suppose p^(succ i) ∣ n, -assert p^i ∣ p^(succ i), from by rewrite [pow_succ']; apply dvd_of_eq_mul; apply rfl, +assert p^i ∣ p^(succ i), + by rewrite [pow_succ']; apply nat.dvd_of_eq_mul; apply rfl, dvd.trans `p^i ∣ p^(succ i)` `p^(succ i) ∣ n` lemma dvd_of_pow_succ_dvd_mul_pow {p i n : nat} (Ppos : p > 0) : p^(succ i) ∣ (n * p^i) → p ∣ n := -by rewrite [pow_succ]; apply dvd_of_mul_dvd_mul_right; apply pow_pos_of_pos _ Ppos +by rewrite [pow_succ]; apply nat.dvd_of_mul_dvd_mul_right; apply pow_pos_of_pos _ Ppos lemma coprime_pow_right {a b} : ∀ n, coprime b a → coprime b (a^n) | 0 h := !comprime_one_right diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 9dd1078463..b74db85183 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -12,14 +12,14 @@ namespace nat /- subtraction -/ -theorem sub_zero (n : ℕ) : n - 0 = n := +protected theorem sub_zero (n : ℕ) : n - 0 = n := rfl theorem sub_succ (n m : ℕ) : n - succ m = pred (n - m) := rfl -theorem zero_sub (n : ℕ) : 0 - n = 0 := -nat.induction_on n !sub_zero +protected theorem zero_sub (n : ℕ) : 0 - n = 0 := +nat.induction_on n !nat.sub_zero (take k : nat, assume IH : 0 - k = 0, calc @@ -30,10 +30,10 @@ nat.induction_on n !sub_zero theorem succ_sub_succ (n m : ℕ) : succ n - succ m = n - m := succ_sub_succ_eq_sub n m -theorem sub_self (n : ℕ) : n - n = 0 := -nat.induction_on n !sub_zero (take k IH, !succ_sub_succ ⬝ IH) +protected theorem sub_self (n : ℕ) : n - n = 0 := +nat.induction_on n !nat.sub_zero (take k IH, !succ_sub_succ ⬝ IH) -theorem add_sub_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m := +protected theorem add_sub_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m := nat.induction_on k (calc (n + 0) - (m + 0) = n - (m + 0) : {!add_zero} @@ -45,10 +45,10 @@ nat.induction_on k ... = succ (n + l) - succ (m + l) : {!add_succ} ... = (n + l) - (m + l) : !succ_sub_succ ... = n - m : IH) -theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m := -!add.comm ▸ !add.comm ▸ !add_sub_add_right +protected theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m := +!add.comm ▸ !add.comm ▸ !nat.add_sub_add_right -theorem add_sub_cancel (n m : ℕ) : n + m - m = n := +protected theorem add_sub_cancel (n m : ℕ) : n + m - m = n := nat.induction_on m (begin rewrite add_zero end) (take k : ℕ, @@ -58,13 +58,13 @@ nat.induction_on m ... = n + k - k : succ_sub_succ ... = n : IH) -theorem add_sub_cancel_left (n m : ℕ) : n + m - n = m := -!add.comm ▸ !add_sub_cancel +protected theorem add_sub_cancel_left (n m : ℕ) : n + m - n = m := +!add.comm ▸ !nat.add_sub_cancel -theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) := +protected theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) := nat.induction_on k (calc - n - m - 0 = n - m : sub_zero + n - m - 0 = n - m : nat.sub_zero ... = n - (m + 0) : add_zero) (take l : nat, assume IH : n - m - l = n - (m + l), @@ -76,22 +76,22 @@ nat.induction_on k theorem succ_sub_sub_succ (n m k : ℕ) : succ n - m - succ k = n - m - k := calc - succ n - m - succ k = succ n - (m + succ k) : sub_sub + succ n - m - succ k = succ n - (m + succ k) : nat.sub_sub ... = succ n - succ (m + k) : add_succ ... = n - (m + k) : succ_sub_succ - ... = n - m - k : sub_sub + ... = n - m - k : nat.sub_sub theorem sub_self_add (n m : ℕ) : n - (n + m) = 0 := calc - n - (n + m) = n - n - m : sub_sub - ... = 0 - m : sub_self - ... = 0 : zero_sub + n - (n + m) = n - n - m : nat.sub_sub + ... = 0 - m : nat.sub_self + ... = 0 : nat.zero_sub -theorem sub.right_comm (m n k : ℕ) : m - n - k = m - k - n := +protected theorem sub.right_comm (m n k : ℕ) : m - n - k = m - k - n := calc - m - n - k = m - (n + k) : !sub_sub + m - n - k = m - (n + k) : !nat.sub_sub ... = m - (k + n) : {!add.comm} - ... = m - k - n : !sub_sub⁻¹ + ... = m - k - n : !nat.sub_sub⁻¹ theorem sub_one (n : ℕ) : n - 1 = pred n := rfl @@ -106,13 +106,13 @@ nat.induction_on n (calc pred 0 * m = 0 * m : pred_zero ... = 0 : zero_mul - ... = 0 - m : zero_sub + ... = 0 - m : nat.zero_sub ... = 0 * m - m : zero_mul) (take k : nat, assume IH : pred k * m = k * m - m, calc pred (succ k) * m = k * m : pred_succ - ... = k * m + m - m : add_sub_cancel + ... = k * m + m - m : nat.add_sub_cancel ... = succ k * m - m : succ_mul) theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n := @@ -121,11 +121,11 @@ calc ... = m * n - n : mul_pred_left ... = n * m - n : mul.comm -theorem mul_sub_right_distrib (n m k : ℕ) : (n - m) * k = n * k - m * k := +protected theorem mul_sub_right_distrib (n m k : ℕ) : (n - m) * k = n * k - m * k := nat.induction_on m (calc - (n - 0) * k = n * k : sub_zero - ... = n * k - 0 : sub_zero + (n - 0) * k = n * k : nat.sub_zero + ... = n * k - 0 : nat.sub_zero ... = n * k - 0 * k : zero_mul) (take l : nat, assume IH : (n - l) * k = n * k - l * k, @@ -133,18 +133,19 @@ nat.induction_on m (n - succ l) * k = pred (n - l) * k : sub_succ ... = (n - l) * k - k : mul_pred_left ... = n * k - l * k - k : IH - ... = n * k - (l * k + k) : sub_sub + ... = n * k - (l * k + k) : nat.sub_sub ... = n * k - (succ l * k) : succ_mul) -theorem mul_sub_left_distrib (n m k : ℕ) : n * (m - k) = n * m - n * k := +protected theorem mul_sub_left_distrib (n m k : ℕ) : n * (m - k) = n * m - n * k := calc n * (m - k) = (m - k) * n : !mul.comm - ... = m * n - k * n : !mul_sub_right_distrib + ... = m * n - k * n : !nat.mul_sub_right_distrib ... = n * m - k * n : {!mul.comm} ... = n * m - n * k : {!mul.comm} -theorem mul_self_sub_mul_self_eq (a b : nat) : a * a - b * b = (a + b) * (a - b) := -by rewrite [mul_sub_left_distrib, *right_distrib, mul.comm b a, add.comm (a*a) (a*b), add_sub_add_left] +protected theorem mul_self_sub_mul_self_eq (a b : nat) : a * a - b * b = (a + b) * (a - b) := +by rewrite [nat.mul_sub_left_distrib, *right_distrib, mul.comm b a, add.comm (a*a) (a*b), + nat.add_sub_add_left] theorem succ_mul_succ_eq (a : nat) : succ a * succ a = a*a + a + a + 1 := calc succ a * succ a = (a+1)*(a+1) : by rewrite [add_one] @@ -175,7 +176,7 @@ sub_induction n m assume H : 0 ≤ k, calc 0 + (k - 0) = k - 0 : zero_add - ... = k : sub_zero) + ... = k : nat.sub_zero) (take k, assume H : succ k ≤ 0, absurd H !not_succ_le_zero) (take k l, assume IH : k ≤ l → k + (l - k) = l, @@ -190,7 +191,7 @@ calc n + (m - n) = n + 0 : sub_eq_zero_of_le H ... = n : add_zero -theorem sub_add_cancel {n m : ℕ} : n ≥ m → n - m + m = n := +protected theorem sub_add_cancel {n m : ℕ} : n ≥ m → n - m + m = n := !add.comm ▸ !add_sub_of_le theorem sub_add_of_le {n m : ℕ} : n ≤ m → n - m + m = m := @@ -207,16 +208,16 @@ obtain (k : ℕ) (Hk : n + k = m), from le.elim H, exists.intro k (calc m - k = n + k - k : by rewrite Hk - ... = n : add_sub_cancel) + ... = n : nat.add_sub_cancel) -theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) := +protected theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) := have l1 : k ≤ m → n + m - k = n + (m - k), from sub_induction k m (take m : ℕ, assume H : 0 ≤ m, calc - n + m - 0 = n + m : sub_zero - ... = n + (m - 0) : sub_zero) + n + m - 0 = n + m : nat.sub_zero + ... = n + (m - 0) : nat.sub_zero) (take k : ℕ, assume H : succ k ≤ 0, absurd H !not_succ_le_zero) (take k m, assume IH : k ≤ m → n + m - k = n + (m - k), @@ -245,21 +246,21 @@ or.elim !le.total (assume H3 : m ≤ n, (sub_eq_zero_of_le H3)⁻¹ ▸ (H1 (n - m) (add_sub_of_le H3)⁻¹)) -theorem sub_eq_of_add_eq {n m k : ℕ} (H : n + m = k) : k - n = m := +protected theorem sub_eq_of_add_eq {n m k : ℕ} (H : n + m = k) : k - n = m := have H2 : k - n + n = m + n, from calc - k - n + n = k : sub_add_cancel (le.intro H) + k - n + n = k : nat.sub_add_cancel (le.intro H) ... = n + m : H⁻¹ ... = m + n : !add.comm, add.right_cancel H2 -theorem eq_sub_of_add_eq {a b c : ℕ} (H : a + c = b) : a = b - c := -(sub_eq_of_add_eq (!add.comm ▸ H))⁻¹ +protected theorem eq_sub_of_add_eq {a b c : ℕ} (H : a + c = b) : a = b - c := +(nat.sub_eq_of_add_eq (!add.comm ▸ H))⁻¹ -theorem sub_eq_of_eq_add {a b c : ℕ} (H : a = c + b) : a - b = c := -sub_eq_of_add_eq (!add.comm ▸ H⁻¹) +protected theorem sub_eq_of_eq_add {a b c : ℕ} (H : a = c + b) : a - b = c := +nat.sub_eq_of_add_eq (!add.comm ▸ H⁻¹) -theorem sub_le_sub_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n - k ≤ m - k := +protected theorem sub_le_sub_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n - k ≤ m - k := obtain (l : ℕ) (Hl : n + l = m), from le.elim H, or.elim !le.total (assume H2 : n ≤ k, (sub_eq_zero_of_le H2)⁻¹ ▸ !zero_le) @@ -267,12 +268,12 @@ or.elim !le.total have H3 : n - k + l = m - k, from calc n - k + l = l + (n - k) : add.comm - ... = l + n - k : add_sub_assoc H2 l + ... = l + n - k : nat.add_sub_assoc H2 l ... = n + l - k : add.comm ... = m - k : Hl, le.intro H3) -theorem sub_le_sub_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k - m ≤ k - n := +protected theorem sub_le_sub_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k - m ≤ k - n := obtain (l : ℕ) (Hl : n + l = m), from le.elim H, sub.cases (assume H2 : k ≤ m, !zero_le) @@ -286,43 +287,43 @@ sub.cases ... = n + l + m' : add.assoc ... = m + m' : Hl ... = k : Hm - ... = k - n + n : sub_add_cancel H3, + ... = k - n + n : nat.sub_add_cancel H3, le.intro (add.right_cancel H4)) open algebra -theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 := -assert H1 : n = n - m + m, from (sub_add_cancel (le_of_lt H))⁻¹, +protected theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 := +assert H1 : n = n - m + m, from (nat.sub_add_cancel (le_of_lt H))⁻¹, have H2 : 0 + m < n - m + m, begin rewrite [zero_add, -H1], exact H end, !lt_of_add_lt_add_right H2 -theorem lt_of_sub_pos {m n : ℕ} (H : n - m > 0) : m < n := +protected theorem lt_of_sub_pos {m n : ℕ} (H : n - m > 0) : m < n := lt_of_not_ge (take H1 : m ≥ n, have H2 : n - m = 0, from sub_eq_zero_of_le H1, !lt.irrefl (H2 ▸ H)) -theorem lt_of_sub_lt_sub_right {n m k : ℕ} (H : n - k < m - k) : n < m := +protected theorem lt_of_sub_lt_sub_right {n m k : ℕ} (H : n - k < m - k) : n < m := lt_of_not_ge (assume H1 : m ≤ n, - have H2 : m - k ≤ n - k, from sub_le_sub_right H1 _, + have H2 : m - k ≤ n - k, from nat.sub_le_sub_right H1 _, not_le_of_gt H H2) -theorem lt_of_sub_lt_sub_left {n m k : ℕ} (H : n - m < n - k) : k < m := +protected theorem lt_of_sub_lt_sub_left {n m k : ℕ} (H : n - m < n - k) : k < m := lt_of_not_ge (assume H1 : m ≤ k, - have H2 : n - k ≤ n - m, from sub_le_sub_left H1 _, + have H2 : n - k ≤ n - m, from nat.sub_le_sub_left H1 _, not_le_of_gt H H2) -theorem sub_lt_sub_add_sub (n m k : ℕ) : n - k ≤ (n - m) + (m - k) := +protected theorem sub_lt_sub_add_sub (n m k : ℕ) : n - k ≤ (n - m) + (m - k) := sub.cases - (assume H : n ≤ m, !zero_add⁻¹ ▸ sub_le_sub_right H k) + (assume H : n ≤ m, !zero_add⁻¹ ▸ nat.sub_le_sub_right H k) (take mn : ℕ, assume Hmn : m + mn = n, sub.cases (assume H : m ≤ k, - have H2 : n - k ≤ n - m, from sub_le_sub_left H n, - assert H3 : n - k ≤ mn, from sub_eq_of_add_eq Hmn ▸ H2, + have H2 : n - k ≤ n - m, from nat.sub_le_sub_left H n, + assert H3 : n - k ≤ mn, from nat.sub_eq_of_add_eq Hmn ▸ H2, show n - k ≤ mn + 0, begin rewrite add_zero, assumption end) (take km : ℕ, assume Hkm : k + km = m, @@ -332,10 +333,10 @@ sub.cases ... = k + km + mn : add.assoc ... = m + mn : Hkm ... = n : Hmn, - have H2 : n - k = mn + km, from sub_eq_of_add_eq H, + have H2 : n - k = mn + km, from nat.sub_eq_of_add_eq H, H2 ▸ !le.refl)) -theorem sub_lt_self {m n : ℕ} (H1 : m > 0) (H2 : n > 0) : m - n < m := +protected 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 @@ -344,22 +345,22 @@ calc ... < 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 := +protected 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 + m = m + k - k : nat.add_sub_cancel + ... ≤ n - k : nat.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 +protected theorem lt_sub_of_add_lt {m n k : ℕ} (H : m + k < n) (H2 : k ≤ n) : m < n - k := +lt_of_succ_le (nat.le_sub_of_add_le (calc succ m + k = succ (m + k) : succ_add_eq_succ_add ... ≤ n : succ_le_of_lt H)) -theorem sub_lt_of_lt_add {v n m : nat} (h₁ : v < n + m) (h₂ : n ≤ v) : v - n < m := +protected theorem sub_lt_of_lt_add {v n m : nat} (h₁ : v < n + m) (h₂ : n ≤ v) : v - n < m := have succ v ≤ n + m, from succ_le_of_lt h₁, have succ (v - n) ≤ m, from calc succ (v - n) = succ v - n : succ_sub h₂ - ... ≤ n + m - n : sub_le_sub_right this n - ... = m : add_sub_cancel_left, + ... ≤ n + m - n : nat.sub_le_sub_right this n + ... = m : nat.add_sub_cancel_left, lt_of_succ_le this /- distance -/ @@ -371,8 +372,8 @@ theorem dist.comm (n m : ℕ) : dist n m = dist m n := theorem dist_self (n : ℕ) : dist n n = 0 := calc - (n - n) + (n - n) = 0 + (n - n) : sub_self - ... = 0 + 0 : sub_self + (n - n) + (n - n) = 0 + (n - n) : nat.sub_self + ... = 0 + 0 : nat.sub_self ... = 0 : rfl theorem eq_of_dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m := @@ -383,7 +384,7 @@ have H5 : m ≤ n, from le_of_sub_eq_zero H4, le.antisymm H3 H5 theorem dist_eq_zero {n m : ℕ} (H : n = m) : dist n m = 0 := -by substvars; rewrite [↑dist, *sub_self, add_zero] +by substvars; rewrite [↑dist, *nat.sub_self, add_zero] theorem dist_eq_sub_of_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n := calc @@ -400,21 +401,21 @@ theorem dist_eq_sub_of_gt {n m : ℕ} (H : n > m) : dist n m = n - m := dist_eq_sub_of_ge (le_of_lt H) theorem dist_zero_right (n : ℕ) : dist n 0 = n := -dist_eq_sub_of_ge !zero_le ⬝ !sub_zero +dist_eq_sub_of_ge !zero_le ⬝ !nat.sub_zero theorem dist_zero_left (n : ℕ) : dist 0 n = n := -dist_eq_sub_of_le !zero_le ⬝ !sub_zero +dist_eq_sub_of_le !zero_le ⬝ !nat.sub_zero theorem dist.intro {n m k : ℕ} (H : n + m = k) : dist k n = m := calc dist k n = k - n : dist_eq_sub_of_ge (le.intro H) - ... = m : sub_eq_of_add_eq H + ... = m : nat.sub_eq_of_add_eq H theorem dist_add_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m := calc dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : rfl - ... = (n - m) + ((m + k) - (n + k)) : add_sub_add_right - ... = (n - m) + (m - n) : add_sub_add_right + ... = (n - m) + ((m + k) - (n + k)) : nat.add_sub_add_right + ... = (n - m) + (m - n) : nat.add_sub_add_right theorem dist_add_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m := begin rewrite [add.comm k n, add.comm k m]; apply dist_add_add_right end @@ -422,7 +423,7 @@ begin rewrite [add.comm k n, add.comm k m]; apply dist_add_add_right end theorem dist_add_eq_of_ge {n m : ℕ} (H : n ≥ m) : dist n m + m = n := calc dist n m + m = n - m + m : {dist_eq_sub_of_ge H} - ... = n : sub_add_cancel H + ... = n : nat.sub_add_cancel H theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m := calc @@ -436,7 +437,7 @@ have H2 : n - m + (k + m) = k + n, from calc n - m + (k + m) = n - m + (m + k) : add.comm ... = n - m + m + k : add.assoc - ... = n + k : sub_add_cancel H + ... = n + k : nat.sub_add_cancel H ... = k + n : add.comm, dist_eq_intro H2 @@ -449,7 +450,7 @@ have (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k begin rewrite [add.comm (k - m) (m - n), {n - m + _ + _}add.assoc, {m - k + _}add.left_comm, -add.assoc] end, -this ▸ add_le_add !sub_lt_sub_add_sub !sub_lt_sub_add_sub +this ▸ add_le_add !nat.sub_lt_sub_add_sub !nat.sub_lt_sub_add_sub theorem dist_add_add_le_add_dist_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l := assert H : dist (n + m) (k + m) + dist (k + m) (k + l) = dist n k + dist m l, @@ -458,7 +459,7 @@ by rewrite -H; apply dist.triangle_inequality theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k := assert ∀ n m, dist n m = n - m + (m - n), from take n m, rfl, -by rewrite [this, this n m, right_distrib, *mul_sub_right_distrib] +by rewrite [this, this n m, right_distrib, *nat.mul_sub_right_distrib] theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m := begin rewrite [mul.comm k n, mul.comm k m, dist_mul_right, mul.comm] end @@ -472,10 +473,10 @@ have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l 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 rewrite [*mul_sub_left_distrib] + ... = dist (n * k - n * l) (m * k - m * l) : by rewrite [*nat.mul_sub_left_distrib] ... = 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) (n * l + m * k - m * l) : nat.add_sub_assoc H2 (n * l) ... = dist (n * k + m * l) (n * l + m * k) : dist_sub_eq_dist_add_right H3 _, or.elim !le.total (assume H : k ≤ l, !dist.comm ▸ !dist.comm ▸ aux l k H) @@ -483,8 +484,10 @@ or.elim !le.total lemma dist_eq_max_sub_min {i j : nat} : dist i j = (max i j) - min i j := or.elim (lt_or_ge i j) - (suppose i < j, begin rewrite [max_eq_right_of_lt this, min_eq_left_of_lt this, dist_eq_sub_of_lt this] end) - (suppose i ≥ j, begin rewrite [max_eq_left this , min_eq_right this, dist_eq_sub_of_ge this] end) + (suppose i < j, + by rewrite [max_eq_right_of_lt this, min_eq_left_of_lt this, dist_eq_sub_of_lt this]) + (suppose i ≥ j, + by rewrite [max_eq_left this , min_eq_right this, dist_eq_sub_of_ge this]) lemma dist_succ {i j : nat} : dist (succ i) (succ j) = dist i j := by rewrite [↑dist, *succ_sub_succ] @@ -494,8 +497,8 @@ begin rewrite dist_eq_max_sub_min, apply sub_le end lemma dist_pos_of_ne {i j : nat} : i ≠ j → dist i j > 0 := assume Pne, lt.by_cases - (suppose i < j, begin rewrite [dist_eq_sub_of_lt this], apply sub_pos_of_lt this end) + (suppose i < j, begin rewrite [dist_eq_sub_of_lt this], apply nat.sub_pos_of_lt this end) (suppose i = j, by contradiction) - (suppose i > j, begin rewrite [dist_eq_sub_of_gt this], apply sub_pos_of_lt this end) + (suppose i > j, begin rewrite [dist_eq_sub_of_gt this], apply nat.sub_pos_of_lt this end) end nat diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 720acaa4d9..442d6763cf 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -306,8 +306,8 @@ theorem reduce_equiv : ∀ a : prerat, reduce a ≡ a (assume anz : an = 0, begin rewrite [↑reduce, if_pos anz, ↑equiv, anz], krewrite zero_mul end) (assume annz : an ≠ 0, - by rewrite [↑reduce, if_neg annz, ↑equiv, algebra.mul.comm, -!mul_div_assoc !gcd_dvd_left, - -!mul_div_assoc !gcd_dvd_right, algebra.mul.comm]) + by rewrite [↑reduce, if_neg annz, ↑equiv, algebra.mul.comm, -!int.mul_div_assoc + !gcd_dvd_left, -!int.mul_div_assoc !gcd_dvd_right, algebra.mul.comm]) theorem reduce_eq_reduce : ∀{a b : prerat}, a ≡ b → reduce a = reduce b | (mk an ad adpos) (mk bn bd bdpos) := @@ -588,7 +588,7 @@ iff.mpr (!eq_div_iff_mul_eq H) (mul_denom a) theorem of_int_div {a b : ℤ} (H : b ∣ a) : of_int (a div b) = of_int a / of_int b := decidable.by_cases (assume bz : b = 0, - by rewrite [bz, div_zero, of_int_zero, algebra.div_zero]) + by rewrite [bz, int.div_zero, of_int_zero, algebra.div_zero]) (assume bnz : b ≠ 0, have bnz' : of_int b ≠ 0, from assume oibz, bnz (of_int.inj oibz), have H' : of_int (a div b) * of_int b = of_int a, from diff --git a/library/data/set/card.lean b/library/data/set/card.lean index 01681f03ae..9dc5fed316 100644 --- a/library/data/set/card.lean +++ b/library/data/set/card.lean @@ -67,7 +67,7 @@ end theorem card_union (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] : card (s₁ ∪ s₂) = card s₁ + card s₂ - card (s₁ ∩ s₂) := calc - card (s₁ ∪ s₂) = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) - card (s₁ ∩ s₂) : add_sub_cancel + card (s₁ ∪ s₂) = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) - card (s₁ ∩ s₂) : nat.add_sub_cancel ... = card s₁ + card s₂ - card (s₁ ∩ s₂) : card_add_card s₁ s₂ theorem card_union_of_disjoint {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ∩ s₂ = ∅) : diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index 91655dd4b7..e4568b1e91 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -119,7 +119,7 @@ take ε, suppose ε > 0, obtain N HN, from H `ε > 0`, exists.intro (N + k) (take n : ℕ, assume nge : n ≥ N + k, - have n - k ≥ N, from le_sub_of_add_le nge, + have n - k ≥ N, from nat.le_sub_of_add_le nge, have dist (X (n - k + k)) y < ε, from HN (n - k) this, show dist (X n) y < ε, using this, by rewrite [(nat.sub_add_cancel (le.trans !le_add_left nge)) at this]; exact this) diff --git a/library/theories/combinatorics/choose.lean b/library/theories/combinatorics/choose.lean index bbf036ada3..e43a42f5d2 100644 --- a/library/theories/combinatorics/choose.lean +++ b/library/theories/combinatorics/choose.lean @@ -113,7 +113,7 @@ begin end theorem choose_def_alt {n k : ℕ} (H : k ≤ n) : choose n k = fact n div (fact k * fact (n -k)) := -eq.symm (div_eq_of_eq_mul_left (mul_pos !fact_pos !fact_pos) +eq.symm (nat.div_eq_of_eq_mul_left (mul_pos !fact_pos !fact_pos) (by rewrite [-mul.assoc, choose_mul_fact_mul_fact H])) theorem fact_mul_fact_dvd_fact {n k : ℕ} (H : k ≤ n) : fact k * fact (n - k) ∣ fact n := diff --git a/library/theories/group_theory/pgroup.lean b/library/theories/group_theory/pgroup.lean index f18e893868..2a5dc136f0 100644 --- a/library/theories/group_theory/pgroup.lean +++ b/library/theories/group_theory/pgroup.lean @@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author : Haitao Zhang -/ -import theories.number_theory.primes data algebra.group algebra.group_power algebra.group_bigops .cyclic .finsubg .hom .perm .action +import theories.number_theory.primes data algebra.group algebra.group_power algebra.group_bigops +import .cyclic .finsubg .hom .perm .action open nat fin list algebra function subtype diff --git a/library/theories/number_theory/irrational_roots.lean b/library/theories/number_theory/irrational_roots.lean index 70b81c2701..482fbe7820 100644 --- a/library/theories/number_theory/irrational_roots.lean +++ b/library/theories/number_theory/irrational_roots.lean @@ -16,15 +16,24 @@ section theorem sqrt_two_irrational {a b : ℕ} (co : coprime a b) : a^2 ≠ 2 * b^2 := assume H : a^2 = 2 * b^2, - have even (a^2), from even_of_exists (exists.intro _ H), - have even a, from even_of_even_pow this, - obtain (c : nat) (aeq : a = 2 * c), from exists_of_even this, - have 2 * (2 * c^2) = 2 * b^2, begin rewrite [-H, aeq, *pow_two, algebra.mul.assoc, algebra.mul.left_comm c] end, - have 2 * c^2 = b^2, from eq_of_mul_eq_mul_left dec_trivial this, - have even (b^2), from even_of_exists (exists.intro _ (eq.symm this)), - have even b, from even_of_even_pow this, - assert 2 ∣ gcd a b, from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`), - have 2 ∣ 1, begin rewrite [gcd_eq_one_of_coprime co at this], exact this end, + have even (a^2), + from even_of_exists (exists.intro _ H), + have even a, + from even_of_even_pow this, + obtain (c : nat) (aeq : a = 2 * c), + from exists_of_even this, + have 2 * (2 * c^2) = 2 * b^2, + by rewrite [-H, aeq, *pow_two, algebra.mul.assoc, algebra.mul.left_comm c], + have 2 * c^2 = b^2, + from eq_of_mul_eq_mul_left dec_trivial this, + have even (b^2), + from even_of_exists (exists.intro _ (eq.symm this)), + have even b, + from even_of_even_pow this, + assert 2 ∣ gcd a b, + from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`), + have 2 ∣ 1, + begin rewrite [gcd_eq_one_of_coprime co at this], exact this end, show false, from absurd `2 ∣ 1` dec_trivial end @@ -41,22 +50,37 @@ section (H : a^n = c * b^n) : b = 1 := have bpos : b > 0, from pos_of_ne_zero (suppose b = 0, - have a^n = 0, by rewrite [H, this, zero_pow npos], - assert a = 0, from eq_zero_of_pow_eq_zero this, - show false, from ne_of_lt `0 < a` this⁻¹), + have a^n = 0, + by rewrite [H, this, zero_pow npos], + assert a = 0, + from eq_zero_of_pow_eq_zero this, + show false, + from ne_of_lt `0 < a` this⁻¹), have H₁ : ∀ p, prime p → ¬ p ∣ b, from - take p, suppose prime p, suppose p ∣ b, - assert p ∣ b^n, from dvd_pow_of_dvd_of_pos `p ∣ b` `n > 0`, - have p ∣ a^n, by rewrite H; apply dvd_mul_of_dvd_right this, - have p ∣ a, from dvd_of_prime_of_dvd_pow `prime p` this, - have ¬ coprime a b, from not_coprime_of_dvd_of_dvd (gt_one_of_prime `prime p`) `p ∣ a` `p ∣ b`, - show false, from this `coprime a b`, - have blt2 : b < 2, from by_contradiction - (suppose ¬ b < 2, - have b ≥ 2, from le_of_not_gt this, - obtain p [primep pdvdb], from exists_prime_and_dvd this, - show false, from H₁ p primep pdvdb), - show b = 1, from (le.antisymm (le_of_lt_succ blt2) (succ_le_of_lt bpos)) + take p, + suppose prime p, + suppose p ∣ b, + assert p ∣ b^n, + from dvd_pow_of_dvd_of_pos `p ∣ b` `n > 0`, + have p ∣ a^n, + by rewrite H; apply dvd_mul_of_dvd_right this, + have p ∣ a, + from dvd_of_prime_of_dvd_pow `prime p` this, + have ¬ coprime a b, + from not_coprime_of_dvd_of_dvd (gt_one_of_prime `prime p`) `p ∣ a` `p ∣ b`, + show false, + from this `coprime a b`, + have blt2 : b < 2, + from by_contradiction + (suppose ¬ b < 2, + have b ≥ 2, + from le_of_not_gt this, + obtain p [primep pdvdb], + from exists_prime_and_dvd this, + show false, + from H₁ p primep pdvdb), + show b = 1, + from (le.antisymm (le_of_lt_succ blt2) (succ_le_of_lt bpos)) end /- @@ -70,39 +94,52 @@ section theorem denom_eq_one_of_pow_eq {q : ℚ} {n : ℕ} {c : ℤ} (npos : n > 0) (H : q^n = c) : denom q = 1 := let a := num q, b := denom q in - have b ≠ 0, from ne_of_gt (denom_pos q), - have bnz : b ≠ (0 : ℚ), from assume H, `b ≠ 0` (of_int.inj H), - have bnnz : ((b : rat)^n ≠ 0), from assume bneqz, bnz (algebra.eq_zero_of_pow_eq_zero bneqz), - have a^n /[rat] b^n = c, using bnz, begin rewrite [*of_int_pow, -algebra.div_pow, -eq_num_div_denom, -H] end, - have (a^n : rat) = c *[rat] b^n, from eq.symm (!mul_eq_of_eq_div bnnz this⁻¹), + have b ≠ 0, + from ne_of_gt (denom_pos q), + have bnz : b ≠ (0 : ℚ), + from assume H, `b ≠ 0` (of_int.inj H), + have bnnz : ((b : rat)^n ≠ 0), + from assume bneqz, bnz (algebra.eq_zero_of_pow_eq_zero bneqz), + have a^n /[rat] b^n = c, + using bnz, begin rewrite [*of_int_pow, -algebra.div_pow, -eq_num_div_denom, -H] end, + have (a^n : rat) = c *[rat] b^n, + from eq.symm (!mul_eq_of_eq_div bnnz this⁻¹), have a^n = c * b^n, -- int version using this, by rewrite [-of_int_pow at this, -of_int_mul at this]; exact of_int.inj this, have (abs a)^n = abs c * (abs b)^n, using this, by rewrite [-abs_pow, this, abs_mul, abs_pow], have H₁ : (nat_abs a)^n = nat_abs c * (nat_abs b)^n, using this, - begin apply int.of_nat.inj, rewrite [int.of_nat_mul, +int.of_nat_pow, +of_nat_nat_abs], exact this end, - have H₂ : nat.coprime (nat_abs a) (nat_abs b), from of_nat.inj !coprime_num_denom, + begin apply int.of_nat.inj, rewrite [int.of_nat_mul, +int.of_nat_pow, +of_nat_nat_abs], + exact this end, + have H₂ : nat.coprime (nat_abs a) (nat_abs b), + from of_nat.inj !coprime_num_denom, have nat_abs b = 1, from by_cases - (suppose q = 0, by rewrite this) + (suppose q = 0, + by rewrite this) (suppose qne0 : q ≠ 0, using H₁ H₂, begin have ane0 : a ≠ 0, from suppose aeq0 : a = 0, - have qeq0 : q = 0, by rewrite [eq_num_div_denom, aeq0, of_int_zero, algebra.zero_div], - absurd qeq0 qne0, + have qeq0 : q = 0, + by rewrite [eq_num_div_denom, aeq0, of_int_zero, algebra.zero_div], + show false, + from qne0 qeq0, have nat_abs a ≠ 0, from suppose nat_abs a = 0, - have aeq0 : a = 0, from eq_zero_of_nat_abs_eq_zero this, - absurd aeq0 ane0, + have aeq0 : a = 0, + from eq_zero_of_nat_abs_eq_zero this, + show false, from ane0 aeq0, show nat_abs b = 1, from (root_irrational npos (pos_of_ne_zero this) H₂ H₁) end), - show b = 1, using this, begin rewrite [-of_nat_nat_abs_of_nonneg (le_of_lt !denom_pos), this] end + show b = 1, + using this, begin rewrite [-of_nat_nat_abs_of_nonneg (le_of_lt !denom_pos), this] end theorem eq_num_pow_of_pow_eq {q : ℚ} {n : ℕ} {c : ℤ} (npos : n > 0) (H : q^n = c) : c = (num q)^n := - have denom q = 1, from denom_eq_one_of_pow_eq npos H, + have denom q = 1, + from denom_eq_one_of_pow_eq npos H, have of_int c = of_int ((num q)^n), using this, by rewrite [-H, eq_num_div_denom q at {1}, this, of_int_one, div_one, of_int_pow], show c = (num q)^n , from of_int.inj this @@ -115,7 +152,8 @@ section theorem not_eq_pow_of_prime {p n : ℕ} (a : ℕ) (ngt1 : n > 1) (primep : prime p) : p ≠ a^n := assume peq : p = a^n, - have npos : n > 0, from lt.trans dec_trivial ngt1, + have npos : n > 0, + from lt.trans dec_trivial ngt1, have pnez : p ≠ 0, from (suppose p = 0, show false, @@ -127,9 +165,12 @@ section n * mult p a = mult p (a^n) : begin rewrite [mult_pow n agtz primep] end ... = mult p p : peq ... = 1 : mult_self (gt_one_of_prime primep), - have n ∣ 1, from dvd_of_mul_right_eq this, - have n = 1, from eq_one_of_dvd_one this, - show false, using this, by rewrite this at ngt1; exact !lt.irrefl ngt1 + have n ∣ 1, + from dvd_of_mul_right_eq this, + have n = 1, + from eq_one_of_dvd_one this, + show false, using this, + by rewrite this at ngt1; exact !lt.irrefl ngt1 open int rat @@ -158,16 +199,22 @@ section example {a b c : ℤ} (co : coprime a b) (apos : a > 0) (bpos : b > 0) (H : a * a = c * (b * b)) : b = 1 := - assert H₁ : gcd (c * b) a = gcd c a, from gcd_mul_right_cancel_of_coprime _ (coprime_swap co), - have a * a = c * b * b, by rewrite -mul.assoc at H; apply H, - have a div (gcd a b) = c * b div gcd (c * b) a, from div_gcd_eq_div_gcd this bpos apos, - have a = c * b div gcd c a, - using this, by revert this; rewrite [↑coprime at co, co, int.div_one, H₁]; intros; assumption, - have a = b * (c div gcd c a), - using this, - by revert this; rewrite [mul.comm, !mul_div_assoc !gcd_dvd_left]; intros; assumption, - have b ∣ a, from dvd_of_mul_right_eq this⁻¹, - have b ∣ gcd a b, from dvd_gcd this !dvd.refl, - have b ∣ 1, using this, by rewrite [↑coprime at co, co at this]; apply this, - show b = 1, from eq_one_of_dvd_one (le_of_lt bpos) this + assert H₁ : gcd (c * b) a = gcd c a, + from gcd_mul_right_cancel_of_coprime _ (coprime_swap co), + have a * a = c * b * b, + by rewrite -mul.assoc at H; apply H, + have a div (gcd a b) = c * b div gcd (c * b) a, + from div_gcd_eq_div_gcd this bpos apos, + have a = c * b div gcd c a, using this, + by revert this; rewrite [↑coprime at co, co, int.div_one, H₁]; intros; assumption, + have a = b * (c div gcd c a), using this, + by revert this; rewrite [mul.comm, !int.mul_div_assoc !gcd_dvd_left]; intros; assumption, + have b ∣ a, + from dvd_of_mul_right_eq this⁻¹, + have b ∣ gcd a b, + from dvd_gcd this !dvd.refl, + have b ∣ 1, using this, + by rewrite [↑coprime at co, co at this]; apply this, + show b = 1, + from eq_one_of_dvd_one (le_of_lt bpos) this end diff --git a/library/theories/number_theory/prime_factorization.lean b/library/theories/number_theory/prime_factorization.lean index 60c494d483..354440a6a4 100644 --- a/library/theories/number_theory/prime_factorization.lean +++ b/library/theories/number_theory/prime_factorization.lean @@ -31,7 +31,7 @@ end theorem mult_rec_decreasing {p n : ℕ} (Hp : p > 1) (Hn : n > 0) : n div p < n := have H' : n < n * p, by rewrite [-mul_one n at {1}]; apply mul_lt_mul_of_pos_left Hp Hn, -div_lt_of_lt_mul H' +nat.div_lt_of_lt_mul H' private definition mult.F (p : ℕ) (n : ℕ) (f: Π {m : ℕ}, m < n → ℕ) : ℕ := if H : (p > 1 ∧ n > 0) ∧ p ∣ n then @@ -95,7 +95,7 @@ begin (take n', suppose n = p * n', have p > 0, from lt.trans zero_lt_one pgt1, - assert n div p = n', from !div_eq_of_eq_mul_right this `n = p * n'`, + assert n div p = n', from !nat.div_eq_of_eq_mul_right this `n = p * n'`, assert n' < n, by rewrite -this; apply mult_rec_decreasing pgt1 npos, begin @@ -124,7 +124,7 @@ begin have p > 0, from lt.trans zero_lt_one pgt1, have psin_pos : p^(succ i) * n > 0, from mul_pos (!pow_pos_of_pos this) npos, have p ∣ p^(succ i) * n, by rewrite [pow_succ, mul.assoc]; apply dvd_mul_right, - rewrite [mult_rec pgt1 psin_pos this, pow_succ', mul.right_comm, !mul_div_cancel `p > 0`, ih], + rewrite [mult_rec pgt1 psin_pos this, pow_succ', mul.right_comm, !nat.mul_div_cancel `p > 0`, ih], rewrite [add.comm i, add.comm (succ i)] end @@ -146,7 +146,7 @@ assume pdvd : p ∣ n div p^(mult p n), obtain m (H : n div p^(mult p n) = p * m), from exists_eq_mul_right_of_dvd pdvd, assert n = p^(succ (mult p n)) * m, from calc - n = p^mult p n * (n div p^mult p n) : by rewrite (mul_div_cancel' !pow_mult_dvd) + n = p^mult p n * (n div p^mult p n) : by rewrite (nat.mul_div_cancel' !pow_mult_dvd) ... = p^(succ (mult p n)) * m : by rewrite [H, pow_succ', mul.assoc], have p^(succ (mult p n)) ∣ n, by rewrite this at {2}; apply dvd_mul_right, have succ (mult p n) ≤ mult p n, from le_mult pgt1 npos this, @@ -156,8 +156,8 @@ theorem mult_mul {p m n : ℕ} (primep : prime p) (mpos : m > 0) (npos : n > 0) mult p (m * n) = mult p m + mult p n := let m' := m div p^mult p m, n' := n div p^mult p n in assert p > 1, from gt_one_of_prime primep, -assert meq : m = p^mult p m * m', by rewrite (mul_div_cancel' !pow_mult_dvd), -assert neq : n = p^mult p n * n', by rewrite (mul_div_cancel' !pow_mult_dvd), +assert meq : m = p^mult p m * m', by rewrite (nat.mul_div_cancel' !pow_mult_dvd), +assert neq : n = p^mult p n * n', by rewrite (nat.mul_div_cancel' !pow_mult_dvd), have m'pos : m' > 0, from pos_of_mul_pos_left (meq ▸ mpos), have n'pos : n' > 0, from pos_of_mul_pos_left (neq ▸ npos), have npdvdm' : ¬ p ∣ m', from !not_dvd_div_pow_mult `p > 1` mpos, @@ -172,7 +172,8 @@ calc ... = mult p m + mult p n : by rewrite [!mult_pow_mul `p > 1` m'n'pos, multm'n'] -theorem mult_pow {p m : ℕ} (n : ℕ) (mpos : m > 0) (primep : prime p) : mult p (m^n) = n * mult p m := +theorem mult_pow {p m : ℕ} (n : ℕ) (mpos : m > 0) (primep : prime p) : + mult p (m^n) = n * mult p m := begin induction n with n ih, krewrite [pow_zero, mult_one_right, zero_mul], @@ -250,7 +251,8 @@ begin {rewrite [pow_zero, mult_one_right]}, have qpos : q > 0, from pos_of_prime primeq, have qipos : q^i > 0, from !pow_pos_of_pos qpos, - rewrite [pow_succ', mult_mul primep qipos qpos, ih, mult_eq_zero_of_prime_of_ne primep primeq pneq] + rewrite [pow_succ', mult_mul primep qipos qpos, ih, mult_eq_zero_of_prime_of_ne primep + primeq pneq] end theorem mult_prod_pow_of_not_mem {p : ℕ} (primep : prime p) {s : finset ℕ}