There are three categories of theorems in Gappa: theorems about real arithmetic, theorems about rounding operators, and rewriting rules.

In the following, variables `a`

, `b`

,
`c`

, and `d`

, represent arbitrary expressions.
Gappa is using backward reasoning, so they are filled by matching the
goal of a theorem against the property Gappa wants to compute. If some
theorem mentions both `a`

and `b`

but only one of
them appears on the right-hand side, then Gappa infers the other one so
that `b`

is an approximate value of `a`

. See the section called “Approximated expressions” for more details. There may be additional
constraints on the expressions that require some of them to be
syntactically different (denoted `a ≠ b`

), or to be
syntactically constant (denoted `a=`

), or to be syntactically
variable (denoted `a~`

).

Theorem name | Goal | Hypotheses | Constraints |
---|---|---|---|

`sub_of_eql` | `BND(a - b)` | `EQL(a, b)` | `a ≠ b` , `(a - b)~` |

`eql_of_cst` | `EQL(a, b)` | `BND(a)` , `BND(b)` | `a=` , `b=` |

`rel_refl` | `REL(a, a)` | ||

`eql_trans` | `EQL(b, c)` | `EQL(b, a)` , `EQL(a, c)` | `a ≠ c` |

`eql_trans` | `EQL(c, a)` | `EQL(c, b)` , `EQL(b, a)` | `b ≠ c` |

`neg` | `BND(-a)` | `BND(a)` | |

`sqrt` | `BND(sqrt(a))` | `BND(a)` | |

`sub_refl` | `BND(a - a)` | ||

`div_refl` | `BND(a / a)` | `NZR(a)` | |

`square` | `BND(a * a)` | `ABS(a)` | |

`neg_a` | `ABS(-a)` | `ABS(a)` | |

`abs_a` | `ABS(|a|)` | `ABS(a)` | |

`add` | `BND(a + b)` | `BND(a)` , `BND(b)` | |

`sub` | `BND(a - b)` | `BND(a)` , `BND(b)` | `a ≠ b` |

`mul_{nop}{nop}` | `BND(a * b)` | `BND(a)` , `BND(b)` | |

`div_{nop}{np}` | `BND(a / b)` | `BND(a)` , `BND(b)` | `a ≠ b` |

`add_aa_{nop}` | `ABS(a + b)` | `ABS(a)` , `ABS(b)` | |

`sub_aa_{nop}` | `ABS(a - b)` | `ABS(a)` , `ABS(b)` | |

`mul_aa` | `ABS(a * b)` | `ABS(a)` , `ABS(b)` | |

`div_aa` | `ABS(a / b)` | `ABS(a)` , `ABS(b)` | |

`bnd_of_abs` | `BND(a)` | `ABS(a)` | `a ≠ |?|` |

`abs_of_bnd_{nop}` | `ABS(a)` | `BND(a)` | `a ≠ |?|` |

`bnd_of_bnd_abs_{np}` | `BND(a)` | `BND(a)` , `ABS(a)` | `a ≠ |?|` |

`uabs_of_abs` | `BND(|a|)` | `ABS(a)` | |

`abs_of_uabs` | `ABS(a)` | `BND(|a|)` | `a ≠ |?|` , `a~` |

`constant{1,2,10}` | `BND(a)` | `a` number | |

`abs_fix` | `FIX(|a|)` | `FIX(a)` | `a~` |

`abs_flt` | `FLT(|a|)` | `FLT(a)` | `a~` |

`neg_fix` | `FIX(-a)` | `FIX(a)` | `a~` |

`neg_flt` | `FLT(-a)` | `FLT(a)` | `a~` |

`add_fix` | `FIX(a + b)` | `FIX(a)` , `FIX(b)` | `a~` or `b~` |

`sub_fix` | `FIX(a - b)` | `FIX(a)` , `FIX(b)` | `a~` or `b~` |

`sub_flt` | `FLT(a - b)` | `FLT(a)` , `FLT(b)` , `REL(a,b)` | `a~` or `b~` |

`sub_flt_rev` | `FLT(b - a)` | `FLT(a)` , `FLT(b)` , `REL(a,b)` | `a~` or `b~` |

`mul_fix` | `FIX(a * b)` | `FIX(a)` , `FIX(b)` | `a~` or `b~` |

`mul_flt` | `FLT(a * b)` | `FLT(a)` , `FLT(b)` | `a~` or `b~` |

