proposition: Lemma mantissa_digits_correct : forall x, valid_mantissa x -> EtoZ (mantissa_digits x) = Zpos (count_digits radix (MtoP x)).
proof: Proof. intros x (px, Vx). unfold mantissa_digits, EtoZ. simpl. rewrite BigN.spec_sub_pos. rewrite BigN.spec_Ndigits. rewrite <- digits_conversion. rewrite <- Zplus_0_r. rewrite <- (Zplus_opp_r (BigN.to_Z (BigN.head0 x)))%Z. rewrite Zplus_assoc. apply (f_equal (fun v => v + _)%Z). rewrite <- Zdigits_mult_Zpower. 2: now apply Zgt_not_eq. 2: apply BigN.spec_pos. refine (_ (BigN.spec_head0 x _)). 2: now rewrite Vx. intros (H1,H2). unfold MtoP. rewrite Vx. set (d := Zdigits radix (Zpos px * radix ^ (BigN.to_Z (BigN.head0 x)))). cut (d <= Zpos (BigN.digits x) /\ Zpos (BigN.digits x) - 1 < d)%Z. lia. unfold d ; clear d. split. apply Zdigits_le_Zpower. rewrite Zabs_Zmult, Zmult_comm. rewrite Z.abs_eq. simpl Z.abs. now rewrite <- Vx. apply Zpower_ge_0. apply Zdigits_gt_Zpower. rewrite Zabs_Zmult, Zmult_comm. rewrite Z.abs_eq. simpl Z.abs. now rewrite <- Vx. apply Zpower_ge_0. rewrite BigN.spec_Ndigits. assert (Zpower 2 (BigN.to_Z (BigN.head0 x)) * 1 < Zpower 2 (Zpos (BigN.digits x)))%Z. apply Z.le_lt_trans with (Zpower 2 (BigN.to_Z (BigN.head0 x)) * Zpos px)%Z. apply Zmult_le_compat_l. now case px. apply (Zpower_ge_0 radix2). rewrite <- Vx. apply BigN.spec_head0. now rewrite Vx. change (~ ((BigN.to_Z (BigN.head0 x)) > Zpos (BigN.digits x))%Z). intros H'. apply (Zlt_not_le _ _ H). rewrite Zmult_1_r. apply (Zpower_le radix2). apply Zlt_le_weak. now apply Z.gt_lt. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig