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/NatInt/NZDiv.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'theories/Numbers/NatInt/NZDiv.v') diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index db64a7963..da7d62ceb 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -247,7 +247,7 @@ intros. assert (0 < b) by (apply lt_trans with 1; auto using lt_0_1). destruct (lt_ge_cases a b). rewrite div_small; try split; order. -rewrite (div_mod a b) at 2; [|order]. +rewrite (div_mod a b) at 2 by order. apply lt_le_trans with (b*(a/b)). rewrite <- (mul_1_l (a/b)) at 1. rewrite <- mul_lt_mono_pos_r; auto. @@ -269,7 +269,7 @@ nzsimpl. rewrite (add_lt_mono_r _ _ (a mod c)). rewrite <- div_mod by order. apply lt_le_trans with b; auto. -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_bound b c); order. @@ -289,7 +289,7 @@ Qed. Lemma mul_succ_div_gt : forall a b, 0<=a -> 0 a < b*(S (a/b)). Proof. intros. -rewrite (div_mod a b) at 1; [|order]. +rewrite (div_mod a b) at 1 by order. rewrite (mul_succ_r). rewrite <- add_lt_mono_l. destruct (mod_bound a b); auto. @@ -300,7 +300,7 @@ Qed. Lemma div_exact : forall a b, 0<=a -> 0 (a == b*(a/b) <-> a mod b == 0). Proof. -intros. rewrite (div_mod a b) at 1; [|order]. +intros. rewrite (div_mod a b) at 1 by order. rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. @@ -344,7 +344,7 @@ Lemma div_le_compat_l: forall p q r, 0<=p -> 0 Proof. intros p q r Hp (Hq,Hqr). apply div_le_lower_bound; auto. - rewrite (div_mod p r) at 2; [|order]. + rewrite (div_mod p r) at 2 by order. apply le_trans with (r*(p/r)). apply mul_le_mono_nonneg_r; try order. apply div_pos; order. @@ -396,7 +396,7 @@ Proof. split. apply mul_nonneg_nonneg; destruct (mod_bound a b); order. rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound a b); auto. - 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). @@ -439,7 +439,7 @@ Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0 Proof. intros a b n Ha Hb Hn. symmetry. generalize (mul_nonneg_nonneg _ _ Ha Hb). - rewrite (div_mod a n) at 1 2; [|order]. + rewrite (div_mod a n) at 1 2 by order. rewrite add_comm, (mul_comm n), (mul_comm _ b). rewrite mul_add_distr_l, mul_assoc. intros. rewrite mod_add; auto. @@ -465,7 +465,7 @@ Lemma add_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0 Proof. intros a b n Ha Hb Hn. symmetry. generalize (add_nonneg_nonneg _ _ Ha Hb). - rewrite (div_mod a n) at 1 2; [|order]. + rewrite (div_mod a n) at 1 2 by order. rewrite <- add_assoc, add_comm, mul_comm. intros. rewrite mod_add; trivial. reflexivity. apply add_nonneg_nonneg; auto. destruct (mod_bound a n); auto. @@ -498,7 +498,7 @@ Proof. rewrite <- add_lt_mono_l; auto. rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l; auto. (* end 0<= ... < 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