diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-10 14:21:09 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-10 14:21:09 +0000 |
commit | 1ac63f8e8cdc66b117a9b0deab1ab7a8afba41df (patch) | |
tree | 2a8fc55ed30fe04b921d1d642334e54f77535ba6 /theories/Numbers | |
parent | 6ac37d6ee6fe113b89177e1c61f520f8d3e6f65f (diff) |
ZBits,ZdivEucl,ZDivFloor: a few lemmas with weaker preconditions
Initial patch by Robbert Krebbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13900 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers')
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZBits.v | 8 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 16 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivFloor.v | 23 |
3 files changed, 29 insertions, 18 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index bf03cf020..39e9f02c5 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -710,11 +710,13 @@ Proof. intros. now rewrite <- 2 shiftl_opp_r, shiftl_shiftl, opp_sub_distr, add_comm. Qed. -Lemma shiftr_shiftr : forall a n m, 0<=n -> 0<=m -> +Lemma shiftr_shiftr : forall a n m, 0<=m -> (a >> n) >> m == a >> (n+m). Proof. - intros a n m Hn Hm. - now rewrite !shiftr_div_pow2, pow_add_r, div_div by order_pos. + intros a n p Hn. bitwise. + rewrite 3 shiftr_spec; trivial. + now rewrite (add_comm n p), add_assoc. + now apply add_nonneg_nonneg. Qed. (** shifts and constants *) diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index c8fd29a54..f72c1b343 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -550,10 +550,11 @@ Proof. Qed. (** With the current convention, the following result isn't always - true for negative divisors. For instance - [ 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) ]. *) + true with a negative intermediate divisor. For instance + [ 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) ] and + [ 3/(-2)/2 = -1 <> 0 = 3 / (-2*2) ]. *) -Lemma div_div : forall a b c, 0<b -> 0<c -> +Lemma div_div : forall a b c, 0<b -> c~=0 -> (a/b)/c == a/(b*c). Proof. intros a b c Hb Hc. @@ -575,12 +576,11 @@ Proof. apply div_mod; order. Qed. -(** Similarly, the following result doesn't always hold for negative - [b] and [c]. For instance [3 mod (-2*-2)) = 3] while - [3 mod (-2) + (-2)*((3/-2) mod -2) = -1]. -*) +(** Similarly, the following result doesn't always hold when [b<0]. + For instance [3 mod (-2*-2)) = 3] while + [3 mod (-2) + (-2)*((3/-2) mod -2) = -1]. *) -Lemma mod_mul_r : forall a b c, 0<b -> 0<c -> +Lemma mod_mul_r : forall a b c, 0<b -> c~=0 -> a mod (b*c) == a mod b + b*((a/b) mod c). Proof. intros a b c Hb Hc. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index 017f995cc..bc1932d44 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -594,15 +594,25 @@ Proof. Qed. (** With the current convention, the following result isn't always - true for negative divisors. For instance - [ 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) ]. *) + true with a negative last divisor. For instance + [ 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) ], or + [ 5/2/(-2) = -1 <> -2 = 5 / (2*-2) ]. *) -Lemma div_div : forall a b c, 0<b -> 0<c -> +Lemma div_div : forall a b c, b~=0 -> 0<c -> (a/b)/c == a/(b*c). Proof. intros a b c Hb Hc. apply div_unique with (b*((a/b) mod c) + a mod b). (* begin 0<= ... <b*c \/ ... *) + apply neg_pos_cases in Hb. destruct Hb as [Hb|Hb]. + right. + destruct (mod_pos_bound (a/b) c), (mod_neg_bound a b); trivial. + split. + apply le_lt_trans with (b*((a/b) mod c) + b). + now rewrite <- mul_succ_r, <- mul_le_mono_neg_l, le_succ_l. + now rewrite <- add_lt_mono_l. + apply add_nonpos_nonpos; trivial. + apply mul_nonpos_nonneg; order. left. destruct (mod_pos_bound (a/b) c), (mod_pos_bound a b); trivial. split. @@ -618,12 +628,12 @@ Proof. apply div_mod; order. Qed. -(** Similarly, the following result doesn't always hold for negative - [b] and [c]. For instance [3 mod (-2*-2)) = 3] while +(** Similarly, the following result doesn't always hold when [c<0]. + For instance [3 mod (-2*-2)) = 3] while [3 mod (-2) + (-2)*((3/-2) mod -2) = -1]. *) -Lemma rem_mul_r : forall a b c, 0<b -> 0<c -> +Lemma rem_mul_r : forall a b c, b~=0 -> 0<c -> a mod (b*c) == a mod b + b*((a/b) mod c). Proof. intros a b c Hb Hc. @@ -642,4 +652,3 @@ Theorem div_mul_le: Proof. exact div_mul_le. Qed. End ZDivProp. - |