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

refactor(library/data/real/division): remove unnecessary 'xrewrite'

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-27 13:52:52 -07:00
parent 3215af3926
commit 3cd81051c6
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/data/real/division.lean
View file

@ -228,7 +228,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
apply rat.le.trans,
apply rat.mul_le_mul,
apply Hs,
xrewrite [-(mul_one 1), -(div_mul_div Hsp Hspn), abs_mul],
rewrite [-(mul_one 1), -(div_mul_div Hsp Hspn), abs_mul],
apply rat.mul_le_mul,
rewrite -(s_inv_of_sep_lt_p Hs Hsep Hmlt),
apply le_ps Hs Hsep,
@ -252,7 +252,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
apply rat.le.trans,
apply rat.mul_le_mul,
apply Hs,
xrewrite [-(mul_one 1), -(div_mul_div Hspm Hsp), abs_mul],
rewrite [-(mul_one 1), -(div_mul_div Hspm Hsp), abs_mul],
apply rat.mul_le_mul,
rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt)),
apply le_ps Hs Hsep,
@ -274,7 +274,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
apply rat.le.trans,
apply rat.mul_le_mul,
apply Hs,
xrewrite [-(mul_one 1), -(div_mul_div Hspm Hspn), abs_mul],
rewrite [-(mul_one 1), -(div_mul_div Hspm Hspn), abs_mul],
apply rat.mul_le_mul,
rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt)),
apply le_ps Hs Hsep,
@ -315,7 +315,7 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H
existsi max (ps Hs Hsep) j,
intro n Hn,
have Hnz : s_inv Hs ((K₂ s (s_inv Hs)) * 2 * n) ≠ 0, from s_inv_ne_zero Hs Hsep _,
xrewrite [↑smul, ↑one, rat.mul.comm, -(mul_one_div_cancel Hnz),
rewrite [↑smul, ↑one, rat.mul.comm, -(mul_one_div_cancel Hnz),
-rat.mul_sub_left_distrib, abs_mul],
apply rat.le.trans,
apply rat.mul_le_mul_of_nonneg_right,
@ -334,13 +334,13 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H
s_ne_zero_of_ge_p Hs Hsep
(show ps Hs Hsep ≤ ((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n),
by rewrite *pnat.mul.assoc; apply pnat.mul_le_mul_right),
xrewrite [(s_inv_of_sep_gt_p Hs Hsep Hp), (div_div Hnz')],
rewrite [(s_inv_of_sep_gt_p Hs Hsep Hp), (div_div Hnz')],
apply rat.le.trans,
apply rat.mul_le_mul_of_nonneg_left,
apply Hs,
apply le_of_lt,
apply rat_of_pnat_is_pos,
xrewrite [rat.mul.left_distrib, mul.comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat.mul.assoc,
rewrite [rat.mul.left_distrib, mul.comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat.mul.assoc,
*(@inv_mul_eq_mul_inv (K₂ s (s_inv Hs))), -*rat.mul.assoc, *inv_cancel_left,
*one_mul, -(add_halves j)],
apply rat.add_le_add,