From e509148de2043a77c697f8a288245f578f3d7c2d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 8 Apr 2009 17:36:36 +0000 Subject: [PATCH] Split format definitions. --- src/Flocq_rnd_FIX.v | 43 ++++++++++++++++++++++++++--------------- src/Flocq_rnd_FLX.v | 32 ++++++++++++++++++++---------- src/Flocq_rnd_generic.v | 22 +++++++++++---------- 3 files changed, 61 insertions(+), 36 deletions(-) diff --git a/src/Flocq_rnd_FIX.v b/src/Flocq_rnd_FIX.v index 84f0913..92ed000 100644 --- a/src/Flocq_rnd_FIX.v +++ b/src/Flocq_rnd_FIX.v @@ -19,11 +19,22 @@ Definition FIX_format (x : R) := Definition FIX_RoundingModeP (rnd : R -> R):= Rounding_for_Format FIX_format rnd. -Theorem FIX_format_satisfies_any : - satisfies_any FIX_format. +Definition FIX_exp (e : Z) := emin. + +Theorem FIX_exp_correct : valid_exp FIX_exp. +Proof. +intros k. +unfold FIX_exp. +split ; intros H. +now apply Zlt_le_weak. +split. +apply Zle_refl. +now intros _ _. +Qed. + +Theorem FIX_format_generic : + forall x : R, generic_format beta FIX_exp x <-> FIX_format x. Proof. -pose (fexp (e : Z) := emin). -refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)). split. (* . *) intros ((xm, xe), (Hx1, Hx2)). @@ -38,23 +49,23 @@ repeat split. rewrite Hx1. apply (f_equal (fun e => F2R (Float beta xm e))). simpl in Hx2. -unfold fexp in Hx2. -apply Hx2. +now unfold FIX_exp in Hx2. (* . *) intros ((xm, xe), (Hx1, Hx2)). -exists (Float beta xm (fexp xe)). +exists (Float beta xm (FIX_exp xe)). split. -unfold fexp. +unfold FIX_exp. now rewrite <- Hx2. now intros Hx3. -(* . *) -intros k. -unfold fexp. -split ; intros H. -now apply Zlt_le_weak. -split. -apply Zle_refl. -now intros _ _. +Qed. + +Theorem FIX_format_satisfies_any : + satisfies_any FIX_format. +Proof. +pose (fexp (e : Z) := emin). +refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)). +exact FIX_format_generic. +exact FIX_exp_correct. Qed. End RND_FIX. diff --git a/src/Flocq_rnd_FLX.v b/src/Flocq_rnd_FLX.v index 9ea9c53..10fd0b5 100644 --- a/src/Flocq_rnd_FLX.v +++ b/src/Flocq_rnd_FLX.v @@ -21,11 +21,18 @@ Definition FLX_format (x : R) := Definition FLX_RoundingModeP (rnd : R -> R):= Rounding_for_Format FLX_format rnd. -Theorem FLX_format_satisfies_any : - satisfies_any FLX_format. +Definition FLX_exp (e : Z) := (e - prec)%Z. + +Theorem FLX_exp_correct : valid_exp FLX_exp. +Proof. +intros k. +unfold FLX_exp. +repeat split ; intros ; omega. +Qed. + +Theorem FLX_format_generic : + forall x : R, generic_format beta FLX_exp x <-> FLX_format x. Proof. -pose (fexp e := (e - prec)%Z). -refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)). split. (* . *) intros ((xm, xe), (Hx1, Hx2)). @@ -51,7 +58,7 @@ apply Rmult_lt_reg_r with (bpow (ex - prec)%Z). apply epow_gt_0. rewrite <- epow_add. replace (prec + (ex - prec))%Z with ex by ring. -change (ex - prec)%Z with (fexp ex). +change (ex - prec)%Z with (FLX_exp ex). rewrite <- Hx2. replace (Z2R (Zabs xm) * bpow xe)%R with (Rabs x). exact (proj2 Hx4). @@ -78,16 +85,21 @@ 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). +change (Fexp (Float beta mx (ex - prec))) with (FLX_exp ex). apply f_equal. apply sym_eq. apply ln_beta_unique. rewrite <- Hx5. now rewrite <- Hx1. -(* . *) -intros k. -unfold fexp. -repeat split ; intros ; omega. +Qed. + +Theorem FLX_format_satisfies_any : + satisfies_any FLX_format. +Proof. +pose (fexp e := (e - prec)%Z). +refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)). +exact FLX_format_generic. +exact FLX_exp_correct. Qed. End RND_FIX. diff --git a/src/Flocq_rnd_generic.v b/src/Flocq_rnd_generic.v index c315683..2a2fdc5 100644 --- a/src/Flocq_rnd_generic.v +++ b/src/Flocq_rnd_generic.v @@ -11,12 +11,14 @@ Notation bpow := (epow beta). Variable fexp : Z -> Z. -Variable valid_fexp : - forall k : Z, - ( (fexp k < k)%Z -> (fexp (k + 1) <= k)%Z ) /\ - ( (k <= fexp k)%Z -> - (fexp (fexp k + 1) <= fexp k)%Z /\ - forall l : Z, (l <= fexp k)%Z -> fexp l = fexp k ). +Definition valid_exp := + forall k : Z, + ( (fexp k < k)%Z -> (fexp (k + 1) <= k)%Z ) /\ + ( (k <= fexp k)%Z -> + (fexp (fexp k + 1) <= fexp k)%Z /\ + forall l : Z, (l <= fexp k)%Z -> fexp l = fexp k ). + +Variable prop_exp : valid_exp. Definition generic_format (x : R) := exists f : float beta, @@ -237,7 +239,7 @@ apply Rle_trans with (bpow ge). apply -> epow_le. simpl in Hg2. rewrite Hg2. -rewrite (proj2 (proj2 (valid_fexp ex) He1) ge'). +rewrite (proj2 (proj2 (prop_exp ex) He1) ge'). exact He1. apply Zle_trans with (2 := He1). cut (ge' - 1 < ex)%Z. omega. @@ -370,7 +372,7 @@ apply Rle_lt_trans with (1 := Hbr). exact Hx. (* - . . a radix power *) rewrite <- Hbl2. -generalize (proj1 (valid_fexp _) He1). +generalize (proj1 (prop_exp _) He1). clear. intros He2. exists (Float beta (- Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))). @@ -449,7 +451,7 @@ rewrite Ropp_mult_distr_l_reverse. rewrite Rmult_1_l. (* - . rounded *) split. -destruct (proj2 (valid_fexp _) He1) as (He2, _). +destruct (proj2 (prop_exp _) He1) as (He2, _). exists (Float beta (- Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))). unfold F2R. simpl. split. @@ -500,7 +502,7 @@ apply <- epow_lt. apply Rle_lt_trans with (1 := proj1 Hge). apply Ropp_lt_cancel. now rewrite Ropp_involutive. -rewrite (proj2 (proj2 (valid_fexp _) He1) _ Hge') in Hg2. +rewrite (proj2 (proj2 (prop_exp _) He1) _ Hge') in Hg2. rewrite <- Hg2 in Hge'. apply Rlt_not_le with (1 := proj2 Hge). rewrite Hg1. -- GitLab