Make Zdigits_mult_Zpower axiom-free.

src/Calc/Fcalc_digits.v

@@ -29,8 +29,6 @@ Section Fcalc_digits.
 Variable beta : radix.
 Notation bpow e := (bpow beta e).
 
-
-
 Theorem Zdigits_ln_beta :
   forall n,
   n <> Z0 ->
@@ -62,35 +60,6 @@ apply sym_eq.
 now apply Zdigits_ln_beta.
 Qed.
 
-Theorem Zdigits_mult_Zpower :
-  forall m e,
-  m <> Z0 -> (0 <= e)%Z ->
-  Zdigits beta (m * Zpower beta e) = (Zdigits beta m + e)%Z.
-Proof.
-intros m e Hm He.
-rewrite <- ln_beta_F2R_Zdigits with (1 := Hm).
-rewrite Zdigits_ln_beta.
-rewrite Z2R_mult.
-now rewrite Z2R_Zpower with (1 := He).
-contradict Hm.
-apply Zmult_integral_l with (2 := Hm).
-apply neq_Z2R.
-rewrite Z2R_Zpower with (1 := He).
-apply Rgt_not_eq.
-apply bpow_gt_0.
-Qed.
-
-Theorem Zdigits_Zpower :
-  forall e,
-  (0 <= e)%Z ->
-  Zdigits beta (Zpower beta e) = (e + 1)%Z.
-Proof.
-intros e He.
-rewrite <- (Zmult_1_l (Zpower beta e)).
-rewrite Zdigits_mult_Zpower ; try easy.
-apply Zplus_comm.
-Qed.
-
 Theorem Zdigits_le :
   forall x y,
   (0 <= x)%Z -> (x <= y)%Z ->

src/Core/Fcore_digits.v

@@ -755,6 +755,7 @@ Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z :=
   end.
 
 End digits_aux.
+
 (** Number of digits of an integer *)
 Definition Zdigits n :=
   match n with
@@ -822,6 +823,20 @@ easy.
 apply Zle_succ_le with (1 := Hv).
 Qed.
 
+Theorem Zdigits_unique :
+  forall n d,
+  (Zpower beta (d - 1) <= Zabs n < Zpower beta d)%Z ->
+  Zdigits n = d.
+Proof.
+intros n d Hd.
+assert (Hd' := Zdigits_correct n).
+apply Zle_antisym.
+apply (Zpower_lt_Zpower beta).
+now apply Zle_lt_trans with (Zabs n).
+apply (Zpower_lt_Zpower beta).
+now apply Zle_lt_trans with (Zabs n).
+Qed.
+
 Theorem Zdigits_abs :
   forall n, Zdigits (Zabs n) = Zdigits n.
 Proof.
@@ -896,4 +911,39 @@ apply Zgt_not_eq.
 now apply Zpower_gt_0.
 Qed.
 
+Theorem Zdigits_mult_Zpower :
+  forall m e,
+  m <> Z0 -> (0 <= e)%Z ->
+  Zdigits (m * Zpower beta e) = (Zdigits m + e)%Z.
+Proof.
+intros m e Hm He.
+assert (H := Zdigits_correct m).
+apply Zdigits_unique.
+rewrite Z.abs_mul, Z.abs_pow, (Zabs_eq beta).
+2: now apply Zlt_le_weak, radix_gt_0.
+split.
+replace (Zdigits m + e - 1)%Z with (Zdigits m - 1 + e)%Z by ring.
+rewrite Zpower_plus with (2 := He).
+apply Zmult_le_compat_r.
+apply H.
+apply Zpower_ge_0.
+now apply Zlt_0_le_0_pred, Zdigits_gt_0.
+rewrite Zpower_plus with (2 := He).
+apply Zmult_lt_compat_r.
+now apply Zpower_gt_0.
+apply H.
+now apply Zlt_le_weak, Zdigits_gt_0.
+Qed.
+
+Theorem Zdigits_Zpower :
+  forall e,
+  (0 <= e)%Z ->
+  Zdigits (Zpower beta e) = (e + 1)%Z.
+Proof.
+intros e He.
+rewrite <- (Zmult_1_l (Zpower beta e)).
+rewrite Zdigits_mult_Zpower ; try easy.
+apply Zplus_comm.
+Qed.
+
 End Fcore_digits.