proposition: Lemma FLT_ulp_double: forall u, ulp_flt (2*u) <= 2*ulp_flt(u).
proof: Proof. intros u. case (Req_bool_spec u 0); intros Hu'. rewrite Hu', Rmult_0_r. rewrite <- (Rmult_1_l (ulp_flt 0)) at 1. apply Rmult_le_compat_r. apply ulp_ge_0. left; apply Rlt_plus_1. rewrite 2!ulp_neq_0; trivial. 2: lra. change 2 with (bpow 1) at 2. rewrite <- bpow_plus. apply bpow_le. case (Rle_or_lt (bpow (emin+prec-1)) (Rabs u)); intros Hu. rewrite cexp_FLT_FLX. rewrite cexp_FLT_FLX; trivial. unfold cexp, FLX_exp. change 2 with (bpow 1). rewrite Rmult_comm, mag_mult_bpow. lia. intros H; contradict Hu. apply Rlt_not_le; rewrite H, Rabs_R0. apply bpow_gt_0. apply Rle_trans with (1:=Hu). rewrite Rabs_mult. pattern (Rabs u) at 1; rewrite <- (Rmult_1_l (Rabs u)). apply Rmult_le_compat_r. apply Rabs_pos. rewrite <- (abs_IZR 2). now apply IZR_le. rewrite cexp_FLT_FIX. rewrite cexp_FLT_FIX; trivial. unfold FIX_exp, cexp; lia. apply Rlt_le_trans with (1:=Hu). apply bpow_le; lia. lra. rewrite Rabs_mult. rewrite Rabs_pos_eq. 2: now apply IZR_le. apply Rlt_le_trans with (2*bpow (emin + prec - 1)). apply Rmult_lt_compat_l with (1 := Rlt_0_2). assumption. change 2 with (bpow 1). rewrite <- bpow_plus. apply bpow_le; lia. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)