From 0af966a42eb60e9af43f9a450d924758a83946c6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Sep 2015 15:41:50 +0200 Subject: Upgrade to Flocq 2.5.0. Note: this version of Flocq is compatible with both Coq 8.4 and 8.5. --- flocq/Prop/Fprop_div_sqrt_error.v | 16 ++-- flocq/Prop/Fprop_mult_error.v | 5 +- flocq/Prop/Fprop_relative.v | 168 +++++++++----------------------------- 3 files changed, 50 insertions(+), 139 deletions(-) (limited to 'flocq/Prop') diff --git a/flocq/Prop/Fprop_div_sqrt_error.v b/flocq/Prop/Fprop_div_sqrt_error.v index ec00ca4e..9d29001d 100644 --- a/flocq/Prop/Fprop_div_sqrt_error.v +++ b/flocq/Prop/Fprop_div_sqrt_error.v @@ -95,9 +95,6 @@ intros e; apply Zle_refl. now rewrite F2R_opp, F2R_mult, <- Hr1, <- Hy1. (* *) destruct (relative_error_FLX_ex beta prec (prec_gt_0 prec) rnd (x / y)%R) as (eps,(Heps1,Heps2)). -apply Rmult_integral_contrapositive_currified. -exact Zx. -now apply Rinv_neq_0_compat. rewrite Heps2. rewrite <- Rabs_Ropp. replace (-(x + - (x / y * (1 + eps) * y)))%R with (x * eps)%R by now field. @@ -135,8 +132,11 @@ now apply Rabs_pos_lt. rewrite Rabs_Ropp. replace (bpow (Fexp fr)) with (ulp beta (FLX_exp prec) (F2R fr)). rewrite <- Hr1. -apply ulp_error_f... -unfold ulp; apply f_equal. +apply error_lt_ulp_round... +apply Rmult_integral_contrapositive_currified; try apply Rinv_neq_0_compat; assumption. +rewrite ulp_neq_0. +2: now rewrite <- Hr1. +apply f_equal. now rewrite Hr2, <- Hr1. replace (prec+(Fexp fr+Fexp fy))%Z with ((prec+Fexp fy)+Fexp fr)%Z by ring. rewrite bpow_plus. @@ -246,8 +246,10 @@ apply Rmult_le_compat_r. apply Rabs_pos. apply Rle_trans with (/2*ulp beta (FLX_exp prec) (F2R fr))%R. rewrite <- Hr1. -apply ulp_half_error_f... -right; unfold ulp; apply f_equal. +apply error_le_half_ulp_round... +right; rewrite ulp_neq_0. +2: now rewrite <- Hr1. +apply f_equal. rewrite Hr2, <- Hr1; trivial. rewrite Rmult_assoc, Rmult_comm. replace (prec+(Fexp fr+Fexp fr))%Z with (Fexp fr + (prec+Fexp fr))%Z by ring. diff --git a/flocq/Prop/Fprop_mult_error.v b/flocq/Prop/Fprop_mult_error.v index e84e80b4..7c71627b 100644 --- a/flocq/Prop/Fprop_mult_error.v +++ b/flocq/Prop/Fprop_mult_error.v @@ -126,8 +126,9 @@ apply Zplus_le_compat_r. rewrite ln_beta_unique with (1 := Hexy). apply ln_beta_le_bpow with (1 := Hz). replace (bpow (exy - prec)) with (ulp beta (FLX_exp prec) (x * y)). -apply ulp_error... -unfold ulp, canonic_exp. +apply error_lt_ulp... +rewrite ulp_neq_0; trivial. +unfold canonic_exp. now rewrite ln_beta_unique with (1 := Hexy). apply Hc1. reflexivity. diff --git a/flocq/Prop/Fprop_relative.v b/flocq/Prop/Fprop_relative.v index f0a8f344..585b71da 100644 --- a/flocq/Prop/Fprop_relative.v +++ b/flocq/Prop/Fprop_relative.v @@ -35,7 +35,7 @@ Section relative_error_conversion. Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. -Lemma relative_error_lt_conversion' : +Lemma relative_error_lt_conversion : forall x b, (0 < b)%R -> (x <> 0 -> Rabs (round beta fexp rnd x - x) < b * Rabs x)%R -> exists eps, @@ -62,19 +62,6 @@ rewrite Rinv_l with (1 := Hx0). now rewrite Rabs_R1, Rmult_1_r. Qed. -(* TODO: remove *) -Lemma relative_error_lt_conversion : - forall x b, (0 < b)%R -> - (Rabs (round beta fexp rnd x - x) < b * Rabs x)%R -> - exists eps, - (Rabs eps < b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R. -Proof. -intros x b Hb0 Hxb. -apply relative_error_lt_conversion'. -exact Hb0. -now intros _. -Qed. - Lemma relative_error_le_conversion : forall x b, (0 <= b)%R -> (Rabs (round beta fexp rnd x - x) <= b * Rabs x)%R -> @@ -113,16 +100,15 @@ Theorem relative_error : forall x, (bpow emin <= Rabs x)%R -> (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R. -Proof. +Proof with auto with typeclass_instances. intros x Hx. -apply Rlt_le_trans with (ulp beta fexp x)%R. -now apply ulp_error. -unfold ulp, canonic_exp. assert (Hx': (x <> 0)%R). -intros H. -apply Rlt_not_le with (2 := Hx). -rewrite H, Rabs_R0. -apply bpow_gt_0. +intros T; contradict Hx; rewrite T, Rabs_R0. +apply Rlt_not_le, bpow_gt_0. +apply Rlt_le_trans with (ulp beta fexp x)%R. +now apply error_lt_ulp... +rewrite ulp_neq_0; trivial. +unfold canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx'). @@ -150,6 +136,7 @@ Proof with auto with typeclass_instances. intros x Hx. apply relative_error_lt_conversion... apply bpow_gt_0. +intros _. now apply relative_error. Qed. @@ -168,28 +155,17 @@ rewrite F2R_0, F2R_Zabs. now apply Rabs_pos_lt. Qed. -Theorem relative_error_F2R_emin_ex' : +Theorem relative_error_F2R_emin_ex : forall m, let x := F2R (Float beta m emin) in exists eps, (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R. Proof with auto with typeclass_instances. intros m x. -apply relative_error_lt_conversion'... +apply relative_error_lt_conversion... apply bpow_gt_0. now apply relative_error_F2R_emin. Qed. -(* TODO: remove *) -Theorem relative_error_F2R_emin_ex : - forall m, let x := F2R (Float beta m emin) in - (x <> 0)%R -> - exists eps, - (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R. -Proof with auto with typeclass_instances. -intros m x _. -apply relative_error_F2R_emin_ex'. -Qed. - Theorem relative_error_round : (0 < p)%Z -> forall x, @@ -197,14 +173,13 @@ Theorem relative_error_round : (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs (round beta fexp rnd x))%R. Proof with auto with typeclass_instances. intros Hp x Hx. -apply Rlt_le_trans with (ulp beta fexp x)%R. -now apply ulp_error. assert (Hx': (x <> 0)%R). -intros H. -apply Rlt_not_le with (2 := Hx). -rewrite H, Rabs_R0. -apply bpow_gt_0. -unfold ulp, canonic_exp. +intros T; contradict Hx; rewrite T, Rabs_R0. +apply Rlt_not_le, bpow_gt_0. +apply Rlt_le_trans with (ulp beta fexp x)%R. +now apply error_lt_ulp. +rewrite ulp_neq_0; trivial. +unfold canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx'). @@ -222,7 +197,7 @@ apply bpow_ge_0. generalize He. apply round_abs_abs... clear rnd valid_rnd x Hx Hx' He. -intros rnd valid_rnd x Hx. +intros rnd valid_rnd x _ Hx. rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))). now apply round_le. apply generic_format_bpow. @@ -257,7 +232,7 @@ Theorem relative_error_N : Proof. intros x Hx. apply Rle_trans with (/2 * ulp beta fexp x)%R. -now apply ulp_half_error. +now apply error_le_half_ulp. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Rlt_le. @@ -268,7 +243,8 @@ intros H. apply Rlt_not_le with (2 := Hx). rewrite H, Rabs_R0. apply bpow_gt_0. -unfold ulp, canonic_exp. +rewrite ulp_neq_0; trivial. +unfold canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx'). @@ -348,7 +324,7 @@ Theorem relative_error_N_round : Proof with auto with typeclass_instances. intros Hp x Hx. apply Rle_trans with (/2 * ulp beta fexp x)%R. -now apply ulp_half_error. +now apply error_le_half_ulp. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Rlt_le. @@ -359,7 +335,8 @@ intros H. apply Rlt_not_le with (2 := Hx). rewrite H, Rabs_R0. apply bpow_gt_0. -unfold ulp, canonic_exp. +rewrite ulp_neq_0; trivial. +unfold canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx'). @@ -377,7 +354,7 @@ apply bpow_ge_0. generalize He. apply round_abs_abs... clear rnd valid_rnd x Hx Hx' He. -intros rnd valid_rnd x Hx. +intros rnd valid_rnd x _ Hx. rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))). now apply round_le. apply generic_format_bpow. @@ -428,17 +405,6 @@ Qed. Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. -(* TODO: remove *) -Theorem relative_error_FLT_F2R_emin : - forall m, let x := F2R (Float beta m (emin + prec - 1)) in - (x <> 0)%R -> - (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R. -Proof with auto with typeclass_instances. -intros m x Hx. -apply relative_error_F2R_emin... -apply relative_error_FLT_aux. -Qed. - Theorem relative_error_FLT : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> @@ -449,7 +415,7 @@ apply relative_error with (emin + prec - 1)%Z... apply relative_error_FLT_aux. Qed. -Theorem relative_error_FLT_F2R_emin' : +Theorem relative_error_FLT_F2R_emin : forall m, let x := F2R (Float beta m emin) in (x <> 0)%R -> (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R. @@ -472,26 +438,13 @@ now exists (Float beta m emin). now apply relative_error_FLT. Qed. -Theorem relative_error_FLT_F2R_emin_ex' : +Theorem relative_error_FLT_F2R_emin_ex : forall m, let x := F2R (Float beta m emin) in exists eps, (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R. Proof with auto with typeclass_instances. intros m x. -apply relative_error_lt_conversion'... -apply bpow_gt_0. -now apply relative_error_FLT_F2R_emin'. -Qed. - -(* TODO: remove *) -Theorem relative_error_FLT_F2R_emin_ex : - forall m, let x := F2R (Float beta m (emin + prec - 1)) in - (x <> 0)%R -> - exists eps, - (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R. -Proof with auto with typeclass_instances. -intros m x _. -apply relative_error_lt_conversion'... +apply relative_error_lt_conversion... apply bpow_gt_0. now apply relative_error_FLT_F2R_emin. Qed. @@ -506,7 +459,7 @@ Proof with auto with typeclass_instances. intros x Hx. apply relative_error_lt_conversion... apply bpow_gt_0. -now apply relative_error_FLT. +intros _; now apply relative_error_FLT. Qed. Variable choice : Z -> bool. @@ -548,7 +501,7 @@ apply relative_error_N_round with (emin + prec - 1)%Z... apply relative_error_FLT_aux. Qed. -Theorem relative_error_N_FLT_F2R_emin' : +Theorem relative_error_N_FLT_F2R_emin : forall m, let x := F2R (Float beta m emin) in (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R. Proof with auto with typeclass_instances. @@ -573,17 +526,7 @@ now exists (Float beta m emin). now apply relative_error_N_FLT. Qed. -(* TODO: remove *) -Theorem relative_error_N_FLT_F2R_emin : - forall m, let x := F2R (Float beta m (emin + prec - 1)) in - (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R. -Proof with auto with typeclass_instances. -intros m x. -apply relative_error_N_F2R_emin... -apply relative_error_FLT_aux. -Qed. - -Theorem relative_error_N_FLT_F2R_emin_ex' : +Theorem relative_error_N_FLT_F2R_emin_ex : forall m, let x := F2R (Float beta m emin) in exists eps, (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R. @@ -594,26 +537,11 @@ apply Rmult_le_pos. apply Rlt_le. apply (RinvN_pos 1). apply bpow_ge_0. -now apply relative_error_N_FLT_F2R_emin'. -Qed. - -(* TODO: remove *) -Theorem relative_error_N_FLT_F2R_emin_ex : - forall m, let x := F2R (Float beta m (emin + prec - 1)) in - exists eps, - (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R. -Proof with auto with typeclass_instances. -intros m x. -apply relative_error_le_conversion... -apply Rlt_le. -apply Rmult_lt_0_compat. -apply Rinv_0_lt_compat. -now apply (Z2R_lt 0 2). -apply bpow_gt_0. now apply relative_error_N_FLT_F2R_emin. Qed. -Theorem relative_error_N_FLT_round_F2R_emin' : + +Theorem relative_error_N_FLT_round_F2R_emin : forall m, let x := F2R (Float beta m emin) in (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R. Proof with auto with typeclass_instances. @@ -639,16 +567,6 @@ apply relative_error_N_round with (emin := (emin + prec - 1)%Z)... apply relative_error_FLT_aux. Qed. -(* TODO: remove *) -Theorem relative_error_N_FLT_round_F2R_emin : - forall m, let x := F2R (Float beta m (emin + prec - 1)) in - (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R. -Proof with auto with typeclass_instances. -intros m x. -apply relative_error_N_round_F2R_emin... -apply relative_error_FLT_aux. -Qed. - Lemma error_N_FLT_aux : forall x, (0 < x)%R -> @@ -682,10 +600,11 @@ auto with real. apply bpow_ge_0. split. apply Rle_trans with (/2*ulp beta (FLT_exp emin prec) x)%R. -apply ulp_half_error. +apply error_le_half_ulp. now apply FLT_exp_valid. apply Rmult_le_compat_l; auto with real. -unfold ulp. +rewrite ulp_neq_0. +2: now apply Rgt_not_eq. apply bpow_le. unfold FLT_exp, canonic_exp. rewrite Zmax_right. @@ -770,28 +689,17 @@ apply He. Qed. (** 1+#ε# property in any rounding in FLX *) -Theorem relative_error_FLX_ex' : +Theorem relative_error_FLX_ex : forall x, exists eps, (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLX_exp prec) rnd x = (x * (1 + eps))%R. Proof with auto with typeclass_instances. intros x. -apply relative_error_lt_conversion'... +apply relative_error_lt_conversion... apply bpow_gt_0. now apply relative_error_FLX. Qed. -(* TODO: remove *) -Theorem relative_error_FLX_ex : - forall x, - (x <> 0)%R -> - exists eps, - (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLX_exp prec) rnd x = (x * (1 + eps))%R. -Proof with auto with typeclass_instances. -intros x _. -apply relative_error_FLX_ex'. -Qed. - Theorem relative_error_FLX_round : forall x, (x <> 0)%R -> -- cgit