michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/data): remove unnecessary parentheses

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-01 14:18:36 -08:00
parent ca57b43698
commit df13588b93
3 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/int/div.lean
View file

@ -45,8 +45,8 @@ theorem neg_succ_of_nat_div (m : nat) {b : ℤ} (H : b > 0) :
-[m +1] 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]
... = -(m div b + 1) : by rewrite [↑divide, (sign_of_pos H), one_mul]
... = -[(#nat m div (nat_abs b)) +1] : 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) :=
calc
@ -89,7 +89,7 @@ calc
by rewrite [neg_add, -neg_mul_eq_neg_mul, sub_neg_eq_add, mul.right_distrib,
one_mul, (add.comm b)]
... = b + -1 + (-m + m div b * b) :
by rewrite [-*add.assoc, (add.comm (-m)), (add.right_comm (-1)), (add.comm b)]
by rewrite [-*add.assoc, add.comm (-m), add.right_comm (-1), (add.comm b)]
... = b - 1 - m mod b :
by rewrite [↑modulo, *sub_eq_add_neg, neg_add, neg_neg]

4
library/data/int/order.lean
View file

@ -587,12 +587,12 @@ or.elim (le.total 0 b)
theorem lt_of_add_one_le {a b : ℤ} (H : a + 1 ≤ b) : a < b :=
obtain n (H1 : a + 1 + n = b), from le.elim H,
have H2 : a + succ n = b, by rewrite [-H1, add.assoc, (add.comm 1)],
have H2 : a + succ n = b, by rewrite [-H1, add.assoc, add.comm 1],
lt.intro H2
theorem add_one_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b :=
obtain n (H1 : a + succ n = b), from lt.elim H,
have H2 : a + 1 + n = b, by rewrite [-H1, add.assoc, (add.comm 1)],
have H2 : a + 1 + n = b, by rewrite [-H1, add.assoc, add.comm 1],
le.intro H2
theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 := trivial

4
library/data/nat/div.lean
View file

@ -313,14 +313,14 @@ calc
(m * n - (k + 1)) div m = (m * n - (k div m * m + k mod m + 1)) div m : eq_div_mul_add_mod
... = (m * n - k div m * m - (k mod m + 1)) div m : by rewrite [*sub_sub]
... = ((n - k div m) * m - (k mod m + 1)) div m :
by rewrite [(mul.comm m), mul_sub_right_distrib]
by rewrite [mul.comm m, mul_sub_right_distrib]
... = ((n - k div m - 1) * m + m - (k mod m + 1)) div m :
by rewrite [H3 at {1}, mul.right_distrib, nat.one_mul]
... = ((n - k div m - 1) * m + (m - (k mod m + 1))) div m : {add_sub_assoc H5 _}
... = (m - (k mod m + 1)) div m + (n - k div m - 1) :
by rewrite [add.comm, (add_mul_div_self_right H4)]
... = n - k div m - 1 :
by rewrite [(div_eq_zero_of_lt H6), zero_add]
by rewrite [div_eq_zero_of_lt H6, zero_add]
/- divides -/