From 4e8389034032a44cd2f03e965badec92e2aaa23e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 25 Apr 2018 10:43:45 +0200 Subject: Upgrade Flocq to version 2.6.1 from upstream (#71) We were previously at 2.5.2. Quoting the NEWS from upstream: Version 2.6.1: - ensured compatibility from Coq 8.4 to 8.8 Version 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Also: in preparation for Coq 8.8, silence warning "compatibility-notation" when building Flocq, because this warning is on by default in 8.8, and Flocq triggers it a lot. --- flocq/Appli/Fappli_double_round.v | 62 ++++----- flocq/Core/Fcore_FLT.v | 29 ++-- flocq/Core/Fcore_Raux.v | 9 +- flocq/Core/Fcore_ulp.v | 218 ++++++++++++++---------------- flocq/Flocq_version.v | 2 +- flocq/Prop/Fprop_mult_error.v | 2 - flocq/Prop/Fprop_plus_error.v | 269 ++++++++++++++++++++++++++++++++++++++ 7 files changed, 420 insertions(+), 171 deletions(-) (limited to 'flocq') diff --git a/flocq/Appli/Fappli_double_round.v b/flocq/Appli/Fappli_double_round.v index 2c4937ab..82f61da3 100644 --- a/flocq/Appli/Fappli_double_round.v +++ b/flocq/Appli/Fappli_double_round.v @@ -5,6 +5,7 @@ Require Import Fcore_defs. Require Import Fcore_generic_fmt. Require Import Fcalc_ops. Require Import Fcore_ulp. +Require Fcore_FLX Fcore_FLT Fcore_FTZ. Require Import Psatz. @@ -659,7 +660,7 @@ Qed. Section Double_round_mult_FLX. -Require Import Fcore_FLX. +Import Fcore_FLX. Variable prec : Z. Variable prec' : Z. @@ -685,8 +686,8 @@ End Double_round_mult_FLX. Section Double_round_mult_FLT. -Require Import Fcore_FLX. -Require Import Fcore_FLT. +Import Fcore_FLX. +Import Fcore_FLT. Variable emin prec : Z. Variable emin' prec' : Z. @@ -718,7 +719,8 @@ End Double_round_mult_FLT. Section Double_round_mult_FTZ. -Require Import Fcore_FTZ. +Import Fcore_FLX. +Import Fcore_FTZ. Variable emin prec : Z. Variable emin' prec' : Z. @@ -796,7 +798,7 @@ Lemma ln_beta_minus_disj : \/ (ln_beta (x - y) = (ln_beta x - 1)%Z :> Z)). Proof. intros x y Px Py Hln. -assert (Hxy : y < x); [now apply (ln_beta_lt_pos beta); [| |omega]|]. +assert (Hxy : y < x); [now apply (ln_beta_lt_pos beta); [ |omega]|]. generalize (ln_beta_minus beta x y Py Hxy); intro Hln2. generalize (ln_beta_minus_lb beta x y Px Py Hln); intro Hln3. omega. @@ -1611,7 +1613,7 @@ Qed. Section Double_round_plus_FLX. -Require Import Fcore_FLX. +Import Fcore_FLX. Variable prec : Z. Variable prec' : Z. @@ -1667,8 +1669,8 @@ End Double_round_plus_FLX. Section Double_round_plus_FLT. -Require Import Fcore_FLX. -Require Import Fcore_FLT. +Import Fcore_FLX. +Import Fcore_FLT. Variable emin prec : Z. Variable emin' prec' : Z. @@ -1739,8 +1741,8 @@ End Double_round_plus_FLT. Section Double_round_plus_FTZ. -Require Import Fcore_FLX. -Require Import Fcore_FTZ. +Import Fcore_FLX. +Import Fcore_FTZ. Variable emin prec : Z. Variable emin' prec' : Z. @@ -2325,7 +2327,7 @@ Qed. Section Double_round_plus_beta_ge_3_FLX. -Require Import Fcore_FLX. +Import Fcore_FLX. Variable prec : Z. Variable prec' : Z. @@ -2385,8 +2387,8 @@ End Double_round_plus_beta_ge_3_FLX. Section Double_round_plus_beta_ge_3_FLT. -Require Import Fcore_FLX. -Require Import Fcore_FLT. +Import Fcore_FLX. +Import Fcore_FLT. Variable emin prec : Z. Variable emin' prec' : Z. @@ -2461,8 +2463,8 @@ End Double_round_plus_beta_ge_3_FLT. Section Double_round_plus_beta_ge_3_FTZ. -Require Import Fcore_FLX. -Require Import Fcore_FTZ. +Import Fcore_FLX. +Import Fcore_FTZ. Variable emin prec : Z. Variable emin' prec' : Z. @@ -2880,7 +2882,7 @@ Qed. Section Double_round_sqrt_FLX. -Require Import Fcore_FLX. +Import Fcore_FLX. Variable prec : Z. Variable prec' : Z. @@ -2917,8 +2919,8 @@ End Double_round_sqrt_FLX. Section Double_round_sqrt_FLT. -Require Import Fcore_FLX. -Require Import Fcore_FLT. +Import Fcore_FLX. +Import Fcore_FLT. Variable emin prec : Z. Variable emin' prec' : Z. @@ -2972,8 +2974,8 @@ End Double_round_sqrt_FLT. Section Double_round_sqrt_FTZ. -Require Import Fcore_FLX. -Require Import Fcore_FTZ. +Import Fcore_FLX. +Import Fcore_FTZ. Variable emin prec : Z. Variable emin' prec' : Z. @@ -3318,7 +3320,7 @@ Qed. Section Double_round_sqrt_beta_ge_4_FLX. -Require Import Fcore_FLX. +Import Fcore_FLX. Variable prec : Z. Variable prec' : Z. @@ -3357,8 +3359,8 @@ End Double_round_sqrt_beta_ge_4_FLX. Section Double_round_sqrt_beta_ge_4_FLT. -Require Import Fcore_FLX. -Require Import Fcore_FLT. +Import Fcore_FLX. +Import Fcore_FLT. Variable emin prec : Z. Variable emin' prec' : Z. @@ -3414,8 +3416,8 @@ End Double_round_sqrt_beta_ge_4_FLT. Section Double_round_sqrt_beta_ge_4_FTZ. -Require Import Fcore_FLX. -Require Import Fcore_FTZ. +Import Fcore_FLX. +Import Fcore_FTZ. Variable emin prec : Z. Variable emin' prec' : Z. @@ -4401,7 +4403,7 @@ Qed. Section Double_round_div_FLX. -Require Import Fcore_FLX. +Import Fcore_FLX. Variable prec : Z. Variable prec' : Z. @@ -4445,8 +4447,8 @@ End Double_round_div_FLX. Section Double_round_div_FLT. -Require Import Fcore_FLX. -Require Import Fcore_FLT. +Import Fcore_FLX. +Import Fcore_FLT. Variable emin prec : Z. Variable emin' prec' : Z. @@ -4515,8 +4517,8 @@ End Double_round_div_FLT. Section Double_round_div_FTZ. -Require Import Fcore_FLX. -Require Import Fcore_FTZ. +Import Fcore_FLX. +Import Fcore_FTZ. Variable emin prec : Z. Variable emin' prec' : Z. diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v index 53dc48a7..2258b1d9 100644 --- a/flocq/Core/Fcore_FLT.v +++ b/flocq/Core/Fcore_FLT.v @@ -257,32 +257,33 @@ apply Rle_lt_trans with (2:=Hx). now apply He. Qed. -Theorem ulp_FLT_le: forall x, (bpow (emin+prec) <= Rabs x)%R -> - (ulp beta FLT_exp x <= Rabs x * bpow (1-prec))%R. +Theorem ulp_FLT_le : + forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> + (ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R. Proof. intros x Hx. -assert (x <> 0)%R. -intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt. -rewrite Z, Rabs_R0; apply bpow_gt_0. -rewrite ulp_neq_0; try assumption. +assert (Zx : (x <> 0)%R). + intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt. + rewrite Z, Rabs_R0; apply bpow_gt_0. +rewrite ulp_neq_0 with (1 := Zx). unfold canonic_exp, FLT_exp. destruct (ln_beta beta x) as (e,He). apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R. rewrite <- bpow_plus. right; apply f_equal. -apply trans_eq with (e-prec)%Z;[idtac|ring]. -simpl; apply Z.max_l. -assert (emin+prec <= e)%Z; try omega. -apply le_bpow with beta. -apply Rle_trans with (1:=Hx). -left; now apply He. +replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring. +apply Z.max_l. +assert (emin+prec-1 < e)%Z; try omega. +apply lt_bpow with beta. +apply Rle_lt_trans with (1:=Hx). +now apply He. apply Rmult_le_compat_r. apply bpow_ge_0. now apply He. Qed. - -Theorem ulp_FLT_ge: forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R. +Theorem ulp_FLT_gt : + forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R. Proof. intros x; case (Req_dec x 0); intros Hx. rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0. diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v index 44db6c35..77235e63 100644 --- a/flocq/Core/Fcore_Raux.v +++ b/flocq/Core/Fcore_Raux.v @@ -1842,10 +1842,13 @@ Qed. Lemma ln_beta_lt_pos : forall x y, - (0 < x)%R -> (0 < y)%R -> + (0 < y)%R -> (ln_beta x < ln_beta y)%Z -> (x < y)%R. Proof. -intros x y Px Py. +intros x y Py. +case (Rle_or_lt x 0); intros Px. +intros H. +now apply Rle_lt_trans with 0%R. destruct (ln_beta x) as (ex, Hex). destruct (ln_beta y) as (ey, Hey). simpl. @@ -2099,7 +2102,7 @@ assert (Hbeta : (2 <= r)%Z). { destruct r as (beta_val,beta_prop). now apply Zle_bool_imp_le. } intros x y Px Py Hln. -assert (Oxy : (y < x)%R); [now apply ln_beta_lt_pos; [| |omega]|]. +assert (Oxy : (y < x)%R); [apply ln_beta_lt_pos;[assumption|omega]|]. destruct (ln_beta x) as (ex,Hex). destruct (ln_beta y) as (ey,Hey). simpl in Hln |- *. diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v index 3bc0eac3..4fdd319e 100644 --- a/flocq/Core/Fcore_ulp.v +++ b/flocq/Core/Fcore_ulp.v @@ -43,7 +43,6 @@ now left. now right. Qed. - (** [negligible_exp] is either none (as in FLX) or Some n such that n <= fexp n. *) Definition negligible_exp: option Z := match (LPO_Z _ (fun z => Z_le_dec_aux z (fexp z))) with @@ -272,6 +271,7 @@ Qed. Lemma not_FTZ_generic_format_ulp: (forall x, F (ulp x)) -> Exp_not_FTZ fexp. +Proof. intros H e. specialize (H (bpow (e-1))). rewrite ulp_neq_0 in H. @@ -1483,23 +1483,27 @@ now apply generic_format_opp. now apply Ropp_lt_contravar. Qed. - -Theorem lt_succ_le: +Theorem lt_succ_le : forall x y, - F x -> F y -> (y <> 0)%R -> + (y <> 0)%R -> (x <= y)%R -> (x < succ y)%R. Proof. -intros x y Fx Fy Zy Hxy. -case (Rle_or_lt (succ y) x); trivial; intros H. -absurd (succ y = y)%R. -apply Rgt_not_eq. +intros x y Zy Hxy. +apply Rle_lt_trans with (1 := Hxy). now apply succ_gt_id. -apply Rle_antisym. -now apply Rle_trans with x. -apply succ_ge_id. Qed. +Theorem pred_lt_le : + forall x y, + (x <> 0)%R -> + (x <= y)%R -> + (pred x < y)%R. +Proof. +intros x y Zy Hxy. +apply Rlt_le_trans with (2 := Hxy). +now apply pred_lt_id. +Qed. Theorem succ_pred_aux : forall x, F x -> (0 < x)%R -> succ (pred x)=x. Proof. @@ -1510,17 +1514,15 @@ rewrite succ_eq_pos. now apply pred_pos_plus_ulp. Qed. -Theorem pred_succ_aux_0 : (pred (succ 0)=0)%R. +Theorem pred_ulp_0 : + pred (ulp 0) = 0%R. Proof. -unfold succ; rewrite Rle_bool_true. -2: apply Rle_refl. -rewrite Rplus_0_l. rewrite pred_eq_pos. 2: apply ulp_ge_0. unfold ulp; rewrite Req_bool_true; trivial. case negligible_exp_spec'. (* *) -intros (H1,H2); rewrite H1. +intros [H1 _]; rewrite H1. unfold pred_pos; rewrite Req_bool_false. 2: apply Rlt_not_eq, bpow_gt_0. unfold ulp; rewrite Req_bool_true; trivial. @@ -1535,111 +1537,73 @@ apply Rminus_diag_eq, f_equal. apply sym_eq, valid_exp; omega. Qed. -Theorem pred_succ_aux : forall x, F x -> (0 < x)%R -> pred (succ x)=x. +Theorem succ_0 : + succ 0 = ulp 0. Proof. -intros x Fx Hx. -rewrite succ_eq_pos;[idtac|now left]. -rewrite pred_eq_pos. -2: apply Rplus_le_le_0_compat;[now left| apply ulp_ge_0]. -unfold pred_pos. -case Req_bool_spec; intros H1. -(* *) -pose (l:=(ln_beta beta (x+ulp x))). -rewrite H1 at 1; fold l. -apply Rplus_eq_reg_r with (ulp x). -rewrite H1; fold l. -rewrite (ulp_neq_0 x) at 3. -2: now apply Rgt_not_eq. -unfold canonic_exp. -replace (fexp (ln_beta beta x)) with (fexp (l-1))%Z. -ring. -apply f_equal, sym_eq. -apply Zle_antisym. -assert (ln_beta beta x - 1 < l - 1)%Z;[idtac|omega]. -apply lt_bpow with beta. -unfold l; rewrite <- H1. -apply Rle_lt_trans with x. -destruct (ln_beta beta x) as (e,He); simpl. -rewrite <- (Rabs_right x) at 1. -2: apply Rle_ge; now left. -now apply He, Rgt_not_eq. -apply Rplus_lt_reg_l with (-x)%R; ring_simplify. -rewrite ulp_neq_0. -apply bpow_gt_0. -now apply Rgt_not_eq. -apply le_bpow with beta. -unfold l; rewrite <- H1. -apply id_p_ulp_le_bpow; trivial. -rewrite <- (Rabs_right x) at 1. -2: apply Rle_ge; now left. -apply bpow_ln_beta_gt. -(* *) -replace (ulp (x+ ulp x)) with (ulp x). -ring. -rewrite ulp_neq_0 at 1. -2: now apply Rgt_not_eq. -rewrite ulp_neq_0 at 1. -2: apply Rgt_not_eq, Rlt_gt. -2: apply Rlt_le_trans with (1:=Hx). -2: apply Rplus_le_reg_l with (-x)%R; ring_simplify. -2: apply ulp_ge_0. -apply f_equal; unfold canonic_exp; apply f_equal. -apply sym_eq, ln_beta_unique. -rewrite Rabs_right. -2: apply Rle_ge; left. -2: apply Rlt_le_trans with (1:=Hx). -2: apply Rplus_le_reg_l with (-x)%R; ring_simplify. -2: apply ulp_ge_0. -destruct (ln_beta beta x) as (e,He); simpl. -rewrite Rabs_right in He. -2: apply Rle_ge; now left. -split. -apply Rle_trans with x. -apply He, Rgt_not_eq; assumption. -apply Rplus_le_reg_l with (-x)%R; ring_simplify. -apply ulp_ge_0. -case (Rle_lt_or_eq_dec (x+ulp x) (bpow e)); trivial. -apply id_p_ulp_le_bpow; trivial. -apply He, Rgt_not_eq; assumption. -intros K; contradict H1. -rewrite K, ln_beta_bpow. -apply f_equal; ring. +unfold succ. +rewrite Rle_bool_true. +apply Rplus_0_l. +apply Rle_refl. Qed. +Theorem pred_0 : + pred 0 = Ropp (ulp 0). +Proof. +rewrite <- succ_0. +rewrite <- Ropp_0 at 1. +apply pred_opp. +Qed. - -Theorem succ_pred : forall x, F x -> succ (pred x)=x. +Theorem pred_succ_aux : + forall x, F x -> (0 < x)%R -> + pred (succ x) = x. +Proof. +intros x Fx Hx. +apply Rle_antisym. +- apply Rnot_lt_le. + intros H. + apply succ_le_lt with (1 := Fx) in H. + revert H. + apply Rlt_not_le. + apply pred_lt_id. + apply Rgt_not_eq. + apply Rlt_le_trans with (1 := Hx). + apply succ_ge_id. + now apply generic_format_pred, generic_format_succ. +- apply le_pred_lt with (1 := Fx). + now apply generic_format_succ. + apply succ_gt_id. + now apply Rgt_not_eq. +Qed. + +Theorem succ_pred : + forall x, F x -> + succ (pred x) = x. Proof. intros x Fx. -case (Rle_or_lt 0 x); intros Hx. -destruct Hx as [Hx|Hx]. +destruct (Rle_or_lt 0 x) as [[Hx|Hx]|Hx]. now apply succ_pred_aux. rewrite <- Hx. -rewrite pred_eq_opp_succ_opp, succ_opp, Ropp_0. -rewrite pred_succ_aux_0; ring. +rewrite pred_0, succ_opp, pred_ulp_0. +apply Ropp_0. rewrite pred_eq_opp_succ_opp, succ_opp. rewrite pred_succ_aux. -ring. +apply Ropp_involutive. now apply generic_format_opp. now apply Ropp_0_gt_lt_contravar. Qed. -Theorem pred_succ : forall x, F x -> pred (succ x)=x. +Theorem pred_succ : + forall x, F x -> + pred (succ x) = x. Proof. intros x Fx. -case (Rle_or_lt 0 x); intros Hx. -destruct Hx as [Hx|Hx]. -now apply pred_succ_aux. -rewrite <- Hx. -apply pred_succ_aux_0. -rewrite succ_eq_opp_pred_opp, pred_opp. -rewrite succ_pred_aux. -ring. +rewrite <- (Ropp_involutive x). +rewrite succ_opp, pred_opp. +apply f_equal, succ_pred. now apply generic_format_opp. -now apply Ropp_0_gt_lt_contravar. Qed. - Theorem round_UP_pred_plus_eps : forall x, F x -> forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x) @@ -2041,26 +2005,16 @@ apply error_le_half_ulp. rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. Qed. - -Theorem pred_le: forall x y, - F x -> F y -> (x <= y)%R -> (pred x <= pred y)%R. +Theorem pred_le : + forall x y, F x -> F y -> (x <= y)%R -> + (pred x <= pred y)%R. Proof. -intros x y Fx Fy Hxy. -assert (V:( ((x = 0) /\ (y = 0)) \/ (x <>0 \/ x < y))%R). -case (Req_dec x 0); intros Zx. -case Hxy; intros Zy. -now right; right. -left; split; trivial; now rewrite <- Zy. -now right; left. -destruct V as [(V1,V2)|V]. -rewrite V1,V2; now right. -apply le_pred_lt; try assumption. -apply generic_format_pred; try assumption. -case V; intros V1. -apply Rlt_le_trans with (2:=Hxy). -now apply pred_lt_id. -apply Rle_lt_trans with (2:=V1). -now apply pred_le_id. +intros x y Fx Fy [Hxy| ->]. +2: apply Rle_refl. +apply le_pred_lt with (2 := Fy). +now apply generic_format_pred. +apply Rle_lt_trans with (2 := Hxy). +apply pred_le_id. Qed. Theorem succ_le: forall x y, @@ -2088,6 +2042,28 @@ rewrite <- (pred_succ x), <- (pred_succ y); try assumption. apply pred_le; trivial; now apply generic_format_succ. Qed. +Theorem pred_lt : + forall x y, F x -> F y -> (x < y)%R -> + (pred x < pred y)%R. +Proof. +intros x y Fx Fy Hxy. +apply Rnot_le_lt. +intros H. +apply Rgt_not_le with (1 := Hxy). +now apply pred_le_inv. +Qed. + +Theorem succ_lt : + forall x y, F x -> F y -> (x < y)%R -> + (succ x < succ y)%R. +Proof. +intros x y Fx Fy Hxy. +apply Rnot_le_lt. +intros H. +apply Rgt_not_le with (1 := Hxy). +now apply succ_le_inv. +Qed. + (* was lt_UP_le_DN *) Theorem le_round_DN_lt_UP : forall x y, F y -> diff --git a/flocq/Flocq_version.v b/flocq/Flocq_version.v index b01a08f9..72d4fe20 100644 --- a/flocq/Flocq_version.v +++ b/flocq/Flocq_version.v @@ -29,4 +29,4 @@ Definition Flocq_version := Eval vm_compute in parse t major (minor * 10 + N_of_ascii h - N_of_ascii "0"%char)%N | Empty_string => (major * 100 + minor)%N end in - parse "2.5.2"%string N0 N0. + parse "2.6.1"%string N0 N0. diff --git a/flocq/Prop/Fprop_mult_error.v b/flocq/Prop/Fprop_mult_error.v index 7c71627b..44448cd6 100644 --- a/flocq/Prop/Fprop_mult_error.v +++ b/flocq/Prop/Fprop_mult_error.v @@ -158,7 +158,6 @@ Notation bpow e := (bpow beta e). Variable emin prec : Z. Context { prec_gt_0_ : Prec_gt_0 prec }. -Variable Hpemin: (emin <= prec)%Z. Notation format := (generic_format beta (FLT_exp emin prec)). Notation cexp := (canonic_exp beta (FLT_exp emin prec)). @@ -173,7 +172,6 @@ Theorem mult_error_FLT : (x*y = 0)%R \/ (bpow (emin + 2*prec - 1) <= Rabs (x * y))%R -> format (round beta (FLT_exp emin prec) rnd (x * y) - (x * y))%R. Proof with auto with typeclass_instances. -clear Hpemin. intros x y Hx Hy Hxy. set (f := (round beta (FLT_exp emin prec) rnd (x * y))). destruct (Req_dec (f - x * y) 0) as [Hr0|Hr0]. diff --git a/flocq/Prop/Fprop_plus_error.v b/flocq/Prop/Fprop_plus_error.v index 41c2f031..9bb5aee8 100644 --- a/flocq/Prop/Fprop_plus_error.v +++ b/flocq/Prop/Fprop_plus_error.v @@ -19,6 +19,7 @@ COPYING file for more details. (** * Error of the rounded-to-nearest addition is representable. *) +Require Import Psatz. Require Import Fcore_Raux. Require Import Fcore_defs. Require Import Fcore_float_prop. @@ -26,6 +27,7 @@ Require Import Fcore_generic_fmt. Require Import Fcore_FIX. Require Import Fcore_FLX. Require Import Fcore_FLT. +Require Import Fcore_ulp. Require Import Fcalc_ops. @@ -267,3 +269,270 @@ rewrite Z2R_plus; ring. Qed. End Fprop_plus_FLT. + +Section Fprop_plus_mult_ulp. + +Variable beta : radix. +Notation bpow e := (bpow beta e). + +Variable fexp : Z -> Z. +Context { valid_exp : Valid_exp fexp }. +Context { monotone_exp : Monotone_exp fexp }. +Variable rnd : R -> Z. +Context { valid_rnd : Valid_rnd rnd }. + +Notation format := (generic_format beta fexp). +Notation cexp := (canonic_exp beta fexp). + +Lemma ex_shift : + forall x e, format x -> (e <= cexp x)%Z -> + exists m, (x = Z2R m * bpow e)%R. +Proof with auto with typeclass_instances. +intros x e Fx He. +exists (Ztrunc (scaled_mantissa beta fexp x)*Zpower beta (cexp x -e))%Z. +rewrite Fx at 1; unfold F2R; simpl. +rewrite Z2R_mult, Rmult_assoc. +f_equal. +rewrite Z2R_Zpower. +2: omega. +rewrite <- bpow_plus; f_equal; ring. +Qed. + +Lemma ln_beta_minus1 : + forall z, z <> 0%R -> + (ln_beta beta z - 1)%Z = ln_beta beta (z / Z2R beta). +Proof. +intros z Hz. +unfold Zminus. +rewrite <- ln_beta_mult_bpow with (1 := Hz). +now rewrite bpow_opp, bpow_1. +Qed. + +Theorem round_plus_mult_ulp : + forall x y, format x -> format y -> (x <> 0)%R -> + exists m, (round beta fexp rnd (x+y) = Z2R m * ulp beta fexp (x/Z2R beta))%R. +Proof with auto with typeclass_instances. +intros x y Fx Fy Zx. +case (Zle_or_lt (ln_beta beta (x/Z2R beta)) (ln_beta beta y)); intros H1. +pose (e:=cexp (x / Z2R beta)). +destruct (ex_shift x e) as (nx, Hnx); try exact Fx. +apply monotone_exp. +rewrite <- (ln_beta_minus1 x Zx); omega. +destruct (ex_shift y e) as (ny, Hny); try assumption. +apply monotone_exp... +destruct (round_repr_same_exp beta fexp rnd (nx+ny) e) as (n,Hn). +exists n. +apply trans_eq with (F2R (Float beta n e)). +rewrite <- Hn; f_equal. +rewrite Hnx, Hny; unfold F2R; simpl; rewrite Z2R_plus; ring. +unfold F2R; simpl. +rewrite ulp_neq_0; try easy. +apply Rmult_integral_contrapositive_currified; try assumption. +apply Rinv_neq_0_compat. +apply Rgt_not_eq. +apply radix_pos. +(* *) +destruct (ex_shift (round beta fexp rnd (x + y)) (cexp (x/Z2R beta))) as (n,Hn). +apply generic_format_round... +apply Zle_trans with (cexp (x+y)). +apply monotone_exp. +rewrite <- ln_beta_minus1 by easy. +rewrite <- (ln_beta_abs beta (x+y)). +(* . *) +assert (U: (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y) = Rabs x - Rabs y)%R). +assert (V: forall x y, (Rabs y <= Rabs x)%R -> + (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y) = Rabs x - Rabs y)%R). +clear; intros x y. +case (Rle_or_lt 0 y); intros Hy. +case Hy; intros Hy'. +case (Rle_or_lt 0 x); intros Hx. +intros _; rewrite (Rabs_pos_eq y) by easy. +rewrite (Rabs_pos_eq x) by easy. +left; apply Rabs_pos_eq. +now apply Rplus_le_le_0_compat. +rewrite (Rabs_pos_eq y) by easy. +rewrite (Rabs_left x) by easy. +intros H; right; split. +now apply Rgt_not_eq. +rewrite Rabs_left1. +ring. +apply Rplus_le_reg_l with (-x)%R; ring_simplify; assumption. +intros _; left. +now rewrite <- Hy', Rabs_R0, 2!Rplus_0_r. +case (Rle_or_lt 0 x); intros Hx. +rewrite (Rabs_left y) by easy. +rewrite (Rabs_pos_eq x) by easy. +intros H; right; split. +now apply Rlt_not_eq. +rewrite Rabs_pos_eq. +ring. +apply Rplus_le_reg_l with (-y)%R; ring_simplify; assumption. +intros _; left. +rewrite (Rabs_left y) by easy. +rewrite (Rabs_left x) by easy. +rewrite Rabs_left1. +ring. +lra. +apply V; left. +apply ln_beta_lt_pos with beta. +now apply Rabs_pos_lt. +rewrite <- ln_beta_minus1 in H1; try assumption. +rewrite 2!ln_beta_abs; omega. +(* . *) +destruct U as [U|U]. +rewrite U; apply Zle_trans with (ln_beta beta x). +omega. +rewrite <- ln_beta_abs. +apply ln_beta_le. +now apply Rabs_pos_lt. +apply Rplus_le_reg_l with (-Rabs x)%R; ring_simplify. +apply Rabs_pos. +destruct U as (U',U); rewrite U. +rewrite <- ln_beta_abs. +apply ln_beta_minus_lb. +now apply Rabs_pos_lt. +now apply Rabs_pos_lt. +rewrite 2!ln_beta_abs. +assert (ln_beta beta y < ln_beta beta x - 1)%Z. +now rewrite (ln_beta_minus1 x Zx). +omega. +apply canonic_exp_round_ge... +intros K. +apply round_plus_eq_zero in K... +contradict H1; apply Zle_not_lt. +rewrite <- (ln_beta_minus1 x Zx). +replace y with (-x)%R. +rewrite ln_beta_opp; omega. +lra. +exists n. +rewrite ulp_neq_0. +assumption. +apply Rmult_integral_contrapositive_currified; try assumption. +apply Rinv_neq_0_compat. +apply Rgt_not_eq. +apply radix_pos. +Qed. + +Context {exp_not_FTZ : Exp_not_FTZ fexp}. + +Theorem round_plus_ge_ulp : + forall x y, format x -> format y -> + round beta fexp rnd (x+y) = 0%R \/ + (ulp beta fexp (x/Z2R beta) <= Rabs (round beta fexp rnd (x+y)))%R. +Proof with auto with typeclass_instances. +intros x y Fx Fy. +case (Req_dec x 0); intros Zx. +(* *) +rewrite Zx, Rplus_0_l. +rewrite round_generic... +unfold Rdiv; rewrite Rmult_0_l. +rewrite Fy at 2. +unfold F2R; simpl; rewrite Rabs_mult. +rewrite (Rabs_pos_eq (bpow _)) by apply bpow_ge_0. +case (Z.eq_dec (Ztrunc (scaled_mantissa beta fexp y)) 0); intros Hm. +left. +rewrite Fy, Hm; unfold F2R; simpl; ring. +right. +apply Rle_trans with (1*bpow (cexp y))%R. +rewrite Rmult_1_l. +rewrite <- ulp_neq_0. +apply ulp_ge_ulp_0... +intros K; apply Hm. +rewrite K, scaled_mantissa_0. +apply (Ztrunc_Z2R 0). +apply Rmult_le_compat_r. +apply bpow_ge_0. +rewrite <- Z2R_abs. +apply (Z2R_le 1). +apply (Zlt_le_succ 0). +now apply Z.abs_pos. +(* *) +destruct (round_plus_mult_ulp x y Fx Fy Zx) as (m,Hm). +case (Z.eq_dec m 0); intros Zm. +left. +rewrite Hm, Zm; simpl; ring. +right. +rewrite Hm, Rabs_mult. +rewrite (Rabs_pos_eq (ulp _ _ _)) by apply ulp_ge_0. +apply Rle_trans with (1*ulp beta fexp (x/Z2R beta))%R. +right; ring. +apply Rmult_le_compat_r. +apply ulp_ge_0. +rewrite <- Z2R_abs. +apply (Z2R_le 1). +apply (Zlt_le_succ 0). +now apply Z.abs_pos. +Qed. + +End Fprop_plus_mult_ulp. + +Section Fprop_plus_ge_ulp. + +Variable beta : radix. +Notation bpow e := (bpow beta e). + +Variable rnd : R -> Z. +Context { valid_rnd : Valid_rnd rnd }. +Variable emin prec : Z. +Context { prec_gt_0_ : Prec_gt_0 prec }. + +Theorem round_plus_ge_ulp_FLT : forall x y e, + generic_format beta (FLT_exp emin prec) x -> generic_format beta (FLT_exp emin prec) y -> + (bpow e <= Rabs x)%R -> + round beta (FLT_exp emin prec) rnd (x+y) = 0%R \/ + (bpow (e - prec) <= Rabs (round beta (FLT_exp emin prec) rnd (x+y)))%R. +Proof with auto with typeclass_instances. +intros x y e Fx Fy He. +assert (Zx: x <> 0%R). + contradict He. + apply Rlt_not_le; rewrite He, Rabs_R0. + apply bpow_gt_0. +case round_plus_ge_ulp with beta (FLT_exp emin prec) rnd x y... +intros H; right. +apply Rle_trans with (2:=H). +rewrite ulp_neq_0. +unfold canonic_exp. +rewrite <- ln_beta_minus1 by easy. +unfold FLT_exp; apply bpow_le. +apply Zle_trans with (2:=Z.le_max_l _ _). +destruct (ln_beta beta x) as (n,Hn); simpl. +assert (e < n)%Z; try omega. +apply lt_bpow with beta. +apply Rle_lt_trans with (1:=He). +now apply Hn. +apply Rmult_integral_contrapositive_currified; try assumption. +apply Rinv_neq_0_compat. +apply Rgt_not_eq. +apply radix_pos. +Qed. + +Theorem round_plus_ge_ulp_FLX : forall x y e, + generic_format beta (FLX_exp prec) x -> generic_format beta (FLX_exp prec) y -> + (bpow e <= Rabs x)%R -> + round beta (FLX_exp prec) rnd (x+y) = 0%R \/ + (bpow (e - prec) <= Rabs (round beta (FLX_exp prec) rnd (x+y)))%R. +Proof with auto with typeclass_instances. +intros x y e Fx Fy He. +assert (Zx: x <> 0%R). + contradict He. + apply Rlt_not_le; rewrite He, Rabs_R0. + apply bpow_gt_0. +case round_plus_ge_ulp with beta (FLX_exp prec) rnd x y... +intros H; right. +apply Rle_trans with (2:=H). +rewrite ulp_neq_0. +unfold canonic_exp. +rewrite <- ln_beta_minus1 by easy. +unfold FLX_exp; apply bpow_le. +destruct (ln_beta beta x) as (n,Hn); simpl. +assert (e < n)%Z; try omega. +apply lt_bpow with beta. +apply Rle_lt_trans with (1:=He). +now apply Hn. +apply Rmult_integral_contrapositive_currified; try assumption. +apply Rinv_neq_0_compat. +apply Rgt_not_eq. +apply radix_pos. +Qed. + +End Fprop_plus_ge_ulp. -- cgit