From 7644d49d591799902f50c2240900db4f302ceff5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 3 Apr 2019 18:57:47 +0200 Subject: Floats.v: avoid using module Zlogarithm in the proofs Rumor has it that this module is scheduled for removal. This is based on pull request #286, with a different implementation. Closes: #286 --- lib/Floats.v | 29 +++++++++++++++++++---------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/lib/Floats.v b/lib/Floats.v index 0247528c..ece9ea18 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -94,11 +94,26 @@ Proof. destruct x as [[]|]; simpl; intros; discriminate. Qed. +(** Relation between number of bits and base-2 logarithm *) + +Lemma digits2_log2: + forall p, Z.pos (Digits.digits2_pos p) = Z.succ (Z.log2 (Z.pos p)). +Proof. + assert (E: forall p, Digits.digits2_pos p = Pos.size p). + { induction p; simpl; rewrite ?IHp; auto. } + intros p. rewrite E. + destruct p; simpl; rewrite ?Pos.add_1_r; reflexivity. +Qed. + Local Notation __ := (eq_refl Datatypes.Lt). Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt). Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt). +Print Digits.digits2_pos. +Print Pos.size. + + (** * Double-precision FP numbers *) Module Float. @@ -115,12 +130,9 @@ Lemma transform_quiet_nan_proof (p : positive) : nan_pl 53 (Pos.lor p (iter_nat xO 51 1%positive)) = true. Proof. unfold nan_pl. intros K. - simpl. rewrite Z.ltb_lt in *. - assert (H : forall x, Digits.digits2_pos x = Pos.size x). - { induction x; simpl; auto; rewrite IHx; zify; omega. } - rewrite H, Psize_log_inf, <- Zlog2_log_inf in *. clear H. + simpl. rewrite Z.ltb_lt, digits2_log2 in *. change (Z.pos (Pos.lor p 2251799813685248)) with (Z.lor (Z.pos p) 2251799813685248%Z). - rewrite Z.log2_lor by (zify; omega). + rewrite Z.log2_lor by xomega. now apply Z.max_case. Qed. @@ -918,12 +930,9 @@ Lemma transform_quiet_nan_proof (p : positive) : nan_pl 24 (Pos.lor p (iter_nat xO 22 1%positive)) = true. Proof. unfold nan_pl. intros K. - simpl. rewrite Z.ltb_lt in *. - assert (H : forall x, Digits.digits2_pos x = Pos.size x). - { induction x; simpl; auto; rewrite IHx; zify; omega. } - rewrite H, Psize_log_inf, <- Zlog2_log_inf in *. clear H. + simpl. rewrite Z.ltb_lt, digits2_log2 in *. change (Z.pos (Pos.lor p 4194304)) with (Z.lor (Z.pos p) 4194304%Z). - rewrite Z.log2_lor by (zify; omega). + rewrite Z.log2_lor by xomega. now apply Z.max_case. Qed. -- cgit