diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 103 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 44 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 13 |
3 files changed, 158 insertions, 2 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index ac75240cfb..cad5e4e67e 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -756,6 +756,7 @@ subdirectories: * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees) * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...) + * **Floats** : Machine implementation of floating-point arithmetic (for the binary64 format) * **Relations** : Relations (definitions and basic results) * **Sorting** : Sorted list (basic definitions and heapsort correctness) * **Strings** : 8-bits characters and strings @@ -768,7 +769,7 @@ are directly accessible with the command ``Require`` (see Section :ref:`compiled-files`). The different modules of the |Coq| standard library are documented -online at http://coq.inria.fr/stdlib. +online at https://coq.inria.fr/stdlib. Peano’s arithmetic (nat) ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -988,6 +989,106 @@ Notation Interpretation Precedence Associativity ``_ :: _`` ``cons`` 60 right ========== ============== ========== ============= +.. _floats_library: + +Floats library +~~~~~~~~~~~~~~ + +The library of primitive floating-point arithmetic can be loaded by +requiring module ``Floats``: + +.. coqtop:: in + + Require Import Floats. + +It exports the module ``PrimFloat`` that provides a primitive type +named ``float``, defined in the kernel (see section :ref:`primitive-floats`), +as well as two variant types ``float_comparison`` and ``float_class``: + + +.. coqtop:: all + + Print float. + Print float_comparison. + Print float_class. + +It then defines the primitive operators below, using the processor +floating-point operators for binary64 in rounding-to-nearest even: + +* ``abs`` +* ``opp`` +* ``sub`` +* ``add`` +* ``mul`` +* ``div`` +* ``sqrt`` +* ``compare`` : compare two floats and return a ``float_comparison`` +* ``classify`` : analyze a float and return a ``float_class`` +* ``of_int63`` : round a primitive integer and convert it into a float +* ``normfr_mantissa`` : take a float in ``[0.5; 1.0)`` and return its mantissa +* ``frshiftexp`` : convert a float to fractional part in ``[0.5; 1.0)`` and integer part +* ``ldshiftexp`` : multiply a float by an integral power of ``2`` +* ``next_up`` : return the next float towards positive infinity +* ``next_down`` : return the next float towards negative infinity + +For special floating-point values, the following constants are also +defined: + +* ``zero`` +* ``neg_zero`` +* ``one`` +* ``two`` +* ``infinity`` +* ``neg_infinity`` +* ``nan`` : Not a Number (assumed to be unique: the "payload" of NaNs is ignored) + +The following table shows the notations available when opening scope +``float_scope``. + +=========== ============== +Notation Interpretation +=========== ============== +``- _`` ``opp`` +``_ - _`` ``sub`` +``_ + _`` ``add`` +``_ * _`` ``mul`` +``_ / _`` ``div`` +``_ == _`` ``eqb`` +``_ < _`` ``ltb`` +``_ <= _`` ``leb`` +``_ ?= _`` ``compare`` +=========== ============== + +Floating-point constants are parsed and pretty-printed as (17-digit) +decimal constants. This ensures that the composition +:math:`\text{parse} \circ \text{print}` amounts to the identity. + +.. example:: + + .. coqtop:: all + + Open Scope float_scope. + Eval compute in 1 + 0.5. + Eval compute in 1 / 0. + Eval compute in 1 / -0. + Eval compute in 0 / 0. + Eval compute in 0 ?= -0. + Eval compute in nan ?= nan. + Eval compute in next_down (-1). + +The primitive operators are specified with respect to their Gallina +counterpart, using the variant type ``spec_float``, and the injection +``Prim2SF``: + +.. coqtop:: all + + Print spec_float. + Check Prim2SF. + Check mul_spec. + +For more details on the available definitions and lemmas, see the +online documentation of the ``Floats`` library. + .. _userscontributions: Users’ contributions diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f50cf9340c..3f122f122b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2411,7 +2411,7 @@ by means of the interactive proof engine. .. _primitive-integers: Primitive Integers --------------------------------- +------------------ The language of terms features 63-bit machine integers as values. The type of such a value is *axiomatized*; it is declared through the following sentence @@ -2464,6 +2464,48 @@ wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on 64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the function :g:`Uint63.compile` from the kernel). +.. _primitive-floats: + +Primitive Floats +---------------- + +The language of terms features Binary64 floating-point numbers as values. +The type of such a value is *axiomatized*; it is declared through the +following sentence (excerpt from the :g:`PrimFloat` module): + +.. coqdoc:: + + Primitive float := #float64_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, the product of two primitive floats can be computed using the +:g:`PrimFloat.mul` function, declared and specified as follows: + +.. coqdoc:: + + Primitive mul := #float64_mul. + Notation "x * y" := (mul x y) : float_scope. + + Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y). + +where :g:`Prim2SF` is defined in the :g:`FloatOps` module. + +The set of such operators is described in section :ref:`floats_library`. + +These primitive declarations are regular axioms. As such, they must be trusted, and are listed by the +:g:`Print Assumptions` command. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient rules to reduce the applications of these primitive +operations, using the floating-point processor operators that are assumed +to comply with the IEEE 754 standard for floating-point arithmetic. + +These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to +types and functions of a :g:`Float64` module. Said module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. + Bidirectionality hints ---------------------- diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index f0ada745e7..eedd8a3d61 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -328,6 +328,19 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/Binary/ZBinary.v theories/Numbers/Integer/NatPairs/ZNatPairs.v </dd> + + <dt> <b> Floats</b>: + Floating-point arithmetic + </dt> + <dd> + theories/Floats/FloatClass.v + theories/Floats/PrimFloat.v + theories/Floats/SpecFloat.v + theories/Floats/FloatOps.v + theories/Floats/FloatAxioms.v + theories/Floats/FloatLemmas.v + (theories/Floats/Floats.v) + </dd> </dl> </dd> |