Theorems of Gappa¶
Predicates¶
Gappa works on sets of facts about realvalued expressions. The following predicates are handled internally:
BND(x,I)
 The value of expression
x
is included in intervalI
. ABS(x,I)
 The absolute value of expression
x
is included in intervalI
. REL(x,y,I)
 The values of expressions
x
andy
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
andy
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 righthand 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.
Theorems about real arithmetic¶
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) 
Theorems about rounding operators¶
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 