Commit 81b2a74c authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added implicit coercions for radix and ln_beta.

parent fb5135b4
......@@ -52,7 +52,7 @@ Qed.
Theorem implies_MinOrMax_not_bpow:
forall x f, format f ->
(0 < f)%R ->
f <> bpow (projT1 (ln_beta beta f)) ->
f <> bpow (ln_beta beta f) ->
(Rabs (f-x) < ulp f)%R ->
MinOrMax x f.
intros x f Hf1 Hf2 Hf3 Hxf1.
......@@ -84,7 +84,7 @@ Qed.
Theorem implies_MinOrMax_bpow:
forall x f, format f ->
f = bpow (projT1 (ln_beta beta f)) ->
f = bpow (ln_beta beta f) ->
(Rabs (f-x) < /2* ulp f)%R ->
MinOrMax x f.
intros x f Hf1 Hf2 Hxf.
......
......@@ -507,17 +507,17 @@ Theorem inbetween_float_new_location :
forall x m e l k,
(0 < k)%Z ->
inbetween_float m e x l ->
inbetween_float (Zdiv m (Zpower (radix_val beta) k)) (e + k) x (new_location (Zpower (radix_val beta) k) (Zmod m (Zpower (radix_val beta) k)) l).
inbetween_float (Zdiv m (Zpower beta k)) (e + k) x (new_location (Zpower beta k) (Zmod m (Zpower beta k)) l).
Proof.
intros x m e l k Hk Hx.
unfold inbetween_float in *.
assert (Hr: forall m, F2R (Float beta m (e + k)) = F2R (Float beta (m * Zpower (radix_val beta) k) e)).
assert (Hr: forall m, F2R (Float beta m (e + k)) = F2R (Float beta (m * Zpower beta k) e)).
clear -Hk. intros m.
rewrite (F2R_change_exp beta e).
apply (f_equal (fun r => F2R (Float beta (m * Zpower _ r) e))).
ring.
omega.
assert (Hp: (Zpower (radix_val beta) k > 0)%Z).
assert (Hp: (Zpower beta k > 0)%Z).
apply Zlt_gt.
now apply Zpower_gt_0.
(* . *)
......@@ -537,10 +537,10 @@ Qed.
Theorem inbetween_float_new_location_single :
forall x m e l,
inbetween_float m e x l ->
inbetween_float (Zdiv m (radix_val beta)) (e + 1) x (new_location (radix_val beta) (Zmod m (radix_val beta)) l).
inbetween_float (Zdiv m beta) (e + 1) x (new_location beta (Zmod m beta) l).
Proof.
intros x m e l Hx.
replace (radix_val beta) with (Zpower (radix_val beta) 1).
replace (radix_val beta) with (Zpower beta 1).
now apply inbetween_float_new_location.
apply Zmult_1_r.
Qed.
......
......@@ -35,15 +35,15 @@ Hypothesis Hp : (0 <= p)%Z.
Fixpoint digits_aux (nb pow : Z) (n : nat) { struct n } : Z :=
match n with
| O => nb
| S n => if Zlt_bool p pow then nb else digits_aux (nb + 1) (Zmult (radix_val beta) pow) n
| S n => if Zlt_bool p pow then nb else digits_aux (nb + 1) (Zmult beta pow) n
end.
Lemma digits_aux_invariant :
forall k n nb,
(0 <= nb)%Z ->
(Zpower (radix_val beta) (nb + Z_of_nat k - 1) <= p)%Z ->
digits_aux (nb + Z_of_nat k) (Zpower (radix_val beta) (nb + Z_of_nat k)) n =
digits_aux nb (Zpower (radix_val beta) nb) (n + k).
(Zpower beta (nb + Z_of_nat k - 1) <= p)%Z ->
digits_aux (nb + Z_of_nat k) (Zpower beta (nb + Z_of_nat k)) n =
digits_aux nb (Zpower beta nb) (n + k).
Proof.
induction k ; intros n nb Hnb.
now rewrite Zplus_0_r, plus_0_r.
......@@ -54,7 +54,7 @@ rewrite (Zplus_comm _ 1), Zplus_assoc.
rewrite IHk.
rewrite <- plus_n_Sm.
simpl.
generalize (Zlt_cases p (Zpower (radix_val beta) nb)).
generalize (Zlt_cases p (Zpower beta nb)).
case Zlt_bool ; intros Hpp.
elim (Zlt_irrefl p).
apply Zlt_le_trans with (1 := Hpp).
......@@ -81,8 +81,8 @@ End digits_aux.
Definition digits n :=
match n with
| Z0 => Z0
| Zneg p => digits_aux (Zpos p) 1 (radix_val beta) (digits2_Pnat p)
| Zpos p => digits_aux n 1 (radix_val beta) (digits2_Pnat p)
| Zneg p => digits_aux (Zpos p) 1 beta (digits2_Pnat p)
| Zpos p => digits_aux n 1 beta (digits2_Pnat p)
end.
Theorem digits_abs :
......@@ -94,7 +94,7 @@ Qed.
Theorem digits_ln_beta :
forall n,
n <> Z0 ->
digits n = projT1 (ln_beta beta (Z2R n)).
digits n = ln_beta beta (Z2R n).
Proof.
intros n Hn.
destruct (ln_beta beta (Z2R n)) as (e, He).
......@@ -117,7 +117,7 @@ now apply (Zlt_le_succ 0).
assert (He2: (Z_of_nat (Zabs_nat (e - 1)) = e - 1)%Z).
rewrite inj_Zabs_nat.
now apply Zabs_eq.
replace (radix_val beta) with (Zpower (radix_val beta) 1).
replace (radix_val beta) with (Zpower beta 1).
replace (digits2_Pnat p) with (digits2_Pnat p - Zabs_nat (e - 1) + Zabs_nat (e - 1)).
rewrite <- digits_aux_invariant.
rewrite He2.
......@@ -125,7 +125,7 @@ ring_simplify (1 + (e - 1))%Z.
destruct (digits2_Pnat p - Zabs_nat (e - 1)) as [|n].
easy.
simpl.
generalize (Zlt_cases (Zpos p) (Zpower (radix_val beta) e)).
generalize (Zlt_cases (Zpos p) (Zpower beta e)).
case Zlt_bool ; intros Hpp.
easy.
elim Rlt_not_le with (1 := proj2 He).
......@@ -154,7 +154,7 @@ exact (proj2 (digits2_Pnat_correct p)).
clear.
induction (S (digits2_Pnat p)).
easy.
change (2 * Zpower_nat 2 n <= radix_val beta * Zpower_nat (radix_val beta) n)%Z.
change (2 * Zpower_nat 2 n <= beta * Zpower_nat beta n)%Z.
apply Zmult_le_compat ; try easy.
apply Zle_bool_imp_le.
apply beta.
......@@ -188,7 +188,7 @@ Qed.
Theorem digits_shift :
forall m e,
m <> Z0 -> (0 <= e)%Z ->
digits (m * Zpower (radix_val beta) e) = (digits m + e)%Z.
digits (m * Zpower beta e) = (digits m + e)%Z.
Proof.
intros m e Hm He.
rewrite 2!digits_ln_beta.
......@@ -316,4 +316,4 @@ rewrite Zmult_0_l, Zplus_0_r, 2!Zplus_0_l.
apply Zle_refl.
Qed.
End Fcalc_digits.
\ No newline at end of file
End Fcalc_digits.
......@@ -21,7 +21,7 @@ Definition Fdiv_aux prec m1 e1 m2 e2 :=
let e := (e1 - e2)%Z in
let (m, e') :=
match (d2 + prec - d1)%Z with
| Zpos p => (m1 * Zpower_pos (radix_val beta) p, e + Zneg p)%Z
| Zpos p => (m1 * Zpower_pos beta p, e + Zneg p)%Z
| _ => (m1, e)
end in
let '(q, r) := Zdiv_eucl m m2 in
......@@ -41,7 +41,7 @@ set (d1 := digits beta m1).
set (d2 := digits beta m2).
case_eq
(match (d2 + prec - d1)%Z with
| Zpos p => ((m1 * Zpower_pos (radix_val beta) p)%Z, (e1 - e2 + Zneg p)%Z)
| Zpos p => ((m1 * Zpower_pos beta p)%Z, (e1 - e2 + Zneg p)%Z)
| _ => (m1, (e1 - e2)%Z)
end).
intros m' e' Hme.
......@@ -56,7 +56,7 @@ repeat split.
now rewrite <- H0.
apply Zle_refl.
replace (e1 - e2 + Zneg p + e2)%Z with (e1 - Zpos p)%Z by (unfold Zminus ; simpl ; ring).
fold (Zpower (radix_val beta) (Zpos p)).
fold (Zpower beta (Zpos p)).
split.
pattern (Zpos p) at 1 ; replace (Zpos p) with (e1 - (e1 - Zpos p))%Z by ring.
apply sym_eq.
......
......@@ -12,8 +12,8 @@ Definition Falign (f1 f2 : float beta) :=
let '(Float m1 e1) := f1 in
let '(Float m2 e2) := f2 in
if Zle_bool e1 e2
then (m1, (m2 * Zpower (radix_val beta) (e2 - e1))%Z, e1)
else ((m1 * Zpower (radix_val beta) (e1 - e2))%Z, m2, e2).
then (m1, (m2 * Zpower beta (e2 - e1))%Z, e1)
else ((m1 * Zpower beta (e1 - e2))%Z, m2, e2).
Theorem Falign_spec :
forall f1 f2 : float beta,
......
......@@ -15,7 +15,7 @@ Definition truncate t :=
let '(m, e, l) := t in
let k := (fexp (digits beta m + e) - e)%Z in
if Zlt_bool 0 k then
let p := Zpower (radix_val beta) k in
let p := Zpower beta k in
(Zdiv m p, (e + k)%Z, new_location p (Zmod m p) l)
else t.
......@@ -31,7 +31,7 @@ Proof.
intros x m e l Hx H1 H2.
unfold truncate.
set (k := (fexp (digits beta m + e) - e)%Z).
set (p := Zpower (radix_val beta) k).
set (p := Zpower beta k).
(* *)
assert (Hx': (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R).
apply inbetween_bounds with (2 := H1).
......
......@@ -13,7 +13,7 @@ Definition round_FIX t :=
let '(m, e, l) := t in
let k := (emin - e)%Z in
if Zlt_bool 0 k then
let p := Zpower (radix_val beta) k in
let p := Zpower beta k in
(Zdiv m p, (e + k)%Z, new_location p (Zmod m p) l)
else t.
......@@ -28,7 +28,7 @@ Proof.
intros x m e l H1 H2.
unfold round_FIX.
set (k := (emin - e)%Z).
set (p := Zpower (radix_val beta) k).
set (p := Zpower beta k).
unfold canonic_exponent, FIX_exp.
generalize (Zlt_cases 0 k).
case (Zlt_bool 0 k) ; intros Hk.
......
......@@ -124,7 +124,7 @@ Definition Fsqrt_aux prec m e :=
let (s', e'') := if Zeven e' then (s, e') else (s + 1, e' - 1)%Z in
let m' :=
match s' with
| Zpos p => (m * Zpower_pos (radix_val beta) p)%Z
| Zpos p => (m * Zpower_pos beta p)%Z
| _ => m
end in
let (q, r) := Zsqrt m' in
......@@ -172,7 +172,7 @@ destruct He as (He1, (He2, (He3, He4))).
(* . shift *)
set (m' := match s' with
| Z0 => m
| Zpos p => (m * Zpower_pos (radix_val beta) p)%Z
| 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).
......@@ -182,7 +182,7 @@ destruct s' as [|p|p].
repeat split ; try easy.
fold d.
omega.
fold (Zpower (radix_val beta) (Zpos p)).
fold (Zpower beta (Zpos p)).
split.
replace (Zpos p) with (Zpos p + e' - e')%Z by ring.
rewrite <- F2R_change_exp.
......
......@@ -19,7 +19,7 @@ Variable Hp : Zlt 0 prec.
(* floating-point format with gradual underflow *)
Definition FLT_format (x : R) :=
exists f : float beta,
x = F2R f /\ (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z /\ (emin <= Fexp f)%Z.
x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z /\ (emin <= Fexp f)%Z.
Definition FLT_RoundingModeP (rnd : R -> R):=
Rounding_for_Format FLT_format rnd.
......@@ -256,7 +256,7 @@ generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.
Hypothesis NE_prop : Zeven (radix_val beta) = false \/ (1 < prec)%Z.
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
Theorem NE_ex_prop_FLT :
NE_ex_prop beta FLT_exp.
......
......@@ -18,7 +18,7 @@ Variable Hp : Zlt 0 prec.
(* unbounded floating-point format *)
Definition FLX_format (x : R) :=
exists f : float beta,
x = F2R f /\ (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z.
x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z.
Definition FLX_RoundingModeP (rnd : R -> R):=
Rounding_for_Format FLX_format rnd.
......@@ -106,7 +106,7 @@ apply iff_trans with (FIX_format beta (ex - prec) x).
apply FLX_format_FIX.
exact (conj (proj1 Hx2) (Rlt_le _ _ (proj2 Hx2))).
apply FIX_format_generic.
assert (Hf: FLX_exp (projT1 (ln_beta beta x)) = FIX_exp (ex - prec) (projT1 (ln_beta beta x))).
assert (Hf: FLX_exp (ln_beta beta x) = FIX_exp (ex - prec) (ln_beta beta x)).
unfold FIX_exp, FLX_exp.
now rewrite ln_beta_unique with (1 := Hx2).
split ;
......@@ -128,7 +128,7 @@ Qed.
Definition FLXN_format (x : R) :=
exists f : float beta,
x = F2R f /\ (x <> R0 ->
Zpower (radix_val beta) (prec - 1) <= Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z.
Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z.
Definition FLXN_RoundingModeP (rnd : R -> R):=
Rounding_for_Format FLXN_format rnd.
......@@ -159,7 +159,7 @@ apply H4.
rewrite <- Z2R_Zpower, <- abs_Z2R.
now apply Z2R_lt.
now apply Zlt_le_weak.
exists (Float beta (xm * Zpower (radix_val beta) (prec - d)) (xe + d - prec)).
exists (Float beta (xm * Zpower beta (prec - d)) (xe + d - prec)).
split.
unfold F2R. simpl.
rewrite mult_Z2R, Z2R_Zpower.
......@@ -228,7 +228,7 @@ unfold FLX_exp.
omega.
Qed.
Hypothesis NE_prop : Zeven (radix_val beta) = false \/ (1 < prec)%Z.
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
Theorem NE_ex_prop_FLX :
NE_ex_prop beta FLX_exp.
......
......@@ -17,7 +17,7 @@ Variable Hp : Zlt 0 prec.
(* floating-point format with abrupt underflow *)
Definition FTZ_format (x : R) :=
exists f : float beta,
x = F2R f /\ (x <> R0 -> Zpower (radix_val beta) (prec - 1) <= Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z /\
x = F2R f /\ (x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z /\
(emin <= Fexp f)%Z.
Definition FTZ_RoundingModeP (rnd : R -> R):=
......
......@@ -1269,7 +1269,7 @@ End Proof_Irrelevance.
Section pow.
Record radix := { radix_val : Z ; radix_prop : Zle_bool 2 radix_val = true }.
Record radix := { radix_val :> Z ; radix_prop : Zle_bool 2 radix_val = true }.
Theorem radix_val_inj :
forall r1 r2, radix_val r1 = radix_val r2 -> r1 = r2.
......@@ -1285,7 +1285,7 @@ Qed.
Variable r : radix.
Theorem radix_gt_1 : (1 < radix_val r)%Z.
Theorem radix_gt_1 : (1 < r)%Z.
Proof.
destruct r as (v, Hr). simpl.
apply Zlt_le_trans with 2%Z.
......@@ -1293,7 +1293,7 @@ easy.
now apply Zle_bool_imp_le.
Qed.
Theorem radix_pos : (0 < Z2R (radix_val r))%R.
Theorem radix_pos : (0 < Z2R r)%R.
Proof.
destruct r as (v, Hr). simpl.
apply (Z2R_lt 0).
......@@ -1304,8 +1304,8 @@ Qed.
Definition bpow e :=
match e with
| Zpos p => Z2R (Zpower_pos (radix_val r) p)
| Zneg p => Rinv (Z2R (Zpower_pos (radix_val r) p))
| Zpos p => Z2R (Zpower_pos r p)
| Zneg p => Rinv (Z2R (Zpower_pos r p))
| Z0 => R1
end.
......@@ -1327,7 +1327,7 @@ Qed.
Theorem bpow_powerRZ :
forall e,
bpow e = powerRZ (Z2R (radix_val r)) e.
bpow e = powerRZ (Z2R r) e.
Proof.
destruct e ; unfold bpow.
reflexivity.
......@@ -1364,14 +1364,14 @@ apply radix_pos.
Qed.
Theorem bpow_1 :
bpow 1 = Z2R (radix_val r).
bpow 1 = Z2R r.
Proof.
unfold bpow, Zpower_pos, iter_pos.
now rewrite Zmult_1_r.
Qed.
Theorem bpow_add1 :
forall e : Z, (bpow (e+1) = Z2R (radix_val r) * bpow e)%R.
forall e : Z, (bpow (e + 1) = Z2R r * bpow e)%R.
Proof.
intros.
rewrite <- bpow_1.
......@@ -1393,7 +1393,7 @@ Qed.
Theorem Z2R_Zpower_nat :
forall e : nat,
Z2R (Zpower_nat (radix_val r) e) = bpow (Z_of_nat e).
Z2R (Zpower_nat r e) = bpow (Z_of_nat e).
Proof.
intros [|e].
split.
......@@ -1405,7 +1405,7 @@ Qed.
Theorem Z2R_Zpower :
forall e : Z,
(0 <= e)%Z ->
Z2R (Zpower (radix_val r) e) = bpow e.
Z2R (Zpower r e) = bpow e.
Proof.
intros [|e|e] H.
split.
......@@ -1435,7 +1435,7 @@ elim (lt_irrefl 0).
pattern O at 2 ; rewrite <- H.
apply lt_O_nat_of_P.
intros n _.
assert (1 < Zpower_nat (radix_val r) 1)%Z.
assert (1 < Zpower_nat r 1)%Z.
unfold Zpower_nat, iter_nat.
rewrite Zmult_1_r.
apply radix_gt_1.
......@@ -1502,10 +1502,10 @@ Qed.
Theorem bpow_exp :
forall e : Z,
bpow e = exp (Z2R e * ln (Z2R (radix_val r))).
bpow e = exp (Z2R e * ln (Z2R r)).
Proof.
(* positive case *)
assert (forall e, bpow (Zpos e) = exp (Z2R (Zpos e) * ln (Z2R (radix_val r)))).
assert (forall e, bpow (Zpos e) = exp (Z2R (Zpos e) * ln (Z2R r))).
intros e.
unfold bpow.
rewrite Zpower_pos_nat.
......@@ -1534,19 +1534,23 @@ rewrite Rmult_0_l.
now rewrite exp_0.
apply H.
unfold bpow.
change (Z2R (Zpower_pos (radix_val r) e)) with (bpow (Zpos e)).
change (Z2R (Zpower_pos r e)) with (bpow (Zpos e)).
rewrite H.
rewrite <- exp_Ropp.
rewrite <- Ropp_mult_distr_l_reverse.
now rewrite <- opp_Z2R.
Qed.
Theorem ln_beta :
forall x : R,
{e | (x <> 0)%R -> (bpow (e - 1)%Z <= Rabs x < bpow e)%R}.
Record ln_beta_prop x := {
ln_beta_val :> Z ;
_ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R
}.
Definition ln_beta :
forall x : R, ln_beta_prop x.
Proof.
intros x.
set (fact := ln (Z2R (radix_val r))).
set (fact := ln (Z2R r)).
(* . *)
assert (0 < fact)%R.
apply exp_lt_inv.
......@@ -1614,7 +1618,7 @@ Qed.
Theorem ln_beta_unique :
forall (x : R) (e : Z),
(bpow (e - 1) <= Rabs x < bpow e)%R ->
projT1 (ln_beta x) = e.
ln_beta x = e :> Z.
Proof.
intros x e1 He.
destruct (Req_dec x 0) as [Hx|Hx].
......@@ -1629,7 +1633,7 @@ Qed.
Theorem ln_beta_opp :
forall x,
projT1 (ln_beta (-x)) = projT1 (ln_beta x).
ln_beta (-x) = ln_beta x :> Z.
Proof.
intros x.
destruct (Req_dec x 0) as [Hx|Hx].
......@@ -1643,20 +1647,19 @@ Qed.
Theorem ln_beta_abs :
forall x,
projT1 (ln_beta (Rabs x)) = projT1 (ln_beta x).
ln_beta (Rabs x) = ln_beta x :> Z.
Proof.
intros x.
set (m := projT1 (ln_beta x)).
unfold Rabs.
case Rcase_abs ; intros _.
now rewrite ln_beta_opp.
apply ln_beta_opp.
apply refl_equal.
Qed.
Theorem ln_beta_monotone_abs :
forall x y,
(x <> 0)%R -> (Rabs x <= Rabs y)%R ->
(projT1 (ln_beta x) <= projT1 (ln_beta y))%Z.
(ln_beta x <= ln_beta y)%Z.
Proof.
intros x y H0x Hxy.
destruct (ln_beta x) as (ex, Hx).
......@@ -1677,7 +1680,7 @@ Qed.
Theorem ln_beta_monotone :
forall x y,
(0 < x)%R -> (x <= y)%R ->
(projT1 (ln_beta x) <= projT1 (ln_beta y))%Z.
(ln_beta x <= ln_beta y)%Z.
Proof.
intros x y H0x Hxy.
apply ln_beta_monotone_abs.
......@@ -1690,7 +1693,7 @@ now apply Rlt_le.
Qed.
Theorem ln_beta_bpow :
forall e, projT1 (ln_beta (bpow e)) = (e + 1)%Z.
forall e, (ln_beta (bpow e) = e + 1 :> Z)%Z.
Proof.
intros e.
apply ln_beta_unique.
......@@ -1718,7 +1721,7 @@ Qed.
Theorem Zpower_gt_1 :
forall p,
(0 < p)%Z ->
(1 < Zpower (radix_val r) p)%Z.
(1 < Zpower r p)%Z.
Proof.
intros.
apply lt_Z2R.
......@@ -1730,7 +1733,7 @@ Qed.
Theorem Zpower_gt_0 :
forall p,
(0 < p)%Z ->
(0 < Zpower (radix_val r) p)%Z.
(0 < Zpower r p)%Z.
Proof.
intros.
apply Zlt_trans with 1%Z.
......
......@@ -261,7 +261,7 @@ Qed.
Theorem ln_beta_F2R_bounds :
forall x m e, (0 < m)%Z ->
(F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
projT1 (ln_beta beta x) = projT1 (ln_beta beta (F2R (Float beta m e))).
ln_beta beta x = ln_beta beta (F2R (Float beta m e)) :> Z.
Proof.
intros x m e Hp (Hx,Hx2).
destruct (ln_beta beta (F2R (Float beta m e))) as (ex, He).
......@@ -308,7 +308,7 @@ Qed.
Theorem F2R_lt_bpow :
forall f : float beta, forall e',
(Zabs (Fnum f) < Zpower (radix_val beta) (e' - Fexp f))%Z ->
(Zabs (Fnum f) < Zpower beta (e' - Fexp f))%Z ->
(Rabs (F2R f) < bpow e')%R.
Proof.
intros (m, e) e' Hm.
......@@ -332,7 +332,7 @@ Qed.
Theorem F2R_change_exp :
forall e' m e : Z,
(e' <= e)%Z ->
F2R (Float beta m e) = F2R (Float beta (m * Zpower (radix_val beta) (e - e')) e').
F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e')) e').
Proof.
intros e' m e He.
unfold F2R. simpl.
......@@ -345,9 +345,9 @@ Qed.
Theorem F2R_prec_normalize :
forall m e e' p : Z,
(Zabs m < Zpower (radix_val beta) p)%Z ->
(Zabs m < Zpower beta p)%Z ->
(bpow (e' - 1)%Z <= Rabs (F2R (Float beta m e)))%R ->
F2R (Float beta m e) = F2R (Float beta (m * Zpower (radix_val beta) (e - e' + p)) (e' - p)).
F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e' + p)) (e' - p)).
Proof.
intros m e e' p Hm Hf.
assert (Hp: (0 <= p)%Z).
......@@ -370,7 +370,7 @@ Qed.
Theorem ln_beta_F2R :
forall m e : Z,
m <> Z0 ->
(projT1 (ln_beta beta (F2R (Float beta m e))) = projT1 (ln_beta beta (Z2R m)) + e)%Z.
(ln_beta beta (F2R (Float beta m e)) = ln_beta beta (Z2R m) + e :> Z)%Z.
Proof.
intros m e H.
destruct (ln_beta beta (Z2R m)) as (d, Hd).
......@@ -396,7 +396,7 @@ Theorem float_distribution_pos :
forall m1 e1 m2 e2 : Z,
(0 < m1)%Z ->
(F2R (Float beta m1 e1) < F2R (Float beta m2 e2) < F2R (Float beta (m1 + 1) e1))%R ->
(e2 < e1)%Z /\ (e1 + projT1 (ln_beta beta (Z2R m1)) = e2 + projT1 (ln_beta beta (Z2R m2)))%Z.
(e2 < e1)%Z /\ (e1 + ln_beta beta (Z2R m1) = e2 + ln_beta beta (Z2R m2))%Z.
Proof.
intros m1 e1 m2 e2 Hp1 (H12, H21).
assert (He: (e2 < e1)%Z).
......
......@@ -21,7 +21,7 @@ Definition valid_exp :=
Variable prop_exp : valid_exp.
Definition canonic_exponent x :=
fexp (projT1 (ln_beta beta x)).
fexp (ln_beta beta x).
Definition canonic (f : float beta) :=
Fexp f = canonic_exponent (F2R f).
......@@ -85,7 +85,7 @@ unfold generic_format, scaled_mantissa.
set (e' := canonic_exponent (F2R (Float beta m e))).
intros He.
unfold F2R at 3. simpl.
assert (H: (Z2R m * bpow e * bpow (- e') = Z2R (m * Zpower (radix_val beta) (e + -e')))%R).
assert (H: (Z2R m * bpow e * bpow (- e') = Z2R (m * Zpower beta (e + -e')))%R).
rewrite Rmult_assoc, <- bpow_add, mult_Z2R.
rewrite Z2R_Zpower.
apply refl_equal.
......@@ -312,10 +312,9 @@ rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r.
now rewrite Ztrunc_Z2R.
Qed.
Theorem canonic_exp_ge:
forall prec,
(forall e, (e-fexp e <= prec)%Z) ->
(forall e, (e - fexp e <= prec)%Z) ->
(* OK with FLX, FLT and FTZ *)
forall x, generic_format x ->
(Rabs x < bpow (prec + canonic_exponent x))%R.
......@@ -324,15 +323,14 @@ case (Req_dec x 0); intros Hxz.
rewrite Hxz, Rabs_R0.
apply bpow_gt_0.
unfold canonic_exponent.
destruct (ln_beta beta x); simpl.
specialize (a Hxz).
apply Rlt_le_trans with (1:=proj2 a).
destruct (ln_beta beta x) as (ex,Ex) ; simpl.
specialize (Ex Hxz).
apply Rlt_le_trans with (1 := proj2 Ex).
apply -> bpow_le.
specialize (Hp x0).
specialize (Hp ex).
omega.
Qed.
Theorem generic_format_bpow_inv :
forall e,
generic_format (bpow e) ->
......@@ -368,7 +366,6 @@ unfold scaled_mantissa.
apply Rmult_le_pos; apply bpow_ge_0.
Qed.
Section Fcore_generic_rounding_pos.
Record Zrounding := mkZrounding {
......@@ -526,7 +523,7 @@ replace (ex - 1)%Z with (ex - 1 + - fexp ex + fexp ex)%Z by ring.
rewrite bpow_add.
apply Rmult_le_compat_r.
apply bpow_ge_0.
assert (Hf: Z2R (Zpower (radix_val beta) (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)).
assert (Hf: Z2R (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)).
apply Z2R_Zpower.
omega.
rewrite <- Hf.
......@@ -553,7 +550,7 @@ pattern ex at 3 ; replace ex with (ex - fexp ex + fexp ex)%Z by ring.
rewrite bpow_add.
apply Rmult_le_compat_r.
apply bpow_ge_0.
assert (Hf: Z2R (Zpower (radix_val beta) (ex - fexp ex)) = bpow (ex - fexp ex)).
assert (Hf: Z2R (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)).
apply Z2R_Zpower.
omega.
rewrite <- Hf.
......@@ -724,7 +721,7 @@ apply F2R_le_0_compat. simpl.
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_monotone.
simpl.
rewrite <- (Rmult_0_l (bpow (- fexp (projT1 (ln_beta beta x))))).
rewrite <- (Rmult_0_l (bpow (- fexp (ln_beta beta x)))).
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply Rlt_le.
......@@ -1031,10 +1028,10 @@ intros e x He Hx.
pattern x at 2 ; rewrite Hx.
unfold F2R at 2. simpl.
rewrite Rmult_assoc, <- bpow_add.
assert (H: Z2R (Zpower (radix_val beta) (canonic_exponent x + - fexp e)) = bpow (canonic_exponent x + - fexp e)).
assert (H: Z2R (Zpower beta (canonic_exponent x + - fexp e)) = bpow (canonic_exponent x + - fexp e)).
apply Z2R_Zpower.
unfold canonic_exponent.
set (ex := projT1 (ln_beta beta x)).
set (ex := ln_beta beta x).
generalize (not_FTZ ex).
generalize (proj2 (proj2 (prop_exp _) He) (fexp ex + 1)%Z).