proposition: Lemma Bfrexp_correct_aux : forall sx mx ex (Hx : bounded mx ex = true), let x := F2R (Float radix2 (cond_Zopp sx (Z.pos mx)) ex) in let z := fst (Ffrexp_core_binary sx mx ex) in let e := snd (Ffrexp_core_binary sx mx ex) in valid_binary z = true /\ ((2 < emax)%Z -> (/2 <= Rabs (SF2R radix2 z) < 1)%R) /\ (x = SF2R radix2 z * bpow radix2 e)%R.
proof: Proof. intros sx mx ex Bx. set (x := F2R _). set (z := fst _). set (e := snd _); simpl. assert (Dmx_le_prec : (Z.pos (digits2_pos mx) <= prec)%Z). { revert Bx; unfold bounded; rewrite Bool.andb_true_iff. unfold canonical_mantissa; rewrite <-Zeq_is_eq_bool; unfold fexp, FLT_exp. case (Z.max_spec (Z.pos (digits2_pos mx) + ex - prec) emin); lia. } assert (Dmx_le_prec' : (digits2_pos mx <= Z.to_pos prec)%positive). { change (_ <= _)%positive with (Z.pos (digits2_pos mx) <= Z.pos (Z.to_pos prec))%Z. now rewrite Z2Pos.id; [|now apply prec_gt_0_]. } unfold z, e, Ffrexp_core_binary. case Z.ltb_spec ; intros Hp ; unfold emin in Hp. { apply (conj Bx). split. clear -Hp ; lia. now rewrite Rmult_1_r. } case (Pos.leb_spec _ _); simpl; intro Dmx. - unfold bounded, F2R; simpl. assert (Dmx' : digits2_pos mx = Z.to_pos prec). { now apply Pos.le_antisym. } assert (Dmx'' : Z.pos (digits2_pos mx) = prec). { now rewrite Dmx', Z2Pos.id; [|apply prec_gt_0_]. } split; [|split]. + apply andb_true_intro. split ; cycle 1. { apply Zle_bool_true. clear -Hp ; lia. } apply Zeq_bool_true; unfold fexp, FLT_exp. rewrite Dmx', Z2Pos.id by apply prec_gt_0_. rewrite Z.max_l. ring. clear -Hp. unfold emin ; lia. + intros _. rewrite Rabs_mult, (Rabs_pos_eq (bpow _ _)) by now apply bpow_ge_0. rewrite <-abs_IZR, abs_cond_Zopp; simpl; split. * apply (Rmult_le_reg_r (bpow radix2 prec)); [now apply bpow_gt_0|]. rewrite Rmult_assoc, <-bpow_plus, Z.add_opp_diag_l; simpl. rewrite Rmult_1_r. change (/ 2)%R with (bpow radix2 (- 1)); rewrite <-bpow_plus. rewrite <-Dmx'', Z.add_comm, Zpos_digits2_pos, Zdigits_mag; [|lia]. set (b := bpow _ _). rewrite <- (Rabs_pos_eq (IZR _)) by now apply IZR_le. now apply bpow_mag_le, IZR_neq. * apply (Rmult_lt_reg_r (bpow radix2 prec)); [now apply bpow_gt_0|]. rewrite Rmult_assoc, <-bpow_plus, Z.add_opp_diag_l; simpl. rewrite Rmult_1_l, Rmult_1_r. rewrite <-Dmx'', Zpos_digits2_pos, Zdigits_mag; [|lia]. set (b := bpow _ _). rewrite <- (Rabs_pos_eq (IZR _)) by now apply IZR_le. apply bpow_mag_gt. + rewrite Rmult_assoc, <- bpow_plus. now replace (_ + _)%Z with ex by ring. - unfold bounded, F2R; simpl. assert (Dmx' : (Z.pos (digits2_pos mx) < prec)%Z). { now rewrite <-(Z2Pos.id prec); [|now apply prec_gt_0_]. } split; [|split]. + unfold bounded; apply andb_true_intro. split ; cycle 1. { apply Zle_bool_true. clear -Hp ; lia. } apply Zeq_bool_true; unfold fexp, FLT_exp. rewrite Zpos_digits2_pos, shift_pos_correct, Z.pow_pos_fold. rewrite Z2Pos.id; [|lia]. rewrite Z.mul_comm; change 2%Z with (radix2 : Z). rewrite Zdigits_mult_Zpower; [|lia|lia]. rewrite Zpos_digits2_pos; replace (_ - _)%Z with (- prec)%Z by ring. now apply Z.max_l. + rewrite Rabs_mult, (Rabs_pos_eq (bpow _ _)); [|now apply bpow_ge_0]. rewrite <-abs_IZR, abs_cond_Zopp; simpl. rewrite shift_pos_correct, mult_IZR. change (IZR (Z.pow_pos _ _)) with (bpow radix2 (Z.pos (Z.to_pos ((prec - Z.pos (digits2_pos mx)))))). rewrite Z2Pos.id; [|lia]. rewrite Rmult_comm, <-Rmult_assoc, <-bpow_plus. set (d := Z.pos (digits2_pos mx)). replace (_ + _)%Z with (- d)%Z by ring; split. * apply (Rmult_le_reg_l (bpow radix2 d)); [now apply bpow_gt_0|]. rewrite <-Rmult_assoc, <-bpow_plus, Z.add_opp_diag_r. rewrite Rmult_1_l. change (/ 2)%R with (bpow radix2 (- 1)); rewrite <-bpow_plus. rewrite <- (Rabs_pos_eq (IZR _)) by now apply IZR_le. unfold d; rewrite Zpos_digits2_pos, Zdigits_mag; [|lia]. now apply bpow_mag_le, IZR_neq. * apply (Rmult_lt_reg_l (bpow radix2 d)); [now apply bpow_gt_0|]. rewrite <-Rmult_assoc, <-bpow_plus, Z.add_opp_diag_r. rewrite Rmult_1_l, Rmult_1_r. rewrite <- (Rabs_pos_eq (IZR _)) by now apply IZR_le. unfold d; rewrite Zpos_digits2_pos, Zdigits_mag; [|lia]. apply bpow_mag_gt. + rewrite Rmult_assoc, <-bpow_plus, shift_pos_correct. rewrite IZR_cond_Zopp, mult_IZR, cond_Ropp_mult_r, <-IZR_cond_Zopp. change (IZR (Z.pow_pos _ _)) with (bpow radix2 (Z.pos (Z.to_pos (prec - Z.pos (digits2_pos mx))))). rewrite Z2Pos.id; [|lia]. rewrite Rmult_comm, <-Rmult_assoc, <-bpow_plus. now replace (_ + _)%Z with ex by ring; rewrite Rmult_comm. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative