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 --- parsing/g_tactic.ml4 | 6 +++--- theories/Numbers/Integer/Abstract/ZDivEucl.v | 10 +++++----- theories/Numbers/Integer/Abstract/ZDivFloor.v | 10 +++++----- theories/Numbers/NatInt/NZDiv.v | 18 +++++++++--------- 4 files changed, 22 insertions(+), 22 deletions(-) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index ef41f938d..c845daf2c 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -22,7 +22,7 @@ open Termops let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta] -let tactic_kw = [ "->"; "<-" ] +let tactic_kw = [ "->"; "<-" ; "by" ] let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) @@ -478,11 +478,11 @@ GEXTEND Gram [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ] ; by_tactic: - [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac + [ [ "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac | -> TacId [] ] ] ; opt_by_tactic: - [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> Some tac + [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac | -> None ] ] ; rename : 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. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index 551ce6b41..611432a6d 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -354,7 +354,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_pos_bound b c); order. @@ -495,7 +495,7 @@ now apply mod_bound_or. rewrite <-(mul_0_l c), <-2mul_lt_mono_neg_r, <-2mul_le_mono_neg_r by order. destruct (mod_bound_or a b); tauto. (* 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). @@ -539,7 +539,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. intros. rewrite mod_add by trivial. @@ -562,7 +562,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. intros. now rewrite mod_add. Qed. @@ -598,7 +598,7 @@ Proof. now rewrite <- add_lt_mono_l. now rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l. (* 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. 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