From daa79c7320d7f72e9ad56e3d0557d6009db61a09 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 30 Sep 2016 14:42:26 +0200 Subject: [PATCH] Simplify proofs a bit. --- src/Core/Fcore_ulp.v | 145 ++++++++++++++++--------------------------- 1 file changed, 52 insertions(+), 93 deletions(-) diff --git a/src/Core/Fcore_ulp.v b/src/Core/Fcore_ulp.v index 1bb5f52..d585061 100644 --- a/src/Core/Fcore_ulp.v +++ b/src/Core/Fcore_ulp.v @@ -1482,7 +1482,6 @@ now apply generic_format_opp. now apply Ropp_lt_contravar. Qed. - Theorem lt_succ_le : forall x y, F x -> F y -> (y <> 0)%R -> @@ -1494,7 +1493,7 @@ apply Rle_lt_trans with (1 := Hxy). now apply succ_gt_id. Qed. -Theorem pred_lt_le: +Theorem pred_lt_le : forall x y, F x -> F y -> (x <> 0)%R -> (x <= y)%R -> @@ -1514,17 +1513,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) = R0. 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. @@ -1539,111 +1536,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) -- 2.24.1