From d6ebd62341fd6bbe2b7d4e5309d8e13f786a9462 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 2 Nov 2010 15:10:43 +0000 Subject: 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 --- doc/stdlib/index-list.html.template | 3 + theories/NArith/BinNat.v | 32 ++- theories/Numbers/Integer/Abstract/ZAxioms.v | 8 +- theories/Numbers/Integer/Abstract/ZProperties.v | 2 +- theories/Numbers/Integer/BigZ/BigZ.v | 3 + theories/Numbers/Integer/BigZ/ZMake.v | 15 ++ theories/Numbers/Integer/Binary/ZBinary.v | 52 ++--- theories/Numbers/Integer/SpecViaZ/ZSig.v | 2 + theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 17 +- theories/Numbers/NatInt/NZLog.v | 297 ++++++++++++++++++++++++ theories/Numbers/Natural/Abstract/NAxioms.v | 9 +- theories/Numbers/Natural/Abstract/NLog.v | 22 ++ theories/Numbers/Natural/Abstract/NPow.v | 2 +- theories/Numbers/Natural/Abstract/NProperties.v | 5 +- theories/Numbers/Natural/BigN/BigN.v | 3 + theories/Numbers/Natural/BigN/NMake.v | 13 +- theories/Numbers/Natural/Binary/NBinary.v | 20 +- theories/Numbers/Natural/Peano/NPeano.v | 5 + theories/Numbers/Natural/SpecViaZ/NSig.v | 3 +- theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 19 +- theories/Numbers/vo.itarget | 2 + theories/ZArith/ZArith.v | 5 +- theories/ZArith/Zlog_def.v | 78 +++++++ theories/ZArith/Zpow_def.v | 110 ++++++++- theories/ZArith/Zpower.v | 2 - theories/ZArith/vo.itarget | 1 + 26 files changed, 640 insertions(+), 90 deletions(-) create mode 100644 theories/Numbers/NatInt/NZLog.v create mode 100644 theories/Numbers/Natural/Abstract/NLog.v create mode 100644 theories/ZArith/Zlog_def.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 4f208c7da8..e0f445d036 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -183,6 +183,7 @@ through the Require Import command.

theories/ZArith/Zpow_def.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v + theories/ZArith/Zlog_def.v theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) theories/ZArith/Zgcd_alt.v @@ -238,6 +239,7 @@ through the Require Import command.

theories/Numbers/NatInt/NZProperties.v theories/Numbers/NatInt/NZPow.v theories/Numbers/NatInt/NZSqrt.v + theories/Numbers/NatInt/NZLog.v @@ -281,6 +283,7 @@ through the Require Import command.

