proposition: Lemma round_round_minus_beta_odd_aux2 : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), (forall ex, (fexp2 ex <= fexp1 ex)%Z) -> forall x y, 0 <= x -> 0 <= y -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> round_round_eq beta fexp1 fexp2 choice1 choice2 (x - y).
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hfexp x y Nnx Nny Fx Fy. destruct (Req_dec x 0) as [Zx|Nzx]; destruct (Req_dec y 0) as [Zy|Nzy]. - unfold round_round_eq. unfold Rminus. now rewrite Zx, Zy, Rplus_0_l, Ropp_0, round_0; [|apply valid_rnd_N]. - assert (Py : 0 < y); [lra|]. unfold Rminus; rewrite Zx, Rplus_0_l. unfold round_round_eq; do 3 rewrite round_N_opp; apply f_equal. apply (neq_midpoint_beta_odd _ _ Vfexp1 Vfexp2 _ _ _ Py (Hfexp _)). rewrite Fy; unfold F2R, scaled_mantissa; simpl. apply float_neq_midpoint_beta_odd. apply Rmult_lt_reg_r with (bpow (cexp beta fexp1 y)). apply bpow_gt_0. rewrite Rmult_0_l; apply Rlt_le_trans with (1:=Py). right; rewrite Fy at 1; unfold F2R, scaled_mantissa; now simpl. - assert (Px : 0 < x); [lra|]. unfold Rminus; rewrite Zy, Ropp_0, Rplus_0_r. apply (neq_midpoint_beta_odd _ _ Vfexp1 Vfexp2 _ _ _ Px (Hfexp _)). rewrite Fx; unfold F2R, scaled_mantissa; simpl. apply float_neq_midpoint_beta_odd. apply Rmult_lt_reg_r with (bpow (cexp beta fexp1 x)). apply bpow_gt_0. rewrite Rmult_0_l; apply Rlt_le_trans with (1:=Px). right; rewrite Fx at 1; unfold F2R, scaled_mantissa; now simpl. - assert (Px : 0 < x); [lra|]. assert (Py : 0 < y); [lra|]. destruct (Rtotal_order x y) as [Hxy|[Hxy|Hxy]]. + replace (x - y) with (- (y - x)) by ring. unfold round_round_eq; do 3 rewrite round_N_opp; apply f_equal. now apply round_round_minus_beta_odd_aux1. + unfold round_round_eq. now rewrite (Rminus_diag_eq _ _ Hxy), round_0; [|apply valid_rnd_N]. + now apply round_round_minus_beta_odd_aux1. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)