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 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 nameGoalHypothesesConstraints
sub_of_eqlBND(a - b)EQL(a, b)a ≠ b, (a - b)~
eql_of_cstEQL(a, b)BND(a), BND(b)a=, b=
rel_reflREL(a, a)
eql_transEQL(b, c)EQL(b, a), EQL(a, c)a ≠ c
eql_transEQL(c, a)EQL(c, b), EQL(b, a)b ≠ c
negBND(-a)BND(a)
sqrtBND(sqrt(a))BND(a)
sub_reflBND(a - a)
div_reflBND(a / a)NZR(a)
squareBND(a * a)ABS(a)
neg_aABS(-a)ABS(a)
abs_aABS(|a|)ABS(a)
addBND(a + b)BND(a), BND(b)
subBND(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_aaABS(a * b)ABS(a), ABS(b)
div_aaABS(a / b)ABS(a), ABS(b)
bnd_of_absBND(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_absBND(|a|)ABS(a)
abs_of_uabsABS(a)BND(|a|)a ≠ |?|, a~
constant{1,2,10}BND(a) a number
abs_fixFIX(|a|)FIX(a)a~
abs_fltFLT(|a|)FLT(a)a~
neg_fixFIX(-a)FIX(a)a~
neg_fltFLT(-a)FLT(a)a~
add_fixFIX(a + b)FIX(a), FIX(b)a~ or b~
sub_fixFIX(a - b)FIX(a), FIX(b)a~ or b~
sub_fltFLT(a - b)FLT(a), FLT(b), REL(a,b)a~ or b~
sub_flt_revFLT(b - a)FLT(a), FLT(b), REL(a,b)a~ or b~
mul_fixFIX(a * b)FIX(a), FIX(b)a~ or b~
mul_fltFLT(a * b)FLT(a), FLT(b)a~ or b~
fix_of_flt_bndFIX(a)FLT(a), ABS(a)a~, a ≠ -?, a ≠ |?|
flt_of_fix_bndFLT(a)FIX(a), ABS(a)a~, a ≠ -?, a ≠ |?|
fix_of_singleton_bndFIX(a)ABS(a)
flt_of_singleton_bndFLT(a)ABS(a)
bnd_of_nzr_relBND((b - a) / a)NZR(a), REL(b,a)a ≠ b
rel_of_nzr_bndREL(a, b)NZR(b), BND((a - b) / b)a ≠ b
add_rrREL(a + b, c + d)REL(a, c), REL(b, d), BND(c / (c + d)), NZR(c + d)
sub_rrREL(a - b, c - d)REL(a, c), REL(b, d), BND(c / (c - d)), NZR(c - d)
mul_rrREL(a * b, c * d)REL(a, c), REL(b, d)a ≠ c, b ≠ d
div_rrREL(a / b, c / d)REL(a, c), REL(b, d), NZR(d)a ≠ c, b ≠ d
composeREL(b, c)REL(b, a), REL(a, c)a ≠ c
composeREL(c, a)REL(c, b), REL(b, a)b ≠ c
compose_swapREL(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_absNZR(a)ABS(a)
nzr_of_nzr_relNZR(b)NZR(a), REL(b, a)
nzr_of_nzr_rel_revNZR(a)NZR(b), REL(b, a)
bnd_div_of_rel_bnd_divBND((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.

GoalHypothesisRounding 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 nameGoalHypotheses
bnd_rewriteBND(a)EQL(a, b), BND(b)
abs_rewriteABS(a)EQL(a, b), ABS(b)
fix_rewriteFIX(a)EQL(a, b), FIX(b)
flt_rewriteFLT(a)EQL(a, b), FLT(b)
nzr_rewriteNZR(a)EQL(a, b), NZR(b)
rel_rewrite_1REL(a, c)EQL(a, b), REL(b, c)
rel_rewrite_2REL(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 nameTargetSourceConstraints
opp_mibs-a - -b[-] (a - b)a ≠ b
add_xalsb + c(b - a) [+] (a + c)
add_xarsc + 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 - cb ≠ c
add_firs(a + b) - (c + b)a - ca ≠ 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_xilua(a + b) [-] bUSR(a + b)
add_xirub(a + b) [-] aUSR(a + b)
sub_xalsb - c(b - a) [+] (a - c)a ≠ c, b ≠ c
sub_xarsc - 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 - ca ≠ 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_xabsba [+] (b - a)USR(b - a)
val_xebsab [-] (b - a)USR(b - a)
mul_xalsb * c((b - a) [*] c) [+] (a * c)
mul_xarsc * b(c [*] (b - a)) [+] (c * a)
mul_filsa * b - a * ca [*] (b - c)b ≠ c
mul_firsa * b - c * b(a - c) [*] ba ≠ c
mul_marsa * b - c * d(a [*] (b - d)) [+] ((a - c) [*] d)a ≠ c, b ≠ d
mul_malsa * b - c * d((a - c) [*] b) [+] (c [*] (b - d))a ≠ c, b ≠ d
mul_mabsa * b - c * d(a [*] (b - d)) [+] ((a - c) [*] b) [-] ((a - c) [*] (b - d))a ≠ c, b ≠ d
mul_mibsa * b - c * d(c [*] (b - d)) [+] ((a - c) [*] d) [+] ((a - c) [*] (b - d))a ≠ c, b ≠ d
mul_xilua(a * b) [/] bUSR(a * b), NZR(b)
mul_xirub(a * b) [/] aUSR(a * b), NZR(a)
div_xalsb / c((b - a) / c) [+] (a / c)NZR(c), a ≠ c, b ≠ c
div_fir(a * b) / baNZR(b)
div_fil(a * b) / abNZR(a)
div_xilua(a / b) [*] bUSR(a / b), NZR(b)
div_xiruba [/] (a / b)USR(a / b), NZR(a), NZR(b)
sqrt_mibssqrt(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)) [-] 1BND(a), BND(b), a ≠ b
sqrt_xibuasqrt(a) [*] sqrt(a)USR(sqrt(a)), BND(a)
sub_xalsc - a(c - b) [+] (b - a)a ≠ c, b ≠ c
val_xabsba [+] (b - a)
val_xebsab [-] (b - a)
val_xabqba [*] (1 [+] ((b - a) / a))NZR(a)
val_xebqab [/] (1 [+] ((b - a) / a))NZR(a), NZR(b)
square_sqrtsqrt(a) * sqrt(a)aBND(a)
addf_1a / (a + b)1 [/] (1 [+] (b / a))NZR(a), NZR(a + b)
addf_2a / (a + b)1 [-] (b / (a + b))NZR(a + b)
addf_3a / (a - b)1 [/] (1 [-] (b / a))NZR(a), NZR(a - b), a ≠ b
addf_4a / (a - b)1 [+] (b / (a - b))NZR(a - b), a ≠ b
addf_5b / (a + b)1 [/] ((a / b) [+] 1)NZR(b), NZR(a + b), a ≠ b
addf_6b / (a + b)1 [-] (a / (a + b))NZR(a + b), a ≠ b
addf_7b / (a - b)1 [/] ((a / b) [-] 1)NZR(b), NZR(a - b), a ≠ b
addf_8b / (a - b)((a / (a - b)) [-] 1)NZR(a - b), a ≠ b

There are also some rewriting rules dealing with REL predicates.

Theorem nameTargetSourceConstraints
opp_fibqREL(-a, -b)REL(a, b)
mul_filqREL(a * b, a * c)REL(b, c)b ≠ c
mul_firqREL(a * b, c * b)REL(a, c)a ≠ c
div_firqREL(a / b, c / b)REL(a, c)a ≠ c

Finally, there are theorems performing basic congruence.

Theorem nameTargetSourceConstraints
opp_fibeEQL(-a, -b)EQL(a, b)a ≠ b
add_fileEQL(a + b, a + c)EQL(b, c)b ≠ c
add_fireEQL(a + b, c + b)EQL(a, c)a ≠ c
sub_fileEQL(a - b, a - c)EQL(b, c)b ≠ c
sub_fireEQL(a - b, c - b)EQL(a, c)a ≠ c
mul_fileEQL(a * b, a * c)EQL(b, c)b ≠ c
mul_fireEQL(a * b, c * b)EQL(a, c)a ≠ c
div_fileEQL(a / b, a / c)EQL(b, c)b ≠ c
div_fireEQL(a / b, c / b)EQL(a, c)a ≠ c