1 files changed, 149 insertions, 59 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 71e48360..1ff88604 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: BinInt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: BinInt.v 11015 2008-05-28 20:06:42Z herbelin $ i*)
 
 (***********************************************************)
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 (***********************************************************)
 
 Require Export BinPos.
@@ -40,43 +40,48 @@ Arguments Scope Zneg [positive_scope].
 Definition Zdouble_plus_one (x:Z) :=
   match x with
     | Z0 => Zpos 1
-    | Zpos p => Zpos (xI p)
+    | Zpos p => Zpos p~1
     | Zneg p => Zneg (Pdouble_minus_one p)
   end.
 
 Definition Zdouble_minus_one (x:Z) :=
   match x with
     | Z0 => Zneg 1
-    | Zneg p => Zneg (xI p)
+    | Zneg p => Zneg p~1
     | Zpos p => Zpos (Pdouble_minus_one p)
   end.
 
 Definition Zdouble (x:Z) :=
   match x with
     | Z0 => Z0
-    | Zpos p => Zpos (xO p)
-    | Zneg p => Zneg (xO p)
+    | Zpos p => Zpos p~0
+    | Zneg p => Zneg p~0
   end.
 
+Open Local Scope positive_scope.
+
 Fixpoint ZPminus (x y:positive) {struct y} : Z :=
   match x, y with
-    | xI x', xI y' => Zdouble (ZPminus x' y')
-    | xI x', xO y' => Zdouble_plus_one (ZPminus x' y')
-    | xI x', xH => Zpos (xO x')
-    | xO x', xI y' => Zdouble_minus_one (ZPminus x' y')
-    | xO x', xO y' => Zdouble (ZPminus x' y')
-    | xO x', xH => Zpos (Pdouble_minus_one x')
-    | xH, xI y' => Zneg (xO y')
-    | xH, xO y' => Zneg (Pdouble_minus_one y')
-    | xH, xH => Z0
+    | p~1, q~1 => Zdouble (ZPminus p q)
+    | p~1, q~0 => Zdouble_plus_one (ZPminus p q)
+    | p~1, 1 => Zpos p~0
+    | p~0, q~1 => Zdouble_minus_one (ZPminus p q)
+    | p~0, q~0 => Zdouble (ZPminus p q)
+    | p~0, 1 => Zpos (Pdouble_minus_one p)
+    | 1, q~1 => Zneg q~0
+    | 1, q~0 => Zneg (Pdouble_minus_one q)
+    | 1, 1 => Z0
   end.
 
+Close Local Scope positive_scope.
+
 (** ** Addition on integers *)
 
 Definition Zplus (x y:Z) :=
   match x, y with
     | Z0, y => y
-    | x, Z0 => x
+    | Zpos x', Z0 => Zpos x'
+    | Zneg x', Z0 => Zneg x'
     | Zpos x', Zpos y' => Zpos (x' + y')
     | Zpos x', Zneg y' =>
       match (x' ?= y')%positive Eq with
@@ -217,6 +222,7 @@ Qed.
 
 
 (**********************************************************************)
+
 (** ** Properties of opposite on binary integer numbers *)
 
 Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p.
@@ -247,30 +253,6 @@ Proof.
       | simplify_eq H; intro E; rewrite E; trivial ].
 Qed.
 
-(*************************************************************************)
-(** **  Properties of the direct definition of successor and predecessor *)
-
-Lemma Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n.
-Proof.
-  intro x; destruct x; simpl in |- *.
-    reflexivity.
-  destruct p; simpl in |- *; try rewrite Pdouble_minus_one_o_succ_eq_xI;
-    reflexivity.
-  destruct p; simpl in |- *; try rewrite Psucc_o_double_minus_one_eq_xO;
-    reflexivity.
-Qed.
-
-Lemma Zsucc'_discr : forall n:Z, n <> Zsucc' n.
-Proof.
-  intro x; destruct x; simpl in |- *.
-  discriminate.
-  injection; apply Psucc_discr.
-  destruct p; simpl in |- *.
-    discriminate.
-    intro H; symmetry  in H; injection H; apply double_moins_un_xO_discr.
-    discriminate.
-Qed.
-
 (**********************************************************************)
 (** ** Other properties of binary integer numbers *)
 
