Library Flocq.Core.Digits

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.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.

Require Import ZArith Zquot.
Require Import Zaux.

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
  | xHO
  | xO pS (digits2_Pnat p)
  | xI pS (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 = Zopp (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,
  (Zabs 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 Zabs 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
  | OZ0
  | 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') (Zmin (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
  | Onb
  | S nif 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
  | Z0Z0
  | Zneg pZdigits_aux (Zpos p) 1 beta (digits2_Pnat p)
  | Zpos pZdigits_aux n 1 beta (digits2_Pnat p)
  end.

Theorem Zdigits_correct :
   n,
  (Zpower beta (Zdigits n - 1) Zabs n < Zpower beta (Zdigits n))%Z.

Theorem Zdigits_unique :
   n d,
  (Zpower beta (d - 1) Zabs n < Zpower beta d)%Z
  Zdigits n = d.

Theorem Zdigits_abs :
   n, Zdigits (Zabs 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 Zabs x)%Z.

Theorem Zdigits_le_Zpower :
   e x,
  (Zabs x < Zpower beta e)%Z
  (Zdigits x e)%Z.

Theorem Zpower_gt_Zdigits :
   e x,
  (Zdigits x e)%Z
  (Zabs x < Zpower beta e)%Z.

Theorem Zdigits_gt_Zpower :
   e x,
  (Zpower beta e Zabs 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.

End Fcore_digits.

Specialized version for computing the number of bits of an integer

Section Zdigits2.

Theorem Z_of_nat_S_digits2_Pnat :
   m : positive,
  Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m).

Fixpoint digits2_pos (n : positive) : positive :=
  match n with
  | xHxH
  | xO pPsucc (digits2_pos p)
  | xI pPsucc (digits2_pos p)
  end.

Theorem Zpos_digits2_pos :
   m : positive,
  Zpos (digits2_pos m) = Zdigits radix2 (Zpos m).

Definition Zdigits2 n :=
  match n with
  | Z0n
  | Zpos pZpos (digits2_pos p)
  | Zneg pZpos (digits2_pos p)
  end.

Lemma Zdigits2_Zdigits :
   n, Zdigits2 n = Zdigits radix2 n.

End Zdigits2.