diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 15:10:43 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 15:10:43 +0000 |
commit | d6ebd62341fd6bbe2b7d4e5309d8e13f786a9462 (patch) | |
tree | 575ec66b8028a599f94d293ae32260b09e7874ef /theories/ZArith/Zpow_def.v | |
parent | 1dccdb6b2c792969c5e09faebc2f761e46192ec4 (diff) |
Numbers : log2. Abstraction, properties and implementations.
Btw, we finally declare the original Zpower as the power on Z.
We should switch to a more efficient one someday, but in the
meantime BigN is proved with respect to the old one.
TODO: reform Zlogarithm with respect to Zlog_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13606 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zpow_def.v')
-rw-r--r-- | theories/ZArith/Zpow_def.v | 110 |
1 files changed, 102 insertions, 8 deletions
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v index 620d6324f..96d05760b 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.v @@ -1,11 +1,20 @@ -Require Import ZArith_base. -Require Import Ring_theory. +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) -Open Local Scope Z_scope. +Require Import BinInt Zmisc Ring_theory. + +Local Open 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_pos (z:Z) (n:positive) := + iter_pos n Z (fun x:Z => z * x) 1. Definition Zpower (x y:Z) := match y with @@ -14,14 +23,99 @@ Definition Zpower (x y:Z) := | Zneg p => 0 end. +Infix "^" := Zpower : Z_scope. + +Lemma Zpower_0_r : forall n, n^0 = 1. +Proof. reflexivity. Qed. + +Lemma Zpower_succ_r : forall a b, 0<=b -> a^(Zsucc b) = a * a^b. +Proof. + intros a [|b|b] Hb; [ | |now elim Hb]; simpl. + reflexivity. + unfold Zpower_pos. now rewrite Pplus_comm, iter_pos_plus. +Qed. + +Lemma Zpower_neg_r : forall a b, b<0 -> a^b = 0. +Proof. + now destruct b. +Qed. + 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. + rewrite <- (Zmult_1_r (pow_pos _ _ _)). generalize 1. + induction p; simpl; intros; rewrite ?IHp, ?Zmult_assoc; trivial. +Qed. + +(** An alternative Zpower *) + +(** This Zpower_opt is extensionnaly equal to Zpower in ZArith, + but not convertible with it, and quicker : the number of + multiplications is logarithmic instead of linear. + + TODO: We should try someday to replace Zpower with this Zpower_opt. +*) + +Definition Zpower_opt n m := + match m with + | Z0 => 1 + | Zpos p => Piter_op Zmult p n + | Zneg p => 0 + end. + +Infix "^^" := Zpower_opt (at level 30, right associativity) : Z_scope. + +Lemma iter_pos_mult_acc : forall f, + (forall x y:Z, (f x)*y = f (x*y)) -> + forall p k, iter_pos p _ f k = (iter_pos p _ f 1)*k. +Proof. + intros f Hf. + induction p; simpl; intros. + rewrite IHp. rewrite Hf. f_equal. rewrite (IHp (iter_pos _ _ _ _)). + rewrite <- Zmult_assoc. f_equal. auto. + rewrite IHp. rewrite (IHp (iter_pos _ _ _ _)). + rewrite <- Zmult_assoc. f_equal. auto. + rewrite Hf. f_equal. now rewrite Zmult_1_l. +Qed. + +Lemma Piter_op_square : forall p a, + Piter_op Zmult p (a*a) = (Piter_op Zmult p a)*(Piter_op Zmult p a). +Proof. + induction p; simpl; intros; trivial. + rewrite IHp. rewrite <- !Zmult_assoc. f_equal. + rewrite Zmult_comm, <- Zmult_assoc. + f_equal. apply Zmult_comm. Qed. +Lemma Zpower_equiv : forall a b, a^^b = a^b. +Proof. + intros a [|p|p]; trivial. + unfold Zpower_opt, Zpower, Zpower_pos. + revert a. + induction p; simpl; intros. + f_equal. + rewrite iter_pos_mult_acc. + now rewrite Piter_op_square, IHp. + intros. symmetry; apply Zmult_assoc. + rewrite iter_pos_mult_acc. + now rewrite Piter_op_square, IHp. + intros. symmetry; apply Zmult_assoc. + now rewrite Zmult_1_r. +Qed. + +Lemma Zpower_opt_0_r : forall n, n^^0 = 1. +Proof. reflexivity. Qed. + +Lemma Zpower_opt_succ_r : forall a b, 0<=b -> a^^(Zsucc b) = a * a^^b. +Proof. + intros a [|b|b] Hb; [ | |now elim Hb]; simpl. + now rewrite Zmult_1_r. + rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc. +Qed. + +Lemma Zpower_opt_neg_r : forall a b, b<0 -> a^^b = 0. +Proof. + now destruct b. +Qed. |