proposition: Theorem output_bnd_correct : forall fmt radix s m e, (Interval.convert_bound (output_bnd fmt false radix s m e) <= FtoR radix s m e)%R /\ (FtoR radix s m e <= Interval.convert_bound (output_bnd fmt true radix s m e))%R.
proof: Proof. intros fmt radix s m e. assert (Hd: forall a b c d, (0 < b)%Z -> (0 < d)%Z -> (a * d <= b * c)%Z -> (IZR a / IZR b <= IZR c/ IZR d)%R). { intros a b c d Hb Hd H. apply Rcomplements.Rle_div_l. now apply IZR_lt. unfold Rdiv. rewrite Rmult_assoc, <- (Rmult_comm (IZR b)), <- Rmult_assoc. apply Rcomplements.Rle_div_r. now apply IZR_lt. rewrite <- 2!mult_IZR. apply IZR_le. now rewrite <- (Zmult_comm b). } unfold output_bnd. destruct (andb fmt (Zeq_bool (Zaux.radix_val radix) 2)) eqn:Hr. 2: destruct e ; (try rewrite Zaux.Zfast_pow_pos_correct) ; split ; apply Rle_refl. destruct fmt. 2: easy. destruct e as [|e|e]. split ; apply Rle_refl. rewrite Zaux.Zfast_pow_pos_correct ; split ; apply Rle_refl. unfold FtoR. set (sm := if s then Z.neg m else Z.pos m). set (e'' := (Zpos e * 3 / 10)%Z). set (e' := Z.to_pos e''). apply Zeq_is_eq_bool in Hr. assert (He1: (0 <= Zpos e - Zpos e')%Z). { apply Zle_minus_le_0. destruct e'' as [|p|p] eqn:He ; try now apply (Zlt_le_succ 0). unfold e'. simpl. rewrite <- He. apply Z.div_le_upper_bound. easy. rewrite Zmult_comm. now apply Zmult_le_compat_r. } assert (He2: (2 ^ (Z.pos e - Zpos e') > 0)%Z). { apply Z.lt_gt. now apply (Zaux.Zpower_gt_0 Zaux.radix2). } assert (He3: (0 <= Zpos e')%Z) by easy. rewrite Zaux.Zfast_pow_pos_correct. generalize (Zdiv.Z_div_mod (sm * Z.pow_pos 5 e') (2 ^ (Zpos e - Zpos e')) He2). set (qr := Z.div_eucl (sm * Z.pow_pos 5 e') (2 ^ (Zpos e - Zpos e'))). rewrite Hr. destruct qr as [q r]. intros [H1 H2]. rewrite Zaux.Zfast_pow_pos_correct. rewrite Z2Pos.inj_pow_pos by easy. simpl. assert (H3: (sm * 10 ^ Zpos e' = 2 ^ (Zpos e) * q + r * 2 ^ Zpos e')%Z). { change 10%Z with (2 * 5)%Z. rewrite Z.pow_mul_l. rewrite <- (Zmult_comm (5 ^ Zpos e')), Zmult_assoc. unfold Z.pow at 1. rewrite H1. pattern (Zpos e) at 2 ; replace (Zpos e) with (Zpos e - Zpos e' + Zpos e')%Z by ring. rewrite Z.pow_add_r ; try easy. ring. } split. - apply Hd. easy. now apply (Zaux.Zpower_gt_0 radix2 (Zpos e)). unfold QArith_base.Qnum, QArith_base.Qden. rewrite Pos2Z.inj_pow. rewrite <- (Zmult_comm sm), H3. rewrite Zplus_0_r, Zmult_comm. rewrite <- (Zplus_0_r (Z.pow_pos 2 e * q)). apply Zplus_le_compat_l. apply Z.mul_nonneg_nonneg. easy. apply (Zaux.Zpower_ge_0 radix2). - apply Hd. now apply (Zaux.Zpower_gt_0 radix2 (Zpos e)). easy. unfold QArith_base.Qnum, QArith_base.Qden. rewrite Pos2Z.inj_pow. rewrite H3. rewrite Z.mul_add_distr_l. apply Zplus_le_compat_l. generalize (Zeq_bool_if r 0). destruct Zeq_bool. intros ->. now rewrite Zmult_0_l, Zmult_0_r. intros _. rewrite Zmult_1_r. change (Z.pow_pos 2 e) with (Z.pow 2 (Zpos e)). replace (Zpos e) with (Zpos e - Zpos e' + Zpos e')%Z by ring. rewrite Z.pow_add_r by easy. apply Zmult_le_compat_r. now apply Zlt_le_weak. apply (Zaux.Zpower_ge_0 radix2). Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval