From eb0c7276eac6ba563dafa98733ee44538004271c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 26 Oct 2011 14:35:31 +0000 Subject: [PATCH] Move digits to Core and rename it Zdigits. Change its correctness proof to be integer-only. --- src/Appli/Fappli_IEEE.v | 3 +- src/Calc/Fcalc_digits.v | 183 ++++------------------------------------ src/Core/Fcore_digits.v | 132 +++++++++++++++++++++++++++++ 3 files changed, 150 insertions(+), 168 deletions(-) diff --git a/src/Appli/Fappli_IEEE.v b/src/Appli/Fappli_IEEE.v index e8f2185..ac8096c 100644 --- a/src/Appli/Fappli_IEEE.v +++ b/src/Appli/Fappli_IEEE.v @@ -19,6 +19,7 @@ COPYING file for more details. (** * IEEE-754 arithmetic *) Require Import Fcore. +Require Import Fcore_digits. Require Import Fcalc_digits. Require Import Fcalc_round. Require Import Fcalc_bracket. @@ -858,7 +859,7 @@ generalize (H _ _ Hx) (H _ _ Hy). clear x y sx sy Hx Hy H. unfold fexp, FLT_exp. refine (_ (digits_mult_ge radix2 (Zpos mx) (Zpos my) _ _)) ; try discriminate. -refine (_ (digits_gt_0 radix2 (Zpos mx) _) (digits_gt_0 radix2 (Zpos my) _)) ; try discriminate. +refine (_ (Zdigits_gt_0 radix2 (Zpos mx) _) (Zdigits_gt_0 radix2 (Zpos my) _)) ; try discriminate. generalize (digits radix2 (Zpos mx)) (digits radix2 (Zpos my)) (digits radix2 (Zpos mx * Zpos my)). clear -Hmax. unfold emin. diff --git a/src/Calc/Fcalc_digits.v b/src/Calc/Fcalc_digits.v index 499ae1c..e117553 100644 --- a/src/Calc/Fcalc_digits.v +++ b/src/Calc/Fcalc_digits.v @@ -23,96 +23,14 @@ COPYING file for more details. Require Import Fcore_Raux. Require Import Fcore_defs. Require Import Fcore_float_prop. +Require Import Fcore_digits. Section Fcalc_digits. Variable beta : radix. Notation bpow e := (bpow beta e). -(** Computes the number of bits (radix 2) of a positive integer. - -It serves as an upper bound on the number of digits to ensure termination. -*) - -Fixpoint digits2_Pnat (n : positive) : nat := - match n with - | xH => O - | xO p => S (digits2_Pnat p) - | xI p => S (digits2_Pnat p) - end. - -Theorem digits2_Pnat_correct : - forall n, - let d := digits2_Pnat n in - (Zpower_nat 2 d <= Zpos n < Zpower_nat 2 (S d))%Z. -Proof. -intros n d. unfold d. clear. -assert (Hp: forall m, (Zpower_nat 2 (S m) = 2 * Zpower_nat 2 m)%Z) by easy. -induction n ; simpl. -rewrite Zpos_xI, 2!Hp. -omega. -rewrite (Zpos_xO n), 2!Hp. -omega. -now split. -Qed. - -Section digits_aux. - -Variable p : Z. -Hypothesis Hp : (0 <= p)%Z. - -Fixpoint digits_aux (nb pow : Z) (n : nat) { struct n } : Z := - match n with - | O => nb - | S n => if Zlt_bool p pow then nb else digits_aux (nb + 1) (Zmult beta pow) n - end. - -Lemma digits_aux_invariant : - forall k n nb, - (0 <= nb)%Z -> - (Zpower beta (nb + Z_of_nat k - 1) <= p)%Z -> - digits_aux (nb + Z_of_nat k) (Zpower beta (nb + Z_of_nat k)) n = - digits_aux nb (Zpower beta nb) (n + k). -Proof. -induction k ; intros n nb Hnb. -now rewrite Zplus_0_r, plus_0_r. -rewrite inj_S. -unfold Zsucc. -intros H. -rewrite (Zplus_comm _ 1), Zplus_assoc. -rewrite IHk. -rewrite <- plus_n_Sm. -simpl. -generalize (Zlt_cases p (Zpower beta nb)). -case Zlt_bool ; intros Hpp. -elim (Zlt_irrefl p). -apply Zlt_le_trans with (1 := Hpp). -apply Zle_trans with (2 := H). -replace (nb + (Z_of_nat k + 1) - 1)%Z with (nb + Z_of_nat k)%Z by ring. -apply le_Z2R. -rewrite Z2R_Zpower with (1 := Hnb). -rewrite Z2R_Zpower. -apply bpow_le. -omega. -omega. -rewrite Zpower_exp. -unfold Zpower at 2, Zpower_pos, iter_pos. -rewrite Zmult_1_r. -now rewrite Zmult_comm. -now apply Zle_ge. -easy. -omega. -now rewrite <- Zplus_assoc, (Zplus_comm 1). -Qed. - -End digits_aux. - -Definition digits n := - match n with - | Z0 => Z0 - | Zneg p => digits_aux (Zpos p) 1 beta (digits2_Pnat p) - | Zpos p => digits_aux n 1 beta (digits2_Pnat p) - end. +Notation digits := (Zdigits beta). Theorem digits_abs : forall n, digits (Zabs n) = digits n. @@ -126,89 +44,18 @@ Theorem digits_ln_beta : digits n = ln_beta beta (Z2R n). Proof. intros n Hn. -destruct (ln_beta beta (Z2R n)) as (e, He). -simpl. +destruct (ln_beta beta (Z2R n)) as (e, He) ; simpl. specialize (He (Z2R_neq _ _ Hn)). rewrite <- Z2R_abs in He. -assert (Hn': (0 < Zabs n)%Z). -destruct n ; try easy. -now elim Hn. -rewrite <- digits_abs. -destruct (Zabs n) as [|p|p] ; try (now elim Hn'). -clear n Hn Hn'. -simpl. -assert (He1: (0 <= e - 1)%Z). -apply Zlt_0_le_0_pred. -apply (lt_bpow beta). +assert (Hd := Zdigits_correct beta n). +assert (Hd' := Zdigits_gt_0 beta n). +apply Zle_antisym ; apply (bpow_lt_bpow beta). apply Rle_lt_trans with (2 := proj2 He). -apply (Z2R_le 1). -now apply (Zlt_le_succ 0). -assert (He2: (Z_of_nat (Zabs_nat (e - 1)) = e - 1)%Z). -rewrite inj_Zabs_nat. -now apply Zabs_eq. -replace (radix_val beta) with (Zpower beta 1). -replace (digits2_Pnat p) with (digits2_Pnat p - Zabs_nat (e - 1) + Zabs_nat (e - 1)). -rewrite <- digits_aux_invariant. -rewrite He2. -ring_simplify (1 + (e - 1))%Z. -destruct (digits2_Pnat p - Zabs_nat (e - 1)) as [|n]. -easy. -simpl. -generalize (Zlt_cases (Zpos p) (Zpower beta e)). -case Zlt_bool ; intros Hpp. -easy. -elim Rlt_not_le with (1 := proj2 He). -rewrite <- Z2R_Zpower. -apply Z2R_le. -now apply Zge_le. -omega. -easy. -rewrite He2. -ring_simplify (1 + (e - 1) - 1)%Z. -apply le_Z2R. -now rewrite Z2R_Zpower. -rewrite plus_comm. -apply le_plus_minus_r. -apply inj_le_rev. -rewrite He2. -cut (e - 1 < Z_of_nat (S (digits2_Pnat p)))%Z. -rewrite inj_S. -omega. -apply (lt_bpow beta). +rewrite <- Z2R_Zpower by omega. +now apply Z2R_le. apply Rle_lt_trans with (1 := proj1 He). -rewrite <- Z2R_Zpower_nat. -apply Z2R_lt. -apply Zlt_le_trans with (Zpower_nat 2 (S (digits2_Pnat p))). -exact (proj2 (digits2_Pnat_correct p)). -clear. -induction (S (digits2_Pnat p)). -easy. -change (2 * Zpower_nat 2 n <= beta * Zpower_nat beta n)%Z. -apply Zmult_le_compat ; try easy. -apply Zle_bool_imp_le. -apply beta. -now apply Zpower_NR0. -apply Zmult_1_r. -Qed. - -Theorem digits_gt_0 : - forall n, (n <> 0)%Z -> (0 < digits n)%Z. -Proof. -intros n H. -rewrite digits_ln_beta with (1 := H). -destruct ln_beta as (e, He). simpl. -apply (lt_bpow beta). -apply Rle_lt_trans with (Rabs (Z2R n)). -simpl. -rewrite <- Z2R_abs. -apply (Z2R_le 1). -apply (Zlt_le_succ 0). -revert H. -case n ; try easy. -intros H. -now elim H. -apply He. -now apply (Z2R_neq _ 0). +rewrite <- Z2R_Zpower by omega. +now apply Z2R_lt. Qed. Theorem digits_ge_0 : @@ -218,7 +65,7 @@ intros n. destruct (Z_eq_dec n 0) as [H|H]. now rewrite H. apply Zlt_le_weak. -now apply digits_gt_0. +now apply Zdigits_gt_0. Qed. Theorem ln_beta_F2R_digits : @@ -472,8 +319,8 @@ apply Zpower_le_digits. apply Zlt_pred. apply Zpower_ge_0. apply Zpower_ge_0. -generalize (digits_gt_0 x). omega. -generalize (digits_gt_0 y). omega. +generalize (Zdigits_gt_0 beta x). omega. +generalize (Zdigits_gt_0 beta y). omega. Qed. Theorem digits_shr : @@ -568,7 +415,7 @@ Definition radix2 := Build_radix 2 (refl_equal _). Theorem Z_of_nat_S_digits2_Pnat : forall m : positive, - Z_of_nat (S (digits2_Pnat m)) = digits radix2 (Zpos m). + Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m). Proof. intros m. rewrite digits_ln_beta. 2: easy. @@ -586,3 +433,5 @@ now apply Z2R_lt. rewrite inj_S. apply Zpred_succ. Qed. + +Notation digits := Zdigits (only parsing). diff --git a/src/Core/Fcore_digits.v b/src/Core/Fcore_digits.v index 4ffa331..86b7cae 100644 --- a/src/Core/Fcore_digits.v +++ b/src/Core/Fcore_digits.v @@ -214,6 +214,33 @@ apply ZO_div_pos with (2 := Hv). now apply Zlt_le_weak. Qed. +(** Computes the number of bits (radix 2) of a positive integer. + +It serves as an upper bound on the number of digits to ensure termination. +*) + +Fixpoint digits2_Pnat (n : positive) : nat := + match n with + | xH => O + | xO p => S (digits2_Pnat p) + | xI p => S (digits2_Pnat p) + end. + +Theorem digits2_Pnat_correct : + forall n, + let d := digits2_Pnat n in + (Zpower_nat 2 d <= Zpos n < Zpower_nat 2 (S d))%Z. +Proof. +intros n d. unfold d. clear. +assert (Hp: forall m, (Zpower_nat 2 (S m) = 2 * Zpower_nat 2 m)%Z) by easy. +induction n ; simpl. +rewrite Zpos_xI, 2!Hp. +omega. +rewrite (Zpos_xO n), 2!Hp. +omega. +now split. +Qed. + Section Fcore_digits. Variable beta : radix. @@ -917,4 +944,109 @@ apply Zdigit_lt. omega. Qed. +Section digits_aux. + +Variable p : Z. +Hypothesis Hp : (0 <= p)%Z. + +Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z := + match n with + | O => nb + | S n => if Zlt_bool p pow then nb else Zdigits_aux (nb + 1) (Zmult beta pow) n + end. + +End digits_aux. + +Definition Zdigits n := + match n with + | Z0 => Z0 + | Zneg p => Zdigits_aux (Zpos p) 1 beta (digits2_Pnat p) + | Zpos p => Zdigits_aux n 1 beta (digits2_Pnat p) + end. + +Theorem Zdigits_correct : + forall n, + (Zpower beta (Zdigits n - 1) <= Zabs n < Zpower beta (Zdigits n))%Z. +Proof. +cut (forall p, Zpower beta (Zdigits (Zpos p) - 1) <= Zpos p < Zpower beta (Zdigits (Zpos p)))%Z. +intros H [|n|n] ; try exact (H n). +now split. +intros n. +simpl. +(* *) +assert (U: (Zpos n < Zpower beta (Z_of_nat (S (digits2_Pnat n))))%Z). +apply Zlt_le_trans with (1 := proj2 (digits2_Pnat_correct n)). +rewrite Zpower_Zpower_nat. +rewrite Zabs_nat_Z_of_nat. +induction (S (digits2_Pnat n)). +easy. +rewrite 2!(Zpower_nat_is_exp 1 n0). +apply Zmult_le_compat with (2 := IHn0). +unfold Zpower_nat, iter_nat. +rewrite 2!Zmult_1_r. +apply Zle_bool_imp_le. +apply beta. +easy. +now apply Zpower_NR0. +apply Zle_0_nat. +(* *) +revert U. +rewrite inj_S. +unfold Zsucc. +generalize (digits2_Pnat n). +intros u U. +pattern (radix_val beta) at 2 4 ; replace (radix_val beta) with (Zpower beta 1) by apply Zmult_1_r. +assert (V: (Zpower beta (1 - 1) <= Zpos n)%Z). +now apply (Zlt_le_succ 0). +generalize (conj V U). +clear. +generalize (Zle_refl 1). +generalize 1%Z at 2 3 5 6 7 9 10. +(* *) +induction u. +easy. +rewrite inj_S; unfold Zsucc. +simpl Zdigits_aux. +intros v Hv U. +case Zlt_bool_spec ; intros K. +now split. +pattern (radix_val beta) at 2 5 ; replace (radix_val beta) with (Zpower beta 1) by apply Zmult_1_r. +rewrite Zmult_pow. +rewrite Zplus_comm. +apply IHu. +clear -Hv ; omega. +split. +now ring_simplify (1 + v - 1)%Z. +now rewrite Zplus_assoc. +easy. +apply Zle_succ_le with (1 := Hv). +Qed. + +Theorem Zdigits_abs : + forall n, Zdigits (Zabs n) = Zdigits n. +Proof. +now intros [|n|n]. +Qed. + +Theorem Zdigits_gt_0 : + forall n, n <> Z0 -> (0 < Zdigits n)%Z. +Proof. +intros n Zn. +rewrite <- (Zdigits_abs n). +assert (Hn: (0 < Zabs n)%Z). +destruct n ; try easy. +now elim Zn. +destruct (Zabs n) as [|p|p] ; try easy ; clear. +simpl. +generalize 1%Z (radix_val beta) (refl_equal Lt : (0 < 1)%Z). +induction (digits2_Pnat p). +easy. +simpl. +intros. +case Zlt_bool. +exact H. +apply IHn. +now apply Zlt_lt_succ. +Qed. + End Fcore_digits. -- GitLab