diff options
Diffstat (limited to 'theories/ZArith/Zpower.v')
| -rw-r--r-- | theories/ZArith/Zpower.v | 126 |
1 files changed, 56 insertions, 70 deletions
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index c9cee31d..1912f5e1 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -6,89 +6,75 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zpower.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Zpower.v 11072 2008-06-08 16:13:37Z herbelin $ i*) +Require Import Wf_nat. Require Import ZArith_base. Require Export Zpow_def. Require Import Omega. Require Import Zcomplements. Open Local Scope Z_scope. -Section section1. +Infix "^" := Zpower : Z_scope. (** * Definition of powers over [Z]*) (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary integer (type [nat]) and [z] a signed integer (type [Z]) *) - Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1. - - (** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for - [plus : nat->nat] and [Zmult : Z->Z] *) - - Lemma Zpower_nat_is_exp : - forall (n m:nat) (z:Z), - Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m. - Proof. - intros; elim n; - [ simpl in |- *; elim (Zpower_nat z m); auto with zarith - | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H; - apply Zmult_assoc ]. - Qed. - - (** This theorem shows that powers of unary and binary integers - are the same thing, modulo the function convert : [positive -> nat] *) - - Theorem Zpower_pos_nat : - forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p). - Proof. - intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *; - apply iter_nat_of_P. - Qed. - - (** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we - deduce that the function [[n:positive](Zpower_pos z n)] is a morphism - for [add : positive->positive] and [Zmult : Z->Z] *) - - Theorem Zpower_pos_is_exp : - forall (n m:positive) (z:Z), - Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m. - Proof. - intros. - rewrite (Zpower_pos_nat z n). - rewrite (Zpower_pos_nat z m). - rewrite (Zpower_pos_nat z (n + m)). - rewrite (nat_of_P_plus_morphism n m). - apply Zpower_nat_is_exp. - Qed. - - Infix "^" := Zpower : Z_scope. - - Hint Immediate Zpower_nat_is_exp: zarith. - Hint Immediate Zpower_pos_is_exp: zarith. - Hint Unfold Zpower_pos: zarith. - Hint Unfold Zpower_nat: zarith. - - Lemma Zpower_exp : - forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m. - Proof. - destruct n; destruct m; auto with zarith. - simpl in |- *; intros; apply Zred_factor0. - simpl in |- *; auto with zarith. - intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith. - intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith. - Qed. - -End section1. - -(** Exporting notation "^" *) - -Infix "^" := Zpower : Z_scope. - -Hint Immediate Zpower_nat_is_exp: zarith. -Hint Immediate Zpower_pos_is_exp: zarith. -Hint Unfold Zpower_pos: zarith. -Hint Unfold Zpower_nat: zarith. +Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1. + +(** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for + [plus : nat->nat] and [Zmult : Z->Z] *) + +Lemma Zpower_nat_is_exp : + forall (n m:nat) (z:Z), + Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m. +Proof. + intros; elim n; + [ simpl in |- *; elim (Zpower_nat z m); auto with zarith + | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H; + apply Zmult_assoc ]. +Qed. + +(** This theorem shows that powers of unary and binary integers + are the same thing, modulo the function convert : [positive -> nat] *) + +Lemma Zpower_pos_nat : + forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p). +Proof. + intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *; + apply iter_nat_of_P. +Qed. + +(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we + deduce that the function [[n:positive](Zpower_pos z n)] is a morphism + for [add : positive->positive] and [Zmult : Z->Z] *) + +Lemma Zpower_pos_is_exp : + forall (n m:positive) (z:Z), + Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m. +Proof. + intros. + rewrite (Zpower_pos_nat z n). + rewrite (Zpower_pos_nat z m). + rewrite (Zpower_pos_nat z (n + m)). + rewrite (nat_of_P_plus_morphism n m). + apply Zpower_nat_is_exp. +Qed. + +Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith. +Hint Unfold Zpower_pos Zpower_nat: zarith. + +Theorem Zpower_exp : + forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m. +Proof. + destruct n; destruct m; auto with zarith. + simpl; intros; apply Zred_factor0. + simpl; auto with zarith. + intros; compute in H0; elim H0; auto. + intros; compute in H; elim H; auto. +Qed. Section Powers_of_2. |