Library Flocq.Core.Fcore_digits
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2011 Sylvie Boldo
Copyright (C) 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) 2011 Sylvie Boldo
Copyright (C) 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.
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.
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.
Section Fcore_digits.
Variable beta : radix.
Definition Zdigit n k := ZOmod (ZOdiv n (Zpower beta k)) beta.
Theorem Zdigit_lt :
forall n k,
(k < 0)%Z ->
Zdigit n k = Z0.
Theorem Zdigit_0 :
forall k, Zdigit 0 k = Z0.
Theorem Zdigit_opp :
forall n k,
Zdigit (-n) k = Zopp (Zdigit n k).
Theorem Zdigit_ge_Zpower_pos :
forall e n,
(0 <= n < Zpower beta e)%Z ->
forall k, (e <= k)%Z -> Zdigit n k = Z0.
Theorem Zdigit_ge_Zpower :
forall e n,
(Zabs n < Zpower beta e)%Z ->
forall k, (e <= k)%Z -> Zdigit n k = Z0.
Theorem Zdigit_not_0_pos :
forall e n, (0 <= e)%Z ->
(Zpower beta e <= n < Zpower beta (e + 1))%Z ->
Zdigit n e <> Z0.
Theorem Zdigit_not_0 :
forall e n, (0 <= e)%Z ->
(Zpower beta e <= Zabs n < Zpower beta (e + 1))%Z ->
Zdigit n e <> Z0.
Theorem Zdigit_mul_pow :
forall n k k', (0 <= k')%Z ->
Zdigit (n * Zpower beta k') k = Zdigit n (k - k').
Theorem Zdigit_div_pow :
forall n k k', (0 <= k)%Z -> (0 <= k')%Z ->
Zdigit (n / Zpower beta k') k = Zdigit n (k + k').
Theorem Zdigit_mod_pow :
forall n k k', (k < k')%Z ->
Zdigit (ZOmod n (Zpower beta k')) k = Zdigit n k.
Theorem Zdigit_mod_pow_out :
forall n k k', (0 <= k' <= k)%Z ->
Zdigit (ZOmod n (Zpower beta k')) k = Z0.
Fixpoint Zsum_digit f k :=
match k with
| O => Z0
| S k => (Zsum_digit f k + f (Z_of_nat k) * Zpower beta (Z_of_nat k))%Z
end.
Theorem Zsum_digit_digit :
forall n k,
Zsum_digit (Zdigit n) k = ZOmod n (Zpower beta (Z_of_nat k)).
Theorem Zpower_gt_id :
forall n, (n < Zpower beta n)%Z.
Theorem Zdigit_ext :
forall n1 n2,
(forall k, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k) ->
n1 = n2.
Theorem ZOmod_plus_pow_digit :
forall u v n, (0 <= u * v)%Z ->
(forall k, (0 <= k < n)%Z -> Zdigit u k = Z0 \/ Zdigit v k = Z0) ->
ZOmod (u + v) (Zpower beta n) = (ZOmod u (Zpower beta n) + ZOmod v (Zpower beta n))%Z.
Theorem ZOdiv_plus_pow_digit :
forall u v n, (0 <= u * v)%Z ->
(forall k, (0 <= k < n)%Z -> Zdigit u k = Z0 \/ Zdigit v k = Z0) ->
ZOdiv (u + v) (Zpower beta n) = (ZOdiv u (Zpower beta n) + ZOdiv v (Zpower beta n))%Z.
Theorem Zdigit_plus :
forall u v, (0 <= u * v)%Z ->
(forall k, (0 <= k)%Z -> Zdigit u k = Z0 \/ Zdigit v k = Z0) ->
forall k,
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z.
Definition Zscale n k :=
if Zle_bool 0 k then n * Zpower beta k else ZOdiv n (Zpower beta (-k)).
Theorem Zdigit_scale :
forall n k k', (0 <= k')%Z ->
Zdigit (Zscale n k) k' = Zdigit n (k' - k).
Theorem Zscale_0 :
forall k,
Zscale 0 k = Z0.
Theorem Zsame_sign_scale :
forall n k,
(0 <= n * Zscale n k)%Z.
Theorem Zscale_mul_pow :
forall n k k', (0 <= k)%Z ->
Zscale (n * Zpower beta k) k' = Zscale n (k + k').
Theorem Zscale_scale :
forall n k k', (0 <= k)%Z ->
Zscale (Zscale n k) k' = Zscale n (k + k').
Definition Zslice n k1 k2 :=
if Zle_bool 0 k2 then ZOmod (Zscale n (-k1)) (Zpower beta k2) else Z0.
Theorem Zdigit_slice :
forall n k1 k2 k, (0 <= k < k2) ->
Zdigit (Zslice n k1 k2) k = Zdigit n (k1 + k).
Theorem Zdigit_slice_out :
forall n k1 k2 k, (k2 <= k)%Z ->
Zdigit (Zslice n k1 k2) k = Z0.
Theorem Zslice_0 :
forall k k',
Zslice 0 k k' = Z0.
Theorem Zsame_sign_slice :
forall n k k',
(0 <= n * Zslice n k k')%Z.
Theorem Zslice_slice :
forall n k1 k2 k1' k2', (0 <= k1' <= k2)%Z ->
Zslice (Zslice n k1 k2) k1' k2' = Zslice n (k1 + k1') (Zmin (k2 - k1') k2').
Theorem Zslice_mul_pow :
forall n k k1 k2, (0 <= k)%Z ->
Zslice (n * Zpower beta k) k1 k2 = Zslice n (k1 - k) k2.
Theorem Zslice_div_pow :
forall n k k1 k2, (0 <= k)%Z -> (0 <= k1)%Z ->
Zslice (n / Zpower beta k) k1 k2 = Zslice n (k1 + k) k2.
Theorem Zslice_scale :
forall n k k1 k2, (0 <= k1)%Z ->
Zslice (Zscale n k) k1 k2 = Zslice n (k1 - k) k2.
Theorem Zslice_div_pow_scale :
forall n k k1 k2, (0 <= k)%Z ->
Zslice (n / Zpower beta k) k1 k2 = Zscale (Zslice n k (k1 + k2)) (-k1).
Theorem Zplus_slice :
forall n k l1 l2, (0 <= l1)%Z -> (0 <= l2)%Z ->
(Zslice n k l1 + Zscale (Zslice n (k + l1) l2) l1)%Z = Zslice n k (l1 + l2).
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.
Number of digits of an integer
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.
Theorem Zdigits_abs :
forall n, Zdigits (Zabs n) = Zdigits n.
Theorem Zdigits_gt_0 :
forall n, n <> Z0 -> (0 < Zdigits n)%Z.
Theorem Zdigits_ge_0 :
forall n, (0 <= Zdigits n)%Z.
Theorem Zdigit_out :
forall n k, (Zdigits n <= k)%Z ->
Zdigit n k = Z0.
Theorem Zdigit_digits :
forall n, n <> Z0 ->
Zdigit n (Zdigits n - 1) <> Z0.
Theorem Zdigits_slice :
forall n k l, (0 <= l)%Z ->
(Zdigits (Zslice n k l) <= l)%Z.
End Fcore_digits.
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.
Theorem Zdigits_abs :
forall n, Zdigits (Zabs n) = Zdigits n.
Theorem Zdigits_gt_0 :
forall n, n <> Z0 -> (0 < Zdigits n)%Z.
Theorem Zdigits_ge_0 :
forall n, (0 <= Zdigits n)%Z.
Theorem Zdigit_out :
forall n k, (Zdigits n <= k)%Z ->
Zdigit n k = Z0.
Theorem Zdigit_digits :
forall n, n <> Z0 ->
Zdigit n (Zdigits n - 1) <> Z0.
Theorem Zdigits_slice :
forall n k l, (0 <= l)%Z ->
(Zdigits (Zslice n k l) <= l)%Z.
End Fcore_digits.