diff options
Diffstat (limited to 'flocq/Core/Fcore_digits.v')
| -rw-r--r-- | flocq/Core/Fcore_digits.v | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v index 13174d29..d40c1a09 100644 --- a/flocq/Core/Fcore_digits.v +++ b/flocq/Core/Fcore_digits.v @@ -21,7 +21,7 @@ Require Import ZArith. Require Import Zquot. Require Import Fcore_Zaux. -(** Computes the number of bits (radix 2) of a positive integer. +(** Number of bits (radix 2) of a positive integer. It serves as an upper bound on the number of digits to ensure termination. *) @@ -466,6 +466,8 @@ now apply Hd. now rewrite 3!Zdigit_lt. Qed. +(** 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)). @@ -545,6 +547,8 @@ rewrite Zle_bool_true with (1 := Hk). now apply Zscale_mul_pow. Qed. +(** 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. @@ -756,6 +760,7 @@ Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z := End digits_aux. (** Number of digits of an integer *) + Definition Zdigits n := match n with | Z0 => Z0 @@ -1011,7 +1016,7 @@ generalize (Zpower_gt_Zdigits e x). omega. Qed. -(** Characterizes the number digits of a product. +(** Number of digits of a product. This strong version is needed for proofs of division and square root algorithms, since they involve operation remainders. @@ -1126,6 +1131,8 @@ Qed. End Fcore_digits. +(** Specialized version for computing the number of bits of an integer *) + Section Zdigits2. Theorem Z_of_nat_S_digits2_Pnat : |