BinInt: Z.add become the alternative Z.add'

 It relies on Z.pos_sub instead of a Pos.compare followed by Pos.sub.
 Proofs seem to be quite easy to adapt, via some rewrite Z.pos_sub_spec.

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

1 files changed, 18 insertions, 55 deletions

diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index b0fef2a9d..4c2a19f69 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -51,26 +51,30 @@ Definition pred_double x :=
     | Zpos p => Zpos (Pos.pred_double p)
   end.
 
+(** ** Subtraction of positive into Z *)
+
+Fixpoint pos_sub (x y:positive) {struct y} : Z :=
+  match x, y with
+    | p~1, q~1 => double (pos_sub p q)
+    | p~1, q~0 => succ_double (pos_sub p q)
+    | p~1, 1 => Zpos p~0
+    | p~0, q~1 => pred_double (pos_sub p q)
+    | p~0, q~0 => double (pos_sub p q)
+    | p~0, 1 => Zpos (Pos.pred_double p)
+    | 1, q~1 => Zneg q~0
+    | 1, q~0 => Zneg (Pos.pred_double q)
+    | 1, 1 => Z0
+  end%positive.
+
 (** ** Addition *)
 
 Definition add x y :=
   match x, y with
     | 0, y => y
-    | Zpos x', 0 => Zpos x'
-    | Zneg x', 0 => Zneg x'
+    | x, 0 => x
     | Zpos x', Zpos y' => Zpos (x' + y')
-    | Zpos x', Zneg y' =>
-      match (x' ?= y')%positive with
-	| Eq => 0
-	| Lt => Zneg (y' - x')
-	| Gt => Zpos (x' - y')
-      end
-    | Zneg x', Zpos y' =>
-      match (x' ?= y')%positive with
-	| Eq => 0
-	| Lt => Zpos (y' - x')
-	| Gt => Zneg (x' - y')
-      end
+    | Zpos x', Zneg y' => pos_sub x' y'
+    | Zneg x', Zpos y' => pos_sub y' x'
     | Zneg x', Zneg y' => Zneg (x' + y')
   end.
 
@@ -115,47 +119,6 @@ Definition mul x y :=
 
 Infix "*" := mul : Z_scope.
 
-(** ** Subtraction of positive into Z *)
-
-Fixpoint pos_sub (x y:positive) {struct y} : Z :=
-  match x, y with
-    | p~1, q~1 => double (pos_sub p q)
-    | p~1, q~0 => succ_double (pos_sub p q)
-    | p~1, 1 => Zpos p~0
-    | p~0, q~1 => pred_double (pos_sub p q)
-    | p~0, q~0 => double (pos_sub p q)
-    | p~0, 1 => Zpos (Pos.pred_double p)
-    | 1, q~1 => Zneg q~0
-    | 1, q~0 => Zneg (Pos.pred_double q)
-    | 1, 1 => Z0
-  end%positive.
-
-(** ** Direct, easier to handle variants of successor and addition *)
-
-Definition succ' x :=
-  match x with
-    | 0 => 1
-    | Zpos x' => Zpos (Pos.succ x')
-    | Zneg x' => pos_sub 1 x'
-  end.
-
-Definition pred' x :=
-  match x with
-    | 0 => -1
-    | Zpos x' => pos_sub x' 1
-    | Zneg x' => Zneg (Pos.succ x')
-  end.
-
-Definition add' x y :=
-  match x, y with
-    | 0, y => y
-    | x, 0 => x
-    | Zpos x', Zpos y' => Zpos (x' + y')
-    | Zpos x', Zneg y' => pos_sub x' y'
-    | Zneg x', Zpos y' => pos_sub y' x'
-    | Zneg x', Zneg y' => Zneg (x' + y')
-  end.
-
 (** ** Power function *)
 
 Definition pow_pos (z:Z) (n:positive) := Pos.iter n (mul z) 1.