From 82791d73beaaeee5eab1fec317c689deb29f0a49 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 6 Jan 2010 09:03:53 +0000 Subject: "by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... by ...") Application in some proofs of Numbers's abstract division git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12630 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Integer/Abstract/ZDivEucl.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'theories/Numbers/Integer/Abstract/ZDivEucl.v') diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index a853395a6..914055654 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -385,7 +385,7 @@ nzsimpl. rewrite (add_lt_mono_r _ _ (a mod c)). rewrite <- div_mod by order. apply lt_le_trans with b; trivial. -rewrite (div_mod b c) at 1; [| order]. +rewrite (div_mod b c) at 1 by order. rewrite <- add_assoc, <- add_le_mono_l. apply le_trans with (c+0). nzsimpl; destruct (mod_always_pos b c); try order. @@ -524,7 +524,7 @@ rewrite abs_mul, (abs_pos c) by order. rewrite <-(mul_0_l c), <-mul_lt_mono_pos_r, <-mul_le_mono_pos_r by trivial. apply mod_always_pos. (* equation *) -rewrite (div_mod a b) at 1; [|order]. +rewrite (div_mod a b) at 1 by order. rewrite mul_add_distr_r. rewrite add_cancel_r. rewrite <- 2 mul_assoc. now rewrite (mul_comm c). @@ -568,7 +568,7 @@ Lemma mul_mod_idemp_l : forall a b n, n~=0 -> ((a mod n)*b) mod n == (a*b) mod n. Proof. intros a b n Hn. symmetry. - rewrite (div_mod a n) at 1; [|order]. + rewrite (div_mod a n) at 1 by order. rewrite add_comm, (mul_comm n), (mul_comm _ b). rewrite mul_add_distr_l, mul_assoc. rewrite mod_add by trivial. @@ -591,7 +591,7 @@ Lemma add_mod_idemp_l : forall a b n, n~=0 -> ((a mod n)+b) mod n == (a+b) mod n. Proof. intros a b n Hn. symmetry. - rewrite (div_mod a n) at 1; [|order]. + rewrite (div_mod a n) at 1 by order. rewrite <- add_assoc, add_comm, mul_comm. now rewrite mod_add. Qed. @@ -628,7 +628,7 @@ Proof. rewrite (abs_pos b) by order. now rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l. (* end 0<= ... < abs(b*c) *) - rewrite (div_mod a b) at 1; [|order]. + rewrite (div_mod a b) at 1 by order. rewrite add_assoc, add_cancel_r. rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. apply div_mod; order. -- cgit v1.2.3