Invoking Gappa
==============

Input and output
----------------

Gappa reads the script whose filename is passed as an argument to the
tool, or on its standard input if none. Such a script is made of three
parts: the definitions, the logical formula, and the hints. Warning
messages, error messages, and results, are displayed on the standard
error output. Gappa also sends to the standard output a formal proof of
the logical formula; its format depends on the selected back-end.
Finally, if the tool was unable to prove some goals, its return code is
a nonzero value.

For example, the following command lines create a simple script in file
:file:`test.g`, pass it to Gappa, and store the generated Coq proof in file
:file:`test.v` file. They also test the return code of Gappa and send the
generated proof to Coq so that it is automatically checked. Since the
proof checker does not display anything, it means no errors were
detected and the result computed by Gappa is correct.

.. code-block:: console

   $ echo "{ x in [-2,2] -> x * x in ? }" > test.g

   $ gappa -Bcoq test.g > test.v
   Results:
     x * x in [0, 4]

   $ echo "Return code is $?"
   Return code is 0

   $ coqc test.v

Note that, if no ranges are left unspecified in the logical formula,
Gappa will not have anything to display in case of success.

.. code-block:: console

   $ echo "{ 1 + 1 = 2 }" | gappa

   $ echo "Return code is $?"
   Return code is 0

Command-line options
--------------------

Selecting a proof back-end
~~~~~~~~~~~~~~~~~~~~~~~~~~

These options are mutually exclusive and cannot be embedded into
scripts.

.. option:: -Bnull

   Do not enable any back-end. This is the default behavior. This is also
   the only back-end compatible with the :option:`-Munconstrained`
   option.

.. option:: -Bcoq

   When this back-end is selected, Gappa generates a script that proves
   the logical formula. This script can be mechanically verified by the
   Coq proof checker. It can also be reused in bigger formal developments
   made with Coq.

.. option:: -Blatex

   When this back-end is selected, Gappa generates a Latex file that
   contains the steps for proving the logical formula.

.. option:: -Bcoq-lambda

   This back-end is used by the ``gappa`` tactic available for the Coq
   proof checker. It generates a lambda-term that can be directly loaded
   by the proof checker, but it only supports the features needed by the
   tactic. For instance, it does not support rewriting rules.

Setting internal parameters
~~~~~~~~~~~~~~~~~~~~~~~~~~~

.. option:: -Eprecision=<integer>

   This option sets the internal MPFR precision that Gappa uses when
   computing bounds of intervals. The default value is 60 and should be
   sufficient for most uses.

.. option:: -Edichotomy=<integer>

   This option limits the depth of a dichotomy split. The default value
   is 100. It means that an interval of width 1 is potentially split
   into :math:`2^{100}` intervals of width :math:`2^{-100}` relatively to
   the original interval. This should be sufficient for most uses too.

.. option:: -Ereverted-fma

   This option causes Gappa to Interpret ``fma(a,b,c)``  as ``c + a * b``.

.. option:: -Eno-reverted-fma

   This option causes Gappa to interpret ``fma(a,b,c)`` as ``a * b + c``.
   This is the default behavior.

.. option:: -Echange-threshold=<float>

   When Gappa discovers a new result, it compares it to the ones
   previously found. If the changes are smaller than the threshold, the
   new result is discarded. The threshold is a floating-point value
   between 0 and 1. Setting it to 0 prevents Gappa from ever discarding
   a better result. By default, its value is 0.01, that is, interval
   bounds or widths have to improve by at least one percent.

.. option:: -Eauto-dichotomy

   This option causes Gappa to select an expression on which to perform
   a :ref:`dichotomy <hint-dichotomy>`. This is the default behavior if the
   logical formula contains no unspecified intervals.

.. option:: -Eno-auto-dichotomy

   This option disables the automatic selection of a dichotomy setting.

Setting modes
~~~~~~~~~~~~~

These options cannot be embedded into scripts.

.. option:: -Munconstrained

   By default, Gappa checks that all the hypotheses hold before applying
   a theorem. This mode weakens the engine by making it skip hypotheses
   that are not needed for computing intermediate results. For example,
   Gappa will no longer check that ``x`` is not zero before applying the
   lemma proving ``x / x in [1,1]``.

   This mode is especially useful when starting a proof on relative
   errors, as it makes it possible to get some early results about them
   without having to prove that they are well-defined.

   At the end of its run, Gappa displays all the facts that are left
   unproven. In the following example, the property ``NZR`` indicates
   that Gappa possibly needs to prove that some values are not zero.

   .. code-block:: gappa

      { x in [1,2] ->
        (x + 1) / (x + 1) in ? /\ (x - 1) / (x - 1) in ? }

   ::

      Results:
        (x + 1) / (x + 1) in [1, 1]
        (x - 1) / (x - 1) in [1, 1]
      Warning: some properties were assumed:
        NZR(x + 1)
        NZR(x - 1)

   Notice that Gappa has assumed ``x + 1`` to be nonzero, while it
   actually can be deduced from ``x in [1,2].`` So there might be false
   positives among assumptions, depending on the order Gappa deduced
   properties.

   This mode cannot be used when a proof back-end is selected, as
   a generated proof would contain holes. It is, however, as slow as if
   a back-end had been selected, since the whole proof graph is kept
   around.

Gathering statistics
^^^^^^^^^^^^^^^^^^^^

.. option:: -Mstatistics

   At the end of its computations, Gappa displays some statistics. For
   example, the second script of :ref:`example-fixed` gives:

   ::

      Statistics:
        2359 expressions were considered,
          but then 127 of those got discarded.
        6317 theorems were considered,
          but then 326 of those got discarded.
        7437 applications were tried. Among those,
          5933 were successful,
          yet 2626 proved useless
          and 13 improved existing results.

   The first two lines show how many intermediate expressions Gappa has
   prepared. The first number tells how many have been considered, and
   the second number tells how many of them were discarded because no
   theorem could handle them. Similarly, the next two lines show how many
   theorem instances Gappa has prepared. The first number tells how many
   have been considered, and the second number tells how many of them
   were discarded because their hypotheses could never have been
   satisfied.

   Once both sets are ready, Gappa tries to deduce new properties by
   repeatedly applying the prepared theorems. The next statistic show how
   many of those theorems Gappa tried to apply. Applications are
   successful if Gappa could satisfy theorem hypotheses. Even if an
   application succeeded, the deduced property could have been (partly)
   useless because a stronger property had already been found at the time
   the theorem was applied. The last two lines track these cases.

Enabling and disabling warning messages
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

By default, all the warning messages are enabled. See appendix for details
on warning messages displayed during :ref:`parsing <warning-messages1>`
and during :ref:`computations <warning-messages2>`.

.. option:: -Wnull-denominator
.. option:: -Wno-null-denominator
.. option:: -Whint-difference
.. option:: -Wno-hint-difference
.. option:: -Wunbound-variable
.. option:: -Wno-unbound-variable
.. option:: -Wdichotomy-failure
.. option:: -Wno-dichotomy-failure


Embedded options
----------------

Options setting internal parameters or enabling warning messages can be
embedded in a Gappa proof script. It is especially important when the
logical property cannot be proved with the default parameters. These
options are passed through a special comment syntax:
``#@ -Edichotomy=200``.