Commit d250eacc authored by BOLDO Sylvie's avatar BOLDO Sylvie

WIP about namings (-> 2.0)

parent dae54a95
......@@ -31,13 +31,13 @@ Variable Hp : Zlt 0 prec.
(* FLX first - probably correct in FLTand maybe FTZ? *)
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
Notation cexp := (canonic_exp beta (FLX_exp prec)).
Notation ulp := (ulp beta (FLX_exp prec)).
Theorem pred_gt_0: forall f,
format f -> (0 < f)%R -> (0 < pred beta (FLX_exp prec) f)%R.
intros f Hf Zf.
unfold pred, Fcore_ulp.ulp, canonic_exponent, FLX_exp.
unfold pred, Fcore_ulp.ulp, canonic_exp, FLX_exp.
destruct (ln_beta beta f) as (ef,Hef).
simpl.
assert (Zf2: (f <>0)%R) by now apply Rgt_not_eq.
......
This diff is collapsed.
......@@ -19,6 +19,7 @@ COPYING file for more details.
(** * IEEE-754 encoding of binary floating-point data *)
Require Import Fcore.
Require Import Fcore_digits.
Require Import Fcalc_digits.
Require Import Fappli_IEEE.
......@@ -197,7 +198,7 @@ Proof.
intros [sx|sx| |sx mx ex Hx] ;
try ( simpl ; apply split_join_bits ; split ; try apply Zle_refl ; try apply Zlt_pred ; trivial ; omega ).
unfold bits_of_binary_float, split_bits_of_binary_float.
assert (Hf: (emin <= ex /\ digits radix2 (Zpos mx) <= prec)%Z).
assert (Hf: (emin <= ex /\ Zdigits radix2 (Zpos mx) <= prec)%Z).
destruct (andb_prop _ _ Hx) as (Hx', _).
unfold bounded_prec in Hx'.
rewrite Z_of_nat_S_digits2_Pnat in Hx'.
......@@ -213,7 +214,7 @@ split.
clear -He_gt_0 H ; omega.
cut (Zpos mx < 2 * 2^mw)%Z. clear ; omega.
replace (2 * 2^mw)%Z with (2^prec)%Z.
apply (Zpower_gt_digits radix2 _ (Zpos mx)).
apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)).
apply Hf.
unfold prec.
rewrite Zplus_comm.
......@@ -264,16 +265,16 @@ case Zeq_bool_spec ; intros He1.
case_eq (x mod 2^mw)%Z ; try easy.
(* subnormal *)
intros px Hm.
assert (digits radix2 (Zpos px) <= mw)%Z.
apply digits_le_Zpower.
assert (Zdigits radix2 (Zpos px) <= mw)%Z.
apply Zdigits_le_Zpower.
simpl.
rewrite <- Hm.
eapply Z_mod_lt.
now apply Zlt_gt.
apply bounded_canonic_lt_emax ; try assumption.
unfold canonic, canonic_exponent.
unfold canonic, canonic_exp.
fold emin.
rewrite ln_beta_F2R_digits. 2: discriminate.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold Fexp, FLT_exp.
apply sym_eq.
apply Zmax_right.
......@@ -283,7 +284,7 @@ apply Rnot_le_lt.
intros H0.
refine (_ (ln_beta_le radix2 _ _ _ H0)).
rewrite ln_beta_bpow.
rewrite ln_beta_F2R_digits. 2: discriminate.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold emin, prec.
apply Zlt_not_le.
cut (0 < emax)%Z. clear -H Hew ; omega.
......@@ -295,9 +296,9 @@ now case Zeq_bool.
case_eq (x mod 2^mw + 2^mw)%Z ; try easy.
(* normal *)
intros px Hm.
assert (prec = digits radix2 (Zpos px)).
assert (prec = Zdigits radix2 (Zpos px)).
(* . *)
rewrite digits_ln_beta. 2: discriminate.
rewrite Zdigits_ln_beta. 2: discriminate.
apply sym_eq.
apply ln_beta_unique.
rewrite <- Z2R_abs.
......@@ -321,8 +322,8 @@ eapply Z_mod_lt.
now apply Zlt_gt.
(* . *)
apply bounded_canonic_lt_emax ; try assumption.
unfold canonic, canonic_exponent.
rewrite ln_beta_F2R_digits. 2: discriminate.
unfold canonic, canonic_exp.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold Fexp, FLT_exp.
rewrite <- H.
set (ex := ((x / 2^mw) mod 2^ew)%Z).
......@@ -342,7 +343,7 @@ apply Rnot_le_lt.
intros H0.
refine (_ (ln_beta_le radix2 _ _ _ H0)).
rewrite ln_beta_bpow.
rewrite ln_beta_F2R_digits. 2: discriminate.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
rewrite <- H.
apply Zlt_not_le.
unfold emin.
......@@ -419,7 +420,7 @@ generalize (Zeq_bool_eq _ _ H1).
rewrite Z_of_nat_S_digits2_Pnat.
unfold FLT_exp, emin.
change Fcalc_digits.radix2 with radix2.
generalize (digits radix2 (Zpos mx)).
generalize (Zdigits radix2 (Zpos mx)).
clear.
intros ; zify ; omega.
(* . *)
......@@ -431,8 +432,8 @@ generalize (Zeq_bool_eq _ _ H1).
rewrite Z_of_nat_S_digits2_Pnat.
unfold FLT_exp, emin, prec.
change Fcalc_digits.radix2 with radix2.
generalize (digits_le_Zpower radix2 _ (Zpos mx) Hm).
generalize (digits radix2 (Zpos mx)).
generalize (Zdigits_le_Zpower radix2 _ (Zpos mx) Hm).
generalize (Zdigits radix2 (Zpos mx)).
clear.
intros ; zify ; omega.
Qed.
......
......@@ -73,7 +73,7 @@ apply sqrt_ge_0.
apply H2.
left.
unfold FLT_exp.
generalize (Zmax_spec (Fcalc_digits.digits beta ms + es - prec) emin).
generalize (Zmax_spec (Fcore_digits.Zdigits beta ms + es - prec) emin).
omega.
Qed.
......
......@@ -30,18 +30,12 @@ Section Fcalc_digits.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Notation digits := (Zdigits beta).
Theorem digits_abs :
forall n, digits (Zabs n) = digits n.
Proof.
now intros [|n|n].
Qed.
Theorem digits_ln_beta :
Theorem Zdigits_ln_beta :
forall n,
n <> Z0 ->
digits n = ln_beta beta (Z2R n).
Zdigits beta n = ln_beta beta (Z2R n).
Proof.
intros n Hn.
destruct (ln_beta beta (Z2R n)) as (e, He) ; simpl.
......@@ -58,35 +52,25 @@ rewrite <- Z2R_Zpower by omega.
now apply Z2R_lt.
Qed.
Theorem digits_ge_0 :
forall n, (0 <= digits n)%Z.
Proof.
intros n.
destruct (Z_eq_dec n 0) as [H|H].
now rewrite H.
apply Zlt_le_weak.
now apply Zdigits_gt_0.
Qed.
Theorem ln_beta_F2R_digits :
Theorem ln_beta_F2R_Zdigits :
forall m e, m <> Z0 ->
(ln_beta beta (F2R (Float beta m e)) = digits m + e :> Z)%Z.
(ln_beta beta (F2R (Float beta m e)) = Zdigits beta m + e :> Z)%Z.
Proof.
intros m e Hm.
rewrite ln_beta_F2R with (1 := Hm).
apply (f_equal (fun v => Zplus v e)).
apply sym_eq.
now apply digits_ln_beta.
now apply Zdigits_ln_beta.
Qed.
Theorem digits_shift :
Theorem Zdigits_mult_Zpower :
forall m e,
m <> Z0 -> (0 <= e)%Z ->
digits (m * Zpower beta e) = (digits m + e)%Z.
Zdigits beta (m * Zpower beta e) = (Zdigits beta m + e)%Z.
Proof.
intros m e Hm He.
rewrite <- ln_beta_F2R_digits with (1 := Hm).
rewrite digits_ln_beta.
rewrite <- ln_beta_F2R_Zdigits with (1 := Hm).
rewrite Zdigits_ln_beta.
rewrite Z2R_mult.
now rewrite Z2R_Zpower with (1 := He).
contradict Hm.
......@@ -97,26 +81,26 @@ apply Rgt_not_eq.
apply bpow_gt_0.
Qed.
Theorem digits_Zpower :
Theorem Zdigits_Zpower :
forall e,
(0 <= e)%Z ->
digits (Zpower beta e) = (e + 1)%Z.
Zdigits beta (Zpower beta e) = (e + 1)%Z.
Proof.
intros e He.
rewrite <- (Zmult_1_l (Zpower beta e)).
rewrite digits_shift ; try easy.
rewrite Zdigits_mult_Zpower ; try easy.
apply Zplus_comm.
Qed.
Theorem digits_le :
Theorem Zdigits_le :
forall x y,
(0 <= x)%Z -> (x <= y)%Z ->
(digits x <= digits y)%Z.
(Zdigits beta x <= Zdigits beta y)%Z.
Proof.
intros x y Hx Hxy.
case (Z_lt_le_dec 0 x).
clear Hx. intros Hx.
rewrite 2!digits_ln_beta.
rewrite 2!Zdigits_ln_beta.
apply ln_beta_le.
now apply (Z2R_lt 0).
now apply Z2R_le.
......@@ -125,23 +109,23 @@ now apply Zlt_le_trans with x.
now apply Zgt_not_eq.
intros Hx'.
rewrite (Zle_antisym _ _ Hx' Hx).
apply digits_ge_0.
apply Zdigits_ge_0.
Qed.
Theorem lt_digits :
Theorem lt_Zdigits :
forall x y,
(0 <= y)%Z ->
(digits x < digits y)%Z ->
(Zdigits beta x < Zdigits beta y)%Z ->
(x < y)%Z.
Proof.
intros x y Hy.
cut (y <= x -> digits y <= digits x)%Z. omega.
now apply digits_le.
cut (y <= x -> Zdigits beta y <= Zdigits beta x)%Z. omega.
now apply Zdigits_le.
Qed.
Theorem Zpower_le_digits :
Theorem Zpower_le_Zdigits :
forall e x,
(e < digits x)%Z ->
(e < Zdigits beta x)%Z ->
(Zpower beta e <= Zabs x)%Z.
Proof.
intros e x Hex.
......@@ -151,19 +135,19 @@ apply Zpower_le.
clear -Hex ; omega.
Qed.
Theorem digits_le_Zpower :
Theorem Zdigits_le_Zpower :
forall e x,
(Zabs x < Zpower beta e)%Z ->
(digits x <= e)%Z.
(Zdigits beta x <= e)%Z.
Proof.
intros e x.
generalize (Zpower_le_digits e x).
generalize (Zpower_le_Zdigits e x).
omega.
Qed.
Theorem Zpower_gt_digits :
Theorem Zpower_gt_Zdigits :
forall e x,
(digits x <= e)%Z ->
(Zdigits beta x <= e)%Z ->
(Zabs x < Zpower beta e)%Z.
Proof.
intros e x Hex.
......@@ -172,13 +156,13 @@ apply Zlt_le_trans with (1 := H2).
now apply Zpower_le.
Qed.
Theorem digits_gt_Zpower :
Theorem Zdigits_gt_Zpower :
forall e x,
(Zpower beta e <= Zabs x)%Z ->
(e < digits x)%Z.
(e < Zdigits beta x)%Z.
Proof.
intros e x Hex.
generalize (Zpower_gt_digits e x).
generalize (Zpower_gt_Zdigits e x).
omega.
Qed.
......@@ -188,10 +172,10 @@ This strong version is needed for proofs of division and square root
algorithms, since they involve operation remainders.
*)
Theorem digits_mult_strong :
Theorem Zdigits_mult_strong :
forall x y,
(0 <= x)%Z -> (0 <= y)%Z ->
(digits (x + y + x * y) <= digits x + digits y)%Z.
(Zdigits beta (x + y + x * y) <= Zdigits beta x + Zdigits beta y)%Z.
Proof.
intros x y Hx Hy.
case (Z_lt_le_dec 0 x).
......@@ -205,7 +189,7 @@ change Z0 with (0 + 0 + 0)%Z.
apply Zplus_lt_compat.
now apply Zplus_lt_compat.
now apply Zmult_lt_0_compat.
rewrite 3!digits_ln_beta ; try now (apply sym_not_eq ; apply Zlt_not_eq).
rewrite 3!Zdigits_ln_beta ; try now (apply sym_not_eq ; apply Zlt_not_eq).
apply ln_beta_le_bpow with (1 := Rgt_not_eq _ _ Hxy).
rewrite Rabs_pos_eq with (1 := Rlt_le _ _ Hxy).
destruct (ln_beta beta (Z2R x)) as (ex, Hex). simpl.
......@@ -248,37 +232,37 @@ rewrite Zmult_0_l, Zplus_0_r, 2!Zplus_0_l.
apply Zle_refl.
Qed.
Theorem digits_mult :
Theorem Zdigits_mult :
forall x y,
(digits (x * y) <= digits x + digits y)%Z.
(Zdigits beta (x * y) <= Zdigits beta x + Zdigits beta y)%Z.
Proof.
intros x y.
rewrite <- digits_abs.
rewrite <- (digits_abs x).
rewrite <- (digits_abs y).
apply Zle_trans with (digits (Zabs x + Zabs y + Zabs x * Zabs y)).
apply digits_le.
rewrite <- Zdigits_abs.
rewrite <- (Zdigits_abs _ x).
rewrite <- (Zdigits_abs _ y).
apply Zle_trans with (Zdigits beta (Zabs x + Zabs y + Zabs x * Zabs y)).
apply Zdigits_le.
apply Zabs_pos.
rewrite Zabs_Zmult.
generalize (Zabs_pos x) (Zabs_pos y).
omega.
apply digits_mult_strong ; apply Zabs_pos.
apply Zdigits_mult_strong ; apply Zabs_pos.
Qed.
Theorem digits_mult_ge :
Theorem Zdigits_mult_ge :
forall x y,
(x <> 0)%Z -> (y <> 0)%Z ->
(digits x + digits y - 1 <= digits (x * y))%Z.
(Zdigits beta x + Zdigits beta y - 1 <= Zdigits beta (x * y))%Z.
Proof.
intros x y Zx Zy.
cut ((digits x - 1) + (digits y - 1) < digits (x * y))%Z. omega.
apply digits_gt_Zpower.
cut ((Zdigits beta x - 1) + (Zdigits beta y - 1) < Zdigits beta (x * y))%Z. omega.
apply Zdigits_gt_Zpower.
rewrite Zabs_Zmult.
rewrite Zpower_exp.
apply Zmult_le_compat.
apply Zpower_le_digits.
apply Zpower_le_Zdigits.
apply Zlt_pred.
apply Zpower_le_digits.
apply Zpower_le_Zdigits.
apply Zlt_pred.
apply Zpower_ge_0.
apply Zpower_ge_0.
......@@ -286,11 +270,11 @@ generalize (Zdigits_gt_0 beta x). omega.
generalize (Zdigits_gt_0 beta y). omega.
Qed.
Theorem digits_shr :
Theorem Zdigits_div_Zpower :
forall m e,
(0 <= m)%Z ->
(0 <= e <= digits m)%Z ->
digits (m / Zpower beta e) = (digits m - e)%Z.
(0 <= e <= Zdigits beta m)%Z ->
Zdigits beta (m / Zpower beta e) = (Zdigits beta m - e)%Z.
Proof.
intros m e Hm He.
destruct (Zle_lt_or_eq 0 m Hm) as [Hm'|Hm'].
......@@ -298,13 +282,13 @@ destruct (Zle_lt_or_eq 0 m Hm) as [Hm'|Hm'].
destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He'].
(* . *)
unfold Zminus.
rewrite <- ln_beta_F2R_digits.
rewrite <- ln_beta_F2R_Zdigits.
2: now apply Zgt_not_eq.
assert (Hp: (0 < Zpower beta e)%Z).
apply lt_Z2R.
rewrite Z2R_Zpower with (1 := proj1 He).
apply bpow_gt_0.
rewrite digits_ln_beta.
rewrite Zdigits_ln_beta.
rewrite <- Zfloor_div with (1 := Zgt_not_eq _ _ Hp).
rewrite Z2R_Zpower with (1 := proj1 He).
unfold Rdiv.
......@@ -332,7 +316,7 @@ apply bpow_ge_0.
rewrite <- Z2R_Zpower with (1 := proj1 He).
apply Z2R_le.
rewrite <- Zabs_eq with (1 := Hm).
now apply Zpower_le_digits.
now apply Zpower_le_Zdigits.
apply Rgt_not_eq.
apply bpow_gt_0.
(* .. *)
......@@ -354,7 +338,7 @@ now apply Zgt_not_eq.
apply Z_div_le.
now apply Zlt_gt.
rewrite <- Zabs_eq with (1 := Hm).
now apply Zpower_le_digits.
now apply Zpower_le_Zdigits.
(* . *)
unfold Zminus.
rewrite He', Zplus_opp_r.
......@@ -362,7 +346,7 @@ rewrite Zdiv_small.
apply refl_equal.
apply conj with (1 := Hm).
pattern m at 1 ; rewrite <- Zabs_eq with (1 := Hm).
apply Zpower_gt_digits.
apply Zpower_gt_Zdigits.
apply Zle_refl.
(* *)
revert He.
......@@ -381,7 +365,7 @@ Theorem Z_of_nat_S_digits2_Pnat :
Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m).
Proof.
intros m.
rewrite digits_ln_beta. 2: easy.
rewrite Zdigits_ln_beta. 2: easy.
apply sym_eq.
apply ln_beta_unique.
generalize (digits2_Pnat m) (digits2_Pnat_correct m).
......@@ -397,4 +381,3 @@ rewrite inj_S.
apply Zpred_succ.
Qed.
Notation digits := Zdigits (only parsing).
......@@ -23,6 +23,7 @@ COPYING file for more details.
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Fcore_digits.
Require Import Fcalc_bracket.
Require Import Fcalc_digits.
......@@ -44,8 +45,8 @@ Complexity is fine as long as p1 <= 2p and p2 <= p.
*)
Definition Fdiv_core prec m1 e1 m2 e2 :=
let d1 := digits beta m1 in
let d2 := digits beta m2 in
let d1 := Zdigits beta m1 in
let d2 := Zdigits beta m2 in
let e := (e1 - e2)%Z in
let (m, e') :=
match (d2 + prec - d1)%Z with
......@@ -60,13 +61,13 @@ Theorem Fdiv_core_correct :
(0 < prec)%Z ->
(0 < m1)%Z -> (0 < m2)%Z ->
let '(m, e, l) := Fdiv_core prec m1 e1 m2 e2 in
(prec <= digits beta m)%Z /\
(prec <= Zdigits beta m)%Z /\
inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l.
Proof.
intros prec m1 e1 m2 e2 Hprec Hm1 Hm2.
unfold Fdiv_core.
set (d1 := digits beta m1).
set (d2 := digits beta m2).
set (d1 := Zdigits beta m1).
set (d2 := Zdigits beta m2).
case_eq
(match (d2 + prec - d1)%Z with
| Zpos p => ((m1 * Zpower_pos beta p)%Z, (e1 - e2 + Zneg p)%Z)
......@@ -74,7 +75,7 @@ case_eq
end).
intros m' e' Hme.
(* . the shifted mantissa m' has enough digits *)
assert (Hs: F2R (Float beta m' (e' + e2)) = F2R (Float beta m1 e1) /\ (0 < m')%Z /\ (d2 + prec <= digits beta m')%Z).
assert (Hs: F2R (Float beta m' (e' + e2)) = F2R (Float beta m1 e1) /\ (0 < m')%Z /\ (d2 + prec <= Zdigits beta m')%Z).
replace (d2 + prec)%Z with (d2 + prec - d1 + d1)%Z by ring.
destruct (d2 + prec - d1)%Z as [|p|p] ;
unfold d1 ;
......@@ -95,7 +96,7 @@ split.
apply Zmult_lt_0_compat.
exact Hm1.
now apply Zpower_gt_0.
rewrite digits_shift.
rewrite Zdigits_mult_Zpower.
rewrite Zplus_comm.
apply Zle_refl.
apply sym_not_eq.
......@@ -113,25 +114,25 @@ destruct (Zdiv_eucl m' m2) as (q, r).
intros (Hq, Hr).
split.
(* . the result mantissa q has enough digits *)
cut (digits beta m' <= d2 + digits beta q)%Z. omega.
cut (Zdigits beta m' <= d2 + Zdigits beta q)%Z. omega.
unfold d2.
rewrite Hq.
assert (Hq': (0 < q)%Z).
apply Zmult_lt_reg_r with (1 := Hm2).
assert (m2 < m')%Z.
apply lt_digits with beta.
apply lt_Zdigits with beta.
now apply Zlt_le_weak.
unfold d2 in Hs3.
clear -Hprec Hs3 ; omega.
cut (q * m2 = m' - r)%Z. clear -Hr H ; omega.
rewrite Hq.
ring.
apply Zle_trans with (digits beta (m2 + q + m2 * q)).
apply digits_le.
apply Zle_trans with (Zdigits beta (m2 + q + m2 * q)).
apply Zdigits_le.
rewrite <- Hq.
now apply Zlt_le_weak.
clear -Hr Hq'. omega.
apply digits_mult_strong ; apply Zlt_le_weak.
apply Zdigits_mult_strong ; apply Zlt_le_weak.
now apply Zle_lt_trans with r.
exact Hq'.
(* . the location is correctly computed *)
......
......@@ -65,29 +65,29 @@ Definition Fopp (f1: float beta) :=
let '(Float m1 e1) := f1 in
Float beta (-m1)%Z e1.
Theorem Fopp_F2R :
Theorem F2R_opp :
forall f1 : float beta,
(F2R (Fopp f1) = -F2R f1)%R.
unfold Fopp, F2R; intros (m1,e1).
simpl; rewrite Z2R_opp; ring.
intros (m1,e1).
apply F2R_Zopp.
Qed.
Definition Fabs (f1: float beta) :=
let '(Float m1 e1) := f1 in
Float beta (Zabs m1)%Z e1.
Theorem Fabs_F2R :
Theorem F2R_abs :
forall f1 : float beta,
(F2R (Fabs f1) = Rabs (F2R f1))%R.
intros (m1,e1).
apply F2R_abs.
apply F2R_Zabs.
Qed.
Definition Fplus (f1 f2 : float beta) :=
let '(m1, m2 ,e) := Falign f1 f2 in
Float beta (m1 + m2) e.
Theorem plus_F2R :
Theorem F2R_plus :
forall f1 f2 : float beta,
F2R (Fplus f1 f2) = (F2R f1 + F2R f2)%R.
Proof.
......@@ -125,12 +125,12 @@ Qed.
Definition Fminus (f1 f2 : float beta) :=
Fplus f1 (Fopp f2).
Theorem minus_F2R :
Theorem F2R_minus :
forall f1 f2 : float beta,
F2R (Fminus f1 f2) = (F2R f1 - F2R f2)%R.
Proof.
intros f1 f2; unfold Fminus.
rewrite plus_F2R, Fopp_F2R.
rewrite F2R_plus, F2R_opp.
ring.
Qed.
......@@ -148,7 +148,7 @@ Definition Fmult (f1 f2 : float beta) :=
let '(Float m2 e2) := f2 in
Float beta (m1 * m2) (e1 + e2).
Theorem mult_F2R :
Theorem F2R_mult :
forall f1 f2 : float beta,
F2R (Fmult f1 f2) = (F2R f1 * F2R f2)%R.
Proof.
......
This diff is collapsed.
......@@ -22,6 +22,7 @@ COPYING file for more details.
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_digits.
Require Import Fcore_float_prop.
Require Import Fcalc_bracket.
Require Import Fcalc_digits.
......@@ -151,7 +152,7 @@ Complexity is fine as long as p1 <= 2p-1.
*)
Definition Fsqrt_core prec m e :=
let d := digits beta m in
let d := Zdigits beta m in
let s := Zmax (2 * prec - d) 0 in
let e' := (e - s)%Z in
let (s', e'') := if Zeven e' then (s, e') else (s + 1, e' - 1)%Z in
......@@ -170,12 +171,12 @@ Theorem Fsqrt_core_correct :
forall prec m e,
(0 < m)%Z ->
let '(m', e', l) := Fsqrt_core prec m e in
(prec <= digits beta m')%Z /\
(prec <= Zdigits beta m')%Z /\
inbetween_float beta m' e' (sqrt (F2R (Float beta m e))) l.
Proof.
intros prec m e Hm.
unfold Fsqrt_core.
set (d := digits beta m).
set (d := Zdigits beta m).
set (s := Zmax (2 * prec - d) 0).
(* . exponent *)
case_eq (if Zeven (e - s) then (s, (e - s)%Z) else ((s + 1)%Z, (e - s - 1)%Z)).
......@@ -208,7 +209,7 @@ set (m' := match s' with
| Zpos p => (m * Zpower_pos beta p)%Z
| Zneg _ => m
end).
assert (Hs: F2R (Float beta m' e') = F2R (Float beta m e) /\ (2 * prec <= digits beta m')%Z /\ (0 < m')%Z).
assert (Hs: F2R (Float beta m' e') = F2R (Float beta m e) /\ (2 * prec <= Zdigits beta m')%Z /\ (0 < m')%Z).
rewrite <- He4.
unfold m'.
destruct s' as [|p|p].
......@@ -224,7 +225,7 @@ ring.
assert (0 < Zpos p)%Z by easy.
omega.
split.
rewrite digits_shift.
rewrite Zdigits_mult_Zpower.
fold d.
omega.
apply sym_not_eq.
......@@ -247,13 +248,13 @@ easy.
rewrite Zmult_comm.
apply Zle_trans with (1 := Hs2).
rewrite Hq.
apply Zle_trans with (digits beta (q + q + q * q)).
apply digits_le.
apply Zle_trans with (Zdigits beta (q + q + q * q)).
apply Zdigits_le.
rewrite <- Hq.
now apply Zlt_le_weak.
omega.
replace (digits beta q * 2)%Z with (digits beta q + digits beta q)%Z by ring.
apply digits_mult_strong.
replace (Zdigits beta q * 2)%Z with (Zdigits beta q + Zdigits beta q)%Z by ring.
apply Zdigits_mult_strong.
omega.
omega.
(* . round *)
......
......@@ -63,7 +63,7 @@ simpl in H2, H3.
rewrite H1.
apply generic_format_F2R.
intros Zmx.
unfold canonic_exponent, FLT_exp.
unfold canonic_exp, FLT_exp.
rewrite ln_beta_F2R with (1 := Zmx).
apply Zmax_lub with (2 := H3).
apply Zplus_le_reg_r with (prec - ex)%Z.
......@@ -76,7 +76,7 @@ Theorem FLT_format_generic :
Proof.
intros x.
unfold generic_format.
set (ex := canonic_exponent beta FLT_exp x).
set (ex := canonic_exp beta FLT_exp x).
set (mx := Ztrunc (scaled_mantissa beta FLT_exp x)).
intros Hx.
rewrite Hx.
......@@ -87,12 +87,12 @@ apply Rmult_lt_reg_r with (bpow ex).
apply bpow_gt_0.
rewrite <- bpow_plus.
change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R.
rewrite F2R_abs.
rewrite F2R_Zabs.
rewrite <- Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0, Rabs_R0.
apply bpow_gt_0.
unfold canonic_exponent in ex.
unfold canonic_exp in ex.
destruct (ln_beta beta x) as (ex', He).
simpl in ex.
specialize (He Hx0).
......@@ -117,10 +117,10 @@ Qed.
Theorem canonic_exp_FLT_FLX :
forall x, x <> R0 ->
(bpow (emin + prec - 1) <= Rabs x)%R ->
canonic_exponent beta FLT_exp x = canonic_exponent beta (FLX_exp prec) x.
canonic_exp beta FLT_exp x = canonic_exp beta (FLX_exp prec) x.
Proof.
intros x Hx0 Hx.
unfold canonic_exponent.
unfold canonic_exp.
apply Zmax_left.
destruct (ln_beta beta x) as (ex, He).
unfold FLX_exp. simpl.
......@@ -156,7 +156,7 @@ unfold generic_format in Hx; rewrite Hx.
apply generic_format_F2R.
intros _.
rewrite <- Hx.
unfold canonic_exponent, FLX_exp, FLT_exp.
unfold canonic_exp, FLX_exp, FLT_exp.
apply Zle_max_l.
Qed.
......@@ -176,10 +176,10 @@ Qed.
Theorem canonic_exp_FLT_FIX :
forall x, x <> R0 ->