Commit 00e1c682 authored by BOLDO Sylvie's avatar BOLDO Sylvie

Des admits en plus :)

parent 12a3f692
......@@ -619,6 +619,8 @@ Definition mkZrounding2 rnd (mono : forall x y, (x <= y)%R -> (rnd x <= rnd y)%Z
Definition ZrndDN := mkZrounding2 Zfloor Zfloor_le Zfloor_Z2R.
Definition ZrndUP := mkZrounding2 Zceil Zceil_le Zceil_Z2R.
(* Definition ZrndTZ := .. SB *)
Theorem rounding_DN_or_UP :
forall rnd x,
......@@ -679,6 +681,29 @@ now rewrite <- Hx.
apply bpow_ge_0.
Qed.
Theorem rounding_monotone_l :
forall rnd x y, generic_format x -> (x <= y)%R -> (x <= rounding rnd y)%R.
Proof.
Admitted. (* SB *)
Theorem rounding_monotone_r :
forall rnd x y, generic_format y -> (x <= y)%R -> (rounding rnd x <= y)%R.
Proof.
Admitted. (* SB *)
Theorem rounding_monotone_abs_l :
forall rnd x y, generic_format x -> (x <= Rabs y)%R -> (x <= Rabs (rounding rnd y))%R.
Proof.
Admitted. (* SB *)
Theorem rounding_monotone_abs_r :
forall rnd x y, generic_format y -> (Rabs x <= y)%R -> (Rabs (rounding rnd x) <= y)%R.
Proof.
Admitted. (* SB *)
Theorem rounding_abs_abs :
forall P : R -> R -> Prop,
( forall rnd x, P x (rounding rnd x) ) ->
......
Require Import Fcore.
Require Import Fcalc_ops.
Section Fprop_divsqrt_error.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable fexp : Z -> Z.
Hypothesis prop_exp : valid_exp fexp.
Notation format := (generic_format beta fexp).
Variable choice : R -> bool.
Theorem div_error_N :
forall x y,
format x -> format y ->
format (x - rounding beta fexp (ZrndN choice) (x/y) * y)%R.
Proof.
(* probablement seulement en FLX *)
Admitted. (* SB *)
(* Theorem div_error_Z :
forall x y,
format x -> format y ->
format (x - rounding beta fexp (ZrndTZ) (x/y) * y)%R.
Proof.
(* probablement seulement en FLX *)
Admitted. (* SB *) *)
Theorem sqrt_error_N :
forall x, (0 <= x)%R ->
format x ->
format (x - Rsqr (rounding beta fexp (ZrndN choice) (sqrt x)))%R.
Proof.
(* probablement seulement en FLX *)
Admitted. (* SB *)
End Fprop_divsqrt_error.
......@@ -511,6 +511,17 @@ omega.
exact Hp.
Qed.
Theorem error_N_FLT :
forall x,
exists eps, exists eta,
(Rabs eps <= /2 * bpow (-prec + 1))%R /\
(Rabs eta <= /2 * bpow (emin))%R /\
(eps*eta=0)%R /\
rounding beta (FLT_exp emin prec) (ZrndN choice) x = (x * (1 + eps) + eta)%R.
Proof.
Admitted. (* SB *)
End Fprop_relative_FLT.
Section Fprop_relative_FLX.
......
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