`fix_of_flt_bnd` | `FIX(a)` | `FLT(a)` , `ABS(a)` | `a~` , `a ≠ -?` , `a ≠ |?|` |

`flt_of_fix_bnd` | `FLT(a)` | `FIX(a)` , `ABS(a)` | `a~` , `a ≠ -?` , `a ≠ |?|` |

`fix_of_singleton_bnd` | `FIX(a)` | `ABS(a)` | |

`flt_of_singleton_bnd` | `FLT(a)` | `ABS(a)` | |

`bnd_of_nzr_rel` | `BND((b - a) / a)` | `NZR(a)` , `REL(b,a)` | `a ≠ b` |

`rel_of_nzr_bnd` | `REL(a, b)` | `NZR(b)` , `BND((a - b) / b)` | `a ≠ b` |

`add_rr` | `REL(a + b, c + d)` | `REL(a, c)` , `REL(b, d)` , `BND(c / (c + d))` , `NZR(c + d)` | |

`sub_rr` | `REL(a - b, c - d)` | `REL(a, c)` , `REL(b, d)` , `BND(c / (c - d))` , `NZR(c - d)` | |

`mul_rr` | `REL(a * b, c * d)` | `REL(a, c)` , `REL(b, d)` | `a ≠ c` , `b ≠ d` |

`div_rr` | `REL(a / b, c / d)` | `REL(a, c)` , `REL(b, d)` , `NZR(d)` | `a ≠ c` , `b ≠ d` |

`compose` | `REL(b, c)` | `REL(b, a)` , `REL(a, c)` | `a ≠ c` |

`compose` | `REL(c, a)` | `REL(c, b)` , `REL(b, a)` | `b ≠ c` |

`compose_swap` | `REL(c * b, d)` | `REL(c, d * a')` , `REL(b, 1 / a')` , `NZR(a')` | `a = 1 / a'` |

`error_of_rel_{nop}{nop}` | `BND(b - a)` | `REL(b, a)` , `BND(a)` | `a ≠ b` |

`nzr_of_abs` | `NZR(a)` | `ABS(a)` | |

`nzr_of_nzr_rel` | `NZR(b)` | `NZR(a)` , `REL(b, a)` | |

`nzr_of_nzr_rel_rev` | `NZR(a)` | `NZR(b)` , `REL(b, a)` | |

`bnd_div_of_rel_bnd_div` | `BND((b - a) / c)` | `REL(b, a)` , `BND(a / c)` , `NZR(c)` |

The following table describes the kind of theorems that can be applied to rounding operators. These theorems have no specific names, as each rounding operator comes with its dedicated set of theorems. When a specific theorem is not available for a given rounding operator, its effect can usually be obtained through an available one combined with a rewriting rule.

Goal | Hypothesis | Rounding kind |
---|---|---|

`BND(rnd(a))` | `BND(a)` | fixed, float |

`BND(rnd(a))` | `BND(rnd(a))` | float |

`BND(rnd(a) - a)` | fixed | |

`BND(rnd(a) - a)` | `BND(a)` | fixed (zr, aw), float (zr, aw, up, dn, nu, nd) |

`BND(rnd(a) - a)` | `ABS(a)` | float (od, ne, nz, na, no) |

`BND(rnd(a) - a)` | `BND(rnd(a))` | fixed (zr, aw), float (up, dn, nu, nd) |

`BND(rnd(a) - a)` | `ABS(rnd(a))` | float (zr, aw, od, ne, nz, na, no) |

`REL(rnd(a), a)` | ||

`REL(rnd(a), a)` | `BND(a)` | |

`REL(rnd(a), a)` | `ABS(a)` | float |

`REL(rnd(a), a)` | `BND(rnd(a))` | |

`REL(rnd(a), a)` | `ABS(rnd(a))` | float |

The following theorems are used to propagate properties about a term to some provably equal term.

Theorem name | Goal | Hypotheses |
---|---|---|

`bnd_rewrite` | `BND(a)` | `EQL(a, b)` , `BND(b)` |

`abs_rewrite` | `ABS(a)` | `EQL(a, b)` , `ABS(b)` |

`fix_rewrite` | `FIX(a)` | `EQL(a, b)` , `FIX(b)` |

`flt_rewrite` | `FLT(a)` | `EQL(a, b)` , `FLT(b)` |

`nzr_rewrite` | `NZR(a)` | `EQL(a, b)` , `NZR(b)` |

