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

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.
-