Library Flocq.Core.Digits
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: https://flocq.gitlabpages.inria.fr/
Copyright (C) 2011-2018 Sylvie Boldo
Copyright (C) 2011-2018 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-2018 Guillaume Melquiond
From Coq Require Import Lia ZArith Zquot.
From Coq Require SpecFloat.
Require Import Zaux.
Notation digits2_pos := SpecFloat.digits2_pos (only parsing).
Notation Zdigits2 := SpecFloat.Zdigits2 (only parsing).
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 :
∀ 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 := Z.rem (Z.quot n (Zpower beta k)) beta.
Theorem Zdigit_lt :
∀ n k,
(k < 0)%Z →
Zdigit n k = Z0.
Theorem Zdigit_0 :
∀ k, Zdigit 0 k = Z0.
Theorem Zdigit_opp :
∀ n k,
Zdigit (-n) k = Z.opp (Zdigit n k).
Theorem Zdigit_ge_Zpower_pos :
∀ e n,
(0 ≤ n < Zpower beta e)%Z →
∀ k, (e ≤ k)%Z → Zdigit n k = Z0.
Theorem Zdigit_ge_Zpower :
∀ e n,
(Z.abs n < Zpower beta e)%Z →
∀ k, (e ≤ k)%Z → Zdigit n k = Z0.
Theorem Zdigit_not_0_pos :
∀ e n, (0 ≤ e)%Z →
(Zpower beta e ≤ n < Zpower beta (e + 1))%Z →
Zdigit n e ≠ Z0.
Theorem Zdigit_not_0 :
∀ e n, (0 ≤ e)%Z →
(Zpower beta e ≤ Z.abs n < Zpower beta (e + 1))%Z →
Zdigit n e ≠ Z0.
Theorem Zdigit_mul_pow :
∀ n k k', (0 ≤ k')%Z →
Zdigit (n × Zpower beta k') k = Zdigit n (k - k').
Theorem Zdigit_div_pow :
∀ n k k', (0 ≤ k)%Z → (0 ≤ k')%Z →
Zdigit (Z.quot n (Zpower beta k')) k = Zdigit n (k + k').
Theorem Zdigit_mod_pow :
∀ n k k', (k < k')%Z →
Zdigit (Z.rem n (Zpower beta k')) k = Zdigit n k.
Theorem Zdigit_mod_pow_out :
∀ n k k', (0 ≤ k' ≤ k)%Z →
Zdigit (Z.rem 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 :
∀ n k,
Zsum_digit (Zdigit n) k = Z.rem n (Zpower beta (Z_of_nat k)).
Theorem Zdigit_ext :
∀ n1 n2,
(∀ k, (0 ≤ k)%Z → Zdigit n1 k = Zdigit n2 k) →
n1 = n2.
Theorem ZOmod_plus_pow_digit :
∀ u v n, (0 ≤ u × v)%Z →
(∀ k, (0 ≤ k < n)%Z → Zdigit u k = Z0 ∨ Zdigit v k = Z0) →
Z.rem (u + v) (Zpower beta n) = (Z.rem u (Zpower beta n) + Z.rem v (Zpower beta n))%Z.
Theorem ZOdiv_plus_pow_digit :
∀ u v n, (0 ≤ u × v)%Z →
(∀ k, (0 ≤ k < n)%Z → Zdigit u k = Z0 ∨ Zdigit v k = Z0) →
Z.quot (u + v) (Zpower beta n) = (Z.quot u (Zpower beta n) + Z.quot v (Zpower beta n))%Z.
Theorem Zdigit_plus :
∀ u v, (0 ≤ u × v)%Z →
(∀ k, (0 ≤ k)%Z → Zdigit u k = Z0 ∨ Zdigit v k = Z0) →
∀ k,
Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z.
Left and right shifts
Definition Zscale n k :=
if Zle_bool 0 k then (n × Zpower beta k)%Z else Z.quot n (Zpower beta (-k)).
Theorem Zdigit_scale :
∀ n k k', (0 ≤ k')%Z →
Zdigit (Zscale n k) k' = Zdigit n (k' - k).
Theorem Zscale_0 :
∀ k,
Zscale 0 k = Z0.
Theorem Zsame_sign_scale :
∀ n k,
(0 ≤ n × Zscale n k)%Z.
Theorem Zscale_mul_pow :
∀ n k k', (0 ≤ k)%Z →
Zscale (n × Zpower beta k) k' = Zscale n (k + k').
Theorem Zscale_scale :
∀ n k k', (0 ≤ k)%Z →
Zscale (Zscale n k) k' = Zscale n (k + k').
Slice of an integer
Definition Zslice n k1 k2 :=
if Zle_bool 0 k2 then Z.rem (Zscale n (-k1)) (Zpower beta k2) else Z0.
Theorem Zdigit_slice :
∀ n k1 k2 k, (0 ≤ k < k2)%Z →
Zdigit (Zslice n k1 k2) k = Zdigit n (k1 + k).
Theorem Zdigit_slice_out :
∀ n k1 k2 k, (k2 ≤ k)%Z →
Zdigit (Zslice n k1 k2) k = Z0.
Theorem Zslice_0 :
∀ k k',
Zslice 0 k k' = Z0.
Theorem Zsame_sign_slice :
∀ n k k',
(0 ≤ n × Zslice n k k')%Z.
Theorem Zslice_slice :
∀ n k1 k2 k1' k2', (0 ≤ k1' ≤ k2)%Z →
Zslice (Zslice n k1 k2) k1' k2' = Zslice n (k1 + k1') (Z.min (k2 - k1') k2').
Theorem Zslice_mul_pow :
∀ n k k1 k2, (0 ≤ k)%Z →
Zslice (n × Zpower beta k) k1 k2 = Zslice n (k1 - k) k2.
Theorem Zslice_div_pow :
∀ n k k1 k2, (0 ≤ k)%Z → (0 ≤ k1)%Z →
Zslice (Z.quot n (Zpower beta k)) k1 k2 = Zslice n (k1 + k) k2.
Theorem Zslice_scale :
∀ n k k1 k2, (0 ≤ k1)%Z →
Zslice (Zscale n k) k1 k2 = Zslice n (k1 - k) k2.
Theorem Zslice_div_pow_scale :
∀ n k k1 k2, (0 ≤ k)%Z →
Zslice (Z.quot n (Zpower beta k)) k1 k2 = Zscale (Zslice n k (k1 + k2)) (-k1).
Theorem Zplus_slice :
∀ 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.
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 :
∀ n,
(Zpower beta (Zdigits n - 1) ≤ Z.abs n < Zpower beta (Zdigits n))%Z.
Theorem Zdigits_unique :
∀ n d,
(Zpower beta (d - 1) ≤ Z.abs n < Zpower beta d)%Z →
Zdigits n = d.
Theorem Zdigits_abs :
∀ n, Zdigits (Z.abs n) = Zdigits n.
Theorem Zdigits_opp :
∀ n, Zdigits (Z.opp n) = Zdigits n.
Theorem Zdigits_cond_Zopp :
∀ s n, Zdigits (cond_Zopp s n) = Zdigits n.
Theorem Zdigits_gt_0 :
∀ n, n ≠ Z0 → (0 < Zdigits n)%Z.
Theorem Zdigits_ge_0 :
∀ n, (0 ≤ Zdigits n)%Z.
Theorem Zdigit_out :
∀ n k, (Zdigits n ≤ k)%Z →
Zdigit n k = Z0.
Theorem Zdigit_digits :
∀ n, n ≠ Z0 →
Zdigit n (Zdigits n - 1) ≠ Z0.
Theorem Zdigits_slice :
∀ n k l, (0 ≤ l)%Z →
(Zdigits (Zslice n k l) ≤ l)%Z.
Theorem Zdigits_mult_Zpower :
∀ m e,
m ≠ Z0 → (0 ≤ e)%Z →
Zdigits (m × Zpower beta e) = (Zdigits m + e)%Z.
Theorem Zdigits_Zpower :
∀ e,
(0 ≤ e)%Z →
Zdigits (Zpower beta e) = (e + 1)%Z.
Theorem Zdigits_le :
∀ x y,
(0 ≤ x)%Z → (x ≤ y)%Z →
(Zdigits x ≤ Zdigits y)%Z.
Theorem lt_Zdigits :
∀ x y,
(0 ≤ y)%Z →
(Zdigits x < Zdigits y)%Z →
(x < y)%Z.
Theorem Zpower_le_Zdigits :
∀ e x,
(e < Zdigits x)%Z →
(Zpower beta e ≤ Z.abs x)%Z.
Theorem Zdigits_le_Zpower :
∀ e x,
(Z.abs x < Zpower beta e)%Z →
(Zdigits x ≤ e)%Z.
Theorem Zpower_gt_Zdigits :
∀ e x,
(Zdigits x ≤ e)%Z →
(Z.abs x < Zpower beta e)%Z.
Theorem Zdigits_gt_Zpower :
∀ e x,
(Zpower beta e ≤ Z.abs x)%Z →
(e < Zdigits x)%Z.
Number of digits of a product.
This strong version is needed for proofs of division and square root
algorithms, since they involve operation remainders.
Theorem Zdigits_mult_strong :
∀ x y,
(0 ≤ x)%Z → (0 ≤ y)%Z →
(Zdigits (x + y + x × y) ≤ Zdigits x + Zdigits y)%Z.
Theorem Zdigits_mult :
∀ x y,
(Zdigits (x × y) ≤ Zdigits x + Zdigits y)%Z.
Theorem Zdigits_mult_ge :
∀ x y,
(x ≠ 0)%Z → (y ≠ 0)%Z →
(Zdigits x + Zdigits y - 1 ≤ Zdigits (x × y))%Z.
Theorem Zdigits_div_Zpower :
∀ m e,
(0 ≤ m)%Z →
(0 ≤ e ≤ Zdigits m)%Z →
Zdigits (m / Zpower beta e) = (Zdigits m - e)%Z.
Theorem Zdigits_succ_le :
∀ x, (0 ≤ x)%Z →
(Zdigits (x + 1) ≤ Zdigits x + 1)%Z.
End Fcore_digits.
Specialized version for computing the number of bits of an integer