proposition: Lemma avg_half_sub_no_underflow_aux1: forall f, format f -> 0 < f -> f <= round_flt (f/2) -> False.
proof: Proof. Proof with auto with typeclass_instances. intros f Ff Hf1 Hf2. apply FLT_format_generic in Ff... destruct Ff as [g H1 H2 H3]. case (Zle_lt_or_eq emin (Fexp g)); try exact H3; intros H4. contradict Hf2. apply Rlt_not_le. rewrite round_generic... apply Rplus_lt_reg_l with (-(f/2)). apply Rle_lt_trans with 0;[right; ring|idtac]. apply Rlt_le_trans with (f*/2);[idtac|right;field]. apply Rmult_lt_0_compat; try assumption. lra. apply generic_format_FLT. exists (Float radix2 (Fnum g) (Fexp g-1)). rewrite H1; unfold F2R; simpl. unfold Zminus; rewrite bpow_plus. apply Rmult_assoc. easy. simpl; lia. contradict Hf2; apply Rlt_not_le. unfold round, scaled_mantissa. replace (cexp (f/2)) with emin. rewrite H1; unfold F2R; simpl. rewrite <- H4. apply Rmult_lt_compat_r. apply bpow_gt_0. apply IZR_lt. replace (IZR (Fnum g) * bpow emin / 2 * bpow (- emin)) with (IZR (Fnum g) /2). apply avg_half_sub_no_underflow_aux_aux. apply lt_IZR. apply Rmult_lt_reg_r with (bpow (Fexp g)). apply bpow_gt_0. rewrite Rmult_0_l. apply Rlt_le_trans with (1:=Hf1). right; rewrite H1; reflexivity. unfold Rdiv; apply trans_eq with (IZR (Fnum g) * / 2 * (bpow (- emin)*bpow emin)). rewrite <- bpow_plus. ring_simplify (-emin+emin)%Z. simpl; ring. ring. apply sym_eq, cexp_FLT_FIX. apply Rgt_not_eq, Rlt_gt. lra. rewrite H1; unfold F2R, Rdiv; simpl. replace (/2) with (bpow (-1)) by reflexivity. rewrite Rmult_assoc, <- bpow_plus. rewrite Rabs_mult. rewrite (Rabs_right (bpow _)). 2: apply Rle_ge, bpow_ge_0. rewrite (Zplus_comm emin _). rewrite (bpow_plus _ prec _). apply Rmult_lt_compat. apply Rabs_pos. apply bpow_ge_0. rewrite <- IZR_Zpower, <- abs_IZR. now apply IZR_lt. unfold Prec_gt_0 in prec_gt_0_; lia. rewrite <- H4; apply bpow_lt. lia. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)