Library Flocq.Calc.Fcalc_digits
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010-2011 Sylvie Boldo
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.
Copyright (C) 2010-2011 Sylvie Boldo
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 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).
Theorem Zdigits_ln_beta :
forall n,
n <> Z0 ->
Zdigits beta n = ln_beta beta (Z2R n).
Theorem ln_beta_F2R_Zdigits :
forall m e, m <> Z0 ->
(ln_beta beta (F2R (Float beta m e)) = Zdigits beta m + e :> Z)%Z.
Theorem Zdigits_mult_Zpower :
forall m e,
m <> Z0 -> (0 <= e)%Z ->
Zdigits beta (m * Zpower beta e) = (Zdigits beta m + e)%Z.
Theorem Zdigits_Zpower :
forall e,
(0 <= e)%Z ->
Zdigits beta (Zpower beta e) = (e + 1)%Z.
Theorem Zdigits_le :
forall x y,
(0 <= x)%Z -> (x <= y)%Z ->
(Zdigits beta x <= Zdigits beta y)%Z.
Theorem lt_Zdigits :
forall x y,
(0 <= y)%Z ->
(Zdigits beta x < Zdigits beta y)%Z ->
(x < y)%Z.
Theorem Zpower_le_Zdigits :
forall e x,
(e < Zdigits beta x)%Z ->
(Zpower beta e <= Zabs x)%Z.
Theorem Zdigits_le_Zpower :
forall e x,
(Zabs x < Zpower beta e)%Z ->
(Zdigits beta x <= e)%Z.
Theorem Zpower_gt_Zdigits :
forall e x,
(Zdigits beta x <= e)%Z ->
(Zabs x < Zpower beta e)%Z.
Theorem Zdigits_gt_Zpower :
forall e x,
(Zpower beta e <= Zabs x)%Z ->
(e < Zdigits beta x)%Z.
Characterizes the number digits of a product.
This strong version is needed for proofs of division and square root algorithms, since they involve operation remainders.
This strong version is needed for proofs of division and square root algorithms, since they involve operation remainders.
Theorem Zdigits_mult_strong :
forall x y,
(0 <= x)%Z -> (0 <= y)%Z ->
(Zdigits beta (x + y + x * y) <= Zdigits beta x + Zdigits beta y)%Z.
Theorem Zdigits_mult :
forall x y,
(Zdigits beta (x * y) <= Zdigits beta x + Zdigits beta y)%Z.
Theorem Zdigits_mult_ge :
forall x y,
(x <> 0)%Z -> (y <> 0)%Z ->
(Zdigits beta x + Zdigits beta y - 1 <= Zdigits beta (x * y))%Z.
Theorem Zdigits_div_Zpower :
forall m e,
(0 <= m)%Z ->
(0 <= e <= Zdigits beta m)%Z ->
Zdigits beta (m / Zpower beta e) = (Zdigits beta m - e)%Z.
End Fcalc_digits.
Definition radix2 := Build_radix 2 (refl_equal _).
Theorem Z_of_nat_S_digits2_Pnat :
forall m : positive,
Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m).