proposition: Lemma avg_sum_half_correct: bpow (emin +prec+prec+1) <= Rabs x -> av2 = round_flt a.
proof: Proof. Proof with auto with typeclass_instances. intros Hx. assert (G:(0 < prec)%Z). unfold Prec_gt_0 in prec_gt_0_; assumption. unfold av2, avg_sum_half. replace (round_flt (x/2)) with (x/2). 2: apply sym_eq, round_generic... 2: apply FLT_format_half; try assumption. 2: apply Rle_trans with (2:=Hx). 2: apply bpow_le; lia. case (Rle_or_lt (bpow (prec + emin)) (Rabs y)). intros Hy. replace (round_flt (y/2)) with (y/2). apply f_equal; unfold a; field. apply sym_eq, round_generic... apply FLT_format_half; assumption. intros Hy. assert (format (x/2)). apply FLT_format_half. assumption. apply Rle_trans with (2:=Hx). apply bpow_le. lia. assert (bpow (prec+emin) <= Rabs (x/2)). apply Rmult_le_reg_l with (bpow 1). apply bpow_gt_0. rewrite <- bpow_plus. apply Rle_trans with (Rabs x). apply Rle_trans with (2:=Hx). apply bpow_le. lia. rewrite <- (Rabs_right (bpow 1)). rewrite <- Rabs_mult. right; apply f_equal. change (bpow 1) with 2. field. apply Rle_ge, bpow_ge_0. assert (K1: Rabs (y / 2) <= bpow (prec+emin-1)). unfold Rdiv; rewrite Rabs_mult. unfold Zminus; rewrite bpow_plus. simpl; rewrite (Rabs_pos_eq (/2)). apply (Rmult_le_compat_r (/2)). lra. now left. lra. assert (K2:bpow (prec+emin-1) <= / 4 * ulp_flt (x / 2)). assert (Z: x/2 <> 0). intros K; contradict H0. rewrite K, Rabs_R0. apply Rlt_not_le, bpow_gt_0. rewrite ulp_neq_0; trivial. replace (/4) with (bpow (-2)) by reflexivity. rewrite <- bpow_plus. apply bpow_le. unfold cexp, FLT_exp. assert (emin+prec+prec+1 -1 < mag radix2 (x/2))%Z. destruct (mag radix2 (x/2)) as (e,He). simpl. apply lt_bpow with radix2. apply Rle_lt_trans with (Rabs (x/2)). unfold Rdiv; rewrite Rabs_mult. unfold Zminus; rewrite bpow_plus. simpl; rewrite (Rabs_right (/2)). apply Rmult_le_compat_r. lra. exact Hx. lra. apply He; trivial. rewrite Z.max_l. lia. lia. apply trans_eq with (x/2). apply round_plus_small_id; try assumption. apply Rle_trans with (2:=K2). apply abs_round_le_generic... apply generic_format_FLT_bpow... lia. unfold a; apply sym_eq. replace ((x+y)/2) with (x/2+y/2) by field. apply round_plus_small_id; try assumption. now apply Rle_trans with (2:=K2). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)