`rel_rewrite_1` | `REL(a, c)` | `EQL(a, b)` , `REL(b, c)` |

`rel_rewrite_2` | `REL(c, a)` | `EQL(a, b)` , `REL(c, b)` |

For the sake of readability, the following theorems are not written
with `BND`

predicates but rather with expressions only. When
trying to obtain some enclosure of the target expression (goal), Gappa
will first consider the source one (hypothesis). As a consequence of this
layout and contrarily to previous tables, constraints will also list
additional hypotheses needed to apply the rules. Whenever an operator is
put between square brackets, it means that only theorems that perform
basic interval arithmetic will be able to match it. A constraint written
using `USR`

means that the theorem will be applied only if a
matching expression appears in the input file.

Theorem name | Target | Source | Constraints |
---|---|---|---|

`opp_mibs` | `-a - -b` | `[-] (a - b)` | `a ≠ b` |

`add_xals` | `b + c` | `(b - a) [+] (a + c)` | |

`add_xars` | `c + b` | `(c + a) [+] (b - a)` | |

`add_mibs` | `(a + b) - (c + d)` | `(a - c) [+] (b - d)` | `a ≠ c` , `b ≠ d` |

`add_fils` | `(a + b) - (a + c)` | `b - c` | `b ≠ c` |

`add_firs` | `(a + b) - (c + b)` | `a - c` | `a ≠ c` |

`add_filq` | `((a + b) - (a + c)) / (a + c)` | `(b - c) / (a + c)` | `NZR(a + c)` , `b ≠ c` |

`add_firq` | `((a + b) - (c + b)) / (c + b)` | `(a - c) / (c + b)` | `NZR(c + b)` , `a ≠ c` |

`add_xilu` | `a` | `(a + b) [-] b` | `USR(a + b)` |

`add_xiru` | `b` | `(a + b) [-] a` | `USR(a + b)` |

`sub_xals` | `b - c` | `(b - a) [+] (a - c)` | `a ≠ c` , `b ≠ c` |

`sub_xars` | `c - b` | `(c - a) [-] (b - a)` | `b ≠ c` |

`sub_mibs` | `(a - b) - (c - d)` | `(a - c) [-] (b - d)` | `a ≠ c` , `b ≠ d` |

`sub_fils` | `(a - b) - (a - c)` | `[-] (b - c)` | `b ≠ c` |

`sub_firs` | `(a - b) - (c - b)` | `a - c` | `a ≠ c` |

`sub_filq` | `((a - b) - (a - c)) / (a - c)` | `[-] ((b - c) / (a - c))` | `NZR(a - c)` , `b ≠ c` |

`sub_firq` | `((a - b) - (c - b)) / (c - b)` | `(a - c) / (c - b)` | `NZR(c - b)` , `a ≠ c` |

`val_xabs` | `b` | `a [+] (b - a)` | `USR(b - a)` |

`val_xebs` | `a` | `b [-] (b - a)` | `USR(b - a)` |

`mul_xals` | `b * c` | `((b - a) [*] c) [+] (a * c)` | |

`mul_xars` | `c * b` | `(c [*] (b - a)) [+] (c * a)` | |

`mul_fils` | `a * b - a * c` | `a [*] (b - c)` | `b ≠ c` |

`mul_firs` | `a * b - c * b` | `(a - c) [*] b` | `a ≠ c` |

`mul_mars` | `a * b - c * d` | `(a [*] (b - d)) [+] ((a - c) [*] d)` | `a ≠ c` , `b ≠ d` |

`mul_mals` | `a * b - c * d` | `((a - c) [*] b) [+] (c [*] (b - d))` | `a ≠ c` , `b ≠ d` |

`mul_mabs` | `a * b - c * d` | `(a [*] (b - d)) [+] ((a - c) [*] b) [-] ((a - c) [*] (b - d))` | `a ≠ c` , `b ≠ d` |

`mul_mibs` | `a * b - c * d` | `(c [*] (b - d)) [+] ((a - c) [*] d) [+] ((a - c) [*] (b - d))` | `a ≠ c` , `b ≠ d` |

`mul_xilu` | `a` | `(a * b) [/] b` | `USR(a * b)` , `NZR(b)` |

`mul_xiru` | `b` | `(a * b) [/] a` | `USR(a * b)` , `NZR(a)` |

`div_xals` | `b / c` | `((b - a) / c) [+] (a / c)` | `NZR(c)` , `a ≠ c` , `b ≠ c` |

