Properly name generic_format_FLT_bpow.

validsdp · May 24, 2020 · 8f8443a · 8f8443a
1 parent c238944
commit 8f8443a
Show file tree

Hide file tree

Showing 5 changed files with 46 additions and 54 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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)).