ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2

 Now we have:
  - Zdiv and Zdiv2 : round toward bottom, no easy sign rule, remainder
    of a/2 is 0 or 1, operations related with two's-complement Zshiftr.
  - Zquot and Zquot2 : round toward zero, Zquot2 (-a) = - Zquot2 a,
    remainder of a/2 is 0 or Zsgn a.

 Ok, I'm introducing an incompatibility here, but I think coherence is
 really desirable. Anyway, people using Zdiv on positive numbers only
 shouldn't even notice the change. Otherwise, it's just a matter of
 sed -e "s/div2/quot2/g".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13695 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 13 deletions

diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 5fe105aa5..7f0885128 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -473,13 +473,7 @@ Qed.
 
 (** Particular case : dividing by 2 is related with parity *)
 
-Lemma Zdiv2_odd_eq : forall a,
- a = 2 * Zdiv2 a + if Zodd_bool a then Zsgn a else 0.
-Proof.
- destruct a as [ |p|p]; try destruct p; trivial.
-Qed.
-
-Lemma Zdiv2_odd_remainder : forall a,
+Lemma Zquot2_odd_remainder : forall a,
  Remainder a 2 (if Zodd_bool a then Zsgn a else 0).
 Proof.
  intros [ |p|p]. simpl.
@@ -488,20 +482,20 @@ Proof.
  right. destruct p; simpl; split; now auto with zarith.
 Qed.
 
-Lemma Zdiv2_quot : forall a, Zdiv2 a = a÷2.
+Lemma Zquot2_quot : forall a, Zquot2 a = a÷2.
 Proof.
  intros.
  apply Zquot_unique_full with (if Zodd_bool a then Zsgn a else 0).
- apply Zdiv2_odd_remainder.
- apply Zdiv2_odd_eq.
+ apply Zquot2_odd_remainder.
+ apply Zquot2_odd_eqn.
 Qed.
 
 Lemma Zrem_odd : forall a, Zrem a 2 = if Zodd_bool a then Zsgn a else 0.
 Proof.
  intros. symmetry.
- apply Zrem_unique_full with (Zdiv2 a).
- apply Zdiv2_odd_remainder.
- apply Zdiv2_odd_eq.
+ apply Zrem_unique_full with (Zquot2 a).
+ apply Zquot2_odd_remainder.
+ apply Zquot2_odd_eqn.
 Qed.
 
 Lemma Zrem_even : forall a, Zrem a 2 = if Zeven_bool a then 0 else Zsgn a.