Skip to content

GitLab

F
flocq
Commit 0a6a2cd1 authored by Pierre Roux's avatar Pierre Roux
Browse files
Options

Properties about innocuous double rounding of usual arithmetic operations.

parent cf6e4536
Hide whitespace changes
Inline Side-by-side
Showing with 7000 additions and 1 deletion
Remakefile.in
View file @ 0a6a2cd1
......@@ -27,7 +27,8 @@ FILES = \
Prop/Fprop_Sterbenz.v \
Appli/Fappli_rnd_odd.v \
Appli/Fappli_IEEE.v \
Appli/Fappli_IEEE_bits.v
Appli/Fappli_IEEE_bits.v \
Appli/Fappli_double_round.v
OBJS = $(addprefix src/,$(addsuffix o,$(FILES)))
......
examples/Double_round_beta_odd.v 0 → 100644
View file @ 0a6a2cd1
(** * 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 Import Fappli_double_round.
Require Import Psatz.
Open Scope R_scope.
Section Double_round_beta_odd.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Notation ln_beta x := (ln_beta beta 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.
Hypothesis Obeta : exists n, (beta = 2 * n + 1 :> Z)%Z.
Lemma midpoint_beta_odd_remains_pos :
forall x,
0 < x ->
forall (ex1 ex2 : Z),
(ex2 <= ex1)%Z ->
x = Z2R (Zfloor (x * bpow (- ex1))) * bpow ex1 ->
exists x',
0 < x'
/\ (ln_beta x' = ln_beta x :> Z)
/\ x' = Z2R (Zfloor (x' * bpow (- ex2))) * bpow ex2
/\ x + / 2 * bpow ex1 = x' + / 2 * bpow ex2.
Proof.
intros x Px ex1 ex2 Hf2.
set (z := (ex1 - ex2)%Z).
assert (Hz : Z_of_nat (Zabs_nat z) = z).
{ rewrite Zabs2Nat.id_abs.
rewrite <- cond_Zopp_Zlt_bool; unfold cond_Zopp.
assert (H : (z <? 0)%Z = false); [|now rewrite H].
apply Zlt_bool_false; unfold z; omega. }
revert Hz.
generalize (Zabs_nat z); intro n.
unfold z; clear z; revert ex1 ex2 Hf2.
induction n.
- simpl.
intros ex1 ex2 _ Hf1 Fx.
exists x.
assert (H : ex2 = ex1) by omega.
split; [|split; [|split]].
+ exact Px.
+ reflexivity.
+ revert Fx; unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl.
now rewrite H.
+ now unfold ulp, canonic_exp; rewrite H.
- intros ex1 ex2 Hf2 HSn Fx.
destruct Obeta as (nb,Hb).
assert (Hbeta : (2 <= beta)%Z).
{ destruct beta as (beta_val,beta_prop).
now apply Zle_bool_imp_le. }
assert (Nnnb : (1 <= nb)%Z) by omega.
assert (Hf1 : (ex1 = ex2 + Z.of_nat n + 1 :> Z)%Z); [|clear HSn].
{ rewrite <- Zplus_assoc.
replace (_ + 1)%Z with (Z.of_nat (S n)); [omega|].
simpl.
now rewrite Zpos_P_of_succ_nat. }
assert (Hf2' : (ex2 + 1 <= ex1)%Z).
{ rewrite Hf1.
rewrite <- Zplus_assoc.
apply Zplus_le_compat_l.
rewrite <- (Zplus_0_l 1) at 1; apply Zplus_le_compat_r.
apply Zle_0_nat. }
assert (Hd1 : Z.of_nat n = (ex1 - (ex2 + 1))%Z);
[now rewrite Hf1; ring|].
set (ex2' := (ex2 + 1)%Z).
destruct (IHn ex1 ex2' Hf2' Hd1 Fx)
as (x',(Px',(Hlx',(Fx',Hx')))); clear Hd1 IHn.
set (u := bpow ex2).
exists (x' + Z2R nb * u).
split; [|split; [|split]].
+ apply (Rlt_le_trans _ _ _ Px').
rewrite <- (Rplus_0_r x') at 1; apply Rplus_le_compat_l.
apply Rmult_le_pos.
* change 0 with (Z2R 0); apply Z2R_le; omega.
* now apply bpow_ge_0.
+ rewrite <- Hlx'.
apply (ln_beta_succ beta (fun e => (e - (ln_beta x' - ex2'))%Z));
[| |split].
* exact Px'.
* unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl.
bpow_simplify.
rewrite Ztrunc_floor; [exact Fx'|].
now apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0].
* apply Rmult_le_pos; [|now apply bpow_ge_0].
change 0 with (Z2R 0); apply Z2R_le; omega.
* unfold u, ulp, ex2', canonic_exp; bpow_simplify.
rewrite Zplus_comm; rewrite bpow_plus.
apply Rmult_lt_compat_r; [now apply bpow_gt_0|].
rewrite bpow_1.
apply Z2R_lt; omega.
+ rewrite Fx' at 1.
unfold ex2' at 2.
rewrite Zplus_comm; rewrite bpow_plus; fold u.
rewrite <- Rmult_assoc; rewrite <- Rmult_plus_distr_r.
apply Rmult_eq_compat_r.
replace (Z2R _) with (x' * bpow (- ex2'));
[|now apply (Rmult_eq_reg_r (bpow ex2'));
[|now apply Rgt_not_eq; apply bpow_gt_0]; bpow_simplify].
rewrite Rmult_plus_distr_r.
unfold u, ex2'; bpow_simplify.
rewrite Fx' at 2; unfold ex2'; bpow_simplify.
rewrite bpow_1; rewrite <- Z2R_mult; rewrite <- Z2R_plus.
rewrite Zfloor_Z2R.
rewrite Z2R_plus.
apply f_equal2; [|reflexivity].
replace (- ex2 - 1)%Z with (- ex2')%Z; [|now unfold ex2'; ring].
rewrite Fx' at 1; unfold ex2'; bpow_simplify.
now rewrite Z2R_mult; rewrite <- bpow_1.
+ rewrite Hx'.
rewrite Rplus_assoc; apply Rplus_eq_compat_l.
rewrite <- Rmult_plus_distr_r.
unfold ex2'; rewrite Zplus_comm; rewrite bpow_plus.
rewrite <- Rmult_assoc; apply Rmult_eq_compat_r.
rewrite (Rmult_eq_reg_l 2 _ (Z2R nb + / 2)); [reflexivity| |lra].
field_simplify; apply Rmult_eq_compat_r.
rewrite bpow_1; change 2 with (Z2R 2); change 1 with (Z2R 1).
now rewrite <- Z2R_mult; rewrite <- Z2R_plus; apply f_equal.
Qed.
Lemma midpoint_beta_odd_remains :
forall x,
0 <= x ->
forall (ex1 ex2 : Z),
(ex2 <= ex1)%Z ->
x = Z2R (Zfloor (x * bpow (- ex1))) * bpow ex1 ->
exists x',
0 <= x'
/\ x' = Z2R (Zfloor (x' * bpow (- ex2))) * bpow ex2
/\ x + / 2 * bpow ex1 = x' + / 2 * bpow ex2.
Proof.
intros x Px ex1 ex2 Hf2 Hx.
set (x1 := x + bpow ex1).
assert (Px1 : 0 < x1).
{ apply (Rle_lt_trans _ _ _ Px).
rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l, bpow_gt_0. }
destruct (midpoint_beta_odd_remains_pos x1 Px1 ex1 ex2 Hf2)
as (x',(Hx'1,(Hx'2,(Hx'3,Hx'4)))).
{ unfold x1 at 2.
rewrite Rmult_plus_distr_r, Hx; bpow_simplify.
change 1 with (Z2R 1); rewrite <- Z2R_plus.
now rewrite Zfloor_Z2R, Z2R_plus, Rmult_plus_distr_r, Rmult_1_l, <- Hx. }
assert (Hx' : x' = x1 + / 2 * bpow ex1 - / 2 * bpow ex2).
{ rewrite Hx'4; ring. }
exists (x' - bpow ex1); split; [|split].
- rewrite Hx'; unfold x1; ring_simplify.
replace (_ - _) with (x + (/ 2 * (bpow ex1 - bpow ex2))) by ring.
apply Rplus_le_le_0_compat; [exact Px|]; apply Rmult_le_pos; [lra|].
now apply Rle_0_minus, bpow_le.
- rewrite Rmult_minus_distr_r; rewrite Hx'3 at 2; bpow_simplify.
rewrite <- (Z2R_Zpower beta (ex1 - ex2)); [|now apply Zle_minus_le_0].
rewrite <- Z2R_minus, Zfloor_Z2R, Z2R_minus.
rewrite (Z2R_Zpower beta (ex1 - ex2)); [|now apply Zle_minus_le_0].
rewrite Rmult_minus_distr_r; bpow_simplify.
now rewrite Hx'3 at 1.
- rewrite Hx'; unfold x1; ring.
Qed.
Lemma neq_midpoint_beta_odd_aux1 :
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 ->
midp beta fexp1 x - / 2 * ulp beta fexp2 x <= x < midp beta fexp1 x ->
double_round_eq beta fexp1 fexp2 choice1 choice2 x.
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx.
unfold double_round_eq.
set (ex1 := fexp1 (ln_beta x)).
set (ex2 := fexp2 (ln_beta x)).
set (rx1 := round beta fexp1 Zfloor x).
assert (Prx1 : 0 <= rx1).
{ rewrite <- (round_0 beta fexp1 Zfloor).
now apply round_le; [exact Vfexp1|apply valid_rnd_DN|apply Rlt_le]. }
assert (Hrx1 : rx1 = Z2R (Zfloor (rx1 * bpow (- ex1))) * bpow ex1).
{ unfold rx1 at 2; unfold round, F2R, scaled_mantissa, canonic_exp; simpl.
unfold ex1; bpow_simplify.
now rewrite Zfloor_Z2R. }
destruct (midpoint_beta_odd_remains rx1 Prx1 ex1 ex2 Hf2f1 Hrx1)
as (rx2,(Nnrx2, (Hrx2, Hrx12))).
assert (Hx' : rx2 <= x < rx2 + / 2 * bpow ex2).
{ split.
- replace rx2 with (rx2 + / 2 * bpow ex2 - / 2 * bpow ex2) by ring.
rewrite <- Hrx12; apply Hx.
- rewrite <- Hrx12; apply Hx. }
assert (Hr2 : round beta fexp2 (Znearest choice2) x = rx2).
{ unfold round, F2R, scaled_mantissa, canonic_exp; simpl.
apply (Rmult_eq_reg_r (bpow (- fexp2 (ln_beta x))));
[|now apply Rgt_not_eq, Rlt_gt, bpow_gt_0].
bpow_simplify.
rewrite (Znearest_imp _ _ (Zfloor (rx2 * bpow (- ex2)))).
- now rewrite Hrx2 at 2; unfold ex2; bpow_simplify.
- apply Rabs_lt; split.
+ apply Rlt_le_trans with 0; [lra|].
apply Rle_0_minus.
apply (Rmult_le_reg_r (bpow ex2)); [now apply bpow_gt_0|].
fold ex2; bpow_simplify.
now rewrite <- Hrx2.
+ apply (Rmult_lt_reg_r (bpow (fexp2 (ln_beta x)))); [now apply bpow_gt_0|].
rewrite Rmult_minus_distr_r; fold ex2; bpow_simplify.
rewrite <- Hrx2.
now apply (Rplus_lt_reg_l rx2); ring_simplify. }
rewrite Hr2.
assert (Hrx2' : rx1 <= rx2 < rx1 + / 2 * bpow ex1).
{ split.
- apply (Rplus_le_reg_r (/ 2 * bpow ex1)).
rewrite Hrx12.
apply Rplus_le_compat_l.
apply Rmult_le_compat_l; [lra|].
now apply bpow_le.
- change (_ + _) with (midp beta fexp1 x).
apply (Rle_lt_trans _ _ _ (proj1 Hx') (proj2 Hx)). }
assert (Hrx2r : rx2 = round beta fexp2 Zfloor x).
{ unfold round, F2R, scaled_mantissa, canonic_exp; simpl.
fold ex2; rewrite Hrx2.
apply Rmult_eq_compat_r, f_equal.
apply eq_sym, Zfloor_imp; split.
- apply (Rle_trans _ _ _ (Zfloor_lb _)).
now apply Rmult_le_compat_r; [apply bpow_ge_0|].
- apply (Rmult_lt_reg_r (bpow ex2)); [now apply bpow_gt_0|]; bpow_simplify.
rewrite Z2R_plus, Rmult_plus_distr_r, <- Hrx2.
apply (Rlt_le_trans _ _ _ (proj2 Hx')).
apply Rplus_le_compat_l, Rmult_le_compat_r; [apply bpow_ge_0|simpl; lra]. }
destruct (Rle_or_lt rx2 0) as [Nprx2|Prx2].
{ (* rx2 = 0 *)
assert (Zrx2 : rx2 = 0); [now apply Rle_antisym|].
rewrite Zrx2, round_0; [|now apply valid_rnd_N].
unfold round, F2R, scaled_mantissa, canonic_exp; simpl.
apply (Rmult_eq_reg_r (bpow (- fexp1 (ln_beta x))));
[|now apply Rgt_not_eq, bpow_gt_0]; rewrite Rmult_0_l; bpow_simplify.
change 0 with (Z2R 0); apply f_equal, eq_sym, Znearest_imp.
apply Rabs_lt; simpl; unfold Rminus; rewrite Ropp_0, Rplus_0_r.
split.
- apply Rlt_trans with 0; [lra|].
now apply Rmult_lt_0_compat; [|apply bpow_gt_0].
- apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|].
bpow_simplify.
rewrite Zrx2, Rplus_0_l in Hx'.
apply (Rlt_le_trans _ _ _ (proj2 Hx')), Rmult_le_compat_l; [lra|].
now apply bpow_le. }
(* 0 < rx2 *)
assert (Hl2 : ln_beta rx2 = ln_beta x :> Z).
{ now rewrite Hrx2r; apply ln_beta_round_DN; [|rewrite <- Hrx2r]. }
assert (Hr12 : round beta fexp1 (Znearest choice1) rx2 = rx1).
{ unfold round, F2R, scaled_mantissa, canonic_exp; simpl.
rewrite Hl2; fold ex1.
apply (Rmult_eq_reg_r (bpow (- ex1)));
[|now apply Rgt_not_eq, bpow_gt_0]; bpow_simplify.
unfold rx1, round, F2R, scaled_mantissa, canonic_exp; simpl.
fold ex1; bpow_simplify.
apply f_equal, Znearest_imp.
apply Rabs_lt; split.
- apply Rlt_le_trans with 0; [lra|apply Rle_0_minus].
now apply (Rmult_le_reg_r (bpow ex1)); bpow_simplify; [apply bpow_gt_0|].
- apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
rewrite Rmult_minus_distr_r; bpow_simplify.
change (Z2R _ * _) with rx1.
apply (Rplus_lt_reg_r rx1); ring_simplify.
apply (Rlt_le_trans _ _ _ (proj2 Hrx2')), Rplus_le_compat_l.
now apply Rmult_le_compat_l; [lra|right]. }
rewrite Hr12.
unfold rx1, round, F2R, scaled_mantissa, canonic_exp; simpl; fold ex1.
apply Rmult_eq_compat_r, f_equal, eq_sym, Znearest_imp, Rabs_lt; split.
- apply Rlt_le_trans with 0; [lra|]; apply Rle_0_minus, Zfloor_lb.
- apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
rewrite Rmult_minus_distr_r; bpow_simplify.
change (Z2R _ * _) with rx1.
now apply (Rplus_lt_reg_l rx1); ring_simplify.
Qed.
Lemma neq_midpoint_beta_odd_aux2 :
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 ->
midp beta fexp1 x < x <= midp beta fexp1 x + / 2 * ulp beta fexp2 x ->
double_round_eq beta fexp1 fexp2 choice1 choice2 x.
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx.
unfold double_round_eq.
set (ex1 := fexp1 (ln_beta x)).
set (ex2 := fexp2 (ln_beta x)).
set (rx1 := round beta fexp1 Zfloor x).
assert (Hbeta : (2 <= beta)%Z).
{ destruct beta as (beta_val,beta_prop).
now apply Zle_bool_imp_le. }
destruct (generic_format_EM beta fexp2 x) as [F2x|NF2x].
{ (* generic_format beta fexp2 x *)
now rewrite (round_generic _ fexp2); [|apply valid_rnd_N|]. }
(* ~ generic_format beta fexp2 x *)
assert (Nnrx1 : 0 <= rx1).
{ rewrite <- (round_0 beta fexp1 Zfloor).
now apply round_le; [exact Vfexp1|apply valid_rnd_DN|apply Rlt_le]. }
assert (Hrx1 : rx1 = Z2R (Zfloor (rx1 * bpow (- ex1))) * bpow ex1).
{ unfold rx1 at 2; unfold round, F2R, scaled_mantissa, canonic_exp; simpl.
unfold ex1; bpow_simplify.
now rewrite Zfloor_Z2R. }
set (rx1c := round beta fexp1 Zceil x).
assert (Hf2f1' : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z) by omega.
assert (NF1x : ~ generic_format beta fexp1 x).
{ now intro H; apply NF2x, (generic_inclusion_ln_beta _ fexp1). }
assert (Hrx1c : rx1c = rx1 + ulp beta fexp1 x).
{ now apply ulp_DN_UP. }
destruct (midpoint_beta_odd_remains rx1 Nnrx1 ex1 ex2 Hf2f1' Hrx1)
as (rx2,(Nnrx2, (Hrx2, Hrx12))).
set (rx2c := rx2 + ulp beta fexp2 x).
assert (Hx' : rx2c - / 2 * bpow ex2 < x <= rx2c).
{ unfold rx2c, ulp, canonic_exp; fold ex1; fold ex2; split.
- replace (_ - _) with (rx2 + / 2 * bpow ex2) by field.
rewrite <- Hrx12; apply Hx.
- replace (_ + _) with (rx2 + / 2 * bpow ex2 + / 2 * bpow ex2) by field.
rewrite <- Hrx12; apply Hx. }
assert (Hrx2c : rx2c = Z2R (Zfloor (rx2c * bpow (- ex2))) * bpow ex2).
{ unfold rx2c, ulp, canonic_exp; fold ex2; rewrite Rmult_plus_distr_r.
bpow_simplify.
rewrite Hrx2 at 2; bpow_simplify.
change 1 with (Z2R 1); rewrite <- Z2R_plus, Zfloor_Z2R, Z2R_plus; simpl.
now rewrite Rmult_plus_distr_r; apply f_equal2; [|now rewrite Rmult_1_l]. }
assert (Prx2c : 0 < rx2c).
{ now apply Rplus_le_lt_0_compat; [|apply bpow_gt_0]. }
assert (Hr2 : round beta fexp2 (Znearest choice2) x = rx2c).
{ unfold round, F2R, scaled_mantissa, canonic_exp; simpl; fold ex2.
apply (Rmult_eq_reg_r (bpow (- ex2))); [|now apply Rgt_not_eq, bpow_gt_0].
bpow_simplify.
rewrite (Znearest_imp _ _ (Zfloor (rx2c * bpow (- ex2)))).
- now apply (Rmult_eq_reg_r (bpow ex2)); bpow_simplify;
[apply eq_sym|apply Rgt_not_eq, bpow_gt_0].
- apply Rabs_lt; split.
+ apply (Rmult_lt_reg_r (bpow ex2)); [now apply bpow_gt_0|].
rewrite Rmult_minus_distr_r; bpow_simplify.
rewrite <- Hrx2c.
now apply (Rplus_lt_reg_l rx2c); ring_simplify.
+ apply Rle_lt_trans with 0; [|lra].
apply Rle_minus.
apply (Rmult_le_reg_r (bpow ex2)); [now apply bpow_gt_0|]; bpow_simplify.
now rewrite <- Hrx2c. }
rewrite Hr2.
assert (Hrx2' : rx1c - / 2 * bpow ex1 < rx2c <= rx1c).
{ split.
- rewrite Hrx1c; unfold ulp, canonic_exp; fold ex1.
replace (_ - _) with (rx1 + / 2 * bpow ex1) by field.
change (_ + _) with (midp beta fexp1 x).
apply (Rlt_le_trans _ _ _ (proj1 Hx) (proj2 Hx')).
- apply (Rplus_le_reg_r (- / 2 * bpow ex2)).
unfold rx2c, ulp, canonic_exp; fold ex2.
replace (_ + _) with (rx2 + / 2 * bpow ex2) by field.
rewrite <- Hrx12.
rewrite Hrx1c, Rplus_assoc; apply Rplus_le_compat_l.
unfold ulp, canonic_exp; fold ex1.
apply (Rplus_le_reg_r (- / 2 * bpow ex1)); field_simplify.
unfold Rdiv; apply Rmult_le_compat_r; [lra|].
now apply Rle_0_minus, bpow_le. }
assert (Hr1 : round beta fexp1 (Znearest choice1) x = rx1c).
{ unfold rx1c, round, F2R, scaled_mantissa, canonic_exp; simpl; fold ex1.
apply Rmult_eq_compat_r, f_equal, Znearest_imp, Rabs_lt; split.
- apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
rewrite Rmult_minus_distr_r; bpow_simplify.
change (Z2R _ * _) with rx1c.
apply (Rplus_lt_reg_l rx1c); ring_simplify.
rewrite Hrx1c; unfold ulp, canonic_exp; fold ex1.
now replace (_ - _) with (rx1 + / 2 * bpow ex1) by field.
- apply Rlt_le_trans with 0; [|lra]; apply Rlt_minus.
apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|]; bpow_simplify.
assert (H : x <= rx1c); [now apply round_UP_pt|].
destruct H as [H|H]; [exact H|].
casetype False; apply NF1x.
unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl; fold ex1.
rewrite Ztrunc_floor;
[|now apply Rmult_le_pos;[apply Rlt_le|apply bpow_ge_0]].
rewrite H at 2.
unfold rx1c, round, F2R, scaled_mantissa, canonic_exp; simpl; fold ex1.
now bpow_simplify; rewrite Zfloor_Z2R; rewrite H at 1. }
rewrite Hr1.
destruct (Rle_or_lt rx1 0) as [Nprx1|Prx1].
{ (* rx1 = 0 *)
assert (Zrx1 : rx1 = 0); [now apply Rle_antisym|].
rewrite Hrx1c, Zrx1, Rplus_0_l.
unfold rx2c, ulp, canonic_exp; fold ex1; fold ex2.
replace (_ + _) with (rx2 + / 2 * bpow ex2 + / 2 * bpow ex2) by field.
rewrite <- Hrx12, Zrx1, Rplus_0_l.
assert (Ph12 : 0 < / 2 * bpow ex1 + / 2 * bpow ex2).
{ now apply Rplus_lt_0_compat;
(apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]). }
assert (Hf1 : (fexp1 (ln_beta x) <= ln_beta x)%Z).
{ apply ln_beta_ge_bpow.
rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
apply Rle_trans with (/ 2 * bpow ex1).
- unfold Zminus; rewrite bpow_plus, Rmult_comm.
fold ex1; apply Rmult_le_compat_r; [now apply bpow_ge_0|].
rewrite bpow_opp; apply Rinv_le; [lra|].
simpl; unfold Z.pow_pos; simpl; rewrite Zmult_1_r.
now change 2 with (Z2R 2); apply Z2R_le.
- apply Rlt_le.
now rewrite <- (Rplus_0_l (_ * _)), <- Zrx1. }
assert (Hl1 : ln_beta (/ 2 * bpow ex1 + / 2 * bpow ex2) = ln_beta x :> Z).
{ apply ln_beta_unique; split.
- rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
apply Rle_trans with x.
+ destruct (ln_beta x) as (ex, Hex); simpl.
now rewrite <- (Rabs_right x);
[apply Hex, Rgt_not_eq|apply Rle_ge, Rlt_le].
+ rewrite <- (Rplus_0_l (_ * _)), <- Zrx1.
apply Hx.
- rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
apply Rlt_le_trans with (bpow ex1); [|now apply bpow_le].
rewrite <- (Rmult_1_l (bpow ex1)) at 2.
replace (1 * bpow ex1) with (/ 2 * bpow ex1 + / 2 * bpow ex1) by field.
now apply Rplus_lt_compat_l, Rmult_lt_compat_l; [lra|apply bpow_lt]. }
unfold round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Hl1.
fold ex1; apply (Rmult_eq_reg_r (bpow (- ex1)));
[|now apply Rgt_not_eq, bpow_gt_0]; bpow_simplify.
change 1 with (Z2R 1); apply f_equal, Znearest_imp; simpl.
apply Rabs_lt; simpl; split.
- apply (Rplus_lt_reg_r 1); replace (- _ + _) with (/ 2) by field.
ring_simplify; apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
rewrite Rmult_plus_distr_r; bpow_simplify.
rewrite <- (Rplus_0_r (_ * _)) at 1; apply Rplus_lt_compat_l.
apply Rmult_lt_0_compat; [lra|apply bpow_gt_0].
- apply (Rplus_lt_reg_r 1); ring_simplify.
apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
do 2 rewrite Rmult_plus_distr_r; bpow_simplify.
now apply Rplus_lt_compat_l, Rmult_lt_compat;
[lra|apply bpow_ge_0|lra|apply bpow_lt]. }
(* 0 < rx1 *)
assert (Hl1 : ln_beta rx1 = ln_beta x :> Z).
{ now apply ln_beta_round_DN. }
assert (Hl2 : ln_beta rx2c = ln_beta x :> Z).
{ apply ln_beta_unique; rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
replace rx2c with (rx1 + (/ 2 * bpow ex1 + / 2 * bpow ex2));
[|now rewrite <- Rplus_assoc, Hrx12;
replace (_ + _) with (rx2 + bpow ex2) by field].
split.
- rewrite <- Rplus_assoc.
change (_ + _) with (midp beta fexp1 x + / 2 * ulp beta fexp2 x).
apply Rle_trans with x; [|now apply Hx].
apply Rge_le; rewrite <- (Rabs_right x) at 1; [|now apply Rle_ge, Rlt_le];
apply Rle_ge; destruct (ln_beta x) as (ex,Hex); simpl; apply Hex.
now apply Rgt_not_eq.
- apply Rlt_le_trans with (rx1 + bpow ex1).
+ apply Rplus_lt_compat_l.
rewrite <- (Rmult_1_l (bpow ex1)) at 2.
replace (1 * bpow ex1) with (/ 2 * bpow ex1 + / 2 * bpow ex1) by field.
now apply Rplus_lt_compat_l, Rmult_lt_compat_l; [lra|apply bpow_lt].
+ unfold ex1; rewrite <- Hl1; apply succ_le_bpow; [exact Prx1| |].
* now apply generic_format_round; [|apply valid_rnd_DN].
* destruct (ln_beta rx1) as (erx1, Herx1); simpl.
rewrite <- (Rabs_right rx1) at 1; [|now apply Rle_ge, Rlt_le].
now apply Herx1, Rgt_not_eq. }
unfold round, F2R, scaled_mantissa, canonic_exp; simpl.
rewrite Hl2; fold ex1.
apply (Rmult_eq_reg_r (bpow (- ex1)));
[|now apply Rgt_not_eq, bpow_gt_0]; bpow_simplify.
rewrite Hrx1c, Rmult_plus_distr_r.
unfold rx1, round, F2R, scaled_mantissa, ulp, canonic_exp; simpl; fold ex1.
bpow_simplify.
change 1 with (Z2R 1); rewrite <- Z2R_plus; apply f_equal, Znearest_imp.
apply Rabs_lt; split.
- rewrite Z2R_plus; simpl; apply (Rplus_lt_reg_r 1); ring_simplify.
replace (- _ + _) with (/ 2) by field.
apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
rewrite Rmult_minus_distr_r; bpow_simplify.
change (Z2R _ * _) with rx1.
apply (Rplus_lt_reg_l rx1); ring_simplify.
apply Rlt_le_trans with x; [apply Hx|apply Hx'].
- apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
rewrite Rmult_minus_distr_r; bpow_simplify.
rewrite Z2R_plus, Rmult_plus_distr_r; simpl; rewrite Rmult_1_l.
change (Z2R _ * _ + _) with (rx1 + ulp beta fexp1 x).
rewrite <- Hrx1c; lra.
Qed.
(* neq_midpoint_beta_odd_aux{1,2} together *)
Lemma neq_midpoint_beta_odd_aux3 :
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 beta fexp1 x ->
double_round_eq beta fexp1 fexp2 choice1 choice2 x.
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx.
destruct (generic_format_EM beta fexp2 x) as [F2x|NF2x].
{ (* generic_format beta fexp2 x *)
unfold double_round_eq.
now rewrite (round_generic _ fexp2); [|apply valid_rnd_N|]. }
(* ~ generic_format beta fexp2 x *)
assert (NF1x : ~ generic_format beta fexp1 x).
{ now intro H; apply NF2x, (generic_inclusion_ln_beta _ fexp1). }
destruct (Rle_or_lt x (midp beta fexp1 x)) as [H1|H1].
- (* x < midp fexp1 x *)
assert (H1' : x < midp beta fexp1 x) by lra.
destruct (Rlt_or_le x (midp beta fexp1 x - / 2 * ulp beta fexp2 x))
as [H2|H2].
+ (* x < midp fexp1 x - / 2 * ulp beta fexp2 x *)
now apply double_round_lt_mid.
+ (* midp fexp1 x - / 2 * ulp beta fexp2 x <= x *)
now apply neq_midpoint_beta_odd_aux1; [| | | |split].
- (* midp fexp1 x < x *)
assert (Hm : midp' beta fexp1 x = midp beta fexp1 x).
{ now unfold midp', midp; rewrite ulp_DN_UP; [field|]. }
destruct (Zle_or_lt (fexp1 (ln_beta x)) (fexp2 (ln_beta x))) as [H3|H3].
+ (* fexp2 (ln_beta x) = fexp1 (ln_beta x) *)
assert (H3' : fexp2 (ln_beta x) = fexp1 (ln_beta x));
[now apply Zle_antisym|].
now apply double_round_gt_mid_same_place; [| | |rewrite Hm].
+ (* fexp2 (ln_beta x) < fexp1 (ln_beta x) *)
destruct (Rlt_or_le (midp beta fexp1 x + / 2 * ulp beta fexp2 x) x)
as [H2|H2].
* (* midp fexp1 x + / 2 * ulp beta fexp2 x < x *)
now apply double_round_gt_mid_further_place; [| | |omega| |rewrite Hm].
* (* x <= midp fexp1 x + / 2 * ulp beta fexp2 x *)
now apply neq_midpoint_beta_odd_aux2; [| | | |split].
Qed.
(* neq_midpoint_beta_odd_aux3 without the hypothesis
fexp1 (ln_beta x) <= ln_beta x *)
Lemma neq_midpoint_beta_odd :
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 ->
x <> midp beta fexp1 x ->
double_round_eq beta fexp1 fexp2 choice1 choice2 x.
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx.
destruct (Zle_or_lt (fexp1 (ln_beta x)) (ln_beta x)) as [H1|H1].
{ (* fexp1 (ln_beta x) <= ln_beta x *)
now apply neq_midpoint_beta_odd_aux3