From 0f919eb26c68d3882e612a1b3a9df45bee6d3624 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 13 Feb 2019 18:53:17 +0100 Subject: Upgrade embedded version of Flocq to 3.1. Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully). --- flocq/Appli/Fappli_double_round.v | 4591 ------------------------------------- 1 file changed, 4591 deletions(-) delete mode 100644 flocq/Appli/Fappli_double_round.v (limited to 'flocq/Appli/Fappli_double_round.v') diff --git a/flocq/Appli/Fappli_double_round.v b/flocq/Appli/Fappli_double_round.v deleted file mode 100644 index 82f61da3..00000000 --- a/flocq/Appli/Fappli_double_round.v +++ /dev/null @@ -1,4591 +0,0 @@ -(** * Conditions for innocuous double rounding. *) - -Require Import Fcore_Raux. -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. - -Open Scope R_scope. - -Section Double_round. - -Variable beta : radix. -Notation bpow e := (bpow beta e). -Notation ln_beta x := (ln_beta beta x). - -Definition double_round_eq fexp1 fexp2 choice1 choice2 x := - round beta fexp1 (Znearest choice1) (round beta fexp2 (Znearest choice2) x) - = round beta fexp1 (Znearest choice1) x. - -(** A little tactic to simplify terms of the form [bpow a * bpow b]. *) -Ltac bpow_simplify := - (* bpow ex * bpow ey ~~> bpow (ex + ey) *) - repeat - match goal with - | |- context [(Fcore_Raux.bpow _ _ * Fcore_Raux.bpow _ _)] => - rewrite <- bpow_plus - | |- context [(?X1 * Fcore_Raux.bpow _ _ * Fcore_Raux.bpow _ _)] => - rewrite (Rmult_assoc X1); rewrite <- bpow_plus - | |- context [(?X1 * (?X2 * Fcore_Raux.bpow _ _) * Fcore_Raux.bpow _ _)] => - rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 * X2)); - rewrite <- bpow_plus - end; - (* ring_simplify arguments of bpow *) - repeat - match goal with - | |- context [(Fcore_Raux.bpow _ ?X)] => - progress ring_simplify X - end; - (* bpow 0 ~~> 1 *) - change (Fcore_Raux.bpow _ 0) with 1; - repeat - match goal with - | |- context [(_ * 1)] => - rewrite Rmult_1_r - end. - -Definition midp (fexp : Z -> Z) (x : R) := - round beta fexp Zfloor x + / 2 * ulp beta fexp x. - -Definition midp' (fexp : Z -> Z) (x : R) := - round beta fexp Zceil x - / 2 * ulp beta fexp x. - -Lemma double_round_lt_mid_further_place' : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z -> - x < bpow (ln_beta x) - / 2 * ulp beta fexp2 x -> - x < midp fexp1 x - / 2 * ulp beta fexp2 x -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx1. -unfold double_round_eq. -set (x' := round beta fexp1 Zfloor x). -intro Hx2'. -assert (Hx2 : x - round beta fexp1 Zfloor x - < / 2 * (ulp beta fexp1 x - ulp beta fexp2 x)). -{ now apply (Rplus_lt_reg_r (round beta fexp1 Zfloor x)); ring_simplify. } -set (x'' := round beta fexp2 (Znearest choice2) x). -assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (ln_beta x))). -apply Rle_trans with (/ 2 * ulp beta fexp2 x). -now unfold x''; apply error_le_half_ulp... -rewrite ulp_neq_0;[now right|now apply Rgt_not_eq]. -assert (Pxx' : 0 <= x - x'). -{ apply Rle_0_minus. - apply round_DN_pt. - exact Vfexp1. } -rewrite 2!ulp_neq_0 in Hx2; try (apply Rgt_not_eq; assumption). -assert (Hr2 : Rabs (x'' - x') < / 2 * bpow (fexp1 (ln_beta x))). -{ replace (x'' - x') with (x'' - x + (x - x')) by ring. - apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)). - replace (/ 2 * _) with (/ 2 * bpow (fexp2 (ln_beta x)) - + (/ 2 * (bpow (fexp1 (ln_beta x)) - - bpow (fexp2 (ln_beta x))))) by ring. - apply Rplus_le_lt_compat. - - exact Hr1. - - now rewrite Rabs_right; [|now apply Rle_ge]; apply Hx2. } -destruct (Req_dec x'' 0) as [Zx''|Nzx'']. -- (* x'' = 0 *) - rewrite Zx'' in Hr1 |- *. - rewrite round_0; [|now apply valid_rnd_N]. - unfold round, F2R, scaled_mantissa, canonic_exp; simpl. - rewrite (Znearest_imp _ _ 0); [now simpl; rewrite Rmult_0_l|]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; - [|now apply Rle_ge; apply bpow_ge_0]. - rewrite <- Rabs_mult; rewrite Rmult_minus_distr_r. - rewrite Rmult_0_l. - bpow_simplify. - rewrite Rabs_minus_sym. - apply (Rle_lt_trans _ _ _ Hr1). - apply Rmult_lt_compat_l; [lra|]. - apply bpow_lt. - omega. -- (* x'' <> 0 *) - assert (Lx'' : ln_beta x'' = ln_beta x :> Z). - { apply Zle_antisym. - - apply ln_beta_le_bpow; [exact Nzx''|]. - replace x'' with (x'' - x + x) by ring. - apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)). - replace (bpow _) with (/ 2 * bpow (fexp2 (ln_beta x)) - + (bpow (ln_beta x) - - / 2 * bpow (fexp2 (ln_beta x)))) by ring. - apply Rplus_le_lt_compat; [exact Hr1|]. - rewrite ulp_neq_0 in Hx1;[idtac| now apply Rgt_not_eq]. - now rewrite Rabs_right; [|apply Rle_ge; apply Rlt_le]. - - unfold x'' in Nzx'' |- *. - now apply ln_beta_round_ge; [|apply valid_rnd_N|]. } - unfold round, F2R, scaled_mantissa, canonic_exp; simpl. - rewrite Lx''. - rewrite (Znearest_imp _ _ (Zfloor (scaled_mantissa beta fexp1 x))). - + rewrite (Znearest_imp _ _ (Zfloor (scaled_mantissa beta fexp1 x))); - [reflexivity|]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; - [|now apply Rle_ge; apply bpow_ge_0]. - rewrite <- Rabs_mult. - rewrite Rmult_minus_distr_r. - fold x'. - bpow_simplify. - rewrite Rabs_right; [|now apply Rle_ge]. - apply (Rlt_le_trans _ _ _ Hx2). - apply Rmult_le_compat_l; [lra|]. - generalize (bpow_ge_0 beta (fexp2 (ln_beta x))). - unfold ulp, canonic_exp; lra. - + apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; - [|now apply Rle_ge; apply bpow_ge_0]. - rewrite <- Rabs_mult. - rewrite Rmult_minus_distr_r. - fold x'. - now bpow_simplify. -Qed. - -Lemma double_round_lt_mid_further_place : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z -> - (fexp1 (ln_beta x) <= ln_beta x)%Z -> - x < midp fexp1 x - / 2 * ulp beta fexp2 x -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1. -intro Hx2'. -assert (Hx2 : x - round beta fexp1 Zfloor x - < / 2 * (ulp beta fexp1 x - ulp beta fexp2 x)). -{ now apply (Rplus_lt_reg_r (round beta fexp1 Zfloor x)); ring_simplify. } -revert Hx2. -unfold double_round_eq. -set (x' := round beta fexp1 Zfloor x). -intro Hx2. -assert (Pxx' : 0 <= x - x'). -{ apply Rle_0_minus. - apply round_DN_pt. - exact Vfexp1. } -assert (x < bpow (ln_beta x) - / 2 * bpow (fexp2 (ln_beta x))); - [|apply double_round_lt_mid_further_place'; try assumption]... -2: rewrite ulp_neq_0;[assumption|now apply Rgt_not_eq]. -destruct (Req_dec x' 0) as [Zx'|Nzx']. -- (* x' = 0 *) - rewrite Zx' in Hx2; rewrite Rminus_0_r in Hx2. - apply (Rlt_le_trans _ _ _ Hx2). - rewrite Rmult_minus_distr_l. - rewrite 2!ulp_neq_0;[idtac|now apply Rgt_not_eq|now apply Rgt_not_eq]. - apply Rplus_le_compat_r. - apply (Rmult_le_reg_r (bpow (- ln_beta x))); [now apply bpow_gt_0|]. - unfold ulp, canonic_exp; bpow_simplify. - apply Rmult_le_reg_l with (1 := Rlt_0_2). - replace (2 * (/ 2 * _)) with (bpow (fexp1 (ln_beta x) - ln_beta x)) by field. - apply Rle_trans with 1; [|lra]. - change 1 with (bpow 0); apply bpow_le. - omega. -- (* x' <> 0 *) - assert (Px' : 0 < x'). - { assert (0 <= x'); [|lra]. - unfold x'. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - rewrite Rmult_0_l. - unfold round, F2R, canonic_exp; simpl; bpow_simplify. - change 0 with (Z2R 0); apply Z2R_le. - apply Zfloor_lub. - rewrite <- (Rabs_right x); [|now apply Rle_ge; apply Rlt_le]. - rewrite scaled_mantissa_abs. - apply Rabs_pos. } - assert (Hx' : x' <= bpow (ln_beta x) - ulp beta fexp1 x). - { apply (Rplus_le_reg_r (ulp beta fexp1 x)); ring_simplify. - rewrite <- ulp_DN. - - change (round _ _ _ _) with x'. - apply id_p_ulp_le_bpow. - + exact Px'. - + change x' with (round beta fexp1 Zfloor x). - now apply generic_format_round; [|apply valid_rnd_DN]. - + apply Rle_lt_trans with x. - * now apply round_DN_pt. - * rewrite <- (Rabs_right x) at 1; [|now apply Rle_ge; apply Rlt_le]. - apply bpow_ln_beta_gt. - - exact Vfexp1. - - exact Px'. } - fold (canonic_exp beta fexp2 x); fold (ulp beta fexp2 x). - assert (/ 2 * ulp beta fexp1 x <= ulp beta fexp1 x). - rewrite <- (Rmult_1_l (ulp _ _ _)) at 2. - apply Rmult_le_compat_r; [|lra]. - apply ulp_ge_0. - rewrite 2!ulp_neq_0 in Hx2;[|now apply Rgt_not_eq|now apply Rgt_not_eq]. - rewrite ulp_neq_0 in Hx';[|now apply Rgt_not_eq]. - rewrite ulp_neq_0 in H;[|now apply Rgt_not_eq]. - lra. -Qed. - -Lemma double_round_lt_mid_same_place : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp2 (ln_beta x) = fexp1 (ln_beta x))%Z -> - x < midp fexp1 x -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 choice1 choice2 x Px Hf2f1. -intro Hx'. -assert (Hx : x - round beta fexp1 Zfloor x < / 2 * ulp beta fexp1 x). -{ now apply (Rplus_lt_reg_r (round beta fexp1 Zfloor x)); ring_simplify. } -revert Hx. -unfold double_round_eq. -set (x' := round beta fexp1 Zfloor x). -intro Hx. -assert (Pxx' : 0 <= x - x'). -{ apply Rle_0_minus. - apply round_DN_pt. - exact Vfexp1. } -assert (H : Rabs (x * bpow (- fexp1 (ln_beta x)) - - Z2R (Zfloor (x * bpow (- fexp1 (ln_beta x))))) < / 2). -{ apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - unfold scaled_mantissa, canonic_exp in Hx. - rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; - [|now apply Rle_ge; apply bpow_ge_0]. - rewrite <- Rabs_mult. - rewrite Rmult_minus_distr_r. - bpow_simplify. - apply Rabs_lt. - change (Z2R _ * _) with x'. - split. - - apply Rlt_le_trans with 0; [|exact Pxx']. - rewrite <- Ropp_0. - apply Ropp_lt_contravar. - rewrite <- (Rmult_0_r (/ 2)). - apply Rmult_lt_compat_l; [lra|]. - apply bpow_gt_0. - - rewrite ulp_neq_0 in Hx;try apply Rgt_not_eq; assumption. } -unfold round at 2. -unfold F2R, scaled_mantissa, canonic_exp; simpl. -rewrite Hf2f1. -rewrite (Znearest_imp _ _ (Zfloor (scaled_mantissa beta fexp1 x))). -- rewrite round_generic. - + unfold round, F2R, scaled_mantissa, canonic_exp; simpl. - now rewrite (Znearest_imp _ _ (Zfloor (x * bpow (- fexp1 (ln_beta x))))). - + now apply valid_rnd_N. - + fold (canonic_exp beta fexp1 x). - change (Z2R _ * bpow _) with (round beta fexp1 Zfloor x). - apply generic_format_round. - exact Vfexp1. - now apply valid_rnd_DN. -- now unfold scaled_mantissa, canonic_exp. -Qed. - -Lemma double_round_lt_mid : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z -> - (fexp1 (ln_beta x) <= ln_beta x)%Z -> - x < midp fexp1 x -> - ((fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z -> - x < midp fexp1 x - / 2 * ulp beta fexp2 x) -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx Hx'. -destruct (Zle_or_lt (fexp1 (ln_beta x)) (fexp2 (ln_beta x))) as [Hf2'|Hf2']. -- (* fexp1 (ln_beta x) <= fexp2 (ln_beta x) *) - assert (Hf2'' : (fexp2 (ln_beta x) = fexp1 (ln_beta x) :> Z)%Z); [omega|]. - now apply double_round_lt_mid_same_place. -- (* fexp2 (ln_beta x) < fexp1 (ln_beta x) *) - assert (Hf2'' : (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z); [omega|]. - generalize (Hx' Hf2''); intro Hx''. - now apply double_round_lt_mid_further_place. -Qed. - -Lemma double_round_gt_mid_further_place' : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z -> - round beta fexp2 (Znearest choice2) x < bpow (ln_beta x) -> - midp' fexp1 x + / 2 * ulp beta fexp2 x < x -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1. -intros Hx1 Hx2'. -assert (Hx2 : round beta fexp1 Zceil x - x - < / 2 * (ulp beta fexp1 x - ulp beta fexp2 x)). -{ apply (Rplus_lt_reg_r (- / 2 * ulp beta fexp1 x + x - + / 2 * ulp beta fexp2 x)); ring_simplify. - now unfold midp' in Hx2'. } -revert Hx1 Hx2. -unfold double_round_eq. -set (x' := round beta fexp1 Zceil x). -set (x'' := round beta fexp2 (Znearest choice2) x). -intros Hx1 Hx2. -assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (ln_beta x))). - apply Rle_trans with (/2* ulp beta fexp2 x). - now unfold x''; apply error_le_half_ulp... - rewrite ulp_neq_0;[now right|now apply Rgt_not_eq]. -assert (Px'x : 0 <= x' - x). -{ apply Rle_0_minus. - apply round_UP_pt. - exact Vfexp1. } -assert (Hr2 : Rabs (x'' - x') < / 2 * bpow (fexp1 (ln_beta x))). -{ replace (x'' - x') with (x'' - x + (x - x')) by ring. - apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)). - replace (/ 2 * _) with (/ 2 * bpow (fexp2 (ln_beta x)) - + (/ 2 * (bpow (fexp1 (ln_beta x)) - - bpow (fexp2 (ln_beta x))))) by ring. - apply Rplus_le_lt_compat. - - exact Hr1. - - rewrite Rabs_minus_sym. - rewrite 2!ulp_neq_0 in Hx2; try (apply Rgt_not_eq; assumption). - now rewrite Rabs_right; [|now apply Rle_ge]; apply Hx2. } -destruct (Req_dec x'' 0) as [Zx''|Nzx'']. -- (* x'' = 0 *) - rewrite Zx'' in Hr1 |- *. - rewrite round_0; [|now apply valid_rnd_N]. - unfold round, F2R, scaled_mantissa, canonic_exp; simpl. - rewrite (Znearest_imp _ _ 0); [now simpl; rewrite Rmult_0_l|]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; - [|now apply Rle_ge; apply bpow_ge_0]. - rewrite <- Rabs_mult; rewrite Rmult_minus_distr_r. - rewrite Rmult_0_l. - bpow_simplify. - rewrite Rabs_minus_sym. - apply (Rle_lt_trans _ _ _ Hr1). - apply Rmult_lt_compat_l; [lra|]. - apply bpow_lt. - omega. -- (* x'' <> 0 *) - assert (Lx'' : ln_beta x'' = ln_beta x :> Z). - { apply Zle_antisym. - - apply ln_beta_le_bpow; [exact Nzx''|]. - rewrite Rabs_right; [exact Hx1|apply Rle_ge]. - apply round_ge_generic. - + exact Vfexp2. - + now apply valid_rnd_N. - + apply generic_format_0. - + now apply Rlt_le. - - unfold x'' in Nzx'' |- *. - now apply ln_beta_round_ge; [|apply valid_rnd_N|]. } - unfold round, F2R, scaled_mantissa, canonic_exp; simpl. - rewrite Lx''. - rewrite (Znearest_imp _ _ (Zceil (scaled_mantissa beta fexp1 x))). - + rewrite (Znearest_imp _ _ (Zceil (scaled_mantissa beta fexp1 x))); - [reflexivity|]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; - [|now apply Rle_ge; apply bpow_ge_0]. - rewrite <- Rabs_mult. - rewrite Rmult_minus_distr_r. - fold x'. - bpow_simplify. - rewrite Rabs_minus_sym. - rewrite Rabs_right; [|now apply Rle_ge]. - apply (Rlt_le_trans _ _ _ Hx2). - apply Rmult_le_compat_l; [lra|]. - generalize (bpow_ge_0 beta (fexp2 (ln_beta x))). - rewrite 2!ulp_neq_0; try (apply Rgt_not_eq; assumption). - unfold canonic_exp; lra. - + apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; - [|now apply Rle_ge; apply bpow_ge_0]. - rewrite <- Rabs_mult. - rewrite Rmult_minus_distr_r. - fold x'. - now bpow_simplify. -Qed. - -Lemma double_round_gt_mid_further_place : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z -> - (fexp1 (ln_beta x) <= ln_beta x)%Z -> - midp' fexp1 x + / 2 * ulp beta fexp2 x < x -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx2'. -assert (Hx2 : round beta fexp1 Zceil x - x - < / 2 * (ulp beta fexp1 x - ulp beta fexp2 x)). -{ apply (Rplus_lt_reg_r (- / 2 * ulp beta fexp1 x + x - + / 2 * ulp beta fexp2 x)); ring_simplify. - now unfold midp' in Hx2'. } -revert Hx2. -unfold double_round_eq. -set (x' := round beta fexp1 Zfloor x). -intro Hx2. -set (x'' := round beta fexp2 (Znearest choice2) x). -destruct (Rlt_or_le x'' (bpow (ln_beta x))) as [Hx''|Hx'']; - [now apply double_round_gt_mid_further_place'|]. -(* bpow (ln_beta x) <= x'' *) -assert (Hx''pow : x'' = bpow (ln_beta x)). -{ assert (H'x'' : x'' < bpow (ln_beta x) + / 2 * ulp beta fexp2 x). - { apply Rle_lt_trans with (x + / 2 * ulp beta fexp2 x). - - apply (Rplus_le_reg_r (- x)); ring_simplify. - apply Rabs_le_inv. - apply error_le_half_ulp. - exact Vfexp2. - - apply Rplus_lt_compat_r. - rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. - apply bpow_ln_beta_gt. } - apply Rle_antisym; [|exact Hx'']. - unfold x'', round, F2R, scaled_mantissa, canonic_exp; simpl. - apply (Rmult_le_reg_r (bpow (- fexp2 (ln_beta x)))); [now apply bpow_gt_0|]. - bpow_simplify. - rewrite <- (Z2R_Zpower _ (_ - _)); [|omega]. - apply Z2R_le. - apply Zlt_succ_le; unfold Z.succ. - apply lt_Z2R. - rewrite Z2R_plus; rewrite Z2R_Zpower; [|omega]. - apply (Rmult_lt_reg_r (bpow (fexp2 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite Rmult_plus_distr_r; rewrite Rmult_1_l. - bpow_simplify. - apply (Rlt_le_trans _ _ _ H'x''). - apply Rplus_le_compat_l. - rewrite <- (Rmult_1_l (Fcore_Raux.bpow _ _)). - rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. - apply Rmult_le_compat_r; [now apply bpow_ge_0|]. - lra. } -assert (Hr : Rabs (x - x'') < / 2 * ulp beta fexp1 x). -{ apply Rle_lt_trans with (/ 2 * ulp beta fexp2 x). - - rewrite Rabs_minus_sym. - apply error_le_half_ulp. - exact Vfexp2. - - apply Rmult_lt_compat_l; [lra|]. - rewrite 2!ulp_neq_0; try now apply Rgt_not_eq. - unfold canonic_exp; apply bpow_lt. - omega. } -unfold round, F2R, scaled_mantissa, canonic_exp; simpl. -assert (Hf : (0 <= ln_beta x - fexp1 (ln_beta x''))%Z). -{ rewrite Hx''pow. - rewrite ln_beta_bpow. - assert (fexp1 (ln_beta x + 1) <= ln_beta x)%Z; [|omega]. - destruct (Zle_or_lt (ln_beta x) (fexp1 (ln_beta x))) as [Hle|Hlt]; - [|now apply Vfexp1]. - assert (H : (ln_beta x = fexp1 (ln_beta x) :> Z)%Z); - [now apply Zle_antisym|]. - rewrite H. - now apply Vfexp1. } -rewrite (Znearest_imp _ _ (beta ^ (ln_beta x - fexp1 (ln_beta x'')))%Z). -- rewrite (Znearest_imp _ _ (beta ^ (ln_beta x - fexp1 (ln_beta x)))%Z). - + rewrite Z2R_Zpower; [|exact Hf]. - rewrite Z2R_Zpower; [|omega]. - now bpow_simplify. - + rewrite Z2R_Zpower; [|omega]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; - [|now apply Rle_ge; apply bpow_ge_0]. - rewrite <- Rabs_mult. - rewrite Rmult_minus_distr_r. - bpow_simplify. - rewrite ulp_neq_0 in Hr;[idtac|now apply Rgt_not_eq]. - rewrite <- Hx''pow; exact Hr. -- rewrite Z2R_Zpower; [|exact Hf]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x'')))); [now apply bpow_gt_0|]. - rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; - [|now apply Rle_ge; apply bpow_ge_0]. - rewrite <- Rabs_mult. - rewrite Rmult_minus_distr_r. - bpow_simplify. - rewrite Rminus_diag_eq; [|exact Hx''pow]. - rewrite Rabs_R0. - rewrite <- (Rmult_0_r (/ 2)). - apply Rmult_lt_compat_l; [lra|apply bpow_gt_0]. -Qed. - -Lemma double_round_gt_mid_same_place : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp2 (ln_beta x) = fexp1 (ln_beta x))%Z -> - midp' fexp1 x < x -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 choice1 choice2 x Px Hf2f1 Hx'. -assert (Hx : round beta fexp1 Zceil x - x < / 2 * ulp beta fexp1 x). -{ apply (Rplus_lt_reg_r (- / 2 * ulp beta fexp1 x + x)); ring_simplify. - now unfold midp' in Hx'. } -assert (H : Rabs (Z2R (Zceil (x * bpow (- fexp1 (ln_beta x)))) - - x * bpow (- fexp1 (ln_beta x))) < / 2). -{ apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - unfold scaled_mantissa, canonic_exp in Hx. - rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; - [|now apply Rle_ge; apply bpow_ge_0]. - rewrite <- Rabs_mult. - rewrite Rmult_minus_distr_r. - bpow_simplify. - apply Rabs_lt. - split. - - apply Rlt_le_trans with 0. - + rewrite <- Ropp_0; apply Ropp_lt_contravar. - rewrite <- (Rmult_0_r (/ 2)). - apply Rmult_lt_compat_l; [lra|]. - apply bpow_gt_0. - + apply Rle_0_minus. - apply round_UP_pt. - exact Vfexp1. - - rewrite ulp_neq_0 in Hx;[exact Hx|now apply Rgt_not_eq]. } -unfold double_round_eq, round at 2. -unfold F2R, scaled_mantissa, canonic_exp; simpl. -rewrite Hf2f1. -rewrite (Znearest_imp _ _ (Zceil (scaled_mantissa beta fexp1 x))). -- rewrite round_generic. - + unfold round, F2R, scaled_mantissa, canonic_exp; simpl. - now rewrite (Znearest_imp _ _ (Zceil (x * bpow (- fexp1 (ln_beta x))))); - [|rewrite Rabs_minus_sym]. - + now apply valid_rnd_N. - + fold (canonic_exp beta fexp1 x). - change (Z2R _ * bpow _) with (round beta fexp1 Zceil x). - apply generic_format_round. - exact Vfexp1. - now apply valid_rnd_UP. -- now rewrite Rabs_minus_sym. -Qed. - -Lemma double_round_gt_mid : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z -> - (fexp1 (ln_beta x) <= ln_beta x)%Z -> - midp' fexp1 x < x -> - ((fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z -> - midp' fexp1 x + / 2 * ulp beta fexp2 x < x) -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx Hx'. -destruct (Zle_or_lt (fexp1 (ln_beta x)) (fexp2 (ln_beta x))) as [Hf2'|Hf2']. -- (* fexp1 (ln_beta x) <= fexp2 (ln_beta x) *) - assert (Hf2'' : (fexp2 (ln_beta x) = fexp1 (ln_beta x) :> Z)%Z); [omega|]. - now apply double_round_gt_mid_same_place. -- (* fexp2 (ln_beta x) < fexp1 (ln_beta x) *) - assert (Hf2'' : (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z); [omega|]. - generalize (Hx' Hf2''); intro Hx''. - now apply double_round_gt_mid_further_place. -Qed. - -Section Double_round_mult. - -Lemma ln_beta_mult_disj : - forall x y, - x <> 0 -> y <> 0 -> - ((ln_beta (x * y) = (ln_beta x + ln_beta y - 1)%Z :> Z) - \/ (ln_beta (x * y) = (ln_beta x + ln_beta y)%Z :> Z)). -Proof. -intros x y Zx Zy. -destruct (ln_beta_mult beta x y Zx Zy). -omega. -Qed. - -Definition double_round_mult_hyp fexp1 fexp2 := - (forall ex ey, (fexp2 (ex + ey) <= fexp1 ex + fexp1 ey)%Z) - /\ (forall ex ey, (fexp2 (ex + ey - 1) <= fexp1 ex + fexp1 ey)%Z). - -Lemma double_round_mult_aux : - forall (fexp1 fexp2 : Z -> Z), - double_round_mult_hyp fexp1 fexp2 -> - forall x y, - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - generic_format beta fexp2 (x * y). -Proof. -intros fexp1 fexp2 Hfexp x y Fx Fy. -destruct (Req_dec x 0) as [Zx|Zx]. -- (* x = 0 *) - rewrite Zx. - rewrite Rmult_0_l. - now apply generic_format_0. -- (* x <> 0 *) - destruct (Req_dec y 0) as [Zy|Zy]. - + (* y = 0 *) - rewrite Zy. - rewrite Rmult_0_r. - now apply generic_format_0. - + (* y <> 0 *) - revert Fx Fy. - unfold generic_format. - unfold canonic_exp. - set (mx := Ztrunc (scaled_mantissa beta fexp1 x)). - set (my := Ztrunc (scaled_mantissa beta fexp1 y)). - unfold F2R; simpl. - intros Fx Fy. - set (fxy := Float beta (mx * my) (fexp1 (ln_beta x) + fexp1 (ln_beta y))). - assert (Hxy : x * y = F2R fxy). - { unfold fxy, F2R; simpl. - rewrite bpow_plus. - rewrite Z2R_mult. - rewrite Fx, Fy at 1. - ring. } - apply generic_format_F2R' with (f := fxy); [now rewrite Hxy|]. - intros _. - unfold canonic_exp, fxy; simpl. - destruct Hfexp as (Hfexp1, Hfexp2). - now destruct (ln_beta_mult_disj x y Zx Zy) as [Lxy|Lxy]; rewrite Lxy. -Qed. - -Variable rnd : R -> Z. -Context { valid_rnd : Valid_rnd rnd }. - -Theorem double_round_mult : - forall (fexp1 fexp2 : Z -> Z), - double_round_mult_hyp fexp1 fexp2 -> - forall x y, - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - round beta fexp1 rnd (round beta fexp2 rnd (x * y)) - = round beta fexp1 rnd (x * y). -Proof. -intros fexp1 fexp2 Hfexp x y Fx Fy. -assert (Hxy : round beta fexp2 rnd (x * y) = x * y). -{ apply round_generic; [assumption|]. - now apply (double_round_mult_aux fexp1 fexp2). } -now rewrite Hxy at 1. -Qed. - -Section Double_round_mult_FLX. - -Import Fcore_FLX. - -Variable prec : Z. -Variable prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Theorem double_round_mult_FLX : - (2 * prec <= prec')%Z -> - forall x y, - FLX_format beta prec x -> FLX_format beta prec y -> - round beta (FLX_exp prec) rnd (round beta (FLX_exp prec') rnd (x * y)) - = round beta (FLX_exp prec) rnd (x * y). -Proof. -intros Hprec x y Fx Fy. -apply double_round_mult; - [|now apply generic_format_FLX|now apply generic_format_FLX]. -unfold double_round_mult_hyp; split; intros ex ey; unfold FLX_exp; -omega. -Qed. - -End Double_round_mult_FLX. - -Section Double_round_mult_FLT. - -Import Fcore_FLX. -Import Fcore_FLT. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Theorem double_round_mult_FLT : - (emin' <= 2 * emin)%Z -> (2 * prec <= prec')%Z -> - forall x y, - FLT_format beta emin prec x -> FLT_format beta emin prec y -> - round beta (FLT_exp emin prec) rnd - (round beta (FLT_exp emin' prec') rnd (x * y)) - = round beta (FLT_exp emin prec) rnd (x * y). -Proof. -intros Hemin Hprec x y Fx Fy. -apply double_round_mult; - [|now apply generic_format_FLT|now apply generic_format_FLT]. -unfold double_round_mult_hyp; split; intros ex ey; -unfold FLT_exp; -generalize (Zmax_spec (ex + ey - prec') emin'); -generalize (Zmax_spec (ex + ey - 1 - prec') emin'); -generalize (Zmax_spec (ex - prec) emin); -generalize (Zmax_spec (ey - prec) emin); -omega. -Qed. - -End Double_round_mult_FLT. - -Section Double_round_mult_FTZ. - -Import Fcore_FLX. -Import Fcore_FTZ. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Theorem double_round_mult_FTZ : - (emin' + prec' <= 2 * emin + prec)%Z -> - (2 * prec <= prec')%Z -> - forall x y, - FTZ_format beta emin prec x -> FTZ_format beta emin prec y -> - round beta (FTZ_exp emin prec) rnd - (round beta (FTZ_exp emin' prec') rnd (x * y)) - = round beta (FTZ_exp emin prec) rnd (x * y). -Proof. -intros Hemin Hprec x y Fx Fy. -apply double_round_mult; - [|now apply generic_format_FTZ|now apply generic_format_FTZ]. -unfold double_round_mult_hyp; split; intros ex ey; -unfold FTZ_exp; -unfold Prec_gt_0 in *; -destruct (Z.ltb_spec (ex + ey - prec') emin'); -destruct (Z.ltb_spec (ex - prec) emin); -destruct (Z.ltb_spec (ey - prec) emin); -destruct (Z.ltb_spec (ex + ey - 1 - prec') emin'); -omega. -Qed. - -End Double_round_mult_FTZ. - -End Double_round_mult. - -Section Double_round_plus. - -Lemma ln_beta_plus_disj : - forall x y, - 0 < y -> y <= x -> - ((ln_beta (x + y) = ln_beta x :> Z) - \/ (ln_beta (x + y) = (ln_beta x + 1)%Z :> Z)). -Proof. -intros x y Py Hxy. -destruct (ln_beta_plus beta x y Py Hxy). -omega. -Qed. - -Lemma ln_beta_plus_separated : - forall fexp : Z -> Z, - forall x y, - 0 < x -> 0 <= y -> - generic_format beta fexp x -> - (ln_beta y <= fexp (ln_beta x))%Z -> - (ln_beta (x + y) = ln_beta x :> Z). -Proof. -intros fexp x y Px Nny Fx Hsep. -destruct (Req_dec y 0) as [Zy|Nzy]. -- (* y = 0 *) - now rewrite Zy; rewrite Rplus_0_r. -- (* y <> 0 *) - apply (ln_beta_plus_eps beta fexp); [assumption|assumption|]. - split; [assumption|]. - rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. - unfold canonic_exp. - destruct (ln_beta y) as (ey, Hey); simpl in *. - apply Rlt_le_trans with (bpow ey). - + now rewrite <- (Rabs_right y); [apply Hey|apply Rle_ge]. - + now apply bpow_le. -Qed. - -Lemma ln_beta_minus_disj : - forall x y, - 0 < x -> 0 < y -> - (ln_beta y <= ln_beta x - 2)%Z -> - ((ln_beta (x - y) = ln_beta x :> Z) - \/ (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]|]. -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. -Qed. - -Lemma ln_beta_minus_separated : - forall fexp : Z -> Z, Valid_exp fexp -> - forall x y, - 0 < x -> 0 < y -> y < x -> - bpow (ln_beta x - 1) < x -> - generic_format beta fexp x -> (ln_beta y <= fexp (ln_beta x))%Z -> - (ln_beta (x - y) = ln_beta x :> Z). -Proof. -intros fexp Vfexp x y Px Py Yltx Xgtpow Fx Ly. -apply ln_beta_unique. -split. -- apply Rabs_ge; right. - assert (Hy : y < ulp beta fexp (bpow (ln_beta x - 1))). - { rewrite ulp_bpow. - replace (_ + _)%Z with (ln_beta x : Z) by ring. - rewrite <- (Rabs_right y); [|now apply Rle_ge; apply Rlt_le]. - apply Rlt_le_trans with (bpow (ln_beta y)). - - apply bpow_ln_beta_gt. - - now apply bpow_le. } - apply (Rplus_le_reg_r y); ring_simplify. - apply Rle_trans with (bpow (ln_beta x - 1) - + ulp beta fexp (bpow (ln_beta x - 1))). - + now apply Rplus_le_compat_l; apply Rlt_le. - + rewrite <- succ_eq_pos;[idtac|apply bpow_ge_0]. - apply succ_le_lt; [apply Vfexp|idtac|exact Fx|assumption]. - apply (generic_format_bpow beta fexp (ln_beta x - 1)). - replace (_ + _)%Z with (ln_beta x : Z) by ring. - assert (fexp (ln_beta x) < ln_beta x)%Z; [|omega]. - now apply ln_beta_generic_gt; [|now apply Rgt_not_eq|]. -- rewrite Rabs_right. - + apply Rlt_trans with x. - * rewrite <- (Rplus_0_r x) at 2. - apply Rplus_lt_compat_l. - rewrite <- Ropp_0. - now apply Ropp_lt_contravar. - * apply Rabs_lt_inv. - apply bpow_ln_beta_gt. - + lra. -Qed. - -Definition double_round_plus_hyp fexp1 fexp2 := - (forall ex ey, (fexp1 (ex + 1) - 1 <= ey)%Z -> (fexp2 ex <= fexp1 ey)%Z) - /\ (forall ex ey, (fexp1 (ex - 1) + 1 <= ey)%Z -> (fexp2 ex <= fexp1 ey)%Z) - /\ (forall ex ey, (fexp1 ex - 1 <= ey)%Z -> (fexp2 ex <= fexp1 ey)%Z) - /\ (forall ex ey, (ex - 1 <= ey)%Z -> (fexp2 ex <= fexp1 ey)%Z). - -Lemma double_round_plus_aux0_aux_aux : - forall (fexp1 fexp2 : Z -> Z), - forall x y, - (fexp1 (ln_beta x) <= fexp1 (ln_beta y))%Z -> - (fexp2 (ln_beta (x + y))%Z <= fexp1 (ln_beta x))%Z -> - (fexp2 (ln_beta (x + y))%Z <= fexp1 (ln_beta y))%Z -> - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - generic_format beta fexp2 (x + y). -Proof. -intros fexp1 fexp2 x y Oxy Hlnx Hlny Fx Fy. -destruct (Req_dec x 0) as [Zx|Nzx]. -- (* x = 0 *) - rewrite Zx, Rplus_0_l in Hlny |- *. - now apply (generic_inclusion_ln_beta beta fexp1). -- (* x <> 0 *) - destruct (Req_dec y 0) as [Zy|Nzy]. - + (* y = 0 *) - rewrite Zy, Rplus_0_r in Hlnx |- *. - now apply (generic_inclusion_ln_beta beta fexp1). - + (* y <> 0 *) - revert Fx Fy. - unfold generic_format at -3, canonic_exp, F2R; simpl. - set (mx := Ztrunc (scaled_mantissa beta fexp1 x)). - set (my := Ztrunc (scaled_mantissa beta fexp1 y)). - intros Fx Fy. - set (fxy := Float beta (mx + my * (beta ^ (fexp1 (ln_beta y) - - fexp1 (ln_beta x)))) - (fexp1 (ln_beta x))). - assert (Hxy : x + y = F2R fxy). - { unfold fxy, F2R; simpl. - rewrite Z2R_plus. - rewrite Rmult_plus_distr_r. - rewrite <- Fx. - rewrite Z2R_mult. - rewrite Z2R_Zpower; [|omega]. - bpow_simplify. - now rewrite <- Fy. } - apply generic_format_F2R' with (f := fxy); [now rewrite Hxy|]. - intros _. - now unfold canonic_exp, fxy; simpl. -Qed. - -Lemma double_round_plus_aux0_aux : - forall (fexp1 fexp2 : Z -> Z), - forall x y, - (fexp2 (ln_beta (x + y))%Z <= fexp1 (ln_beta x))%Z -> - (fexp2 (ln_beta (x + y))%Z <= fexp1 (ln_beta y))%Z -> - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - generic_format beta fexp2 (x + y). -Proof. -intros fexp1 fexp2 x y Hlnx Hlny Fx Fy. -destruct (Z.le_gt_cases (fexp1 (ln_beta x)) (fexp1 (ln_beta y))) as [Hle|Hgt]. -- now apply (double_round_plus_aux0_aux_aux fexp1). -- rewrite Rplus_comm in Hlnx, Hlny |- *. - now apply (double_round_plus_aux0_aux_aux fexp1); [omega| | | |]. -Qed. - -(* fexp1 (ln_beta x) - 1 <= ln_beta y : - * addition is exact in the largest precision (fexp2). *) -Lemma double_round_plus_aux0 : - forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - (0 < x)%R -> (0 < y)%R -> (y <= x)%R -> - (fexp1 (ln_beta x) - 1 <= ln_beta y)%Z -> - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - generic_format beta fexp2 (x + y). -Proof. -intros fexp1 fexp2 Vfexp1 Hexp x y Px Py Hyx Hln Fx Fy. -assert (Nny : (0 <= y)%R); [now apply Rlt_le|]. -destruct Hexp as (_,(Hexp2,(Hexp3,Hexp4))). -destruct (Z.le_gt_cases (ln_beta y) (fexp1 (ln_beta x))) as [Hle|Hgt]. -- (* ln_beta y <= fexp1 (ln_beta x) *) - assert (Lxy : ln_beta (x + y) = ln_beta x :> Z); - [now apply (ln_beta_plus_separated fexp1)|]. - apply (double_round_plus_aux0_aux fexp1); - [| |assumption|assumption]; rewrite Lxy. - + now apply Hexp4; omega. - + now apply Hexp3; omega. -- (* fexp1 (ln_beta x) < ln_beta y *) - apply (double_round_plus_aux0_aux fexp1); [| |assumption|assumption]. - destruct (ln_beta_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - + now apply Hexp4; omega. - + apply Hexp2; apply (ln_beta_le beta y x Py) in Hyx. - replace (_ - _)%Z with (ln_beta x : Z) by ring. - omega. - + destruct (ln_beta_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - * now apply Hexp3; omega. - * apply Hexp2. - replace (_ - _)%Z with (ln_beta x : Z) by ring. - omega. -Qed. - -Lemma double_round_plus_aux1_aux : - forall k, (0 < k)%Z -> - forall (fexp : Z -> Z), - forall x y, - 0 < x -> 0 < y -> - (ln_beta y <= fexp (ln_beta x) - k)%Z -> - (ln_beta (x + y) = ln_beta x :> Z) -> - generic_format beta fexp x -> - 0 < (x + y) - round beta fexp Zfloor (x + y) < bpow (fexp (ln_beta x) - k). -Proof. -assert (Hbeta : (2 <= beta)%Z). -{ destruct beta as (beta_val,beta_prop). - now apply Zle_bool_imp_le. } -intros k Hk fexp x y Px Py Hln Hlxy Fx. -revert Fx. -unfold round, generic_format, F2R, scaled_mantissa, canonic_exp; simpl. -rewrite Hlxy. -set (mx := Ztrunc (x * bpow (- fexp (ln_beta x)))). -intros Fx. -assert (R : (x + y) * bpow (- fexp (ln_beta x)) - = Z2R mx + y * bpow (- fexp (ln_beta x))). -{ rewrite Fx at 1. - rewrite Rmult_plus_distr_r. - now bpow_simplify. } -rewrite R. -assert (LB : 0 < y * bpow (- fexp (ln_beta x))). -{ rewrite <- (Rmult_0_r y). - now apply Rmult_lt_compat_l; [|apply bpow_gt_0]. } -assert (UB : y * bpow (- fexp (ln_beta x)) < / Z2R (beta ^ k)). -{ apply Rlt_le_trans with (bpow (ln_beta y) * bpow (- fexp (ln_beta x))). - - apply Rmult_lt_compat_r; [now apply bpow_gt_0|]. - rewrite <- (Rabs_right y) at 1; [|now apply Rle_ge; apply Rlt_le]. - apply bpow_ln_beta_gt. - - apply Rle_trans with (bpow (fexp (ln_beta x) - k) - * bpow (- fexp (ln_beta x)))%R. - + apply Rmult_le_compat_r; [now apply bpow_ge_0|]. - now apply bpow_le. - + bpow_simplify. - rewrite bpow_opp. - destruct k. - * omega. - * simpl; unfold Fcore_Raux.bpow, Z.pow_pos. - now apply Rle_refl. - * casetype False; apply (Zlt_irrefl 0). - apply (Zlt_trans _ _ _ Hk). - apply Zlt_neg_0. } -rewrite (Zfloor_imp mx). -{ split; ring_simplify. - - apply (Rmult_lt_reg_r (bpow (- fexp (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite Rmult_minus_distr_r, Rmult_0_l. - bpow_simplify. - rewrite R; ring_simplify. - now apply Rmult_lt_0_compat; [|apply bpow_gt_0]. - - apply (Rmult_lt_reg_r (bpow (- fexp (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite Rmult_minus_distr_r. - bpow_simplify. - rewrite R; ring_simplify. - apply (Rlt_le_trans _ _ _ UB). - rewrite bpow_opp. - apply Rinv_le; [now apply bpow_gt_0|]. - now rewrite Z2R_Zpower; [right|omega]. } -split. -- rewrite <- Rplus_0_r at 1; apply Rplus_le_compat_l. - now apply Rlt_le. -- rewrite Z2R_plus; apply Rplus_lt_compat_l. - apply (Rmult_lt_reg_r (bpow (fexp (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite Rmult_1_l. - bpow_simplify. - apply Rlt_trans with (bpow (ln_beta y)). - + rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. - apply bpow_ln_beta_gt. - + apply bpow_lt; omega. -Qed. - -(* ln_beta y <= fexp1 (ln_beta x) - 2 : double_round_lt_mid applies. *) -Lemma double_round_plus_aux1 : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - 0 < x -> 0 < y -> - (ln_beta y <= fexp1 (ln_beta x) - 2)%Z -> - generic_format beta fexp1 x -> - double_round_eq fexp1 fexp2 choice1 choice2 (x + y). -Proof. -assert (Hbeta : (2 <= beta)%Z). -{ destruct beta as (beta_val,beta_prop). - now apply Zle_bool_imp_le. } -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Hly Fx. -assert (Lxy : ln_beta (x + y) = ln_beta x :> Z); - [now apply (ln_beta_plus_separated fexp1); [|apply Rlt_le| |omega]|]. -destruct Hexp as (_,(_,(_,Hexp4))). -assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z); - [now apply Hexp4; omega|]. -assert (Bpow2 : bpow (- 2) <= / 2 * / 2). -{ replace (/2 * /2) with (/4) by field. - rewrite (bpow_opp _ 2). - apply Rinv_le; [lra|]. - apply (Z2R_le (2 * 2) (beta * (beta * 1))). - rewrite Zmult_1_r. - now apply Zmult_le_compat; omega. } -assert (P2 : (0 < 2)%Z) by omega. -unfold double_round_eq. -apply double_round_lt_mid. -- exact Vfexp1. -- exact Vfexp2. -- lra. -- now rewrite Lxy. -- rewrite Lxy. - assert (fexp1 (ln_beta x) < ln_beta x)%Z; [|omega]. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. -- unfold midp. - apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). - apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 2 P2 fexp1 x y Px - Py Hly Lxy Fx))). - ring_simplify. - rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. - unfold canonic_exp; rewrite Lxy. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - bpow_simplify. - apply (Rle_trans _ _ _ Bpow2). - rewrite <- (Rmult_1_r (/ 2)) at 3. - apply Rmult_le_compat_l; lra. -- rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. - unfold round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Lxy. - intro Hf2'. - apply (Rmult_lt_reg_r (bpow (- fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - bpow_simplify. - apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). - unfold midp; ring_simplify. - apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 2 P2 fexp1 x y Px - Py Hly Lxy Fx))). - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. - unfold canonic_exp; rewrite Lxy, Rmult_minus_distr_r; bpow_simplify. - apply (Rle_trans _ _ _ Bpow2). - rewrite <- (Rmult_1_r (/ 2)) at 3; rewrite <- Rmult_minus_distr_l. - apply Rmult_le_compat_l; [lra|]. - apply (Rplus_le_reg_r (- 1)); ring_simplify. - replace (_ - _) with (- (/ 2)) by lra. - apply Ropp_le_contravar. - { apply Rle_trans with (bpow (- 1)). - - apply bpow_le; omega. - - unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - apply Rinv_le; [lra|]. - change 2 with (Z2R 2); apply Z2R_le; omega. } -Qed. - -(* double_round_plus_aux{0,1} together *) -Lemma double_round_plus_aux2 : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - 0 < x -> 0 < y -> y <= x -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x + y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Hyx Fx Fy. -unfold double_round_eq. -destruct (Zle_or_lt (ln_beta y) (fexp1 (ln_beta x) - 2)) as [Hly|Hly]. -- (* ln_beta y <= fexp1 (ln_beta x) - 2 *) - now apply double_round_plus_aux1. -- (* fexp1 (ln_beta x) - 2 < ln_beta y *) - rewrite (round_generic beta fexp2). - + reflexivity. - + now apply valid_rnd_N. - + assert (Hf1 : (fexp1 (ln_beta x) - 1 <= ln_beta y)%Z); [omega|]. - now apply (double_round_plus_aux0 fexp1). -Qed. - -Lemma double_round_plus_aux : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - 0 <= x -> 0 <= y -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x + y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Nnx Nny Fx Fy. -unfold double_round_eq. -destruct (Req_dec x 0) as [Zx|Nzx]. -- (* x = 0 *) - destruct Hexp as (_,(_,(_,Hexp4))). - rewrite Zx; rewrite Rplus_0_l. - rewrite (round_generic beta fexp2). - + reflexivity. - + now apply valid_rnd_N. - + apply (generic_inclusion_ln_beta beta fexp1). - now intros _; apply Hexp4; omega. - exact Fy. -- (* x <> 0 *) - destruct (Req_dec y 0) as [Zy|Nzy]. - + (* y = 0 *) - destruct Hexp as (_,(_,(_,Hexp4))). - rewrite Zy; rewrite Rplus_0_r. - rewrite (round_generic beta fexp2). - * reflexivity. - * now apply valid_rnd_N. - * apply (generic_inclusion_ln_beta beta fexp1). - now intros _; apply Hexp4; omega. - exact Fx. - + (* y <> 0 *) - assert (Px : 0 < x); [lra|]. - assert (Py : 0 < y); [lra|]. - destruct (Rlt_or_le x y) as [H|H]. - * (* x < y *) - apply Rlt_le in H. - rewrite Rplus_comm. - now apply double_round_plus_aux2. - * now apply double_round_plus_aux2. -Qed. - -Lemma double_round_minus_aux0_aux : - forall (fexp1 fexp2 : Z -> Z), - forall x y, - (fexp2 (ln_beta (x - y))%Z <= fexp1 (ln_beta x))%Z -> - (fexp2 (ln_beta (x - y))%Z <= fexp1 (ln_beta y))%Z -> - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - generic_format beta fexp2 (x - y). -Proof. -intros fexp1 fexp2 x y. -replace (x - y)%R with (x + (- y))%R; [|ring]. -intros Hlnx Hlny Fx Fy. -rewrite <- (ln_beta_opp beta y) in Hlny. -apply generic_format_opp in Fy. -now apply (double_round_plus_aux0_aux fexp1). -Qed. - -(* fexp1 (ln_beta x) - 1 <= ln_beta y : - * substraction is exact in the largest precision (fexp2). *) -Lemma double_round_minus_aux0 : - forall (fexp1 fexp2 : Z -> Z), - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - 0 < y -> y < x -> - (fexp1 (ln_beta x) - 1 <= ln_beta y)%Z -> - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - generic_format beta fexp2 (x - y). -Proof. -intros fexp1 fexp2 Hexp x y Py Hyx Hln Fx Fy. -assert (Px := Rlt_trans 0 y x Py Hyx). -destruct Hexp as (Hexp1,(_,(Hexp3,Hexp4))). -assert (Lyx : (ln_beta y <= ln_beta x)%Z); - [now apply ln_beta_le; [|apply Rlt_le]|]. -destruct (Z.lt_ge_cases (ln_beta x - 2) (ln_beta y)) as [Hlt|Hge]. -- (* ln_beta x - 2 < ln_beta y *) - assert (Hor : (ln_beta y = ln_beta x :> Z) - \/ (ln_beta y = ln_beta x - 1 :> Z)%Z); [omega|]. - destruct Hor as [Heq|Heqm1]. - + (* ln_beta y = ln_beta x *) - apply (double_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - * apply Hexp4. - apply Zle_trans with (ln_beta (x - y)); [omega|]. - now apply ln_beta_minus. - * rewrite Heq. - apply Hexp4. - apply Zle_trans with (ln_beta (x - y)); [omega|]. - now apply ln_beta_minus. - + (* ln_beta y = ln_beta x - 1 *) - apply (double_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - * apply Hexp4. - apply Zle_trans with (ln_beta (x - y)); [omega|]. - now apply ln_beta_minus. - * rewrite Heqm1. - apply Hexp4. - apply Zplus_le_compat_r. - now apply ln_beta_minus. -- (* ln_beta y <= ln_beta x - 2 *) - destruct (ln_beta_minus_disj x y Px Py Hge) as [Lxmy|Lxmy]. - + (* ln_beta (x - y) = ln_beta x *) - apply (double_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - * apply Hexp4. - omega. - * now rewrite Lxmy; apply Hexp3. - + (* ln_beta (x - y) = ln_beta x - 1 *) - apply (double_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]; - rewrite Lxmy. - * apply Hexp1. - replace (_ + _)%Z with (ln_beta x : Z); [|ring]. - now apply Zle_trans with (ln_beta y). - * apply Hexp1. - now replace (_ + _)%Z with (ln_beta x : Z); [|ring]. -Qed. - -(* ln_beta y <= fexp1 (ln_beta x) - 2, - * fexp1 (ln_beta (x - y)) - 1 <= ln_beta y : - * substraction is exact in the largest precision (fexp2). *) -Lemma double_round_minus_aux1 : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - 0 < y -> y < x -> - (ln_beta y <= fexp1 (ln_beta x) - 2)%Z -> - (fexp1 (ln_beta (x - y)) - 1 <= ln_beta y)%Z -> - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - generic_format beta fexp2 (x - y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 Hexp x y Py Hyx Hln Hln' Fx Fy. -assert (Px := Rlt_trans 0 y x Py Hyx). -destruct Hexp as (Hexp1,(Hexp2,(Hexp3,Hexp4))). -assert (Lyx : (ln_beta y <= ln_beta x)%Z); - [now apply ln_beta_le; [|apply Rlt_le]|]. -assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -assert (Hfy : (fexp1 (ln_beta y) < ln_beta y)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -apply (double_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. -- apply Zle_trans with (fexp1 (ln_beta (x - y))). - + apply Hexp4; omega. - + omega. -- now apply Hexp3. -Qed. - -Lemma double_round_minus_aux2_aux : - forall (fexp : Z -> Z), - Valid_exp fexp -> - forall x y, - 0 < y -> y < x -> - (ln_beta y <= fexp (ln_beta x) - 1)%Z -> - generic_format beta fexp x -> - generic_format beta fexp y -> - round beta fexp Zceil (x - y) - (x - y) <= y. -Proof. -intros fexp Vfexp x y Py Hxy Hly Fx Fy. -assert (Px := Rlt_trans 0 y x Py Hxy). -revert Fx. -unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl. -set (mx := Ztrunc (x * bpow (- fexp (ln_beta x)))). -intro Fx. -assert (Hfx : (fexp (ln_beta x) < ln_beta x)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -assert (Hfy : (fexp (ln_beta y) < ln_beta y)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -destruct (Rlt_or_le (bpow (ln_beta x - 1)) x) as [Hx|Hx]. -- (* bpow (ln_beta x - 1) < x *) - assert (Lxy : ln_beta (x - y) = ln_beta x :> Z); - [now apply (ln_beta_minus_separated fexp); [| | | | | |omega]|]. - assert (Rxy : round beta fexp Zceil (x - y) = x). - { unfold round, F2R, scaled_mantissa, canonic_exp; simpl. - rewrite Lxy. - apply eq_sym; rewrite Fx at 1; apply eq_sym. - apply Rmult_eq_compat_r. - apply f_equal. - rewrite Fx at 1. - rewrite Rmult_minus_distr_r. - bpow_simplify. - apply Zceil_imp. - split. - - unfold Zminus; rewrite Z2R_plus. - apply Rplus_lt_compat_l. - apply Ropp_lt_contravar; simpl. - apply (Rmult_lt_reg_r (bpow (fexp (ln_beta x)))); - [now apply bpow_gt_0|]. - rewrite Rmult_1_l; bpow_simplify. - apply Rlt_le_trans with (bpow (ln_beta y)). - + rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. - apply bpow_ln_beta_gt. - + apply bpow_le. - omega. - - rewrite <- (Rplus_0_r (Z2R _)) at 2. - apply Rplus_le_compat_l. - rewrite <- Ropp_0; apply Ropp_le_contravar. - rewrite <- (Rmult_0_r y). - apply Rmult_le_compat_l; [now apply Rlt_le|]. - now apply bpow_ge_0. } - rewrite Rxy; ring_simplify. - apply Rle_refl. -- (* x <= bpow (ln_beta x - 1) *) - assert (Xpow : x = bpow (ln_beta x - 1)). - { apply Rle_antisym; [exact Hx|]. - destruct (ln_beta x) as (ex, Hex); simpl. - rewrite <- (Rabs_right x); [|now apply Rle_ge; apply Rlt_le]. - apply Hex. - now apply Rgt_not_eq. } - assert (Lxy : (ln_beta (x - y) = ln_beta x - 1 :> Z)%Z). - { apply Zle_antisym. - - apply ln_beta_le_bpow. - + apply Rminus_eq_contra. - now intro Hx'; rewrite Hx' in Hxy; apply (Rlt_irrefl y). - + rewrite Rabs_right; lra. - - apply (ln_beta_minus_lb beta x y Px Py). - omega. } - assert (Hfx1 : (fexp (ln_beta x - 1) < ln_beta x - 1)%Z); - [now apply (valid_exp_large fexp (ln_beta y)); [|omega]|]. - assert (Rxy : round beta fexp Zceil (x - y) <= x). - { rewrite Xpow at 2. - unfold round, F2R, scaled_mantissa, canonic_exp; simpl. - rewrite Lxy. - apply (Rmult_le_reg_r (bpow (- fexp (ln_beta x - 1)%Z))); - [now apply bpow_gt_0|]. - bpow_simplify. - rewrite <- (Z2R_Zpower beta (_ - _ - _)); [|omega]. - apply Z2R_le. - apply Zceil_glb. - rewrite Z2R_Zpower; [|omega]. - rewrite Xpow at 1. - rewrite Rmult_minus_distr_r. - bpow_simplify. - rewrite <- (Rplus_0_r (bpow _)) at 2. - apply Rplus_le_compat_l. - rewrite <- Ropp_0; apply Ropp_le_contravar. - rewrite <- (Rmult_0_r y). - apply Rmult_le_compat_l; [now apply Rlt_le|]. - now apply bpow_ge_0. } - lra. -Qed. - -(* ln_beta y <= fexp1 (ln_beta x) - 2 : - * ln_beta y <= fexp1 (ln_beta (x - y)) - 2 : - * double_round_gt_mid applies. *) -Lemma double_round_minus_aux2 : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - 0 < y -> y < x -> - (ln_beta y <= fexp1 (ln_beta x) - 2)%Z -> - (ln_beta y <= fexp1 (ln_beta (x - y)) - 2)%Z -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x - y). -Proof. -assert (Hbeta : (2 <= beta)%Z). -{ destruct beta as (beta_val,beta_prop). - now apply Zle_bool_imp_le. } -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hxy Hly Hly' Fx Fy. -assert (Px := Rlt_trans 0 y x Py Hxy). -destruct Hexp as (_,(_,(_,Hexp4))). -assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z); - [now apply Hexp4; omega|]. -assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -assert (Bpow2 : bpow (- 2) <= / 2 * / 2). -{ replace (/2 * /2) with (/4) by field. - rewrite (bpow_opp _ 2). - apply Rinv_le; [lra|]. - apply (Z2R_le (2 * 2) (beta * (beta * 1))). - rewrite Zmult_1_r. - now apply Zmult_le_compat; omega. } -assert (Ly : y < bpow (ln_beta y)). -{ apply Rabs_lt_inv. - apply bpow_ln_beta_gt. } -unfold double_round_eq. -apply double_round_gt_mid. -- exact Vfexp1. -- exact Vfexp2. -- lra. -- apply Hexp4; omega. -- assert (fexp1 (ln_beta (x - y)) < ln_beta (x - y))%Z; [|omega]. - apply (valid_exp_large fexp1 (ln_beta x - 1)). - + apply (valid_exp_large fexp1 (ln_beta y)); [|omega]. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. - + now apply ln_beta_minus_lb; [| |omega]. -- unfold midp'. - apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y))). - ring_simplify. - replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring. - apply Rlt_le_trans with (bpow (fexp1 (ln_beta (x - y)) - 2)). - + apply Rle_lt_trans with y; - [now apply double_round_minus_aux2_aux; try assumption; omega|]. - apply (Rlt_le_trans _ _ _ Ly). - now apply bpow_le. - + rewrite ulp_neq_0;[idtac|now apply sym_not_eq, Rlt_not_eq, Rgt_minus]. - unfold canonic_exp. - replace (_ - 2)%Z with (fexp1 (ln_beta (x - y)) - 1 - 1)%Z by ring. - unfold Zminus at 1; rewrite bpow_plus. - rewrite Rmult_comm. - apply Rmult_le_compat. - * now apply bpow_ge_0. - * now apply bpow_ge_0. - * unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite Zmult_1_r; apply Rinv_le. - lra. - now change 2 with (Z2R 2); apply Z2R_le. - * apply bpow_le; omega. -- intro Hf2'. - unfold midp'. - apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y) - - / 2 * ulp beta fexp2 (x - y))). - ring_simplify. - replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring. - apply Rle_lt_trans with y; - [now apply double_round_minus_aux2_aux; try assumption; omega|]. - apply (Rlt_le_trans _ _ _ Ly). - apply Rle_trans with (bpow (fexp1 (ln_beta (x - y)) - 2)); - [now apply bpow_le|]. - replace (_ - 2)%Z with (fexp1 (ln_beta (x - y)) - 1 - 1)%Z by ring. - unfold Zminus at 1; rewrite bpow_plus. - rewrite <- Rmult_minus_distr_l. - rewrite Rmult_comm; apply Rmult_le_compat. - + apply bpow_ge_0. - + apply bpow_ge_0. - + unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite Zmult_1_r; apply Rinv_le; [lra|]. - now change 2 with (Z2R 2); apply Z2R_le. - + rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, Rgt_minus. - unfold canonic_exp. - apply (Rplus_le_reg_r (bpow (fexp2 (ln_beta (x - y))))); ring_simplify. - apply Rle_trans with (2 * bpow (fexp1 (ln_beta (x - y)) - 1)). - * replace (2 * bpow (fexp1 (ln_beta (x - y)) - 1)) with (bpow (fexp1 (ln_beta (x - y)) - 1) + bpow (fexp1 (ln_beta (x - y)) - 1)) by ring. - apply Rplus_le_compat_l. - now apply bpow_le. - * unfold Zminus; rewrite bpow_plus. - rewrite Rmult_comm; rewrite Rmult_assoc. - rewrite <- Rmult_1_r. - apply Rmult_le_compat_l; [now apply bpow_ge_0|]. - unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite Zmult_1_r. - apply Z2R_le, Rinv_le in Hbeta. - simpl in Hbeta. - lra. - apply Rlt_0_2. -Qed. - -(* double_round_minus_aux{0,1,2} together *) -Lemma double_round_minus_aux3 : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - 0 < y -> y <= x -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x - y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hyx Fx Fy. -assert (Px := Rlt_le_trans 0 y x Py Hyx). -unfold double_round_eq. -destruct (Req_dec y x) as [Hy|Hy]. -- (* y = x *) - rewrite Hy; replace (x - x) with 0 by ring. - rewrite round_0. - + reflexivity. - + now apply valid_rnd_N. -- (* y < x *) - assert (Hyx' : y < x); [lra|]. - destruct (Zle_or_lt (ln_beta y) (fexp1 (ln_beta x) - 2)) as [Hly|Hly]. - + (* ln_beta y <= fexp1 (ln_beta x) - 2 *) - destruct (Zle_or_lt (ln_beta y) (fexp1 (ln_beta (x - y)) - 2)) - as [Hly'|Hly']. - * (* ln_beta y <= fexp1 (ln_beta (x - y)) - 2 *) - now apply double_round_minus_aux2. - * (* fexp1 (ln_beta (x - y)) - 2 < ln_beta y *) - { rewrite (round_generic beta fexp2). - - reflexivity. - - now apply valid_rnd_N. - - assert (Hf1 : (fexp1 (ln_beta (x - y)) - 1 <= ln_beta y)%Z); [omega|]. - now apply (double_round_minus_aux1 fexp1). } - + rewrite (round_generic beta fexp2). - * reflexivity. - * now apply valid_rnd_N. - * assert (Hf1 : (fexp1 (ln_beta x) - 1 <= ln_beta y)%Z); [omega|]. - now apply (double_round_minus_aux0 fexp1). -Qed. - -Lemma double_round_minus_aux : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - 0 <= x -> 0 <= y -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x - y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Nnx Nny Fx Fy. -unfold double_round_eq. -destruct (Req_dec x 0) as [Zx|Nzx]. -- (* x = 0 *) - rewrite Zx; unfold Rminus; rewrite Rplus_0_l. - do 3 rewrite round_N_opp. - rewrite (round_generic beta fexp2). - * reflexivity. - * now apply valid_rnd_N. - * apply (generic_inclusion_ln_beta beta fexp1). - destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. - exact Fy. -- (* x <> 0 *) - destruct (Req_dec y 0) as [Zy|Nzy]. - + (* y = 0 *) - rewrite Zy; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. - rewrite (round_generic beta fexp2). - * reflexivity. - * now apply valid_rnd_N. - * apply (generic_inclusion_ln_beta beta fexp1). - destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. - exact Fx. - + (* y <> 0 *) - assert (Px : 0 < x); [lra|]. - assert (Py : 0 < y); [lra|]. - destruct (Rlt_or_le x y) as [H|H]. - * (* x < y *) - apply Rlt_le in H. - replace (x - y) with (- (y - x)) by ring. - do 3 rewrite round_N_opp. - apply Ropp_eq_compat. - now apply double_round_minus_aux3. - * (* y <= x *) - now apply double_round_minus_aux3. -Qed. - -Lemma double_round_plus : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x + y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Fx Fy. -unfold double_round_eq. -destruct (Rlt_or_le x 0) as [Sx|Sx]; destruct (Rlt_or_le y 0) as [Sy|Sy]. -- (* x < 0, y < 0 *) - replace (x + y) with (- (- x - y)); [|ring]. - do 3 rewrite round_N_opp. - apply Ropp_eq_compat. - assert (Px : 0 <= - x); [lra|]. - assert (Py : 0 <= - y); [lra|]. - apply generic_format_opp in Fx. - apply generic_format_opp in Fy. - now apply double_round_plus_aux. -- (* x < 0, 0 <= y *) - replace (x + y) with (y - (- x)); [|ring]. - assert (Px : 0 <= - x); [lra|]. - apply generic_format_opp in Fx. - now apply double_round_minus_aux. -- (* 0 <= x, y < 0 *) - replace (x + y) with (x - (- y)); [|ring]. - assert (Py : 0 <= - y); [lra|]. - apply generic_format_opp in Fy. - now apply double_round_minus_aux. -- (* 0 <= x, 0 <= y *) - now apply double_round_plus_aux. -Qed. - -Lemma double_round_minus : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_hyp fexp1 fexp2 -> - forall x y, - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x - y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Fx Fy. -unfold Rminus. -apply generic_format_opp in Fy. -now apply double_round_plus. -Qed. - -Section Double_round_plus_FLX. - -Import Fcore_FLX. - -Variable prec : Z. -Variable prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FLX_double_round_plus_hyp : - (2 * prec + 1 <= prec')%Z -> - double_round_plus_hyp (FLX_exp prec) (FLX_exp prec'). -Proof. -intros Hprec. -unfold FLX_exp. -unfold double_round_plus_hyp; split; [|split; [|split]]; -intros ex ey; try omega. -unfold Prec_gt_0 in prec_gt_0_. -omega. -Qed. - -Theorem double_round_plus_FLX : - forall choice1 choice2, - (2 * prec + 1 <= prec')%Z -> - forall x y, - FLX_format beta prec x -> FLX_format beta prec y -> - double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x + y). -Proof. -intros choice1 choice2 Hprec x y Fx Fy. -apply double_round_plus. -- now apply FLX_exp_valid. -- now apply FLX_exp_valid. -- now apply FLX_double_round_plus_hyp. -- now apply generic_format_FLX. -- now apply generic_format_FLX. -Qed. - -Theorem double_round_minus_FLX : - forall choice1 choice2, - (2 * prec + 1 <= prec')%Z -> - forall x y, - FLX_format beta prec x -> FLX_format beta prec y -> - double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x - y). -Proof. -intros choice1 choice2 Hprec x y Fx Fy. -apply double_round_minus. -- now apply FLX_exp_valid. -- now apply FLX_exp_valid. -- now apply FLX_double_round_plus_hyp. -- now apply generic_format_FLX. -- now apply generic_format_FLX. -Qed. - -End Double_round_plus_FLX. - -Section Double_round_plus_FLT. - -Import Fcore_FLX. -Import Fcore_FLT. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FLT_double_round_plus_hyp : - (emin' <= emin)%Z -> (2 * prec + 1 <= prec')%Z -> - double_round_plus_hyp (FLT_exp emin prec) (FLT_exp emin' prec'). -Proof. -intros Hemin Hprec. -unfold FLT_exp. -unfold double_round_plus_hyp; split; [|split; [|split]]; intros ex ey. -- generalize (Zmax_spec (ex + 1 - prec) emin). - generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ey - prec) emin). - omega. -- generalize (Zmax_spec (ex - 1 - prec) emin). - generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ey - prec) emin). - omega. -- generalize (Zmax_spec (ex - prec) emin). - generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ey - prec) emin). - omega. -- unfold Prec_gt_0 in prec_gt_0_. - generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ey - prec) emin). - omega. -Qed. - -Theorem double_round_plus_FLT : - forall choice1 choice2, - (emin' <= emin)%Z -> (2 * prec + 1 <= prec')%Z -> - forall x y, - FLT_format beta emin prec x -> FLT_format beta emin prec y -> - double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec') - choice1 choice2 (x + y). -Proof. -intros choice1 choice2 Hemin Hprec x y Fx Fy. -apply double_round_plus. -- now apply FLT_exp_valid. -- now apply FLT_exp_valid. -- now apply FLT_double_round_plus_hyp. -- now apply generic_format_FLT. -- now apply generic_format_FLT. -Qed. - -Theorem double_round_minus_FLT : - forall choice1 choice2, - (emin' <= emin)%Z -> (2 * prec + 1 <= prec')%Z -> - forall x y, - FLT_format beta emin prec x -> FLT_format beta emin prec y -> - double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec') - choice1 choice2 (x - y). -Proof. -intros choice1 choice2 Hemin Hprec x y Fx Fy. -apply double_round_minus. -- now apply FLT_exp_valid. -- now apply FLT_exp_valid. -- now apply FLT_double_round_plus_hyp. -- now apply generic_format_FLT. -- now apply generic_format_FLT. -Qed. - -End Double_round_plus_FLT. - -Section Double_round_plus_FTZ. - -Import Fcore_FLX. -Import Fcore_FTZ. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FTZ_double_round_plus_hyp : - (emin' + prec' <= emin + 1)%Z -> (2 * prec + 1 <= prec')%Z -> - double_round_plus_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec'). -Proof. -intros Hemin Hprec. -unfold FTZ_exp. -unfold Prec_gt_0 in *. -unfold double_round_plus_hyp; split; [|split; [|split]]; intros ex ey. -- destruct (Z.ltb_spec (ex + 1 - prec) emin); - destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ey - prec) emin); - omega. -- destruct (Z.ltb_spec (ex - 1 - prec) emin); - destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ey - prec) emin); - omega. -- destruct (Z.ltb_spec (ex - prec) emin); - destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ey - prec) emin); - omega. -- destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ey - prec) emin); - omega. -Qed. - -Theorem double_round_plus_FTZ : - forall choice1 choice2, - (emin' + prec' <= emin + 1)%Z -> (2 * prec + 1 <= prec')%Z -> - forall x y, - FTZ_format beta emin prec x -> FTZ_format beta emin prec y -> - double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec') - choice1 choice2 (x + y). -Proof. -intros choice1 choice2 Hemin Hprec x y Fx Fy. -apply double_round_plus. -- now apply FTZ_exp_valid. -- now apply FTZ_exp_valid. -- now apply FTZ_double_round_plus_hyp. -- now apply generic_format_FTZ. -- now apply generic_format_FTZ. -Qed. - -Theorem double_round_minus_FTZ : - forall choice1 choice2, - (emin' + prec' <= emin + 1)%Z -> (2 * prec + 1 <= prec')%Z -> - forall x y, - FTZ_format beta emin prec x -> FTZ_format beta emin prec y -> - double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec') - choice1 choice2 (x - y). -Proof. -intros choice1 choice2 Hemin Hprec x y Fx Fy. -apply double_round_minus. -- now apply FTZ_exp_valid. -- now apply FTZ_exp_valid. -- now apply FTZ_double_round_plus_hyp. -- now apply generic_format_FTZ. -- now apply generic_format_FTZ. -Qed. - -End Double_round_plus_FTZ. - -Section Double_round_plus_beta_ge_3. - -Definition double_round_plus_beta_ge_3_hyp fexp1 fexp2 := - (forall ex ey, (fexp1 (ex + 1) <= ey)%Z -> (fexp2 ex <= fexp1 ey)%Z) - /\ (forall ex ey, (fexp1 (ex - 1) + 1 <= ey)%Z -> (fexp2 ex <= fexp1 ey)%Z) - /\ (forall ex ey, (fexp1 ex <= ey)%Z -> (fexp2 ex <= fexp1 ey)%Z) - /\ (forall ex ey, (ex - 1 <= ey)%Z -> (fexp2 ex <= fexp1 ey)%Z). - -(* fexp1 (ln_beta x) <= ln_beta y : - * addition is exact in the largest precision (fexp2). *) -Lemma double_round_plus_beta_ge_3_aux0 : - forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - (0 < y)%R -> (y <= x)%R -> - (fexp1 (ln_beta x) <= ln_beta y)%Z -> - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - generic_format beta fexp2 (x + y). -Proof. -intros fexp1 fexp2 Vfexp1 Hexp x y Py Hyx Hln Fx Fy. -assert (Px := Rlt_le_trans 0 y x Py Hyx). -assert (Nny : (0 <= y)%R); [now apply Rlt_le|]. -destruct Hexp as (_,(Hexp2,(Hexp3,Hexp4))). -destruct (Z.le_gt_cases (ln_beta y) (fexp1 (ln_beta x))) as [Hle|Hgt]. -- (* ln_beta y <= fexp1 (ln_beta x) *) - assert (Lxy : ln_beta (x + y) = ln_beta x :> Z); - [now apply (ln_beta_plus_separated fexp1)|]. - apply (double_round_plus_aux0_aux fexp1); - [| |assumption|assumption]; rewrite Lxy. - + now apply Hexp4; omega. - + now apply Hexp3; omega. -- (* fexp1 (ln_beta x) < ln_beta y *) - apply (double_round_plus_aux0_aux fexp1); [| |assumption|assumption]. - destruct (ln_beta_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - + now apply Hexp4; omega. - + apply Hexp2; apply (ln_beta_le beta y x Py) in Hyx. - replace (_ - _)%Z with (ln_beta x : Z) by ring. - omega. - + destruct (ln_beta_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - * now apply Hexp3; omega. - * apply Hexp2. - replace (_ - _)%Z with (ln_beta x : Z) by ring. - omega. -Qed. - -(* ln_beta y <= fexp1 (ln_beta x) - 1 : double_round_lt_mid applies. *) -Lemma double_round_plus_beta_ge_3_aux1 : - (3 <= beta)%Z -> - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - 0 < x -> 0 < y -> - (ln_beta y <= fexp1 (ln_beta x) - 1)%Z -> - generic_format beta fexp1 x -> - double_round_eq fexp1 fexp2 choice1 choice2 (x + y). -Proof. -intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Hly Fx. -assert (Lxy : ln_beta (x + y) = ln_beta x :> Z); - [now apply (ln_beta_plus_separated fexp1); [|apply Rlt_le| |omega]|]. -destruct Hexp as (_,(_,(_,Hexp4))). -assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z); - [now apply Hexp4; omega|]. -assert (Bpow3 : bpow (- 1) <= / 3). -{ unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite Zmult_1_r. - apply Rinv_le; [lra|]. - now change 3 with (Z2R 3); apply Z2R_le. } -assert (P1 : (0 < 1)%Z) by omega. -unfold double_round_eq. -apply double_round_lt_mid. -- exact Vfexp1. -- exact Vfexp2. -- lra. -- now rewrite Lxy. -- rewrite Lxy. - assert (fexp1 (ln_beta x) < ln_beta x)%Z; [|omega]. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. -- unfold midp. - apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). - apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 1 P1 fexp1 x y Px - Py Hly Lxy Fx))). - ring_simplify. - rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. - unfold canonic_exp; rewrite Lxy. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - bpow_simplify. - apply (Rle_trans _ _ _ Bpow3); lra. -- rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. - unfold round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Lxy. - intro Hf2'. - unfold midp. - apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))); ring_simplify. - rewrite <- Rmult_minus_distr_l. - apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 1 P1 fexp1 x y Px - Py Hly Lxy Fx))). - rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. - unfold canonic_exp; rewrite Lxy. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - rewrite (Rmult_assoc (/ 2)). - rewrite Rmult_minus_distr_r. - bpow_simplify. - apply (Rle_trans _ _ _ Bpow3). - apply Rle_trans with (/ 2 * (2 / 3)); [lra|]. - apply Rmult_le_compat_l; [lra|]. - apply (Rplus_le_reg_r (- 1)); ring_simplify. - replace (_ - _) with (- (/ 3)) by lra. - apply Ropp_le_contravar. - now apply Rle_trans with (bpow (- 1)); [apply bpow_le; omega|]. -Qed. - -(* double_round_plus_beta_ge_3_aux{0,1} together *) -Lemma double_round_plus_beta_ge_3_aux2 : - (3 <= beta)%Z -> - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - 0 < y -> y <= x -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x + y). -Proof. -intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hyx Fx Fy. -assert (Px := Rlt_le_trans 0 y x Py Hyx). -unfold double_round_eq. -destruct (Zle_or_lt (ln_beta y) (fexp1 (ln_beta x) - 1)) as [Hly|Hly]. -- (* ln_beta y <= fexp1 (ln_beta x) - 1 *) - now apply double_round_plus_beta_ge_3_aux1. -- (* fexp1 (ln_beta x) - 1 < ln_beta y *) - rewrite (round_generic beta fexp2). - + reflexivity. - + now apply valid_rnd_N. - + assert (Hf1 : (fexp1 (ln_beta x) <= ln_beta y)%Z); [omega|]. - now apply (double_round_plus_beta_ge_3_aux0 fexp1). -Qed. - -Lemma double_round_plus_beta_ge_3_aux : - (3 <= beta)%Z -> - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - 0 <= x -> 0 <= y -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x + y). -Proof. -intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Nnx Nny Fx Fy. -unfold double_round_eq. -destruct (Req_dec x 0) as [Zx|Nzx]. -- (* x = 0 *) - destruct Hexp as (_,(_,(_,Hexp4))). - rewrite Zx; rewrite Rplus_0_l. - rewrite (round_generic beta fexp2). - + reflexivity. - + now apply valid_rnd_N. - + apply (generic_inclusion_ln_beta beta fexp1). - now intros _; apply Hexp4; omega. - exact Fy. -- (* x <> 0 *) - destruct (Req_dec y 0) as [Zy|Nzy]. - + (* y = 0 *) - destruct Hexp as (_,(_,(_,Hexp4))). - rewrite Zy; rewrite Rplus_0_r. - rewrite (round_generic beta fexp2). - * reflexivity. - * now apply valid_rnd_N. - * apply (generic_inclusion_ln_beta beta fexp1). - now intros _; apply Hexp4; omega. - exact Fx. - + (* y <> 0 *) - assert (Px : 0 < x); [lra|]. - assert (Py : 0 < y); [lra|]. - destruct (Rlt_or_le x y) as [H|H]. - * (* x < y *) - apply Rlt_le in H. - rewrite Rplus_comm. - now apply double_round_plus_beta_ge_3_aux2. - * now apply double_round_plus_beta_ge_3_aux2. -Qed. - -(* fexp1 (ln_beta x) <= ln_beta y : - * substraction is exact in the largest precision (fexp2). *) -Lemma double_round_minus_beta_ge_3_aux0 : - forall (fexp1 fexp2 : Z -> Z), - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - 0 < y -> y < x -> - (fexp1 (ln_beta x) <= ln_beta y)%Z -> - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - generic_format beta fexp2 (x - y). -Proof. -intros fexp1 fexp2 Hexp x y Py Hyx Hln Fx Fy. -assert (Px := Rlt_trans 0 y x Py Hyx). -destruct Hexp as (Hexp1,(_,(Hexp3,Hexp4))). -assert (Lyx : (ln_beta y <= ln_beta x)%Z); - [now apply ln_beta_le; [|apply Rlt_le]|]. -destruct (Z.lt_ge_cases (ln_beta x - 2) (ln_beta y)) as [Hlt|Hge]. -- (* ln_beta x - 2 < ln_beta y *) - assert (Hor : (ln_beta y = ln_beta x :> Z) - \/ (ln_beta y = ln_beta x - 1 :> Z)%Z); [omega|]. - destruct Hor as [Heq|Heqm1]. - + (* ln_beta y = ln_beta x *) - apply (double_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - * apply Hexp4. - apply Zle_trans with (ln_beta (x - y)); [omega|]. - now apply ln_beta_minus. - * rewrite Heq. - apply Hexp4. - apply Zle_trans with (ln_beta (x - y)); [omega|]. - now apply ln_beta_minus. - + (* ln_beta y = ln_beta x - 1 *) - apply (double_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - * apply Hexp4. - apply Zle_trans with (ln_beta (x - y)); [omega|]. - now apply ln_beta_minus. - * rewrite Heqm1. - apply Hexp4. - apply Zplus_le_compat_r. - now apply ln_beta_minus. -- (* ln_beta y <= ln_beta x - 2 *) - destruct (ln_beta_minus_disj x y Px Py Hge) as [Lxmy|Lxmy]. - + (* ln_beta (x - y) = ln_beta x *) - apply (double_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - * apply Hexp4. - omega. - * now rewrite Lxmy; apply Hexp3. - + (* ln_beta (x - y) = ln_beta x - 1 *) - apply (double_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]; - rewrite Lxmy. - * apply Hexp1. - replace (_ + _)%Z with (ln_beta x : Z); [|ring]. - now apply Zle_trans with (ln_beta y). - * apply Hexp1. - now replace (_ + _)%Z with (ln_beta x : Z); [|ring]. -Qed. - -(* ln_beta y <= fexp1 (ln_beta x) - 1, - * fexp1 (ln_beta (x - y)) <= ln_beta y : - * substraction is exact in the largest precision (fexp2). *) -Lemma double_round_minus_beta_ge_3_aux1 : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - 0 < y -> y < x -> - (ln_beta y <= fexp1 (ln_beta x) - 1)%Z -> - (fexp1 (ln_beta (x - y)) <= ln_beta y)%Z -> - generic_format beta fexp1 x -> generic_format beta fexp1 y -> - generic_format beta fexp2 (x - y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 Hexp x y Py Hyx Hln Hln' Fx Fy. -assert (Px := Rlt_trans 0 y x Py Hyx). -destruct Hexp as (Hexp1,(Hexp2,(Hexp3,Hexp4))). -assert (Lyx : (ln_beta y <= ln_beta x)%Z); - [now apply ln_beta_le; [|apply Rlt_le]|]. -assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -assert (Hfy : (fexp1 (ln_beta y) < ln_beta y)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -apply (double_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. -- apply Zle_trans with (fexp1 (ln_beta (x - y))). - + apply Hexp4; omega. - + omega. -- now apply Hexp3. -Qed. - -(* ln_beta y <= fexp1 (ln_beta x) - 1 : - * ln_beta y <= fexp1 (ln_beta (x - y)) - 1 : - * double_round_gt_mid applies. *) -Lemma double_round_minus_beta_ge_3_aux2 : - (3 <= beta)%Z -> - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - 0 < y -> y < x -> - (ln_beta y <= fexp1 (ln_beta x) - 1)%Z -> - (ln_beta y <= fexp1 (ln_beta (x - y)) - 1)%Z -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x - y). -Proof. -intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hxy Hly Hly' Fx Fy. -assert (Px := Rlt_trans 0 y x Py Hxy). -destruct Hexp as (_,(_,(_,Hexp4))). -assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z); - [now apply Hexp4; omega|]. -assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -assert (Bpow3 : bpow (- 1) <= / 3). -{ unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite Zmult_1_r. - apply Rinv_le; [lra|]. - now change 3 with (Z2R 3); apply Z2R_le. } -assert (Ly : y < bpow (ln_beta y)). -{ apply Rabs_lt_inv. - apply bpow_ln_beta_gt. } -unfold double_round_eq. -apply double_round_gt_mid. -- exact Vfexp1. -- exact Vfexp2. -- lra. -- apply Hexp4; omega. -- assert (fexp1 (ln_beta (x - y)) < ln_beta (x - y))%Z; [|omega]. - apply (valid_exp_large fexp1 (ln_beta x - 1)). - + apply (valid_exp_large fexp1 (ln_beta y)); [|omega]. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. - + now apply ln_beta_minus_lb; [| |omega]. -- unfold midp'. - apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y))). - ring_simplify. - replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring. - apply Rlt_le_trans with (bpow (fexp1 (ln_beta (x - y)) - 1)). - + apply Rle_lt_trans with y; - [now apply double_round_minus_aux2_aux|]. - apply (Rlt_le_trans _ _ _ Ly). - now apply bpow_le. - + rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rgt_minus]. - unfold canonic_exp. - unfold Zminus at 1; rewrite bpow_plus. - rewrite Rmult_comm. - apply Rmult_le_compat_r; [now apply bpow_ge_0|]. - unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite Zmult_1_r; apply Rinv_le; [lra|]. - now change 2 with (Z2R 2); apply Z2R_le; omega. -- intro Hf2'. - unfold midp'. - apply (Rplus_lt_reg_r (/ 2 * (ulp beta fexp1 (x - y) - - ulp beta fexp2 (x - y)) - (x - y))). - ring_simplify; rewrite <- Rmult_minus_distr_l. - replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring. - apply Rle_lt_trans with y; - [now apply double_round_minus_aux2_aux|]. - apply (Rlt_le_trans _ _ _ Ly). - apply Rle_trans with (bpow (fexp1 (ln_beta (x - y)) - 1)); - [now apply bpow_le|]. - rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, Rgt_minus. - unfold canonic_exp. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta (x - y))))); - [now apply bpow_gt_0|]. - rewrite Rmult_assoc. - rewrite Rmult_minus_distr_r. - bpow_simplify. - apply Rle_trans with (/ 3). - + unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite Zmult_1_r; apply Rinv_le; [lra|]. - now change 3 with (Z2R 3); apply Z2R_le. - + replace (/ 3) with (/ 2 * (2 / 3)) by field. - apply Rmult_le_compat_l; [lra|]. - apply (Rplus_le_reg_r (- 1)); ring_simplify. - replace (_ - _) with (- / 3) by field. - apply Ropp_le_contravar. - apply Rle_trans with (bpow (- 1)). - * apply bpow_le; omega. - * unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite Zmult_1_r; apply Rinv_le; [lra|]. - now change 3 with (Z2R 3); apply Z2R_le. -Qed. - -(* double_round_minus_aux{0,1,2} together *) -Lemma double_round_minus_beta_ge_3_aux3 : - (3 <= beta)%Z -> - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - 0 < y -> y <= x -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x - y). -Proof. -intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hyx Fx Fy. -assert (Px := Rlt_le_trans 0 y x Py Hyx). -unfold double_round_eq. -destruct (Req_dec y x) as [Hy|Hy]. -- (* y = x *) - rewrite Hy; replace (x - x) with 0 by ring. - rewrite round_0. - + reflexivity. - + now apply valid_rnd_N. -- (* y < x *) - assert (Hyx' : y < x); [lra|]. - destruct (Zle_or_lt (ln_beta y) (fexp1 (ln_beta x) - 1)) as [Hly|Hly]. - + (* ln_beta y <= fexp1 (ln_beta x) - 1 *) - destruct (Zle_or_lt (ln_beta y) (fexp1 (ln_beta (x - y)) - 1)) - as [Hly'|Hly']. - * (* ln_beta y <= fexp1 (ln_beta (x - y)) - 1 *) - now apply double_round_minus_beta_ge_3_aux2. - * (* fexp1 (ln_beta (x - y)) - 1 < ln_beta y *) - { rewrite (round_generic beta fexp2). - - reflexivity. - - now apply valid_rnd_N. - - assert (Hf1 : (fexp1 (ln_beta (x - y)) <= ln_beta y)%Z); [omega|]. - now apply (double_round_minus_beta_ge_3_aux1 fexp1). } - + rewrite (round_generic beta fexp2). - * reflexivity. - * now apply valid_rnd_N. - * assert (Hf1 : (fexp1 (ln_beta x) <= ln_beta y)%Z); [omega|]. - now apply (double_round_minus_beta_ge_3_aux0 fexp1). -Qed. - -Lemma double_round_minus_beta_ge_3_aux : - (3 <= beta)%Z -> - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - 0 <= x -> 0 <= y -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x - y). -Proof. -intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Nnx Nny Fx Fy. -unfold double_round_eq. -destruct (Req_dec x 0) as [Zx|Nzx]. -- (* x = 0 *) - rewrite Zx; unfold Rminus; rewrite Rplus_0_l. - do 3 rewrite round_N_opp. - rewrite (round_generic beta fexp2). - * reflexivity. - * now apply valid_rnd_N. - * apply (generic_inclusion_ln_beta beta fexp1). - destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. - exact Fy. -- (* x <> 0 *) - destruct (Req_dec y 0) as [Zy|Nzy]. - + (* y = 0 *) - rewrite Zy; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. - rewrite (round_generic beta fexp2). - * reflexivity. - * now apply valid_rnd_N. - * apply (generic_inclusion_ln_beta beta fexp1). - destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. - exact Fx. - + (* y <> 0 *) - assert (Px : 0 < x); [lra|]. - assert (Py : 0 < y); [lra|]. - destruct (Rlt_or_le x y) as [H|H]. - * (* x < y *) - apply Rlt_le in H. - replace (x - y) with (- (y - x)) by ring. - do 3 rewrite round_N_opp. - apply Ropp_eq_compat. - now apply double_round_minus_beta_ge_3_aux3. - * (* y <= x *) - now apply double_round_minus_beta_ge_3_aux3. -Qed. - -Lemma double_round_plus_beta_ge_3 : - (3 <= beta)%Z -> - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x + y). -Proof. -intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Fx Fy. -unfold double_round_eq. -destruct (Rlt_or_le x 0) as [Sx|Sx]; destruct (Rlt_or_le y 0) as [Sy|Sy]. -- (* x < 0, y < 0 *) - replace (x + y) with (- (- x - y)); [|ring]. - do 3 rewrite round_N_opp. - apply Ropp_eq_compat. - assert (Px : 0 <= - x); [lra|]. - assert (Py : 0 <= - y); [lra|]. - apply generic_format_opp in Fx. - apply generic_format_opp in Fy. - now apply double_round_plus_beta_ge_3_aux. -- (* x < 0, 0 <= y *) - replace (x + y) with (y - (- x)); [|ring]. - assert (Px : 0 <= - x); [lra|]. - apply generic_format_opp in Fx. - now apply double_round_minus_beta_ge_3_aux. -- (* 0 <= x, y < 0 *) - replace (x + y) with (x - (- y)); [|ring]. - assert (Py : 0 <= - y); [lra|]. - apply generic_format_opp in Fy. - now apply double_round_minus_beta_ge_3_aux. -- (* 0 <= x, 0 <= y *) - now apply double_round_plus_beta_ge_3_aux. -Qed. - -Lemma double_round_minus_beta_ge_3 : - (3 <= beta)%Z -> - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_plus_beta_ge_3_hyp fexp1 fexp2 -> - forall x y, - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x - y). -Proof. -intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Fx Fy. -unfold Rminus. -apply generic_format_opp in Fy. -now apply double_round_plus_beta_ge_3. -Qed. - -Section Double_round_plus_beta_ge_3_FLX. - -Import Fcore_FLX. - -Variable prec : Z. -Variable prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FLX_double_round_plus_beta_ge_3_hyp : - (2 * prec <= prec')%Z -> - double_round_plus_beta_ge_3_hyp (FLX_exp prec) (FLX_exp prec'). -Proof. -intros Hprec. -unfold FLX_exp. -unfold double_round_plus_beta_ge_3_hyp; split; [|split; [|split]]; -intros ex ey; try omega. -unfold Prec_gt_0 in prec_gt_0_. -omega. -Qed. - -Theorem double_round_plus_beta_ge_3_FLX : - (3 <= beta)%Z -> - forall choice1 choice2, - (2 * prec <= prec')%Z -> - forall x y, - FLX_format beta prec x -> FLX_format beta prec y -> - double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x + y). -Proof. -intros Hbeta choice1 choice2 Hprec x y Fx Fy. -apply double_round_plus_beta_ge_3. -- exact Hbeta. -- now apply FLX_exp_valid. -- now apply FLX_exp_valid. -- now apply FLX_double_round_plus_beta_ge_3_hyp. -- now apply generic_format_FLX. -- now apply generic_format_FLX. -Qed. - -Theorem double_round_minus_beta_ge_3_FLX : - (3 <= beta)%Z -> - forall choice1 choice2, - (2 * prec <= prec')%Z -> - forall x y, - FLX_format beta prec x -> FLX_format beta prec y -> - double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x - y). -Proof. -intros Hbeta choice1 choice2 Hprec x y Fx Fy. -apply double_round_minus_beta_ge_3. -- exact Hbeta. -- now apply FLX_exp_valid. -- now apply FLX_exp_valid. -- now apply FLX_double_round_plus_beta_ge_3_hyp. -- now apply generic_format_FLX. -- now apply generic_format_FLX. -Qed. - -End Double_round_plus_beta_ge_3_FLX. - -Section Double_round_plus_beta_ge_3_FLT. - -Import Fcore_FLX. -Import Fcore_FLT. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FLT_double_round_plus_beta_ge_3_hyp : - (emin' <= emin)%Z -> (2 * prec <= prec')%Z -> - double_round_plus_beta_ge_3_hyp (FLT_exp emin prec) (FLT_exp emin' prec'). -Proof. -intros Hemin Hprec. -unfold FLT_exp. -unfold double_round_plus_beta_ge_3_hyp; split; [|split; [|split]]; intros ex ey. -- generalize (Zmax_spec (ex + 1 - prec) emin). - generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ey - prec) emin). - omega. -- generalize (Zmax_spec (ex - 1 - prec) emin). - generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ey - prec) emin). - omega. -- generalize (Zmax_spec (ex - prec) emin). - generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ey - prec) emin). - omega. -- unfold Prec_gt_0 in prec_gt_0_. - generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ey - prec) emin). - omega. -Qed. - -Theorem double_round_plus_beta_ge_3_FLT : - (3 <= beta)%Z -> - forall choice1 choice2, - (emin' <= emin)%Z -> (2 * prec <= prec')%Z -> - forall x y, - FLT_format beta emin prec x -> FLT_format beta emin prec y -> - double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec') - choice1 choice2 (x + y). -Proof. -intros Hbeta choice1 choice2 Hemin Hprec x y Fx Fy. -apply double_round_plus_beta_ge_3. -- exact Hbeta. -- now apply FLT_exp_valid. -- now apply FLT_exp_valid. -- now apply FLT_double_round_plus_beta_ge_3_hyp. -- now apply generic_format_FLT. -- now apply generic_format_FLT. -Qed. - -Theorem double_round_minus_beta_ge_3_FLT : - (3 <= beta)%Z -> - forall choice1 choice2, - (emin' <= emin)%Z -> (2 * prec <= prec')%Z -> - forall x y, - FLT_format beta emin prec x -> FLT_format beta emin prec y -> - double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec') - choice1 choice2 (x - y). -Proof. -intros Hbeta choice1 choice2 Hemin Hprec x y Fx Fy. -apply double_round_minus_beta_ge_3. -- exact Hbeta. -- now apply FLT_exp_valid. -- now apply FLT_exp_valid. -- now apply FLT_double_round_plus_beta_ge_3_hyp. -- now apply generic_format_FLT. -- now apply generic_format_FLT. -Qed. - -End Double_round_plus_beta_ge_3_FLT. - -Section Double_round_plus_beta_ge_3_FTZ. - -Import Fcore_FLX. -Import Fcore_FTZ. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FTZ_double_round_plus_beta_ge_3_hyp : - (emin' + prec' <= emin + 1)%Z -> (2 * prec <= prec')%Z -> - double_round_plus_beta_ge_3_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec'). -Proof. -intros Hemin Hprec. -unfold FTZ_exp. -unfold Prec_gt_0 in *. -unfold double_round_plus_beta_ge_3_hyp; split; [|split; [|split]]; intros ex ey. -- destruct (Z.ltb_spec (ex + 1 - prec) emin); - destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ey - prec) emin); - omega. -- destruct (Z.ltb_spec (ex - 1 - prec) emin); - destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ey - prec) emin); - omega. -- destruct (Z.ltb_spec (ex - prec) emin); - destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ey - prec) emin); - omega. -- destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ey - prec) emin); - omega. -Qed. - -Theorem double_round_plus_beta_ge_3_FTZ : - (3 <= beta)%Z -> - forall choice1 choice2, - (emin' + prec' <= emin + 1)%Z -> (2 * prec <= prec')%Z -> - forall x y, - FTZ_format beta emin prec x -> FTZ_format beta emin prec y -> - double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec') - choice1 choice2 (x + y). -Proof. -intros Hbeta choice1 choice2 Hemin Hprec x y Fx Fy. -apply double_round_plus_beta_ge_3. -- exact Hbeta. -- now apply FTZ_exp_valid. -- now apply FTZ_exp_valid. -- now apply FTZ_double_round_plus_beta_ge_3_hyp. -- now apply generic_format_FTZ. -- now apply generic_format_FTZ. -Qed. - -Theorem double_round_minus_beta_ge_3_FTZ : - (3 <= beta)%Z -> - forall choice1 choice2, - (emin' + prec' <= emin + 1)%Z -> (2 * prec <= prec')%Z -> - forall x y, - FTZ_format beta emin prec x -> FTZ_format beta emin prec y -> - double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec') - choice1 choice2 (x - y). -Proof. -intros Hbeta choice1 choice2 Hemin Hprec x y Fx Fy. -apply double_round_minus_beta_ge_3. -- exact Hbeta. -- now apply FTZ_exp_valid. -- now apply FTZ_exp_valid. -- now apply FTZ_double_round_plus_beta_ge_3_hyp. -- now apply generic_format_FTZ. -- now apply generic_format_FTZ. -Qed. - -End Double_round_plus_beta_ge_3_FTZ. - -End Double_round_plus_beta_ge_3. - -End Double_round_plus. - -Lemma double_round_mid_cases : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z -> - (fexp1 (ln_beta x) <= ln_beta x)%Z -> - (Rabs (x - midp fexp1 x) <= / 2 * (ulp beta fexp2 x) -> - double_round_eq fexp1 fexp2 choice1 choice2 x) -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1. -unfold double_round_eq, midp. -set (rd := round beta fexp1 Zfloor x). -set (u1 := ulp beta fexp1 x). -set (u2 := ulp beta fexp2 x). -intros Cmid. -destruct (generic_format_EM beta fexp1 x) as [Fx|Nfx]. -- (* generic_format beta fexp1 x *) - rewrite (round_generic beta fexp2); [reflexivity|now apply valid_rnd_N|]. - now apply (generic_inclusion_ln_beta beta fexp1); [omega|]. -- (* ~ generic_format beta fexp1 x *) - assert (Hceil : round beta fexp1 Zceil x = rd + u1); - [now apply round_UP_DN_ulp|]. - assert (Hf2' : (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z); [omega|]. - destruct (Rlt_or_le (x - rd) (/ 2 * (u1 - u2))). - + (* x - rd < / 2 * (u1 - u2) *) - apply double_round_lt_mid_further_place; try assumption. - unfold midp. fold rd; fold u1; fold u2. - apply (Rplus_lt_reg_r (- rd)); ring_simplify. - now rewrite <- Rmult_minus_distr_l. - + (* / 2 * (u1 - u2) <= x - rd *) - { destruct (Rlt_or_le (/ 2 * (u1 + u2)) (x - rd)). - - (* / 2 * (u1 + u2) < x - rd *) - assert (round beta fexp1 Zceil x - x - < / 2 * (ulp beta fexp1 x - ulp beta fexp2 x)). - { rewrite Hceil; fold u1; fold u2. - lra. } - apply double_round_gt_mid_further_place; try assumption. - unfold midp'; lra. - - (* x - rd <= / 2 * (u1 + u2) *) - apply Cmid, Rabs_le; split; lra. } -Qed. - -Section Double_round_sqrt. - -Definition double_round_sqrt_hyp fexp1 fexp2 := - (forall ex, (2 * fexp1 ex <= fexp1 (2 * ex))%Z) - /\ (forall ex, (2 * fexp1 ex <= fexp1 (2 * ex - 1))%Z) - /\ (forall ex, (fexp1 (2 * ex) < 2 * ex)%Z -> - (fexp2 ex + ex <= 2 * fexp1 ex - 2)%Z). - -Lemma ln_beta_sqrt_disj : - forall x, - 0 < x -> - (ln_beta x = 2 * ln_beta (sqrt x) - 1 :> Z)%Z - \/ (ln_beta x = 2 * ln_beta (sqrt x) :> Z)%Z. -Proof. -intros x Px. -generalize (ln_beta_sqrt beta x Px). -intro H. -omega. -Qed. - -Lemma double_round_sqrt_aux : - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - double_round_sqrt_hyp fexp1 fexp2 -> - forall x, - 0 < x -> - (fexp2 (ln_beta (sqrt x)) <= fexp1 (ln_beta (sqrt x)) - 1)%Z -> - generic_format beta fexp1 x -> - / 2 * ulp beta fexp2 (sqrt x) < Rabs (sqrt x - midp fexp1 (sqrt x)). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx. -assert (Hbeta : (2 <= beta)%Z). -{ destruct beta as (beta_val,beta_prop). - now apply Zle_bool_imp_le. } -set (a := round beta fexp1 Zfloor (sqrt x)). -set (u1 := bpow (fexp1 (ln_beta (sqrt x)))). -set (u2 := bpow (fexp2 (ln_beta (sqrt x)))). -set (b := / 2 * (u1 - u2)). -set (b' := / 2 * (u1 + u2)). -unfold midp; rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, sqrt_lt_R0. -apply Rnot_ge_lt; intro H; apply Rge_le in H. -assert (Fa : generic_format beta fexp1 a). -{ unfold a. - apply generic_format_round. - - exact Vfexp1. - - now apply valid_rnd_DN. } -revert Fa; revert Fx. -unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl. -set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))). -set (ma := Ztrunc (a * bpow (- fexp1 (ln_beta a)))). -intros Fx Fa. -assert (Nna : 0 <= a). -{ rewrite <- (round_0 beta fexp1 Zfloor). - unfold a; apply round_le. - - exact Vfexp1. - - now apply valid_rnd_DN. - - apply sqrt_pos. } -assert (Phu1 : 0 < / 2 * u1). -{ apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]. } -assert (Phu2 : 0 < / 2 * u2). -{ apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]. } -assert (Pb : 0 < b). -{ unfold b. - rewrite <- (Rmult_0_r (/ 2)). - apply Rmult_lt_compat_l; [lra|]. - apply Rlt_Rminus. - unfold u2, u1. - apply bpow_lt. - omega. } -assert (Pb' : 0 < b'). -{ now unfold b'; rewrite Rmult_plus_distr_l; apply Rplus_lt_0_compat. } -assert (Hr : sqrt x <= a + b'). -{ unfold b'; apply (Rplus_le_reg_r (- / 2 * u1 - a)); ring_simplify. - replace (_ - _) with (sqrt x - (a + / 2 * u1)) by ring. - now apply Rabs_le_inv. } -assert (Hl : a + b <= sqrt x). -{ unfold b; apply (Rplus_le_reg_r (- / 2 * u1 - a)); ring_simplify. - replace (_ + sqrt _) with (sqrt x - (a + / 2 * u1)) by ring. - rewrite Ropp_mult_distr_l_reverse. - now apply Rabs_le_inv in H; destruct H. } -assert (Hf1 : (2 * fexp1 (ln_beta (sqrt x)) <= fexp1 (ln_beta (x)))%Z); - [destruct (ln_beta_sqrt_disj x Px) as [H'|H']; rewrite H'; apply Hexp|]. -assert (Hlx : (fexp1 (2 * ln_beta (sqrt x)) < 2 * ln_beta (sqrt x))%Z). -{ destruct (ln_beta_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (ln_beta x)); [|omega]. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. - - rewrite <- Hlx. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. } -assert (Hsl : a * a + u1 * a - u2 * a + b * b <= x). -{ replace (_ + _) with ((a + b) * (a + b)); [|now unfold b; field]. - rewrite <- sqrt_def; [|now apply Rlt_le]. - assert (H' : 0 <= a + b); [now apply Rlt_le, Rplus_le_lt_0_compat|]. - now apply Rmult_le_compat. } -assert (Hsr : x <= a * a + u1 * a + u2 * a + b' * b'). -{ replace (_ + _) with ((a + b') * (a + b')); [|now unfold b'; field]. - rewrite <- (sqrt_def x); [|now apply Rlt_le]. - assert (H' : 0 <= sqrt x); [now apply sqrt_pos|]. - now apply Rmult_le_compat. } -destruct (Req_dec a 0) as [Za|Nza]. -- (* a = 0 *) - apply (Rlt_irrefl 0). - apply Rlt_le_trans with (b * b); [now apply Rmult_lt_0_compat|]. - apply Rle_trans with x. - + revert Hsl; unfold Rminus; rewrite Za; do 3 rewrite Rmult_0_r. - now rewrite Ropp_0; do 3 rewrite Rplus_0_l. - + rewrite Fx. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - rewrite Rmult_0_l; bpow_simplify. - unfold mx. - rewrite Ztrunc_floor; - [|now apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0]]. - apply Req_le. - change 0 with (Z2R 0); apply f_equal. - apply Zfloor_imp. - split; [now apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0]|simpl]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite Rmult_1_l; bpow_simplify. - apply Rlt_le_trans with (bpow (2 * fexp1 (ln_beta (sqrt x)))); - [|now apply bpow_le]. - change 2%Z with (1 + 1)%Z; rewrite Zmult_plus_distr_l; rewrite Zmult_1_l. - rewrite bpow_plus. - rewrite <- (sqrt_def x) at 1; [|now apply Rlt_le]. - assert (sqrt x < bpow (fexp1 (ln_beta (sqrt x)))); - [|now apply Rmult_lt_compat; [apply sqrt_pos|apply sqrt_pos| |]]. - apply (Rle_lt_trans _ _ _ Hr); rewrite Za; rewrite Rplus_0_l. - unfold b'; change (bpow _) with u1. - apply Rlt_le_trans with (/ 2 * (u1 + u1)); [|lra]. - apply Rmult_lt_compat_l; [lra|]; apply Rplus_lt_compat_l. - unfold u2, u1, ulp, canonic_exp; apply bpow_lt; omega. -- (* a <> 0 *) - assert (Pa : 0 < a); [lra|]. - assert (Hla : (ln_beta a = ln_beta (sqrt x) :> Z)). - { unfold a; apply ln_beta_DN. - - exact Vfexp1. - - now fold a. } - assert (Hl' : 0 < - (u2 * a) + b * b). - { apply (Rplus_lt_reg_r (u2 * a)); ring_simplify. - unfold b; ring_simplify. - apply (Rplus_lt_reg_r (/ 2 * u2 * u1)); field_simplify. - replace (_ / 2) with (u2 * (a + / 2 * u1)) by field. - replace (_ / 8) with (/ 4 * (u2 ^ 2 + u1 ^ 2)) by field. - apply Rlt_le_trans with (u2 * bpow (ln_beta (sqrt x))). - - apply Rmult_lt_compat_l; [now unfold u2, ulp; apply bpow_gt_0|]. - unfold u1; rewrite <- Hla. - apply Rlt_le_trans with (a + bpow (fexp1 (ln_beta a))). - + apply Rplus_lt_compat_l. - rewrite <- (Rmult_1_l (bpow _)) at 2. - apply Rmult_lt_compat_r; [apply bpow_gt_0|lra]. - + apply Rle_trans with (a+ ulp beta fexp1 a). - right; now rewrite ulp_neq_0. - apply (id_p_ulp_le_bpow _ _ _ _ Pa Fa). - apply Rabs_lt_inv, bpow_ln_beta_gt. - - apply Rle_trans with (bpow (- 2) * u1 ^ 2). - + unfold pow; rewrite Rmult_1_r. - unfold u1, u2, ulp, canonic_exp; bpow_simplify; apply bpow_le. - now apply Hexp. - + apply Rmult_le_compat. - * apply bpow_ge_0. - * apply pow2_ge_0. - * unfold Fcore_Raux.bpow, Z.pow_pos; simpl; rewrite Zmult_1_r. - apply Rinv_le; [lra|]. - change 4 with (Z2R (2 * 2)%Z); apply Z2R_le, Zmult_le_compat; omega. - * rewrite <- (Rplus_0_l (u1 ^ 2)) at 1; apply Rplus_le_compat_r. - apply pow2_ge_0. } - assert (Hr' : x <= a * a + u1 * a). - { rewrite Hla in Fa. - rewrite <- Rmult_plus_distr_r. - unfold u1, ulp, canonic_exp. - rewrite <- (Rmult_1_l (bpow _)); rewrite Fa; rewrite <- Rmult_plus_distr_r. - rewrite <- Rmult_assoc; rewrite (Rmult_comm _ (Z2R ma)). - rewrite <- (Rmult_assoc (Z2R ma)); bpow_simplify. - apply (Rmult_le_reg_r (bpow (- 2 * fexp1 (ln_beta (sqrt x))))); - [now apply bpow_gt_0|bpow_simplify]. - rewrite Fx at 1; bpow_simplify. - rewrite <- Z2R_Zpower; [|omega]. - change 1 with (Z2R 1); rewrite <- Z2R_plus; do 2 rewrite <- Z2R_mult. - apply Z2R_le, Zlt_succ_le, lt_Z2R. - unfold Z.succ; rewrite Z2R_plus; do 2 rewrite Z2R_mult; rewrite Z2R_plus. - rewrite Z2R_Zpower; [|omega]. - apply (Rmult_lt_reg_r (bpow (2 * fexp1 (ln_beta (sqrt x))))); - [now apply bpow_gt_0|bpow_simplify]. - rewrite <- Fx. - change 2%Z with (1 + 1)%Z; rewrite Zmult_plus_distr_l; rewrite Zmult_1_l. - rewrite bpow_plus; simpl. - replace (_ * _) with (a * a + u1 * a + u1 * u1); - [|unfold u1, ulp, canonic_exp; rewrite Fa; ring]. - apply (Rle_lt_trans _ _ _ Hsr). - rewrite Rplus_assoc; apply Rplus_lt_compat_l. - apply (Rplus_lt_reg_r (- b' * b' + / 2 * u1 * u2)); ring_simplify. - replace (_ + _) with ((a + / 2 * u1) * u2) by ring. - apply Rlt_le_trans with (bpow (ln_beta (sqrt x)) * u2). - - apply Rmult_lt_compat_r; [now unfold u2, ulp; apply bpow_gt_0|]. - apply Rlt_le_trans with (a + u1); [lra|]. - unfold u1; fold (canonic_exp beta fexp1 (sqrt x)). - rewrite <- canonic_exp_DN; [|exact Vfexp1|exact Pa]; fold a. - rewrite <- ulp_neq_0; trivial. - apply id_p_ulp_le_bpow. - + exact Pa. - + now apply round_DN_pt. - + apply Rle_lt_trans with (sqrt x). - * now apply round_DN_pt. - * apply Rabs_lt_inv. - apply bpow_ln_beta_gt. - - apply Rle_trans with (/ 2 * u1 ^ 2). - + apply Rle_trans with (bpow (- 2) * u1 ^ 2). - * unfold pow; rewrite Rmult_1_r. - unfold u2, u1, ulp, canonic_exp. - bpow_simplify. - apply bpow_le. - rewrite Zplus_comm. - now apply Hexp. - * apply Rmult_le_compat_r; [now apply pow2_ge_0|]. - unfold Fcore_Raux.bpow; simpl; unfold Z.pow_pos; simpl. - rewrite Zmult_1_r. - apply Rinv_le; [lra|]. - change 2 with (Z2R 2); apply Z2R_le. - rewrite <- (Zmult_1_l 2). - apply Zmult_le_compat; omega. - + assert (u2 ^ 2 < u1 ^ 2); [|unfold b'; lra]. - unfold pow; do 2 rewrite Rmult_1_r. - assert (H' : 0 <= u2); [unfold u2, ulp; apply bpow_ge_0|]. - assert (u2 < u1); [|now apply Rmult_lt_compat]. - unfold u1, u2, ulp, canonic_exp; apply bpow_lt; omega. } - apply (Rlt_irrefl (a * a + u1 * a)). - apply Rlt_le_trans with (a * a + u1 * a - u2 * a + b * b). - + rewrite <- (Rplus_0_r (a * a + _)) at 1. - unfold Rminus; rewrite (Rplus_assoc _ _ (b * b)). - now apply Rplus_lt_compat_l. - + now apply Rle_trans with x. -Qed. - - -Lemma double_round_sqrt : - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_sqrt_hyp fexp1 fexp2 -> - forall x, - generic_format beta fexp1 x -> - double_round_eq fexp1 fexp2 choice1 choice2 (sqrt x). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x Fx. -unfold double_round_eq. -destruct (Rle_or_lt x 0) as [Npx|Px]. -- (* x <= 0 *) - rewrite (sqrt_neg _ Npx). - now rewrite round_0; [|apply valid_rnd_N]. -- (* 0 < x *) - assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); - [now apply ln_beta_generic_gt; try assumption; lra|]. - assert (Hfsx : (fexp1 (ln_beta (sqrt x)) < ln_beta (sqrt x))%Z). - { destruct (Rle_or_lt x 1) as [Hx|Hx]. - - (* x <= 1 *) - apply (valid_exp_large fexp1 (ln_beta x)); [exact Hfx|]. - apply ln_beta_le; [exact Px|]. - rewrite <- (sqrt_def x) at 1; [|lra]. - rewrite <- Rmult_1_r. - apply Rmult_le_compat_l. - + apply sqrt_pos. - + rewrite <- sqrt_1. - now apply sqrt_le_1_alt. - - (* 1 < x *) - generalize ((proj1 (proj2 Hexp)) 1%Z). - replace (_ - 1)%Z with 1%Z by ring. - intro Hexp10. - assert (Hf0 : (fexp1 1 < 1)%Z); [omega|clear Hexp10]. - apply (valid_exp_large fexp1 1); [exact Hf0|]. - apply ln_beta_ge_bpow. - rewrite Zeq_minus; [|reflexivity]. - unfold Fcore_Raux.bpow; simpl. - apply Rabs_ge; right. - rewrite <- sqrt_1. - apply sqrt_le_1_alt. - now apply Rlt_le. } - assert (Hf2 : (fexp2 (ln_beta (sqrt x)) <= fexp1 (ln_beta (sqrt x)) - 1)%Z). - { assert (H : (fexp1 (2 * ln_beta (sqrt x)) < 2 * ln_beta (sqrt x))%Z). - { destruct (ln_beta_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (ln_beta x)); [|omega]. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. - - rewrite <- Hlx. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. } - generalize ((proj2 (proj2 Hexp)) (ln_beta (sqrt x)) H). - omega. } - apply double_round_mid_cases. - + exact Vfexp1. - + exact Vfexp2. - + now apply sqrt_lt_R0. - + omega. - + omega. - + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid). - apply (double_round_sqrt_aux fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx). -Qed. - -Section Double_round_sqrt_FLX. - -Import Fcore_FLX. - -Variable prec : Z. -Variable prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FLX_double_round_sqrt_hyp : - (2 * prec + 2 <= prec')%Z -> - double_round_sqrt_hyp (FLX_exp prec) (FLX_exp prec'). -Proof. -intros Hprec. -unfold FLX_exp. -unfold Prec_gt_0 in prec_gt_0_. -unfold double_round_sqrt_hyp; split; [|split]; intro ex; omega. -Qed. - -Theorem double_round_sqrt_FLX : - forall choice1 choice2, - (2 * prec + 2 <= prec')%Z -> - forall x, - FLX_format beta prec x -> - double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (sqrt x). -Proof. -intros choice1 choice2 Hprec x Fx. -apply double_round_sqrt. -- now apply FLX_exp_valid. -- now apply FLX_exp_valid. -- now apply FLX_double_round_sqrt_hyp. -- now apply generic_format_FLX. -Qed. - -End Double_round_sqrt_FLX. - -Section Double_round_sqrt_FLT. - -Import Fcore_FLX. -Import Fcore_FLT. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FLT_double_round_sqrt_hyp : - (emin <= 0)%Z -> - ((emin' <= emin - prec - 2)%Z - \/ (2 * emin' <= emin - 4 * prec - 2)%Z) -> - (2 * prec + 2 <= prec')%Z -> - double_round_sqrt_hyp (FLT_exp emin prec) (FLT_exp emin' prec'). -Proof. -intros Hemin Heminprec Hprec. -unfold FLT_exp. -unfold Prec_gt_0 in prec_gt_0_. -unfold double_round_sqrt_hyp; split; [|split]; intros ex. -- generalize (Zmax_spec (ex - prec) emin). - generalize (Zmax_spec (2 * ex - prec) emin). - omega. -- generalize (Zmax_spec (ex - prec) emin). - generalize (Zmax_spec (2 * ex - 1 - prec) emin). - omega. -- generalize (Zmax_spec (2 * ex - prec) emin). - generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ex - prec) emin). - omega. -Qed. - -Theorem double_round_sqrt_FLT : - forall choice1 choice2, - (emin <= 0)%Z -> - ((emin' <= emin - prec - 2)%Z - \/ (2 * emin' <= emin - 4 * prec - 2)%Z) -> - (2 * prec + 2 <= prec')%Z -> - forall x, - FLT_format beta emin prec x -> - double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec') - choice1 choice2 (sqrt x). -Proof. -intros choice1 choice2 Hemin Heminprec Hprec x Fx. -apply double_round_sqrt. -- now apply FLT_exp_valid. -- now apply FLT_exp_valid. -- now apply FLT_double_round_sqrt_hyp. -- now apply generic_format_FLT. -Qed. - -End Double_round_sqrt_FLT. - -Section Double_round_sqrt_FTZ. - -Import Fcore_FLX. -Import Fcore_FTZ. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FTZ_double_round_sqrt_hyp : - (2 * (emin' + prec') <= emin + prec <= 1)%Z -> - (2 * prec + 2 <= prec')%Z -> - double_round_sqrt_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec'). -Proof. -intros Hemin Hprec. -unfold FTZ_exp. -unfold Prec_gt_0 in *. -unfold double_round_sqrt_hyp; split; [|split]; intros ex. -- destruct (Z.ltb_spec (ex - prec) emin); - destruct (Z.ltb_spec (2 * ex - prec) emin); - omega. -- destruct (Z.ltb_spec (ex - prec) emin); - destruct (Z.ltb_spec (2 * ex - 1 - prec) emin); - omega. -- intro H. - destruct (Zle_or_lt emin (2 * ex - prec)) as [H'|H']. - + destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ex - prec) emin); - omega. - + casetype False. - rewrite (Zlt_bool_true _ _ H') in H. - omega. -Qed. - -Theorem double_round_sqrt_FTZ : - (4 <= beta)%Z -> - forall choice1 choice2, - (2 * (emin' + prec') <= emin + prec <= 1)%Z -> - (2 * prec + 2 <= prec')%Z -> - forall x, - FTZ_format beta emin prec x -> - double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec') - choice1 choice2 (sqrt x). -Proof. -intros Hbeta choice1 choice2 Hemin Hprec x Fx. -apply double_round_sqrt. -- now apply FTZ_exp_valid. -- now apply FTZ_exp_valid. -- now apply FTZ_double_round_sqrt_hyp. -- now apply generic_format_FTZ. -Qed. - -End Double_round_sqrt_FTZ. - -Section Double_round_sqrt_beta_ge_4. - -Definition double_round_sqrt_beta_ge_4_hyp fexp1 fexp2 := - (forall ex, (2 * fexp1 ex <= fexp1 (2 * ex))%Z) - /\ (forall ex, (2 * fexp1 ex <= fexp1 (2 * ex - 1))%Z) - /\ (forall ex, (fexp1 (2 * ex) < 2 * ex)%Z -> - (fexp2 ex + ex <= 2 * fexp1 ex - 1)%Z). - -Lemma double_round_sqrt_beta_ge_4_aux : - (4 <= beta)%Z -> - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - double_round_sqrt_beta_ge_4_hyp fexp1 fexp2 -> - forall x, - 0 < x -> - (fexp2 (ln_beta (sqrt x)) <= fexp1 (ln_beta (sqrt x)) - 1)%Z -> - generic_format beta fexp1 x -> - / 2 * ulp beta fexp2 (sqrt x) < Rabs (sqrt x - midp fexp1 (sqrt x)). -Proof. -intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx. -set (a := round beta fexp1 Zfloor (sqrt x)). -set (u1 := bpow (fexp1 (ln_beta (sqrt x)))). -set (u2 := bpow (fexp2 (ln_beta (sqrt x)))). -set (b := / 2 * (u1 - u2)). -set (b' := / 2 * (u1 + u2)). -unfold midp; rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, sqrt_lt_R0. -apply Rnot_ge_lt; intro H; apply Rge_le in H. -assert (Fa : generic_format beta fexp1 a). -{ unfold a. - apply generic_format_round. - - exact Vfexp1. - - now apply valid_rnd_DN. } -revert Fa; revert Fx. -unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl. -set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))). -set (ma := Ztrunc (a * bpow (- fexp1 (ln_beta a)))). -intros Fx Fa. -assert (Nna : 0 <= a). -{ rewrite <- (round_0 beta fexp1 Zfloor). - unfold a; apply round_le. - - exact Vfexp1. - - now apply valid_rnd_DN. - - apply sqrt_pos. } -assert (Phu1 : 0 < / 2 * u1). -{ apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]. } -assert (Phu2 : 0 < / 2 * u2). -{ apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]. } -assert (Pb : 0 < b). -{ unfold b. - rewrite <- (Rmult_0_r (/ 2)). - apply Rmult_lt_compat_l; [lra|]. - apply Rlt_Rminus. - unfold u2, u1, ulp, canonic_exp. - apply bpow_lt. - omega. } -assert (Pb' : 0 < b'). -{ now unfold b'; rewrite Rmult_plus_distr_l; apply Rplus_lt_0_compat. } -assert (Hr : sqrt x <= a + b'). -{ unfold b'; apply (Rplus_le_reg_r (- / 2 * u1 - a)); ring_simplify. - replace (_ - _) with (sqrt x - (a + / 2 * u1)) by ring. - now apply Rabs_le_inv. } -assert (Hl : a + b <= sqrt x). -{ unfold b; apply (Rplus_le_reg_r (- / 2 * u1 - a)); ring_simplify. - replace (_ + sqrt _) with (sqrt x - (a + / 2 * u1)) by ring. - rewrite Ropp_mult_distr_l_reverse. - now apply Rabs_le_inv in H; destruct H. } -assert (Hf1 : (2 * fexp1 (ln_beta (sqrt x)) <= fexp1 (ln_beta (x)))%Z); - [destruct (ln_beta_sqrt_disj x Px) as [H'|H']; rewrite H'; apply Hexp|]. -assert (Hlx : (fexp1 (2 * ln_beta (sqrt x)) < 2 * ln_beta (sqrt x))%Z). -{ destruct (ln_beta_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (ln_beta x)); [|omega]. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. - - rewrite <- Hlx. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. } -assert (Hsl : a * a + u1 * a - u2 * a + b * b <= x). -{ replace (_ + _) with ((a + b) * (a + b)); [|now unfold b; field]. - rewrite <- sqrt_def; [|now apply Rlt_le]. - assert (H' : 0 <= a + b); [now apply Rlt_le, Rplus_le_lt_0_compat|]. - now apply Rmult_le_compat. } -assert (Hsr : x <= a * a + u1 * a + u2 * a + b' * b'). -{ replace (_ + _) with ((a + b') * (a + b')); [|now unfold b'; field]. - rewrite <- (sqrt_def x); [|now apply Rlt_le]. - assert (H' : 0 <= sqrt x); [now apply sqrt_pos|]. - now apply Rmult_le_compat. } -destruct (Req_dec a 0) as [Za|Nza]. -- (* a = 0 *) - apply (Rlt_irrefl 0). - apply Rlt_le_trans with (b * b); [now apply Rmult_lt_0_compat|]. - apply Rle_trans with x. - + revert Hsl; unfold Rminus; rewrite Za; do 3 rewrite Rmult_0_r. - now rewrite Ropp_0; do 3 rewrite Rplus_0_l. - + rewrite Fx. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - rewrite Rmult_0_l; bpow_simplify. - unfold mx. - rewrite Ztrunc_floor; - [|now apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0]]. - apply Req_le. - change 0 with (Z2R 0); apply f_equal. - apply Zfloor_imp. - split; [now apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0]|simpl]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - rewrite Rmult_1_l; bpow_simplify. - apply Rlt_le_trans with (bpow (2 * fexp1 (ln_beta (sqrt x)))); - [|now apply bpow_le]. - change 2%Z with (1 + 1)%Z; rewrite Zmult_plus_distr_l; rewrite Zmult_1_l. - rewrite bpow_plus. - rewrite <- (sqrt_def x) at 1; [|now apply Rlt_le]. - assert (sqrt x < bpow (fexp1 (ln_beta (sqrt x)))); - [|now apply Rmult_lt_compat; [apply sqrt_pos|apply sqrt_pos| |]]. - apply (Rle_lt_trans _ _ _ Hr); rewrite Za; rewrite Rplus_0_l. - unfold b'; change (bpow _) with u1. - apply Rlt_le_trans with (/ 2 * (u1 + u1)); [|lra]. - apply Rmult_lt_compat_l; [lra|]; apply Rplus_lt_compat_l. - unfold u2, u1, ulp, canonic_exp; apply bpow_lt; omega. -- (* a <> 0 *) - assert (Pa : 0 < a); [lra|]. - assert (Hla : (ln_beta a = ln_beta (sqrt x) :> Z)). - { unfold a; apply ln_beta_DN. - - exact Vfexp1. - - now fold a. } - assert (Hl' : 0 < - (u2 * a) + b * b). - { apply (Rplus_lt_reg_r (u2 * a)); ring_simplify. - unfold b; ring_simplify. - apply (Rplus_lt_reg_r (/ 2 * u2 * u1)); field_simplify. - replace (_ / 2) with (u2 * (a + / 2 * u1)) by field. - replace (_ / 8) with (/ 4 * (u2 ^ 2 + u1 ^ 2)) by field. - apply Rlt_le_trans with (u2 * bpow (ln_beta (sqrt x))). - - apply Rmult_lt_compat_l; [now unfold u2, ulp; apply bpow_gt_0|]. - unfold u1; rewrite <- Hla. - apply Rlt_le_trans with (a + ulp beta fexp1 a). - + apply Rplus_lt_compat_l. - rewrite <- (Rmult_1_l (ulp _ _ _)). - rewrite ulp_neq_0; trivial. - apply Rmult_lt_compat_r; [apply bpow_gt_0|lra]. - + apply (id_p_ulp_le_bpow _ _ _ _ Pa Fa). - apply Rabs_lt_inv, bpow_ln_beta_gt. - - apply Rle_trans with (bpow (- 1) * u1 ^ 2). - + unfold pow; rewrite Rmult_1_r. - unfold u1, u2, ulp, canonic_exp; bpow_simplify; apply bpow_le. - now apply Hexp. - + apply Rmult_le_compat. - * apply bpow_ge_0. - * apply pow2_ge_0. - * unfold Fcore_Raux.bpow, Z.pow_pos; simpl; rewrite Zmult_1_r. - apply Rinv_le; [lra|]. - now change 4 with (Z2R 4); apply Z2R_le. - * rewrite <- (Rplus_0_l (u1 ^ 2)) at 1; apply Rplus_le_compat_r. - apply pow2_ge_0. } - assert (Hr' : x <= a * a + u1 * a). - { rewrite Hla in Fa. - rewrite <- Rmult_plus_distr_r. - unfold u1, ulp, canonic_exp. - rewrite <- (Rmult_1_l (bpow _)); rewrite Fa; rewrite <- Rmult_plus_distr_r. - rewrite <- Rmult_assoc; rewrite (Rmult_comm _ (Z2R ma)). - rewrite <- (Rmult_assoc (Z2R ma)); bpow_simplify. - apply (Rmult_le_reg_r (bpow (- 2 * fexp1 (ln_beta (sqrt x))))); - [now apply bpow_gt_0|bpow_simplify]. - rewrite Fx at 1; bpow_simplify. - rewrite <- Z2R_Zpower; [|omega]. - change 1 with (Z2R 1); rewrite <- Z2R_plus; do 2 rewrite <- Z2R_mult. - apply Z2R_le, Zlt_succ_le, lt_Z2R. - unfold Z.succ; rewrite Z2R_plus; do 2 rewrite Z2R_mult; rewrite Z2R_plus. - rewrite Z2R_Zpower; [|omega]. - apply (Rmult_lt_reg_r (bpow (2 * fexp1 (ln_beta (sqrt x))))); - [now apply bpow_gt_0|bpow_simplify]. - rewrite <- Fx. - change 2%Z with (1 + 1)%Z; rewrite Zmult_plus_distr_l; rewrite Zmult_1_l. - rewrite bpow_plus; simpl. - replace (_ * _) with (a * a + u1 * a + u1 * u1); - [|unfold u1, ulp, canonic_exp; rewrite Fa; ring]. - apply (Rle_lt_trans _ _ _ Hsr). - rewrite Rplus_assoc; apply Rplus_lt_compat_l. - apply (Rplus_lt_reg_r (- b' * b' + / 2 * u1 * u2)); ring_simplify. - replace (_ + _) with ((a + / 2 * u1) * u2) by ring. - apply Rlt_le_trans with (bpow (ln_beta (sqrt x)) * u2). - - apply Rmult_lt_compat_r; [now unfold u2, ulp; apply bpow_gt_0|]. - apply Rlt_le_trans with (a + u1); [lra|]. - unfold u1; fold (canonic_exp beta fexp1 (sqrt x)). - rewrite <- canonic_exp_DN; [|exact Vfexp1|exact Pa]; fold a. - rewrite <- ulp_neq_0; trivial. - apply id_p_ulp_le_bpow. - + exact Pa. - + now apply round_DN_pt. - + apply Rle_lt_trans with (sqrt x). - * now apply round_DN_pt. - * apply Rabs_lt_inv. - apply bpow_ln_beta_gt. - - apply Rle_trans with (/ 2 * u1 ^ 2). - + apply Rle_trans with (bpow (- 1) * u1 ^ 2). - * unfold pow; rewrite Rmult_1_r. - unfold u2, u1, ulp, canonic_exp. - bpow_simplify. - apply bpow_le. - rewrite Zplus_comm. - now apply Hexp. - * apply Rmult_le_compat_r; [now apply pow2_ge_0|]. - unfold Fcore_Raux.bpow; simpl; unfold Z.pow_pos; simpl. - rewrite Zmult_1_r. - apply Rinv_le; [lra|]. - change 2 with (Z2R 2); apply Z2R_le; omega. - + assert (u2 ^ 2 < u1 ^ 2); [|unfold b'; lra]. - unfold pow; do 2 rewrite Rmult_1_r. - assert (H' : 0 <= u2); [unfold u2, ulp; apply bpow_ge_0|]. - assert (u2 < u1); [|now apply Rmult_lt_compat]. - unfold u1, u2, ulp, canonic_exp; apply bpow_lt; omega. } - apply (Rlt_irrefl (a * a + u1 * a)). - apply Rlt_le_trans with (a * a + u1 * a - u2 * a + b * b). - + rewrite <- (Rplus_0_r (a * a + _)) at 1. - unfold Rminus; rewrite (Rplus_assoc _ _ (b * b)). - now apply Rplus_lt_compat_l. - + now apply Rle_trans with x. -Qed. - -Lemma double_round_sqrt_beta_ge_4 : - (4 <= beta)%Z -> - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_sqrt_beta_ge_4_hyp fexp1 fexp2 -> - forall x, - generic_format beta fexp1 x -> - double_round_eq fexp1 fexp2 choice1 choice2 (sqrt x). -Proof. -intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x Fx. -unfold double_round_eq. -destruct (Rle_or_lt x 0) as [Npx|Px]. -- (* x <= 0 *) - assert (Hs : sqrt x = 0). - { destruct (Req_dec x 0) as [Zx|Nzx]. - - (* x = 0 *) - rewrite Zx. - exact sqrt_0. - - (* x < 0 *) - unfold sqrt. - destruct Rcase_abs. - + reflexivity. - + casetype False; lra. } - rewrite Hs. - rewrite round_0. - + reflexivity. - + now apply valid_rnd_N. -- (* 0 < x *) - assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); - [now apply ln_beta_generic_gt; try assumption; lra|]. - assert (Hfsx : (fexp1 (ln_beta (sqrt x)) < ln_beta (sqrt x))%Z). - { destruct (Rle_or_lt x 1) as [Hx|Hx]. - - (* x <= 1 *) - apply (valid_exp_large fexp1 (ln_beta x)); [exact Hfx|]. - apply ln_beta_le; [exact Px|]. - rewrite <- (sqrt_def x) at 1; [|lra]. - rewrite <- Rmult_1_r. - apply Rmult_le_compat_l. - + apply sqrt_pos. - + rewrite <- sqrt_1. - now apply sqrt_le_1_alt. - - (* 1 < x *) - generalize ((proj1 (proj2 Hexp)) 1%Z). - replace (_ - 1)%Z with 1%Z by ring. - intro Hexp10. - assert (Hf0 : (fexp1 1 < 1)%Z); [omega|clear Hexp10]. - apply (valid_exp_large fexp1 1); [exact Hf0|]. - apply ln_beta_ge_bpow. - rewrite Zeq_minus; [|reflexivity]. - unfold Fcore_Raux.bpow; simpl. - apply Rabs_ge; right. - rewrite <- sqrt_1. - apply sqrt_le_1_alt. - now apply Rlt_le. } - assert (Hf2 : (fexp2 (ln_beta (sqrt x)) <= fexp1 (ln_beta (sqrt x)) - 1)%Z). - { assert (H : (fexp1 (2 * ln_beta (sqrt x)) < 2 * ln_beta (sqrt x))%Z). - { destruct (ln_beta_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (ln_beta x)); [|omega]. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. - - rewrite <- Hlx. - now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]. } - generalize ((proj2 (proj2 Hexp)) (ln_beta (sqrt x)) H). - omega. } - apply double_round_mid_cases. - + exact Vfexp1. - + exact Vfexp2. - + now apply sqrt_lt_R0. - + omega. - + omega. - + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid). - apply (double_round_sqrt_beta_ge_4_aux Hbeta fexp1 fexp2 Vfexp1 Vfexp2 - Hexp x Px Hf2 Fx). -Qed. - -Section Double_round_sqrt_beta_ge_4_FLX. - -Import Fcore_FLX. - -Variable prec : Z. -Variable prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FLX_double_round_sqrt_beta_ge_4_hyp : - (2 * prec + 1 <= prec')%Z -> - double_round_sqrt_beta_ge_4_hyp (FLX_exp prec) (FLX_exp prec'). -Proof. -intros Hprec. -unfold FLX_exp. -unfold Prec_gt_0 in prec_gt_0_. -unfold double_round_sqrt_beta_ge_4_hyp; split; [|split]; intro ex; omega. -Qed. - -Theorem double_round_sqrt_beta_ge_4_FLX : - (4 <= beta)%Z -> - forall choice1 choice2, - (2 * prec + 1 <= prec')%Z -> - forall x, - FLX_format beta prec x -> - double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (sqrt x). -Proof. -intros Hbeta choice1 choice2 Hprec x Fx. -apply double_round_sqrt_beta_ge_4. -- exact Hbeta. -- now apply FLX_exp_valid. -- now apply FLX_exp_valid. -- now apply FLX_double_round_sqrt_beta_ge_4_hyp. -- now apply generic_format_FLX. -Qed. - -End Double_round_sqrt_beta_ge_4_FLX. - -Section Double_round_sqrt_beta_ge_4_FLT. - -Import Fcore_FLX. -Import Fcore_FLT. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FLT_double_round_sqrt_beta_ge_4_hyp : - (emin <= 0)%Z -> - ((emin' <= emin - prec - 1)%Z - \/ (2 * emin' <= emin - 4 * prec)%Z) -> - (2 * prec + 1 <= prec')%Z -> - double_round_sqrt_beta_ge_4_hyp (FLT_exp emin prec) (FLT_exp emin' prec'). -Proof. -intros Hemin Heminprec Hprec. -unfold FLT_exp. -unfold Prec_gt_0 in prec_gt_0_. -unfold double_round_sqrt_beta_ge_4_hyp; split; [|split]; intros ex. -- generalize (Zmax_spec (ex - prec) emin). - generalize (Zmax_spec (2 * ex - prec) emin). - omega. -- generalize (Zmax_spec (ex - prec) emin). - generalize (Zmax_spec (2 * ex - 1 - prec) emin). - omega. -- generalize (Zmax_spec (2 * ex - prec) emin). - generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ex - prec) emin). - omega. -Qed. - -Theorem double_round_sqrt_beta_ge_4_FLT : - (4 <= beta)%Z -> - forall choice1 choice2, - (emin <= 0)%Z -> - ((emin' <= emin - prec - 1)%Z - \/ (2 * emin' <= emin - 4 * prec)%Z) -> - (2 * prec + 1 <= prec')%Z -> - forall x, - FLT_format beta emin prec x -> - double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec') - choice1 choice2 (sqrt x). -Proof. -intros Hbeta choice1 choice2 Hemin Heminprec Hprec x Fx. -apply double_round_sqrt_beta_ge_4. -- exact Hbeta. -- now apply FLT_exp_valid. -- now apply FLT_exp_valid. -- now apply FLT_double_round_sqrt_beta_ge_4_hyp. -- now apply generic_format_FLT. -Qed. - -End Double_round_sqrt_beta_ge_4_FLT. - -Section Double_round_sqrt_beta_ge_4_FTZ. - -Import Fcore_FLX. -Import Fcore_FTZ. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FTZ_double_round_sqrt_beta_ge_4_hyp : - (2 * (emin' + prec') <= emin + prec <= 1)%Z -> - (2 * prec + 1 <= prec')%Z -> - double_round_sqrt_beta_ge_4_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec'). -Proof. -intros Hemin Hprec. -unfold FTZ_exp. -unfold Prec_gt_0 in *. -unfold double_round_sqrt_beta_ge_4_hyp; split; [|split]; intros ex. -- destruct (Z.ltb_spec (ex - prec) emin); - destruct (Z.ltb_spec (2 * ex - prec) emin); - omega. -- destruct (Z.ltb_spec (ex - prec) emin); - destruct (Z.ltb_spec (2 * ex - 1 - prec) emin); - omega. -- intro H. - destruct (Zle_or_lt emin (2 * ex - prec)) as [H'|H']. - + destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ex - prec) emin); - omega. - + casetype False. - rewrite (Zlt_bool_true _ _ H') in H. - omega. -Qed. - -Theorem double_round_sqrt_beta_ge_4_FTZ : - (4 <= beta)%Z -> - forall choice1 choice2, - (2 * (emin' + prec') <= emin + prec <= 1)%Z -> - (2 * prec + 1 <= prec')%Z -> - forall x, - FTZ_format beta emin prec x -> - double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec') - choice1 choice2 (sqrt x). -Proof. -intros Hbeta choice1 choice2 Hemin Hprec x Fx. -apply double_round_sqrt_beta_ge_4. -- exact Hbeta. -- now apply FTZ_exp_valid. -- now apply FTZ_exp_valid. -- now apply FTZ_double_round_sqrt_beta_ge_4_hyp. -- now apply generic_format_FTZ. -Qed. - -End Double_round_sqrt_beta_ge_4_FTZ. - -End Double_round_sqrt_beta_ge_4. - -End Double_round_sqrt. - -Section Double_round_div. - -Lemma double_round_eq_mid_beta_even : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - (exists n, (beta = 2 * n :> Z)%Z) -> - forall x, - 0 < x -> - (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z -> - (fexp1 (ln_beta x) <= ln_beta x)%Z -> - x = midp fexp1 x -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Ebeta x Px Hf2 Hf1. -unfold double_round_eq. -unfold midp. -set (rd := round beta fexp1 Zfloor x). -set (u := ulp beta fexp1 x). -intro H; apply (Rplus_eq_compat_l (- rd)) in H. -ring_simplify in H; revert H. -rewrite Rplus_comm; fold (Rminus x rd). -intro Xmid. -destruct Ebeta as (n,Ebeta). -assert (Hbeta : (2 <= beta)%Z). -{ destruct beta as (beta_val,beta_prop). - now apply Zle_bool_imp_le. } -apply (Rplus_eq_compat_l rd) in Xmid; ring_simplify in Xmid. -rewrite (round_generic beta fexp2); [reflexivity|now apply valid_rnd_N|]. -set (f := Float beta (Zfloor (scaled_mantissa beta fexp2 rd) - + n * beta ^ (fexp1 (ln_beta x) - 1 - - fexp2 (ln_beta x))) - (canonic_exp beta fexp2 x)). -assert (Hf : F2R f = x). -{ unfold f, F2R; simpl. - rewrite Z2R_plus. - rewrite Rmult_plus_distr_r. - rewrite Z2R_mult. - rewrite Z2R_Zpower; [|omega]. - unfold canonic_exp at 2; bpow_simplify. - unfold Zminus; rewrite bpow_plus. - rewrite (Rmult_comm _ (bpow (- 1))). - rewrite <- (Rmult_assoc (Z2R n)). - change (bpow (- 1)) with (/ Z2R (beta * 1)). - rewrite Zmult_1_r. - rewrite Ebeta. - rewrite (Z2R_mult 2). - rewrite Rinv_mult_distr; - [|simpl; lra|change 0 with (Z2R 0); apply Z2R_neq; omega]. - rewrite <- Rmult_assoc; rewrite (Rmult_comm (Z2R n)); - rewrite (Rmult_assoc _ (Z2R n)). - rewrite Rinv_r; - [rewrite Rmult_1_r|change 0 with (Z2R 0); apply Z2R_neq; omega]. - simpl; fold (canonic_exp beta fexp1 x). - rewrite <- 2!ulp_neq_0; try now apply Rgt_not_eq. - fold u; rewrite Xmid at 2. - apply f_equal2; [|reflexivity]. - rewrite ulp_neq_0; try now apply Rgt_not_eq. - destruct (Req_dec rd 0) as [Zrd|Nzrd]. - - (* rd = 0 *) - rewrite Zrd. - rewrite scaled_mantissa_0. - change 0 with (Z2R 0) at 1; rewrite Zfloor_Z2R. - now rewrite Rmult_0_l. - - (* rd <> 0 *) - assert (Nnrd : 0 <= rd). - { apply round_DN_pt. - - exact Vfexp1. - - apply generic_format_0. - - now apply Rlt_le. } - assert (Prd : 0 < rd); [lra|]. - assert (Lrd : (ln_beta rd = ln_beta x :> Z)). - { apply Zle_antisym. - - apply ln_beta_le; [exact Prd|]. - now apply round_DN_pt. - - apply ln_beta_round_ge. - + exact Vfexp1. - + now apply valid_rnd_DN. - + exact Nzrd. } - unfold scaled_mantissa. - unfold rd at 1. - unfold round, F2R, scaled_mantissa, canonic_exp; simpl. - bpow_simplify. - rewrite Lrd. - rewrite <- (Z2R_Zpower _ (_ - _)); [|omega]. - rewrite <- Z2R_mult. - rewrite (Zfloor_imp (Zfloor (x * bpow (- fexp1 (ln_beta x))) * - beta ^ (fexp1 (ln_beta x) - fexp2 (ln_beta x)))). - + rewrite Z2R_mult. - rewrite Z2R_Zpower; [|omega]. - bpow_simplify. - now unfold rd. - + split; [now apply Rle_refl|]. - rewrite Z2R_plus. - simpl; lra. } -apply (generic_format_F2R' _ _ x f Hf). -intros _. -apply Zle_refl. -Qed. - -Lemma double_round_really_zero : - forall (fexp1 fexp2 : Z -> Z), - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (ln_beta x <= fexp1 (ln_beta x) - 2)%Z -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf1. -assert (Hlx : bpow (ln_beta x - 1) <= x < bpow (ln_beta x)). -{ destruct (ln_beta x) as (ex,Hex); simpl. - rewrite <- (Rabs_right x); [|now apply Rle_ge; apply Rlt_le]. - apply Hex. - now apply Rgt_not_eq. } -unfold double_round_eq. -rewrite (round_N_really_small_pos beta fexp1 _ x (ln_beta x)); [|exact Hlx|omega]. -set (x'' := round beta fexp2 (Znearest choice2) x). -destruct (Req_dec x'' 0) as [Zx''|Nzx'']; - [now rewrite Zx''; rewrite round_0; [|apply valid_rnd_N]|]. -destruct (Zle_or_lt (fexp2 (ln_beta x)) (ln_beta x)). -- (* fexp2 (ln_beta x) <= ln_beta x *) - destruct (Rlt_or_le x'' (bpow (ln_beta x))). - + (* x'' < bpow (ln_beta x) *) - rewrite (round_N_really_small_pos beta fexp1 _ _ (ln_beta x)); - [reflexivity|split; [|exact H0]|omega]. - apply round_large_pos_ge_pow; [now apply valid_rnd_N| |now apply Hlx]. - fold x''; assert (0 <= x''); [|lra]; unfold x''. - rewrite <- (round_0 beta fexp2 (Znearest choice2)). - now apply round_le; [|apply valid_rnd_N|apply Rlt_le]. - + (* bpow (ln_beta x) <= x'' *) - assert (Hx'' : x'' = bpow (ln_beta x)). - { apply Rle_antisym; [|exact H0]. - rewrite <- (round_generic beta fexp2 (Znearest choice2) (bpow _)). - - now apply round_le; [|apply valid_rnd_N|apply Rlt_le]. - - now apply generic_format_bpow'. } - rewrite Hx''. - unfold round, F2R, scaled_mantissa, canonic_exp; simpl. - rewrite ln_beta_bpow. - assert (Hf11 : (fexp1 (ln_beta x + 1) = fexp1 (ln_beta x) :> Z)%Z); - [apply Vfexp1; omega|]. - rewrite Hf11. - apply (Rmult_eq_reg_r (bpow (- fexp1 (ln_beta x)))); - [|now apply Rgt_not_eq; apply bpow_gt_0]. - rewrite Rmult_0_l; bpow_simplify. - change 0 with (Z2R 0); apply f_equal. - apply Znearest_imp. - simpl; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. - rewrite Rabs_right; [|now apply Rle_ge; apply bpow_ge_0]. - apply Rle_lt_trans with (bpow (- 2)); [now apply bpow_le; omega|]. - unfold Fcore_Raux.bpow, Z.pow_pos; simpl; rewrite Zmult_1_r. - assert (Hbeta : (2 <= beta)%Z). - { destruct beta as (beta_val,beta_prop); simpl. - now apply Zle_bool_imp_le. } - apply Rinv_lt_contravar. - * apply Rmult_lt_0_compat; [lra|]. - rewrite Z2R_mult; apply Rmult_lt_0_compat; change 0 with (Z2R 0); - apply Z2R_lt; omega. - * change 2 with (Z2R 2); apply Z2R_lt. - apply (Zle_lt_trans _ _ _ Hbeta). - rewrite <- (Zmult_1_r beta) at 1. - apply Zmult_lt_compat_l; omega. -- (* ln_beta x < fexp2 (ln_beta x) *) - casetype False; apply Nzx''. - now apply (round_N_really_small_pos beta _ _ _ (ln_beta x)). -Qed. - -Lemma double_round_zero : - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp1 (ln_beta x) = ln_beta x + 1 :> Z)%Z -> - x < bpow (ln_beta x) - / 2 * ulp beta fexp2 x -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf1. -unfold double_round_eq. -set (x'' := round beta fexp2 (Znearest choice2) x). -set (u1 := ulp beta fexp1 x). -set (u2 := ulp beta fexp2 x). -intro Hx. -assert (Hlx : bpow (ln_beta x - 1) <= x < bpow (ln_beta x)). -{ destruct (ln_beta x) as (ex,Hex); simpl. - rewrite <- (Rabs_right x); [|now apply Rle_ge; apply Rlt_le]. - apply Hex. - now apply Rgt_not_eq. } -rewrite (round_N_really_small_pos beta fexp1 choice1 x (ln_beta x)); - [|exact Hlx|omega]. -destruct (Req_dec x'' 0) as [Zx''|Nzx'']; - [now rewrite Zx''; rewrite round_0; [reflexivity|apply valid_rnd_N]|]. -rewrite (round_N_really_small_pos beta _ _ x'' (ln_beta x)); - [reflexivity| |omega]. -split. -- apply round_large_pos_ge_pow. - + now apply valid_rnd_N. - + assert (0 <= x''); [|now fold x''; lra]. - rewrite <- (round_0 beta fexp2 (Znearest choice2)). - now apply round_le; [|apply valid_rnd_N|apply Rlt_le]. - + apply Rle_trans with (Rabs x); - [|now rewrite Rabs_right; [apply Rle_refl|apply Rle_ge; apply Rlt_le]]. - destruct (ln_beta x) as (ex,Hex); simpl; apply Hex. - now apply Rgt_not_eq. -- replace x'' with (x + (x'' - x)) by ring. - replace (bpow _) with (bpow (ln_beta x) - / 2 * u2 + / 2 * u2) by ring. - apply Rplus_lt_le_compat; [exact Hx|]. - apply Rabs_le_inv. - now apply error_le_half_ulp. -Qed. - -Lemma double_round_all_mid_cases : - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - forall x, - 0 < x -> - (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z -> - ((fexp1 (ln_beta x) = ln_beta x + 1 :> Z)%Z -> - bpow (ln_beta x) - / 2 * ulp beta fexp2 x <= x -> - double_round_eq fexp1 fexp2 choice1 choice2 x) -> - ((fexp1 (ln_beta x) <= ln_beta x)%Z -> - midp fexp1 x - / 2 * ulp beta fexp2 x <= x < midp fexp1 x -> - double_round_eq fexp1 fexp2 choice1 choice2 x) -> - ((fexp1 (ln_beta x) <= ln_beta x)%Z -> - x = midp fexp1 x -> - double_round_eq fexp1 fexp2 choice1 choice2 x) -> - ((fexp1 (ln_beta x) <= ln_beta x)%Z -> - midp fexp1 x < x <= midp fexp1 x + / 2 * ulp beta fexp2 x -> - double_round_eq fexp1 fexp2 choice1 choice2 x) -> - double_round_eq fexp1 fexp2 choice1 choice2 x. -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2. -set (x' := round beta fexp1 Zfloor x). -set (u1 := ulp beta fexp1 x). -set (u2 := ulp beta fexp2 x). -intros Cz Clt Ceq Cgt. -destruct (Ztrichotomy (ln_beta x) (fexp1 (ln_beta x) - 1)) as [Hlt|[Heq|Hgt]]. -- (* ln_beta x < fexp1 (ln_beta x) - 1 *) - assert (H : (ln_beta x <= fexp1 (ln_beta x) - 2)%Z) by omega. - now apply double_round_really_zero. -- (* ln_beta x = fexp1 (ln_beta x) - 1 *) - assert (H : (fexp1 (ln_beta x) = (ln_beta x + 1))%Z) by omega. - destruct (Rlt_or_le x (bpow (ln_beta x) - / 2 * u2)) as [Hlt'|Hge']. - + now apply double_round_zero. - + now apply Cz. -- (* ln_beta x > fexp1 (ln_beta x) - 1 *) - assert (H : (fexp1 (ln_beta x) <= ln_beta x)%Z) by omega. - destruct (Rtotal_order x (midp fexp1 x)) as [Hlt'|[Heq'|Hgt']]. - + (* x < midp fexp1 x *) - destruct (Rlt_or_le x (midp fexp1 x - / 2 * u2)) as [Hlt''|Hle'']. - * now apply double_round_lt_mid_further_place; [| | |omega| |]. - * now apply Clt; [|split]. - + (* x = midp fexp1 x *) - now apply Ceq. - + (* x > midp fexp1 x *) - destruct (Rle_or_lt x (midp fexp1 x + / 2 * u2)) as [Hlt''|Hle'']. - * now apply Cgt; [|split]. - * { destruct (generic_format_EM beta fexp1 x) as [Fx|Nfx]. - - (* generic_format beta fexp1 x *) - unfold double_round_eq; rewrite (round_generic beta fexp2); - [reflexivity|now apply valid_rnd_N|]. - now apply (generic_inclusion_ln_beta beta fexp1); [omega|]. - - (* ~ generic_format beta fexp1 x *) - assert (Hceil : round beta fexp1 Zceil x = x' + u1); - [now apply round_UP_DN_ulp|]. - assert (Hf2' : (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z); - [omega|]. - assert (midp' fexp1 x + / 2 * ulp beta fexp2 x < x); - [|now apply double_round_gt_mid_further_place]. - revert Hle''; unfold midp, midp'; fold x'. - rewrite Hceil; fold u1; fold u2. - lra. } -Qed. - -Lemma ln_beta_div_disj : - forall x y : R, - 0 < x -> 0 < y -> - ((ln_beta (x / y) = ln_beta x - ln_beta y :> Z)%Z - \/ (ln_beta (x / y) = ln_beta x - ln_beta y + 1 :> Z)%Z). -Proof. -intros x y Px Py. -generalize (ln_beta_div beta x y Px Py). -omega. -Qed. - -Definition double_round_div_hyp fexp1 fexp2 := - (forall ex, (fexp2 ex <= fexp1 ex - 1)%Z) - /\ (forall ex ey, (fexp1 ex < ex)%Z -> (fexp1 ey < ey)%Z -> - (fexp1 (ex - ey) <= ex - ey + 1)%Z -> - (fexp2 (ex - ey) <= fexp1 ex - ey)%Z) - /\ (forall ex ey, (fexp1 ex < ex)%Z -> (fexp1 ey < ey)%Z -> - (fexp1 (ex - ey + 1) <= ex - ey + 1 + 1)%Z -> - (fexp2 (ex - ey + 1) <= fexp1 ex - ey)%Z) - /\ (forall ex ey, (fexp1 ex < ex)%Z -> (fexp1 ey < ey)%Z -> - (fexp1 (ex - ey) <= ex - ey)%Z -> - (fexp2 (ex - ey) <= fexp1 (ex - ey) - + fexp1 ey - ey)%Z) - /\ (forall ex ey, (fexp1 ex < ex)%Z -> (fexp1 ey < ey)%Z -> - (fexp1 (ex - ey) = ex - ey + 1)%Z -> - (fexp2 (ex - ey) <= ex - ey - ey + fexp1 ey)%Z). - -Lemma double_round_div_aux0 : - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_div_hyp fexp1 fexp2 -> - forall x y, - 0 < x -> 0 < y -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - fexp1 (ln_beta (x / y)) = (ln_beta (x / y) + 1)%Z -> - ~ (bpow (ln_beta (x / y)) - / 2 * ulp beta fexp2 (x / y) <= x / y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Fx Fy Hf1. -assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -assert (Hfy : (fexp1 (ln_beta y) < ln_beta y)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -set (p := bpow (ln_beta (x / y))). -set (u2 := bpow (fexp2 (ln_beta (x / y)))). -revert Fx Fy. -unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl. -set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))). -set (my := Ztrunc (y * bpow (- fexp1 (ln_beta y)))). -intros Fx Fy. -rewrite ulp_neq_0. -2: apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac]. -2: now apply Rinv_neq_0_compat, Rgt_not_eq. -intro Hl. -assert (Hr : x / y < p); - [now apply Rabs_lt_inv; apply bpow_ln_beta_gt|]. -apply (Rlt_irrefl (p - / 2 * u2)). -apply (Rle_lt_trans _ _ _ Hl). -apply (Rmult_lt_reg_r y _ _ Py). -unfold Rdiv; rewrite Rmult_assoc. -rewrite Rinv_l; [|now apply Rgt_not_eq]; rewrite Rmult_1_r. -destruct (Zle_or_lt Z0 (fexp1 (ln_beta x) - ln_beta (x / y) - - fexp1 (ln_beta y))%Z) as [He|He]. -- (* ln_beta (x / y) + fexp1 (ln_beta y) <= fexp1 (ln_beta x) *) - apply Rle_lt_trans with (p * y - p * bpow (fexp1 (ln_beta y))). - + rewrite Fx; rewrite Fy at 1. - rewrite <- Rmult_assoc. - rewrite (Rmult_comm p). - unfold p; bpow_simplify. - apply (Rmult_le_reg_r (bpow (- ln_beta (x / y) - fexp1 (ln_beta y)))); - [now apply bpow_gt_0|]. - rewrite Rmult_minus_distr_r. - bpow_simplify. - rewrite <- Z2R_Zpower; [|exact He]. - rewrite <- Z2R_mult. - change 1 with (Z2R 1); rewrite <- Z2R_minus. - apply Z2R_le. - apply (Zplus_le_reg_r _ _ 1); ring_simplify. - apply Zlt_le_succ. - apply lt_Z2R. - rewrite Z2R_mult. - rewrite Z2R_Zpower; [|exact He]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta y) + ln_beta (x / y)))); - [now apply bpow_gt_0|]. - bpow_simplify. - rewrite <- Fx. - rewrite bpow_plus. - rewrite <- Rmult_assoc; rewrite <- Fy. - fold p. - apply (Rmult_lt_reg_r (/ y)); [now apply Rinv_0_lt_compat|]. - field_simplify; lra. - + rewrite Rmult_minus_distr_r. - unfold Rminus; apply Rplus_lt_compat_l. - apply Ropp_lt_contravar. - apply Rlt_le_trans with (u2 * bpow (ln_beta y)). - * rewrite <- (Rmult_1_l (u2 * _)). - rewrite Rmult_assoc. - { apply Rmult_lt_compat. - - lra. - - now apply Rmult_le_pos; [apply bpow_ge_0|apply Rlt_le]. - - lra. - - apply Rmult_lt_compat_l; [now apply bpow_gt_0|]. - apply Rabs_lt_inv. - apply bpow_ln_beta_gt. } - * unfold u2, p, ulp, canonic_exp; bpow_simplify; apply bpow_le. - apply (Zplus_le_reg_r _ _ (- ln_beta y)); ring_simplify. - rewrite (Zplus_comm (- _)); fold (Zminus (ln_beta (x / y)) (ln_beta y)). - destruct (ln_beta_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; - [now apply Hexp; [| |rewrite <- Hxy]|]. - replace (_ - _ + 1)%Z with ((ln_beta x + 1) - ln_beta y)%Z by ring. - apply Hexp. - { now assert (fexp1 (ln_beta x + 1) <= ln_beta x)%Z; - [apply valid_exp|omega]. } - { assumption. } - replace (_ + 1 - _)%Z with (ln_beta x - ln_beta y + 1)%Z by ring. - now rewrite <- Hxy. -- (* fexp1 (ln_beta x) < ln_beta (x / y) + fexp1 (ln_beta y) *) - apply Rle_lt_trans with (p * y - bpow (fexp1 (ln_beta x))). - + rewrite Fx at 1; rewrite Fy at 1. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - rewrite Rmult_minus_distr_r. - bpow_simplify. - rewrite (Rmult_comm p). - unfold p; bpow_simplify. - rewrite <- Z2R_Zpower; [|omega]. - rewrite <- Z2R_mult. - change 1 with (Z2R 1); rewrite <- Z2R_minus. - apply Z2R_le. - apply (Zplus_le_reg_r _ _ 1); ring_simplify. - apply Zlt_le_succ. - apply lt_Z2R. - rewrite Z2R_mult. - rewrite Z2R_Zpower; [|omega]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); - [now apply bpow_gt_0|bpow_simplify]. - rewrite <- Fx. - rewrite Zplus_comm; rewrite bpow_plus. - rewrite <- Rmult_assoc; rewrite <- Fy. - fold p. - apply (Rmult_lt_reg_r (/ y)); [now apply Rinv_0_lt_compat|]. - field_simplify; lra. - + rewrite Rmult_minus_distr_r. - unfold Rminus; apply Rplus_lt_compat_l. - apply Ropp_lt_contravar. - apply Rlt_le_trans with (u2 * bpow (ln_beta y)). - * rewrite <- (Rmult_1_l (u2 * _)). - rewrite Rmult_assoc. - { apply Rmult_lt_compat. - - lra. - - now apply Rmult_le_pos; [apply bpow_ge_0|apply Rlt_le]. - - lra. - - apply Rmult_lt_compat_l; [now apply bpow_gt_0|]. - apply Rabs_lt_inv. - apply bpow_ln_beta_gt. } - * unfold u2, p, ulp, canonic_exp; bpow_simplify; apply bpow_le. - apply (Zplus_le_reg_r _ _ (- ln_beta y)); ring_simplify. - rewrite (Zplus_comm (- _)); fold (Zminus (ln_beta (x / y)) (ln_beta y)). - destruct (ln_beta_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; - apply Hexp; try assumption; rewrite <- Hxy; rewrite Hf1; apply Zle_refl. -Qed. - -Lemma double_round_div_aux1 : - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_div_hyp fexp1 fexp2 -> - forall x y, - 0 < x -> 0 < y -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - (fexp1 (ln_beta (x / y)) <= ln_beta (x / y))%Z -> - ~ (midp fexp1 (x / y) - / 2 * ulp beta fexp2 (x / y) - <= x / y - < midp fexp1 (x / y)). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Fx Fy Hf1. -assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -assert (Hfy : (fexp1 (ln_beta y) < ln_beta y)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -assert (S : (x / y <> 0)%R). -apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac]. -now apply Rinv_neq_0_compat, Rgt_not_eq. -cut (~ (/ 2 * (ulp beta fexp1 (x / y) - ulp beta fexp2 (x / y)) - <= x / y - round beta fexp1 Zfloor (x / y) - < / 2 * ulp beta fexp1 (x / y))). -{ intro H; intro H'; apply H; split. - - apply (Rplus_le_reg_l (round beta fexp1 Zfloor (x / y))). - ring_simplify. - apply H'. - - apply (Rplus_lt_reg_l (round beta fexp1 Zfloor (x / y))). - ring_simplify. - apply H'. } -set (u1 := bpow (fexp1 (ln_beta (x / y)))). -set (u2 := bpow (fexp2 (ln_beta (x / y)))). -set (x' := round beta fexp1 Zfloor (x / y)). -rewrite 2!ulp_neq_0; trivial. -revert Fx Fy. -unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl. -set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))). -set (my := Ztrunc (y * bpow (- fexp1 (ln_beta y)))). -intros Fx Fy. -intro Hlr. -apply (Rlt_irrefl (/ 2 * (u1 - u2))). -apply (Rle_lt_trans _ _ _ (proj1 Hlr)). -apply (Rplus_lt_reg_r x'); ring_simplify. -apply (Rmult_lt_reg_r y _ _ Py). -unfold Rdiv; rewrite Rmult_assoc. -rewrite Rinv_l; [|now apply Rgt_not_eq]; rewrite Rmult_1_r. -rewrite Rmult_minus_distr_r; rewrite Rmult_plus_distr_r. -apply (Rmult_lt_reg_l 2); [lra|]. -rewrite Rmult_minus_distr_l; rewrite Rmult_plus_distr_l. -do 5 rewrite <- Rmult_assoc. -rewrite Rinv_r; [|lra]; do 2 rewrite Rmult_1_l. -destruct (Zle_or_lt Z0 (fexp1 (ln_beta x) - fexp1 (ln_beta (x / y)) - - fexp1 (ln_beta y))%Z) as [He|He]. -- (* fexp1 (ln_beta (x / y)) + fexp1 (ln_beta y)) <= fexp1 (ln_beta x) *) - apply Rle_lt_trans with (2 * x' * y + u1 * y - - bpow (fexp1 (ln_beta (x / y)) - + fexp1 (ln_beta y))). - + rewrite Fx at 1; rewrite Fy at 1 2. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta (x / y)) - - fexp1 (ln_beta y)))); - [now apply bpow_gt_0|]. - rewrite Rmult_minus_distr_r; rewrite (Rmult_plus_distr_r (_ * _ * _)). - bpow_simplify. - replace (2 * x' * _ * _) - with (2 * Z2R my * x' * bpow (- fexp1 (ln_beta (x / y)))) by ring. - rewrite (Rmult_comm u1). - unfold x', u1, round, F2R, ulp, scaled_mantissa, canonic_exp; simpl. - bpow_simplify. - rewrite <- Z2R_Zpower; [|exact He]. - change 2 with (Z2R 2). - do 4 rewrite <- Z2R_mult. - rewrite <- Z2R_plus. - change 1 with (Z2R 1); rewrite <- Z2R_minus. - apply Z2R_le. - apply (Zplus_le_reg_r _ _ 1); ring_simplify. - apply Zlt_le_succ. - apply lt_Z2R. - rewrite Z2R_plus. - do 4 rewrite Z2R_mult; simpl. - rewrite Z2R_Zpower; [|exact He]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta (x / y)) - + fexp1 (ln_beta y)))); - [now apply bpow_gt_0|bpow_simplify]. - rewrite Rmult_assoc. - rewrite <- Fx. - rewrite (Rmult_plus_distr_r _ _ (Fcore_Raux.bpow _ _)). - rewrite Rmult_assoc. - rewrite bpow_plus. - rewrite <- (Rmult_assoc (Z2R (Zfloor _))). - change (Z2R (Zfloor _) * _) with x'. - do 2 rewrite (Rmult_comm _ (bpow (fexp1 (ln_beta y)))). - rewrite Rmult_assoc. - do 2 rewrite <- (Rmult_assoc (Z2R my)). - rewrite <- Fy. - change (bpow _) with u1. - apply (Rmult_lt_reg_l (/ 2)); [lra|]. - rewrite Rmult_plus_distr_l. - do 4 rewrite <- Rmult_assoc. - rewrite Rinv_l; [|lra]; do 2 rewrite Rmult_1_l. - apply (Rplus_lt_reg_r (- y * x')); ring_simplify. - apply (Rmult_lt_reg_l (/ y)); [now apply Rinv_0_lt_compat|]. - rewrite Rmult_minus_distr_l. - do 3 rewrite <- Rmult_assoc. - rewrite Rinv_l; [|now apply Rgt_not_eq]; do 2 rewrite Rmult_1_l. - now rewrite Rmult_comm. - + apply Rplus_lt_compat_l. - apply Ropp_lt_contravar. - apply Rlt_le_trans with (u2 * bpow (ln_beta y)). - * { apply Rmult_lt_compat_l. - - apply bpow_gt_0. - - apply Rabs_lt_inv. - apply bpow_ln_beta_gt. } - * unfold u2, ulp, canonic_exp; bpow_simplify; apply bpow_le. - apply (Zplus_le_reg_r _ _ (- ln_beta y)); ring_simplify. - rewrite <- Zplus_assoc; rewrite (Zplus_comm (- _)). - destruct (ln_beta_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; - [now apply Hexp; [| |rewrite <- Hxy]|]. - replace (_ - _ + 1)%Z with ((ln_beta x + 1) - ln_beta y)%Z by ring. - apply Hexp. - { now assert (fexp1 (ln_beta x + 1) <= ln_beta x)%Z; - [apply valid_exp|omega]. } - { assumption. } - replace (_ + 1 - _)%Z with (ln_beta x - ln_beta y + 1)%Z by ring. - now rewrite <- Hxy. -- (* fexp1 (ln_beta x) < fexp1 (ln_beta (x / y)) + fexp1 (ln_beta y) *) - apply Rle_lt_trans with (2 * x' * y + u1 * y - bpow (fexp1 (ln_beta x))). - + rewrite Fx at 1; rewrite Fy at 1 2. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - rewrite Rmult_minus_distr_r; rewrite (Rmult_plus_distr_r (_ * _ * _)). - bpow_simplify. - replace (2 * x' * _ * _) - with (2 * Z2R my * x' * bpow (fexp1 (ln_beta y) - fexp1 (ln_beta x))) by ring. - rewrite (Rmult_comm u1). - unfold x', u1, round, F2R, ulp, scaled_mantissa, canonic_exp; simpl. - bpow_simplify. - rewrite <- (Z2R_Zpower _ (_ - _)%Z); [|omega]. - change 2 with (Z2R 2). - do 5 rewrite <- Z2R_mult. - rewrite <- Z2R_plus. - change 1 with (Z2R 1); rewrite <- Z2R_minus. - apply Z2R_le. - apply (Zplus_le_reg_r _ _ 1); ring_simplify. - apply Zlt_le_succ. - apply lt_Z2R. - rewrite Z2R_plus. - do 5 rewrite Z2R_mult; simpl. - rewrite Z2R_Zpower; [|omega]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - rewrite Rmult_assoc. - rewrite <- Fx. - rewrite (Rmult_plus_distr_r _ _ (Fcore_Raux.bpow _ _)). - bpow_simplify. - rewrite Rmult_assoc. - rewrite bpow_plus. - rewrite <- (Rmult_assoc (Z2R (Zfloor _))). - change (Z2R (Zfloor _) * _) with x'. - do 2 rewrite (Rmult_comm _ (bpow (fexp1 (ln_beta y)))). - rewrite Rmult_assoc. - do 2 rewrite <- (Rmult_assoc (Z2R my)). - rewrite <- Fy. - change (bpow _) with u1. - apply (Rmult_lt_reg_l (/ 2)); [lra|]. - rewrite Rmult_plus_distr_l. - do 4 rewrite <- Rmult_assoc. - rewrite Rinv_l; [|lra]; do 2 rewrite Rmult_1_l. - apply (Rplus_lt_reg_r (- y * x')); ring_simplify. - apply (Rmult_lt_reg_l (/ y)); [now apply Rinv_0_lt_compat|]. - rewrite Rmult_minus_distr_l. - do 3 rewrite <- Rmult_assoc. - rewrite Rinv_l; [|now apply Rgt_not_eq]; do 2 rewrite Rmult_1_l. - now rewrite Rmult_comm. - + apply Rplus_lt_compat_l. - apply Ropp_lt_contravar. - apply Rlt_le_trans with (u2 * bpow (ln_beta y)). - * { apply Rmult_lt_compat_l. - - apply bpow_gt_0. - - apply Rabs_lt_inv. - apply bpow_ln_beta_gt. } - * unfold u2, ulp, canonic_exp; bpow_simplify; apply bpow_le. - apply (Zplus_le_reg_r _ _ (- ln_beta y)); ring_simplify. - rewrite (Zplus_comm (- _)). - destruct (ln_beta_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; - apply Hexp; try assumption; rewrite <- Hxy; omega. -Qed. - -Lemma double_round_div_aux2 : - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - double_round_div_hyp fexp1 fexp2 -> - forall x y, - 0 < x -> 0 < y -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - (fexp1 (ln_beta (x / y)) <= ln_beta (x / y))%Z -> - ~ (midp fexp1 (x / y) - < x / y - <= midp fexp1 (x / y) + / 2 * ulp beta fexp2 (x / y)). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Fx Fy Hf1. -assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -assert (Hfy : (fexp1 (ln_beta y) < ln_beta y)%Z); - [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. -cut (~ (/ 2 * ulp beta fexp1 (x / y) - < x / y - round beta fexp1 Zfloor (x / y) - <= / 2 * (ulp beta fexp1 (x / y) + ulp beta fexp2 (x / y)))). -{ intro H; intro H'; apply H; split. - - apply (Rplus_lt_reg_l (round beta fexp1 Zfloor (x / y))). - ring_simplify. - apply H'. - - apply (Rplus_le_reg_l (round beta fexp1 Zfloor (x / y))). - ring_simplify. - apply H'. } -set (u1 := bpow (fexp1 (ln_beta (x / y)))). -set (u2 := bpow (fexp2 (ln_beta (x / y)))). -set (x' := round beta fexp1 Zfloor (x / y)). -assert (S : (x / y <> 0)%R). -apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac]. -now apply Rinv_neq_0_compat, Rgt_not_eq. -rewrite 2!ulp_neq_0; trivial. -revert Fx Fy. -unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl. -set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))). -set (my := Ztrunc (y * bpow (- fexp1 (ln_beta y)))). -intros Fx Fy. -intro Hlr. -apply (Rlt_irrefl (/ 2 * (u1 + u2))). -apply Rlt_le_trans with (x / y - x'); [|now apply Hlr]. -apply (Rplus_lt_reg_r x'); ring_simplify. -apply (Rmult_lt_reg_r y _ _ Py). -unfold Rdiv; rewrite Rmult_assoc. -rewrite Rinv_l; [|now apply Rgt_not_eq]; rewrite Rmult_1_r. -do 2 rewrite Rmult_plus_distr_r. -apply (Rmult_lt_reg_l 2); [lra|]. -do 2 rewrite Rmult_plus_distr_l. -do 5 rewrite <- Rmult_assoc. -rewrite Rinv_r; [|lra]; do 2 rewrite Rmult_1_l. -destruct (Zle_or_lt Z0 (fexp1 (ln_beta x) - fexp1 (ln_beta (x / y)) - - fexp1 (ln_beta y))%Z) as [He|He]. -- (* fexp1 (ln_beta (x / y)) + fexp1 (ln_beta y) <= fexp1 (ln_beta x) *) - apply Rlt_le_trans with (u1 * y + bpow (fexp1 (ln_beta (x / y)) - + fexp1 (ln_beta y)) - + 2 * x' * y). - + apply Rplus_lt_compat_r, Rplus_lt_compat_l. - apply Rlt_le_trans with (u2 * bpow (ln_beta y)). - * { apply Rmult_lt_compat_l. - - apply bpow_gt_0. - - apply Rabs_lt_inv. - apply bpow_ln_beta_gt. } - * unfold u2, ulp, canonic_exp; bpow_simplify; apply bpow_le. - apply (Zplus_le_reg_r _ _ (- ln_beta y)); ring_simplify. - rewrite <- Zplus_assoc; rewrite (Zplus_comm (- _)). - destruct (ln_beta_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; - [now apply Hexp; [| |rewrite <- Hxy]|]. - replace (_ - _ + 1)%Z with ((ln_beta x + 1) - ln_beta y)%Z by ring. - apply Hexp. - { now assert (fexp1 (ln_beta x + 1) <= ln_beta x)%Z; - [apply valid_exp|omega]. } - { assumption. } - replace (_ + 1 - _)%Z with (ln_beta x - ln_beta y + 1)%Z by ring. - now rewrite <- Hxy. - + apply Rge_le; rewrite Fx at 1; apply Rle_ge. - replace (u1 * y) with (u1 * (Z2R my * bpow (fexp1 (ln_beta y)))); - [|now apply eq_sym; rewrite Fy at 1]. - replace (2 * x' * y) with (2 * x' * (Z2R my * bpow (fexp1 (ln_beta y)))); - [|now apply eq_sym; rewrite Fy at 1]. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta (x / y)) - - fexp1 (ln_beta y)))); - [now apply bpow_gt_0|]. - do 2 rewrite Rmult_plus_distr_r. - bpow_simplify. - rewrite (Rmult_comm u1). - unfold u1, ulp, canonic_exp; bpow_simplify. - rewrite (Rmult_assoc 2). - rewrite (Rmult_comm x'). - rewrite (Rmult_assoc 2). - unfold x', round, F2R, scaled_mantissa, canonic_exp; simpl. - bpow_simplify. - rewrite <- (Z2R_Zpower _ (_ - _)%Z); [|exact He]. - change 2 with (Z2R 2). - do 4 rewrite <- Z2R_mult. - change 1 with (Z2R 1); do 2 rewrite <- Z2R_plus. - apply Z2R_le. - rewrite Zplus_comm, Zplus_assoc. - apply Zlt_le_succ. - apply lt_Z2R. - rewrite Z2R_plus. - do 4 rewrite Z2R_mult; simpl. - rewrite Z2R_Zpower; [|exact He]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta y)))); - [now apply bpow_gt_0|]. - rewrite Rmult_plus_distr_r. - rewrite (Rmult_comm _ (Z2R _)). - do 2 rewrite Rmult_assoc. - rewrite <- Fy. - bpow_simplify. - unfold Zminus; rewrite bpow_plus. - rewrite (Rmult_assoc _ (Z2R mx)). - rewrite <- (Rmult_assoc (Z2R mx)). - rewrite <- Fx. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta (x / y))))); - [now apply bpow_gt_0|]. - rewrite Rmult_plus_distr_r. - bpow_simplify. - rewrite (Rmult_comm _ y). - do 2 rewrite Rmult_assoc. - change (Z2R (Zfloor _) * _) with x'. - change (bpow _) with u1. - apply (Rmult_lt_reg_l (/ 2)); [lra|]. - rewrite Rmult_plus_distr_l. - do 4 rewrite <- Rmult_assoc. - rewrite Rinv_l; [|lra]; do 2 rewrite Rmult_1_l. - apply (Rplus_lt_reg_r (- y * x')); ring_simplify. - apply (Rmult_lt_reg_l (/ y)); [now apply Rinv_0_lt_compat|]. - rewrite Rmult_plus_distr_l. - do 3 rewrite <- Rmult_assoc. - rewrite Ropp_mult_distr_r_reverse. - rewrite Ropp_mult_distr_l_reverse. - rewrite Rinv_l; [|now apply Rgt_not_eq]; do 2 rewrite Rmult_1_l. - rewrite (Rmult_comm (/ y)). - now rewrite (Rplus_comm (- x')). -- (* fexp1 (ln_beta x) < fexp1 (ln_beta (x / y)) + fexp1 (ln_beta y) *) - apply Rlt_le_trans with (2 * x' * y + u1 * y + bpow (fexp1 (ln_beta x))). - + rewrite Rplus_comm, Rplus_assoc; do 2 apply Rplus_lt_compat_l. - apply Rlt_le_trans with (u2 * bpow (ln_beta y)). - * apply Rmult_lt_compat_l. - now apply bpow_gt_0. - now apply Rabs_lt_inv; apply bpow_ln_beta_gt. - * unfold u2, ulp, canonic_exp; bpow_simplify; apply bpow_le. - apply (Zplus_le_reg_r _ _ (- ln_beta y)); ring_simplify. - rewrite (Zplus_comm (- _)). - destruct (ln_beta_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; - apply Hexp; try assumption; rewrite <- Hxy; omega. - + apply Rge_le; rewrite Fx at 1; apply Rle_ge. - rewrite Fy at 1 2. - apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - do 2 rewrite Rmult_plus_distr_r. - bpow_simplify. - replace (2 * x' * _ * _) - with (2 * Z2R my * x' * bpow (fexp1 (ln_beta y) - fexp1 (ln_beta x))) by ring. - rewrite (Rmult_comm u1). - unfold x', u1, round, F2R, ulp, scaled_mantissa, canonic_exp; simpl. - bpow_simplify. - rewrite <- (Z2R_Zpower _ (_ - _)%Z); [|omega]. - change 2 with (Z2R 2). - do 5 rewrite <- Z2R_mult. - change 1 with (Z2R 1); do 2 rewrite <- Z2R_plus. - apply Z2R_le. - apply Zlt_le_succ. - apply lt_Z2R. - rewrite Z2R_plus. - do 5 rewrite Z2R_mult; simpl. - rewrite Z2R_Zpower; [|omega]. - apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); - [now apply bpow_gt_0|]. - rewrite (Rmult_assoc _ (Z2R mx)). - rewrite <- Fx. - rewrite Rmult_plus_distr_r. - bpow_simplify. - rewrite bpow_plus. - rewrite Rmult_assoc. - rewrite <- (Rmult_assoc (Z2R _)). - change (Z2R _ * bpow _) with x'. - do 2 rewrite (Rmult_comm _ (bpow (fexp1 (ln_beta y)))). - rewrite Rmult_assoc. - do 2 rewrite <- (Rmult_assoc (Z2R my)). - rewrite <- Fy. - change (bpow _) with u1. - apply (Rmult_lt_reg_l (/ 2)); [lra|]. - rewrite Rmult_plus_distr_l. - do 4 rewrite <- Rmult_assoc. - rewrite Rinv_l; [|lra]; do 2 rewrite Rmult_1_l. - apply (Rplus_lt_reg_r (- y * x')); ring_simplify. - apply (Rmult_lt_reg_l (/ y)); [now apply Rinv_0_lt_compat|]. - rewrite Rmult_plus_distr_l. - do 3 rewrite <- Rmult_assoc. - rewrite Ropp_mult_distr_r_reverse. - rewrite Ropp_mult_distr_l_reverse. - rewrite Rinv_l; [|now apply Rgt_not_eq]; do 2 rewrite Rmult_1_l. - rewrite (Rmult_comm (/ y)). - now rewrite (Rplus_comm (- x')). -Qed. - -Lemma double_round_div_aux : - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - (exists n, (beta = 2 * n :> Z)%Z) -> - double_round_div_hyp fexp1 fexp2 -> - forall x y, - 0 < x -> 0 < y -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x / y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Ebeta Hexp x y Px Py Fx Fy. -assert (Pxy : 0 < x / y). -{ apply Rmult_lt_0_compat; [exact Px|]. - now apply Rinv_0_lt_compat. } -apply double_round_all_mid_cases. -- exact Vfexp1. -- exact Vfexp2. -- exact Pxy. -- apply Hexp. -- intros Hf1 Hlxy. - casetype False. - now apply (double_round_div_aux0 fexp1 fexp2 _ _ choice1 choice2 Hexp x y). -- intros Hf1 Hlxy. - casetype False. - now apply (double_round_div_aux1 fexp1 fexp2 _ _ choice1 choice2 Hexp x y). -- intro H. - apply double_round_eq_mid_beta_even; try assumption. - apply Hexp. -- intros Hf1 Hlxy. - casetype False. - now apply (double_round_div_aux2 fexp1 fexp2 _ _ choice1 choice2 Hexp x y). -Qed. - -Lemma double_round_div : - forall fexp1 fexp2 : Z -> Z, - Valid_exp fexp1 -> Valid_exp fexp2 -> - forall (choice1 choice2 : Z -> bool), - (exists n, (beta = 2 * n :> Z)%Z) -> - double_round_div_hyp fexp1 fexp2 -> - forall x y, - y <> 0 -> - generic_format beta fexp1 x -> - generic_format beta fexp1 y -> - double_round_eq fexp1 fexp2 choice1 choice2 (x / y). -Proof. -intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Ebeta Hexp x y Nzy Fx Fy. -unfold double_round_eq. -destruct (Rtotal_order x 0) as [Nx|[Zx|Px]]. -- (* x < 0 *) - destruct (Rtotal_order y 0) as [Ny|[Zy|Py]]. - + (* y < 0 *) - rewrite <- (Ropp_involutive x). - rewrite <- (Ropp_involutive y). - rewrite Ropp_div. - unfold Rdiv; rewrite <- Ropp_inv_permute; [|lra]. - rewrite Ropp_mult_distr_r_reverse. - rewrite Ropp_involutive. - fold ((- x) / (- y)). - apply Ropp_lt_contravar in Nx. - apply Ropp_lt_contravar in Ny. - rewrite Ropp_0 in Nx, Ny. - apply generic_format_opp in Fx. - apply generic_format_opp in Fy. - now apply double_round_div_aux. - + (* y = 0 *) - now casetype False; apply Nzy. - + (* y > 0 *) - rewrite <- (Ropp_involutive x). - rewrite Ropp_div. - do 3 rewrite round_N_opp. - apply Ropp_eq_compat. - apply Ropp_lt_contravar in Nx. - rewrite Ropp_0 in Nx. - apply generic_format_opp in Fx. - now apply double_round_div_aux. -- (* x = 0 *) - rewrite Zx. - unfold Rdiv; rewrite Rmult_0_l. - now rewrite round_0; [|apply valid_rnd_N]. -- (* x > 0 *) - destruct (Rtotal_order y 0) as [Ny|[Zy|Py]]. - + (* y < 0 *) - rewrite <- (Ropp_involutive y). - unfold Rdiv; rewrite <- Ropp_inv_permute; [|lra]. - rewrite Ropp_mult_distr_r_reverse. - do 3 rewrite round_N_opp. - apply Ropp_eq_compat. - apply Ropp_lt_contravar in Ny. - rewrite Ropp_0 in Ny. - apply generic_format_opp in Fy. - now apply double_round_div_aux. - + (* y = 0 *) - now casetype False; apply Nzy. - + (* y > 0 *) - now apply double_round_div_aux. -Qed. - -Section Double_round_div_FLX. - -Import Fcore_FLX. - -Variable prec : Z. -Variable prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FLX_double_round_div_hyp : - (2 * prec <= prec')%Z -> - double_round_div_hyp (FLX_exp prec) (FLX_exp prec'). -Proof. -intros Hprec. -unfold Prec_gt_0 in prec_gt_0_. -unfold FLX_exp. -unfold double_round_div_hyp. -split; [now intro ex; omega|]. -split; [|split; [|split]]; intros ex ey; omega. -Qed. - -Theorem double_round_div_FLX : - forall choice1 choice2, - (exists n, (beta = 2 * n :> Z)%Z) -> - (2 * prec <= prec')%Z -> - forall x y, - y <> 0 -> - FLX_format beta prec x -> FLX_format beta prec y -> - double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x / y). -Proof. -intros choice1 choice2 Ebeta Hprec x y Nzy Fx Fy. -apply double_round_div. -- now apply FLX_exp_valid. -- now apply FLX_exp_valid. -- exact Ebeta. -- now apply FLX_double_round_div_hyp. -- exact Nzy. -- now apply generic_format_FLX. -- now apply generic_format_FLX. -Qed. - -End Double_round_div_FLX. - -Section Double_round_div_FLT. - -Import Fcore_FLX. -Import Fcore_FLT. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FLT_double_round_div_hyp : - (emin' <= emin - prec - 2)%Z -> - (2 * prec <= prec')%Z -> - double_round_div_hyp (FLT_exp emin prec) (FLT_exp emin' prec'). -Proof. -intros Hemin Hprec. -unfold FLT_exp. -unfold Prec_gt_0 in prec_gt_0_. -unfold double_round_div_hyp. -split; [intro ex|split; [|split; [|split]]; intros ex ey]. -- generalize (Zmax_spec (ex - prec') emin'). - generalize (Zmax_spec (ex - prec) emin). - omega. -- generalize (Zmax_spec (ex - prec) emin). - generalize (Zmax_spec (ey - prec) emin). - generalize (Zmax_spec (ex - ey - prec) emin). - generalize (Zmax_spec (ex - ey - prec') emin'). - omega. -- generalize (Zmax_spec (ex - prec) emin). - generalize (Zmax_spec (ey - prec) emin). - generalize (Zmax_spec (ex - ey + 1 - prec) emin). - generalize (Zmax_spec (ex - ey + 1 - prec') emin'). - omega. -- generalize (Zmax_spec (ex - prec) emin). - generalize (Zmax_spec (ey - prec) emin). - generalize (Zmax_spec (ex - ey - prec) emin). - generalize (Zmax_spec (ex - ey - prec') emin'). - omega. -- generalize (Zmax_spec (ex - prec) emin). - generalize (Zmax_spec (ey - prec) emin). - generalize (Zmax_spec (ex - ey - prec) emin). - generalize (Zmax_spec (ex - ey - prec') emin'). - omega. -Qed. - -Theorem double_round_div_FLT : - forall choice1 choice2, - (exists n, (beta = 2 * n :> Z)%Z) -> - (emin' <= emin - prec - 2)%Z -> - (2 * prec <= prec')%Z -> - forall x y, - y <> 0 -> - FLT_format beta emin prec x -> FLT_format beta emin prec y -> - double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec') - choice1 choice2 (x / y). -Proof. -intros choice1 choice2 Ebeta Hemin Hprec x y Nzy Fx Fy. -apply double_round_div. -- now apply FLT_exp_valid. -- now apply FLT_exp_valid. -- exact Ebeta. -- now apply FLT_double_round_div_hyp. -- exact Nzy. -- now apply generic_format_FLT. -- now apply generic_format_FLT. -Qed. - -End Double_round_div_FLT. - -Section Double_round_div_FTZ. - -Import Fcore_FLX. -Import Fcore_FTZ. - -Variable emin prec : Z. -Variable emin' prec' : Z. - -Context { prec_gt_0_ : Prec_gt_0 prec }. -Context { prec_gt_0_' : Prec_gt_0 prec' }. - -Lemma FTZ_double_round_div_hyp : - (emin' + prec' <= emin - 1)%Z -> - (2 * prec <= prec')%Z -> - double_round_div_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec'). -Proof. -intros Hemin Hprec. -unfold FTZ_exp. -unfold Prec_gt_0 in prec_gt_0_. -unfold Prec_gt_0 in prec_gt_0_. -unfold double_round_div_hyp. -split; [intro ex|split; [|split; [|split]]; intros ex ey]. -- destruct (Z.ltb_spec (ex - prec') emin'); - destruct (Z.ltb_spec (ex - prec) emin); - omega. -- destruct (Z.ltb_spec (ex - prec) emin); - destruct (Z.ltb_spec (ey - prec) emin); - destruct (Z.ltb_spec (ex - ey - prec) emin); - destruct (Z.ltb_spec (ex - ey - prec') emin'); - omega. -- destruct (Z.ltb_spec (ex - prec) emin); - destruct (Z.ltb_spec (ey - prec) emin); - destruct (Z.ltb_spec (ex - ey + 1 - prec) emin); - destruct (Z.ltb_spec (ex - ey + 1 - prec') emin'); - omega. -- destruct (Z.ltb_spec (ex - prec) emin); - destruct (Z.ltb_spec (ey - prec) emin); - destruct (Z.ltb_spec (ex - ey - prec) emin); - destruct (Z.ltb_spec (ex - ey - prec') emin'); - omega. -- destruct (Z.ltb_spec (ex - prec) emin); - destruct (Z.ltb_spec (ey - prec) emin); - destruct (Z.ltb_spec (ex - ey - prec) emin); - destruct (Z.ltb_spec (ex - ey - prec') emin'); - omega. -Qed. - -Theorem double_round_div_FTZ : - forall choice1 choice2, - (exists n, (beta = 2 * n :> Z)%Z) -> - (emin' + prec' <= emin - 1)%Z -> - (2 * prec <= prec')%Z -> - forall x y, - y <> 0 -> - FTZ_format beta emin prec x -> FTZ_format beta emin prec y -> - double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec') - choice1 choice2 (x / y). -Proof. -intros choice1 choice2 Ebeta Hemin Hprec x y Nzy Fx Fy. -apply double_round_div. -- now apply FTZ_exp_valid. -- now apply FTZ_exp_valid. -- exact Ebeta. -- now apply FTZ_double_round_div_hyp. -- exact Nzy. -- now apply generic_format_FTZ. -- now apply generic_format_FTZ. -Qed. - -End Double_round_div_FTZ. - -End Double_round_div. - -End Double_round. -- cgit