`div_fir` | `(a * b) / b` | `a` | `NZR(b)` |

`div_fil` | `(a * b) / a` | `b` | `NZR(a)` |

`div_xilu` | `a` | `(a / b) [*] b` | `USR(a / b)` , `NZR(b)` |

`div_xiru` | `b` | `a [/] (a / b)` | `USR(a / b)` , `NZR(a)` , `NZR(b)` |

`sqrt_mibs` | `sqrt(a) - sqrt(b)` | `(a - b) [/] (sqrt(a) [+] sqrt(b))` | `BND(a)` , `BND(b)` , `a ≠ b` |

`sqrt_mibq` | `(sqrt(a) - sqrt(b)) / sqrt(b)` | `sqrt(1 [+] ((a - b) / b)) [-] 1` | `BND(a)` , `BND(b)` , `a ≠ b` |

`sqrt_xibu` | `a` | `sqrt(a) [*] sqrt(a)` | `USR(sqrt(a))` , `BND(a)` |

`sub_xals` | `c - a` | `(c - b) [+] (b - a)` | `a ≠ c` , `b ≠ c` |

`val_xabs` | `b` | `a [+] (b - a)` | |

`val_xebs` | `a` | `b [-] (b - a)` | |

`val_xabq` | `b` | `a [*] (1 [+] ((b - a) / a))` | `NZR(a)` |

`val_xebq` | `a` | `b [/] (1 [+] ((b - a) / a))` | `NZR(a)` , `NZR(b)` |

`square_sqrt` | `sqrt(a) * sqrt(a)` | `a` | `BND(a)` |

`addf_1` | `a / (a + b)` | `1 [/] (1 [+] (b / a))` | `NZR(a)` , `NZR(a + b)` |

`addf_2` | `a / (a + b)` | `1 [-] (b / (a + b))` | `NZR(a + b)` |

`addf_3` | `a / (a - b)` | `1 [/] (1 [-] (b / a))` | `NZR(a)` , `NZR(a - b)` , `a ≠ b` |

`addf_4` | `a / (a - b)` | `1 [+] (b / (a - b))` | `NZR(a - b)` , `a ≠ b` |

`addf_5` | `b / (a + b)` | `1 [/] ((a / b) [+] 1)` | `NZR(b)` , `NZR(a + b)` , `a ≠ b` |

`addf_6` | `b / (a + b)` | `1 [-] (a / (a + b))` | `NZR(a + b)` , `a ≠ b` |

`addf_7` | `b / (a - b)` | `1 [/] ((a / b) [-] 1)` | `NZR(b)` , `NZR(a - b)` , `a ≠ b` |

`addf_8` | `b / (a - b)` | `((a / (a - b)) [-] 1)` | `NZR(a - b)` , `a ≠ b` |

There are also some rewriting rules dealing with `REL`

predicates.

Theorem name | Target | Source | Constraints |
---|---|---|---|

`opp_fibq` | `REL(-a, -b)` | `REL(a, b)` | |

`mul_filq` | `REL(a * b, a * c)` | `REL(b, c)` | `b ≠ c` |

`mul_firq` | `REL(a * b, c * b)` | `REL(a, c)` | `a ≠ c` |

`div_firq` | `REL(a / b, c / b)` | `REL(a, c)` | `a ≠ c` |

Finally, there are theorems performing basic congruence.

Theorem name | Target | Source | Constraints |
---|---|---|---|

`opp_fibe` | `EQL(-a, -b)` | `EQL(a, b)` | `a ≠ b` |

`add_file` | `EQL(a + b, a + c)` | `EQL(b, c)` | `b ≠ c` |

`add_fire` | `EQL(a + b, c + b)` | `EQL(a, c)` | `a ≠ c` |

`sub_file` | `EQL(a - b, a - c)` | `EQL(b, c)` | `b ≠ c` |

`sub_fire` | `EQL(a - b, c - b)` | `EQL(a, c)` | `a ≠ c` |

`mul_file` | `EQL(a * b, a * c)` | `EQL(b, c)` | `b ≠ c` |

`mul_fire` | `EQL(a * b, c * b)` | `EQL(a, c)` | `a ≠ c` |

`div_file` | `EQL(a / b, a / c)` | `EQL(b, c)` | `b ≠ c` |

`div_fire` | `EQL(a / b, c / b)` | `EQL(a, c)` | `a ≠ c` |