# 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 `test.g`, pass it to Gappa, and store the generated Coq proof in 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.

    $ 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.

    $ 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.

-Bnull

  Do not enable any back-end. This is the default behavior. This is also the only back-end compatible with the `-Munconstrained` 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.

-Blatex

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

-Bd2

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

-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

-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.

-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 \(2^{100}\) intervals of width \(2^{-100}\) relatively to the original interval. This should be sufficient for most uses too.

-Ereverted-fma

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

-Eno-reverted-fma

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

-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.

-Eauto-dichotomy

  This option causes Gappa to select an expression on which to perform a dichotomy. This is the default behavior if the logical formula contains no unspecified intervals.

-Eno-auto-dichotomy

  This option disables the automatic selection of a dichotomy setting.

### Setting modes

These options cannot be embedded into scripts.

-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.

      { 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

-Mstatistics

  At the end of its computations, Gappa displays some statistics. For example, the second script of Fixed-point Newton division 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 parsing and during computations.

-Wnull-denominator

-Wno-null-denominator

-Whint-difference

-Wno-hint-difference

-Wunbound-variable

-Wno-unbound-variable

-Wdichotomy-failure

-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`.