From 5f293cee9ca5a0bfa7c4bb833914a745ff124edf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Jun 2015 16:12:24 -0700 Subject: [PATCH] refactor(library/algebra/ordered_field): improve compilation time --- library/algebra/ordered_field.lean | 36 ++++++++++++++++-------------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index a093e1a4f..3309b1c64 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -172,16 +172,16 @@ section linear_ordered_field theorem div_lt_div_of_mul_sub_mul_div_neg (Hc : c ≠ 0) (Hd : d ≠ 0) (H : (a * d - b * c) / (c * d) < 0) : a / c < b / d := - have H1 : (a * d - c * b) / (c * d) < 0, from !mul.comm ▸ H, - have H2 : a / c - b / d < 0, from (div_sub_div Hc Hd)⁻¹ ▸ H1, - have H3 [visible] : a / c - b / d + b / d < 0 + b / d, from add_lt_add_right H2 _, + assert H1 : (a * d - c * b) / (c * d) < 0, by rewrite [mul.comm c b]; exact H, + assert H2 : a / c - b / d < 0, by rewrite [div_sub_div Hc Hd]; exact H1, + assert H3 : a / c - b / d + b / d < 0 + b / d, from add_lt_add_right H2 _, begin rewrite [zero_add at H3, neg_add_cancel_right at H3], exact H3 end theorem div_le_div_of_mul_sub_mul_div_nonpos (Hc : c ≠ 0) (Hd : d ≠ 0) (H : (a * d - b * c) / (c * d) ≤ 0) : a / c ≤ b / d := - have H1 : (a * d - c * b) / (c * d) ≤ 0, from !mul.comm ▸ H, - have H2 : a / c - b / d ≤ 0, from (div_sub_div Hc Hd)⁻¹ ▸ H1, - have H3 [visible] : a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right H2 _, + assert H1 : (a * d - c * b) / (c * d) ≤ 0, by rewrite [mul.comm c b]; exact H, + assert H2 : a / c - b / d ≤ 0, by rewrite [div_sub_div Hc Hd]; exact H1, + assert H3 : a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right H2 _, begin rewrite [zero_add at H3, neg_add_cancel_right at H3], exact H3 end theorem pos_div_of_pos_of_pos (Ha : 0 < a) (Hb : 0 < b) : 0 < a / b := @@ -270,12 +270,14 @@ section linear_ordered_field theorem two_ne_zero : (1 : A) + 1 ≠ 0 := ne.symm (ne_of_lt (add_pos zero_lt_one zero_lt_one)) - theorem add_halves : a / (1 + 1) + a / (1 + 1) = a := + notation 2 := 1 + 1 + + theorem add_halves : a / 2 + a / 2 = a := calc - a / (1 + 1) + a / (1 + 1) = (a + a) / (1 + 1) : div_add_div_same - ... = (a * 1 + a * 1) / (1 + 1) : by rewrite mul_one - ... = (a * (1 + 1)) / (1 + 1) : left_distrib - ... = a : mul_div_cancel two_ne_zero + a / 2 + a / 2 = (a + a) / 2 : by rewrite div_add_div_same + ... = (a * 1 + a * 1) / 2 : by rewrite mul_one + ... = (a * 2) / 2 : by rewrite left_distrib + ... = a : by rewrite [@mul_div_cancel A _ _ _ two_ne_zero] theorem nonneg_le_nonneg_of_squares_le (Ha : a ≥ 0) (Hb : b ≥ 0) (H : a * a ≤ b * b) : a ≤ b := begin @@ -288,7 +290,7 @@ theorem nonneg_le_nonneg_of_squares_le (Ha : a ≥ 0) (Hb : b ≥ 0) (H : a * a apply (not_le_of_gt H') H end - theorem div_two : (a + a) / (1 + 1) = a := + theorem div_two : (a + a) / 2 = a := symm (iff.mp' (eq_div_iff_mul_eq (ne_of_gt (add_pos zero_lt_one zero_lt_one))) (by rewrite [left_distrib, *mul_one])) @@ -355,15 +357,15 @@ section discrete_linear_ordered_field theorem le_of_div_le_neg (H : b < 0) (Hl : 1 / a ≤ 1 / b) : b ≤ a := - have Ha : a ≠ 0, from ne_of_lt (neg_of_div_neg (calc + assert Ha : a ≠ 0, from ne_of_lt (neg_of_div_neg (calc 1 / a ≤ 1 / b : Hl ... < 0 : div_neg_of_neg H)), have H' : -b > 0, from neg_pos_of_neg H, have Hl' : - (1 / b) ≤ - (1 / a), from neg_le_neg Hl, have Hl'' : 1 / - b ≤ 1 / - a, from calc - 1 / -b = - (1 / b) : one_div_neg_eq_neg_one_div (ne_of_lt H) + 1 / -b = - (1 / b) : by rewrite [one_div_neg_eq_neg_one_div (ne_of_lt H)] ... ≤ - (1 / a) : Hl' - ... = 1 / -a : one_div_neg_eq_neg_one_div Ha, + ... = 1 / -a : by rewrite [one_div_neg_eq_neg_one_div Ha], le_of_neg_le_neg (le_of_div_le H' Hl'') theorem lt_of_div_lt (H : 0 < a) (Hl : 1 / a < 1 / b) : b < a := @@ -372,7 +374,7 @@ section discrete_linear_ordered_field ... < 1 / b : Hl), have H : 1 < a / b, from (calc 1 = a / a : div_self (ne.symm (ne_of_lt H)) - ... = a * (1 / a) : div_eq_mul_one_div + ... = a * (1 / a) : div_eq_mul_one_div ... < a * (1 / b) : mul_lt_mul_of_pos_left Hl H ... = a / b : div_eq_mul_one_div), lt_of_one_lt_div Hb H @@ -456,7 +458,7 @@ section discrete_linear_ordered_field theorem ge_sub_of_abs_sub_le_right (H : abs (a - b) ≤ c) : b ≥ a - c := ge_sub_of_abs_sub_le_left (!abs_sub ▸ H) - theorem abs_sub_square : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b := + theorem abs_sub_square : abs (a - b) * abs (a - b) = a * a + b * b - 2 * a * b := by rewrite [abs_mul_self, *mul_sub_left_distrib, *mul_sub_right_distrib, sub_add_eq_sub_sub, sub_neg_eq_add, *right_distrib, sub_add_eq_sub_sub, *one_mul, *add.assoc, {_ + b * b}add.comm, {_ + (b * b + _)}add.comm, mul.comm b a, *add.assoc]