# Theorems of Gappa¶

## Predicates¶

Gappa works on sets of facts about real-valued expressions. The following predicates are handled internally:

BND(x,I)
The value of expression x is included in interval I.
ABS(x,I)
The absolute value of expression x is included in interval I.
REL(x,y,I)
The values of expressions x and y satisfy $$x = y \times (1 + \varepsilon)$$ with $$\varepsilon\in I$$.
FIX(x,k)
The value of expression x is such that $$\exists m \in \mathbb{Z},~x = m \cdot 2^k$$.
FLT(x,k)
The value of expression x is such that $$\exists m,e \in \mathbb{Z},~x = m \cdot 2^e \land |m| < 2^k$$.
NZR(x)
The value of expression x is not zero.
EQL(x,y)
Expressions x and y have equal values.

In the definitions above, I denotes an interval whose bounds have known numerical values, while k is a known integer. In the description of the theorems, these parameters will usually be ignored. For instance, BND(x) just means that an enclosure of x is known. In addition, EQL properties are also used to express rewriting hints provided by the user.

## Theorems¶

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 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~). A constraint written using USR means that the theorem will be applied only if a matching expression appears in the input file.

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)
square_rev ABS(a) BND(a * a) USR(a * 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~, USR(|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, 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

### Rewriting rules¶

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.

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_firs a / b - c / b (a - c) [/] b NZR(b), a ≠ c
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