diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zpow_def.v | 27 | ||||
| -rw-r--r-- | theories/ZArith/Zpower.v | 17 | ||||
| -rw-r--r-- | theories/ZArith/Zsqrt.v | 4 |
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, |