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/Core/Fcore_FLT.v | 29 +++---- flocq/Core/Fcore_Raux.v | 9 +- flocq/Core/Fcore_ulp.v | 218 +++++++++++++++++++++--------------------------- 3 files changed, 118 insertions(+), 138 deletions(-) (limited to 'flocq/Core') 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 -> -- cgit