Command-line options

Selecting a proof back-end

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

Null back-end.

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.

Coq back-end

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.

Latex back-end

Option: -Blatex

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

Coq lambda-term back-end

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

Internal precision

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.

Dichotomy depth

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.

Fused multiply-add format

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.

Threshold for accepting new results

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.

Automatic dichotomy

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.

Setting modes

These options cannot be embedded into scripts.

Assuming vague hypotheses

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 ? }
  (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 the section called “Fixed-point Newton division” gives:

  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 annex for details on warning messages displayed during parsing and during computations.