Commit bfecafc1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Rename theories.

parent f7755906
FILES = \
Flocq_version.v \
Core/Fcore_Raux.v \
Core/Fcore_Zaux.v \
Core/Fcore_defs.v \
Core/Fcore_digits.v \
Core/Fcore_float_prop.v \
Core/Fcore_FIX.v \
Core/Fcore_FLT.v \
Core/Fcore_FLX.v \
Core/Fcore_FTZ.v \
Core/Fcore_generic_fmt.v \
Core/Fcore_rnd.v \
Core/Fcore_rnd_ne.v \
Core/Fcore_ulp.v \
Core/Fcore.v \
Calc/Fcalc_bracket.v \
Calc/Fcalc_digits.v \
Calc/Fcalc_div.v \
Calc/Fcalc_ops.v \
Calc/Fcalc_round.v \
Calc/Fcalc_sqrt.v \
Prop/Fprop_div_sqrt_error.v \
Prop/Fprop_mult_error.v \
Prop/Fprop_plus_error.v \
Prop/Fprop_relative.v \
Prop/Fprop_Sterbenz.v \
Appli/Fappli_rnd_odd.v \
Appli/Fappli_IEEE.v \
Appli/Fappli_IEEE_bits.v \
Appli/Fappli_double_round.v
Version.v \
Core/Raux.v \
Core/Zaux.v \
Core/Definitions.v \
Core/Digits.v \
Core/Float_prop.v \
Core/FIX.v \
Core/FLT.v \
Core/FLX.v \
Core/FTZ.v \
Core/Generic_fmt.v \
Core/Round_pred.v \
Core/Round_NE.v \
Core/Ulp.v \
Core/Core.v \
Calc/Bracket.v \
Calc/Div.v \
Calc/Operations.v \
Calc/Round.v \
Calc/Sqrt.v \
Prop/Div_sqrt_error.v \
Prop/Mult_error.v \
Prop/Plus_error.v \
Prop/Relative.v \
Prop/Sterbenz.v \
Prop/Round_odd.v \
Prop/Double_rounding.v \
IEEE754/Binary.v \
IEEE754/Bits.v
OBJS = $(addprefix src/,$(addsuffix o,$(FILES)))
EXAMPLES = \
Average.v \
Compute.v \
Double_round_beta_odd.v \
Double_rounding_odd_radix.v \
Homogen.v
MORE_EXAMPLES = \
......@@ -71,7 +70,7 @@ configure config.status: configure.in
clean:
rm -f $(OBJS) $(EOBJS) $(MOBJS) src/*.glob examples/*.glob
for d in src src/Core src/Calc src/Prop src/Appli examples; do \
for d in src src/Core src/Calc src/Prop src/IEEE754 examples; do \
rm -f $d/.coq-native/*.o $d/.coq-native/*.cm*; done
find . -type d -name ".coq-native" -empty -prune -exec rmdir "{}" \;
......@@ -88,7 +87,7 @@ install:
prefix=@prefix@
exec_prefix=@exec_prefix@
mkdir -p @libdir@
for d in Core Calc Prop Appli; do mkdir -p @libdir@/$d; done
for d in Core Calc Prop IEEE754; do mkdir -p @libdir@/$d; done
for f in $(OBJS); do cp $f @libdir@/${f#src/}; done
( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "@libdir@/{}" \; )
......@@ -96,7 +95,7 @@ EXTRA_DIST = \
configure
REMOVE_FROM_DIST = \
src/Appli/Fappli_Axpy.v \
examples/Axpy.v \
src/Translate/
dist: $(EXTRA_DIST)
......
......@@ -68,5 +68,5 @@ MINGW*)
;;
esac
AC_CONFIG_FILES([Remakefile src/Flocq_version.v])
AC_CONFIG_FILES([Remakefile src/Version.v])
AC_OUTPUT
Require Import Fcore.
Require Import Fprop_plus_error.
Require Import Fourier.
From Flocq Require Import Core Plus_error.
Open Scope R_scope.
......
Require Import Fcore.
Require Import Fcalc_bracket Fcalc_round Fcalc_ops Fcalc_div Fcalc_sqrt.
From Flocq Require Import Core Bracket Round Operations Div Sqrt.
Section Compute.
......
(** * Conditions for innocuous double rounding. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_generic_fmt.
Require Import Fcalc_ops.
Require Import Fcore_ulp.
Require Import Fappli_double_round.
Require Import Psatz.
From Flocq Require Import Raux Definitions Generic_fmt Operations Ulp.
From Flocq Require Import FLX FLT FTZ Double_rounding.
Open Scope R_scope.
......@@ -23,22 +17,22 @@ Ltac bpow_simplify :=
(* bpow ex * bpow ey ~~> bpow (ex + ey) *)
repeat
match goal with
| |- context [(Fcore_Raux.bpow _ _ * Fcore_Raux.bpow _ _)] =>
| |- context [(Raux.bpow _ _ * Raux.bpow _ _)] =>
rewrite <- bpow_plus
| |- context [(?X1 * Fcore_Raux.bpow _ _ * Fcore_Raux.bpow _ _)] =>
| |- context [(?X1 * Raux.bpow _ _ * Raux.bpow _ _)] =>
rewrite (Rmult_assoc X1); rewrite <- bpow_plus
| |- context [(?X1 * (?X2 * Fcore_Raux.bpow _ _) * Fcore_Raux.bpow _ _)] =>
| |- context [(?X1 * (?X2 * Raux.bpow _ _) * Raux.bpow _ _)] =>
rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 * X2));
rewrite <- bpow_plus
end;
(* ring_simplify arguments of bpow *)
repeat
match goal with
| |- context [(Fcore_Raux.bpow _ ?X)] =>
| |- context [(Raux.bpow _ ?X)] =>
progress ring_simplify X
end;
(* bpow 0 ~~> 1 *)
change (Fcore_Raux.bpow _ 0) with 1;
change (Raux.bpow _ 0) with 1;
repeat
match goal with
| |- context [(_ * 1)] =>
......@@ -836,8 +830,6 @@ Qed.
Section Double_round_mult_beta_odd_FLX.
Require Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -864,9 +856,6 @@ End Double_round_mult_beta_odd_FLX.
Section Double_round_mult_beta_odd_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -897,8 +886,6 @@ End Double_round_mult_beta_odd_FLT.
Section Double_round_mult_beta_odd_FTZ.
Require Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -1169,8 +1156,6 @@ Qed.
Section Double_round_plus_beta_odd_FLX.
Require Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -1213,9 +1198,6 @@ End Double_round_plus_beta_odd_FLX.
Section Double_round_plus_beta_odd_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -1266,8 +1248,6 @@ End Double_round_plus_beta_odd_FLT.
Section Double_round_plus_beta_odd_FTZ.
Require Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -1547,8 +1527,6 @@ Qed.
Section Double_round_sqrt_beta_odd_FLX.
Require Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -1574,9 +1552,6 @@ End Double_round_sqrt_beta_odd_FLX.
Section Double_round_sqrt_beta_odd_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -1606,8 +1581,6 @@ End Double_round_sqrt_beta_odd_FLT.
Section Double_round_sqrt_beta_odd_FTZ.
Require Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -2273,8 +2246,6 @@ Qed.
Section Double_round_div_beta_odd_rna_FLX.
Require Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -2304,9 +2275,6 @@ End Double_round_div_beta_odd_rna_FLX.
Section Double_round_div_beta_odd_rna_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -2340,9 +2308,6 @@ End Double_round_div_beta_odd_rna_FLT.
Section Double_round_div_beta_odd_rna_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......
Require Import Reals.
Require Import Fcore.
Require Import Fcalc_ops.
Require Import Psatz.
Require Import Fprop_relative.
Require Import Fprop_plus_error.
Require Import Reals Psatz.
From Flocq Require Import Core Operations Relative Plus_error.
Section Theory.
......
......@@ -19,9 +19,7 @@ COPYING file for more details.
(** * 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.
Require Import Fcore_float_prop.
Require Import Raux Definitions Float_prop.
Section Fcalc_bracket.
......
......@@ -19,12 +19,7 @@ COPYING file for more details.
(** * Helper function and theorem for computing the rounded quotient of two floating-point numbers. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Fcore_digits.
Require Import Fcalc_bracket.
Require Import Fcalc_digits.
Require Import Raux Definitions Float_prop Digits Bracket.
Section Fcalc_div.
......
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010-2013 Sylvie Boldo
#<br />#
Copyright (C) 2010-2013 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.
*)
(** * Functions for computing the number of digits of integers and related theorems. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Fcore_digits.
Section Fcalc_digits.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Theorem Zdigits_ln_beta :
forall n,
n <> Z0 ->
Zdigits beta n = ln_beta beta (Z2R n).
Proof.
intros n Hn.
destruct (ln_beta beta (Z2R n)) as (e, He) ; simpl.
specialize (He (Z2R_neq _ _ Hn)).
rewrite <- Z2R_abs in He.
assert (Hd := Zdigits_correct beta n).
assert (Hd' := Zdigits_gt_0 beta n).
apply Zle_antisym ; apply (bpow_lt_bpow beta).
apply Rle_lt_trans with (2 := proj2 He).
rewrite <- Z2R_Zpower by omega.
now apply Z2R_le.
apply Rle_lt_trans with (1 := proj1 He).
rewrite <- Z2R_Zpower by omega.
now apply Z2R_lt.
Qed.
Theorem ln_beta_F2R_Zdigits :
forall m e, m <> Z0 ->
(ln_beta beta (F2R (Float beta m e)) = Zdigits beta m + e :> Z)%Z.
Proof.
intros m e Hm.
rewrite ln_beta_F2R with (1 := Hm).
apply (f_equal (fun v => Zplus v e)).
apply sym_eq.
now apply Zdigits_ln_beta.
Qed.
End Fcalc_digits.
......@@ -18,9 +18,7 @@ COPYING file for more details.
*)
(** Basic operations on floats: alignment, addition, multiplication *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Raux Definitions Float_prop.
Section Float_ops.
......
......@@ -19,10 +19,7 @@ COPYING file for more details.
(** * Helper function for computing the rounded value of a real number. *)
Require Import Fcore.
Require Import Fcore_digits.
Require Import Fcalc_bracket.
Require Import Fcalc_digits.
Require Import Core Digits Bracket.
Section Fcalc_round.
......
......@@ -19,12 +19,7 @@ COPYING file for more details.
(** * Helper functions and theorems for computing the rounded square root of a floating-point number. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_digits.
Require Import Fcore_float_prop.
Require Import Fcalc_bracket.
Require Import Fcalc_digits.
Require Import Raux Definitions Digits Float_prop Bracket.
Section Fcalc_sqrt.
......
......@@ -18,13 +18,5 @@ COPYING file for more details.
*)
(** To ease the import *)
Require Export Fcore_Raux.
Require Export Fcore_defs.
Require Export Fcore_float_prop.
Require Export Fcore_rnd.
Require Export Fcore_generic_fmt.
Require Export Fcore_rnd_ne.
Require Export Fcore_FIX.
Require Export Fcore_FLX.
Require Export Fcore_FLT.
Require Export Fcore_ulp.
Require Export Raux Definitions Float_prop Round_pred Generic_fmt Round_NE.
Require Export FIX FLX FLT Ulp.
......@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** * Basic definitions: float and rounding property *)
Require Import Fcore_Raux.
Require Import Raux.
Section Def.
......
......@@ -17,9 +17,8 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
Require Import ZArith.
Require Import Zquot.
Require Import Fcore_Zaux.
Require Import ZArith Zquot.
Require Import Zaux.
(** Number of bits (radix 2) of a positive integer.
......
......@@ -18,12 +18,7 @@ COPYING file for more details.
*)
(** * Fixed-point format *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_ulp.
Require Import Fcore_rnd_ne.
Require Import Raux Definitions Round_pred Generic_fmt Ulp Round_NE.
Section RND_FIX.
......
......@@ -18,15 +18,8 @@ COPYING file for more details.
*)
(** * Floating-point format with gradual underflow *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Fcore_FLX.
Require Import Fcore_FIX.
Require Import Fcore_ulp.
Require Import Fcore_rnd_ne.
Require Import Raux Definitions Round_pred Generic_fmt Float_prop.
Require Import FLX FIX Ulp Round_NE.
Section RND_FLT.
......
......@@ -18,14 +18,8 @@ COPYING file for more details.
*)
(** * Floating-point format without underflow *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Fcore_FIX.
Require Import Fcore_ulp.
Require Import Fcore_rnd_ne.
Require Import Raux Definitions Round_pred Generic_fmt Float_prop.
Require Import FIX Ulp Round_NE.
Section RND_FLX.
......
......@@ -18,13 +18,8 @@ COPYING file for more details.
*)
(** * Floating-point format with abrupt underflow *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Fcore_ulp.
Require Import Fcore_FLX.
Require Import Raux Definitions Round_pred Generic_fmt.
Require Import Float_prop Ulp FLX.
Section RND_FTZ.
......
......@@ -18,13 +18,11 @@ COPYING file for more details.
*)
(** * Basic properties of floating-point formats: lemmas about mantissa, exponent... *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Raux Definitions Digits.
Section Float_prop.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Theorem Rcompare_F2R :
......@@ -453,6 +451,37 @@ apply ln_beta_mult_bpow.
exact (Z2R_neq m 0 H).
Qed.
Theorem Zdigits_ln_beta :
forall n,
n <> Z0 ->
Zdigits beta n = ln_beta beta (Z2R n).
Proof.
intros n Hn.
destruct (ln_beta beta (Z2R n)) as (e, He) ; simpl.
specialize (He (Z2R_neq _ _ Hn)).
rewrite <- Z2R_abs in He.
assert (Hd := Zdigits_correct beta n).
assert (Hd' := Zdigits_gt_0 beta n).
apply Zle_antisym ; apply (bpow_lt_bpow beta).
apply Rle_lt_trans with (2 := proj2 He).
rewrite <- Z2R_Zpower by omega.
now apply Z2R_le.
apply Rle_lt_trans with (1 := proj1 He).
rewrite <- Z2R_Zpower by omega.
now apply Z2R_lt.
Qed.
Theorem ln_beta_F2R_Zdigits :
forall m e, m <> Z0 ->
(ln_beta beta (F2R (Float beta m e)) = Zdigits beta m + e :> Z)%Z.
Proof.
intros m e Hm.
rewrite ln_beta_F2R with (1 := Hm).
apply (f_equal (fun v => Zplus v e)).
apply sym_eq.
now apply Zdigits_ln_beta.
Qed.
Theorem float_distribution_pos :
forall m1 e1 m2 e2 : Z,
(0 < m1)%Z ->
......
......@@ -18,10 +18,7 @@ COPYING file for more details.
*)
(** * What is a real number belonging to a format, and many properties. *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_float_prop.
Require Import Raux Definitions Round_pred Float_prop.
Section Generic.
......@@ -1968,7 +1965,7 @@ Qed.
Lemma round_N_really_small_pos :
forall x,
forall ex,
(Fcore_Raux.bpow beta (ex - 1) <= x < Fcore_Raux.bpow beta ex)%R ->
(Raux.bpow beta (ex - 1) <= x < Raux.bpow beta ex)%R ->
(ex < fexp ex)%Z ->
(round Znearest x = 0)%R.
Proof.
......@@ -2000,7 +1997,7 @@ apply Rle_trans with (bpow (fexp (ln_beta beta x) - 1)).
- unfold Zminus; rewrite bpow_plus.
rewrite Rmult_comm.
apply Rmult_le_compat_r; [now apply bpow_ge_0|].
unfold Fcore_Raux.bpow, Z.pow_pos; simpl.
unfold Raux.bpow, Z.pow_pos; simpl.
rewrite Zmult_1_r.
apply Rinv_le; [exact Rlt_0_2|].
change 2%R with (Z2R 2); apply Z2R_le.
......
......@@ -18,9 +18,8 @@ COPYING file for more details.
*)
(** * Missing definitions/lemmas *)
Require Export Reals.
Require Export ZArith.
Require Export Fcore_Zaux.
Require Export Reals ZArith.
Require Export Zaux.
Section Rmissing.
......
......@@ -18,12 +18,7 @@ COPYING file for more details.
*)
(** * Rounding to nearest, ties to even: existence, unicity... *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Fcore_ulp.
Require Import Raux Definitions Round_pred Generic_fmt Float_prop Ulp.
Notation ZnearestE := (Znearest (fun x => negb (Zeven x))).
......@@ -276,7 +271,7 @@ intros Hd1.
case_eq (Zeven md) ; [ intros He | intros Ho ].
right.
exists (Float beta md ed).
unfold Fcore_generic_fmt.canonic.
unfold Generic_fmt.canonic.
rewrite <- Hd1.
now repeat split.
left.
......@@ -287,15 +282,15 @@ set (mu := Ztrunc (scaled_mantissa beta fexp u)).
intros Hu1.
rewrite Hu1.
eexists ; repeat split.
unfold Fcore_generic_fmt.canonic.
unfold Generic_fmt.canonic.
now rewrite <- Hu1.
rewrite (DN_UP_parity_generic x (Float beta md ed) (Float beta mu eu)).
simpl.
now rewrite Ho.
exact Hf.
unfold Fcore_generic_fmt.canonic.
unfold Generic_fmt.canonic.
now rewrite <- Hd1.
unfold Fcore_generic_fmt.canonic.
unfold Generic_fmt.canonic.
now rewrite <- Hu1.
rewrite <- Hd1.
apply Rnd_DN_pt_unicity with (1 := Hd).
......@@ -355,7 +350,7 @@ exists (Float beta (Ztrunc (scaled_mantissa beta fexp xr)) (canonic_exp beta fex
split.
apply round_N_pt...
split.
unfold Fcore_generic_fmt.canonic. simpl.
unfold Generic_fmt.canonic. simpl.
apply f_equal.
apply round_N_pt...
simpl.
......
......@@ -18,8 +18,7 @@ COPYING file for more details.
*)
(** * Roundings: properties and/or functions *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Raux Definitions.
Section RND_prop.
......
......@@ -18,11 +18,7 @@ COPYING file for more details.
*)
(** * Unit in the Last Place: our definition using fexp and its properties, successor and predecessor *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Raux Definitions Round_pred Generic_fmt Float_prop.
Section Fcore_ulp.
......
......@@ -18,15 +18,7 @@ COPYING file for more details.
*)
(** * IEEE-754 arithmetic *)
Require Import Fcore.
Require Import Fcore_digits.
Require Import Fcalc_digits.
Require Import Fcalc_round.
Require Import Fcalc_bracket.
Require Import Fcalc_ops.
Require Import Fcalc_div.
Require Import Fcalc_sqrt.
Require Import Fprop_relative.
Require Import Core Digits Round Bracket Operations Div Sqrt Relative.
Section AnyRadix.
......
......@@ -18,10 +18,7 @@ COPYING file for more details.
*)
(** * IEEE-754 encoding of binary floating-point data *)
Require Import Fcore.
Require Import Fcore_digits.
Require Import Fcalc_digits.
Require Import Fappli_IEEE.
Require Import Core Digits Binary.
Section Binary_Bits.
......
......@@ -18,9 +18,7 @@ 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.
Require Import Core Operations Relative.