proposition: Lemma round_round_minus_beta_odd_aux1 : 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 -> y < x -> 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 Px Py Hxy Fx Fy. apply neq_midpoint_beta_odd; try assumption. - now apply Rlt_Rminus. - apply Hfexp. - intro Hxy'. revert Fx Fy. unfold generic_format, F2R, scaled_mantissa, cexp; simpl. set (mx := Ztrunc (x * bpow (- fexp1 (mag x)))). set (my := Ztrunc (y * bpow (- fexp1 (mag y)))). set (ex := mag x). set (ey := mag y). intros Fx Fy. revert Hxy'. rewrite Fx, Fy. destruct (Zle_or_lt (fexp1 ex) (fexp1 ey)) as [Hexy|Hexy]. + replace (fexp1 ey) with (fexp1 ey - fexp1 ex + fexp1 ex)%Z by ring. rewrite bpow_plus, <- Rmult_assoc, <- Rmult_minus_distr_r. rewrite <- IZR_Zpower; [|now apply Zle_minus_le_0]. rewrite <- mult_IZR, <- minus_IZR. apply float_neq_midpoint_beta_odd. apply (Rmult_lt_reg_r (bpow (fexp1 ex))); [now apply bpow_gt_0|]. rewrite minus_IZR, mult_IZR, IZR_Zpower; [|now apply Zle_minus_le_0]. rewrite Rmult_0_l, Rmult_minus_distr_r; bpow_simplify. rewrite <- Fx, <- Fy. now apply Rlt_Rminus. + replace (fexp1 ex) with (fexp1 ex - fexp1 ey + fexp1 ey)%Z by ring. rewrite bpow_plus, <- Rmult_assoc, <- Rmult_minus_distr_r. rewrite <- IZR_Zpower by lia. rewrite <- mult_IZR, <- minus_IZR. apply float_neq_midpoint_beta_odd. apply (Rmult_lt_reg_r (bpow (fexp1 ey))); [now apply bpow_gt_0|]. rewrite minus_IZR, mult_IZR, IZR_Zpower by lia. rewrite Rmult_0_l, Rmult_minus_distr_r; bpow_simplify. rewrite <- Fx, <- Fy. now apply Rlt_Rminus. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)