@@ -313,10 +295,15 @@ Qed.
 Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
 Proof.
   intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q];
-    simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq); 
+    simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq);
       reflexivity.
 Qed.
 
+Theorem Zopp_succ : forall n:Z, Zopp (Zsucc n) = Zpred (Zopp n).
+Proof.
+intro; unfold Zsucc; now rewrite Zopp_plus_distr.
+Qed.
+
 (** ** opposite is inverse for addition *)
 
 Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.
@@ -520,11 +507,13 @@ Proof.
       trivial with arith.
 Qed.
 
-Lemma Zplus_succ_r : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
+Lemma Zplus_succ_r_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
 Proof.
   intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith.
 Qed.
 
+Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing).
+
 Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m.
 Proof.
   unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc;
@@ -586,10 +575,10 @@ Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).
 Proof.
   intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *;
     rewrite Zplus_0_r; trivial with arith.
-Qed. 
+Qed.
 
 Hint Immediate Zsucc_pred: zarith.
- 
+
 Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n).
 Proof.
   intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *;
@@ -603,7 +592,59 @@ Proof.
     do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1));
       unfold Zsucc in H; rewrite H; trivial with arith.
 Qed.
- 
+
+(*************************************************************************)
+(** **  Properties of the direct definition of successor and predecessor *)
+
+Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n.
+Proof.
+destruct n as [| p | p]; simpl.
+reflexivity.
+now rewrite Pplus_one_succ_r.
+now destruct p as [q | q |].
+Qed.
+
+Theorem Zpred_pred' : forall n:Z, Zpred n = Zpred' n.
+Proof.
+destruct n as [| p | p]; simpl.
+reflexivity.
+now destruct p as [q | q |].
+now rewrite Pplus_one_succ_r.
+Qed.
+
+Theorem Zsucc'_inj : forall n m:Z, Zsucc' n = Zsucc' m -> n = m.
+Proof.
+intros n m; do 2 rewrite <- Zsucc_succ'; now apply Zsucc_inj.
+Qed.
+
+Theorem Zsucc'_pred' : forall n:Z, Zsucc' (Zpred' n) = n.
+Proof.
+intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred';
+symmetry; apply Zsucc_pred.
+Qed.
+
+Theorem Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n.
+Proof.
+intro; apply Zsucc'_inj; now rewrite Zsucc'_pred'.
+Qed.
+
+Theorem Zpred'_inj : forall n m:Z, Zpred' n = Zpred' m -> n = m.
+Proof.
+intros n m H.
+rewrite <- (Zsucc'_pred' n); rewrite <- (Zsucc'_pred' m); now rewrite H.
+Qed.
+
+Theorem Zsucc'_discr : forall n:Z, n <> Zsucc' n.
+Proof.
+  intro x; destruct x; simpl in |- *.
+  discriminate.
+  injection; apply Psucc_discr.
+  destruct p; simpl in |- *.
+    discriminate.
+    intro H; symmetry  in H; injection H; apply double_moins_un_xO_discr.
+    discriminate.
+Qed.
+
 (** Misc properties, usually redundant or non natural *)
 
 Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m.
@@ -645,6 +686,22 @@ Qed.
 
 (** ** Relating [minus] with [plus] and [Zsucc] *)
 
