diff options
Diffstat (limited to 'flocq/Core/Digits.v')
| -rw-r--r-- | flocq/Core/Digits.v | 37 |
1 files changed, 30 insertions, 7 deletions
diff --git a/flocq/Core/Digits.v b/flocq/Core/Digits.v index a18ff8d6..7fe51cca 100644 --- a/flocq/Core/Digits.v +++ b/flocq/Core/Digits.v @@ -18,12 +18,12 @@ COPYING file for more details. *) From Coq Require Import Lia ZArith Zquot. +From Coq Require SpecFloat. Require Import Zaux. -Require Import SpecFloatCompat. -Notation digits2_pos := digits2_pos (only parsing). -Notation Zdigits2 := Zdigits2 (only parsing). +Notation digits2_pos := SpecFloat.digits2_pos (only parsing). +Notation Zdigits2 := SpecFloat.Zdigits2 (only parsing). (** Number of bits (radix 2) of a positive integer. @@ -594,12 +594,12 @@ destruct (Zle_or_lt k2' k) as [Hk''|Hk'']. now apply Zdigit_slice_out. rewrite Zdigit_slice by now split. apply Zdigit_slice_out. -zify ; lia. -rewrite Zdigit_slice by (zify ; lia). +lia. +rewrite Zdigit_slice by lia. rewrite (Zdigit_slice n (k1 + k1')) by now split. rewrite Zdigit_slice. now rewrite Zplus_assoc. -zify ; lia. +lia. unfold Zslice. rewrite Z.min_r. now rewrite Zle_bool_false. @@ -821,6 +821,18 @@ Proof. now intros [|n|n]. Qed. +Theorem Zdigits_opp : + forall n, Zdigits (Z.opp n) = Zdigits n. +Proof. +now intros [|n|n]. +Qed. + +Theorem Zdigits_cond_Zopp : + forall s n, Zdigits (cond_Zopp s n) = Zdigits n. +Proof. +now intros [|] [|n|n]. +Qed. + Theorem Zdigits_gt_0 : forall n, n <> Z0 -> (0 < Zdigits n)%Z. Proof. @@ -933,7 +945,7 @@ intros x y Zx Hxy. assert (Hx := Zdigits_correct x). assert (Hy := Zdigits_correct y). apply (Zpower_lt_Zpower beta). -zify ; lia. +lia. Qed. Theorem lt_Zdigits : @@ -1103,6 +1115,17 @@ exact Hm. now rewrite <- (Z.abs_eq m) at 1. Qed. +Theorem Zdigits_succ_le : + forall x, (0 <= x)%Z -> + (Zdigits (x + 1) <= Zdigits x + 1)%Z. +Proof. + destruct x as [| p | p]; [intros _; now simpl | intros _ | lia]. + transitivity (Zdigits (Z.pos p * beta ^ 1)); + [apply Zdigits_le; [lia |] | rewrite Zdigits_mult_Zpower; lia]. + apply Ztac.Zlt_le_add_1. rewrite <-Z.mul_1_r at 1. apply Zmult_lt_compat_l; [lia |]. + rewrite Z.pow_1_r. apply radix_gt_1. +Qed. + End Fcore_digits. (** Specialized version for computing the number of bits of an integer *) |