Commit daa79c73 by Guillaume Melquiond

### Simplify proofs a bit.

parent 6a292044
 ... @@ -1482,7 +1482,6 @@ now apply generic_format_opp. ... @@ -1482,7 +1482,6 @@ now apply generic_format_opp. now apply Ropp_lt_contravar. now apply Ropp_lt_contravar. Qed. Qed. Theorem lt_succ_le : Theorem lt_succ_le : forall x y, forall x y, F x -> F y -> (y <> 0)%R -> F x -> F y -> (y <> 0)%R -> ... @@ -1494,7 +1493,7 @@ apply Rle_lt_trans with (1 := Hxy). ... @@ -1494,7 +1493,7 @@ apply Rle_lt_trans with (1 := Hxy). now apply succ_gt_id. now apply succ_gt_id. Qed. Qed. Theorem pred_lt_le: Theorem pred_lt_le : forall x y, forall x y, F x -> F y -> (x <> 0)%R -> F x -> F y -> (x <> 0)%R -> (x <= y)%R -> (x <= y)%R -> ... @@ -1514,17 +1513,15 @@ rewrite succ_eq_pos. ... @@ -1514,17 +1513,15 @@ rewrite succ_eq_pos. now apply pred_pos_plus_ulp. now apply pred_pos_plus_ulp. Qed. Qed. Theorem pred_succ_aux_0 : (pred (succ 0)=0)%R. Theorem pred_ulp_0 : pred (ulp 0) = R0. Proof. Proof. unfold succ; rewrite Rle_bool_true. 2: apply Rle_refl. rewrite Rplus_0_l. rewrite pred_eq_pos. rewrite pred_eq_pos. 2: apply ulp_ge_0. 2: apply ulp_ge_0. unfold ulp; rewrite Req_bool_true; trivial. unfold ulp; rewrite Req_bool_true; trivial. case negligible_exp_spec'. case negligible_exp_spec'. (* *) (* *) intros (H1,H2); rewrite H1. intros [H1 _]; rewrite H1. unfold pred_pos; rewrite Req_bool_false. unfold pred_pos; rewrite Req_bool_false. 2: apply Rlt_not_eq, bpow_gt_0. 2: apply Rlt_not_eq, bpow_gt_0. unfold ulp; rewrite Req_bool_true; trivial. unfold ulp; rewrite Req_bool_true; trivial. ... @@ -1539,111 +1536,73 @@ apply Rminus_diag_eq, f_equal. ... @@ -1539,111 +1536,73 @@ apply Rminus_diag_eq, f_equal. apply sym_eq, valid_exp; omega. apply sym_eq, valid_exp; omega. Qed. Qed. Theorem pred_succ_aux : forall x, F x -> (0 < x)%R -> pred (succ x)=x. Theorem succ_0 : succ 0 = ulp 0. Proof. Proof. intros x Fx Hx. unfold succ. rewrite succ_eq_pos;[idtac|now left]. rewrite Rle_bool_true. rewrite pred_eq_pos. apply Rplus_0_l. 2: apply Rplus_le_le_0_compat;[now left| apply ulp_ge_0]. apply Rle_refl. 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. Qed. Qed. Theorem pred_0 : pred 0 = Ropp (ulp 0). Proof. rewrite <- succ_0. rewrite <- Ropp_0 at 1. apply pred_opp. Qed. Theorem pred_succ_aux : Theorem succ_pred : forall x, F x -> succ (pred x)=x. 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. Proof. intros x Fx. intros x Fx. case (Rle_or_lt 0 x); intros Hx. destruct (Rle_or_lt 0 x) as [[Hx|Hx]|Hx]. destruct Hx as [Hx|Hx]. now apply succ_pred_aux. now apply succ_pred_aux. rewrite <- Hx. rewrite <- Hx. rewrite pred_eq_opp_succ_opp, succ_opp, Ropp_0. rewrite pred_0, succ_opp, pred_ulp_0. rewrite pred_succ_aux_0; ring. apply Ropp_0. rewrite pred_eq_opp_succ_opp, succ_opp. rewrite pred_eq_opp_succ_opp, succ_opp. rewrite pred_succ_aux. rewrite pred_succ_aux. ring. apply Ropp_involutive. now apply generic_format_opp. now apply generic_format_opp. now apply Ropp_0_gt_lt_contravar. now apply Ropp_0_gt_lt_contravar. Qed. Qed. Theorem pred_succ : forall x, F x -> pred (succ x)=x. Theorem pred_succ : forall x, F x -> pred (succ x) = x. Proof. Proof. intros x Fx. intros x Fx. case (Rle_or_lt 0 x); intros Hx. rewrite <- (Ropp_involutive x). destruct Hx as [Hx|Hx]. rewrite succ_opp, pred_opp. now apply pred_succ_aux. apply f_equal, succ_pred. rewrite <- Hx. apply pred_succ_aux_0. rewrite succ_eq_opp_pred_opp, pred_opp. rewrite succ_pred_aux. ring. now apply generic_format_opp. now apply generic_format_opp. now apply Ropp_0_gt_lt_contravar. Qed. Qed. Theorem round_UP_pred_plus_eps : Theorem round_UP_pred_plus_eps : forall x, F x -> forall x, F x -> forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x) forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x) ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!