Commit 75ceaaca authored by BOLDO Sylvie's avatar BOLDO Sylvie

Release 2.0.0

parent afb2fa06
......@@ -18,6 +18,7 @@ Version 2.0.0:
. Rnd_NE_pt_FIX, Rnd_NE_pt_FLX, Rnd_NE_pt_FLT
. round_NE_pt_FLX, round_NE_pt_FLT
. Zrnd_opp_le, Zrnd_Z2R_opp
- removed example file Fappli_sqrt_FLT_ne
- split theorems on equivalence between specific and generic formats
into both directions:
. FIX_format_generic and generic_format_FIX
......
AC_INIT([Flocq], [1.4.0],
AC_INIT([Flocq], [2.0.0],
[Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[flocq])
AM_INIT_AUTOMAKE
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......@@ -841,6 +841,8 @@ Proof.
now intros [sx|sx| |sx mx ex] H.
Qed.
(** Multiplication *)
Lemma Bmult_correct_aux :
forall m sx mx ex (Hx : bounded mx ex = true) sy my ey (Hy : bounded my ey = true),
let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in
......@@ -1120,6 +1122,7 @@ apply Rlt_bool_true.
now apply F2R_lt_0_compat.
Qed.
(** Addition *)
Definition Bplus m x y :=
match x, y with
| B754_nan, _ => x
......@@ -1292,7 +1295,7 @@ now rewrite is_finite_Bopp.
now destruct y as [ | | | ].
Qed.
(** Division *)
Definition Fdiv_core_binary m1 e1 m2 e2 :=
let d1 := Zdigits2 m1 in
let d2 := Zdigits2 m2 in
......@@ -1446,6 +1449,7 @@ intros H2.
now rewrite B2FF_FF2B.
Qed.
(** Square root *)
Definition Fsqrt_core_binary m e :=
let d := Zdigits2 m in
let s := Zmax (2 * prec - d) 0 in
......
......@@ -495,6 +495,7 @@ Qed.
End Binary_Bits.
(** Specialization for IEEE single precision operations *)
Section B32_Bits.
Definition binary32 := binary_float 24 128.
......@@ -519,6 +520,7 @@ Definition bits_of_b32 : binary32 -> Z := bits_of_binary_float 23 8.
End B32_Bits.
(** Specialization for IEEE double precision operations *)
Section B64_Bits.
Definition binary64 := binary_float 53 1024.
......
(**
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
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
Require Import Fcore.
Require Import Fcalc_bracket.
Require Import Fcalc_round.
Require Import Fcalc_sqrt.
Section test.
Variable beta : radix.
Variable prec emin : Z.
Variable Hprec : (1 < prec)%Z.
Instance prec_gt_0_ : Prec_gt_0 prec.
unfold Prec_gt_0.
omega.
Qed.
Definition Fsqrt_FLT_ne (f : float beta) :=
let '(Float m e) := f in
if Zle_bool m 0 then Float beta 0 0
else
let '(m', e', l) := truncate beta (FLT_exp emin prec) (Fsqrt_core beta prec m e) in
Float beta (cond_incr (round_N (negb (Zeven m')) l) m') e'.
Theorem Fsqrt_FLT_ne_correct :
forall x,
Rnd_NE_pt beta (FLT_exp emin prec) (sqrt (F2R x)) (F2R (Fsqrt_FLT_ne x)).
Proof with auto with typeclass_instances.
intros x.
replace (F2R (Fsqrt_FLT_ne x)) with (round beta (FLT_exp emin prec) ZnearestE (sqrt (F2R x))).
apply round_NE_pt...
unfold Fsqrt_FLT_ne.
destruct x as (mx, ex).
generalize (Zle_cases mx 0).
case (Zle_bool mx 0) ; intros Hm.
(* mx = 0 *)
rewrite F2R_0.
replace (sqrt (F2R (Float beta mx ex))) with R0.
apply round_0...
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm'].
unfold sqrt.
case Rcase_abs ; intros Hs.
easy.
elim Rge_not_lt with (1 := Hs).
now apply F2R_lt_0_compat.
rewrite Hm', F2R_0.
now rewrite sqrt_0.
(* 0 < mx *)
generalize (Fsqrt_core_correct beta prec mx ex (Zgt_lt _ _ Hm)).
destruct (Fsqrt_core beta prec mx ex) as ((ms, es), ls).
intros (H1, H2).
generalize (round_trunc_NE_correct beta (FLT_exp emin prec) (sqrt (F2R (Float beta mx ex))) ms es ls).
destruct (truncate beta (FLT_exp emin prec) (ms, es, ls)) as ((mr, er), lr).
intros Hr. apply Hr. clear Hr.
apply sqrt_ge_0.
apply H2.
left.
unfold FLT_exp.
generalize (Zmax_spec (Fcore_digits.Zdigits beta ms + es - prec) emin).
omega.
Qed.
End test.
(*
Definition radix10 : radix.
now refine (Build_radix 10 _).
Defined.
Time Eval vm_compute in (Fsqrt radix10 20 (-15) (Float radix10 2 0)).
*)
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......@@ -17,8 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Locations: where a real number is positioned with respect to
its rounded-down value in an arbitrary format. *)
(** * Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......@@ -17,8 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Functions for computing the number of digits of integers
and related theorems. *)
(** * Functions for computing the number of digits of integers and related theorems. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......@@ -17,8 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Helper function and theorem for computing the rounded quotient
of two floating-point numbers. *)
(** * Helper function and theorem for computing the rounded quotient of two floating-point numbers. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......@@ -17,7 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** Basic operations on floats: alignement, addition, multiplication *)
(** Basic operations on floats: alignment, addition, multiplication *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......@@ -17,8 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Helper functions and theorems for computing the rounded
square root of a floating-point number. *)
(** * Helper functions and theorems for computing the rounded square root of a floating-point number. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......@@ -17,7 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * To ease the import *)
(** To ease the import *)
Require Export Fcore_Raux.
Require Export Fcore_defs.
Require Export Fcore_float_prop.
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......@@ -485,6 +485,7 @@ Qed.
End Z2R.
(** Decidable comparison on reals *)
Section Rcompare.
Definition Rcompare x y :=
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -755,7 +755,7 @@ Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z :=
end.
End digits_aux.
(** Number of digits of an integer *)
Definition Zdigits n :=
match n with
| Z0 => Z0
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......@@ -451,7 +451,7 @@ Qed.
Section Fcore_generic_round_pos.
(** * Rounding functions: R -> Z *)
(** Rounding functions: R -> Z *)
Variable rnd : R -> Z.
......@@ -485,7 +485,7 @@ rewrite Zfloor_Z2R, Zrnd_Z2R in Hx.
apply Zlt_irrefl with (1 := Hx).
Qed.
(** * the most useful one: R -> F *)
(** the most useful one: R -> F *)
Definition round x :=
F2R (Float beta (rnd (scaled_mantissa x)) (canonic_exp x)).
......@@ -1720,6 +1720,7 @@ End rndN_opp.
End Format.
(** Inclusion of a format into an extended format *)
Section Inclusion.
Variables fexp1 fexp2 : Z -> Z.
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2011 Sylvie Boldo
#<br />#
Copyright (C) 2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** Helper for detecting the version of Flocq *)
Require Import BinNat.
Require Import Ascii String.
......
......@@ -26,8 +26,7 @@ FILES = \
Prop/Fprop_relative.v \
Prop/Fprop_Sterbenz.v \
Appli/Fappli_IEEE.v \
Appli/Fappli_IEEE_bits.v \
Appli/Fappli_sqrt_FLT_ne.v
Appli/Fappli_IEEE_bits.v
EXTRA_DIST = $(FILES)
CLEANFILES = $(FILES:=o) $(FILES:=d) $(FILES:.v=.glob)
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......
......@@ -2,9 +2,9 @@
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010 Guillaume Melquiond
Copyright (C) 2010-2011 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
......@@ -126,7 +126,7 @@ apply bpow_ge_0.
apply He.
Qed.
(** * 1+#&epsilon;# property in any rounding *)
(** 1+#&epsilon;# property in any rounding *)
Theorem relative_error_ex :
forall x,
(bpow emin <= Rabs x)%R ->
......@@ -262,7 +262,7 @@ apply bpow_ge_0.
apply He.
Qed.
(** * 1+#&epsilon;# property in rounding to nearest *)
(** 1+#&epsilon;# property in rounding to nearest *)
Theorem relative_error_N_ex :
forall x,
(bpow emin <= Rabs x)%R ->
......@@ -436,7 +436,7 @@ apply bpow_gt_0.
now apply relative_error_FLT_F2R_emin.
Qed.
(** * 1+#&epsilon;# property in any rounding in FLT *)
(** 1+#&epsilon;# property in any rounding in FLT *)
Theorem relative_error_FLT_ex :
forall x,
(bpow (emin + prec - 1) <= Rabs x)%R ->
......@@ -461,7 +461,7 @@ apply relative_error_N with (emin + prec - 1)%Z...
apply relative_error_FLT_aux.
Qed.
(** * 1+#&epsilon;# property in rounding to nearest in FLT *)
(** 1+#&epsilon;# property in rounding to nearest in FLT *)
Theorem relative_error_N_FLT_ex :
forall x,
(bpow (emin + prec - 1) <= Rabs x)%R ->
......@@ -605,7 +605,7 @@ apply relative_error_FLX_aux.
apply He.
Qed.
(** * 1+#&epsilon;# property in any rounding in FLX *)
(** 1+#&epsilon;# property in any rounding in FLX *)
Theorem relative_error_FLX_ex :
forall x,
(x <> 0)%R ->
......@@ -655,7 +655,7 @@ apply relative_error_FLX_aux.
apply He.
Qed.
(** * 1+#&epsilon;# property in rounding to nearest in FLX *)
(** 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