diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean index d8bf80e28..586d27ae1 100644 --- a/library/algebra/group_power.lean +++ b/library/algebra/group_power.lean @@ -96,38 +96,38 @@ open nat int algebra definition ipow (a : A) : ℤ → A | (of_nat n) := a^n -| -[n +1] := (a^(nat.succ n))⁻¹ +| -[1+n] := (a^(nat.succ n))⁻¹ private lemma ipow_add_aux (a : A) (m n : nat) : - ipow a ((of_nat m) + -[n +1]) = ipow a (of_nat m) * ipow a (-[n +1]) := + ipow a ((of_nat m) + -[1+n]) = ipow a (of_nat m) * ipow a (-[1+n]) := or.elim (nat.lt_or_ge m (nat.succ n)) (assume H : (#nat m < nat.succ n), assert H1 : (#nat nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H, calc - ipow a ((of_nat m) + -[n +1]) = ipow a (sub_nat_nat m (nat.succ n)) : rfl - ... = ipow a (-[nat.pred (nat.sub (nat.succ n) m) +1]) : {sub_nat_nat_of_lt H} + ipow a ((of_nat m) + -[1+n]) = ipow a (sub_nat_nat m (nat.succ n)) : rfl + ... = ipow a (-[1+ nat.pred (nat.sub (nat.succ n) m)]) : {sub_nat_nat_of_lt H} ... = (pow a (nat.succ (nat.pred (nat.sub (nat.succ n) m))))⁻¹ : rfl ... = (pow a (nat.succ n) * (pow a m)⁻¹)⁻¹ : by rewrite [nat.succ_pred_of_pos H1, pow_sub a (nat.le_of_lt H)] ... = pow a m * (pow a (nat.succ n))⁻¹ : by rewrite [mul_inv, inv_inv] - ... = ipow a (of_nat m) * ipow a (-[n +1]) : rfl) + ... = ipow a (of_nat m) * ipow a (-[1+n]) : rfl) (assume H : (#nat m ≥ nat.succ n), calc - ipow a ((of_nat m) + -[n +1]) = ipow a (sub_nat_nat m (nat.succ n)) : rfl + ipow a ((of_nat m) + -[1+n]) = ipow a (sub_nat_nat m (nat.succ n)) : rfl ... = ipow a (#nat m - nat.succ n) : {sub_nat_nat_of_ge H} ... = pow a m * (pow a (nat.succ n))⁻¹ : pow_sub a H - ... = ipow a (of_nat m) * ipow a (-[n +1]) : rfl) + ... = ipow a (of_nat m) * ipow a (-[1+n]) : rfl) theorem ipow_add (a : A) : ∀i j : int, ipow a (i + j) = ipow a i * ipow a j | (of_nat m) (of_nat n) := !pow_add -| (of_nat m) -[n +1] := !ipow_add_aux -| -[ m+1] (of_nat n) := by rewrite [int.add.comm, ipow_add_aux, ↑ipow, -*inv_pow, pow_inv_comm] -| -[ m+1] -[n+1] := +| (of_nat m) -[1+n] := !ipow_add_aux +| -[1+m] (of_nat n) := by rewrite [int.add.comm, ipow_add_aux, ↑ipow, -*inv_pow, pow_inv_comm] +| -[1+m] -[1+n] := calc - ipow a (-[ m+1] + -[n+1]) = (a^(#nat nat.succ m + nat.succ n))⁻¹ : rfl + ipow a (-[1+m] + -[1+n]) = (a^(#nat nat.succ m + nat.succ n))⁻¹ : rfl ... = (a^(nat.succ m))⁻¹ * (a^(nat.succ n))⁻¹ : by rewrite [pow_add, pow_comm, mul_inv] - ... = ipow a (-[ m+1]) * ipow a (-[n+1]) : rfl + ... = ipow a (-[1+m]) * ipow a (-[1+n]) : rfl theorem ipow_comm (a : A) (i j : ℤ) : ipow a i * ipow a j = ipow a j * ipow a i := by rewrite [-*ipow_add, int.add.comm] diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 034af64eb..9b8d6037d 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -85,7 +85,7 @@ definition mul (a b : ℤ) : ℤ := /- notation -/ -notation `-[` n `+1]` := int.neg_succ_of_nat n -- for pretty-printing output +notation `-[1+` n `]` := int.neg_succ_of_nat n -- for pretty-printing output prefix - := int.neg infix + := int.add infix * := int.mul @@ -101,7 +101,7 @@ iff.intro of_nat.inj !congr_arg theorem neg_succ_of_nat.inj {m n : ℕ} (H : neg_succ_of_nat m = neg_succ_of_nat n) : m = n := by injection H; assumption -theorem neg_succ_of_nat_eq (n : ℕ) : -[n +1] = -(n + 1) := rfl +theorem neg_succ_of_nat_eq (n : ℕ) : -[1+ n] = -(n + 1) := rfl definition has_decidable_eq [instance] : decidable_eq ℤ := take a b, @@ -641,7 +641,7 @@ have H1 : m = (#nat m - n + n), from (nat.sub_add_cancel H)⁻¹, have H2 : m = (#nat m - n) + n, from congr_arg of_nat H1, (sub_eq_of_eq_add H2)⁻¹ -theorem neg_succ_of_nat_eq' (m : ℕ) : -[m +1] = -m - 1 := +theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 := by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add] definition succ (a : ℤ) := a + (nat.succ zero) diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 8143e3b0c..e4dc32492 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -21,7 +21,7 @@ definition divide (a b : ℤ) : ℤ := sign b * (match a with | of_nat m := #nat m div (nat_abs b) - | -[ m +1] := -[ (#nat m div (nat_abs b)) +1] + | -[1+m] := -[1+ (#nat m div (nat_abs b))] end) notation a div b := divide a b @@ -37,17 +37,17 @@ nat.cases_on n (take n, by rewrite [↑divide, sign_of_succ, one_mul]) theorem neg_succ_of_nat_div (m : nat) {b : ℤ} (H : b > 0) : - -[m +1] div b = -(m div b + 1) := + -[1+m] div b = -(m div b + 1) := calc - -[m +1] div b = sign b * _ : rfl - ... = -[(#nat m div (nat_abs b)) +1] : by rewrite [sign_of_pos H, one_mul] + -[1+m] div b = sign b * _ : rfl + ... = -[1+(#nat m div (nat_abs b))] : by rewrite [sign_of_pos H, one_mul] ... = -(m div b + 1) : by rewrite [↑divide, sign_of_pos H, one_mul] theorem div_neg (a b : ℤ) : a div -b = -(a div b) := by rewrite [↑divide, sign_neg, neg_mul_eq_neg_mul, nat_abs_neg] theorem div_of_neg_of_pos {a b : ℤ} (Ha : a < 0) (Hb : b > 0) : a div b = -((-a - 1) div b + 1) := -obtain m (H1 : a = -[m +1]), from exists_eq_neg_succ_of_nat Ha, +obtain m (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, @@ -100,12 +100,12 @@ int.cases_on a m div n = #nat m div n : of_nat_div ... = 0 : nat.div_eq_zero_of_lt (lt_of_of_nat_lt_of_nat H)) (take n, - assume H : m < -[ n +1], - have H1 : ¬(m < -[ n +1]), from dec_trivial, + assume H : m < -[1+n], + have H1 : ¬(m < -[1+n]), from dec_trivial, absurd H H1)) (take m, - assume H : 0 ≤ -[ m +1], - have H1 : ¬ (0 ≤ -[ m +1]), from dec_trivial, + assume H : 0 ≤ -[1+m], + have H1 : ¬ (0 ≤ -[1+m]), from dec_trivial, absurd H H1) theorem div_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < abs b) : a div b = 0 := @@ -134,14 +134,14 @@ Hm⁻¹ ▸ (calc private theorem add_mul_div_self_aux2 {a : ℤ} {k : ℕ} (n : ℕ) (H1 : a < 0) (H2 : #nat k > 0) : (a + n * k) div k = a div k + n := -obtain m (Hm : a = -[m +1]), from exists_eq_neg_succ_of_nat H1, +obtain m (Hm : a = -[1+m]), from exists_eq_neg_succ_of_nat H1, or.elim (nat.lt_or_ge m (#nat n * k)) (assume m_lt_nk : #nat m < n * k, have H3 : #nat (m + 1 ≤ n * k), from nat.succ_le_of_lt m_lt_nk, have H4 : #nat m div k + 1 ≤ n, from nat.succ_le_of_lt (nat.div_lt_of_lt_mul m_lt_nk), Hm⁻¹ ▸ (calc - (-[m +1] + n * k) div k = (n * k - (m + 1)) div k : by rewrite [add.comm, neg_succ_of_nat_eq] + (-[1+m] + n * k) div k = (n * k - (m + 1)) div k : by rewrite [add.comm, neg_succ_of_nat_eq] ... = ((#nat n * k) - (#nat m + 1)) div k : rfl ... = (#nat n * k - (m + 1)) div k : {(of_nat_sub H3)⁻¹} ... = #nat (n * k - (m + 1)) div k : of_nat_div @@ -152,11 +152,11 @@ or.elim (nat.lt_or_ge m (#nat n * k)) ... = n - (#nat m div k + 1) : of_nat_sub H4 ... = -(m div k + 1) + n : by rewrite [add.comm, -sub_eq_add_neg, of_nat_add, of_nat_div] - ... = -[m +1] div k + n : + ... = -[1+m] div k + n : neg_succ_of_nat_div m (of_nat_lt_of_nat_of_lt H2))) (assume nk_le_m : #nat n * k ≤ m, eq.symm (Hm⁻¹ ▸ (calc - -[m +1] div k + n = -(m div k + 1) + n : + -[1+m] div k + n = -(m div k + 1) + n : neg_succ_of_nat_div m (of_nat_lt_of_nat_of_lt H2) ... = -((#nat m div k) + 1) + n : of_nat_div ... = -((#nat (m - n * k + n * k) div k) + 1) + n : nat.sub_add_cancel nk_le_m @@ -164,13 +164,13 @@ or.elim (nat.lt_or_ge m (#nat n * k)) ... = -((#nat m - n * k) div k + 1) : by rewrite [of_nat_add, *neg_add, add.right_comm, neg_add_cancel_right, of_nat_div] - ... = -[(#nat m - n * k) +1] div k : + ... = -[1+(#nat m - n * k)] div k : neg_succ_of_nat_div _ (of_nat_lt_of_nat_of_lt H2) ... = -((#nat m - n * k) + 1) div k : rfl ... = -(m - (#nat n * k) + 1) div k : of_nat_sub nk_le_m ... = (-(m + 1) + n * k) div k : by rewrite [sub_eq_add_neg, -*add.assoc, *neg_add, neg_neg, add.right_comm] - ... = (-[m +1] + n * k) div k : rfl))) + ... = (-[1+m] + n * k) div k : rfl))) 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 := @@ -236,9 +236,9 @@ calc ... = (#nat m mod n) : sub_eq_of_eq_add H theorem neg_succ_of_nat_mod (m : ℕ) {b : ℤ} (bpos : b > 0) : - -[m +1] mod b = b - 1 - m mod b := + -[1+m] mod b = b - 1 - m mod b := calc - -[m +1] mod b = -(m + 1) - -[m +1] div b * b : rfl + -[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) : by rewrite [neg_add, -neg_mul_eq_neg_mul, sub_neg_eq_add, mul.right_distrib, @@ -300,7 +300,7 @@ have H2 : a mod (abs b) ≥ 0, from have H3 : 1 + m mod (abs b) ≤ (abs b), from (!add.comm ▸ add_one_le_of_lt (of_nat_mod_abs_lt m H)), calc - -[ m +1] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1 + -[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.mp' !sub_nonneg_iff_le H3), !mod_abs ▸ H2 @@ -314,7 +314,7 @@ have H2 : a mod (abs b) < abs b, from have H3 : abs b ≠ 0, from assume H', H (eq_zero_of_abs_eq_zero H'), have H4 : 1 + m mod (abs b) > 0, from add_pos_of_pos_of_nonneg dec_trivial (mod_nonneg _ H3), calc - -[ m +1] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1 + -[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] ... < abs b : sub_lt_self _ H4), !mod_abs ▸ H2 diff --git a/library/data/int/order.lean b/library/data/int/order.lean index b65e62d56..636d02d02 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -363,7 +363,7 @@ theorem lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) : a < b := theorem sign_of_succ (n : nat) : sign (nat.succ n) = 1 := sign_of_pos (of_nat_pos !nat.succ_pos) -theorem exists_eq_neg_succ_of_nat {a : ℤ} : a < 0 → ∃m : ℕ, a = -[m +1] := +theorem exists_eq_neg_succ_of_nat {a : ℤ} : a < 0 → ∃m : ℕ, a = -[1+m] := int.cases_on a (take m H, absurd (of_nat_nonneg m : 0 ≤ m) (not_le_of_gt H)) (take m H, exists.intro m rfl) diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index b2d04b8ee..e8f4992c5 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -105,9 +105,9 @@ theorem of_int.inj {a b : ℤ} : of_int a ≡ of_int b → a = b := by rewrite [↑of_int, ↑equiv, *mul_one]; intros; assumption definition inv : prerat → prerat -| inv (prerat.mk nat.zero d dp) := zero +| inv (prerat.mk nat.zero d dp) := zero | inv (prerat.mk (nat.succ n) d dp) := prerat.mk d (nat.succ n) !of_nat_succ_pos -| inv (prerat.mk -[n +1] d dp) := prerat.mk (-d) (nat.succ n) !of_nat_succ_pos +| inv (prerat.mk -[1+n] d dp) := prerat.mk (-d) (nat.succ n) !of_nat_succ_pos theorem equiv_zero_of_num_eq_zero {a : prerat} (H : num a = 0) : a ≡ zero := by rewrite [↑equiv, H, ↑zero, ↑num, ↑of_int, *zero_mul] @@ -132,9 +132,9 @@ obtain (n' : nat) (Hn' : n = of_nat n'), from exists_eq_of_nat (le_of_lt np), have H1 : (#nat n' > nat.zero), from lt_of_of_nat_lt_of_nat (Hn' ▸ np), obtain (k : nat) (Hk : n' = nat.succ k), from nat.exists_eq_succ_of_lt H1, have H2 : -d * n = -d * nat.succ k, by rewrite [Hn', Hk], -have H3 : inv (mk -[k +1] d dp) ≡ mk (-d) n np, from H2, -have H4 : -[k +1] = -n, from calc - -[k +1] = -(nat.succ k) : rfl +have H3 : inv (mk -[1+k] d dp) ≡ mk (-d) n np, from H2, +have H4 : -[1+k] = -n, from calc + -[1+k] = -(nat.succ k) : rfl ... = -n : by rewrite [Hk⁻¹, Hn'], H4 ▸ H3 @@ -298,13 +298,15 @@ theorem reduce_eq_reduce : ∀{a b : prerat}, a ≡ b → reduce a = reduce b decidable.by_cases (assume anz : an = 0, have H' : bn * ad = 0, by rewrite [-H, anz, zero_mul], - assert bnz : bn = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt adpos), + assert bnz : bn = 0, + from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt adpos), by rewrite [↑reduce, if_pos anz, if_pos bnz]) (assume annz : an ≠ 0, assert bnnz : bn ≠ 0, from assume bnz, have H' : an * bd = 0, by rewrite [H, bnz, zero_mul], - have anz : an = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt bdpos), + have anz : an = 0, + from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt bdpos), show false, from annz anz, begin rewrite [↑reduce, if_neg annz, if_neg bnnz], @@ -395,7 +397,7 @@ calc ... = of_int a - of_int b : {of_int_neg b} theorem of_int.inj {a b : ℤ} (H : of_int a = of_int b) : a = b := -sorry +prerat.of_int.inj (quot.exact H) theorem of_nat_eq (a : ℕ) : of_nat a = of_int (int.of_nat a) := rfl