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

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] intervals of width [math] relatively to the original interval. This should be sufficient for most uses too.

Option: `-E[no-]reverted-fma`

By default (`-Eno-reverted-fma`

), the expression
`fma(a,b,c)`

is interpreted as `a * b + c`

. As this may
not be the preferred order for the operands, the option makes Gappa use
`c + a * b`

instead.

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: `-E[no-]auto-dichotomy`

Gappa can automatically select an expression on which to perform a dichotomy. This behavior is disabled if the logical formula contains some unspecified intervals. It can also be disabled using this option.

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.

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

Option: `-Mstatistics`

At the end of its computations, Gappa displays some statistics. For example, the second script of the section called “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.

By default, all the warning messages are enabled. See annex for details on warning messages displayed during parsing and during computations.