diff options
author | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
commit | 55ce117e8083477593cf1ff2e51a3641c7973830 (patch) | |
tree | a82defb4105f175c71b0d13cae42831ce608c4d6 /theories/ZArith/Zpow_def.v | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'theories/ZArith/Zpow_def.v')
-rw-r--r-- | theories/ZArith/Zpow_def.v | 27 |
1 files changed, 27 insertions, 0 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. + |