proposition: Lemma FLT_round_half: forall z, bpow (prec+emin) <= Rabs z -> round_flt (z/2)= round_flt z /2.
proof: Proof. Proof with auto with typeclass_instances. intros z Hz. apply Rmult_eq_reg_l with 2. 2: apply sym_not_eq; auto with real. apply trans_eq with (round_flt z). 2: field. assert (z <> 0)%R. intros K; contradict Hz. rewrite K, Rabs_R0; apply Rlt_not_le. apply bpow_gt_0. assert (cexp (z/2) = cexp z -1)%Z. assert (prec+emin < mag radix2 z)%Z. apply lt_bpow with radix2. destruct mag as (e,He); simpl. apply Rle_lt_trans with (1:=Hz). now apply He. unfold cexp, FLT_exp. replace ((mag radix2 (z/2))-prec)%Z with ((mag radix2 z -1) -prec)%Z. rewrite Z.max_l; lia. apply Zplus_eq_compat; try reflexivity. apply sym_eq, mag_unique. destruct (mag radix2 z) as (e,He); simpl. unfold Rdiv; rewrite Rabs_mult. rewrite (Rabs_right (/2)). split. apply Rmult_le_reg_l with (bpow 1). apply bpow_gt_0. rewrite <- bpow_plus. replace (1+(e-1-1))%Z with (e-1)%Z by ring. apply Rle_trans with (Rabs z). now apply He. change (bpow 1) with 2%R. right; simpl; field. apply Rmult_lt_reg_l with (bpow 1). apply bpow_gt_0. rewrite <- bpow_plus. replace (1+(e-1))%Z with e by ring. apply Rle_lt_trans with (Rabs z). change (bpow 1) with 2. right; field. now apply He. lra. unfold round, scaled_mantissa, F2R. rewrite H0; simpl. rewrite Rmult_comm, Rmult_assoc. apply f_equal2. apply f_equal, f_equal. replace (-(cexp z -1))%Z with (-cexp z +1)%Z by ring. rewrite bpow_plus. change (bpow 1) with 2. field. unfold Zminus; rewrite bpow_plus. change (bpow (-(1))) with (/2). field. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)