proposition: Theorem Fscale2_correct : forall beta (f : float beta) d, match radix_val beta with Zpos (xO _) => true | _ => false end = true -> FtoX (Fscale2 f d) = Xmul (FtoX f) (Xreal (bpow radix2 d)).
proof: Proof. intros beta [| |s m e] d Hb ; simpl. apply refl_equal. now rewrite Rmult_0_l. revert Hb. destruct beta as (beta, Hb). simpl. destruct beta as [|[p|p|]|p] ; try easy. intros _. set (beta := Build_radix (Zpos p~0) Hb). cut (FtoX match d return (float beta) with | 0%Z => Float s m e | Zpos nb => Float s (iter_pos (fun x : positive => xO x) nb m) e | Zneg nb => Float s (iter_pos (fun x : positive => Pmult p x) nb m) (e + d) end = Xreal (FtoR beta s m e * bpow radix2 d)). intro H. destruct p as [p|p|] ; try exact H. unfold FtoX. rewrite 2!FtoR_split. unfold F2R. simpl. now rewrite bpow_plus, Rmult_assoc. destruct d as [|nb|nb]. now rewrite Rmult_1_r. unfold FtoX. apply f_equal. rewrite 2!FtoR_split. simpl. replace (IZR (Zpower_pos 2 nb)) with (F2R (Defs.Float beta (Zpower_pos 2 nb) 0)). 2: apply Rmult_1_r. rewrite <- F2R_mult. simpl. rewrite Zplus_0_r. rewrite <- cond_Zopp_mult. apply (f_equal (fun v => F2R (Defs.Float beta (cond_Zopp s v) e))). apply (shift_correct radix2). unfold FtoX. apply f_equal. rewrite 2!FtoR_split. apply Rmult_eq_reg_r with (bpow radix2 (Zpos nb)). 2: apply Rgt_not_eq ; apply bpow_gt_0. rewrite Rmult_assoc, <- bpow_plus. change (Zneg nb) with (Z.opp (Zpos nb)). rewrite Zplus_opp_l, Rmult_1_r. fold (e - Zpos nb)%Z. simpl. replace (IZR (Zpower_pos 2 nb)) with (F2R (Defs.Float beta (Zpower_pos 2 nb) 0)). 2: apply Rmult_1_r. rewrite <- F2R_mult. simpl. rewrite Zplus_0_r. rewrite (F2R_change_exp beta (e - Zpos nb) _ e). 2: generalize (Zgt_pos_0 nb) ; clearbody beta ; lia. ring_simplify (e - (e - Zpos nb))%Z. rewrite <- 2!cond_Zopp_mult. apply (f_equal (fun v => F2R (Defs.Float beta (cond_Zopp s v) _))). rewrite Z.pow_pos_fold. rewrite iter_pos_nat. rewrite 2!Zpower_Zpower_nat by easy. simpl Z.abs_nat. unfold beta. simpl radix_val. clear. revert m. induction (nat_of_P nb). easy. intros m. rewrite iter_nat_S, 2!Zpower_nat_S. rewrite Zpos_mult_morphism. replace (Zpos m * (Zpos (xO p) * Zpower_nat (Zpos (xO p)) n))%Z with (Zpos m * Zpower_nat (Zpos (xO p)) n * Zpos (xO p))%Z by ring. rewrite <- IHn. change (Zpos (xO p)) with (2 * Zpos p)%Z. ring. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic