proposition: Lemma avg_half_sub_between_aux: forall u v, format u -> format v -> u <= v -> u <= avg_half_sub u v <= v.
proof: Proof. Proof with auto with typeclass_instances. clear Fx Fy a av x y. intros x y Fx Fy M. split. apply round_ge_generic... apply Rplus_le_reg_l with (-x). ring_simplify. apply round_ge_generic... apply generic_format_0. unfold Rdiv; apply Rmult_le_pos. apply round_ge_generic... apply generic_format_0. apply Rplus_le_reg_l with x. now ring_simplify. lra. apply round_le_generic... assert (H:(0 <= round radix2 (FLT_exp emin prec) Zfloor (y-x))). apply round_ge_generic... apply generic_format_0. apply Rplus_le_reg_l with x. now ring_simplify. destruct H as [H|H]. pattern y at 2; replace y with (x + (y-x)) by ring. apply Rplus_le_compat_l. case (generic_format_EM radix2 (FLT_exp emin prec) (y-x)); intros K. apply round_le_generic... rewrite round_generic... apply Rmult_le_reg_l with (1 := Rlt_0_2). apply Rplus_le_reg_l with (2*x-y). apply Rle_trans with x. right; field. apply Rle_trans with (1:=M). right; field. apply Rle_trans with (round radix2 (FLT_exp emin prec) Zfloor (y - x)). apply round_le_generic... apply generic_format_round... apply Rmult_le_reg_l with (1 := Rlt_0_2). apply Rle_trans with (round_flt (y - x)). right; field. case (round_DN_or_UP radix2 (FLT_exp emin prec) ZnearestE (y-x)); intros H1; rewrite H1. apply Rplus_le_reg_l with (-round radix2 (FLT_exp emin prec) Zfloor (y - x)). ring_simplify. now left. rewrite round_UP_DN_ulp. apply Rplus_le_reg_l with (-round radix2 (FLT_exp emin prec) Zfloor (y - x)); ring_simplify. apply round_DN_pt... apply generic_format_ulp... case (Rle_or_lt (bpow (emin + prec - 1)) (y-x)); intros P. apply FLT_ulp_le_id... apply Rle_trans with (2:=P). apply bpow_le; unfold Prec_gt_0 in prec_gt_0_; lia. contradict K. apply FLT_format_plus_small... now apply generic_format_opp. rewrite Rabs_right. apply Rle_trans with (bpow (emin+prec-1)). left; exact P. apply bpow_le; lia. apply Rle_ge; apply Rplus_le_reg_l with x; now ring_simplify. assumption. apply round_DN_pt... case M; intros H1. 2: rewrite H1; replace (y-y) with 0 by ring. 2: rewrite round_0... 2: unfold Rdiv; rewrite Rmult_0_l. 2: rewrite round_0... 2: right; ring. apply Rle_trans with (x+0). 2: rewrite Rplus_0_r; assumption. apply Rplus_le_compat_l. replace 0 with (round_flt (bpow emin/2)). apply round_le... unfold Rdiv; apply Rmult_le_compat_r. lra. apply round_le_generic... apply generic_format_FLT_bpow... lia. case (Rle_or_lt (y-x) (bpow emin)); trivial. intros H2. contradict H. apply Rlt_not_eq. apply Rlt_le_trans with (bpow emin). apply bpow_gt_0. apply round_DN_pt... apply generic_format_FLT_bpow... lia. now left. replace (bpow emin /2) with (bpow (emin-1)). unfold round, scaled_mantissa, cexp, FLT_exp. rewrite mag_bpow. replace (emin - 1 + 1 - prec)%Z with (emin-prec)%Z by ring. rewrite Z.max_r. 2: unfold Prec_gt_0 in prec_gt_0_; lia. rewrite <- bpow_plus. replace (emin-1+-emin)%Z with (-1)%Z by ring. replace (ZnearestE (bpow (-1))) with 0%Z. unfold F2R; simpl; ring. change (bpow (-1)) with (/2). simpl; unfold Znearest. replace (Zfloor (/2)) with 0%Z. rewrite Rcompare_Eq. reflexivity. simpl; ring. apply sym_eq, Zfloor_imp. simpl ; lra. unfold Zminus; rewrite bpow_plus. reflexivity. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)