Commit e33daa41 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Turn Valid_exp into a canonical structure.

parent 9d0eb3d0
This diff is collapsed.
......@@ -4,8 +4,7 @@ Section Compute.
Variable beta : radix.
Variable fexp : Z -> Z.
Context { valid_exp : Valid_exp fexp }.
Variable fexp : Valid_exp.
Variable prec : Z.
Hypothesis Hprec : (0 < prec)%Z.
......
This diff is collapsed.
......@@ -4,10 +4,10 @@ From Flocq Require Import Core Operations Relative Plus_error.
Section Theory.
Variable emin : Z.
Variable prec : Z.
Context {Hprec : Prec_gt_0 prec}.
Notation fexp := (FLT_exp emin prec).
Section prec.
Variable prec : Z.
Definition Bmin := bpow radix2 (emin + prec - 1).
......@@ -15,6 +15,22 @@ Definition hombnd (m M u v : R) (b B : float radix2) :=
(0 <= F2R b)%R /\ (1 <= F2R B)%R /\
((Bmin <= m)%R -> (Rabs (u - v) <= F2R b * M)%R /\ (Rabs v <= F2R B * M)%R).
Definition mult_err b1 B1 b2 B2 :=
Fplus radix2 (Fplus radix2 (Fmult radix2 b1 B2) (Fmult radix2 B1 b2)) (Fmult radix2 b1 b2).
Definition round_err b B :=
Fplus radix2 (Fmult radix2 (Fplus radix2 b B) (Float radix2 1 (- prec))) b.
End prec.
Section Prec_gt_0.
Variable prec : Prec_gt_0.
Notation fexp := (FLT_exp emin prec).
Notation Bmin := (Bmin prec).
Notation hombnd := (hombnd prec).
Lemma hombnd_fact :
forall m M1 M2 u v b B,
(M1 <= M2)%R ->
......@@ -99,9 +115,6 @@ rewrite 2!Rabs_Ropp.
now split.
Qed.
Definition mult_err b1 B1 b2 B2 :=
Fplus radix2 (Fplus radix2 (Fmult radix2 b1 B2) (Fmult radix2 B1 b2)) (Fmult radix2 b1 b2).
Lemma hombnd_mult :
forall m M1 u1 v1 b1 B1 M2 u2 v2 b2 B2,
hombnd m M1 u1 v1 b1 B1 ->
......@@ -146,13 +159,10 @@ rewrite H0, Rabs_mult.
now apply Rmult_le_compat ; try apply Rabs_pos.
Qed.
Definition round_err b B :=
Fplus radix2 (Fmult radix2 (Fplus radix2 b B) (Float radix2 1 (- prec))) b.
Lemma hombnd_rnd :
forall m M u v b B,
hombnd m M u v b B ->
hombnd (Rmin m M) M (round radix2 fexp ZnearestE u) v (round_err b B) B.
hombnd (Rmin m M) M (round radix2 fexp ZnearestE u) v (round_err prec b B) B.
Proof with auto with typeclass_instances.
intros m M u v b B [Ho1 [Ho2 Ho]].
unfold hombnd, round_err.
......@@ -210,6 +220,8 @@ rewrite F2R_bpow.
ring.
Qed.
End Prec_gt_0.
End Theory.
Section Example.
......@@ -221,6 +233,8 @@ Definition mul x y := round radix2 fxp ZnearestE (x * y).
Definition hombnd' := hombnd (-1074) 53.
Canonical Structure prec53 := Build_Prec_gt_0 53 eq_refl.
Lemma hombnd_sub_init :
forall u v,
generic_format radix2 fxp u ->
......@@ -245,7 +259,6 @@ apply FLT_format_plus_small ; try easy.
now apply generic_format_opp.
replace (F2R (Float radix2 1 (-53))) with (bpow radix2 (-1) * bpow radix2 (-53 + 1))%R.
apply relative_error_N_FLT.
easy.
apply Rlt_le.
apply Rle_lt_trans with (2 := S).
now apply bpow_le.
......
......@@ -29,7 +29,6 @@ Notation bpow e := (bpow beta e).
Section Fcalc_round_fexp.
Variable fexp : Z -> Z.
Context { valid_exp : Valid_exp fexp }.
Notation format := (generic_format beta fexp).
(** Relates location and rounding. *)
......@@ -265,12 +264,12 @@ Theorem inbetween_int_ZR :
forall x m l,
inbetween_int m x l ->
Ztrunc x = cond_incr (round_ZR (Zlt_bool m 0) l) m.
Proof with auto with typeclass_instances.
Proof.
intros x m l Hl.
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
rewrite Zrnd_Z2R...
now rewrite Zrnd_Z2R.
(* not Exact *)
unfold Ztrunc.
assert (Hm: Zfloor x = m).
......@@ -357,12 +356,12 @@ Theorem inbetween_int_N :
forall choice x m l,
inbetween_int m x l ->
Znearest choice x = cond_incr (round_N (choice m) l) m.
Proof with auto with typeclass_instances.
Proof.
intros choice x m l Hl.
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
rewrite Zrnd_Z2R...
now rewrite Zrnd_Z2R.
(* not Exact *)
unfold Znearest.
assert (Hm: Zfloor x = m).
......@@ -386,7 +385,7 @@ Theorem inbetween_int_N_sign :
forall choice x m l,
inbetween_int m (Rabs x) l ->
Znearest choice x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (if Rlt_bool x 0 then negb (choice (-(m + 1))%Z) else choice m) l) m).
Proof with auto with typeclass_instances.
Proof.
intros choice x m l Hl.
simpl.
unfold Rabs in Hl.
......@@ -399,7 +398,7 @@ rewrite Znearest_opp.
apply f_equal.
inversion_clear Hl as [Hx|l' Hx Hl'].
rewrite Hx.
apply Zrnd_Z2R...
apply Zrnd_Z2R.
assert (Hm: Zfloor (-x) = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
......@@ -423,7 +422,7 @@ rewrite Rlt_bool_false with (1 := Zx).
simpl.
inversion_clear Hl as [Hx|l' Hx Hl'].
rewrite Hx.
apply Zrnd_Z2R...
apply Zrnd_Z2R.
assert (Hm: Zfloor x = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
......@@ -633,7 +632,7 @@ Theorem truncate_correct_format :
x = F2R (Float beta m' e') /\ e' = cexp beta fexp x.
Proof.
intros m e Hm x Fx He.
assert (Hc: cexp beta fexp x = fexp (Zdigits beta m + e)).
assert (Hc: cexp beta fexp x = fexp (Zdigits beta m + e)%Z).
unfold cexp, x.
now rewrite mag_F2R_Zdigits.
unfold truncate.
......@@ -671,6 +670,15 @@ unfold k in Hk.
omega.
Qed.
End Fcalc_round_fexp.
Section valid_exp.
Variable fexp : Valid_exp.
Notation format := (generic_format beta (Generic_fmt.fexp fexp)).
Notation truncate := (truncate (Generic_fmt.fexp fexp)).
Theorem truncate_correct_partial :
forall x m e l,
(0 < x)%R ->
......@@ -716,7 +724,7 @@ ring_simplify.
rewrite <- Hm'.
simpl.
apply sym_eq.
apply valid_exp.
apply valid_exp3.
exact H2.
apply Zle_trans with e.
eapply bpow_lt_bpow.
......@@ -751,7 +759,7 @@ Theorem truncate_correct :
Proof.
intros x m e l [Hx|Hx] H1 H2.
(* 0 < x *)
destruct (Zle_or_lt e (fexp (Zdigits beta m + e))) as [H3|H3].
destruct (Zle_or_lt e (fexp (Zdigits beta m + e)%Z)) as [H3|H3].
(* . enough digits *)
generalize (truncate_correct_partial x m e l Hx H1 H3).
destruct (truncate (m, e, l)) as ((m', e'), l').
......@@ -765,7 +773,7 @@ elim (Zlt_irrefl e).
now apply Zle_lt_trans with (1 := H2).
rewrite H2 in H1 |- *.
unfold truncate.
generalize (Zlt_cases 0 (fexp (Zdigits beta m + e) - e)).
generalize (Zlt_cases 0 (fexp (Zdigits beta m + e)%Z - e)).
case Zlt_bool.
intros H.
apply False_ind.
......@@ -1032,7 +1040,7 @@ Definition round_sign_NA_correct :=
Definition round_trunc_sign_NA_correct :=
round_trunc_sign_any_correct _ (fun s m l => cond_incr (round_N true l) m) inbetween_int_NA_sign.
End Fcalc_round_fexp.
End valid_exp.
(** Specialization of truncate for FIX formats. *)
......
......@@ -36,17 +36,33 @@ Definition FIX_exp (e : Z) := emin.
(** Properties of the FIX format *)
Global Instance FIX_exp_valid : Valid_exp FIX_exp.
Lemma FIX_exp_valid1 :
forall k : Z, (FIX_exp k < k)%Z ->
(FIX_exp (k + 1) <= k)%Z.
Proof.
intros k.
unfold FIX_exp.
split ; intros H.
intros k Hk.
now apply Zlt_le_weak.
split.
Qed.
Lemma FIX_exp_valid2 :
forall k : Z, (k <= FIX_exp k)%Z ->
(FIX_exp (FIX_exp k + 1) <= FIX_exp k)%Z.
Proof.
intros k Hk.
apply Zle_refl.
now intros _ _.
Qed.
Lemma FIX_exp_valid3 :
forall k l : Z,
(k <= FIX_exp k)%Z -> (l <= FIX_exp k)%Z ->
FIX_exp l = FIX_exp k.
Proof.
now intros k l Hk Hl.
Qed.
Canonical Structure FIX_exp_valid :=
Build_Valid_exp FIX_exp FIX_exp_valid1 FIX_exp_valid2 FIX_exp_valid3.
Theorem generic_format_FIX :
forall x, FIX_format x -> generic_format beta FIX_exp x.
Proof.
......@@ -66,14 +82,15 @@ Qed.
Theorem FIX_format_satisfies_any :
satisfies_any FIX_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp)).
eapply satisfies_any_eq.
intros x.
split.
apply FIX_format_generic.
apply generic_format_FIX.
apply generic_format_satisfies_any.
Qed.
Global Instance FIX_exp_monotone : Monotone_exp FIX_exp.
Global Instance FIX_exp_monotone : Monotone_exp FIX_exp_valid.
Proof.
intros ex ey H.
apply Zle_refl.
......
......@@ -27,9 +27,11 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable emin prec : Z.
Variable emin : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Section prec.
Variable prec : Z.
Inductive FLT_format (x : R) : Prop :=
FLT_spec (f : float beta) :
......@@ -39,20 +41,56 @@ Inductive FLT_format (x : R) : Prop :=
Definition FLT_exp e := Zmax (e - prec) emin.
(** Properties of the FLT format *)
Global Instance FLT_exp_valid : Valid_exp FLT_exp.
Lemma FLT_exp_valid1 :
forall k : Z, (FLT_exp k < k)%Z ->
(FLT_exp (k + 1) <= k)%Z.
Proof.
intros k.
unfold FLT_exp.
zify ; omega.
Qed.
End prec.
Section Prec_gt_0.
Variable prec : Prec_gt_0.
Local Notation FLT_exp' := FLT_exp (only parsing).
Local Notation FLT_format' := FLT_format (only parsing).
Notation FLT_exp := (FLT_exp prec).
Notation FLT_format := (FLT_format prec).
Lemma FLT_exp_valid2 :
forall k : Z, (k <= FLT_exp k)%Z ->
(FLT_exp (FLT_exp k + 1) <= FLT_exp k)%Z.
Proof.
intros k.
unfold FLT_exp.
generalize (prec_gt_0 prec).
repeat split ;
intros ; zify ; omega.
zify ; omega.
Qed.
Lemma FLT_exp_valid3 :
forall k l : Z,
(k <= FLT_exp k)%Z -> (l <= FLT_exp k)%Z ->
FLT_exp l = FLT_exp k.
Proof.
intros k l.
unfold FLT_exp.
generalize (prec_gt_0 prec).
zify ; omega.
Qed.
Canonical Structure FLT_exp_valid :=
Build_Valid_exp FLT_exp (FLT_exp_valid1 prec) FLT_exp_valid2 FLT_exp_valid3.
Theorem generic_format_FLT :
forall x, FLT_format x -> generic_format beta FLT_exp x.
forall prec x, FLT_format' prec x -> generic_format beta (FLT_exp' prec) x.
Proof.
clear prec_gt_0_.
intros x [[mx ex] H1 H2 H3].
clear prec.
intros prec x [[mx ex] H1 H2 H3].
simpl in H2, H3.
rewrite H1.
apply generic_format_F2R.
......@@ -76,7 +114,7 @@ intros Hx.
rewrite Hx.
eexists ; repeat split ; simpl.
apply lt_Z2R.
rewrite Z2R_Zpower. 2: now apply Zlt_le_weak.
rewrite Z2R_Zpower. 2: apply Zlt_le_weak, prec_gt_0.
apply Rmult_lt_reg_r with (bpow ex).
apply bpow_gt_0.
rewrite <- bpow_plus.
......@@ -98,27 +136,24 @@ apply Zle_max_l.
apply Zle_max_r.
Qed.
Theorem FLT_format_bpow :
forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e).
Proof.
intros e He.
apply generic_format_bpow; unfold FLT_exp.
apply Z.max_case; try assumption.
unfold Prec_gt_0 in prec_gt_0_; omega.
generalize (prec_gt_0 prec) ; omega.
Qed.
Theorem FLT_format_satisfies_any :
satisfies_any FLT_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp)).
eapply satisfies_any_eq.
intros x.
split.
apply FLT_format_generic.
apply generic_format_FLT.
apply generic_format_satisfies_any.
Qed.
Theorem cexp_FLT_FLX :
......@@ -157,11 +192,11 @@ now rewrite cexp_FLT_FLX.
Qed.
Theorem generic_format_FLX_FLT :
forall x : R,
generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x.
forall (prec : Z) (x : R),
generic_format beta (FLT_exp' prec) x -> generic_format beta (FLX_exp prec) x.
Proof.
clear prec_gt_0_.
intros x Hx.
clear prec.
intros prec x Hx.
unfold generic_format in Hx; rewrite Hx.
apply generic_format_F2R.
intros _.
......@@ -198,12 +233,12 @@ now apply Hex.
Qed.
Theorem generic_format_FIX_FLT :
forall x : R,
generic_format beta FLT_exp x ->
forall (prec : Z) (x : R),
generic_format beta (FLT_exp' prec) x ->
generic_format beta (FIX_exp emin) x.
Proof.
clear prec_gt_0_.
intros x Hx.
clear prec.
intros prec x Hx.
rewrite Hx.
apply generic_format_F2R.
intros _.
......@@ -216,18 +251,20 @@ Theorem generic_format_FLT_FIX :
(Rabs x <= bpow (emin + prec))%R ->
generic_format beta (FIX_exp emin) x ->
generic_format beta FLT_exp x.
Proof with auto with typeclass_instances.
apply generic_inclusion_le...
Proof.
apply generic_inclusion_le.
intros e He.
simpl.
unfold FIX_exp.
apply Zmax_lub.
omega.
apply Zle_refl.
Qed.
Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R ->
ulp beta FLT_exp x = bpow emin.
Proof with auto with typeclass_instances.
Theorem ulp_FLT_small :
forall x : R, (Rabs x < bpow (emin+prec))%R ->
ulp beta FLT_exp x = bpow emin.
Proof.
intros x Hx.
unfold ulp; case Req_bool_spec; intros Hx2.
(* x = 0 *)
......@@ -237,10 +274,12 @@ apply Zle_not_lt; unfold FLT_exp.
apply Zle_trans with (2:=Z.le_max_r _ _); omega.
assert (V:FLT_exp emin = emin).
unfold FLT_exp; apply Z.max_r.
unfold Prec_gt_0 in prec_gt_0_; omega.
generalize (prec_gt_0 prec) ; omega.
intros n H2; rewrite <-V.
apply f_equal, fexp_negligible_exp_eq...
omega.
apply f_equal, fexp_negligible_exp_eq.
exact H2.
simpl.
now rewrite V.
(* x <> 0 *)
apply f_equal; unfold cexp, FLT_exp.
apply Z.max_r.
......@@ -293,12 +332,11 @@ apply bpow_le.
apply Z.le_max_l.
Qed.
(** FLT is a nice format: it has a monotone exponent... *)
Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
Global Instance FLT_exp_monotone : Monotone_exp FLT_exp_valid.
Proof.
intros ex ey.
simpl.
unfold FLT_exp.
zify ; omega.
Qed.
......@@ -306,12 +344,13 @@ Qed.
(** and it allows a rounding to nearest, ties to even. *)
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
Global Instance exists_NE_FLT : Exists_NE beta FLT_exp.
Global Instance exists_NE_FLT : Exists_NE beta FLT_exp_valid.
Proof.
destruct NE_prop as [H|H].
now left.
right.
intros e.
simpl.
unfold FLT_exp.
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
rewrite H2 ; clear H2.
......@@ -323,4 +362,6 @@ generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.
End Prec_gt_0.
End RND_FLT.
......@@ -21,43 +21,88 @@ COPYING file for more details.
Require Import Raux Definitions Round_pred Generic_fmt Float_prop.
Require Import FIX Ulp Round_NE.
Record Prec_gt_0 := {
prec :> Z ;
prec_gt_0 : (0 < prec)%Z
}.
Section RND_FLX.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable prec : Z.
Class Prec_gt_0 :=
prec_gt_0 : (0 < prec)%Z.
Section prec.
Context { prec_gt_0_ : Prec_gt_0 }.
Variable prec : Z.
Inductive FLX_format (x : R) : Prop :=
FLX_spec (f : float beta) :
x = F2R f -> (Zabs (Fnum f) < Zpower beta prec)%Z -> FLX_format x.
(** unbounded floating-point format with normal mantissas *)
Inductive FLXN_format (x : R) : Prop :=
FLXN_spec (f : float beta) :
x = F2R f ->
(x <> 0%R -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
FLXN_format x.
Definition FLX_exp (e : Z) := (e - prec)%Z.
(** Properties of the FLX format *)
Global Instance FLX_exp_valid : Valid_exp FLX_exp.
Lemma FLX_exp_valid1 :
forall k : Z, (FLX_exp k < k)%Z ->
(FLX_exp (k + 1) <= k)%Z.
Proof.
intros k.
unfold FLX_exp.
omega.
Qed.
End prec.
Section Prec_gt_0.
Variable prec : Prec_gt_0.
Local Notation FLX_exp' := FLX_exp (only parsing).
Local Notation FLX_format' := FLX_format (only parsing).
Notation FLX_exp := (FLX_exp prec).
Notation FLX_format := (FLX_format prec).
Lemma FLX_exp_valid2 :
forall k : Z, (k <= FLX_exp k)%Z ->
(FLX_exp (FLX_exp k + 1) <= FLX_exp k)%Z.
Proof.
intros k.
unfold FLX_exp.
generalize prec_gt_0.
repeat split ; intros ; omega.
generalize (prec_gt_0 prec).
omega.
Qed.
Lemma FLX_exp_valid3 :
forall k l : Z,
(k <= FLX_exp k)%Z -> (l <= FLX_exp k)%Z ->
FLX_exp l = FLX_exp k.
Proof.
intros k l.
unfold FLX_exp.
generalize (prec_gt_0 prec).
omega.
Qed.
Canonical Structure FLX_exp_valid :=
Build_Valid_exp FLX_exp (FLX_exp_valid1 prec) FLX_exp_valid2 FLX_exp_valid3.
Theorem FIX_format_FLX :
forall x e,
forall (prec : Z) x e,
(bpow (e - 1) <= Rabs x <= bpow e)%R ->
FLX_format x ->
FLX_format' prec x ->
FIX_format beta (e - prec) x.
Proof.
clear prec_gt_0_.
intros x e Hx [[xm xe] H1 H2].
clear prec.
intros prec x e Hx [[xm xe] H1 H2].
rewrite H1, (F2R_prec_normalize beta xm xe e prec).
now eexists.
exact H2.
......@@ -79,7 +124,7 @@ apply Rmult_lt_reg_r with (bpow (cexp beta FLX_exp (Rabs x))).
apply bpow_gt_0.
rewrite scaled_mantissa_mult_bpow.
rewrite Z2R_Zpower, <- bpow_plus.
2: now apply Zlt_le_weak.
2: apply Zlt_le_weak, prec_gt_0.
unfold cexp, FLX_exp.
ring_simplify (prec + (mag beta (Rabs x) - prec))%Z.
rewrite mag_abs.
......@@ -91,10 +136,10 @@ now apply Ex.
Qed.
Theorem generic_format_FLX :
forall x, FLX_format x -> generic_format beta FLX_exp x.
forall prec x, FLX_format' prec x -> generic_format beta (FLX_exp' prec) x.
Proof.
clear prec_gt_0_.
intros x [[mx ex] H1 H2].
clear prec.
intros prec x [[mx ex] H1 H2].
simpl in H2.
rewrite H1.
apply generic_format_F2R.
......@@ -109,11 +154,12 @@ Qed.
Theorem FLX_format_satisfies_any :
satisfies_any FLX_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)).
eapply satisfies_any_eq.
intros x.
split.
apply FLX_format_generic.
apply generic_format_FLX.
apply generic_format_satisfies_any.
Qed.
Theorem FLX_format_FIX :
......@@ -121,26 +167,20 @@ Theorem FLX_format_FIX :
(bpow (e - 1) <= Rabs x <= bpow e)%R ->
FIX_format beta (e - prec) x ->
FLX_format x.
Proof with auto with typeclass_instances.
Proof.
intros x e Hx Fx.
apply FLX_format_generic.
apply generic_format_FIX in Fx.
revert Fx.
apply generic_inclusion with (e := e)...
apply generic_inclusion with (2 := Hx).
apply Zle_refl.
Qed.
(** unbounded floating-point format with normal mantissas *)
Inductive FLXN_format (x : R) : Prop :=
FLXN_spec (f : float beta) :
x = F2R f ->
(x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
FLXN_format x.
Theorem generic_format_FLXN :
forall x, FLXN_format x -> generic_format beta FLX_exp x.
forall prec x, FLXN_format prec x -> generic_format beta (FLX_exp' prec) x.
Proof.
intros x [[xm ex] H1 H2].
clear prec.
intros prec x [[xm ex] H1 H2].
destruct (Req_dec x 0) as [Zx|Zx].
rewrite Zx.
apply generic_format_0.
......@@ -152,7 +192,7 @@ apply H2.
Qed.
Theorem FLXN_format_generic :
forall x, generic_format beta FLX_exp x -> FLXN_format x.
forall x, generic_format beta FLX_exp x -> FLXN_format prec x.
Proof.
intros x Hx.
rewrite Hx.
......@@ -165,7 +205,7 @@ split.
(* *)
apply le_Z2R.
rewrite Z2R_Zpower.
2: now apply Zlt_0_le_0_pred.
2: apply Zlt_0_le_0_pred, prec_gt_0.
rewrite Z2R_abs, <- scaled_mantissa_generic with (1 := Hx).
apply Rmult_le_reg_r with (bpow (cexp beta FLX_exp x)).
apply bpow_gt_0.
......@@ -181,7 +221,7 @@ now apply Ex.
(* *)
apply lt_Z2R.
rewrite Z2R_Zpower.
2: now apply Zlt_le_weak.
2: apply Zlt_le_weak, prec_gt_0.
rewrite Z2R_abs, <- scaled_mantissa_generic with (1 := Hx).
apply Rmult_lt_reg_r with (bpow (cexp beta FLX_exp x)).
apply bpow_gt_0.
......@@ -197,21 +237,23 @@ now apply Ex.
Qed.
Theorem FLXN_format_satisfies_any :
satisfies_any FLXN_format.
satisfies_any (FLXN_format prec).
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)).
split ; intros H.
now apply FLXN_format_generic.
now apply generic_format_FLXN.
eapply satisfies_any_eq.
split.
apply FLXN_format_generic.
apply generic_format_FLXN.
apply generic_format_satisfies_any.
Qed.
Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.
Theorem ulp_FLX_0: ulp beta FLX_exp 0 = 0%R.
Proof.
unfold ulp; rewrite Req_bool_true; trivial.
case (negligible_exp_spec FLX_exp).
intros _; reflexivity.
intros n H2; contradict H2.
unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega.
unfold FLX_exp.
generalize (prec_gt_0 prec); omega.
Qed.
Theorem ulp_FLX_le :
......@@ -244,7 +286,7 @@ left; now apply bpow_mag_gt.
Qed.
(** FLX is a nice format: it has a monotone exponent... *)
Global Instance FLX_exp_monotone : Monotone_exp FLX_exp. <