Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

3 files changed, 32 insertions, 16 deletions

diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
new file mode 100644
index 00000000..b0f372de
--- /dev/null
+++ b/theories/ZArith/Zpow_def.v
@@ -0,0 +1,27 @@
+Require Import ZArith_base.
+Require Import Ring_theory.
+
+Open Local Scope Z_scope.
+ 
+(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
+      integer (type [positive]) and [z] a signed integer (type [Z]) *) 
+Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1.
+  
+Definition Zpower (x y:Z) :=
+    match y with
+      | Zpos p => Zpower_pos x p
+      | Z0 => 1
+      | Zneg p => 0
+    end.
+
+Lemma Zpower_theory : power_theory 1 Zmult (eq (A:=Z)) Z_of_N Zpower.
+Proof.
+ constructor. intros.
+ destruct n;simpl;trivial.
+ unfold Zpower_pos.
+ assert (forall k, iter_pos p Z (fun x : Z => r * x) k = pow_pos Zmult r p*k).
+ induction p;simpl;intros;repeat rewrite IHp;trivial;
+   repeat rewrite Zmult_assoc;trivial.
+ rewrite H;rewrite Zmult_1_r;trivial.
+Qed.
+ 
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 446f663c..c9cee31d 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -6,9 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zpower.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Zpower.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import ZArith_base.
+Require Export Zpow_def.
 Require Import Omega.
 Require Import Zcomplements.
 Open Local Scope Z_scope.
@@ -35,11 +36,6 @@ Section section1.
 	  apply Zmult_assoc ].
   Qed.
 
-  (** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
-      integer (type [positive]) and [z] a signed integer (type [Z]) *) 
-
-  Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1.
-
   (** This theorem shows that powers of unary and binary integers
      are the same thing, modulo the function convert : [positive -> nat] *)
 
@@ -66,13 +62,6 @@ Section section1.
     apply Zpower_nat_is_exp.
   Qed.
 
-  Definition Zpower (x y:Z) :=
-    match y with
-      | Zpos p => Zpower_pos x p
-      | Z0 => 1
-      | Zneg p => 0
-    end.
-
   Infix "^" := Zpower : Z_scope.
 
   Hint Immediate Zpower_nat_is_exp: zarith.
@@ -382,4 +371,4 @@ Section power_div_with_rest.
       apply Zdiv_rest_proof with (q := a0) (r := b); assumption.
   Qed.
 
-End power_div_with_rest.
\ No newline at end of file
+End power_div_with_rest.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 9893bed3..3f475a63 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Zsqrt.v 9245 2006-10-17 12:53:34Z notin $ *)
+(* $Id: Zsqrt.v 9551 2007-01-29 15:13:35Z bgregoir $ *)
 
 Require Import ZArithRing.
 Require Import Omega.
@@ -132,7 +132,7 @@ Definition Zsqrt :
                (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0
                _)
     end); try omega.
-split; [ omega | rewrite Heq; ring_simplify ((s + 1) * (s + 1)); omega ].
+ split; [ omega | rewrite Heq; ring_simplify (s*s) ((s + 1) * (s + 1)); omega ].
 Defined.
 
 (** Define a function of type Z->Z that computes the integer square root,