Commit c7dc30cc authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Proved FLX using generic format.

parent a1b583ad
......@@ -29,19 +29,11 @@ Definition IdempotentP (F : R -> Prop) (rnd : R -> R) :=
Definition Rounding_for_Format (F : R -> Prop) (rnd : R -> R) :=
MonotoneP rnd /\ IdempotentP F rnd.
(* unbounded floating-point format *)
Definition FLX_format (prec : Z) (x : R) :=
exists f : float beta,
x = F2R f /\ (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z.
(* floating-point format with gradual underflow *)
Definition FLT_format (emin prec : Z) (x : R) :=
exists f : float beta,
x = F2R f /\ (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z /\ (emin <= Fexp f)%Z.
Definition FLX_RoundingModeP (prec : Z) (rnd : R -> R):=
Rounding_for_Format (FLX_format prec) rnd.
Definition FLT_RoundingModeP (emin prec : Z) (rnd : R -> R):=
Rounding_for_Format (FLT_format emin prec) rnd.
......
......@@ -3,15 +3,13 @@ Require Import Flocq_defs.
Section Float_prop.
Open Scope R_scope.
Variable beta : radix.
Notation bpow := (epow beta).
Lemma F2R_ge_0_imp_Fnum :
Theorem F2R_ge_0_imp_Fnum :
forall f : float beta,
0 <= F2R f ->
(0 <= F2R f)%R ->
(0 <= Fnum f)%Z.
Proof.
intros f H.
......@@ -22,9 +20,9 @@ rewrite Rmult_0_r.
now rewrite Rmult_comm.
Qed.
Lemma F2R_le_0_imp_Fnum :
Theorem F2R_le_0_imp_Fnum :
forall f : float beta,
F2R f <= 0 ->
(F2R f <= 0)%R ->
(Fnum f <= 0)%Z.
Proof.
intros f H.
......@@ -41,10 +39,35 @@ apply Ropp_le_contravar.
now rewrite Rmult_comm.
Qed.
Lemma F2R_prec_normalize :
Theorem abs_F2R :
forall m e : Z,
Rabs (F2R (Float beta m e)) = F2R (Float beta (Zabs m) e).
Proof.
intros m e.
unfold F2R.
rewrite Rabs_mult.
rewrite Rabs_Z2R.
simpl.
apply f_equal.
apply Rabs_right.
apply Rle_ge.
apply epow_ge_0.
Qed.
Theorem opp_F2R :
forall m e : Z,
Ropp (F2R (Float beta m e)) = F2R (Float beta (Zopp m) e).
Proof.
intros m e.
unfold F2R. simpl.
rewrite <- Ropp_mult_distr_l_reverse.
now rewrite opp_Z2R.
Qed.
Theorem F2R_prec_normalize_pos :
forall m e e' p : Z,
(Zabs m < Zpower (radix_val beta) p)%Z ->
bpow e' <= F2R (Float beta m e) ->
(bpow e' <= F2R (Float beta m e))%R ->
exists m' : Z,
F2R (Float beta m e) = F2R (Float beta m' (e' - (p - 1))).
Proof.
......@@ -87,4 +110,30 @@ elim Zlt_not_le with (1 := Hm).
apply Zabs_pos.
Qed.
Theorem F2R_prec_normalize :
forall m e e' p : Z,
(Zabs m < Zpower (radix_val beta) p)%Z ->
(bpow e' <= Rabs (F2R (Float beta m e)))%R ->
exists m' : Z,
F2R (Float beta m e) = F2R (Float beta m' (e' - (p - 1))).
Proof.
intros [|m|m] e e' p Hm Hf.
exists Z0.
unfold F2R. simpl.
now rewrite 2!Rmult_0_l.
(* . *)
apply F2R_prec_normalize_pos.
exact Hm.
now rewrite abs_F2R in Hf.
(* . *)
destruct (F2R_prec_normalize_pos (Zpos m) e e' p) as (m', Hm').
exact Hm.
now rewrite abs_F2R in Hf.
exists (Zopp m').
rewrite <- opp_F2R.
rewrite <- Hm'.
unfold F2R. simpl.
apply Ropp_mult_distr_l_reverse.
Qed.
End Float_prop.
\ No newline at end of file
......@@ -23,18 +23,9 @@ Theorem FIX_format_satisfies_any :
satisfies_any FIX_format.
Proof.
pose (fexp (e : Z) := emin).
(* . *)
destruct (generic_format_satisfies_any beta fexp) as (Hzero, Hsym, rnd, Hrnd).
intros k.
unfold fexp.
split ; intros H.
now apply Zlt_le_weak.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)).
split.
apply Zle_refl.
now intros _ _.
(* . *)
assert (Heq : forall x, generic_format beta fexp x <-> FIX_format x).
split.
intros ((xm, xe), (Hx1, Hx2)).
destruct (Req_dec x 0) as [Hx3|Hx3].
exists (Float beta 0 emin).
......@@ -49,6 +40,7 @@ apply (f_equal (fun e => F2R (Float beta xm e))).
simpl in Hx2.
unfold fexp in Hx2.
apply Hx2.
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
exists (Float beta xm (fexp xe)).
split.
......@@ -56,21 +48,13 @@ unfold fexp.
now rewrite <- Hx2.
now intros Hx3.
(* . *)
refine (Satisfies_any _ _ _ rnd _).
now apply -> Heq.
intros x Hx.
apply -> Heq.
apply Hsym.
now apply <- Heq.
intros x.
destruct (Hrnd x) as (H1, (H2, H3)).
split.
now apply -> Heq.
intros k.
unfold fexp.
split ; intros H.
now apply Zlt_le_weak.
split.
exact H2.
intros g Hg Hgx.
apply H3 ; try assumption.
now apply <- Heq.
apply Zle_refl.
now intros _ _.
Qed.
End RND_FIX.
Require Import Flocq_Raux.
Require Import Flocq_defs.
Require Import Flocq_float_prop.
Require Import Flocq_rnd_ex.
Require Import Flocq_rnd_prop.
Require Import Flocq_rnd_FIX.
Require Import Flocq_rnd_generic.
Require Import Flocq_float_prop.
Section RND_FIX.
Open Scope R_scope.
Variable beta : radix.
Notation bpow := (epow beta).
......@@ -16,224 +13,81 @@ Notation bpow := (epow beta).
Variable prec : Z.
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.
Definition FLX_RoundingModeP (rnd : R -> R):=
Rounding_for_Format FLX_format rnd.
Theorem FLX_format_satisfies_any :
satisfies_any (FLX_format beta prec).
satisfies_any FLX_format.
Proof.
refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
(* symmetric set *)
pose (fexp e := (e - prec)%Z).
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)).
split.
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
destruct (Req_dec x 0) as [Hx3|Hx3].
exists (Float beta 0 0).
split.
unfold F2R.
unfold F2R. simpl.
now rewrite Rmult_0_l.
apply lt_Z2R.
rewrite Z2R_Zpower.
apply epow_gt_0.
now apply Zlt_le_weak.
intros x ((m,e),(H1,H2)).
exists (Float beta (-m) e).
split.
rewrite H1.
unfold F2R.
simpl.
now rewrite opp_Z2R, Ropp_mult_distr_l_reverse.
simpl.
now rewrite Zabs_Zopp.
(* rounding down *)
(* . *)
assert (Hfix: forall rnd emin, Rnd_DN (FIX_format beta emin) rnd ->
FIX_format beta emin 0 /\ Rounding_for_Format (FIX_format beta emin) rnd).
intros.
split.
eapply FIX_format_satisfies_any.
apply Zpower_lt.
now apply Zlt_le_trans with (2 := radix_prop beta).
exact Hp.
specialize (Hx2 Hx3).
exists (Float beta xm xe).
split.
now apply Rnd_DN_monotone with (FIX_format beta emin).
now apply Rnd_DN_idempotent.
(* . *)
assert (Hh: forall x, 0 > x -> 0 < -x).
intros x Hx.
apply Ropp_gt_lt_0_contravar.
exact Hx.
exists (fun x =>
let e :=
Zminus match total_order_T 0 x with
| inleft (left Hx) => projS1 (ln_beta beta _ Hx)
| inleft (right Hx) => Z0
| inright Hx => projS1 (ln_beta beta _ (Hh _ Hx))
end prec in
match satisfies_any_imp_DN _ (FIX_format_satisfies_any beta e) with
| exist rnd Hr => rnd x
end).
(* . *)
intros x.
destruct (total_order_T 0 x) as [[Hx|Hx]|Hx].
(* x positive *)
clear Hh.
set (e := (projT1 (ln_beta beta x Hx) - prec)%Z).
destruct (satisfies_any_imp_DN _ (FIX_format_satisfies_any beta e)) as (rnd,Hr).
destruct (Hr x) as ((f,(Hr1,Hr2)),(Hr3,Hr4)).
destruct (ln_beta beta x Hx) as (e', Hb).
simpl in e.
split.
(* - rnd x is compatible with the format *)
assert (Hm: (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z).
apply Zgt_lt.
apply Znot_le_gt.
intros Hm.
apply Rlt_not_le with (1 := proj2 Hb).
apply Rle_trans with (2 := Hr3).
rewrite Hr1.
unfold F2R.
rewrite Hr2.
replace e' with (prec + e)%Z by ( unfold e ; ring ).
rewrite epow_add.
apply Rmult_le_compat_r.
apply epow_ge_0.
rewrite <- Z2R_Zpower.
apply Z2R_le.
rewrite <- (Zabs_eq (Fnum f)).
exact Hm.
apply F2R_ge_0_imp_Fnum.
rewrite <- Hr1.
apply Rnd_pos_imp_pos with (FIX_format beta e) ; try apply (Hfix _ _ Hr).
now apply Rlt_le.
now apply Zlt_le_weak.
now exists f ; split.
(* - rnd x is the biggest float smaller than x *)
split.
exact Hr3.
intros g ((mg,eg),(Hg1,Hg2)) Hgx.
destruct (Rle_or_lt g (bpow (e' - 1)%Z)).
apply Rle_trans with (1 := H).
apply Hr4.
exists (Float beta (Zpower (radix_val beta) (prec - 1)) e).
repeat split.
unfold F2R.
simpl.
rewrite Z2R_Zpower.
rewrite <- epow_add.
unfold e.
apply f_equal.
ring.
omega.
apply Hb.
apply Hr4.
destruct (F2R_prec_normalize beta mg eg (e' - 1) prec Hg2) as (mg',Hg).
rewrite <- Hg1.
now apply Rlt_le.
rewrite Hg1, Hg.
replace (e' - 1 - (prec - 1))%Z with (e' - prec)%Z by ring.
now exists (Float beta mg' (e' - prec)).
exact Hgx.
rewrite <- Hx.
(* x zero *)
clear -Hp Hfix.
destruct (satisfies_any_imp_DN _ (FIX_format_satisfies_any beta (0 - prec))) as (rnd,Hr).
rewrite Rnd_0 with (FIX_format beta (0 - prec)) rnd ; try apply (Hfix _ _ Hr).
repeat split ; trivial ; try apply Rle_refl.
exists (Float beta 0 0).
unfold F2R.
exact Hx1.
simpl.
split.
now rewrite Rmult_0_l.
destruct (ln_beta beta (Rabs x) (Rabs_pos_lt x Hx3)) as (ex, Hx4).
simpl in Hx2.
apply lt_Z2R.
rewrite Z2R_Zpower.
apply Rmult_lt_reg_r with (bpow (ex - prec)%Z).
apply epow_gt_0.
now apply Zlt_le_weak.
(* x negative *)
set (Hx' := Hh _ Hx).
set (e := (projT1 (ln_beta beta _ Hx') - prec)%Z).
destruct (satisfies_any_imp_DN _ (FIX_format_satisfies_any beta e)) as (rnd,Hr).
destruct (Hr x) as ((f,(Hr1,Hr2)),(Hr3,Hr4)).
destruct (ln_beta beta _ Hx') as (e', Hb).
simpl in e.
split.
(* - rnd x is compatible with the format *)
destruct (Rle_or_lt (rnd x) (-bpow e')) as [Hd|Hd].
(* -. rnd x is -beta^e' *)
assert (H': rnd x = -bpow e').
apply Rle_antisym ; try assumption.
apply Hr4.
exists (Float beta (- Zpower (radix_val beta) prec)%Z e).
repeat split.
unfold F2R. simpl.
rewrite opp_Z2R.
rewrite Ropp_mult_distr_l_reverse.
rewrite Z2R_Zpower.
rewrite <- epow_add.
apply (f_equal (fun e => - bpow e)).
unfold e ; ring.
replace (prec + (ex - prec))%Z with ex by ring.
change (ex - prec)%Z with (fexp ex).
rewrite <- Hx2.
replace (Z2R (Zabs xm) * bpow xe)%R with (Rabs x).
exact (proj2 Hx4).
rewrite Hx1.
apply abs_F2R.
now apply Zlt_le_weak.
apply Ropp_le_cancel.
rewrite Ropp_involutive.
apply Rlt_le.
apply Hb.
exists (Float beta (-1)%Z (e')).
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
destruct (Req_dec x 0) as [Hx3|Hx3].
rewrite Hx3.
exists (Float beta 0 0).
split.
unfold F2R. simpl.
rewrite Ropp_mult_distr_l_reverse.
now rewrite Rmult_1_l.
simpl.
apply lt_Z2R.
rewrite Z2R_Zpower.
change (Z2R 1) with (bpow Z0).
now apply -> epow_lt.
now apply Zlt_le_weak.
(* -. rnd x is not -beta^e' *)
assert (Hm: (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z).
apply Zgt_lt.
apply Znot_le_gt.
intros Hm.
apply Rlt_not_le with (1 := Hd).
apply Ropp_le_cancel.
rewrite Ropp_involutive.
rewrite Hr1.
unfold F2R.
rewrite Hr2.
replace e' with (prec + e)%Z by (unfold e; ring).
rewrite epow_add.
rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_compat_r.
apply epow_ge_0.
rewrite <- Z2R_Zpower.
rewrite <- opp_Z2R.
apply Z2R_le.
rewrite <- (Zabs_non_eq (Fnum f)).
apply Hm.
apply F2R_le_0_imp_Fnum.
rewrite <- Hr1.
apply Rnd_neg_imp_neg with (FIX_format beta e) ; try apply (Hfix _ _ Hr).
now apply Rlt_le.
now apply Zlt_le_weak.
now exists f ; split.
(* - rnd x is the biggest float smaller than x *)
split.
exact Hr3.
intros g ((mg,eg),(Hg1,Hg2)) Hgx.
apply Hr4.
destruct (F2R_prec_normalize beta (-mg)%Z eg (e' - 1) prec) as (mg',Hg).
now rewrite Zabs_Zopp.
apply Rle_trans with (1 := proj1 Hb).
unfold F2R.
simpl.
rewrite opp_Z2R.
rewrite Ropp_mult_distr_l_reverse.
apply Ropp_le_contravar.
unfold F2R in Hg1.
simpl in Hg1.
now rewrite <- Hg1.
exists (Float beta (-mg') e).
repeat split.
rewrite Hg1.
unfold F2R.
simpl.
rewrite opp_Z2R.
rewrite Ropp_mult_distr_l_reverse.
rewrite <- (Ropp_involutive (Z2R mg * bpow eg)).
now rewrite Rmult_0_l.
intros H.
now elim H.
destruct (ln_beta beta (Rabs x) (Rabs_pos_lt _ Hx3)) as (ex, Hx4).
simpl in Hx2.
destruct (F2R_prec_normalize beta xm xe (ex - 1) prec Hx2) as (mx, Hx5).
rewrite <- Hx1.
exact (proj1 Hx4).
rewrite Hx1.
replace (ex - 1 - (prec - 1))%Z with (ex - prec)%Z in Hx5 by ring.
rewrite Hx5.
eexists ; repeat split.
intros H.
change (Fexp (Float beta mx (ex - prec))) with (fexp ex).
apply f_equal.
rewrite <- Ropp_mult_distr_l_reverse.
rewrite <- opp_Z2R.
now replace e with (e' - 1 - (prec - 1))%Z by (unfold e ; ring).
exact Hgx.
apply sym_eq.
apply ln_beta_unique.
rewrite <- Hx5.
now rewrite <- Hx1.
(* . *)
intros k.
unfold fexp.
repeat split ; intros ; omega.
Qed.
End RND_FIX.
......@@ -12,6 +12,30 @@ Inductive satisfies_any (F : R -> Prop) :=
F 0 -> ( forall x : R, F x -> F (-x) ) ->
forall rnd : R -> R, Rnd_DN F rnd -> satisfies_any F.
Theorem satisfies_any_eq :
forall F1 F2 : R -> Prop,
( forall x, F1 x <-> F2 x ) ->
satisfies_any F1 ->
satisfies_any F2.
Proof.
intros F1 F2 Heq (Hzero, Hsym, rnd, Hrnd).
refine (Satisfies_any _ _ _ rnd _).
now apply -> Heq.
intros x Hx.
apply -> Heq.
apply Hsym.
now apply <- Heq.
intros x.
destruct (Hrnd x) as (H1, (H2, H3)).
split.
now apply -> Heq.
split.
exact H2.
intros g Hg Hgx.
apply H3 ; try assumption.
now apply <- Heq.
Qed.
Theorem satisfies_any_imp_DN :
forall F : R -> Prop,
satisfies_any F ->
......
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