diff options
| author | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2014-10-07 15:28:21 +0200 |
|---|---|---|
| committer | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2014-10-07 15:28:21 +0200 |
| commit | 7159e8142480fd0d851f3fd54b07dc8890f5b610 (patch) | |
| tree | 1259927d05b3e82846bbef014d864816f8a19a91 /flocq/Core/Fcore_FLT.v | |
| parent | fe29750c851cf41d37cab764b1c4d0f0ee68f0d5 (diff) | |
| download | compcert-kvx-7159e8142480fd0d851f3fd54b07dc8890f5b610.tar.gz compcert-kvx-7159e8142480fd0d851f3fd54b07dc8890f5b610.zip | |
Upgrade to flocq 2.4.0
Diffstat (limited to 'flocq/Core/Fcore_FLT.v')
| -rw-r--r-- | flocq/Core/Fcore_FLT.v | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v index c057b6ce..273ff69f 100644 --- a/flocq/Core/Fcore_FLT.v +++ b/flocq/Core/Fcore_FLT.v @@ -104,6 +104,19 @@ 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. +Qed. + + + + Theorem FLT_format_satisfies_any : satisfies_any FLT_format. Proof. @@ -115,11 +128,14 @@ apply generic_format_FLT. Qed. Theorem canonic_exp_FLT_FLX : - forall x, x <> R0 -> + forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> canonic_exp beta FLT_exp x = canonic_exp beta (FLX_exp prec) x. Proof. -intros x Hx0 Hx. +intros x Hx. +assert (Hx0: x <> 0%R). +intros H1; rewrite H1, Rabs_R0 in Hx. +contradict Hx; apply Rlt_not_le, bpow_gt_0. unfold canonic_exp. apply Zmax_left. destruct (ln_beta beta x) as (ex, He). @@ -166,10 +182,6 @@ Theorem round_FLT_FLX : forall rnd x, intros rnd x Hx. unfold round, scaled_mantissa. rewrite canonic_exp_FLT_FLX ; trivial. -contradict Hx. -rewrite Hx, Rabs_R0. -apply Rlt_not_le. -apply bpow_gt_0. Qed. (** Links between FLT and FIX (underflow) *) |