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 backend. 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
Commandline options¶
Selecting a proof backend¶
These options are mutually exclusive and cannot be embedded into scripts.

Bnull
¶
Do not enable any backend. This is the default behavior. This is also the only backend compatible with the
Munconstrained
option.

Bcoq
¶
When this backend 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 backend is selected, Gappa generates a Latex file that contains the steps for proving the logical formula.

Bcoqlambda
¶
This backend is used by the
gappa
tactic available for the Coq proof checker. It generates a lambdaterm 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.

Erevertedfma
¶
This option causes Gappa to Interpret
fma(a,b,c)
asc + a * b
.

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

Echangethreshold
=<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 floatingpoint 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.

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

Enoautodichotomy
¶
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 provingx / 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 welldefined.
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 fromx 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 backend is selected, as a generated proof would contain holes. It is, however, as slow as if a backend 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 Fixedpoint 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.

Wnulldenominator
¶

Wnonulldenominator
¶

Whintdifference
¶

Wnohintdifference
¶

Wunboundvariable
¶

Wnounboundvariable
¶

Wdichotomyfailure
¶

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