proposition: Fact ex16 : forall (f : float r) rnd, Valid_rnd rnd -> exists m', round r phi rnd (F2R f) = F2R ({| Fnum := m'; Fexp := Fexp f |} : float r).
proof: Proof. intros [mx ex] rnd Vrnd. unfold round, scaled_mantissa. set (ex' := cexp r phi (F2R {| Fnum := mx; Fexp := ex |})). unfold F2R; simpl. destruct (Zle_or_lt ex' ex) as [ex'Lex | exLex']. exists mx. replace (IZR mx * bpow r ex * bpow r (- ex')) with (IZR (mx * r ^ (ex + - ex'))). destruct Vrnd as [_ HH]; rewrite HH. rewrite mult_IZR, IZR_Zpower, bpow_plus; try lia. rewrite bpow_opp; field. assert (HH1 := bpow_gt_0 r ex'); lra. rewrite mult_IZR, IZR_Zpower, bpow_plus; try lia; lra. exists ((rnd (IZR mx * bpow r (ex - ex'))%R) * Zpower r (ex' - ex))%Z. rewrite mult_IZR, IZR_Zpower; try lia. replace (IZR mx * bpow r ex * bpow r (- ex')) with (IZR mx * bpow r (ex - ex')). replace (bpow r ex') with (bpow r (ex + (ex' - ex))). rewrite bpow_plus; lra. replace (ex + (ex' - ex))%Z with ex'; try lia; auto. replace (ex - ex')%Z with (ex + -ex')%Z; try lia; auto. rewrite bpow_plus; lra. Qed.
imports: Psatz ZArith Reals Flocq(FTZ Core Operations)