Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 5742a158 authored by BOLDO Sylvie's avatar BOLDO Sylvie

Comments

parent a90ca0c2
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Sterbenz conditions for exact subtraction *)
Require Import Fcore.
Require Import Fcalc_ops.
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Remainder of the division and square root are in the FLX format *)
Require Import Fcore.
Require Import Fcalc_ops.
Require Import Fprop_relative.
......@@ -66,6 +68,7 @@ exists (Float beta (Ztrunc (scaled_mantissa beta (FLX_exp prec) x)) (cexp x)).
split; auto.
Qed.
(** Remainder of the division in FLX *)
Theorem div_error_FLX :
forall Zrnd x y,
format x -> format y ->
......@@ -145,9 +148,10 @@ destruct (ln_beta beta y); simpl.
left; now apply a.
Qed.
(** Remainder of the square in FLX (with p>1) and rounding to nearest *)
Variable Hp1 : Zlt 1 prec.
Theorem sqrt_error_N :
Theorem sqrt_error_FLX_N :
forall x, format x ->
format (x - Rsqr (round beta (FLX_exp prec) (rndN choice) (sqrt x)))%R.
Proof.
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Error of the multiplication is in the FLX/FLT format *)
Require Import Fcore.
Require Import Fcalc_ops.
......@@ -30,6 +32,7 @@ Variable Hp : Zlt 0 prec.
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
(** Auxiliary result that provides the exponent *)
Theorem mult_error_FLX_aux:
forall rnd,
forall x y,
......@@ -131,7 +134,7 @@ apply Hc1.
reflexivity.
Qed.
(** Error of the multiplication in FLX *)
Theorem mult_error_FLX :
forall rnd,
forall x y,
......@@ -162,7 +165,7 @@ Variable Hpemin: (emin <= prec)%Z.
Notation format := (generic_format beta (FLT_exp emin prec)).
Notation cexp := (canonic_exponent beta (FLT_exp emin prec)).
(** Error of the multiplication in FLT with underflow requirements *)
Theorem mult_error_FLT :
forall rnd,
forall x y,
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Error of the multiplication is in generic format and rounding to nearest *)
Require Import Fcore.
Require Import Fcalc_ops.
......@@ -109,6 +111,7 @@ rewrite Rabs_Ropp.
now apply (generic_N_pt beta _ prop_exp choice (x + y)).
Qed.
(** Error of the addition *)
Theorem plus_error :
forall x y,
format x -> format y ->
......@@ -177,6 +180,7 @@ ring_simplify (exy - 1 + 1)%Z.
omega.
Qed.
(** rnd(x+y)=0 -> x+y = 0 provided this is not a FTZ format *)
Theorem round_plus_eq_zero :
forall rnd x y,
format x -> format y ->
......
(*
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
This library is free software; you can redistribute it and/or
......@@ -16,6 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Relative error of the roundings *)
Require Import Fcore.
Section Fprop_relative.
......@@ -116,6 +118,7 @@ apply bpow_ge_0.
apply He.
Qed.
(** * 1+#&epsilon;# property in any rounding *)
Theorem generic_relative_error_ex :
forall x,
(bpow emin <= Rabs x)%R ->
......@@ -252,6 +255,7 @@ apply bpow_ge_0.
apply He.
Qed.
(** * 1+#&epsilon;# property in rounding to nearest *)
Theorem generic_relative_error_N_ex :
forall x,
(bpow emin <= Rabs x)%R ->
......@@ -426,6 +430,7 @@ apply bpow_gt_0.
now apply relative_error_FLT_F2R.
Qed.
(** * 1+#&epsilon;# property in any rounding in FLT *)
Theorem relative_error_FLT_ex :
forall x,
(bpow (emin + prec - 1) <= Rabs x)%R ->
......@@ -455,6 +460,7 @@ omega.
exact Hx.
Qed.
(** * 1+#&epsilon;# property in rounding to nearest in FLT *)
Theorem relative_error_N_FLT_ex :
forall x,
(bpow (emin + prec - 1) <= Rabs x)%R ->
......@@ -607,6 +613,7 @@ omega.
apply He.
Qed.
(** * 1+#&epsilon;# property in any rounding in FLX *)
Theorem relative_error_FLX_ex :
forall x,
(x <> 0)%R ->
......@@ -661,6 +668,7 @@ omega.
apply He.
Qed.
(** * 1+#&epsilon;# property in rounding to nearest in FLX *)
Theorem relative_error_N_FLX_ex :
forall x,
exists eps,
......
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