+Lemma Zminus_plus_distr : forall n m p:Z, n - (m + p) = n - m - p.
+Proof.
+intros; unfold Zminus; rewrite Zopp_plus_distr; apply Zplus_assoc.
+Qed.
+
+Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m.
+Proof.
+  intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m));
+    rewrite <- Zplus_assoc; apply Zplus_comm.
+Qed.
+
+Lemma Zminus_succ_r : forall n m:Z, n - (Zsucc m) = Zpred (n - m).
+Proof.
+intros; unfold Zsucc; now rewrite Zminus_plus_distr.
+Qed.
+
 Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m.
 Proof.
   intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m);
@@ -665,12 +722,6 @@ Proof.
     apply Zplus_0_r.
 Qed.
 
-Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m.
-Proof.
-  intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m));
-    rewrite <- Zplus_assoc; apply Zplus_comm.
-Qed.
-
 Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m.
 Proof.
   intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr;
@@ -696,6 +747,16 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt -> 
+  Zpos (b-a) = Zpos b - Zpos a.
+Proof.
+  intros.
+  simpl.
+  change Eq with (CompOpp Eq).
+  rewrite <- Pcompare_antisym.
+  rewrite H; simpl; auto.
+Qed.
+
 (** ** Misc redundant properties *)
 
 Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0.
@@ -805,6 +866,19 @@ Proof.
 	reflexivity).
 Qed.
 
+(** ** Multiplication and Doubling *)
+
+Lemma Zdouble_mult : forall z, Zdouble z = (Zpos 2) * z.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma Zdouble_plus_one_mult : forall z, 
+  Zdouble_plus_one z = (Zpos 2) * z + (Zpos 1).
+Proof.
+  destruct z; simpl; auto with zarith.
+Qed.
+
 (** ** Multiplication and Opposite *)
 
 Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m.
@@ -967,22 +1041,37 @@ Qed.
 (**********************************************************************)
 (** * Relating binary positive numbers and binary integers *)
 
-Lemma Zpos_xI : forall p:positive, Zpos (xI p) = Zpos 2 * Zpos p + Zpos 1.
+Lemma Zpos_eq : forall p q:positive, p = q -> Zpos p = Zpos q.
+Proof.
+  intros; f_equal; auto.
+Qed.
+
+Lemma Zpos_eq_rev : forall p q:positive, Zpos p = Zpos q -> p = q.
+Proof.
+  inversion 1; auto.
+Qed.
+
+Lemma Zpos_eq_iff : forall p q:positive, p = q <-> Zpos p = Zpos q.
+Proof.
+  split; [apply Zpos_eq|apply Zpos_eq_rev].
+Qed.
+
+Lemma Zpos_xI : forall p:positive, Zpos p~1 = Zpos 2 * Zpos p + Zpos 1.
 Proof.
   intro; apply refl_equal.
 Qed.
 
-Lemma Zpos_xO : forall p:positive, Zpos (xO p) = Zpos 2 * Zpos p.
+Lemma Zpos_xO : forall p:positive, Zpos p~0 = Zpos 2 * Zpos p.
 Proof.
   intro; apply refl_equal.
 Qed.
 
-Lemma Zneg_xI : forall p:positive, Zneg (xI p) = Zpos 2 * Zneg p - Zpos 1.
+Lemma Zneg_xI : forall p:positive, Zneg p~1 = Zpos 2 * Zneg p - Zpos 1.
 Proof.
   intro; apply refl_equal.
 Qed.
 
-Lemma Zneg_xO : forall p:positive, Zneg (xO p) = Zpos 2 * Zneg p.
+Lemma Zneg_xO : forall p:positive, Zneg p~0 = Zpos 2 * Zneg p.
 Proof.
   reflexivity.
 Qed.
@@ -1057,7 +1146,8 @@ Definition Zabs_N (z:Z) :=
     | Zneg p => Npos p
   end.
 
-Definition Z_of_N (x:N) := match x with
-                             | N0 => Z0
-                             | Npos p => Zpos p
-                           end.
+Definition Z_of_N (x:N) := 
+  match x with
+    | N0 => Z0
+    | Npos p => Zpos p
+  end.