theories/Numbers/Natural/Abstract/NParity.v theories/Numbers/Natural/Abstract/NPow.v theories/Numbers/Natural/Abstract/NSqrt.v + theories/Numbers/Natural/Abstract/NLog.v theories/Numbers/Natural/Abstract/NProperties.v theories/Numbers/Natural/Binary/NBinary.v theories/Numbers/Natural/Peano/NPeano.v diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 0bd227b5de..eb89fb20df 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -442,15 +442,13 @@ Proof. Qed. Theorem Ncompare_n_Sm : - forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m. + forall n m : N, (n ?= Nsucc m) = Lt <-> (n ?= m) = Lt \/ n = m. Proof. -intros n m; split; destruct n as [| p]; destruct m as [| q]; simpl; auto. -destruct p; simpl; intros; discriminate. -pose proof (Pcompare_p_Sq p q) as (?,_). -assert (p = q <-> Npos p = Npos q); [split; congruence | tauto]. -intros H; destruct H; discriminate. -pose proof (Pcompare_p_Sq p q) as (_,?); -assert (p = q <-> Npos p = Npos q); [split; congruence | tauto]. +intros [|p] [|q]; simpl; split; intros H; auto. +destruct p; discriminate. +destruct H; discriminate. +apply Pcompare_p_Sq in H; destruct H; subst; auto. +apply Pcompare_p_Sq; destruct H; [left|right]; congruence. Qed. Lemma Nle_lteq : forall x y, x <= y <-> x < y \/ x=y. @@ -460,9 +458,17 @@ generalize (Ncompare_eq_correct x y). destruct (x ?= y); intuition; discriminate. Qed. +Lemma Nlt_succ_r : forall n m, n < Nsucc m <-> n<=m. +Proof. +intros n m. +eapply iff_trans. apply Ncompare_n_Sm. apply iff_sym, Nle_lteq. +Qed. + Lemma Nle_trans : forall n m p, n<=m -> m<=p -> n<=p. Proof. - intros n m p. rewrite 3 Nle_lteq. intros [H|H] [H'|H']; subst; auto. + intros n m p H H'. + apply Nle_lteq. apply Nle_lteq in H. apply Nle_lteq in H'. + destruct H, H'; subst; auto. left; now apply Nlt_trans with m. Qed. @@ -470,8 +476,10 @@ Lemma Nle_succ_l : forall n m, Nsucc n <= m <-> n < m. Proof. intros. unfold Nle, Nlt. - rewrite <- 2 (Ncompare_antisym m), 2 CompOpp_iff, Ncompare_n_Sm, <- (Nle_lteq m n). - unfold Nle. simpl. destruct (m ?= n); split; auto; now destruct 1. + rewrite <- 2 (Ncompare_antisym m). + generalize (Nlt_succ_r m n). unfold Nle,Nlt. + destruct Ncompare, Ncompare; simpl; intros (U,V); + intuition; now try discriminate V. Qed. Lemma Ncompare_spec : forall x y, CompSpec eq Nlt x y (Ncompare x y). @@ -512,7 +520,7 @@ Qed. Lemma Nmult_le_mono_l : forall n m p, m<=p -> n*m<=n*p. Proof. intros [|n] m p. intros _ H. discriminate. - rewrite 2 Nle_lteq. intros [H|H]; [left|right]. + intros. apply Nle_lteq. apply Nle_lteq in H. destruct H; [left|right]. now apply Nmult_lt_mono_l. congruence. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 6e6cd7f0fc..47286c729e 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -9,7 +9,7 @@ (************************************************************************) Require Export NZAxioms. -Require Import NZPow NZSqrt. +Require Import NZPow NZSqrt NZLog. (** We obtain integers by postulating that successor of predecessor is identity. *) @@ -70,16 +70,16 @@ Module Type Parity (Import Z : ZAxiomsMiniSig'). Axiom odd_spec : forall n, odd n = true <-> Odd n. End Parity. -(** For the power and sqrt functions, the NZ axiomatizations are enough. *) +(** For pow sqrt log2, the NZ axiomatizations are enough. *) (** Let's group everything *) Module Type ZAxiomsSig := ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity - <+ NZPow.NZPow <+ NZSqrt.NZSqrt. + <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2. Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity - <+ NZPow.NZPow' <+ NZSqrt.NZSqrt'. + <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2. (** Division is left apart, since many different flavours are available *) diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 8b34e5b2db..d2e9626737 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -12,4 +12,4 @@ Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow. Module Type ZProp (Z:ZAxiomsSig) := ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z - <+ NZSqrt.NZSqrtProp Z Z. + <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 92be49bdaf..b2bf8703ea 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -63,10 +63,13 @@ Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope]. Arguments Scope BigZ.pow_pos [bigZ_scope positive_scope]. Arguments Scope BigZ.pow_N [bigZ_scope N_scope]. Arguments Scope BigZ.pow [bigZ_scope bigZ_scope]. +Arguments Scope BigZ.log2 [bigZ_scope]. Arguments Scope BigZ.sqrt [bigZ_scope]. Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope]. Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope]. Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope]. +Arguments Scope BigZ.even [bigZ_scope]. +Arguments Scope BigZ.odd [bigZ_scope]. Local Notation "0" := BigZ.zero : bigZ_scope. Local Notation "1" := BigZ.one : bigZ_scope. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 099554cd0b..b341b32095 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -332,6 +332,21 @@ Module Make (N:NType) <: ZType. apply N.spec_0. Qed. + Definition log2 x := + match x with + | Pos nx => Pos (N.log2 nx) + | Neg nx => zero + end. + + Theorem spec_log2: forall x, to_Z (log2 x) = Zlog2 (to_Z x). + Proof. + intros. destruct x as [p|p]; simpl. apply N.spec_log2. + rewrite N.spec_0. + destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ]. + rewrite Zlog2_nonpos; auto with zarith. + now rewrite <- EQ. + Qed. + Definition sqrt x := match x with | Pos nx => Pos (N.sqrt nx) diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 48d166c0ab..bdaa748e4a 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -9,40 +9,12 @@ (************************************************************************) -Require Import ZAxioms ZProperties. -Require Import BinInt Zcompare Zorder ZArith_dec Zbool Zeven Zsqrt_def. +Require Import ZAxioms ZProperties BinInt Zcompare Zorder ZArith_dec + Zbool Zeven Zsqrt_def Zpow_def Zlog_def. Local Open Scope Z_scope. -(** An alternative Zpow *) - -(** The Zpow is extensionnaly equal to Zpower in ZArith, but not - convertible with it. This Zpow uses a logarithmic number of - multiplications instead of a linear one. We should try someday to - replace Zpower with this Zpow. -*) - -Definition Zpow n m := - match m with - | Z0 => 1 - | Zpos p => Piter_op Zmult p n - | Zneg p => 0 - end. - -Lemma Zpow_0_r : forall n, Zpow n 0 = 1. -Proof. reflexivity. Qed. - -Lemma Zpow_succ_r : forall a b, 0<=b -> Zpow a (Zsucc b) = a * Zpow 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 Zpow_neg_r : forall a b, b<0 -> Zpow a b = 0. -Proof. - now destruct b. -Qed. +(** Bi-directional induction for Z. *) Theorem Z_bi_induction : forall A : Z -> Prop, Proper (eq ==> iff) A -> @@ -167,12 +139,12 @@ Definition odd := Zodd_bool. (** Power *) -Program Instance pow_wd : Proper (eq==>eq==>eq) Zpow. +Program Instance pow_wd : Proper (eq==>eq==>eq) Zpower. -Definition pow_0_r := Zpow_0_r. -Definition pow_succ_r := Zpow_succ_r. -Definition pow_neg_r := Zpow_neg_r. -Definition pow := Zpow. +Definition pow_0_r := Zpower_0_r. +Definition pow_succ_r := Zpower_succ_r. +Definition pow_neg_r := Zpower_neg_r. +Definition pow := Zpower. (** Sqrt *) @@ -185,6 +157,14 @@ Definition sqrt_spec := Zsqrt_spec. Definition sqrt_neg := Zsqrt_neg. Definition sqrt := Zsqrt. +(** Log2 *) + +Program Instance log2_wd : Proper (eq==>eq) Zlog2. + +Definition log2_spec := Zlog2_spec. +Definition log2_nonpos := Zlog2_nonpos. +Definition log2 := Zlog2. + (** We define [eq] only here to avoid refering to this [eq] above. *) Definition eq := (@eq Z). diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index 37f5b294e1..b5c761a6f2 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -51,6 +51,7 @@ Module Type ZType. Parameter pow_N : t -> N -> t. Parameter pow : t -> t -> t. Parameter sqrt : t -> t. + Parameter log2 : t -> t. Parameter div_eucl : t -> t -> t * t. Parameter div : t -> t -> t. Parameter modulo : t -> t -> t. @@ -79,6 +80,7 @@ Module Type ZType. Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n. Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n]. Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x]. + Parameter spec_log2: forall x, [log2 x] = Zlog2 [x]. Parameter spec_div_eucl: forall x y, let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. Parameter spec_div: forall x y, [div x y] = [x] / [y]. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index c2965016ad..96f243fa62 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -20,7 +20,7 @@ Hint Rewrite spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn - spec_pow spec_even spec_odd + spec_pow spec_log2 spec_even spec_odd : zsimpl. Ltac zsimpl := autorewrite with zsimpl. @@ -293,6 +293,21 @@ Proof. intros n. zify. apply Zsqrt_neg. Qed. +(** Log2 *) + +Program Instance log2_wd : Proper (eq==>eq) log2. + +Lemma log2_spec : forall n, 0 + 2^(log2 n) <= n /\ n < 2^(succ (log2 n)). +Proof. + intros n. zify. apply Zlog2_spec. +Qed. + +Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0. +Proof. + intros n. zify. apply Zlog2_nonpos. +Qed. + (** Even / Odd *) Definition Even n := exists m, n == 2*m. diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v new file mode 100644 index 0000000000..4742cc6991 --- /dev/null +++ b/theories/Numbers/NatInt/NZLog.v @@ -0,0 +1,297 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t. +End Log2. + +Module Type NZLog2Spec (A : NZOrdAxiomsSig')(B : Pow' A)(C : Log2 A). + Import A B C. + Declare Instance log2_wd : Proper (eq==>eq) log2. + Axiom log2_spec : forall a, 0 2^(log2 a) <= a < 2^(S (log2 a)). + Axiom log2_nonpos : forall a, a<=0 -> log2 a == 0. +End NZLog2Spec. + +Module Type NZLog2 (A : NZOrdAxiomsSig)(B : Pow A) := Log2 A <+ NZLog2Spec A B. + +(** Derived properties of logarithm *) + +Module NZLog2Prop + (Import A : NZOrdAxiomsSig') + (Import B : NZPow' A) + (Import C : NZLog2 A B) + (Import D : NZMulOrderProp A) + (Import E : NZPowProp A B D). + +(** log2 is always non-negative *) + +Lemma log2_nonneg : forall a, 0 <= log2 a. +Proof. + intros a. destruct (le_gt_cases a 0) as [Ha|Ha]. + now rewrite log2_nonpos. + destruct (log2_spec a Ha) as (_,LT). + apply lt_succ_r, (pow_gt_1 2). order'. + rewrite <- le_succ_l, <- one_succ in Ha. order. +Qed. + +(** A tactic for proving positivity and non-negativity *) + +Ltac order_pos := +((apply add_pos_pos || apply add_nonneg_nonneg || + apply mul_pos_pos || apply mul_nonneg_nonneg || + apply pow_nonneg || apply log2_nonneg || + apply (le_le_succ_r 0)); + order_pos) (* in case of success of an apply, we recurse *) +|| order'. (* otherwise *) + +(** The spec of log2 indeed determines it *) + +Lemma log2_unique : forall a b, 0<=b -> 2^b<=a<2^(S b) -> log2 a == b. +Proof. + intros a b Hb (LEb,LTb). + assert (Ha : 0 < a). + apply lt_le_trans with (2^b); trivial. + apply pow_pos_nonneg; order'. + assert (Hc := log2_nonneg a). + destruct (log2_spec a Ha) as (LEc,LTc). + assert (log2 a <= b). + apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. + now apply le_le_succ_r. + assert (b <= log2 a). + apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. + now apply le_le_succ_r. + order. +Qed. + +(** log2 is exact on powers of 2 *) + +Lemma log2_pow2 : forall a, 0<=a -> log2 (2^a) == a. +Proof. + intros a Ha. + apply log2_unique; trivial. + split. order. apply pow_lt_mono_r. order'. split; trivial. + apply lt_succ_diag_r. +Qed. + +(** log2 and basic constants *) + +Lemma log2_1 : log2 1 == 0. +Proof. + rewrite <- (pow_0_r 2). now apply log2_pow2. +Qed. + +Lemma log2_2 : log2 2 == 1. +Proof. + rewrite <- (pow_1_r 2). apply log2_pow2; order'. +Qed. + +(** log2 n is strictly positive for 1 0 < log2 a. +Proof. + intros a Ha. + assert (Ha' : 0 < a) by order'. + assert (H := log2_nonneg a). apply le_lteq in H. + destruct H; trivial. + generalize (log2_spec a Ha'). rewrite <- H in *. nzsimpl; try order. + intros (_,H'). rewrite two_succ in H'. apply lt_succ_r in H'; order. +Qed. + +(** Said otherwise, log2 is null only below 1 *) + +Lemma log2_null : forall a, log2 a == 0 <-> a <= 1. +Proof. + intros a. split; intros H. + destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. + generalize (log2_pos a Ha); order. + apply le_lteq in H; destruct H. + apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ. + rewrite H. apply log2_1. +Qed. + +(** log2 is a monotone function (but not a strict one) *) + +Lemma log2_le_mono : forall a b, a<=b -> log2 a <= log2 b. +Proof. + intros a b H. + destruct (le_gt_cases a 0) as [Ha|Ha]. + rewrite log2_nonpos; order_pos. + assert (Hb : 0 < b) by order. + destruct (log2_spec a Ha) as (LEa,_). + destruct (log2_spec b Hb) as (_,LTb). + apply lt_succ_r, (pow_lt_mono_r_iff 2); order_pos. +Qed. + +(** No reverse result for <=, consider for instance log2 3 <= log2 2 *) + +Lemma log2_lt_cancel : forall a b, log2 a < log2 b -> a < b. +Proof. + intros a b H. + destruct (le_gt_cases b 0) as [Hb|Hb]. + rewrite (log2_nonpos b) in H; trivial. + generalize (log2_nonneg a); order. + destruct (le_gt_cases a 0) as [Ha|Ha]. order. + destruct (log2_spec a Ha) as (_,LTa). + destruct (log2_spec b Hb) as (LEb,_). + apply le_succ_l in H. + apply (pow_le_mono_r_iff 2) in H; order_pos. +Qed. + +(** When left side is a power of 2, we have an equivalence for <= *) + +Lemma log2_le_pow2 : forall a b, 0 0<=b -> (2^b<=a <-> b <= log2 a). +Proof. + intros a b Ha Hb. + split; intros H. + rewrite <- (log2_pow2 b); trivial. now apply log2_le_mono. + transitivity (2^(log2 a)). + apply pow_le_mono_r; order'. + now destruct (log2_spec a Ha). +Qed. + +(** When right side is a square, we have an equivalence for < *) + +Lemma log2_lt_pow2 : forall a b, 0 0<=b -> (a<2^b <-> log2 a < b). +Proof. + intros a b Ha Hb. + split; intros H. + apply (pow_lt_mono_r_iff 2); try order_pos. + apply le_lt_trans with a; trivial. + now destruct (log2_spec a Ha). + apply log2_lt_cancel; try order. + now rewrite log2_pow2. +Qed. + +(** Comparing log2 and identity *) + +Lemma log2_lt_lin : forall a, 0 log2 a < a. +Proof. + intros a Ha. + apply (pow_lt_mono_r_iff 2); try order_pos. + apply le_lt_trans with a. + now destruct (log2_spec a Ha). + apply pow_gt_lin_r; order'. +Qed. + +Lemma log2_le_lin : forall a, 0<=a -> log2 a <= a. +Proof. + intros a Ha. + apply le_lteq in Ha; destruct Ha as [Ha|Ha]. + now apply lt_le_incl, log2_lt_lin. + rewrite <- Ha, log2_nonpos; order. +Qed. + +(** Log2 and multiplication. *) + +(** Due to rounding error, we don't have the usual + [log2 (a*b) = log2 a + log2 b] but we may be off by 1 at most *) + +Lemma log2_mul_below : forall a b, 0 0 + log2 a + log2 b <= log2 (a*b). +Proof. + intros a b Ha Hb. + apply log2_le_pow2; try order_pos. + rewrite pow_add_r by order_pos. + apply mul_le_mono_nonneg; try apply log2_spec; order_pos. +Qed. + +Lemma log2_mul_above : forall a b, 0<=a -> 0<=b -> + log2 (a*b) <= log2 a + log2 b + 1. +Proof. + intros a b Ha Hb. + apply le_lteq in Ha. destruct Ha as [Ha|Ha]. + apply le_lteq in Hb. destruct Hb as [Hb|Hb]. + apply lt_succ_r. + rewrite add_1_r, <- add_succ_r, <- add_succ_l. + apply log2_lt_pow2; try order_pos. + rewrite pow_add_r by order_pos. + apply mul_lt_mono_nonneg; try order; now apply log2_spec. + rewrite <- Hb. nzsimpl. rewrite log2_nonpos; order_pos. + rewrite <- Ha. nzsimpl. rewrite log2_nonpos; order_pos. +Qed. + +(** And we can't find better approximations in general. + - The lower bound is exact for powers of 2. + - Concerning the upper bound, for any c>0, take a=b=2^c-1, + then log2 (a*b) = c+c -1 while (log2 a) = (log2 b) = c-1 +*) + +(** Log2 and addition *) + +Lemma log2_add_le : forall a b, a~=1 -> b~=1 -> log2 (a+b) <= log2 a + log2 b. +Proof. + intros a b Ha Hb. + destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|]. + rewrite one_succ, lt_succ_r in Ha'. + rewrite (log2_nonpos a); trivial. nzsimpl. apply log2_le_mono. + rewrite <- (add_0_l b) at 2. now apply add_le_mono. + destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. + rewrite one_succ, lt_succ_r in Hb'. + rewrite (log2_nonpos b); trivial. nzsimpl. apply log2_le_mono. + rewrite <- (add_0_r a) at 2. now apply add_le_mono. + clear Ha Hb. + apply lt_succ_r. + apply log2_lt_pow2; try order_pos. + rewrite pow_succ_r by order_pos. + rewrite two_succ, one_succ at 1. nzsimpl. + apply add_lt_mono. + apply lt_le_trans with (2^(S (log2 a))). apply log2_spec; order'. + apply pow_le_mono_r. order'. rewrite <- add_1_r. apply add_le_mono_l. + rewrite one_succ; now apply le_succ_l, log2_pos. + apply lt_le_trans with (2^(S (log2 b))). apply log2_spec; order'. + apply pow_le_mono_r. order'. rewrite <- add_1_l. apply add_le_mono_r. + rewrite one_succ; now apply le_succ_l, log2_pos. +Qed. + +(** The sum of two log2 is less than twice the log2 of the sum. + This can almost be seen as a convexity inequality. *) + +Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b -> + 2*2*a*b <= (a+b)*(a+b). +Proof. + intros. + nzsimpl'. + rewrite !mul_add_distr_l, !mul_add_distr_r. + rewrite (add_comm _ (b*b)), add_assoc. + apply add_le_mono_r. + rewrite (add_shuffle0 (a*a)), (mul_comm b a). + apply add_le_mono_r. + rewrite (mul_comm a b) at 1. + now apply crossmul_le_addsquare. +Qed. + +Lemma add_log2_lt : forall a b, 0 0 + log2 a + log2 b < 2 * log2 (a+b). +Proof. + intros a b Ha Hb. + apply (pow_lt_mono_r_iff 2); try order_pos. + rewrite !pow_add_r by order_pos. + apply le_lt_trans with (a*b). + apply mul_le_mono_nonneg; try order_pos; now apply log2_spec. + apply (mul_lt_mono_pos_r (2^2)). + apply pow_pos_nonneg; order'. + rewrite (mul_comm 2). + rewrite <- pow_add_r by order_pos. + rewrite <- mul_succ_l. + rewrite pow_mul_r by order_pos. + apply le_lt_trans with ((a+b)^2). + rewrite !pow_2_r, (mul_comm (a*b)), mul_assoc. + apply quadmul_le_squareadd; order. + apply pow_lt_mono_l. order'. split. order_pos. + apply log2_spec; order_pos. +Qed. + +(** We can't be more precise : consider for instance a=2 b=4, then 1+2<2*2 *) + +End NZLog2Prop. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 78e38b3cf3..2fbfb04c24 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Export NZAxioms NZPow NZSqrt NZDiv. +Require Export NZAxioms NZPow NZSqrt NZLog NZDiv. (** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *) @@ -32,8 +32,6 @@ Module Type Parity (Import N : NAxiomsMiniSig'). Axiom odd_spec : forall n, odd n = true <-> Odd n. End Parity. -(** For Power and Sqrt functions : NZPow and NZSqrt are enough *) - (** Division Function : we reuse NZDiv.DivMod and NZDiv.NZDivCommon, and add to that a N-specific constraint. *) @@ -41,15 +39,16 @@ Module Type NDivSpecific (Import N : NAxiomsMiniSig')(Import DM : DivMod' N). Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b. End NDivSpecific. +(** For pow sqrt log2, the NZ axiomatizations are enough. *) (** We now group everything together. *) Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity - <+ NZPow.NZPow <+ NZSqrt.NZSqrt + <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ DivMod <+ NZDivCommon <+ NDivSpecific. Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity - <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' + <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ DivMod' <+ NZDivCommon <+ NDivSpecific. diff --git a/theories/Numbers/Natural/Abstract/NLog.v b/theories/Numbers/Natural/Abstract/NLog.v new file mode 100644 index 0000000000..7fbf4280a3 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NLog.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 0 -> + Lemma spec_log2_pos : forall x, [x]<>0 -> 2^[log2 x] <= [x] < 2^([log2 x]+1). Proof. intros x H. rewrite log2_fold. @@ -1178,6 +1178,15 @@ Module Make (W0:CyclicType) <: NType. apply ZnZ.spec_head0; auto with zarith. Qed. + Lemma spec_log2 : forall x, [log2 x] = Zlog2 [x]. + Proof. + intros. destruct (Z_lt_ge_dec 0 [x]). + symmetry. apply Z.log2_unique. apply spec_pos. + apply spec_log2_pos. intro EQ; rewrite EQ in *; auto with zarith. + rewrite spec_log2_0. rewrite Z.log2_nonpos; auto with zarith. + generalize (spec_pos x); auto with zarith. + Qed. + Lemma log2_digits_head0 : forall x, 0 < [x] -> [log2 x] = Zpos (digits x) - [head0 x] - 1. Proof. @@ -1311,7 +1320,7 @@ Module Make (W0:CyclicType) <: NType. (* [x] <> 0 *) apply spec_unsafe_shiftl_aux with ([log2 x] + 1); auto with zarith. generalize (spec_pos (log2 x)); auto with zarith. - destruct (spec_log2 x); auto with zarith. + destruct (spec_log2_pos x); auto with zarith. rewrite log2_digits_head0; auto with zarith. generalize (spec_pos x); auto with zarith. Qed. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 8b7b06966f..97e7b36784 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -62,18 +62,7 @@ Program Instance lt_wd : Proper (eq==>eq==>iff) Nlt. Definition lt_eq_cases := Nle_lteq. Definition lt_irrefl := Nlt_irrefl. - -Theorem lt_succ_r : forall n m, n < (Nsucc m) <-> n <= m. -Proof. -intros n m; unfold Nlt, Nle; destruct n as [| p]; destruct m as [| q]; simpl; -split; intro H; try reflexivity; try discriminate. -destruct p; simpl; intros; discriminate. exfalso; now apply H. -apply -> Pcompare_p_Sq in H. destruct H as [H | H]. -now rewrite H. now rewrite H, Pcompare_refl. -apply <- Pcompare_p_Sq. case_eq ((p ?= q)%positive Eq); intro H1. -right; now apply Pcompare_Eq_eq. now left. exfalso; now apply H. -Qed. - +Definition lt_succ_r := Nlt_succ_r. Definition eqb_eq := Neqb_eq. Definition compare_spec := Ncompare_spec. @@ -169,6 +158,12 @@ Definition pow_succ_r n p (H:0 <= p) := Npow_succ_r n p. Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. Proof. destruct b; discriminate. Qed. +(** Log2 *) + +Program Instance log2_wd : Proper (eq==>eq) Nlog2. +Definition log2_spec := Nlog2_spec. +Definition log2_nonpos := Nlog2_nonpos. + (** Sqrt *) Program Instance sqrt_wd : Proper (eq==>eq) Nsqrt. @@ -202,6 +197,7 @@ Definition pow := Npow. Definition even := Neven. Definition odd := Nodd. Definition sqrt := Nsqrt. +Definition log2 := Nlog2. Include NProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index a3203948a4..3255fda683 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -444,6 +444,11 @@ Definition pow_succ_r := pow_succ_r. Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed. Definition pow := pow. +Program Instance log2_wd : Proper (eq==>eq) log2. +Definition log2_spec := log2_spec. +Definition log2_nonpos := log2_nonpos. +Definition log2 := log2. + Program Instance sqrt_wd : Proper (eq==>eq) sqrt. Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a. Lemma sqrt_neg : forall a, a<0 -> sqrt a = 0. inversion 1. Qed. diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index 703897eba5..dc2d27fa44 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -78,8 +78,7 @@ Module Type NType. Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n. Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n]. Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x]. - Parameter spec_log2_0: forall x, [x] = 0 -> [log2 x] = 0. - Parameter spec_log2: forall x, [x]<>0 -> 2^[log2 x] <= [x] < 2^([log2 x]+1). + Parameter spec_log2: forall x, [log2 x] = Zlog2 [x]. Parameter spec_div_eucl: forall x y, let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. Parameter spec_div: forall x y, [div x y] = [x] / [y]. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index f242951e54..64dcd1967e 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -16,7 +16,8 @@ Module NTypeIsNAxioms (Import N : NType'). Hint Rewrite spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_sqrt - spec_max spec_min spec_pow_pos spec_pow_N spec_pow spec_even spec_odd + spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow + spec_even spec_odd : nsimpl. Ltac nsimpl := autorewrite with nsimpl. Ltac ncongruence := unfold eq, to_N; repeat red; intros; nsimpl; congruence. @@ -242,6 +243,22 @@ Proof. generalize (spec_pos n); omega. Qed. +(** Log2 *) + +Program Instance log2_wd : Proper (eq==>eq) log2. + +Lemma log2_spec : forall n, 0 + 2^(log2 n) <= n /\ n < 2^(succ (log2 n)). +Proof. + intros n. zify. change (Zlog2 [n]+1)%Z with (Zsucc (Zlog2 [n])). + apply Zlog2_spec. +Qed. + +Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0. +Proof. + intros n. zify. apply Zlog2_nonpos. +Qed. + (** Even / Odd *) Definition Even n := exists m, n == 2*m. diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget index 7867b8caa0..fbfaa80075 100644 --- a/theories/Numbers/vo.itarget +++ b/theories/Numbers/vo.itarget @@ -49,6 +49,7 @@ NatInt/NZDomain.vo NatInt/NZDiv.vo NatInt/NZPow.vo NatInt/NZSqrt.vo +NatInt/NZLog.vo Natural/Abstract/NAddOrder.vo Natural/Abstract/NAdd.vo Natural/Abstract/NAxioms.vo @@ -65,6 +66,7 @@ Natural/Abstract/NMaxMin.vo Natural/Abstract/NParity.vo Natural/Abstract/NPow.vo Natural/Abstract/NSqrt.vo +Natural/Abstract/NLog.vo Natural/BigN/BigN.vo Natural/BigN/Nbasic.vo Natural/BigN/NMake_gen.vo diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index 93121d48f2..8199ed369c 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 0000000000..05ceca2013 --- /dev/null +++ b/theories/ZArith/Zlog_def.v @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 620d6324f7..96d05760bb 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 *) +(* 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 54ecf49130..bafee949d4 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 28db6848dc..7802a8655d 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 -- cgit v1.2.3