diff options
author | 2010-11-02 15:10:43 +0000 | |
---|---|---|
committer | 2010-11-02 15:10:43 +0000 | |
commit | d6ebd62341fd6bbe2b7d4e5309d8e13f786a9462 (patch) | |
tree | 575ec66b8028a599f94d293ae32260b09e7874ef /theories/ZArith | |
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')
-rw-r--r-- | theories/ZArith/ZArith.v | 5 | ||||
-rw-r--r-- | theories/ZArith/Zlog_def.v | 78 | ||||
-rw-r--r-- | theories/ZArith/Zpow_def.v | 110 | ||||
-rw-r--r-- | theories/ZArith/Zpower.v | 2 | ||||
-rw-r--r-- | theories/ZArith/vo.itarget | 1 |
5 files changed, 185 insertions, 11 deletions
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index 93121d48f..8199ed369 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -10,10 +10,13 @@ Require Export ZArith_base. +(** Extra definitions *) + +Require Export Zpow_def Zsqrt_def Zlog_def. + (** Extra modules using [Omega] or [Ring]. *) Require Export Zcomplements. -Require Export Zsqrt_def. Require Export Zpower. Require Export Zdiv. Require Export Zlogarithm. diff --git a/theories/ZArith/Zlog_def.v b/theories/ZArith/Zlog_def.v new file mode 100644 index 000000000..05ceca201 --- /dev/null +++ b/theories/ZArith/Zlog_def.v @@ -0,0 +1,78 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +Require Import BinInt Zorder Zpow_def. + +Local Open Scope Z_scope. + +(** Definition of Zlog2 *) + +(** TODO: this is equal to Zlogarithm.log_inf *) + +Fixpoint Plog2_Z (p:positive) : Z := + match p with + | 1 => Z0 + | p~0 => Zsucc (Plog2_Z p) + | p~1 => Zsucc (Plog2_Z p) + end%positive. + +Definition Zlog2 z := + match z with + | Zpos p => Plog2_Z p + | _ => 0 + end. + +Lemma Plog2_Z_nonneg : forall p, 0 <= Plog2_Z p. +Proof. + induction p; simpl; auto with zarith. +Qed. + +(** TODO : to move ... *) + +Lemma Zle_succ_l : forall n m, Zsucc n <= m <-> n < m. +Proof. + intros. split; intros H. + rewrite (Zsucc_pred m). apply Zle_lt_succ, Zsucc_le_reg. + now rewrite <- Zsucc_pred. + now apply Zlt_le_succ. +Qed. + +Lemma Plog2_Z_spec : forall p, + 2^(Plog2_Z p) <= Zpos p < 2^(Zsucc (Plog2_Z p)). +Proof. + induction p; simpl; + try rewrite 2 Zpower_succ_r; auto using Plog2_Z_nonneg with zarith. + (* p~1 *) + change (Zpos p~1) with (Zsucc (2 * Zpos p)). + split; destruct IHp as [LE LT]. + apply Zle_trans with (2 * Zpos p). + now apply Zmult_le_compat_l. + apply Zle_succ. + apply Zle_succ_l. apply Zle_succ_l in LT. + replace (Zsucc (Zsucc (2 * Zpos p))) with (2 * (Zsucc (Zpos p))). + now apply Zmult_le_compat_l. + simpl. now rewrite Pplus_one_succ_r. + (* p~0 *) + change (Zpos p~0) with (2 * Zpos p). + split; destruct IHp. + now apply Zmult_le_compat_l. + now apply Zmult_lt_compat_l. + (* 1 *) + now split. +Qed. + +Lemma Zlog2_spec : forall n, 0 < n -> + 2^(Zlog2 n) <= n < 2^(Zsucc (Zlog2 n)). +Proof. + intros [|p|p] Hn; try discriminate. apply Plog2_Z_spec. +Qed. + +Lemma Zlog2_nonpos : forall n, n<=0 -> Zlog2 n = 0. +Proof. + intros [|p|p] Hn. reflexivity. now destruct Hn. reflexivity. +Qed. 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. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 54ecf4913..bafee949d 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -13,8 +13,6 @@ Require Import Omega. Require Import Zcomplements. Open Local Scope Z_scope. -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 diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget index 28db6848d..7802a8655 100644 --- a/theories/ZArith/vo.itarget +++ b/theories/ZArith/vo.itarget @@ -30,3 +30,4 @@ Zpow_facts.vo Zsqrt_compat.vo Zwf.vo Zsqrt_def.vo +Zlog_def.vo |