Commit 6b980516 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Factor definitions of radix2. Simplify and move Z_of_nat_S_digits2_Pnat.

parent e2f7eefe
......@@ -102,8 +102,6 @@ Definition B2FF x :=
| B754_nan b (exist pl _) => F754_nan b pl
end.
Definition radix2 := Build_radix 2 (refl_equal true).
Definition B2R f :=
match f with
| B754_finite s m e _ => F2R (Float radix2 (cond_Zopp s (Zpos m)) e)
......@@ -445,7 +443,6 @@ apply bpow_le.
rewrite H. 2: discriminate.
revert H1. clear -H2.
rewrite Z_of_nat_S_digits2_Pnat.
change Fcalc_digits.radix2 with radix2.
unfold fexp, FLT_exp.
generalize (Zdigits radix2 (Zpos mx)).
intros ; zify ; subst.
......@@ -475,7 +472,6 @@ unfold canonic_mantissa.
unfold canonic, Fexp in Cx.
rewrite Cx at 2.
rewrite Z_of_nat_S_digits2_Pnat.
change Fcalc_digits.radix2 with radix2.
unfold canonic_exp.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
now apply -> Zeq_is_eq_bool.
......@@ -853,7 +849,6 @@ rewrite Zle_bool_refl.
rewrite Bool.andb_true_r.
apply Zeq_bool_true.
rewrite Z_of_nat_S_digits2_Pnat.
change Fcalc_digits.radix2 with radix2.
replace (Zdigits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec.
unfold fexp, FLT_exp, emin.
generalize (prec_gt_0 prec).
......
......@@ -219,7 +219,6 @@ unfold canonic_mantissa in Hx'.
rewrite Z_of_nat_S_digits2_Pnat in Hx'.
generalize (Zeq_bool_eq _ _ Hx').
unfold FLT_exp.
change (Fcalc_digits.radix2) with radix2.
unfold emin.
clear ; zify ; omega.
destruct (Zle_bool_spec (2^mw) (Zpos mx)) as [H|H] ;
......@@ -496,7 +495,6 @@ destruct (andb_prop _ _ Bx) as (H1, _).
generalize (Zeq_bool_eq _ _ H1).
rewrite Z_of_nat_S_digits2_Pnat.
unfold FLT_exp, emin.
change Fcalc_digits.radix2 with radix2.
generalize (Zdigits radix2 (Zpos mx)).
clear.
intros ; zify ; omega.
......@@ -508,7 +506,6 @@ destruct (andb_prop _ _ Bx) as (H1, _).
generalize (Zeq_bool_eq _ _ H1).
rewrite Z_of_nat_S_digits2_Pnat.
unfold FLT_exp, emin, prec.
change Fcalc_digits.radix2 with radix2.
generalize (Zdigits_le_Zpower radix2 _ (Zpos mx) Hm).
generalize (Zdigits radix2 (Zpos mx)).
clear.
......
......@@ -61,27 +61,3 @@ now apply Zdigits_ln_beta.
Qed.
End Fcalc_digits.
Definition radix2 := Build_radix 2 (refl_equal _).
Theorem Z_of_nat_S_digits2_Pnat :
forall m : positive,
Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m).
Proof.
intros m.
rewrite Zdigits_ln_beta. 2: easy.
apply sym_eq.
apply ln_beta_unique.
generalize (digits2_Pnat m) (digits2_Pnat_correct m).
intros d H.
simpl in H.
replace (Z_of_nat (S d) - 1)%Z with (Z_of_nat d).
rewrite <- Z2R_abs.
rewrite <- 2!Z2R_Zpower_nat.
split.
now apply Z2R_le.
now apply Z2R_lt.
rewrite inj_S.
apply Zpred_succ.
Qed.
......@@ -233,6 +233,8 @@ apply f_equal.
apply eqbool_irrelevance.
Qed.
Definition radix2 := Build_radix 2 (refl_equal _).
Variable r : radix.
Theorem radix_gt_0 : (0 < r)%Z.
......
......@@ -746,7 +746,6 @@ Qed.
Section digits_aux.
Variable p : Z.
Hypothesis Hp : (0 <= p)%Z.
Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z :=
match n with
......@@ -1126,3 +1125,21 @@ now rewrite <- (Zabs_eq m) at 1.
Qed.
End Fcore_digits.
Section Zdigits2.
Theorem Z_of_nat_S_digits2_Pnat :
forall m : positive,
Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m).
Proof.
intros m.
apply eq_sym, Zdigits_unique.
rewrite <- Zpower_nat_Z.
rewrite Nat2Z.inj_succ.
change (_ - 1)%Z with (Zpred (Zsucc (Z.of_nat (digits2_Pnat m)))).
rewrite <- Zpred_succ.
rewrite <- Zpower_nat_Z.
apply digits2_Pnat_correct.
Qed.
End Zdigits2.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment