From 8f8443a5249123f2b5b2dc680d51247468441932 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 24 May 2020 09:26:42 +0200 Subject: [PATCH] Properly name generic_format_FLT_bpow. --- examples/Average.v | 26 +++++++++++++------------- src/Core/FLT.v | 26 +++++++++++++------------- src/IEEE754/BinarySingleNaN.v | 20 ++++++-------------- src/Pff/Pff2Flocq.v | 20 ++++++++++---------- src/Prop/Round_odd.v | 8 ++++---- 5 files changed, 46 insertions(+), 54 deletions(-) diff --git a/examples/Average.v b/examples/Average.v index cc4279d..89538c1 100644 --- a/examples/Average.v +++ b/examples/Average.v @@ -298,8 +298,8 @@ assert (0 < pred_flt f). apply Rlt_le_trans with (bpow emin). apply bpow_gt_0. apply pred_ge_gt... -apply FLT_format_bpow... -omega. +apply generic_format_FLT_bpow... +apply Z.le_refl. apply Rlt_le_trans with (2:=H1). apply bpow_lt. unfold Prec_gt_0 in prec_gt_0_; omega. @@ -371,7 +371,7 @@ apply Rle_ge; now left. assert (bpow (mag radix2 f -1) + ulp_flt (bpow (mag radix2 f-1)) <= f). rewrite <- succ_eq_pos;[idtac|apply bpow_ge_0]. apply succ_le_lt... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... unfold Prec_gt_0 in prec_gt_0_;omega. rewrite ulp_bpow in H4. unfold FLT_exp in H4. @@ -626,7 +626,7 @@ now apply sym_eq, FLT_round_half. apply FLT_format_half. apply generic_format_round... apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... unfold Prec_gt_0 in prec_gt_0_; omega. (* subnormal case: addition is exact, but division by 2 is not *) intros H. @@ -716,7 +716,7 @@ apply bpow_gt_0. (* *) rewrite avg_naive_correct. apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. Qed. @@ -828,7 +828,7 @@ apply trans_eq with (x/2). apply round_plus_small_id; try assumption. apply Rle_trans with (2:=K2). apply abs_round_le_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. unfold a; apply sym_eq. replace ((x+y)/2) with (x/2+y/2) by field. @@ -1009,7 +1009,7 @@ apply round_le... unfold Rdiv; apply Rmult_le_compat_r. lra. apply round_le_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. case (Rle_or_lt (y-x) (bpow emin)); trivial. intros H2. @@ -1018,7 +1018,7 @@ apply Rlt_not_eq. apply Rlt_le_trans with (bpow emin). apply bpow_gt_0. apply round_DN_pt... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. now left. replace (bpow emin /2) with (bpow (emin-1)). @@ -1231,7 +1231,7 @@ rewrite round_generic with (x:=y)... apply Rlt_le_trans with (bpow emin). apply bpow_gt_0. apply round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. apply Rle_trans with (1:=H). right; apply Rabs_right. @@ -1367,7 +1367,7 @@ rewrite J1,J3,J2,J4,T1,T2; unfold F2R; simpl. rewrite Rmult_0_l, Rmult_1_l, 2!Rplus_0_l. unfold Rminus; rewrite Ropp_0, Rplus_0_r. rewrite (round_generic _ _ _ (bpow (emin)))... -2: apply FLT_format_bpow... +2: apply generic_format_FLT_bpow... 2: omega. rewrite G1. rewrite round_0... @@ -1399,13 +1399,13 @@ rewrite J1,J3,J2,J4,T1,T2; unfold F2R; simpl. rewrite Rmult_0_l, Rplus_0_r. replace (0 - _ * bpow emin) with (bpow emin) by ring. rewrite (round_generic _ _ _ (bpow emin))... -2: apply FLT_format_bpow... +2: apply generic_format_FLT_bpow... 2: omega. rewrite G1. replace (_ * bpow emin + 0) with (-bpow emin) by ring. rewrite round_generic... 2: apply generic_format_opp. -2: apply FLT_format_bpow... +2: apply generic_format_FLT_bpow... 2: omega. replace (- bpow emin - _ * bpow emin / 2) with (-(bpow emin/2)) by field. rewrite Rabs_Ropp. @@ -1561,7 +1561,7 @@ apply round_generic... apply FLT_format_half... apply generic_format_round... apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... unfold Prec_gt_0 in prec_gt_0_; omega. rewrite Rabs_right; try assumption. apply Rle_ge; left; apply Rplus_lt_reg_l with u; now ring_simplify. diff --git a/src/Core/FLT.v b/src/Core/FLT.v index 577e9a3..1ed312a 100644 --- a/src/Core/FLT.v +++ b/src/Core/FLT.v @@ -99,7 +99,7 @@ apply Z.le_max_l. apply Z.le_max_r. Qed. -Theorem FLT_format_bpow : +Theorem generic_format_FLT_bpow : forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e). Proof. intros e He. @@ -108,6 +108,14 @@ apply Z.max_case; try assumption. unfold Prec_gt_0 in prec_gt_0_; omega. Qed. +Theorem FLT_format_bpow : + forall e, (emin <= e)%Z -> FLT_format (bpow e). +Proof. +intros e He. +apply FLT_format_generic. +now apply generic_format_FLT_bpow. +Qed. + Theorem FLT_format_satisfies_any : satisfies_any FLT_format. Proof. @@ -262,20 +270,12 @@ destruct (Z.max_spec (n - prec) emin) as [(Hm, Hm')|(Hm, Hm')]. revert Hn prec_gt_0_; unfold FLT_exp, Prec_gt_0; rewrite Hm'; lia. Qed. -Theorem generic_format_FLT_1 (Hemin : (emin <= 0)%Z) : +Theorem generic_format_FLT_1 : + (emin <= 0)%Z -> generic_format beta FLT_exp 1. Proof. -unfold generic_format, scaled_mantissa, cexp, F2R; simpl. -rewrite Rmult_1_l, (mag_unique beta 1 1). -{ unfold FLT_exp. - destruct (Z.max_spec_le (1 - prec) emin) as [(H,Hm)|(H,Hm)]; rewrite Hm; - (rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]); - (rewrite Ztrunc_IZR, IZR_Zpower, <-bpow_plus; - [|unfold Prec_gt_0 in prec_gt_0_; omega]); - now replace (_ + _)%Z with Z0 by ring. } -rewrite Rabs_R1; simpl; split; [now right|]. -rewrite IZR_Zpower_pos; simpl; rewrite Rmult_1_r; apply IZR_lt. -apply (Z.lt_le_trans _ 2); [omega|]; apply Zle_bool_imp_le, beta. +intros Hemin. +now apply (generic_format_FLT_bpow 0). Qed. Theorem ulp_FLT_0 : diff --git a/src/IEEE754/BinarySingleNaN.v b/src/IEEE754/BinarySingleNaN.v index 974a138..c7ea611 100644 --- a/src/IEEE754/BinarySingleNaN.v +++ b/src/IEEE754/BinarySingleNaN.v @@ -2472,11 +2472,8 @@ Proof. intros [sx|sx| |sx mx ex Hx] Fx ; try easy ; simpl. - repeat split. change fexp with (FLT_exp emin prec). - rewrite ulp_FLT_small. + rewrite ulp_FLT_0 by easy. apply F2R_bpow. - easy. - rewrite Rabs_R0. - apply bpow_gt_0. - destruct (binary_round_correct mode_ZR false 1 ex) as [H1 H2]. revert H2. simpl. @@ -2499,16 +2496,11 @@ intros [sx|sx| |sx mx ex Hx] Fx ; try easy ; simpl. + rewrite F2R_bpow. apply sym_eq, round_generic. typeclasses eauto. - apply generic_format_bpow. - apply (canonical_canonical_mantissa false) in H5. - rewrite H5 at 2. - simpl. - unfold cexp. - apply monotone_exp. - apply FLT_exp_monotone. - rewrite mag_F2R_Zdigits by easy. - generalize (Zdigits_gt_0 radix2 (Zpos mx)). - lia. + apply generic_format_FLT_bpow. + easy. + rewrite (canonical_canonical_mantissa false _ _ H5). + apply Z.max_le_iff. + now right. Qed. Definition Bulp' x := Bldexp mode_NE Bone (fexp (snd (Bfrexp x))). diff --git a/src/Pff/Pff2Flocq.v b/src/Pff/Pff2Flocq.v index 8b4c7fe..834e2ba 100644 --- a/src/Pff/Pff2Flocq.v +++ b/src/Pff/Pff2Flocq.v @@ -1020,7 +1020,7 @@ left; unfold u1. rewrite K; apply round_0... right; unfold u1. apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. Qed. @@ -1337,7 +1337,7 @@ apply round_FLT_plus_ge; try assumption... apply generic_format_round... apply generic_format_round... apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. apply Rle_trans with (2:=H). apply bpow_le; omega. @@ -1371,7 +1371,7 @@ right. case U2; intros Hy. unfold r1; rewrite Hy, Rplus_0_r. apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. apply Rle_trans with (2:=H). apply bpow_le; omega. @@ -1395,7 +1395,7 @@ assert (T:round_flt (u1 + y) <> 0 -> (bpow beta (emin + 3 * prec - 2 - prec) <= intros K; apply round_FLT_plus_ge... apply generic_format_round... apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. apply Rle_trans with (2:=H). apply bpow_le; omega. @@ -1411,7 +1411,7 @@ rewrite H1, Rplus_0_l. unfold u2, u1; rewrite H2, round_0... fold u1 u2; intros H2. apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. apply Rle_trans with (2:=H2). apply bpow_le; omega. @@ -1427,7 +1427,7 @@ intros L; case U1; intros J; try easy. apply Rle_trans with (2:=J); apply bpow_le. omega. intros K; apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. assert (K':u1 + y + u2 <> 0). intros L; apply K; rewrite L. @@ -1906,7 +1906,7 @@ unfold Rminus; apply round_FLT_plus_ge... apply generic_format_round... apply generic_format_opp, generic_format_round... apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. apply Rle_trans with (2:=U1 Z1); apply bpow_le; omega. apply round_plus_neq_0... @@ -1960,7 +1960,7 @@ Lemma U5_discri1_aux : forall x y e, format x -> format y Proof with auto with typeclass_instances. intros x y e Fx Fy He Hex Hey H. apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... case (Rle_or_lt (bpow e) (Rabs (x+y))); intros H1; try easy. absurd (round_flt (x + y) = x + y); try assumption. apply round_generic... @@ -2225,7 +2225,7 @@ rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by omega. rewrite Hfp''. apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. apply Rle_trans with (2:=U1 Zbb). apply bpow_le; omega. @@ -2236,7 +2236,7 @@ rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by omega. rewrite Hfq''. apply abs_round_ge_generic... -apply FLT_format_bpow... +apply generic_format_FLT_bpow... omega. apply Rle_trans with (2:=U2 Zac). apply bpow_le; omega. diff --git a/src/Prop/Round_odd.v b/src/Prop/Round_odd.v index df2952c..48572db 100644 --- a/src/Prop/Round_odd.v +++ b/src/Prop/Round_odd.v @@ -1105,14 +1105,14 @@ intros _; rewrite Zx, round_0... destruct (mag beta x) as (e,He); simpl; intros H. apply mag_unique; split. apply abs_round_ge_generic... -apply FLT_format_bpow... -auto with zarith. +apply generic_format_FLT_bpow... +now apply Z.lt_le_pred. now apply He. assert (V: (Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) <= bpow beta e)%R). apply abs_round_le_generic... -apply FLT_format_bpow... -auto with zarith. +apply generic_format_FLT_bpow... +now apply Zlt_le_weak. left; now apply He. case V; try easy; intros K. assert (H0:Rnd_odd_pt beta (FLT_exp emin prec) x (round beta (FLT_exp emin prec) Zrnd_odd x)).