From 697df0e68cdd85443bdce626b40593e51fc66197 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 29 Oct 2015 15:36:26 -0400 Subject: [PATCH] refactor(library/*): use type classes for div and mod --- library/algebra/field.lean | 8 +- library/data/encodable.lean | 14 +- library/data/equiv.lean | 6 +- library/data/fin.lean | 16 +- library/data/finset/equiv.lean | 69 +-- library/data/int/div.lean | 500 +++++++++--------- library/data/int/gcd.lean | 74 +-- library/data/nat/div.lean | 472 ++++++++--------- library/data/nat/examples/partial_sum.lean | 4 +- library/data/nat/gcd.lean | 108 ++-- library/data/nat/parity.lean | 37 +- library/data/nat/power.lean | 10 +- library/data/rat/basic.lean | 18 +- library/data/real/division.lean | 23 +- library/init/reserved_notation.lean | 77 ++- library/theories/combinatorics/choose.lean | 2 +- library/theories/group_theory/cyclic.lean | 38 +- library/theories/group_theory/pgroup.lean | 15 +- library/theories/number_theory/bezout.lean | 18 +- .../number_theory/irrational_roots.lean | 66 +-- .../number_theory/prime_factorization.lean | 24 +- library/theories/number_theory/primes.lean | 2 +- tests/lean/local_notation_bug2.lean | 4 +- .../local_notation_bug2.lean.expected.out | 2 +- tests/lean/noncomp_theory.lean.expected.out | 4 +- tests/lean/run/occurs_check_bug1.lean | 2 +- tests/lean/struct_class.lean.expected.out | 10 +- 27 files changed, 809 insertions(+), 814 deletions(-) diff --git a/library/algebra/field.lean b/library/algebra/field.lean index 7f842a2c0..69729d157 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -14,20 +14,18 @@ namespace algebra variable {A : Type} --- in division rings, 1 / 0 = 0 structure division_ring [class] (A : Type) extends ring A, has_inv A, zero_ne_one_class A := (mul_inv_cancel : ∀{a}, a ≠ zero → mul a (inv a) = one) (inv_mul_cancel : ∀{a}, a ≠ zero → mul (inv a) a = one) - --(inv_zero : inv zero = zero) section division_ring variables [s : division_ring A] {a b c : A} include s - protected definition division (a b : A) : A := a * b⁻¹ + protected definition div (a b : A) : A := a * b⁻¹ - definition division_ring_has_division [reducible] [instance] : has_division A := - has_division.mk algebra.division + definition division_ring_has_div [reducible] [instance] : has_div A := + has_div.mk algebra.div lemma division.def (a b : A) : a / b = a * b⁻¹ := rfl diff --git a/library/data/encodable.lean b/library/data/encodable.lean index 6ae21c5d5..319fba650 100644 --- a/library/data/encodable.lean +++ b/library/data/encodable.lean @@ -6,7 +6,7 @@ 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 +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 @@ -23,7 +23,7 @@ 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] : +definition encodable_fintype [instance] {A : Type} [h₁ : fintype A] [h₂ : decidable_eq A] : encodable A := encodable.mk (λ a, find a (elements_of A)) @@ -57,13 +57,13 @@ private definition encode_sum : sum A B → nat | (sum.inr b) := 2 * encode b + 1 private definition decode_sum (n : nat) : option (sum A B) := -if n mod 2 = 0 then - match decode A (n div 2) with +if n % 2 = 0 then + match decode A (n / 2) with | some a := some (sum.inl a) | none := none end else - match decode B ((n - 1) div 2) with + match decode B ((n - 1) / 2) with | some b := some (sum.inr b) | none := none end @@ -74,12 +74,12 @@ 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)), nat.mul_div_cancel_left _ aux, + 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, - assert aux₂ : 1 mod 2 = (1:nat), by rewrite [nat.modulo_def], + assert aux₂ : 1 % 2 = (1:nat), by rewrite [nat.mod_def], assert aux₃ : 1 ≠ (0:nat), from dec_trivial, begin esimp [encode_sum, decode_sum], diff --git a/library/data/equiv.lean b/library/data/equiv.lean index b4c5ff1dc..42829f6ca 100644 --- a/library/data/equiv.lean +++ b/library/data/equiv.lean @@ -263,16 +263,16 @@ calc (nat + bool) ≃ (nat + (unit + unit)) : sum_congr !equiv.refl bool_equiv_u open decidable definition nat_sum_nat_equiv_nat [simp] : (nat + nat) ≃ nat := mk (λ s, match s with inl n := 2*n | inr n := 2*n+1 end) - (λ n, if even n then inl (n div 2) else inr ((n - 1) div 2)) + (λ n, if even n then inl (n / 2) else inr ((n - 1) / 2)) (λ s, begin have two_gt_0 : 2 > zero, from dec_trivial, cases s, {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, + {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, + (λ h : even n, by rewrite [if_pos h]; esimp; rewrite [nat.mul_div_cancel' (dvd_of_even h)]) (λ h : ¬ even n, begin diff --git a/library/data/fin.lean b/library/data/fin.lean index 9a72d7ed9..b64a1772f 100644 --- a/library/data/fin.lean +++ b/library/data/fin.lean @@ -95,7 +95,7 @@ has_zero.mk (fin.zero n) theorem val_zero (n : nat) : val (0 : fin (succ n)) = 0 := rfl definition mk_mod [reducible] (n i : nat) : fin (succ n) := -mk (i mod (succ n)) (mod_lt _ !zero_lt_succ) +mk (i % (succ n)) (mod_lt _ !zero_lt_succ) theorem mk_mod_zero_eq (n : nat) : mk_mod n 0 = 0 := rfl @@ -218,12 +218,12 @@ end lift_lower section madd definition madd (i j : fin (succ n)) : fin (succ n) := -mk ((i + j) mod (succ n)) (mod_lt _ !zero_lt_succ) +mk ((i + j) % (succ n)) (mod_lt _ !zero_lt_succ) definition minv : ∀ i : fin (succ n), fin (succ n) -| (mk iv ilt) := mk ((succ n - iv) mod succ n) (mod_lt _ !zero_lt_succ) +| (mk iv ilt) := mk ((succ n - iv) % succ n) (mod_lt _ !zero_lt_succ) -lemma val_madd : ∀ i j : fin (succ n), val (madd i j) = (i + j) mod (succ n) +lemma val_madd : ∀ i j : fin (succ n), val (madd i j) = (i + j) % (succ n) | (mk iv ilt) (mk jv jlt) := by esimp lemma madd_inj : ∀ {i : fin (succ n)}, injective (madd i) @@ -238,7 +238,7 @@ end)) lemma madd_mk_mod {i j : nat} : madd (mk_mod n i) (mk_mod n j) = mk_mod n (i+j) := eq_of_veq begin esimp [madd, mk_mod], rewrite [ mod_add_mod, add_mod_mod ] end -lemma val_mod : ∀ i : fin (succ n), (val i) mod (succ n) = val i +lemma val_mod : ∀ i : fin (succ n), (val i) % (succ n) = val i | (mk iv ilt) := by esimp; rewrite [(mod_eq_of_lt ilt)] lemma madd_comm (i j : fin (succ n)) : madd i j = madd j i := @@ -450,13 +450,13 @@ assert aux₁ : ∀ {v₁ v₂}, v₁ < n → v₂ < m → v₁ + v₂ * n < n*m assert v₁ + (v₂ * n + n) < n + n * m, from add_lt_add_of_lt_of_le h₁ this, have v₁ + v₂ * n + n < n * m + n, by rewrite [add.assoc, add.comm (n*m) n]; exact this, lt_of_add_lt_add_right this, -assert aux₂ : ∀ v, v mod n < n, from +assert aux₂ : ∀ v, v % n < n, from take v, mod_lt _ `n > 0`, -assert aux₃ : ∀ {v}, v < n * m → v div n < m, from +assert aux₃ : ∀ {v}, v < n * m → v / n < m, from 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, + inv_fun := λ f : fin (n*m), match f with (mk v hlt) := (mk (v % n) (aux₂ v), mk (v / n) (aux₃ hlt)) end, left_inv := begin intro p, cases p with f₁ f₂, cases f₁ with v₁ hlt₁, cases f₂ with v₂ hlt₂, esimp, congruence, diff --git a/library/data/finset/equiv.lean b/library/data/finset/equiv.lean index 620d7074c..107a30f93 100644 --- a/library/data/finset/equiv.lean +++ b/library/data/finset/equiv.lean @@ -22,22 +22,22 @@ lemma to_nat_insert {n : nat} {s : finset nat} : n ∉ s → to_nat (insert n s) assume h, Sum_insert_of_not_mem _ h protected definition of_nat (s : nat) : finset nat := -{ n ∈ upto (succ s) | odd (s div 2^n) } +{ n ∈ upto (succ s) | odd (s / 2^n) } open finset (of_nat) private lemma of_nat_zero : of_nat 0 = ∅ := rfl -private lemma odd_of_mem_of_nat {n : nat} {s : nat} : n ∈ of_nat s → odd (s div 2^n) := +private lemma odd_of_mem_of_nat {n : nat} {s : nat} : n ∈ of_nat s → odd (s / 2^n) := assume h, of_mem_sep h -private lemma mem_of_nat_of_odd {n : nat} {s : nat} : odd (s div 2^n) → n ∈ of_nat s := +private lemma mem_of_nat_of_odd {n : nat} {s : nat} : odd (s / 2^n) → n ∈ of_nat s := assume h, have 2^n < succ s, from by_contradiction (suppose ¬(2^n < succ s), assert 2^n > s, from lt_of_succ_le (le_of_not_gt this), - assert s div 2^n = 0, from div_eq_zero_of_lt this, + assert s / 2^n = 0, from div_eq_zero_of_lt this, by rewrite this at h; exact absurd h dec_trivial), have n < succ s, from calc n ≤ 2^n : le_pow_self dec_trivial n @@ -45,15 +45,15 @@ have n < succ s, from calc have n ∈ upto (succ s), from mem_upto_of_lt this, mem_sep_of_mem this h -private lemma succ_mem_of_nat (n : nat) (s : nat) : succ n ∈ of_nat s ↔ n ∈ of_nat (s div 2) := +private lemma succ_mem_of_nat (n : nat) (s : nat) : succ n ∈ of_nat s ↔ n ∈ of_nat (s / 2) := 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, 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, -nat.div_div_eq_div_mul]; assumption, + assert odd (s / 2^(succ n)), from odd_of_mem_of_nat this, + have odd ((s / 2) / (2 ^ n)), by rewrite [pow_succ' at this, nat.div_div_eq_div_mul, mul.comm]; assumption, + show n ∈ of_nat (s / 2), from mem_of_nat_of_odd this) + (suppose n ∈ of_nat (s / 2), + assert odd ((s / 2) / (2 ^ n)), from odd_of_mem_of_nat this, + assert odd (s / 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 := @@ -123,12 +123,12 @@ begin match n with | 0 := iff.intro (λ h, !mem_insert) (λ h, by rewrite [hw at zmem]; exact zmem) | succ m := - assert d₁ : 1 div 2 = (0:nat), from dec_trivial, + assert d₁ : 1 / 2 = (0:nat), from dec_trivial, 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, nat.mul_div_cancel _ (dec_trivial : 2 > 0)] - ... ↔ succ m ∈ of_nat (2*w) : succ_mem_of_nat, + succ m ∈ of_nat (2 * w + 1) ↔ m ∈ of_nat ((2*w+1) / 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 / 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)) (λ hr, or.elim (eq_or_mem_of_mem_insert hr) @@ -140,8 +140,9 @@ end private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n + s) = insert n (of_nat s) | 0 s h := of_nat_eq_insert_zero h | (succ n) s h := - have n ∉ of_nat (s div 2), from iff.mp (not_iff_not_of_iff !succ_mem_of_nat) h, - assert ih : of_nat (2^n + s div 2) = insert n (of_nat (s div 2)), from of_nat_eq_insert this, + have n ∉ of_nat (s / 2), + from iff.mp (not_iff_not_of_iff !succ_mem_of_nat) h, + assert ih : of_nat (2^n + s / 2) = insert n (of_nat (s / 2)), from of_nat_eq_insert this, finset.ext (λ x, have gen : ∀ m, m ∈ of_nat (2^(succ n) + s) ↔ m ∈ insert (succ n) (of_nat s) | zero := @@ -163,10 +164,10 @@ private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n ... ↔ odd s : aux₁ ... ↔ 0 ∈ insert (succ n) (of_nat s) : aux₂ | (succ m) := - assert aux : m ∈ insert n (of_nat (s div 2)) ↔ succ m ∈ insert (succ n) (of_nat s), from iff.intro + assert aux : m ∈ insert n (of_nat (s / 2)) ↔ succ m ∈ insert (succ n) (of_nat s), from iff.intro (assume hl, or.elim (eq_or_mem_of_mem_insert hl) (suppose m = n, by subst m; apply mem_insert) - (suppose m ∈ of_nat (s div 2), finset.mem_insert_of_mem _ (iff.mpr !succ_mem_of_nat this))) + (suppose m ∈ of_nat (s / 2), finset.mem_insert_of_mem _ (iff.mpr !succ_mem_of_nat this))) (assume hr, or.elim (eq_or_mem_of_mem_insert hr) (suppose succ m = succ n, assert m = n, by injection this; assumption, @@ -174,9 +175,9 @@ private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n (suppose succ m ∈ of_nat s, finset.mem_insert_of_mem _ (iff.mp !succ_mem_of_nat this))), calc succ m ∈ of_nat (2^(succ n) + s) ↔ succ m ∈ of_nat (2^n * 2 + s) : by rewrite pow_succ' - ... ↔ m ∈ of_nat ((2^n * 2 + s) div 2) : succ_mem_of_nat - ... ↔ m ∈ of_nat (2^n + s div 2) : by rewrite [add.comm, add_mul_div_self (dec_trivial : 2 > 0), add.comm] - ... ↔ m ∈ insert n (of_nat (s div 2)) : by rewrite ih + ... ↔ m ∈ of_nat ((2^n * 2 + s) / 2) : succ_mem_of_nat + ... ↔ m ∈ of_nat (2^n + s / 2) : by rewrite [add.comm, add_mul_div_self (dec_trivial : 2 > 0), add.comm] + ... ↔ m ∈ insert n (of_nat (s / 2)) : by rewrite ih ... ↔ succ m ∈ insert (succ n) (of_nat s) : aux, gen x) @@ -233,16 +234,16 @@ finset.ext (λ m, and.intro (or.inr h₁) (or.inr h₂)) end) -private lemma of_nat_div2 (s : nat) : of_nat (s div 2) = predimage (of_nat s) := +private lemma of_nat_div2 (s : nat) : of_nat (s / 2) = predimage (of_nat s) := finset.ext (λ n, iff.intro - (suppose n ∈ of_nat (s div 2), + (suppose n ∈ of_nat (s / 2), have succ n ∈ of_nat s, from iff.mpr !succ_mem_of_nat this, mem_predimage_of_succ_mem this) (suppose n ∈ predimage (of_nat s), have succ n ∈ of_nat s, from succ_mem_of_mem_predimage this, iff.mp !succ_mem_of_nat this)) -private lemma to_nat_predimage (s : finset nat) : to_nat (predimage s) = (to_nat s) div 2 := +private lemma to_nat_predimage (s : finset nat) : to_nat (predimage s) = (to_nat s) / 2 := begin induction s with a s nains ih, reflexivity, @@ -253,8 +254,8 @@ begin obtain (w : nat) (hw : to_nat s = 2*w), from exists_of_even this, begin rewrite hw, - have d₁ : 1 div 2 = (0:nat), from dec_trivial, - show 2 * w div 2 = (1 + 2 * w) div 2, by + have d₁ : 1 / 2 = (0:nat), from dec_trivial, + show 2 * w / 2 = (1 + 2 * w) / 2, by rewrite [add_mul_div_self_left _ _ (dec_trivial : 2 > 0), mul.comm, nat.mul_div_cancel _ (dec_trivial : 2 > 0), d₁, zero_add] end }, @@ -268,12 +269,12 @@ nat.strong_induction_on s (λ n ih, by_cases (suppose n = 0, by rewrite this) (suppose n ≠ 0, - have n div 2 < n, from div_lt_of_ne_zero this, - have to_nat (of_nat (n div 2)) = n div 2, from ih _ this, - have e₁ : to_nat (of_nat n) div 2 = n div 2, from calc - to_nat (of_nat n) div 2 = to_nat (predimage (of_nat n)) : by rewrite to_nat_predimage - ... = to_nat (of_nat (n div 2)) : by rewrite of_nat_div2 - ... = n div 2 : this, + have n / 2 < n, from div_lt_of_ne_zero this, + have to_nat (of_nat (n / 2)) = n / 2, from ih _ this, + have e₁ : to_nat (of_nat n) / 2 = n / 2, from calc + to_nat (of_nat n) / 2 = to_nat (predimage (of_nat n)) : by rewrite to_nat_predimage + ... = to_nat (of_nat (n / 2)) : by rewrite of_nat_div2 + ... = n / 2 : this, have e₂ : even (to_nat (of_nat n)) ↔ even n, from calc even (to_nat (of_nat n)) ↔ 0 ∉ of_nat n : even_to_nat ... ↔ even n : even_of_not_zero_mem, diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 32f6c9d17..f7185ec7b 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -5,7 +5,7 @@ Author: Jeremy Avigad Definitions and properties of div and mod, following the SSReflect library. -Following SSReflect and the SMTlib standard, we define a mod b so that 0 ≤ a mod b < |b| when b ≠ 0. +Following SSReflect and the SMTlib standard, we define a % b so that 0 ≤ a % b < |b| when b ≠ 0. -/ import data.int.order data.nat.div open [coercions] [reduce_hints] nat @@ -17,110 +17,110 @@ namespace int /- definitions -/ -protected definition divide (a b : ℤ) : ℤ := +protected definition div (a b : ℤ) : ℤ := sign b * (match a with - | of_nat m := of_nat (m div (nat_abs b)) - | -[1+m] := -[1+ ((m:nat) div (nat_abs b))] + | of_nat m := of_nat (m / (nat_abs b)) + | -[1+m] := -[1+ ((m:nat) / (nat_abs b))] end) -definition int_has_divide [reducible] [instance] [priority int.prio] : has_divide int := -has_divide.mk int.divide +definition int_has_div [reducible] [instance] [priority int.prio] : has_div int := +has_div.mk int.div -lemma of_nat_div_eq (m : nat) (b : ℤ) : (of_nat m) div b = sign b * of_nat (m div (nat_abs b)) := +lemma of_nat_div_eq (m : nat) (b : ℤ) : (of_nat m) / b = sign b * of_nat (m / (nat_abs b)) := rfl -lemma neg_succ_div_eq (m: nat) (b : ℤ) : -[1+m] div b = sign b * -[1+ (m div (nat_abs b))] := +lemma neg_succ_div_eq (m: nat) (b : ℤ) : -[1+m] / b = sign b * -[1+ (m / (nat_abs b))] := rfl -lemma divide.def (a b : ℤ) : a div b = +lemma div_def (a b : ℤ) : a / b = sign b * (match a with - | of_nat m := of_nat (m div (nat_abs b)) - | -[1+m] := -[1+ ((m:nat) div (nat_abs b))] + | of_nat m := of_nat (m / (nat_abs b)) + | -[1+m] := -[1+ ((m:nat) / (nat_abs b))] end) := rfl -protected definition modulo (a b : ℤ) : ℤ := a - a div b * b +protected definition mod (a b : ℤ) : ℤ := a - a / b * b -definition int_has_modulo [reducible] [instance] [priority int.prio] : has_modulo int := -has_modulo.mk int.modulo +definition int_has_mod [reducible] [instance] [priority int.prio] : has_mod int := +has_mod.mk int.mod -lemma modulo.def (a b : ℤ) : a mod b = a - a div b * b := +lemma mod_def (a b : ℤ) : a % b = a - a / b * b := rfl -notation [priority int.prio] a ≡ b `[mod `:0 c:0 `]` := a mod c = b mod c +notation [priority int.prio] a ≡ b `[mod `:0 c:0 `]` := a % c = b % c -/- div -/ +/- / -/ -theorem of_nat_div (m n : nat) : of_nat (m div n) = (of_nat m) div (of_nat n) := +theorem of_nat_div (m n : nat) : of_nat (m / n) = (of_nat m) / (of_nat n) := nat.cases_on n (begin rewrite [of_nat_div_eq, of_nat_zero, sign_zero, zero_mul, nat.div_zero] end) (take (n : nat), by rewrite [of_nat_div_eq, sign_of_succ, one_mul]) theorem neg_succ_of_nat_div (m : nat) {b : ℤ} (H : b > 0) : - -[1+m] div b = -(m div b + 1) := + -[1+m] / b = -(m / b + 1) := calc - -[1+m] div b = sign b * _ : rfl - ... = -[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] + -[1+m] / b = sign b * _ : rfl + ... = -[1+(m / (nat_abs b))] : by rewrite [sign_of_pos H, one_mul] + ... = -(m / b + 1) : by rewrite [of_nat_div_eq, sign_of_pos H, one_mul] -protected theorem div_neg (a b : ℤ) : a div -b = -(a div b) := +protected theorem div_neg (a b : ℤ) : a / -b = -(a / b) := begin induction a, - rewrite [*of_nat_div_eq, sign_neg, neg_mul_eq_neg_mul, nat_abs_neg], + rewrite [*of_nat_div_eq, sign_neg, neg_mul_eq_neg_mul, nat_abs_neg], rewrite [*neg_succ_div_eq, sign_neg, neg_mul_eq_neg_mul, nat_abs_neg], end -theorem div_of_neg_of_pos {a b : ℤ} (Ha : a < 0) (Hb : b > 0) : a div b = -((-a - 1) div b + 1) := +theorem div_of_neg_of_pos {a b : ℤ} (Ha : a < 0) (Hb : b > 0) : a / b = -((-a - 1) / b + 1) := obtain (m : nat) (H1 : a = -[1+m]), from exists_eq_neg_succ_of_nat Ha, calc - a div b = -(m div b + 1) : by rewrite [H1, neg_succ_of_nat_div _ Hb] - ... = -((-a -1) div b + 1) : by rewrite [H1, neg_succ_of_nat_eq', neg_sub, sub_neg_eq_add, + a / b = -(m / b + 1) : by rewrite [H1, neg_succ_of_nat_div _ Hb] + ... = -((-a -1) / b + 1) : by rewrite [H1, neg_succ_of_nat_eq', neg_sub, sub_neg_eq_add, add.comm 1, add_sub_cancel] -protected 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 / 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] + a / b = m / n : by rewrite [Hm, Hn] ... ≥ 0 : by rewrite -of_nat_div; apply trivial -protected 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 / b ≤ 0 := calc - 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)) + a / b = -(a / -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 := +theorem div_neg' {a b : ℤ} (Ha : a < 0) (Hb : b > 0) : a / 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 (int.div_nonneg this (le_of_lt Hb)), +have (-a - 1) / 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 + a / b = -((-a - 1) / b + 1) : div_of_neg_of_pos Ha Hb + ... < 0 : neg_neg_of_pos this -protected theorem zero_div (b : ℤ) : 0 div b = 0 := +protected theorem zero_div (b : ℤ) : 0 / b = 0 := by rewrite [of_nat_div_eq, nat.zero_div, of_nat_zero, mul_zero] -protected theorem div_zero (a : ℤ) : a div 0 = 0 := -by rewrite [divide.def, sign_zero, zero_mul] +protected theorem div_zero (a : ℤ) : a / 0 = 0 := +by rewrite [div_def, sign_zero, zero_mul] -protected theorem div_one (a : ℤ) : a div 1 = a := +protected theorem div_one (a : ℤ) : a / 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]) (take m : nat, by rewrite [!neg_succ_of_nat_div this, -of_nat_one, -of_nat_div, nat.div_one]) -theorem eq_div_mul_add_mod (a b : ℤ) : a = a div b * b + a mod b := +theorem eq_div_mul_add_mod (a b : ℤ) : a = a / b * b + a % b := !add.comm ▸ eq_add_of_sub_eq rfl -theorem div_eq_zero_of_lt {a b : ℤ} : 0 ≤ a → a < b → a div b = 0 := +theorem div_eq_zero_of_lt {a b : ℤ} : 0 ≤ a → a < b → a / b = 0 := int.cases_on a (take (m : nat), assume H, int.cases_on b (take (n : nat), assume H : m < n, - show m div n = 0, + show m / n = 0, by rewrite [-of_nat_div, nat.div_eq_zero_of_lt (lt_of_of_nat_lt_of_nat H)]) (take (n : nat), assume H : m < -[1+n], @@ -131,20 +131,20 @@ int.cases_on a have ¬ (0 ≤ -[1+m]), from dec_trivial, absurd H this) -theorem div_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < abs b) : a div b = 0 := +theorem div_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < abs b) : a / b = 0 := lt.by_cases (suppose b < 0, assert a < -b, from abs_of_neg this ▸ H2, calc - 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]) + a / b = - (a / -b) : by rewrite [int.div_neg, neg_neg] + ... = 0 : by rewrite [div_eq_zero_of_lt H1 this, neg_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) private theorem add_mul_div_self_aux1 {a : ℤ} {k : ℕ} (n : ℕ) (H1 : a ≥ 0) (H2 : k > 0) : - (a + n * k) div k = a div k + n := + (a + n * k) / k = a / k + n := obtain (m : nat) (Hm : a = of_nat m), from exists_eq_of_nat H1, begin subst Hm, @@ -152,156 +152,157 @@ begin end private theorem add_mul_div_self_aux2 {a : ℤ} {k : ℕ} (n : ℕ) (H1 : a < 0) (H2 : k > 0) : - (a + n * k) div k = a div k + n := + (a + n * k) / k = a / k + n := obtain m (Hm : a = -[1+m]), from exists_eq_neg_succ_of_nat H1, or.elim (nat.lt_or_ge m (n * k)) (assume m_lt_nk : m < n * k, assert H3 : m + 1 ≤ n * k, from nat.succ_le_of_lt m_lt_nk, - assert H4 : m div k + 1 ≤ n, + assert H4 : m / k + 1 ≤ n, from nat.succ_le_of_lt (nat.div_lt_of_lt_mul m_lt_nk), - have (-[1+m] + n * k) div k = -[1+m] div k + n, from calc - (-[1+m] + n * k) div k - = of_nat ((k * n - (m + 1)) div k) : + have (-[1+m] + n * k) / k = -[1+m] / k + n, from calc + (-[1+m] + n * k) / k + = of_nat ((k * n - (m + 1)) / k) : by rewrite [add.comm, neg_succ_of_nat_eq, of_nat_div, algebra.mul.comm k n, of_nat_sub H3] - ... = of_nat (n - m div k - 1) : + ... = of_nat (n - m / k - 1) : nat.mul_sub_div_of_lt (!nat.mul_comm ▸ m_lt_nk) - ... = -[1+m] div k + n : + ... = -[1+m] / k + n : by rewrite [nat.sub_sub, of_nat_sub H4, int.add_comm, sub_eq_add_neg, !neg_succ_of_nat_div (of_nat_lt_of_nat_of_lt H2), of_nat_add, of_nat_div], Hm⁻¹ ▸ this) (assume nk_le_m : n * k ≤ m, - have -[1+m] div k + n = (-[1+m] + n * k) div k, from calc - -[1+m] div k + n - = -(of_nat ((m - n * k + n * k) div k) + 1) + n : + have -[1+m] / k + n = (-[1+m] + n * k) / k, from calc + -[1+m] / k + n + = -(of_nat ((m - n * k + n * k) / k) + 1) + n : by rewrite [neg_succ_of_nat_div m (of_nat_lt_of_nat_of_lt H2), nat.sub_add_cancel nk_le_m, of_nat_div] - ... = -(of_nat ((m - n * k) div k + n) + 1) + n : nat.add_mul_div_self H2 - ... = -(of_nat (m - n * k) div k + 1) : + ... = -(of_nat ((m - n * k) / k + n) + 1) + n : nat.add_mul_div_self H2 + ... = -(of_nat (m - n * k) / k + 1) : by rewrite [of_nat_add, *neg_add, add.right_comm, neg_add_cancel_right, of_nat_div] - ... = -[1+(m - n * k)] div k : + ... = -[1+(m - n * k)] / k : neg_succ_of_nat_div _ (of_nat_lt_of_nat_of_lt H2) - ... = -(of_nat(m - n * k) + 1) div k : rfl - ... = -(of_nat m - of_nat(n * k) + 1) div k : of_nat_sub nk_le_m - ... = (-(of_nat m + 1) + n * k) div k : + ... = -(of_nat(m - n * k) + 1) / k : rfl + ... = -(of_nat m - of_nat(n * k) + 1) / k : of_nat_sub nk_le_m + ... = (-(of_nat m + 1) + n * k) / k : by rewrite [sub_eq_add_neg, -*add.assoc, *neg_add, neg_neg, add.right_comm] - ... = (-[1+m] + n * k) div k : rfl, + ... = (-[1+m] + n * k) / k : rfl, Hm⁻¹ ▸ this⁻¹) private theorem add_mul_div_self_aux3 (a : ℤ) {b c : ℤ} (H1 : b ≥ 0) (H2 : c > 0) : - (a + b * c) div c = a div c + b := + (a + b * c) / c = a / c + b := obtain (n : nat) (Hn : b = of_nat n), from exists_eq_of_nat H1, obtain (k : nat) (Hk : c = of_nat k), from exists_eq_of_nat (le_of_lt H2), have knz : k ≠ 0, from assume kz, !lt.irrefl (kz ▸ Hk ▸ H2), have kgt0 : (#nat k > 0), from nat.pos_of_ne_zero knz, -have H3 : (a + n * k) div k = a div k + n, from +have H3 : (a + n * k) / k = a / k + n, from or.elim (lt_or_ge a 0) (assume Ha : a < 0, add_mul_div_self_aux2 _ Ha kgt0) (assume Ha : a ≥ 0, add_mul_div_self_aux1 _ Ha kgt0), Hn⁻¹ ▸ Hk⁻¹ ▸ H3 private theorem add_mul_div_self_aux4 (a b : ℤ) {c : ℤ} (H : c > 0) : - (a + b * c) div c = a div c + b := + (a + b * c) / c = a / c + b := or.elim (le.total 0 b) (assume H1 : 0 ≤ b, add_mul_div_self_aux3 _ H1 H) (assume H1 : 0 ≥ b, eq.symm (calc - a div c + b = (a + b * c + -b * c) div c + b : + a / c + b = (a + b * c + -b * c) / c + b : by rewrite [-neg_mul_eq_neg_mul, add_neg_cancel_right] - ... = (a + b * c) div c + - b + b : + ... = (a + b * c) / c + - b + b : add_mul_div_self_aux3 _ (neg_nonneg_of_nonpos H1) H - ... = (a + b * c) div c : neg_add_cancel_right)) + ... = (a + b * c) / c : neg_add_cancel_right)) -protected 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) / c = a / 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 [int.div_neg, neg_mul_neg, neg_neg] - ... = -(a div -c + -b) : !add_mul_div_self_aux4 H2 - ... = a div c + b : by rewrite [int.div_neg, neg_add, *neg_neg]) + (a + b * c) / c = - ((a + -b * -c) / -c) : by rewrite [int.div_neg, neg_mul_neg, neg_neg] + ... = -(a / -c + -b) : !add_mul_div_self_aux4 H2 + ... = a / c + b : by rewrite [int.div_neg, neg_add, *neg_neg]) protected theorem add_mul_div_self_left (a : ℤ) {b : ℤ} (c : ℤ) (H : b ≠ 0) : - (a + b * c) div b = a div b + c := + (a + b * c) / b = a / b + c := !mul.comm ▸ !int.add_mul_div_self H -protected 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 / b = a := calc - 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] + a * b / b = (0 + a * b) / b : zero_add + ... = 0 / b + a : !int.add_mul_div_self H + ... = a : by rewrite [int.zero_div, zero_add] -protected theorem mul_div_cancel_left {a : ℤ} (b : ℤ) (H : a ≠ 0) : a * b div a = b := +protected theorem mul_div_cancel_left {a : ℤ} (b : ℤ) (H : a ≠ 0) : a * b / a = b := !mul.comm ▸ int.mul_div_cancel b H -protected theorem div_self {a : ℤ} (H : a ≠ 0) : a div a = 1 := +protected theorem div_self {a : ℤ} (H : a ≠ 0) : a / a = 1 := !mul_one ▸ !int.mul_div_cancel_left H /- mod -/ -theorem of_nat_mod (m n : nat) : m mod n = of_nat (m mod n) := -have H : m = of_nat (m mod n) + m div n * n, from calc - m = of_nat (m div n * n + m mod n) : nat.eq_div_mul_add_mod - ... = of_nat (m div n) * n + of_nat (m mod n) : rfl - ... = m div n * n + of_nat (m mod n) : of_nat_div - ... = of_nat (m mod n) + m div n * n : add.comm, +theorem of_nat_mod (m n : nat) : m % n = of_nat (m % n) := +have H : m = of_nat (m % n) + m / n * n, from calc + m = of_nat (m / n * n + m % n) : nat.eq_div_mul_add_mod + ... = of_nat (m / n) * n + of_nat (m % n) : rfl + ... = m / n * n + of_nat (m % n) : of_nat_div + ... = of_nat (m % n) + m / n * n : add.comm, calc - m mod n = m - m div n * n : rfl - ... = of_nat (m mod n) : sub_eq_of_eq_add H + m % n = m - m / n * n : rfl + ... = of_nat (m % n) : sub_eq_of_eq_add H theorem neg_succ_of_nat_mod (m : ℕ) {b : ℤ} (bpos : b > 0) : - -[1+m] mod b = b - 1 - m mod b := + -[1+m] % b = b - 1 - m % b := calc - -[1+m] mod b = -(m + 1) - -[1+m] div b * b : rfl - ... = -(m + 1) - -(m div b + 1) * b : neg_succ_of_nat_div _ bpos - ... = -m + -1 + (b + m div b * b) : + -[1+m] % b = -(m + 1) - -[1+m] / b * b : rfl + ... = -(m + 1) - -(m / b + 1) * b : neg_succ_of_nat_div _ bpos + ... = -m + -1 + (b + m / b * b) : by rewrite [neg_add, -neg_mul_eq_neg_mul, sub_neg_eq_add, right_distrib, one_mul, (add.comm b)] - ... = b + -1 + (-m + m div b * b) : + ... = b + -1 + (-m + m / b * b) : by rewrite [-*add.assoc, add.comm (-m), add.right_comm (-1), (add.comm b)] - ... = b - 1 - m mod b : - by rewrite [(modulo.def), *sub_eq_add_neg, neg_add, neg_neg] + ... = b - 1 - m % b : + by rewrite [(mod_def), *sub_eq_add_neg, neg_add, neg_neg] + -- it seems the parser has difficulty here, because "mod" is a token? -theorem mod_neg (a b : ℤ) : a mod -b = a mod b := +theorem mod_neg (a b : ℤ) : a % -b = a % b := calc - a mod -b = a - (a div -b) * -b : rfl - ... = a - -(a div b) * -b : int.div_neg - ... = a - a div b * b : neg_mul_neg - ... = a mod b : rfl + a % -b = a - (a / -b) * -b : rfl + ... = a - -(a / b) * -b : int.div_neg + ... = a - a / b * b : neg_mul_neg + ... = a % b : rfl -theorem mod_abs (a b : ℤ) : a mod (abs b) = a mod b := +theorem mod_abs (a b : ℤ) : a % (abs b) = a % b := abs.by_cases rfl !mod_neg -theorem zero_mod (b : ℤ) : 0 mod b = 0 := -by rewrite [(modulo.def), int.zero_div, zero_mul, sub_zero] +theorem zero_mod (b : ℤ) : 0 % b = 0 := +by rewrite [(mod_def), int.zero_div, zero_mul, sub_zero] -theorem mod_zero (a : ℤ) : a mod 0 = a := -by rewrite [(modulo.def), mul_zero, sub_zero] +theorem mod_zero (a : ℤ) : a % 0 = a := +by rewrite [(mod_def), mul_zero, sub_zero] -theorem mod_one (a : ℤ) : a mod 1 = 0 := +theorem mod_one (a : ℤ) : a % 1 = 0 := calc - a mod 1 = a - a div 1 * 1 : rfl + a % 1 = a - a / 1 * 1 : rfl ... = 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)) := +private lemma of_nat_mod_abs (m : ℕ) (b : ℤ) : m % (abs b) = of_nat (m % (nat_abs b)) := calc - m mod (abs b) = m mod (nat_abs b) : of_nat_nat_abs - ... = of_nat (m mod (nat_abs b)) : of_nat_mod + m % (abs b) = m % (nat_abs b) : of_nat_nat_abs + ... = of_nat (m % (nat_abs b)) : of_nat_mod -private lemma of_nat_mod_abs_lt (m : ℕ) {b : ℤ} (H : b ≠ 0) : m mod (abs b) < (abs b) := +private lemma of_nat_mod_abs_lt (m : ℕ) {b : ℤ} (H : b ≠ 0) : m % (abs b) < (abs b) := have H1 : abs b > 0, from abs_pos_of_ne_zero H, have H2 : (#nat nat_abs b > 0), from lt_of_of_nat_lt_of_nat (!of_nat_nat_abs⁻¹ ▸ H1), calc - m mod (abs b) = of_nat (m mod (nat_abs b)) : of_nat_mod_abs m b + m % (abs b) = of_nat (m % (nat_abs b)) : of_nat_mod_abs m b ... < nat_abs b : of_nat_lt_of_nat_of_lt (!nat.mod_lt H2) ... = abs b : of_nat_nat_abs _ -theorem mod_eq_of_lt {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < b) : a mod b = a := +theorem mod_eq_of_lt {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < b) : a % b = a := obtain (m : nat) (Hm : a = of_nat m), from exists_eq_of_nat H1, obtain (n : nat) (Hn : b = of_nat n), from exists_eq_of_nat (le_of_lt (lt_of_le_of_lt H1 H2)), begin @@ -310,181 +311,180 @@ begin apply nat.mod_eq_of_lt end -theorem mod_nonneg (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b ≥ 0 := +theorem mod_nonneg (a : ℤ) {b : ℤ} (H : b ≠ 0) : a % b ≥ 0 := have H1 : abs b > 0, from abs_pos_of_ne_zero H, -have H2 : a mod (abs b) ≥ 0, from +have H2 : a % (abs b) ≥ 0, from int.cases_on a - (take m : nat, (of_nat_mod_abs m b)⁻¹ ▸ of_nat_nonneg (nat.modulo m (nat_abs b))) + (take m : nat, (of_nat_mod_abs m b)⁻¹ ▸ of_nat_nonneg (nat.mod m (nat_abs b))) (take m : nat, - have H3 : 1 + m mod (abs b) ≤ (abs b), + have H3 : 1 + m % (abs b) ≤ (abs b), from (!add.comm ▸ add_one_le_of_lt (of_nat_mod_abs_lt m H)), calc - -[1+m] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1 - ... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc] - ... ≥ 0 : iff.mpr !sub_nonneg_iff_le H3), + -[1+m] % (abs b) = abs b - 1 - m % (abs b) : neg_succ_of_nat_mod _ H1 + ... = abs b - (1 + m % (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc] + ... ≥ 0 : iff.mpr !sub_nonneg_iff_le H3), !mod_abs ▸ H2 -theorem mod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) : a mod b < (abs b) := +theorem mod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) : a % b < (abs b) := have H1 : abs b > 0, from abs_pos_of_ne_zero H, -have H2 : a mod (abs b) < abs b, from +have H2 : a % (abs b) < abs b, from int.cases_on a (take m, of_nat_mod_abs_lt m H) (take m : nat, have H3 : abs b ≠ 0, from assume H', H (eq_zero_of_abs_eq_zero H'), - have H4 : 1 + m mod (abs b) > 0, + have H4 : 1 + m % (abs b) > 0, from add_pos_of_pos_of_nonneg dec_trivial (mod_nonneg _ H3), calc - -[1+m] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1 - ... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc] + -[1+m] % (abs b) = abs b - 1 - m % (abs b) : neg_succ_of_nat_mod _ H1 + ... = abs b - (1 + m % (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc] ... < abs b : sub_lt_self _ H4), !mod_abs ▸ H2 -theorem add_mul_mod_self {a b c : ℤ} : (a + b * c) mod c = a mod c := +theorem add_mul_mod_self {a b c : ℤ} : (a + b * c) % c = a % c := decidable.by_cases (assume cz : c = 0, by rewrite [cz, mul_zero, add_zero]) - (assume cnz, by rewrite [(modulo.def), !int.add_mul_div_self cnz, right_distrib, + (assume cnz, by rewrite [(mod_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 := +theorem add_mul_mod_self_left (a b c : ℤ) : (a + b * c) % b = a % b := !mul.comm ▸ !add_mul_mod_self -theorem add_mod_self {a b : ℤ} : (a + b) mod b = a mod b := +theorem add_mod_self {a b : ℤ} : (a + b) % b = a % b := by rewrite -(int.mul_one b) at {1}; apply add_mul_mod_self_left -theorem add_mod_self_left {a b : ℤ} : (a + b) mod a = b mod a := +theorem add_mod_self_left {a b : ℤ} : (a + b) % a = b % a := !add.comm ▸ !add_mod_self -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] +theorem mod_add_mod (m n k : ℤ) : (m % n + k) % n = (m + k) % n := +by rewrite [eq_div_mul_add_mod m n at {2}, add.assoc, add.comm (m / n * n), add_mul_mod_self] -theorem add_mod_mod (m n k : ℤ) : (m + n mod k) mod k = (m + n) mod k := +theorem add_mod_mod (m n k : ℤ) : (m + n % k) % k = (m + n) % k := by rewrite [add.comm, mod_add_mod, add.comm] -theorem add_mod_eq_add_mod_right {m n k : ℤ} (i : ℤ) (H : m mod n = k mod n) : - (m + i) mod n = (k + i) mod n := +theorem add_mod_eq_add_mod_right {m n k : ℤ} (i : ℤ) (H : m % n = k % n) : + (m + i) % n = (k + i) % n := by rewrite [-mod_add_mod, -mod_add_mod k, H] -theorem add_mod_eq_add_mod_left {m n k : ℤ} (i : ℤ) (H : m mod n = k mod n) : - (i + m) mod n = (i + k) mod n := +theorem add_mod_eq_add_mod_left {m n k : ℤ} (i : ℤ) (H : m % n = k % n) : + (i + m) % n = (i + k) % n := by rewrite [add.comm, add_mod_eq_add_mod_right _ H, add.comm] theorem mod_eq_mod_of_add_mod_eq_add_mod_right {m n k i : ℤ} - (H : (m + i) mod n = (k + i) mod n) : - m mod n = k mod n := -assert H1 : (m + i + (-i)) mod n = (k + i + (-i)) mod n, from add_mod_eq_add_mod_right _ H, + (H : (m + i) % n = (k + i) % n) : + m % n = k % n := +assert H1 : (m + i + (-i)) % n = (k + i + (-i)) % n, from add_mod_eq_add_mod_right _ H, by rewrite [*add_neg_cancel_right at H1]; apply H1 theorem mod_eq_mod_of_add_mod_eq_add_mod_left {m n k i : ℤ} : - (i + m) mod n = (i + k) mod n → m mod n = k mod n := + (i + m) % n = (i + k) % n → m % n = k % n := by rewrite [add.comm i m, add.comm i k]; apply mod_eq_mod_of_add_mod_eq_add_mod_right -theorem mul_mod_left (a b : ℤ) : (a * b) mod b = 0 := +theorem mul_mod_left (a b : ℤ) : (a * b) % b = 0 := by rewrite [-zero_add (a * b), add_mul_mod_self, zero_mod] -theorem mul_mod_right (a b : ℤ) : (a * b) mod a = 0 := +theorem mul_mod_right (a b : ℤ) : (a * b) % a = 0 := !mul.comm ▸ !mul_mod_left -theorem mod_self {a : ℤ} : a mod a = 0 := +theorem mod_self {a : ℤ} : a % a = 0 := decidable.by_cases (assume H : a = 0, H⁻¹ ▸ !mod_zero) (assume H : a ≠ 0, calc - a mod a = a - a div a * a : rfl + a % a = a - a / a * a : rfl ... = 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 := +theorem mod_lt_of_pos (a : ℤ) {b : ℤ} (H : b > 0) : a % b < b := !abs_of_pos H ▸ !mod_lt (ne.symm (ne_of_lt H)) -/- properties of div and mod -/ +/- properties of / and % -/ theorem mul_div_mul_of_pos_aux {a : ℤ} (b : ℤ) {c : ℤ} - (H1 : a > 0) (H2 : c > 0) : a * b div (a * c) = b div c := + (H1 : a > 0) (H2 : c > 0) : a * b / (a * c) = b / c := have H3 : a * c ≠ 0, from ne.symm (ne_of_lt (mul_pos H1 H2)), -have H4 : a * (b mod c) < a * c, from mul_lt_mul_of_pos_left (!mod_lt_of_pos H2) H1, -have H5 : a * (b mod c) ≥ 0, from mul_nonneg (le_of_lt H1) (!mod_nonneg (ne.symm (ne_of_lt H2))), +have H4 : a * (b % c) < a * c, from mul_lt_mul_of_pos_left (!mod_lt_of_pos H2) H1, +have H5 : a * (b % c) ≥ 0, from mul_nonneg (le_of_lt H1) (!mod_nonneg (ne.symm (ne_of_lt H2))), calc - a * b div (a * c) = a * (b div c * c + b mod c) div (a * c) : eq_div_mul_add_mod + a * b / (a * c) = a * (b / c * c + b % c) / (a * c) : eq_div_mul_add_mod - ... = (a * (b mod c) + a * c * (b div c)) div (a * c) : + ... = (a * (b % c) + a * c * (b / c)) / (a * c) : by rewrite [!add.comm, int.left_distrib, mul.comm _ c, -!mul.assoc] - ... = 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 + ... = a * (b % c) / (a * c) + b / c : !int.add_mul_div_self_left H3 + ... = 0 + b / c : {!div_eq_zero_of_lt H5 H4} + ... = b / c : zero_add -theorem mul_div_mul_of_pos {a : ℤ} (b c : ℤ) (H : a > 0) : a * b div (a * c) = b div c := +theorem mul_div_mul_of_pos {a : ℤ} (b c : ℤ) (H : a > 0) : a * b / (a * c) = b / c := lt.by_cases (assume H1 : c < 0, have H2 : -c > 0, from neg_pos_of_neg H1, calc - a * b div (a * c) = - (a * b div (a * -c)) : + a * b / (a * c) = - (a * b / (a * -c)) : 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 [int.div_neg, neg_neg]) + ... = - (b / -c) : mul_div_mul_of_pos_aux _ H H2 + ... = b / c : by rewrite [int.div_neg, neg_neg]) (assume H1 : c = 0, calc - a * b div (a * c) = 0 : by rewrite [H1, mul_zero, int.div_zero] - ... = b div c : by rewrite [H1, int.div_zero]) + a * b / (a * c) = 0 : by rewrite [H1, mul_zero, int.div_zero] + ... = b / c : by rewrite [H1, int.div_zero]) (assume H1 : c > 0, mul_div_mul_of_pos_aux _ H H1) theorem mul_div_mul_of_pos_left (a : ℤ) {b : ℤ} (c : ℤ) (H : b > 0) : - a * b div (c * b) = a div c := + a * b / (c * b) = a / c := !mul.comm ▸ !mul.comm ▸ !mul_div_mul_of_pos H --- TODO: something strange here: why doesn't !modulo.def or !(modulo.def) work? -theorem mul_mod_mul_of_pos {a : ℤ} (b c : ℤ) (H : a > 0) : a * b mod (a * c) = a * (b mod c) := -by rewrite [(modulo.def), modulo.def, !mul_div_mul_of_pos H, mul_sub_left_distrib, mul.left_comm] +theorem mul_mod_mul_of_pos {a : ℤ} (b c : ℤ) (H : a > 0) : a * b % (a * c) = a * (b % c) := +by rewrite [(mod_def), mod_def, !mul_div_mul_of_pos H, mul_sub_left_distrib, mul.left_comm] -theorem lt_div_add_one_mul_self (a : ℤ) {b : ℤ} (H : b > 0) : a < (a div b + 1) * b := -have H : a - a div b * b < b, from !mod_lt_of_pos H, +theorem lt_div_add_one_mul_self (a : ℤ) {b : ℤ} (H : b > 0) : a < (a / b + 1) * b := +have H : a - a / b * b < b, from !mod_lt_of_pos H, calc - a < a div b * b + b : iff.mpr !lt_add_iff_sub_lt_left H - ... = (a div b + 1) * b : by rewrite [right_distrib, one_mul] + a < a / b * b + b : iff.mpr !lt_add_iff_sub_lt_left H + ... = (a / b + 1) * b : by rewrite [right_distrib, one_mul] -theorem div_le_of_nonneg_of_nonneg {a b : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) : a div b ≤ a := +theorem div_le_of_nonneg_of_nonneg {a b : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) : a / b ≤ a := obtain (m : ℕ) (Hm : a = m), from exists_eq_of_nat Ha, obtain (n : ℕ) (Hn : b = n), from exists_eq_of_nat Hb, calc - a div b = of_nat (m div n) : by rewrite [Hm, Hn, of_nat_div] - ... ≤ m : of_nat_le_of_nat_of_le !nat.div_le_self - ... = a : Hm + a / b = of_nat (m / n) : by rewrite [Hm, Hn, of_nat_div] + ... ≤ m : of_nat_le_of_nat_of_le !nat.div_le_self + ... = a : Hm -theorem abs_div_le_abs (a b : ℤ) : abs (a div b) ≤ abs a := -have H : ∀a b, b > 0 → abs (a div b) ≤ abs a, from +theorem abs_div_le_abs (a b : ℤ) : abs (a / b) ≤ abs a := +have H : ∀a b, b > 0 → abs (a / b) ≤ abs a, from take a b, assume H1 : b > 0, or.elim (le_or_gt 0 a) (assume H2 : 0 ≤ a, have H3 : 0 ≤ b, from le_of_lt H1, calc - abs (a div b) = a div b : abs_of_nonneg (int.div_nonneg H2 H3) - ... ≤ a : div_le_of_nonneg_of_nonneg H2 H3 - ... = abs a : abs_of_nonneg H2) + abs (a / b) = a / 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, + have H4 : (-a - 1) / b + 1 ≥ 0, 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), + have H5 : (-a - 1) / b ≤ -a - 1, from div_le_of_nonneg_of_nonneg H3 (le_of_lt H1), calc - abs (a div b) = abs ((-a - 1) div b + 1) : by rewrite [div_of_neg_of_pos H2 H1, abs_neg] - ... = (-a - 1) div b + 1 : abs_of_nonneg H4 - ... ≤ -a - 1 + 1 : add_le_add_right H5 _ - ... = abs a : by rewrite [sub_add_cancel, abs_of_neg H2]), + abs (a / b) = abs ((-a - 1) / b + 1) : by rewrite [div_of_neg_of_pos H2 H1, abs_neg] + ... = (-a - 1) / b + 1 : abs_of_nonneg H4 + ... ≤ -a - 1 + 1 : add_le_add_right H5 _ + ... = abs a : by rewrite [sub_add_cancel, abs_of_neg H2]), lt.by_cases (assume H1 : b < 0, calc - abs (a div b) = abs (a div -b) : by rewrite [int.div_neg, abs_neg] - ... ≤ abs a : H _ _ (neg_pos_of_neg H1)) + abs (a / b) = abs (a / -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, int.div_zero, abs_zero] + abs (a / b) = 0 : by rewrite [H1, int.div_zero, abs_zero] ... ≤ abs a : abs_nonneg) (assume H1 : b > 0, H _ _ H1) -theorem div_mul_cancel_of_mod_eq_zero {a b : ℤ} (H : a mod b = 0) : a div b * b = a := +theorem div_mul_cancel_of_mod_eq_zero {a b : ℤ} (H : a % b = 0) : a / b * b = a := by rewrite [eq_div_mul_add_mod a b at {2}, H, add_zero] -theorem mul_div_cancel_of_mod_eq_zero {a b : ℤ} (H : a mod b = 0) : b * (a div b) = a := +theorem mul_div_cancel_of_mod_eq_zero {a b : ℤ} (H : a % b = 0) : b * (a / b) = a := !mul.comm ▸ div_mul_cancel_of_mod_eq_zero H /- dvd -/ @@ -519,72 +519,72 @@ begin apply nat.dvd.antisymm end -theorem dvd_of_mod_eq_zero {a b : ℤ} (H : b mod a = 0) : a ∣ b := +theorem dvd_of_mod_eq_zero {a b : ℤ} (H : b % a = 0) : a ∣ b := dvd.intro (!mul.comm ▸ div_mul_cancel_of_mod_eq_zero H) -theorem mod_eq_zero_of_dvd {a b : ℤ} (H : a ∣ b) : b mod a = 0 := +theorem mod_eq_zero_of_dvd {a b : ℤ} (H : a ∣ b) : b % a = 0 := dvd.elim H (take z, assume H1 : b = a * z, H1⁻¹ ▸ !mul_mod_right) -theorem dvd_iff_mod_eq_zero (a b : ℤ) : a ∣ b ↔ b mod a = 0 := +theorem dvd_iff_mod_eq_zero (a b : ℤ) : a ∣ b ↔ b % a = 0 := 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) -protected 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 / b * b = a := div_mul_cancel_of_mod_eq_zero (mod_eq_zero_of_dvd H) -protected theorem mul_div_cancel' {a b : ℤ} (H : a ∣ b) : a * (b div a) = b := +protected theorem mul_div_cancel' {a b : ℤ} (H : a ∣ b) : a * (b / a) = b := !mul.comm ▸ !int.div_mul_cancel H -protected 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) / c = a * (b / c) := decidable.by_cases (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, *(!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 (int.div_mul_cancel H1)⁻¹, -have H4 : c = c div a * a, from (int.div_mul_cancel (dvd.trans H1 H2))⁻¹, +theorem div_dvd_div {a b c : ℤ} (H1 : a ∣ b) (H2 : b ∣ c) : b / a ∣ c / a := +have H3 : b = b / a * a, from (int.div_mul_cancel H1)⁻¹, +have H4 : c = c / 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 ⬝ !int.div_zero), + have H6: c / 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)) protected theorem div_eq_iff_eq_mul_right {a b : ℤ} (c : ℤ) (H : b ≠ 0) (H' : b ∣ a) : - a div b = c ↔ a = b * c := + a / b = c ↔ a = b * c := iff.intro (assume H1, by rewrite [-H1, int.mul_div_cancel' H']) (assume H1, by rewrite [H1, !int.mul_div_cancel_left H]) protected theorem div_eq_iff_eq_mul_left {a b : ℤ} (c : ℤ) (H : b ≠ 0) (H' : b ∣ a) : - a div b = c ↔ a = c * b := + a / b = c ↔ a = c * b := !mul.comm ▸ !int.div_eq_iff_eq_mul_right H H' -protected 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 / b = c) : a = b * c := calc - a = b * (a div b) : int.mul_div_cancel' H1 - ... = b * c : H2 + a = b * (a / b) : int.mul_div_cancel' H1 + ... = b * c : H2 protected theorem div_eq_of_eq_mul_right {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = b * c) : - a div b = c := + a / b = c := calc - a div b = b * c div b : H2 - ... = c : !int.mul_div_cancel_left H1 + a / b = b * c / b : H2 + ... = c : !int.mul_div_cancel_left H1 -protected 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 / b = c) : a = c * b := !mul.comm ▸ !int.eq_mul_of_div_eq_right H1 H2 protected theorem div_eq_of_eq_mul_left {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = c * b) : - a div b = c := + a / b = c := 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) := +theorem neg_div_of_dvd {a b : ℤ} (H : b ∣ a) : -a / b = -(a / b) := decidable.by_cases (assume H1 : b = 0, by rewrite [H1, *int.div_zero, neg_zero]) (assume H1 : b ≠ 0, @@ -592,7 +592,7 @@ decidable.by_cases (take c, assume H' : a = b * c, by rewrite [H', neg_mul_eq_mul_neg, *!int.mul_div_cancel_left H1])) -protected theorem sign_eq_div_abs (a : ℤ) : sign a = a div (abs a) := +protected theorem sign_eq_div_abs (a : ℤ) : sign a = a / (abs a) := decidable.by_cases (suppose a = 0, by subst a) (suppose a ≠ 0, @@ -612,21 +612,21 @@ or.elim !le_or_gt ... ≤ a * c : mul_le_mul_of_nonneg_left (add_one_le_of_lt `c > 0`) (le_of_lt `a > 0`) ... = b : Hc) -/- div and ordering -/ +/- / and ordering -/ -protected 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 / 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) + a = a / b * b + a % b : eq_div_mul_add_mod + ... ≥ a / b * b : le_add_of_nonneg_right (!mod_nonneg H) -protected 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 / 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 + a / c * c = a / c * c + 0 : add_zero + ... ≤ a / c * c + a % c : add_le_add_left (!mod_nonneg (ne_of_gt H)) + ... = a : eq_div_mul_add_mod + ... ≤ b * c : H') H -protected 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 / 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, @@ -637,66 +637,66 @@ or.elim (lt_or_eq_of_le H2) (assume H3 : 0 = b, by rewrite [-H3, int.div_zero]; apply H1) -protected 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 / c) : a * c ≤ b := calc - a * c ≤ b div c * c : !mul_le_mul_of_nonneg_right H2 (le_of_lt H1) + a * c ≤ b / c * c : !mul_le_mul_of_nonneg_right H2 (le_of_lt H1) ... ≤ b : !int.div_mul_le (ne_of_gt H1) -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 +protected theorem le_div_of_mul_le {a b c : ℤ} (H1 : c > 0) (H2 : a * c ≤ b) : a ≤ b / c := +have H3 : a * c < (b / c + 1) * c, from calc - a * c ≤ b : H2 - ... = b div c * c + b mod c : eq_div_mul_add_mod - ... < b div c * c + c : add_lt_add_left (!mod_lt_of_pos H1) - ... = (b div c + 1) * c : by rewrite [right_distrib, one_mul], + a * c ≤ b : H2 + ... = b / c * c + b % c : eq_div_mul_add_mod + ... < b / c * c + c : add_lt_add_left (!mod_lt_of_pos H1) + ... = (b / 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)) -protected theorem le_div_iff_mul_le {a b c : ℤ} (H : c > 0) : a ≤ b div c ↔ a * c ≤ b := +protected theorem le_div_iff_mul_le {a b c : ℤ} (H : c > 0) : a ≤ b / c ↔ a * c ≤ b := iff.intro (!int.mul_le_of_le_div H) (!int.le_div_of_mul_le H) -protected theorem div_le_div {a b c : ℤ} (H : c > 0) (H' : a ≤ b) : a div c ≤ b div c := +protected theorem div_le_div {a b c : ℤ} (H : c > 0) (H' : a ≤ b) : a / c ≤ b / c := int.le_div_of_mul_le H (le.trans (!int.div_mul_le (ne_of_gt H)) H') -protected 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 / c < b := lt_of_mul_lt_mul_right (calc - a div c * c = a div c * c + 0 : add_zero - ... ≤ a div c * c + a mod c : add_le_add_left (!mod_nonneg (ne_of_gt H)) - ... = a : eq_div_mul_add_mod - ... < b * c : H') + a / c * c = a / c * c + 0 : add_zero + ... ≤ a / c * c + a % c : add_le_add_left (!mod_nonneg (ne_of_gt H)) + ... = a : eq_div_mul_add_mod + ... < b * c : H') (le_of_lt H) -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, +protected theorem lt_mul_of_div_lt {a b c : ℤ} (H1 : c > 0) (H2 : a / c < b) : a < b * c := +assert H3 : (a / 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, +have H4 : a / c * c + c ≤ b * c, by rewrite [right_distrib at H3, one_mul at H3]; apply H3, calc - a = a div c * c + a mod c : eq_div_mul_add_mod - ... < a div c * c + c : add_lt_add_left (!mod_lt_of_pos H1) - ... ≤ b * c : H4 + a = a / c * c + a % c : eq_div_mul_add_mod + ... < a / c * c + c : add_lt_add_left (!mod_lt_of_pos H1) + ... ≤ b * c : H4 -protected theorem div_lt_iff_lt_mul {a b c : ℤ} (H : c > 0) : a div c < b ↔ a < b * c := +protected theorem div_lt_iff_lt_mul {a b c : ℤ} (H : c > 0) : a / c < b ↔ a < b * c := iff.intro (!int.lt_mul_of_div_lt H) (!int.div_lt_of_lt_mul H) 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 := + a / b ≤ c ↔ a ≤ c * b := by rewrite [propext (!le_iff_mul_le_mul_right H), !int.div_mul_cancel H'] -protected 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 / b ≤ c) : a ≤ c * b := 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 := +theorem div_pos_of_pos_of_dvd {a b : ℤ} (H1 : a > 0) (H2 : b ≥ 0) (H3 : b ∣ a) : a / 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 (int.div_mul_cancel H3); apply H1, +have H6 : (a / 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 := + a / b = c / d := begin apply int.div_eq_of_eq_mul_right H3, rewrite [-!int.mul_div_assoc H2], diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean index 0037f5f29..f694188a6 100644 --- a/library/data/int/gcd.lean +++ b/library/data/int/gcd.lean @@ -44,21 +44,21 @@ by rewrite [↑gcd, *nat_abs_abs] section open nat -theorem gcd_of_ne_zero (a : ℤ) {b : ℤ} (H : b ≠ 0) : gcd a b = gcd b (abs a mod abs b) := +theorem gcd_of_ne_zero (a : ℤ) {b : ℤ} (H : b ≠ 0) : gcd a b = gcd b (abs a % abs b) := have nat_abs b ≠ 0, from assume H', H (eq_zero_of_nat_abs_eq_zero H'), have nat_abs b > 0, from pos_of_ne_zero this, -assert nat.gcd (nat_abs a) (nat_abs b) = (nat.gcd (nat_abs b) (nat_abs a mod nat_abs b)), +assert nat.gcd (nat_abs a) (nat_abs b) = (nat.gcd (nat_abs b) (nat_abs a % nat_abs b)), from @nat.gcd_of_pos (nat_abs a) (nat_abs b) this, calc - gcd a b = nat.gcd (nat_abs b) (nat_abs a mod nat_abs b) : by rewrite [↑gcd, this] - ... = gcd (abs b) (abs a mod abs b) : by rewrite [↑gcd, -*of_nat_nat_abs, of_nat_mod] - ... = gcd b (abs a mod abs b) : by rewrite [↑gcd, *nat_abs_abs] + gcd a b = nat.gcd (nat_abs b) (nat_abs a % nat_abs b) : by rewrite [↑gcd, this] + ... = gcd (abs b) (abs a % abs b) : by rewrite [↑gcd, -*of_nat_nat_abs, of_nat_mod] + ... = gcd b (abs a % abs b) : by rewrite [↑gcd, *nat_abs_abs] end -theorem gcd_of_pos (a : ℤ) {b : ℤ} (H : b > 0) : gcd a b = gcd b (abs a mod b) := +theorem gcd_of_pos (a : ℤ) {b : ℤ} (H : b > 0) : gcd a b = gcd b (abs a % b) := by rewrite [!gcd_of_ne_zero (ne_of_gt H), abs_of_pos H] -theorem gcd_of_nonneg_of_pos {a b : ℤ} (H1 : a ≥ 0) (H2 : b > 0) : gcd a b = gcd b (a mod b) := +theorem gcd_of_nonneg_of_pos {a b : ℤ} (H1 : a ≥ 0) (H2 : b > 0) : gcd a b = gcd b (a % b) := by rewrite [!gcd_of_pos H2, abs_of_nonneg H1] theorem gcd_self (a : ℤ) : gcd a a = abs a := @@ -114,21 +114,21 @@ theorem eq_zero_of_gcd_eq_zero_right {a b : ℤ} (H : gcd a b = 0) : b = 0 := by rewrite gcd.comm at H; apply !eq_zero_of_gcd_eq_zero_left H theorem gcd_div {a b c : ℤ} (H1 : c ∣ a) (H2 : c ∣ b) : - gcd (a div c) (b div c) = gcd a b div (abs c) := + gcd (a / c) (b / c) = gcd a b / (abs c) := decidable.by_cases (suppose c = 0, calc - 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 : int.div_zero - ... = gcd a b div (abs c) : by subst c) + gcd (a / c) (b / c) = gcd 0 0 : by subst c; rewrite *int.div_zero + ... = 0 : gcd_zero_left + ... = gcd a b / 0 : int.div_zero + ... = gcd a b / (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 (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) : int.div_mul_cancel H1 - ... = gcd a b : int.div_mul_cancel H2)))) + gcd (a / c) (b / c) * abs c = gcd (a / c * c) (b / c * c) : gcd_mul_right + ... = gcd a (b / 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 @@ -138,7 +138,7 @@ theorem gcd_dvd_gcd_mul_right (a b c : ℤ) : gcd a b ∣ gcd (a * c) b := theorem div_gcd_eq_div_gcd_of_nonneg {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = a₂ * b₁) (H1 : b₁ ≠ 0) (H2 : b₂ ≠ 0) (H3 : a₁ ≥ 0) (H4 : a₂ ≥ 0) : - a₁ div (gcd a₁ b₁) = a₂ div (gcd a₂ b₂) := + a₁ / (gcd a₁ b₁) = a₂ / (gcd a₂ b₂) := begin apply div_eq_div_of_dvd_of_dvd, repeat (apply gcd_dvd_left), @@ -149,7 +149,7 @@ begin end theorem div_gcd_eq_div_gcd {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = a₂ * b₁) (H1 : b₁ > 0) (H2 : b₂ > 0) : - a₁ div (gcd a₁ b₁) = a₂ div (gcd a₂ b₂) := + a₁ / (gcd a₁ b₁) = a₂ / (gcd a₂ b₂) := or.elim (le_or_gt 0 a₁) (assume H3 : a₁ ≥ 0, have H4 : a₂ * b₁ ≥ 0, by rewrite -H; apply mul_nonneg H3 (le_of_lt H2), @@ -158,7 +158,7 @@ or.elim (le_or_gt 0 a₁) (assume H3 : a₁ < 0, have H4 : a₂ * b₁ < 0, by rewrite -H; apply mul_neg_of_neg_of_pos H3 H2, assert H5 : a₂ < 0, from neg_of_mul_neg_right H4 (le_of_lt H1), - assert H6 : abs a₁ div (gcd (abs a₁) (abs b₁)) = abs a₂ div (gcd (abs a₂) (abs b₂)), + assert H6 : abs a₁ / (gcd (abs a₁) (abs b₁)) = abs a₂ / (gcd (abs a₂) (abs b₂)), begin apply div_gcd_eq_div_gcd_of_nonneg, rewrite [abs_of_pos H1, abs_of_pos H2, abs_of_neg H3, abs_of_neg H5], @@ -167,17 +167,17 @@ or.elim (le_or_gt 0 a₁) apply ne_of_gt (abs_pos_of_pos H2), repeat (apply abs_nonneg) end, - have H7 : -a₁ div (gcd a₁ b₁) = -a₂ div (gcd a₂ b₂), + have H7 : -a₁ / (gcd a₁ b₁) = -a₂ / (gcd a₂ b₂), begin rewrite [-abs_of_neg H3, -abs_of_neg H5, -gcd_abs_abs a₁], rewrite [-gcd_abs_abs a₂ b₂], exact H6 end, calc - a₁ div (gcd a₁ b₁) = -(-a₁ div (gcd a₁ b₁)) : + a₁ / (gcd a₁ b₁) = -(-a₁ / (gcd a₁ b₁)) : by rewrite [neg_div_of_dvd !gcd_dvd_left, neg_neg] - ... = -(-a₂ div (gcd a₂ b₂)) : H7 - ... = a₂ div (gcd a₂ b₂) : + ... = -(-a₂ / (gcd a₂ b₂)) : H7 + ... = a₂ / (gcd a₂ b₂) : by rewrite [neg_div_of_dvd !gcd_dvd_left, neg_neg]) /- lcm -/ @@ -283,11 +283,11 @@ theorem gcd_mul_right_cancel_of_coprime_right {c a : ℤ} (b : ℤ) (H : coprime !gcd.comm ▸ !gcd.comm ▸ !gcd_mul_right_cancel_of_coprime H theorem coprime_div_gcd_div_gcd {a b : ℤ} (H : gcd a b ≠ 0) : - coprime (a div gcd a b) (b div gcd a b) := + coprime (a / gcd a b) (b / gcd a b) := 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, int.div_self H] + gcd (a / gcd a b) (b / gcd a b) + = gcd a b / abs (gcd a b) : gcd_div !gcd_dvd_left !gcd_dvd_right + ... = 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 (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)⁻¹, +have H1 : a = (a / gcd a b) * gcd a b, from (int.div_mul_cancel !gcd_dvd_left)⁻¹, +have H2 : b = (b / 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 := @@ -336,16 +336,16 @@ decidable.by_cases exists.intro _ (exists.intro _ (and.intro `c = 0 * b` (and.intro `0 ∣ a` `b ∣ b`)))) (suppose gcd c a ≠ 0, have gcd c a ∣ c, from !gcd_dvd_left, - have H3 : c div gcd c a ∣ (a * b) div gcd c a, from div_dvd_div this H, - have H4 : (a * b) div gcd c a = (a div gcd c a) * b, from + have H3 : c / gcd c a ∣ (a * b) / gcd c a, from div_dvd_div this H, + have H4 : (a * b) / gcd c a = (a / 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) : !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 (int.mul_div_cancel' `gcd c a ∣ c`)⁻¹, + a * b / gcd c a = b * a / gcd c a : mul.comm + ... = b * (a / gcd c a) : !int.mul_div_assoc !gcd_dvd_right + ... = a / gcd c a * b : mul.comm, + have H5 : c / gcd c a ∣ (a / gcd c a) * b, from H4 ▸ H3, + have H6 : coprime (c / gcd c a) (a / gcd c a), from coprime_div_gcd_div_gcd `gcd c a ≠ 0`, + have H7 : c / gcd c a ∣ b, from dvd_of_coprime_of_dvd_mul_left H6 H5, + have H8 : c = gcd c a * (c / 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 6c37a83a4..b7d58b627 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -20,58 +20,58 @@ and.rec (λ ypos ylex, sub_lt (lt_of_lt_of_le ypos ylex) ypos) private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero -protected definition divide := fix div.F +protected definition div := fix div.F -definition nat_has_divide [reducible] [instance] [priority nat.prio] : has_divide nat := -has_divide.mk nat.divide +definition nat_has_divide [reducible] [instance] [priority nat.prio] : has_div nat := +has_div.mk nat.div -theorem divide_def (x y : nat) : divide x y = if 0 < y ∧ y ≤ x then divide (x - y) y + 1 else 0 := +theorem div_def (x y : nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := congr_fun (fix_eq div.F x) y -protected theorem div_zero (a : ℕ) : a div 0 = 0 := -divide_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0)) +protected theorem div_zero (a : ℕ) : a / 0 = 0 := +div_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 div_eq_zero_of_lt {a b : ℕ} (h : a < b) : a / b = 0 := +div_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_gt h)) -protected theorem zero_div (b : ℕ) : 0 div b = 0 := -divide_def 0 b ⬝ if_neg (and.rec not_le_of_gt) +protected theorem zero_div (b : ℕ) : 0 / b = 0 := +div_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) := -divide_def a b ⬝ if_pos (and.intro h₁ h₂) +theorem div_eq_succ_sub_div {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a / b = succ ((a - b) / b) := +div_def a b ⬝ if_pos (and.intro h₁ h₂) -theorem add_div_self (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) := +theorem add_div_self (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) / z = succ (x / z) := calc - (x + z) div z = if 0 < z ∧ z ≤ x + z then (x + z - z) div z + 1 else 0 : !divide_def - ... = (x + z - z) div z + 1 : if_pos (and.intro H (le_add_left z x)) - ... = succ (x div z) : {!nat.add_sub_cancel} + (x + z) / z = if 0 < z ∧ z ≤ x + z then (x + z - z) / z + 1 else 0 : !div_def + ... = (x + z - z) / z + 1 : if_pos (and.intro H (le_add_left z x)) + ... = succ (x / z) : {!nat.add_sub_cancel} -theorem add_div_self_left {x : ℕ} (z : ℕ) (H : x > 0) : (x + z) div x = succ (z div x) := +theorem add_div_self_left {x : ℕ} (z : ℕ) (H : x > 0) : (x + z) / x = succ (z / x) := !add.comm ▸ !add_div_self H -theorem add_mul_div_self {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y := +theorem add_mul_div_self {x y z : ℕ} (H : z > 0) : (x + y * z) / z = x / z + y := nat.induction_on y - (calc (x + 0 * z) div z = (x + 0) div z : zero_mul - ... = x div z : add_zero - ... = x div z + 0 : add_zero) + (calc (x + 0 * z) / z = (x + 0) / z : zero_mul + ... = x / z : add_zero + ... = x / z + 0 : add_zero) (take y, - assume IH : (x + y * z) div z = x div z + y, calc - (x + succ y * z) div z = (x + (y * z + z)) div z : succ_mul - ... = (x + y * z + z) div z : add.assoc - ... = succ ((x + y * z) div z) : !add_div_self H - ... = succ (x div z + y) : IH) + assume IH : (x + y * z) / z = x / z + y, calc + (x + succ y * z) / z = (x + (y * z + z)) / z : succ_mul + ... = (x + y * z + z) / z : add.assoc + ... = succ ((x + y * z) / z) : !add_div_self H + ... = succ (x / z + y) : IH) -theorem add_mul_div_self_left (x z : ℕ) {y : ℕ} (H : y > 0) : (x + y * z) div y = x div y + z := +theorem add_mul_div_self_left (x z : ℕ) {y : ℕ} (H : y > 0) : (x + y * z) / y = x / y + z := !mul.comm ▸ add_mul_div_self H -protected 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 / 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 : nat.zero_div - ... = m : zero_add + m * n / n = (0 + m * n) / n : zero_add + ... = 0 / n + m : add_mul_div_self H + ... = 0 + m : nat.zero_div + ... = m : zero_add -protected theorem mul_div_cancel_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n div m = n := +protected theorem mul_div_cancel_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n / m = n := !mul.comm ▸ !nat.mul_div_cancel H /- mod -/ @@ -79,147 +79,147 @@ protected theorem mul_div_cancel_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n di private definition mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x -protected definition modulo := fix mod.F +protected definition mod := fix mod.F -definition nat_has_modulo [reducible] [instance] [priority nat.prio] : has_modulo nat := -has_modulo.mk nat.modulo +definition nat_has_mod [reducible] [instance] [priority nat.prio] : has_mod nat := +has_mod.mk nat.mod -notation [priority nat.prio] a ≡ b `[mod `:0 c:0 `]` := a mod c = b mod c +notation [priority nat.prio] a ≡ b `[mod `:0 c:0 `]` := a % c = b % c -theorem modulo_def (x y : nat) : modulo x y = if 0 < y ∧ y ≤ x then modulo (x - y) y else x := +theorem mod_def (x y : nat) : mod x y = if 0 < y ∧ y ≤ x then mod (x - y) y else x := congr_fun (fix_eq mod.F x) y -theorem mod_zero (a : ℕ) : a mod 0 = a := -modulo_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0)) +theorem mod_zero (a : ℕ) : a % 0 = a := +mod_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0)) -theorem mod_eq_of_lt {a b : ℕ} (h : a < b) : a mod b = a := -modulo_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_gt h)) +theorem mod_eq_of_lt {a b : ℕ} (h : a < b) : a % b = a := +mod_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_gt h)) -theorem zero_mod (b : ℕ) : 0 mod b = 0 := -modulo_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0))) +theorem zero_mod (b : ℕ) : 0 % b = 0 := +mod_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l r) (lt.irrefl 0))) -theorem mod_eq_sub_mod {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a mod b = (a - b) mod b := -modulo_def a b ⬝ if_pos (and.intro h₁ h₂) +theorem mod_eq_sub_mod {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a % b = (a - b) % b := +mod_def a b ⬝ if_pos (and.intro h₁ h₂) -theorem add_mod_self (x z : ℕ) : (x + z) mod z = x mod z := +theorem add_mod_self (x z : ℕ) : (x + z) % z = x % z := by_cases_zero_pos z (by rewrite add_zero) (take z, assume H : z > 0, 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 : nat.add_sub_cancel) + (x + z) % z = if 0 < z ∧ z ≤ x + z then (x + z - z) % z else _ : mod_def + ... = (x + z - z) % z : if_pos (and.intro H (le_add_left z x)) + ... = x % z : nat.add_sub_cancel) -theorem add_mod_self_left (x z : ℕ) : (x + z) mod x = z mod x := +theorem add_mod_self_left (x z : ℕ) : (x + z) % x = z % x := !add.comm ▸ !add_mod_self -theorem add_mul_mod_self (x y z : ℕ) : (x + y * z) mod z = x mod z := +theorem add_mul_mod_self (x y z : ℕ) : (x + y * z) % z = x % z := nat.induction_on y - (calc (x + 0 * z) mod z = (x + 0) mod z : zero_mul - ... = x mod z : add_zero) + (calc (x + 0 * z) % z = (x + 0) % z : zero_mul + ... = x % z : add_zero) (take y, - assume IH : (x + y * z) mod z = x mod z, + assume IH : (x + y * z) % z = x % z, calc - (x + succ y * z) mod z = (x + (y * z + z)) mod z : succ_mul - ... = (x + y * z + z) mod z : add.assoc - ... = (x + y * z) mod z : !add_mod_self - ... = x mod z : IH) + (x + succ y * z) % z = (x + (y * z + z)) % z : succ_mul + ... = (x + y * z + z) % z : add.assoc + ... = (x + y * z) % z : !add_mod_self + ... = x % z : IH) -theorem add_mul_mod_self_left (x y z : ℕ) : (x + y * z) mod y = x mod y := +theorem add_mul_mod_self_left (x y z : ℕ) : (x + y * z) % y = x % y := !mul.comm ▸ !add_mul_mod_self -theorem mul_mod_left (m n : ℕ) : (m * n) mod n = 0 := +theorem mul_mod_left (m n : ℕ) : (m * n) % n = 0 := by rewrite [-zero_add (m * n), add_mul_mod_self, zero_mod] -theorem mul_mod_right (m n : ℕ) : (m * n) mod m = 0 := +theorem mul_mod_right (m n : ℕ) : (m * n) % m = 0 := !mul.comm ▸ !mul_mod_left -theorem mod_lt (x : ℕ) {y : ℕ} (H : y > 0) : x mod y < y := +theorem mod_lt (x : ℕ) {y : ℕ} (H : y > 0) : x % y < y := nat.case_strong_induction_on x - (show 0 mod y < y, from !zero_mod⁻¹ ▸ H) + (show 0 % y < y, from !zero_mod⁻¹ ▸ H) (take x, - assume IH : ∀x', x' ≤ x → x' mod y < y, - show succ x mod y < y, from + assume IH : ∀x', x' ≤ x → x' % y < y, + show succ x % y < y, from by_cases -- (succ x < y) (assume H1 : succ x < y, - have succ x mod y = succ x, from mod_eq_of_lt H1, - show succ x mod y < y, from this⁻¹ ▸ H1) + have succ x % y = succ x, from mod_eq_of_lt H1, + show succ x % y < y, from this⁻¹ ▸ H1) (assume H1 : ¬ succ x < y, have y ≤ succ x, from le_of_not_gt H1, - have h : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H this, + have h : succ x % y = (succ x - y) % y, from mod_eq_sub_mod H this, have succ x - y < succ x, from sub_lt !succ_pos H, have succ x - y ≤ x, from le_of_lt_succ this, - show succ x mod y < y, from h⁻¹ ▸ IH _ this)) + show succ x % y < y, from h⁻¹ ▸ IH _ this)) -theorem mod_one (n : ℕ) : n mod 1 = 0 := -have H1 : n mod 1 < 1, from !mod_lt !succ_pos, +theorem mod_one (n : ℕ) : n % 1 = 0 := +have H1 : n % 1 < 1, from !mod_lt !succ_pos, eq_zero_of_le_zero (le_of_lt_succ H1) /- properties of div and mod -/ --- the quotient / remainder theorem -theorem eq_div_mul_add_mod (x y : ℕ) : x = x div y * y + x mod y := +-- the quotient - remainder theorem +theorem eq_div_mul_add_mod (x y : ℕ) : x = x / y * y + x % y := begin eapply by_cases_zero_pos y, - show x = x div 0 * 0 + x mod 0, from + show x = x / 0 * 0 + x % 0, from (calc - x div 0 * 0 + x mod 0 = 0 + x mod 0 : mul_zero - ... = x mod 0 : zero_add - ... = x : mod_zero)⁻¹, + x / 0 * 0 + x % 0 = 0 + x % 0 : mul_zero + ... = x % 0 : zero_add + ... = x : mod_zero)⁻¹, intro y H, - show x = x div y * y + x mod y, + show x = x / y * y + x % y, begin eapply nat.case_strong_induction_on x, - show 0 = (0 div y) * y + 0 mod y, by rewrite [zero_mod, add_zero, nat.zero_div, zero_mul], + show 0 = (0 / y) * y + 0 % 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 + show succ x = succ x / y * y + succ x % y, from if H1 : succ x < y then - assert H2 : succ x div y = 0, from div_eq_zero_of_lt H1, - assert H3 : succ x mod y = succ x, from mod_eq_of_lt H1, + assert H2 : succ x / y = 0, from div_eq_zero_of_lt H1, + assert H3 : succ x % y = succ x, from mod_eq_of_lt H1, begin rewrite [H2, H3, zero_mul, zero_add] end else have H2 : y ≤ succ x, from le_of_not_gt H1, - assert H3 : succ x div y = succ ((succ x - y) div y), from div_eq_succ_sub_div H H2, - assert H4 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2, + assert H3 : succ x / y = succ ((succ x - y) / y), from div_eq_succ_sub_div H H2, + assert H4 : succ x % y = (succ x - y) % y, from mod_eq_sub_mod H H2, have H5 : succ x - y < succ x, from sub_lt !succ_pos H, assert H6 : succ x - y ≤ x, from le_of_lt_succ H5, (calc - succ x div y * y + succ x mod y = - succ ((succ x - y) div y) * y + succ x mod y : by rewrite H3 - ... = ((succ x - y) div y) * y + y + succ x mod y : by rewrite succ_mul - ... = ((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 : nat.sub_add_cancel H2)⁻¹ + succ x / y * y + succ x % y = + succ ((succ x - y) / y) * y + succ x % y : by rewrite H3 + ... = ((succ x - y) / y) * y + y + succ x % y : by rewrite succ_mul + ... = ((succ x - y) / y) * y + y + (succ x - y) % y : by rewrite H4 + ... = ((succ x - y) / y) * y + (succ x - y) % y + y : add.right_comm + ... = succ x - y + y : by rewrite -(IH _ H6) + ... = 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 := +theorem mod_eq_sub_div_mul (x y : ℕ) : x % y = x - x / y * y := 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] +theorem mod_add_mod (m n k : ℕ) : (m % n + k) % n = (m + k) % n := +by rewrite [eq_div_mul_add_mod m n at {2}, add.assoc, add.comm (m / n * n), add_mul_mod_self] -theorem add_mod_mod (m n k : ℕ) : (m + n mod k) mod k = (m + n) mod k := +theorem add_mod_mod (m n k : ℕ) : (m + n % k) % k = (m + n) % k := by rewrite [add.comm, mod_add_mod, add.comm] -theorem add_mod_eq_add_mod_right {m n k : ℕ} (i : ℕ) (H : m mod n = k mod n) : - (m + i) mod n = (k + i) mod n := +theorem add_mod_eq_add_mod_right {m n k : ℕ} (i : ℕ) (H : m % n = k % n) : + (m + i) % n = (k + i) % n := by rewrite [-mod_add_mod, -mod_add_mod k, H] -theorem add_mod_eq_add_mod_left {m n k : ℕ} (i : ℕ) (H : m mod n = k mod n) : - (i + m) mod n = (i + k) mod n := +theorem add_mod_eq_add_mod_left {m n k : ℕ} (i : ℕ) (H : m % n = k % n) : + (i + m) % n = (i + k) % n := by rewrite [add.comm, add_mod_eq_add_mod_right _ H, add.comm] theorem mod_eq_mod_of_add_mod_eq_add_mod_right {m n k i : ℕ} : - (m + i) mod n = (k + i) mod n → m mod n = k mod n := + (m + i) % n = (k + i) % n → m % n = k % n := by_cases_zero_pos n (by rewrite [*mod_zero]; apply eq_of_add_eq_add_right) (take n, assume npos : n > 0, - assume H1 : (m + i) mod n = (k + i) mod n, - have H2 : (m + i mod n) mod n = (k + i mod n) mod n, by rewrite [*add_mod_mod, H1], - assert H3 : (m + i mod n + (n - i mod n)) mod n = (k + i mod n + (n - i mod n)) mod n, + assume H1 : (m + i) % n = (k + i) % n, + have H2 : (m + i % n) % n = (k + i % n) % n, by rewrite [*add_mod_mod, H1], + assert H3 : (m + i % n + (n - i % n)) % n = (k + i % n + (n - i % n)) % n, from add_mod_eq_add_mod_right _ H2, begin revert H3, @@ -228,21 +228,21 @@ by_cases_zero_pos n end) theorem mod_eq_mod_of_add_mod_eq_add_mod_left {m n k i : ℕ} : - (i + m) mod n = (i + k) mod n → m mod n = k mod n := + (i + m) % n = (i + k) % n → m % n = k % n := by rewrite [add.comm i m, add.comm i k]; apply mod_eq_mod_of_add_mod_eq_add_mod_right -theorem mod_le {x y : ℕ} : x mod y ≤ x := +theorem mod_le {x y : ℕ} : x % y ≤ x := !eq_div_mul_add_mod⁻¹ ▸ !le_add_left theorem eq_remainder {q1 r1 q2 r2 y : ℕ} (H1 : r1 < y) (H2 : r2 < y) (H3 : q1 * y + r1 = q2 * y + r2) : r1 = r2 := calc - r1 = r1 mod y : mod_eq_of_lt H1 - ... = (r1 + q1 * y) mod y : !add_mul_mod_self⁻¹ - ... = (q1 * y + r1) mod y : add.comm - ... = (r2 + q2 * y) mod y : by rewrite [H3, add.comm] - ... = r2 mod y : !add_mul_mod_self - ... = r2 : mod_eq_of_lt H2 + r1 = r1 % y : mod_eq_of_lt H1 + ... = (r1 + q1 * y) % y : !add_mul_mod_self⁻¹ + ... = (q1 * y + r1) % y : add.comm + ... = (r2 + q2 * y) % y : by rewrite [H3, add.comm] + ... = r2 % y : !add_mul_mod_self + ... = r2 : mod_eq_of_lt H2 theorem eq_quotient {q1 r1 q2 r2 y : ℕ} (H1 : r1 < y) (H2 : r2 < y) (H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 := @@ -251,93 +251,93 @@ 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 -protected 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) / (z * y) = x / y := if H : y = 0 then 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, + have H1 : (z * x) % (z * y) < z * y, from !mod_lt zypos, + have H2 : z * (x % 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) + ((z * x) / (z * y)) * (z * y) + (z * x) % (z * y) = z * x : eq_div_mul_add_mod + ... = z * (x / y * y + x % y) : eq_div_mul_add_mod + ... = z * (x / y * y) + z * (x % y) : left_distrib + ... = (x / y) * (z * y) + z * (x % y) : mul.left_comm) -protected theorem mul_div_mul_right {x z y : ℕ} (zpos : z > 0) : (x * z) div (y * z) = x div y := +protected theorem mul_div_mul_right {x z y : ℕ} (zpos : z > 0) : (x * z) / (y * z) = x / 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) := +theorem mul_mod_mul_left (z x y : ℕ) : (z * x) % (z * y) = z * (x % y) := or.elim (eq_zero_or_pos z) (assume H : z = 0, H⁻¹ ▸ calc - (0 * x) mod (z * y) = 0 mod (z * y) : zero_mul - ... = 0 : zero_mod - ... = 0 * (x mod y) : zero_mul) + (0 * x) % (z * y) = 0 % (z * y) : zero_mul + ... = 0 : zero_mod + ... = 0 * (x % y) : zero_mul) (assume zpos : z > 0, or.elim (eq_zero_or_pos y) (assume H : y = 0, by rewrite [H, mul_zero, *mod_zero]) (assume ypos : y > 0, 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, + have H1 : (z * x) % (z * y) < z * y, from !mod_lt zypos, + have H2 : z * (x % y) < z * y, from mul_lt_mul_of_pos_left (!mod_lt ypos) zpos, eq_remainder 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))) + ((z * x) / (z * y)) * (z * y) + (z * x) % (z * y) = z * x : eq_div_mul_add_mod + ... = z * (x / y * y + x % y) : eq_div_mul_add_mod + ... = z * (x / y * y) + z * (x % y) : left_distrib + ... = (x / y) * (z * y) + z * (x % y) : mul.left_comm))) -theorem mul_mod_mul_right (x z y : ℕ) : (x * z) mod (y * z) = (x mod y) * z := +theorem mul_mod_mul_right (x z y : ℕ) : (x * z) % (y * z) = (x % y) * z := mul.comm z x ▸ mul.comm z y ▸ !mul.comm ▸ !mul_mod_mul_left -theorem mod_self (n : ℕ) : n mod n = 0 := +theorem mod_self (n : ℕ) : n % n = 0 := nat.cases_on n (by rewrite zero_mod) (take n, by rewrite [-zero_add (succ n) at {1}, add_mod_self]) -theorem mul_mod_eq_mod_mul_mod (m n k : nat) : (m * n) mod k = ((m mod k) * n) mod k := +theorem mul_mod_eq_mod_mul_mod (m n k : nat) : (m * n) % k = ((m % k) * n) % k := calc - (m * n) mod k = (((m div k) * k + m mod k) * n) mod k : eq_div_mul_add_mod - ... = ((m mod k) * n) mod k : + (m * n) % k = (((m / k) * k + m % k) * n) % k : eq_div_mul_add_mod + ... = ((m % k) * n) % k : by rewrite [right_distrib, mul.right_comm, add.comm, add_mul_mod_self] -theorem mul_mod_eq_mul_mod_mod (m n k : nat) : (m * n) mod k = (m * (n mod k)) mod k := +theorem mul_mod_eq_mul_mod_mod (m n k : nat) : (m * n) % k = (m * (n % k)) % k := !mul.comm ▸ !mul.comm ▸ !mul_mod_eq_mod_mul_mod -protected theorem div_one (n : ℕ) : n div 1 = n := -assert n div 1 * 1 + n mod 1 = n, from !eq_div_mul_add_mod⁻¹, +protected theorem div_one (n : ℕ) : n / 1 = n := +assert n / 1 * 1 + n % 1 = n, from !eq_div_mul_add_mod⁻¹, begin rewrite [-this at {2}, mul_one, mod_one] end -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, +protected theorem div_self {n : ℕ} (H : n > 0) : n / n = 1 := +assert (n * 1) / (n * 1) = 1 / 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 := +theorem div_mul_cancel_of_mod_eq_zero {m n : ℕ} (H : m % n = 0) : m / n * n = m := by rewrite [eq_div_mul_add_mod m n at {2}, H, add_zero] -theorem mul_div_cancel_of_mod_eq_zero {m n : ℕ} (H : m mod n = 0) : n * (m div n) = m := +theorem mul_div_cancel_of_mod_eq_zero {m n : ℕ} (H : m % n = 0) : n * (m / n) = m := !mul.comm ▸ div_mul_cancel_of_mod_eq_zero H /- dvd -/ -theorem dvd_of_mod_eq_zero {m n : ℕ} (H : n mod m = 0) : m ∣ n := +theorem dvd_of_mod_eq_zero {m n : ℕ} (H : n % m = 0) : m ∣ n := dvd.intro (!mul.comm ▸ div_mul_cancel_of_mod_eq_zero H) -theorem mod_eq_zero_of_dvd {m n : ℕ} (H : m ∣ n) : n mod m = 0 := +theorem mod_eq_zero_of_dvd {m n : ℕ} (H : m ∣ n) : n % m = 0 := dvd.elim H (take z, assume H1 : n = m * z, H1⁻¹ ▸ !mul_mod_right) -theorem dvd_iff_mod_eq_zero (m n : ℕ) : m ∣ n ↔ n mod m = 0 := +theorem dvd_iff_mod_eq_zero (m n : ℕ) : m ∣ n ↔ n % m = 0 := 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) -protected 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 / n * n = m := div_mul_cancel_of_mod_eq_zero (mod_eq_zero_of_dvd H) -protected theorem mul_div_cancel' {m n : ℕ} (H : n ∣ m) : n * (m div n) = m := +protected theorem mul_div_cancel' {m n : ℕ} (H : n ∣ m) : n * (m / 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₂ := @@ -376,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⁻¹)) -protected 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 / k = m * (n / k) := or.elim (eq_zero_or_pos k) (assume H1 : k = 0, calc - m * n div k = m * n div 0 : H1 - ... = 0 : nat.div_zero - ... = m * 0 : mul_zero m - ... = m * (n div 0) : nat.div_zero - ... = m * (n div k) : H1) + m * n / k = m * n / 0 : H1 + ... = 0 : nat.div_zero + ... = m * 0 : mul_zero m + ... = m * (n / 0) : nat.div_zero + ... = m * (n / k) : H1) (assume H1 : k > 0, - have H2 : n = n div k * k, from (nat.div_mul_cancel H)⁻¹, + have H2 : n = n / 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) : nat.mul_div_cancel _ H1) + m * n / k = m * (n / k * k) / k : H2 + ... = m * (n / k) * k / k : mul.assoc + ... = m * (n / 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 @@ -405,47 +405,47 @@ 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 (nat.div_mul_cancel H1)⁻¹, -have H4 : n = n div k * k, from (nat.div_mul_cancel (dvd.trans H1 H2))⁻¹, +theorem div_dvd_div {k m n : ℕ} (H1 : k ∣ m) (H2 : m ∣ n) : m / k ∣ n / k := +have H3 : m = m / k * k, from (nat.div_mul_cancel H1)⁻¹, +have H4 : n = n / 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 ⬝ !nat.div_zero), + have H6: n / k = 0, from (congr_arg _ H5 ⬝ !nat.div_zero), H6⁻¹ ▸ !dvd_zero) (assume H5 : k > 0, nat.dvd_of_mul_dvd_mul_right H5 (H3 ▸ H4 ▸ H2)) protected theorem div_eq_iff_eq_mul_right {m n : ℕ} (k : ℕ) (H : n > 0) (H' : n ∣ m) : - m div n = k ↔ m = n * k := + m / n = k ↔ m = n * k := iff.intro (assume H1, by rewrite [-H1, nat.mul_div_cancel' H']) (assume H1, by rewrite [H1, !nat.mul_div_cancel_left H]) protected theorem div_eq_iff_eq_mul_left {m n : ℕ} (k : ℕ) (H : n > 0) (H' : n ∣ m) : - m div n = k ↔ m = k * n := + m / n = k ↔ m = k * n := !mul.comm ▸ !nat.div_eq_iff_eq_mul_right H H' -protected 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 / n = k) : m = n * k := calc - m = n * (m div n) : nat.mul_div_cancel' H1 - ... = n * k : H2 + m = n * (m / n) : nat.mul_div_cancel' H1 + ... = n * k : H2 protected theorem div_eq_of_eq_mul_right {m n k : ℕ} (H1 : n > 0) (H2 : m = n * k) : - m div n = k := + m / n = k := calc - m div n = n * k div n : H2 - ... = k : !nat.mul_div_cancel_left H1 + m / n = n * k / n : H2 + ... = k : !nat.mul_div_cancel_left H1 -protected 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 / n = k) : m = k * n := !mul.comm ▸ !nat.eq_mul_of_div_eq_right H1 H2 protected theorem div_eq_of_eq_mul_left {m n k : ℕ} (H1 : n > 0) (H2 : m = k * n) : - m div n = k := + m / n = k := !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 := +lemma add_mod_eq_of_dvd (i j n : nat) : n ∣ j → (i + j) % n = i % n := assume h, obtain k (hk : j = n * k), from exists_eq_mul_right_of_dvd h, begin @@ -453,39 +453,39 @@ begin apply add_mul_mod_self end -/- div and ordering -/ +/- / and ordering -/ lemma le_of_dvd {m n : nat} : n > 0 → m ∣ n → m ≤ n := assume (h₁ : n > 0) (h₂ : m ∣ n), -assert h₃ : n mod m = 0, from mod_eq_zero_of_dvd h₂, +assert h₃ : n % m = 0, from mod_eq_zero_of_dvd h₂, by_contradiction (λ nle : ¬ m ≤ n, have h₄ : m > n, from lt_of_not_ge nle, - assert h₅ : n mod m = n, from mod_eq_of_lt h₄, + assert h₅ : n % m = n, from mod_eq_of_lt h₄, begin rewrite h₃ at h₅, subst n, exact absurd h₁ (lt.irrefl 0) end) -theorem div_mul_le (m n : ℕ) : m div n * n ≤ m := +theorem div_mul_le (m n : ℕ) : m / n * n ≤ m := calc - m = m div n * n + m mod n : eq_div_mul_add_mod - ... ≥ m div n * n : le_add_right + m = m / n * n + m % n : eq_div_mul_add_mod + ... ≥ m / n * n : le_add_right -protected 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 / k ≤ n := or.elim (eq_zero_or_pos k) (assume H1 : k = 0, calc - m div k = m div 0 : H1 + m / k = m / 0 : H1 ... = 0 : nat.div_zero ... ≤ n : zero_le) (assume H1 : k > 0, le_of_mul_le_mul_right (calc - m div k * k ≤ m div k * k + m mod k : le_add_right - ... = m : eq_div_mul_add_mod - ... ≤ n * k : H) H1) + m / k * k ≤ m / k * k + m % k : le_add_right + ... = m : eq_div_mul_add_mod + ... ≤ n * k : H) H1) -protected theorem div_le_self (m n : ℕ) : m div n ≤ m := +protected theorem div_le_self (m n : ℕ) : m / n ≤ m := nat.cases_on n (!nat.div_zero⁻¹ ▸ !zero_le) take n, have H : m ≤ m * succ n, from calc @@ -493,86 +493,86 @@ nat.cases_on n (!nat.div_zero⁻¹ ▸ !zero_le) ... ≤ m * succ n : !mul_le_mul_left (succ_le_succ !zero_le), nat.div_le_of_le_mul H -protected 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 / k) : m * k ≤ n := calc - m * k ≤ n div k * k : !mul_le_mul_right H + m * k ≤ n / k * k : !mul_le_mul_right H ... ≤ n : div_mul_le -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 +protected theorem le_div_of_mul_le {m n k : ℕ} (H1 : k > 0) (H2 : m * k ≤ n) : m ≤ n / k := +have H3 : m * k < (succ (n / k)) * k, from calc - m * k ≤ n : H2 - ... = n div k * k + n mod k : eq_div_mul_add_mod - ... < n div k * k + k : add_lt_add_left (!mod_lt H1) - ... = (succ (n div k)) * k : succ_mul, + m * k ≤ n : H2 + ... = n / k * k + n % k : eq_div_mul_add_mod + ... < n / k * k + k : add_lt_add_left (!mod_lt H1) + ... = (succ (n / k)) * k : succ_mul, le_of_lt_succ (lt_of_mul_lt_mul_right H3) -protected theorem le_div_iff_mul_le {m n k : ℕ} (H : k > 0) : m ≤ n div k ↔ m * k ≤ n := +protected theorem le_div_iff_mul_le {m n k : ℕ} (H : k > 0) : m ≤ n / k ↔ m * k ≤ n := iff.intro !nat.mul_le_of_le_div (!nat.le_div_of_mul_le H) -protected 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 / k ≤ n / k := by_cases_zero_pos k (by rewrite [*nat.div_zero]) (take k, assume H1 : k > 0, nat.le_div_of_mul_le H1 (le.trans !div_mul_le H)) -protected 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 / 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) + m / k * k ≤ m / k * k + m % k : le_add_right + ... = m : eq_div_mul_add_mod + ... < n * k : H) -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, +protected theorem lt_mul_of_div_lt {m n k : ℕ} (H1 : k > 0) (H2 : m / k < n) : m < n * k := +assert H3 : succ (m / k) * k ≤ n * k, from !mul_le_mul_right (succ_le_of_lt H2), +have H4 : m / k * k + k ≤ n * k, by rewrite [succ_mul at H3]; apply H3, calc - m = m div k * k + m mod k : eq_div_mul_add_mod - ... < m div k * k + k : add_lt_add_left (!mod_lt H1) - ... ≤ n * k : H4 + m = m / k * k + m % k : eq_div_mul_add_mod + ... < m / k * k + k : add_lt_add_left (!mod_lt H1) + ... ≤ n * k : H4 -protected theorem div_lt_iff_lt_mul {m n k : ℕ} (H : k > 0) : m div k < n ↔ m < n * k := +protected theorem div_lt_iff_lt_mul {m n k : ℕ} (H : k > 0) : m / k < n ↔ m < n * k := iff.intro (!nat.lt_mul_of_div_lt H) !nat.div_lt_of_lt_mul 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 := + m / n ≤ k ↔ m ≤ k * n := by rewrite [propext (!le_iff_mul_le_mul_right H), !nat.div_mul_cancel H'] -protected 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 / n ≤ k) : m ≤ k * n := 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 := + (m * n - (k + 1)) / m = n - k / m - 1 := begin - have H1 : k div m < n, from nat.div_lt_of_lt_mul (!mul.comm ▸ H), - have H2 : n - k div m ≥ 1, from + have H1 : k / m < n, from nat.div_lt_of_lt_mul (!mul.comm ▸ H), + have H2 : n - k / m ≥ 1, from 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 (nat.sub_add_cancel H2)⁻¹, + 1 + k / m = succ (k / m) : add.comm + ... ≤ n : succ_le_of_lt H1), + have H3 : n - k / m = n - k / 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 nat.sub_lt_self H4 !succ_pos, + have H5 : k % m + 1 ≤ m, from succ_le_of_lt (!mod_lt H4), + have H6 : m - (k % 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 [*nat.sub_sub] - ... = ((n - k div m) * m - (k mod m + 1)) div m : + (m * n - (k + 1)) / m = (m * n - (k / m * m + k % m + 1)) / m : eq_div_mul_add_mod + ... = (m * n - k / m * m - (k % m + 1)) / m : by rewrite [*nat.sub_sub] + ... = ((n - k / m) * m - (k % m + 1)) / m : by rewrite [mul.comm m, nat.mul_sub_right_distrib] - ... = ((n - k div m - 1) * m + m - (k mod m + 1)) div m : + ... = ((n - k / m - 1) * m + m - (k % m + 1)) / m : by rewrite [H3 at {1}, right_distrib, nat.one_mul] - ... = ((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) : + ... = ((n - k / m - 1) * m + (m - (k % m + 1))) / m : {nat.add_sub_assoc H5 _} + ... = (m - (k % m + 1)) / m + (n - k / m - 1) : by rewrite [add.comm, (add_mul_div_self H4)] - ... = n - k div m - 1 : + ... = n - k / m - 1 : by rewrite [div_eq_zero_of_lt H6, zero_add] end -private lemma div_div_aux (a b c : nat) : b > 0 → c > 0 → (a div b) div c = a div (b * c) := +private lemma div_div_aux (a b c : nat) : b > 0 → c > 0 → (a / b) / c = a / (b * c) := suppose b > 0, suppose c > 0, nat.strong_induction_on a (λ a ih, - let k₁ := a div (b*c) in - let k₂ := a mod (b*c) in + let k₁ := a / (b*c) in + let k₂ := a %(b*c) in assert bc_pos : b*c > 0, from mul_pos `b > 0` `c > 0`, assert k₂ < b * c, from mod_lt _ bc_pos, assert k₂ ≤ a, from !mod_le, @@ -580,24 +580,24 @@ 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 nat.div_lt_of_lt_mul i₁, + assert a / 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` + show (a / b) / c = 0, from div_eq_zero_of_lt `a / b < c` end) (suppose k₂ < a, assert a = k₁*(b*c) + k₂, from eq_div_mul_add_mod a (b*c), - assert a div b = k₁*c + k₂ div b, by + assert a / b = k₁*c + k₂ / b, by rewrite [this at {1}, mul.comm b c at {2}, -mul.assoc, add.comm, add_mul_div_self `b > 0`, add.comm], - assert e₁ : (a div b) div c = k₁ + (k₂ div b) div c, by + assert e₁ : (a / b) / c = k₁ + (k₂ / b) / c, by rewrite [this, add.comm, add_mul_div_self `c > 0`, add.comm], - assert e₂ : (k₂ div b) div c = k₂ div (b * c), from ih k₂ `k₂ < a`, - assert e₃ : k₂ div (b * c) = 0, from div_eq_zero_of_lt `k₂ < b * c`, - assert (k₂ div b) div c = 0, by rewrite [e₂, e₃], - show (a div b) div c = k₁, by rewrite [e₁, this])) + assert e₂ : (k₂ / b) / c = k₂ / (b * c), from ih k₂ `k₂ < a`, + assert e₃ : k₂ / (b * c) = 0, from div_eq_zero_of_lt `k₂ < b * c`, + assert (k₂ / b) / c = 0, by rewrite [e₂, e₃], + show (a / b) / c = k₁, by rewrite [e₁, this])) -protected 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 / b) / c = a / (b * c) := begin cases b with b, rewrite [zero_mul, *nat.div_zero, nat.zero_div], @@ -606,7 +606,7 @@ begin apply div_div_aux a (succ b) (succ c) dec_trivial dec_trivial end -lemma div_lt_of_ne_zero : ∀ {n : nat}, n ≠ 0 → n div 2 < n +lemma div_lt_of_ne_zero : ∀ {n : nat}, n ≠ 0 → n / 2 < n | 0 h := absurd rfl h | (succ n) h := begin diff --git a/library/data/nat/examples/partial_sum.lean b/library/data/nat/examples/partial_sum.lean index f8b02c638..f50793686 100644 --- a/library/data/nat/examples/partial_sum.lean +++ b/library/data/nat/examples/partial_sum.lean @@ -26,8 +26,8 @@ lemma two_mul_partial_sum_eq : ∀ n, 2 * partial_sum n = (succ n) * n ... = (n + 2) * succ n : add.comm ... = (succ (succ n)) * succ n : rfl -theorem partial_sum_eq : ∀ n, partial_sum n = ((n + 1) * n) div 2 := +theorem partial_sum_eq : ∀ n, partial_sum n = ((n + 1) * n) / 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 * partial_sum n) / 2 = ((succ n) * n) / 2, by rewrite two_mul_partial_sum_eq, assert h₂ : (2:nat) > 0, from dec_trivial, 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 6f17e3987..422ec7f2d 100644 --- a/library/data/nat/gcd.lean +++ b/library/data/nat/gcd.lean @@ -20,25 +20,25 @@ intro_k (measure.wf pr₂) 20 -- we use intro_k to be able to execute gcd effic local attribute pair_nat.lt.wf [instance] -- instance will not be saved in .olean local infixl ` ≺ `:50 := pair_nat.lt -private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) := +private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x % succ y₁) ≺ (x, succ y₁) := !mod_lt (succ_pos y₁) definition gcd.F : Π (p₁ : nat × nat), (Π p₂ : nat × nat, p₂ ≺ p₁ → nat) → nat | (x, 0) f := x -| (x, succ y) f := f (succ y, x mod succ y) !gcd.lt.dec +| (x, succ y) f := f (succ y, x % succ y) !gcd.lt.dec definition gcd (x y : nat) := fix gcd.F (x, y) theorem gcd_zero_right (x : nat) : gcd x 0 = x := rfl -theorem gcd_succ (x y : nat) : gcd x (succ y) = gcd (succ y) (x mod succ y) := +theorem gcd_succ (x y : nat) : gcd x (succ y) = gcd (succ y) (x % succ y) := well_founded.fix_eq gcd.F (x, succ y) theorem gcd_one_right (n : ℕ) : gcd n 1 = 1 := -calc gcd n 1 = gcd 1 (n mod 1) : gcd_succ - ... = gcd 1 0 : mod_one +calc gcd n 1 = gcd 1 (n % 1) : gcd_succ + ... = gcd 1 0 : mod_one -theorem gcd_def (x : ℕ) : Π (y : ℕ), gcd x y = if y = 0 then x else gcd y (x mod y) +theorem gcd_def (x : ℕ) : Π (y : ℕ), gcd x y = if y = 0 then x else gcd y (x % y) | 0 := !gcd_zero_right | (succ y) := !gcd_succ ⬝ (if_neg !succ_ne_zero)⁻¹ @@ -46,29 +46,29 @@ theorem gcd_def (x : ℕ) : Π (y : ℕ), gcd x y = if y = 0 then x else gcd y ( theorem gcd_self : Π (n : ℕ), gcd n n = n | 0 := rfl | (succ n₁) := calc - gcd (succ n₁) (succ n₁) = gcd (succ n₁) (succ n₁ mod succ n₁) : gcd_succ + gcd (succ n₁) (succ n₁) = gcd (succ n₁) (succ n₁ % succ n₁) : gcd_succ ... = gcd (succ n₁) 0 : mod_self theorem gcd_zero_left : Π (n : ℕ), gcd 0 n = n | 0 := rfl | (succ n₁) := calc - gcd 0 (succ n₁) = gcd (succ n₁) (0 mod succ n₁) : gcd_succ + gcd 0 (succ n₁) = gcd (succ n₁) (0 % succ n₁) : gcd_succ ... = gcd (succ n₁) 0 : zero_mod -theorem gcd_of_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) := +theorem gcd_of_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m % n) := gcd_def m n ⬝ if_neg (ne_zero_of_pos H) -theorem gcd_rec (m n : ℕ) : gcd m n = gcd n (m mod n) := +theorem gcd_rec (m n : ℕ) : gcd m n = gcd n (m % n) := by_cases_zero_pos n (calc - m = gcd 0 m : gcd_zero_left - ... = gcd 0 (m mod 0) : mod_zero) + m = gcd 0 m : gcd_zero_left + ... = gcd 0 (m % 0) : mod_zero) (take n, assume H : 0 < n, gcd_of_pos m H) theorem gcd.induction {P : ℕ → ℕ → Prop} (m n : ℕ) (H0 : ∀m, P m 0) - (H1 : ∀m n, 0 < n → P n (m mod n) → P m n) : + (H1 : ∀m n, 0 < n → P n (m % n) → P m n) : P m n := induction (m, n) (prod.rec (λm, nat.rec (λ IH, H0 m) (λ n₁ v (IH : ∀p₂, p₂ ≺ (m, succ n₁) → P (pr₁ p₂) (pr₂ p₂)), @@ -78,10 +78,10 @@ theorem gcd_dvd (m n : ℕ) : (gcd m n ∣ m) ∧ (gcd m n ∣ n) := gcd.induction m n (take m, and.intro (!one_mul ▸ !dvd_mul_left) !dvd_zero) (take m n (npos : 0 < n), and.rec - (assume (IH₁ : gcd n (m mod n) ∣ n) (IH₂ : gcd n (m mod n) ∣ (m mod n)), - have H : (gcd n (m mod n) ∣ (m div n * n + m mod n)), from + (assume (IH₁ : gcd n (m % n) ∣ n) (IH₂ : gcd n (m % n) ∣ (m % n)), + have H : (gcd n (m % n) ∣ (m / n * n + m % n)), from dvd_add (dvd.trans IH₁ !dvd_mul_left) IH₂, - have H1 : (gcd n (m mod n) ∣ m), from !eq_div_mul_add_mod⁻¹ ▸ H, + have H1 : (gcd n (m % n) ∣ m), from !eq_div_mul_add_mod⁻¹ ▸ H, show (gcd m n ∣ m) ∧ (gcd m n ∣ n), from !gcd_rec⁻¹ ▸ (and.intro H1 IH₁))) theorem gcd_dvd_left (m n : ℕ) : gcd m n ∣ m := and.left !gcd_dvd @@ -91,10 +91,10 @@ theorem gcd_dvd_right (m n : ℕ) : gcd m n ∣ n := and.right !gcd_dvd theorem dvd_gcd {m n k : ℕ} : k ∣ m → k ∣ n → k ∣ gcd m n := gcd.induction m n (take m, imp.intro) (take m n (npos : n > 0) - (IH : k ∣ n → k ∣ m mod n → k ∣ gcd n (m mod n)) + (IH : k ∣ n → k ∣ m % n → k ∣ gcd n (m % 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 nat.dvd_of_dvd_add_left H3 (dvd.trans H2 !dvd_mul_left), + have H3 : k ∣ m / n * n + m % n, from !eq_div_mul_add_mod ▸ H1, + have H4 : k ∣ m % 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 := @@ -119,12 +119,12 @@ gcd.induction n k (take n, calc gcd (m * n) (m * 0) = gcd (m * n) 0 : mul_zero) (take n k, assume H : 0 < k, - assume IH : gcd (m * k) (m * (n mod k)) = m * gcd k (n mod k), + assume IH : gcd (m * k) (m * (n % k)) = m * gcd k (n % k), calc - gcd (m * n) (m * k) = gcd (m * k) (m * n mod (m * k)) : !gcd_rec - ... = gcd (m * k) (m * (n mod k)) : mul_mod_mul_left - ... = m * gcd k (n mod k) : IH - ... = m * gcd n k : !gcd_rec) + gcd (m * n) (m * k) = gcd (m * k) (m * n % (m * k)) : !gcd_rec + ... = gcd (m * k) (m * (n % k)) : mul_mod_mul_left + ... = m * gcd k (n % k) : IH + ... = m * gcd n k : !gcd_rec) theorem gcd_mul_right (m n k : ℕ) : gcd (m * n) (k * n) = gcd m k * n := calc @@ -148,13 +148,13 @@ theorem eq_zero_of_gcd_eq_zero_right {m n : ℕ} (H : gcd m n = 0) : n = 0 := 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 := + gcd (m / k) (n / k) = gcd m n / k := or.elim (eq_zero_or_pos k) (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))⁻¹) + gcd m n = gcd m (n / k * k) : nat.div_mul_cancel H2 + ... = gcd (m / k * k) (n / k * k) : nat.div_mul_cancel H1 + ... = gcd (m / k) (n / k) * k : gcd_mul_right))⁻¹) theorem gcd_dvd_gcd_mul_left (m n k : ℕ) : gcd m n ∣ gcd (k * m) n := dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right @@ -170,42 +170,42 @@ theorem gcd_dvd_gcd_mul_right_right (m n k : ℕ) : gcd m n ∣ gcd m (n * k) := /- lcm -/ -definition lcm (m n : ℕ) : ℕ := m * n div (gcd m n) +definition lcm (m n : ℕ) : ℕ := m * n / (gcd m n) theorem lcm.comm (m n : ℕ) : lcm m n = lcm n m := calc - lcm m n = m * n div gcd m n : rfl - ... = n * m div gcd m n : mul.comm - ... = n * m div gcd n m : gcd.comm + lcm m n = m * n / gcd m n : rfl + ... = n * m / gcd m n : mul.comm + ... = n * m / gcd n m : gcd.comm ... = lcm n m : rfl 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 + lcm 0 m = 0 * m / gcd 0 m : rfl + ... = 0 / gcd 0 m : zero_mul ... = 0 : nat.zero_div theorem lcm_zero_right (m : ℕ) : lcm m 0 = 0 := !lcm.comm ▸ !lcm_zero_left theorem lcm_one_left (m : ℕ) : lcm 1 m = m := calc - lcm 1 m = 1 * m div gcd 1 m : rfl - ... = m div gcd 1 m : one_mul - ... = m div 1 : gcd_one_left + lcm 1 m = 1 * m / gcd 1 m : rfl + ... = m / gcd 1 m : one_mul + ... = m / 1 : gcd_one_left ... = 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 +have H : m * m / m = m, from 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 + lcm m m = m * m / gcd m m : rfl + ... = m * m / 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 nat.mul_div_assoc _ !gcd_dvd_right, +have H : lcm m n = m * (n / gcd m n), from nat.mul_div_assoc _ !gcd_dvd_right, dvd.intro H⁻¹ theorem dvd_lcm_right (m n : ℕ) : n ∣ lcm m n := @@ -299,9 +299,9 @@ theorem gcd_mul_right_cancel_of_coprime_right {k m : ℕ} (n : ℕ) (H : coprime !gcd.comm ▸ !gcd.comm ▸ !gcd_mul_right_cancel_of_coprime H theorem coprime_div_gcd_div_gcd {m n : ℕ} (H : gcd m n > 0) : - coprime (m div gcd m n) (n div gcd m n) := + coprime (m / gcd m n) (n / 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 + gcd (m / gcd m n) (n / gcd m n) = gcd m n / gcd m n : gcd_div !gcd_dvd_left !gcd_dvd_right ... = 1 : nat.div_self H theorem not_coprime_of_dvd_of_dvd {m n d : ℕ} (dgt1 : d > 1) (Hm : d ∣ m) (Hn : d ∣ 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 (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)⁻¹, +have H1 : m = (m / gcd m n) * gcd m n, from (nat.div_mul_cancel !gcd_dvd_left)⁻¹, +have H2 : n = (n / 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 nat.div_dvd_div H2 H, - have H4 : (m * n) div gcd k m = (m div gcd k m) * n, from + have H3 : k / gcd k m ∣ (m * n) / gcd k m, from nat.div_dvd_div H2 H, + have H4 : (m * n) / gcd k m = (m / 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) : !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 (nat.mul_div_cancel' H2)⁻¹, + m * n / gcd k m = n * m / gcd k m : mul.comm + ... = n * (m / gcd k m) : !nat.mul_div_assoc !gcd_dvd_right + ... = m / gcd k m * n : mul.comm, + have H5 : k / gcd k m ∣ (m / gcd k m) * n, from H4 ▸ H3, + have H6 : coprime (k / gcd k m) (m / gcd k m), from coprime_div_gcd_div_gcd H1, + have H7 : k / gcd k m ∣ n, from dvd_of_coprime_of_dvd_mul_left H6 H5, + have H8 : k = gcd k m * (k / 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/parity.lean b/library/data/nat/parity.lean index 01a440e95..5ad13ab71 100644 --- a/library/data/nat/parity.lean +++ b/library/data/nat/parity.lean @@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -Parity +Parity. -/ import data.nat.power logic.identities @@ -11,7 +11,7 @@ namespace nat open decidable open algebra -definition even (n : nat) := n mod 2 = 0 +definition even (n : nat) := n % 2 = 0 definition decidable_even [instance] : ∀ n, decidable (even n) := take n, !nat.has_decidable_eq @@ -77,22 +77,22 @@ lemma eq_1_of_ne_0_lt_2 : ∀ {n : nat}, n ≠ 0 → n < 2 → n = 1 | 1 h₁ h₂ := rfl | (n+2) h₁ h₂ := absurd (lt_of_succ_lt_succ (lt_of_succ_lt_succ h₂)) !not_lt_zero -lemma mod_eq_of_odd {n} : odd n → n mod 2 = 1 := +lemma mod_eq_of_odd {n} : odd n → n % 2 = 1 := suppose odd n, - have ¬ n mod 2 = 0, from this, - have n mod 2 < 2, from mod_lt n dec_trivial, - eq_1_of_ne_0_lt_2 `¬ n mod 2 = 0` `n mod 2 < 2` + have ¬ n % 2 = 0, from this, + have n % 2 < 2, from mod_lt n dec_trivial, + eq_1_of_ne_0_lt_2 `¬ n % 2 = 0` `n % 2 < 2` -lemma odd_of_mod_eq {n} : n mod 2 = 1 → odd n := -suppose n mod 2 = 1, +lemma odd_of_mod_eq {n} : n % 2 = 1 → odd n := +suppose n % 2 = 1, by_contradiction (suppose ¬ odd n, - assert n mod 2 = 0, from even_of_not_odd this, + assert n % 2 = 0, from even_of_not_odd this, by rewrite this at *; contradiction) lemma even_succ_of_odd {n} : odd n → even (succ n) := suppose odd n, - assert n mod 2 = 1 mod 2, from mod_eq_of_odd this, - assert (n+1) mod 2 = 2 mod 2, from add_mod_eq_add_mod_right 1 this, + assert n % 2 = 1 % 2, from mod_eq_of_odd this, + assert (n+1) % 2 = 2 % 2, from add_mod_eq_add_mod_right 1 this, by rewrite mod_self at this; exact this lemma odd_succ_succ_of_odd {n} : odd n → odd (succ (succ n)) := @@ -175,7 +175,7 @@ assume h, by_contradiction (λ hn, have ∃ k, n = 2 * k, from exists_of_even this, obtain k₁ (hk₁ : n = 2 * k₁ + 1), from h, obtain k₂ (hk₂ : n = 2 * k₂), from this, - assert (2 * k₁ + 1) mod 2 = (2 * k₂) mod 2, by rewrite [-hk₁, -hk₂], + assert (2 * k₁ + 1) % 2 = (2 * k₂) % 2, by rewrite [-hk₁, -hk₂], begin rewrite [mul_mod_right at this, add.comm at this, add_mul_mod_self_left at this], contradiction @@ -189,7 +189,8 @@ even_of_exists (exists.intro (k₁+k₂) (by rewrite [hk₁, hk₂, left_distrib lemma even_add_of_odd_of_odd {n m} : odd n → odd m → even (n+m) := suppose odd n, suppose odd m, -assert even (succ n + succ m), from even_add_of_even_of_even (even_succ_of_odd `odd n`) (even_succ_of_odd `odd m`), +assert even (succ n + succ m), + from even_add_of_even_of_even (even_succ_of_odd `odd n`) (even_succ_of_odd `odd m`), have even(succ (succ (n + m))), by rewrite [add_succ at this, succ_add at this]; exact this, even_of_even_succ_succ this @@ -259,7 +260,7 @@ by_contradiction have odd (n^m), from odd_pow this, show false, from this `even (n^m)`) -lemma eq_of_div2_of_even {n m : nat} : n div 2 = m div 2 → (even n ↔ even m) → n = m := +lemma eq_of_div2_of_even {n m : nat} : n / 2 = m / 2 → (even n ↔ even m) → n = m := assume h₁ h₂, or.elim (em (even n)) (suppose even n, or.elim (em (even m)) @@ -274,13 +275,15 @@ assume h₁ h₂, (suppose odd n, or.elim (em (even m)) (suppose even m, absurd `odd n` (not_odd_of_even (iff.mpr h₂ `even m`))) (suppose odd m, - assert d : 1 div 2 = (0:nat), from dec_trivial, + assert d : 1 / 2 = (0:nat), from dec_trivial, obtain w₁ (hw₁ : n = 2*w₁ + 1), from exists_of_odd `odd n`, obtain w₂ (hw₂ : m = 2*w₂ + 1), from exists_of_odd `odd m`, begin substvars, - rewrite [add.comm at h₁, add_mul_div_self_left _ _ (dec_trivial : 2 > 0) at h₁, d at h₁, zero_add at h₁], - rewrite [add.comm at h₁, add_mul_div_self_left _ _ (dec_trivial : 2 > 0) at h₁, d at h₁, zero_add at h₁], + rewrite [add.comm at h₁, add_mul_div_self_left _ _ (dec_trivial : 2 > 0) at h₁, d at h₁, + zero_add at h₁], + rewrite [add.comm at h₁, add_mul_div_self_left _ _ (dec_trivial : 2 > 0) at h₁, d at h₁, + zero_add at h₁], rewrite h₁ end)) end nat diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean index 2944e3869..0526d5d6c 100644 --- a/library/data/nat/power.lean +++ b/library/data/nat/power.lean @@ -56,7 +56,7 @@ theorem mul_self_eq_pow_2 (a : nat) : a * a = a ^ 2 := show a * a = a ^ (succ (succ zero)), from by rewrite [*pow_succ, *pow_zero, mul_one] -theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → a^b = a^c → b = c +theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → a ^ b = a ^ c → b = c | a 0 0 h₁ h₂ := rfl | a (succ b) 0 h₁ h₂ := assert a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂), @@ -71,7 +71,7 @@ theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → a^b = a^c → b = c assert a^b = a^c, by rewrite [*pow_succ at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero this) h₂), by rewrite [pow_cancel_left h₁ this] -theorem pow_div_cancel : ∀ {a b : nat}, a ≠ 0 → (a ^ succ b) div a = a ^ b +theorem pow_div_cancel : ∀ {a b : nat}, a ≠ 0 → (a ^ succ b) / a = a ^ b | 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)] @@ -83,13 +83,13 @@ lemma dvd_pow_of_dvd_of_pos : ∀ {i j n : nat}, i ∣ j → n > 0 → i ∣ j^n | i j 0 h₁ h₂ := absurd h₂ !lt.irrefl | i j (succ n) h₁ h₂ := by rewrite [pow_succ']; apply dvd_mul_of_dvd_right h₁ -lemma pow_mod_eq_zero (i : nat) {n : nat} (h : n > 0) : (i^n) mod i = 0 := +lemma pow_mod_eq_zero (i : nat) {n : nat} (h : n > 0) : (i ^ n) % i = 0 := 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), - by rewrite [pow_succ']; apply nat.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) : diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 442d6763c..0f5c30900 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -286,9 +286,9 @@ by esimp [mul, of_int, equiv]; rewrite [*int.mul_one] definition reduce : prerat → prerat | (mk an ad adpos) := - have pos : ad div gcd an ad > 0, from div_pos_of_pos_of_dvd adpos !gcd_nonneg !gcd_dvd_right, + have pos : ad / gcd an ad > 0, from div_pos_of_pos_of_dvd adpos !gcd_nonneg !gcd_dvd_right, if an = 0 then prerat.zero - else mk (an div gcd an ad) (ad div gcd an ad) pos + else mk (an / gcd an ad) (ad / gcd an ad) pos protected theorem eq {a b : prerat} (Hn : num a = num b) (Hd : denom a = denom b) : a = b := begin @@ -306,10 +306,10 @@ 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, -!int.mul_div_assoc + 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 +theorem reduce_eq_reduce : ∀ {a b : prerat}, a ≡ b → reduce a = reduce b | (mk an ad adpos) (mk bn bd bdpos) := assume H : an * bd = bn * ad, decidable.by_cases @@ -575,8 +575,8 @@ protected definition discrete_field [reducible] [trans_instance] : algebra.discr inv_zero := rat.inv_zero, has_decidable_eq := has_decidable_eq⦄ -definition rat_has_division [instance] [reducible] [priority rat.prio] : has_division rat := -has_division.mk has_division.division +definition rat_has_div [instance] [reducible] [priority rat.prio] : has_div rat := +has_div.mk has_div.div definition rat_has_pow_nat [instance] [reducible] [priority rat.prio] : has_pow_nat rat := has_pow_nat.mk has_pow_nat.pow_nat @@ -585,19 +585,19 @@ theorem eq_num_div_denom (a : ℚ) : a = num a / denom a := have H : of_int (denom a) ≠ 0, from assume H', ne_of_gt (denom_pos a) (of_int.inj H'), 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 := +theorem of_int_div {a b : ℤ} (H : b ∣ a) : of_int (a / b) = of_int a / of_int b := decidable.by_cases (assume bz : b = 0, 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 + have H' : of_int (a / b) * of_int b = of_int a, from dvd.elim H (take c, assume Hc : a = b * c, by rewrite [Hc, !int.mul_div_cancel_left bnz, mul.comm]), iff.mpr (!eq_div_iff_mul_eq bnz') H') -theorem of_nat_div {a b : ℕ} (H : b ∣ a) : of_nat (a div b) = of_nat a / of_nat b := +theorem of_nat_div {a b : ℕ} (H : b ∣ a) : of_nat (a / b) = of_nat a / of_nat b := have H' : (int.of_nat b ∣ int.of_nat a), by rewrite [int.of_nat_dvd_of_nat_iff]; exact H, by+ rewrite [of_nat_eq, int.of_nat_div, of_int_div H'] diff --git a/library/data/real/division.lean b/library/data/real/division.lean index f3024349d..0db408acc 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -274,7 +274,7 @@ theorem s_inv_ne_zero {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) apply pnat.mul_le_mul_left end) -protected theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : +protected theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv Hs) ≡ one := begin let Rsi := reg_inv_reg Hs Hsep, @@ -330,7 +330,7 @@ protected theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : apply pnat.mul_le_mul_right end -protected theorem inv_mul {s : seq} (Hs : regular s) (Hsep : sep s zero) : +protected theorem inv_mul {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul (s_inv Hs) s ≡ one := begin apply equiv.trans, @@ -545,7 +545,7 @@ theorem s_le_of_equiv_le_right {s t u : seq} (Hs : regular s) (Ht : regular t) ( noncomputable definition r_inv (s : reg_seq) : reg_seq := reg_seq.mk (s_inv (reg_seq.is_reg s)) (if H : sep (reg_seq.sq s) zero then reg_inv_reg (reg_seq.is_reg s) H else - assert Hz : s_inv (reg_seq.is_reg s) = zero, from funext (λ n, dif_neg H), + assert Hz : s_inv (reg_seq.is_reg s) = zero, from funext (λ n, dif_neg H), by rewrite Hz; apply zero_is_reg) theorem r_inv_zero : requiv (r_inv r_zero) r_zero := @@ -583,19 +583,18 @@ end rat_seq namespace real open [classes] rat_seq -noncomputable protected definition inv (x : ℝ) : ℝ := +noncomputable protected definition inv (x : ℝ) : ℝ := quot.lift_on x (λ a, quot.mk (rat_seq.r_inv a)) (λ a b H, quot.sound (rat_seq.r_inv_well_defined H)) noncomputable definition real_has_inv [instance] [reducible] [priority real.prio] : has_inv real := has_inv.mk real.inv -noncomputable protected definition division (x y : ℝ) : ℝ := +noncomputable protected definition div (x y : ℝ) : ℝ := x * y⁻¹ -noncomputable definition real_has_division [instance] [reducible] [priority real.prio] : - has_division real := -has_division.mk real.division +noncomputable definition real_has_div [instance] [reducible] [priority real.prio] : has_div real := + has_div.mk real.div protected theorem le_total (x y : ℝ) : x ≤ y ∨ y ≤ x := quot.induction_on₂ x y (λ s t, rat_seq.r_le_total s t) @@ -615,10 +614,10 @@ theorem sep_of_neq {x y : ℝ} : ¬ x = y → x ≢ y := theorem sep_is_neq (x y : ℝ) : (x ≢ y) = (¬ x = y) := propext (iff.intro neq_of_sep sep_of_neq) -protected theorem mul_inv_cancel (x : ℝ) : x ≠ 0 → x * x⁻¹ = 1 := +protected theorem mul_inv_cancel (x : ℝ) : x ≠ 0 → x * x⁻¹ = 1 := !sep_is_neq ▸ !real.mul_inv_cancel' -protected theorem inv_mul_cancel (x : ℝ) : x ≠ 0 → x⁻¹ * x = 1 := +protected theorem inv_mul_cancel (x : ℝ) : x ≠ 0 → x⁻¹ * x = 1 := !sep_is_neq ▸ !real.inv_mul_cancel' protected theorem inv_zero : (0 : ℝ)⁻¹ = 0 := quot.sound (rat_seq.r_inv_zero) @@ -663,10 +662,10 @@ by_cases open int -theorem of_int_div (x y : ℤ) (H : (#int y ∣ x)) : of_int ((x div y)) = of_int x / of_int y := +theorem of_int_div (x y : ℤ) (H : y ∣ x) : of_int (x / y) = of_int x / of_int y := by rewrite [of_int_eq, rat.of_int_div H, of_rat_divide] -theorem of_nat_div (x y : ℕ) (H : (#nat y ∣ x)) : of_nat (x div y) = of_nat x / of_nat y := +theorem of_nat_div (x y : ℕ) (H : y ∣ x) : of_nat (x / y) = of_nat x / of_nat y := by rewrite [of_nat_eq, rat.of_nat_div H, of_rat_divide] /- useful for proving equalities -/ diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 21ab2e297..658cc80ad 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -10,32 +10,31 @@ notation `assume` binders `,` r:(scoped f, f) := r notation `take` binders `,` r:(scoped f, f) := r structure has_zero [class] (A : Type) := (zero : A) -structure has_one [class] (A : Type) := (one : A) -structure has_add [class] (A : Type) := (add : A → A → A) -structure has_mul [class] (A : Type) := (mul : A → A → A) -structure has_inv [class] (A : Type) := (inv : A → A) -structure has_neg [class] (A : Type) := (neg : A → A) -structure has_sub [class] (A : Type) := (sub : A → A → A) -structure has_division [class] (A : Type) := (division : A → A → A) -structure has_divide [class] (A : Type) := (divide : A → A → A) -structure has_modulo [class] (A : Type) := (modulo : A → A → A) -structure has_dvd [class] (A : Type) := (dvd : A → A → Prop) -structure has_le [class] (A : Type) := (le : A → A → Prop) -structure has_lt [class] (A : Type) := (lt : A → A → Prop) +structure has_one [class] (A : Type) := (one : A) +structure has_add [class] (A : Type) := (add : A → A → A) +structure has_mul [class] (A : Type) := (mul : A → A → A) +structure has_inv [class] (A : Type) := (inv : A → A) +structure has_neg [class] (A : Type) := (neg : A → A) +structure has_sub [class] (A : Type) := (sub : A → A → A) +structure has_div [class] (A : Type) := (div : A → A → A) +structure has_dvd [class] (A : Type) := (dvd : A → A → Prop) +structure has_mod [class] (A : Type) := (mod : A → A → A) +structure has_le [class] (A : Type) := (le : A → A → Prop) +structure has_lt [class] (A : Type) := (lt : A → A → Prop) + +definition zero {A : Type} [s : has_zero A] : A := has_zero.zero A +definition one {A : Type} [s : has_one A] : A := has_one.one A +definition add {A : Type} [s : has_add A] : A → A → A := has_add.add +definition mul {A : Type} [s : has_mul A] : A → A → A := has_mul.mul +definition sub {A : Type} [s : has_sub A] : A → A → A := has_sub.sub +definition div {A : Type} [s : has_div A] : A → A → A := has_div.div +definition dvd {A : Type} [s : has_dvd A] : A → A → Prop := has_dvd.dvd +definition mod {A : Type} [s : has_mod A] : A → A → A := has_mod.mod +definition neg {A : Type} [s : has_neg A] : A → A := has_neg.neg +definition inv {A : Type} [s : has_inv A] : A → A := has_inv.inv +definition le {A : Type} [s : has_le A] : A → A → Prop := has_le.le +definition lt {A : Type} [s : has_lt A] : A → A → Prop := has_lt.lt -definition zero {A : Type} [s : has_zero A] : A := has_zero.zero A -definition one {A : Type} [s : has_one A] : A := has_one.one A -definition add {A : Type} [s : has_add A] : A → A → A := has_add.add -definition mul {A : Type} [s : has_mul A] : A → A → A := has_mul.mul -definition sub {A : Type} [s : has_sub A] : A → A → A := has_sub.sub -definition division {A : Type} [s : has_division A] : A → A → A := has_division.division -definition divide {A : Type} [s : has_divide A] : A → A → A := has_divide.divide -definition modulo {A : Type} [s : has_modulo A] : A → A → A := has_modulo.modulo -definition dvd {A : Type} [s : has_dvd A] : A → A → Prop := has_dvd.dvd -definition neg {A : Type} [s : has_neg A] : A → A := has_neg.neg -definition inv {A : Type} [s : has_inv A] : A → A := has_inv.inv -definition le {A : Type} [s : has_le A] : A → A → Prop := has_le.le -definition lt {A : Type} [s : has_lt A] : A → A → Prop := has_lt.lt definition ge [reducible] {A : Type} [s : has_le A] (a b : A) : Prop := le b a definition gt [reducible] {A : Type} [s : has_lt A] (a b : A) : Prop := lt b a definition bit0 {A : Type} [s : has_add A] (a : A) : A := add a a @@ -164,9 +163,8 @@ reserve infixl ` × `:30 reserve infixl ` + `:65 reserve infixl ` - `:65 reserve infixl ` * `:70 -reserve infixl ` div `:70 -reserve infixl ` mod `:70 reserve infixl ` / `:70 +reserve infixl ` % `:70 reserve prefix `-`:100 reserve infix ` ^ `:80 @@ -200,10 +198,9 @@ reserve infixr ` :: `:65 infix + := add infix * := mul infix - := sub -infix / := division -infix div := divide +infix / := div infix ∣ := dvd -infix mod := modulo +infix % := mod prefix - := neg postfix ⁻¹ := inv infix ≤ := le @@ -211,13 +208,13 @@ infix ≥ := ge infix < := lt infix > := gt -notation [parsing_only] x ` +[`:65 A:0 `] `:0 y:65 := @add A _ x y -notation [parsing_only] x ` -[`:65 A:0 `] `:0 y:65 := @sub A _ x y -notation [parsing_only] x ` *[`:70 A:0 `] `:0 y:70 := @mul A _ x y -notation [parsing_only] x ` /[`:70 A:0 `] `:0 y:70 := @division A _ x y -notation [parsing_only] x ` div[`:70 A:0 `] `:0 y:70 := @divide A _ x y -notation [parsing_only] x ` mod[`:70 A:0 `] `:0 y:70 := @modulo A _ x y -notation [parsing_only] x ` ≤[`:50 A:0 `] `:0 y:50 := @le A _ x y -notation [parsing_only] x ` ≥[`:50 A:0 `] `:0 y:50 := @ge A _ x y -notation [parsing_only] x ` <[`:50 A:0 `] `:0 y:50 := @lt A _ x y -notation [parsing_only] x ` >[`:50 A:0 `] `:0 y:50 := @gt A _ x y +notation [parsing_only] x ` +[`:65 A:0 `] `:0 y:65 := @add A _ x y +notation [parsing_only] x ` -[`:65 A:0 `] `:0 y:65 := @sub A _ x y +notation [parsing_only] x ` *[`:70 A:0 `] `:0 y:70 := @mul A _ x y +notation [parsing_only] x ` /[`:70 A:0 `] `:0 y:70 := @div A _ x y +notation [parsing_only] x ` ∣[`:70 A:0 `] `:0 y:70 := @dvd A _ x y +notation [parsing_only] x ` %[`:70 A:0 `] `:0 y:70 := @mod A _ x y +notation [parsing_only] x ` ≤[`:50 A:0 `] `:0 y:50 := @le A _ x y +notation [parsing_only] x ` ≥[`:50 A:0 `] `:0 y:50 := @ge A _ x y +notation [parsing_only] x ` <[`:50 A:0 `] `:0 y:50 := @lt A _ x y +notation [parsing_only] x ` >[`:50 A:0 `] `:0 y:50 := @gt A _ x y diff --git a/library/theories/combinatorics/choose.lean b/library/theories/combinatorics/choose.lean index e43a42f5d..2815ec80a 100644 --- a/library/theories/combinatorics/choose.lean +++ b/library/theories/combinatorics/choose.lean @@ -112,7 +112,7 @@ begin end end -theorem choose_def_alt {n k : ℕ} (H : k ≤ n) : choose n k = fact n div (fact k * fact (n -k)) := +theorem choose_def_alt {n k : ℕ} (H : k ≤ n) : choose n k = fact n / (fact k * fact (n -k)) := 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])) diff --git a/library/theories/group_theory/cyclic.lean b/library/theories/group_theory/cyclic.lean index dc8f1ec54..752dd8150 100644 --- a/library/theories/group_theory/cyclic.lean +++ b/library/theories/group_theory/cyclic.lean @@ -20,17 +20,17 @@ variable {A : Type} variable [ambG : group A] include ambG -lemma pow_mod {a : A} {n m : nat} : a ^ m = 1 → a ^ n = a ^ (n mod m) := +lemma pow_mod {a : A} {n m : nat} : a ^ m = 1 → a ^ n = a ^ (n % m) := assume Pid, -assert a ^ (n div m * m) = 1, from calc - a ^ (n div m * m) = a ^ (m * (n div m)) : by rewrite (mul.comm (n div m) m) - ... = (a ^ m) ^ (n div m) : by rewrite pow_mul - ... = 1 ^ (n div m) : by rewrite Pid - ... = 1 : one_pow (n div m), -calc a ^ n = a ^ (n div m * m + n mod m) : by rewrite -(eq_div_mul_add_mod n m) - ... = a ^ (n div m * m) * a ^ (n mod m) : by rewrite pow_add - ... = 1 * a ^ (n mod m) : by rewrite this - ... = a ^ (n mod m) : by rewrite one_mul +assert a ^ (n / m * m) = 1, from calc + a ^ (n / m * m) = a ^ (m * (n / m)) : by rewrite (mul.comm (n / m) m) + ... = (a ^ m) ^ (n / m) : by rewrite pow_mul + ... = 1 ^ (n / m) : by rewrite Pid + ... = 1 : one_pow (n / m), +calc a ^ n = a ^ (n / m * m + n % m) : by rewrite -(eq_div_mul_add_mod n m) + ... = a ^ (n / m * m) * a ^ (n % m) : by rewrite pow_add + ... = 1 * a ^ (n % m) : by rewrite this + ... = a ^ (n % m) : by rewrite one_mul lemma pow_sub_eq_one_of_pow_eq {a : A} {i j : nat} : a^i = a^j → a^(i - j) = 1 := @@ -47,9 +47,9 @@ assume Pe, or.elim (lt_or_ge i j) lemma pow_madd {a : A} {n : nat} {i j : fin (succ n)} : a^(succ n) = 1 → a^(val (i + j)) = a^i * a^j := assume Pe, calc -a^(val (i + j)) = a^((i + j) mod (succ n)) : rfl - ... = a^(val i + val j) : by rewrite [-pow_mod Pe] - ... = a^i * a^j : by rewrite pow_add +a^(val (i + j)) = a^((i + j) % (succ n)) : rfl + ... = a^(val i + val j) : by rewrite [-pow_mod Pe] + ... = a^i * a^j : by rewrite pow_add lemma mk_pow_mod {a : A} {n m : nat} : a ^ (succ m) = 1 → a ^ n = a ^ (mk_mod m n) := assume Pe, pow_mod Pe @@ -113,7 +113,7 @@ obtain j Pjlt Pjh, from of_mem_sep Phin, begin rewrite [-Pig, -Pjh, -pow_add, pow_mod Pe], apply mem_sep_of_mem !mem_univ, - existsi ((i + j) mod (succ n)), apply and.intro, + existsi ((i + j) % (succ n)), apply and.intro, apply nat.lt_trans (mod_lt (i+j) !zero_lt_succ) (succ_lt_succ Plt), apply rfl end @@ -200,7 +200,7 @@ or.elim (eq_or_lt_of_le (order_le Pone)) (λ P, P) exact absurd (pow_order a) Pn end) lemma order_dvd_of_pow_eq_one {a : A} {n : nat} (Pone : a^n = 1) : order a ∣ n := -assert Pe : a^(n mod order a) = 1, from +assert Pe : a^(n % order a) = 1, from begin revert Pone, rewrite [eq_div_mul_add_mod n (order a) at {1}, pow_add, mul.comm _ (order a), pow_mul, pow_order, one_pow, one_mul], @@ -373,10 +373,10 @@ lemma rotl_perm_pow_eq : ∀ {i : nat}, (rotl_perm A n 1) ^ i = rotl_perm A n i lemma rotl_perm_pow_eq_one : (rotl_perm A n 1) ^ n = 1 := eq.trans rotl_perm_pow_eq (eq_of_feq begin esimp [rotl_perm], rewrite [↑rotl_fun, rotl_id] end) -lemma rotl_perm_mod {i : nat} : rotl_perm A n i = rotl_perm A n (i mod n) := -calc rotl_perm A n i = (rotl_perm A n 1) ^ i : by rewrite rotl_perm_pow_eq - ... = (rotl_perm A n 1) ^ (i mod n) : by rewrite (pow_mod rotl_perm_pow_eq_one) - ... = rotl_perm A n (i mod n) : by rewrite rotl_perm_pow_eq +lemma rotl_perm_mod {i : nat} : rotl_perm A n i = rotl_perm A n (i % n) := +calc rotl_perm A n i = (rotl_perm A n 1) ^ i : by rewrite rotl_perm_pow_eq + ... = (rotl_perm A n 1) ^ (i % n) : by rewrite (pow_mod rotl_perm_pow_eq_one) + ... = rotl_perm A n (i % n) : by rewrite rotl_perm_pow_eq -- needs A to have at least two elements! lemma rotl_perm_pow_ne_one (Pex : ∃ a b : A, a ≠ b) : ∀ i, i < n → (rotl_perm A (succ n) 1)^(succ i) ≠ 1 := diff --git a/library/theories/group_theory/pgroup.lean b/library/theories/group_theory/pgroup.lean index 2a5dc136f..ef02fdf52 100644 --- a/library/theories/group_theory/pgroup.lean +++ b/library/theories/group_theory/pgroup.lean @@ -3,8 +3,7 @@ Copyright (c) 2015 Haitao Zhang. All rights reserved. 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 +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 @@ -29,7 +28,7 @@ include Hom open finset.partition lemma card_mod_eq_of_action_by_psubg {p : nat} : - ∀ {m : nat}, psubg H p m → (card S) mod p = (card (fixed_points hom H)) mod p + ∀ {m : nat}, psubg H p m → (card S) % p = (card (fixed_points hom H)) % p | 0 := by rewrite [↑psubg, pow_zero]; intro Psubg; rewrite [finsubg_eq_singleton_one_of_card_one (and.right Psubg), fixed_points_of_one] | (succ m) := take Ppsubg, begin @@ -64,7 +63,7 @@ variables {H : finset G} [finsubgH : is_finsubg H] include finsubgH lemma card_psubg_cosets_mod_eq {p : nat} {m : nat} : - psubg H p m → (card (lcoset_type univ H)) mod p = card (lcoset_type (normalizer H) H) mod p := + psubg H p m → (card (lcoset_type univ H)) % p = card (lcoset_type (normalizer H) H) % p := assume Psubg, by rewrite [-card_aol_fixed_points_eq_card_cosets]; exact card_mod_eq_of_action_by_psubg Psubg end psubg_cosets @@ -258,7 +257,7 @@ lemma rotl_peo_seq_compose {n i j : nat} : (rotl_peo_seq A n i) ∘ (rotl_peo_seq A n j) = rotl_peo_seq A n (j + i) := funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, ↑rotl_perm, ↑rotl_fun, compose.assoc, rotl_compose] end -lemma rotl_peo_seq_mod {n i : nat} : rotl_peo_seq A n i = rotl_peo_seq A n (i mod succ n) := +lemma rotl_peo_seq_mod {n i : nat} : rotl_peo_seq A n i = rotl_peo_seq A n (i % succ n) := funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, rotl_perm_mod] end lemma rotl_peo_seq_inj {n m : nat} : injective (rotl_peo_seq A n m) := @@ -323,11 +322,11 @@ let pp := nat.pred p, spp := nat.succ pp in assert Peq : spp = p, from succ_pred_prime Pprime, assert Ppsubg : psubg (@univ (fin spp) _) spp 1, from and.intro (eq.symm Peq ▸ Pprime) (by rewrite [Peq, card_fin, pow_one]), -have (pow_nat (card A) pp) mod spp = (card (fixed_points (rotl_perm_ps A pp) univ)) mod spp, +have (pow_nat (card A) pp) % spp = (card (fixed_points (rotl_perm_ps A pp) univ)) % spp, by rewrite -card_peo_seq; apply card_mod_eq_of_action_by_psubg Ppsubg, -have Pcardmod : (pow_nat (card A) pp) mod p = (card (fixed_points (rotl_perm_ps A pp) univ)) mod p, +have Pcardmod : (pow_nat (card A) pp) % p = (card (fixed_points (rotl_perm_ps A pp) univ)) % p, from Peq ▸ this, -have Pfpcardmod : (card (fixed_points (rotl_perm_ps A pp) univ)) mod p = 0, +have Pfpcardmod : (card (fixed_points (rotl_perm_ps A pp) univ)) % p = 0, from eq.trans (eq.symm Pcardmod) (mod_eq_zero_of_dvd (dvd_pow_of_dvd_of_pos Pdvd (pred_prime_pos Pprime))), have Pfpcardpos : card (fixed_points (rotl_perm_ps A pp) univ) > 0, from card_pos_of_mem peo_seq_one_mem_fixed_points, diff --git a/library/theories/number_theory/bezout.lean b/library/theories/number_theory/bezout.lean index 95c6257ea..dd7cf7385 100644 --- a/library/theories/number_theory/bezout.lean +++ b/library/theories/number_theory/bezout.lean @@ -20,7 +20,7 @@ private definition pair_nat.lt.wf : well_founded pair_nat.lt := intro_k (measure local attribute pair_nat.lt.wf [instance] local infixl `≺`:50 := pair_nat.lt -private definition gcd.lt.dec (x y₁ : ℕ) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) := +private definition gcd.lt.dec (x y₁ : ℕ) : (succ y₁, x % succ y₁) ≺ (x, succ y₁) := !nat.mod_lt (succ_pos y₁) private definition egcd_rec_f (z : ℤ) : ℤ → ℤ → ℤ × ℤ := λ s t, (t, s - t * z) @@ -29,8 +29,8 @@ definition egcd.F : Π (p₁ : ℕ × ℕ), (Π p₂ : ℕ × ℕ, p₂ ≺ p₁ | (x, y) := nat.cases_on y (λ f, (1, 0) ) (λ y₁ (f : Π p₂, p₂ ≺ (x, succ y₁) → ℤ × ℤ), - let bz := f (succ y₁, x mod succ y₁) !gcd.lt.dec in - prod.cases_on bz (egcd_rec_f (x div succ y₁))) + let bz := f (succ y₁, x % succ y₁) !gcd.lt.dec in + prod.cases_on bz (egcd_rec_f (x / succ y₁))) definition egcd (x y : ℕ) := fix egcd.F (pair x y) @@ -38,12 +38,12 @@ theorem egcd_zero (x : ℕ) : egcd x 0 = (1, 0) := well_founded.fix_eq egcd.F (x, 0) theorem egcd_succ (x y : ℕ) : - egcd x (succ y) = prod.cases_on (egcd (succ y) (x mod succ y)) (egcd_rec_f (x div succ y)) := + egcd x (succ y) = prod.cases_on (egcd (succ y) (x % succ y)) (egcd_rec_f (x / succ y)) := well_founded.fix_eq egcd.F (x, succ y) theorem egcd_of_pos (x : ℕ) {y : ℕ} (ypos : y > 0) : - let erec := egcd y (x mod y), u := pr₁ erec, v := pr₂ erec in - egcd x y = (v, u - v * (x div y)) := + let erec := egcd y (x % y), u := pr₁ erec, v := pr₂ erec in + egcd x y = (v, u - v * (x / y)) := obtain (y' : nat) (yeq : y = succ y'), from exists_eq_succ_of_pos ypos, begin rewrite [yeq, egcd_succ, -prod.eta (egcd _ _)], @@ -64,11 +64,11 @@ gcd.induction x y rewrite [gcd_rec, -IH], rewrite [algebra.add.comm], rewrite [-of_nat_mod], - rewrite [int.modulo.def], + rewrite [int.mod_def], rewrite [+algebra.mul_sub_right_distrib], rewrite [+algebra.mul_sub_left_distrib, *left_distrib], - rewrite [*sub_eq_add_neg, {pr₂ (egcd n (m mod n)) * of_nat m + - _}algebra.add.comm, -algebra.add.assoc], - rewrite [algebra.mul.assoc] + rewrite [*sub_eq_add_neg, {pr₂ (egcd n (m % n)) * of_nat m + - _}algebra.add.comm], + rewrite [-algebra.add.assoc ,algebra.mul.assoc] end) theorem Bezout_aux (x y : ℕ) : ∃ a b : ℤ, a * x + b * y = gcd x y := diff --git a/library/theories/number_theory/irrational_roots.lean b/library/theories/number_theory/irrational_roots.lean index 482fbe782..81c2268b9 100644 --- a/library/theories/number_theory/irrational_roots.lean +++ b/library/theories/number_theory/irrational_roots.lean @@ -52,13 +52,13 @@ section (suppose b = 0, have a^n = 0, by rewrite [H, this, zero_pow npos], - assert a = 0, + 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, + take p, + suppose prime p, suppose p ∣ b, assert p ∣ b^n, from dvd_pow_of_dvd_of_pos `p ∣ b` `n > 0`, @@ -68,18 +68,18 @@ section 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, + show false, from this `coprime a b`, - have blt2 : b < 2, + have blt2 : b < 2, from by_contradiction (suppose ¬ b < 2, have b ≥ 2, from le_of_not_gt this, - obtain p [primep pdvdb], + obtain p [primep pdvdb], from exists_prime_and_dvd this, - show false, + show false, from H₁ p primep pdvdb), - show b = 1, + show b = 1, from (le.antisymm (le_of_lt_succ blt2) (succ_le_of_lt bpos)) end @@ -94,15 +94,15 @@ 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, + have b ≠ 0, from ne_of_gt (denom_pos q), - have bnz : b ≠ (0 : ℚ), + have bnz : b ≠ (0 : ℚ), from assume H, `b ≠ 0` (of_int.inj H), - have bnnz : ((b : rat)^n ≠ 0), + 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, + 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, + 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, @@ -110,35 +110,35 @@ section 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], + 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), + 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, + (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, + have qeq0 : q = 0, by rewrite [eq_num_div_denom, aeq0, of_int_zero, algebra.zero_div], - show false, + show false, from qne0 qeq0, have nat_abs a ≠ 0, from suppose nat_abs a = 0, - have aeq0 : a = 0, + 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, + 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, + 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], @@ -152,7 +152,7 @@ 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, + have npos : n > 0, from lt.trans dec_trivial ngt1, have pnez : p ≠ 0, from (suppose p = 0, @@ -165,11 +165,11 @@ 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, + have n ∣ 1, from dvd_of_mul_right_eq this, have n = 1, from eq_one_of_dvd_one this, - show false, using this, + show false, using this, by rewrite this at ngt1; exact !lt.irrefl ngt1 open int rat @@ -199,22 +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, + 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, + 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, + have a / (gcd a b) = c * b / gcd (c * b) a, from div_gcd_eq_div_gcd this bpos apos, - have a = c * b div gcd c a, using this, + have a = c * b / 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, + have a = b * (c / gcd c a), using this, by revert this; rewrite [mul.comm, !int.mul_div_assoc !gcd_dvd_left]; intros; assumption, - have b ∣ a, + have b ∣ a, from dvd_of_mul_right_eq this⁻¹, - have b ∣ gcd a b, + have b ∣ gcd a b, from dvd_gcd this !dvd.refl, - have b ∣ 1, using this, + have b ∣ 1, using this, by rewrite [↑coprime at co, co at this]; apply this, - show b = 1, + 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 354440a6a..e3385d71c 100644 --- a/library/theories/number_theory/prime_factorization.lean +++ b/library/theories/number_theory/prime_factorization.lean @@ -28,7 +28,7 @@ end /- multiplicity -/ -theorem mult_rec_decreasing {p n : ℕ} (Hp : p > 1) (Hn : n > 0) : n div p < n := +theorem mult_rec_decreasing {p n : ℕ} (Hp : p > 1) (Hn : n > 0) : n / p < n := have H' : n < n * p, by rewrite [-mul_one n at {1}]; apply mul_lt_mul_of_pos_left Hp Hn, nat.div_lt_of_lt_mul H' @@ -41,7 +41,7 @@ else 0 definition mult (p n : ℕ) : ℕ := fix (mult.F p) n theorem mult_rec {p n : ℕ} (pgt1 : p > 1) (ngt0 : n > 0) (pdivn : p ∣ n) : - mult p n = succ (mult p (n div p)) := + mult p n = succ (mult p (n / p)) := have (p > 1 ∧ n > 0) ∧ p ∣ n, from and.intro (and.intro pgt1 ngt0) pdivn, eq.trans (well_founded.fix_eq (mult.F p) n) (dif_pos this) @@ -95,11 +95,11 @@ begin (take n', suppose n = p * n', have p > 0, from lt.trans zero_lt_one pgt1, - assert n div p = n', from !nat.div_eq_of_eq_mul_right this `n = p * n'`, + assert n / 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 - rewrite [mult_rec pgt1 npos pdvdn, `n div p = n'`, pow_succ], subst n, + rewrite [mult_rec pgt1 npos pdvdn, `n / p = n'`, pow_succ], subst n, apply mul_dvd_mul !dvd.refl, apply ih _ this end) @@ -141,12 +141,12 @@ dvd.elim pidvd assert m > 0, from pos_of_mul_pos_left (this ▸ npos), by subst n; rewrite [mult_pow_mul i pgt1 this]; apply le_add_right) -theorem not_dvd_div_pow_mult {p n : ℕ} (pgt1 : p > 1) (npos : n > 0) : ¬ p ∣ n div p^(mult p n) := -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, +theorem not_dvd_div_pow_mult {p n : ℕ} (pgt1 : p > 1) (npos : n > 0) : ¬ p ∣ n / p^(mult p n) := +assume pdvd : p ∣ n / p^(mult p n), +obtain m (H : n / 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 (nat.mul_div_cancel' !pow_mult_dvd) + n = p^mult p n * (n / 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, @@ -154,7 +154,7 @@ show false, from !not_succ_le_self this 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 +let m' := m / p^mult p m, n' := n / p^mult p n in assert p > 1, from gt_one_of_prime primep, 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), @@ -168,11 +168,11 @@ assert multm'n' : mult p (m' * n') = 0, from mult_eq_zero_of_not_dvd npdvdm'n', calc mult p (m * n) = mult p (p^(mult p m + mult p n) * (m' * n')) : by rewrite [pow_add, mul.right_comm, -mul.assoc, -meq, mul.assoc, - mul.comm (n div _), -neq] + mul.comm (n / _), -neq] ... = 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) : +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, @@ -251,7 +251,7 @@ 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 + rewrite [pow_succ', mult_mul primep qipos qpos, ih, mult_eq_zero_of_prime_of_ne primep primeq pneq] end diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean index c1b5d555d..6bf253285 100644 --- a/library/theories/number_theory/primes.lean +++ b/library/theories/number_theory/primes.lean @@ -63,7 +63,7 @@ assume h, succ_pred_of_pos (pos_of_prime h) lemma eq_one_or_eq_self_of_prime_of_dvd {p m : nat} : prime p → m ∣ p → m = 1 ∨ m = p := assume h d, obtain h₁ h₂, from h, h₂ m d -lemma gt_one_of_pos_of_prime_dvd {i p : nat} : prime p → 0 < i → i mod p = 0 → 1 < i := +lemma gt_one_of_pos_of_prime_dvd {i p : nat} : prime p → 0 < i → i % p = 0 → 1 < i := assume ipp pos h, have p ≥ 2, from ge_two_of_prime ipp, have p ∣ i, from dvd_of_mod_eq_zero h, diff --git a/tests/lean/local_notation_bug2.lean b/tests/lean/local_notation_bug2.lean index 7ce70798a..747dd72ad 100644 --- a/tests/lean/local_notation_bug2.lean +++ b/tests/lean/local_notation_bug2.lean @@ -2,6 +2,6 @@ open nat section parameters (b : ℕ) definition add_b (n : ℕ) := n + b -local postfix `%`:max := add_b +local postfix `%%`:max := add_b end -eval 5% -- Error, unexpected token +eval 5%% -- Error, unexpected token diff --git a/tests/lean/local_notation_bug2.lean.expected.out b/tests/lean/local_notation_bug2.lean.expected.out index e13686c29..110ad0ee4 100644 --- a/tests/lean/local_notation_bug2.lean.expected.out +++ b/tests/lean/local_notation_bug2.lean.expected.out @@ -1 +1 @@ -local_notation_bug2.lean:7:6: error: unexpected token +local_notation_bug2.lean:7:7: error: invalid expression diff --git a/tests/lean/noncomp_theory.lean.expected.out b/tests/lean/noncomp_theory.lean.expected.out index 07d4bbd0a..03fea7cda 100644 --- a/tests/lean/noncomp_theory.lean.expected.out +++ b/tests/lean/noncomp_theory.lean.expected.out @@ -1,5 +1,5 @@ -noncomp_theory.lean:4:0: error: definition 'f' is noncomputable, it depends on 'real.real_has_division' +noncomp_theory.lean:4:0: error: definition 'f' is noncomputable, it depends on 'real.real_has_div' noncomputable definition g : ℝ → ℝ → ℝ := -λ (a : ℝ), division (a + a) +λ (a : ℝ), div (a + a) definition r : ℕ → ℕ := λ (a : ℕ), a diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean index e22d0401d..83e2dc736 100644 --- a/tests/lean/run/occurs_check_bug1.lean +++ b/tests/lean/run/occurs_check_bug1.lean @@ -4,7 +4,7 @@ open nat prod open decidable constant modulo1 (x : ℕ) (y : ℕ) : ℕ -infixl `mod` := modulo1 +infixl `mod`:70 := modulo1 constant gcd_aux : ℕ × ℕ → ℕ diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out index 430227112..bf4b448aa 100644 --- a/tests/lean/struct_class.lean.expected.out +++ b/tests/lean/struct_class.lean.expected.out @@ -1,12 +1,11 @@ decidable : Prop → Type₁ has_add : Type → Type -has_divide : Type → Type -has_division : Type → Type +has_div : Type → Type has_dvd : Type → Type has_inv : Type → Type has_le : Type → Type has_lt : Type → Type -has_modulo : Type → Type +has_mod : Type → Type has_mul : Type → Type has_neg : Type → Type has_one : Type → Type @@ -21,13 +20,12 @@ subsingleton : Type → Prop well_founded : Π {A : Type}, (A → A → Prop) → Prop decidable : Prop → Type₁ has_add : Type → Type -has_divide : Type → Type -has_division : Type → Type +has_div : Type → Type has_dvd : Type → Type has_inv : Type → Type has_le : Type → Type has_lt : Type → Type -has_modulo : Type → Type +has_mod : Type → Type has_mul : Type → Type has_neg : Type → Type has_one : Type → Type