proposition: Lemma float10_of_pos_correct : forall x, float10R (float10_of_pos x) = IZR (Zpos x).
proof: Proof. intros x. unfold float10_of_pos. rewrite <- (Rmult_1_r (IZR (Zpos x))). change (IZR (Zpos x) * 1)%R with (float10R (Float10 (Zpos x) 0%Z)). generalize (Digits.digits2_Pnat x) 0%Z. intros n. revert x. induction n ; intros m e. easy. destruct m as [m|m|] ; try easy. generalize (Z.pos_div_eucl_eq m 5 eq_refl). destruct Z.pos_div_eucl as [q r]. intros Hm. destruct r as [|r|r] ; try easy. destruct q as [|q|q] ; try easy. rewrite IHn. rewrite Pos2Z.pos_xO, Hm. replace (2 * (Zpos q * 5 + 0))%Z with (Zpos q * 10)%Z by ring. unfold float10R, F2R. simpl. unfold Z.succ. rewrite Zplus_comm. rewrite bpow_plus, <- Rmult_assoc. change (Zpos (q * 10)) with (Zpos q * 10)%Z. now rewrite mult_IZR. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library