# 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\).

`LIN(x,y,I)`

  The values of expressions `x` and `y` satisfy \(x = y \times \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` in the hypotheses but only one of them appears on in the goal, 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~`
`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`
`bnd_of_rel` | `BND((b - a) / a)` | `REL(b, a)` | `a ≠ b`
`rel_of_nzr_bnd` | `REL(a, b)` | `NZR(b)`, `BND((a - b) / b)` | `a ≠ b`
`add_rr_left` | `REL(a + b, c + d)` | `REL(a, c)`, `REL(b, d)`, `LIN(c, c + d)` |
`add_rr_right` | `REL(a + b, c + d)` | `REL(a, c)`, `REL(b, d)`, `LIN(d, c + d)` |
`sub_rr_left` | `REL(a - b, c - d)` | `REL(a, c)`, `REL(b, d)`, `LIN(c, c - d)` |
`sub_rr_right` | `REL(a - b, c - d)` | `REL(a, c)`, `REL(b, d)`, `LIN(d, 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)` | `a ≠ c`, `b ≠ d`
`inv_r` | `REL(a / b, a / c)` | `REL(b, c)` | `b ≠ c`
`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`
`bnd_of_bnd_rel_{nop}` | `BND(b)` | `REL(b, a)`, `BND(a)` | `a ≠ b`, `b~`
`bnd_of_rel_bnd_{nop}` | `BND(a)` | `BND(b)`, `REL(b, a)` | `a ≠ b`, `a~`
`neg_nzr` | `NZR(-a)` | `NZR(a)` |
`mul_nzr` | `NZR(a * b)` | `NZR(a)`, `NZR(b)` |
`div_nzr` | `NZR(a / b)` | `NZR(a)`, `NZR(b)` |
`div_nzr_rev_l` | `NZR(a)` | `NZR(a / b)` | `USR(a / b)`
`div_nzr_rev_r` | `NZR(b)` | `NZR(a / b)` | `USR(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)` |
`lin_of_rel` | `LIN(a, b)` | `REL(a, b)` |
`lin_of_rel2` | `LIN(b - a, a)` | `REL(b, a)` |
`add_flt_lin` | `FLT(a + b)` | `FLT(a)`, `FLT(b)`, `LIN(a, b)` |
`add_flt_lin_rev` | `FLT(a + b)` | `FLT(a)`, `FLT(b)`, `LIN(b, a)` |
`sub_flt_lin` | `FLT(a - b)` | `FLT(a)`, `FLT(b)`, `LIN(a, b)` |
`sub_flt_lin_rev` | `FLT(a - b)` | `FLT(a)`, `FLT(b)`, `LIN(b, a)` |
`lin_of_bnd_div` | `LIN(a, b)` | `NZR(b)`, `BND(a / b)` |
`bnd_div_of_lin` | `BND(a / b)` | `NZR(b)`, `LIN(a, b)` | `a ≠ b`
`bnd_of_lin` | `BND(a / b)` | `LIN(a, b)` | `a ≠ b`
`add_ll` | `LIN(a + b, c)` | `LIN(a, c)`, `LIN(b, c)` |
`sub_ll` | `LIN(a - b, c)` | `LIN(a, c)`, `LIN(b, c)` | `a ≠ b`
`minus_lin` | `LIN(-a, b)` | `LIN(a, b)` |
`mul_ll_{nop}{nop}` | `LIN(a * b, c * d)` | `LIN(a, c)`, `LIN(b, d)` | `a ≠ c`, `a ≠ d`, `b ≠ c`, `b ≠ d`
`lin_of_lin_rel_{nop}{nop}` | `LIN(b - a, c)` | `LIN(a, c)`, `REL(b, a)` | `a ≠ c`
`bnd_of_bnd_fix` | `BND(a)` | `BND(a)`, `FIX(a)` |

### 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
`REL(rnd(a), a)` | `FIX(a)` | float
`FIX(rnd(a))` |  | fixed, float
`FIX(rnd(a))` | `FIX(a)` | fixed, float
`FLT(rnd(a))` |  | float
`FLT(rnd(a))` | `FLT(a)` | fixed, float
`EQL(rnd(a), a)` | `FIX(a)` | fixed
`EQL(rnd(a), a)` | `FIX(a)`, `FLT(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)`
`lin_rewrite_1` | `LIN(a, c)` | `EQL(a, b)`, `LIN(b, c)`
`lin_rewrite_2` | `LIN(c, a)` | `EQL(a, b)`, `LIN(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_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`
`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_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)`
`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_9` | `a / (a + b)` | `1 [-] (1 [/] (1 [+] (a / b)))` | `NZR(b)`, `NZR(a + b)`
`addf_10` | `b / (a + b)` | `1 [-] (1 [/] (1 [+] (b / a)))` | `NZR(a)`, `NZR(a + b)`
`addf_11` | `a / (a - b)` | `1 [-] (1 [/] (1 [-] (a / b)))` | `NZR(b)`, `NZR(a - b)`
`addf_12` | `b / (a - b)` | `(1 [/] (1 [-] (b / a))) [-] 1` | `NZR(a)`, `NZR(a - b)`

There are also some rewriting rules dealing with predicates `REL` and `LIN`.

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`
`opp_fibm` | `LIN(-a, -b)` | `LIN(a, b)` |
`mul_film` | `LIN(a * b, a * c)` | `LIN(b, c)` | `b ≠ c`
`mul_firm` | `LIN(a * b, c * b)` | `LIN(a, c)` | `a ≠ c`
`mul_fism` | `LIN(a * b, c * a)` | `LIN(b, c)` |
`mul_fitm` | `LIN(a * b, b * c)` | `LIN(a, c)` |
`div_firq` | `LIN(a / b, c / b)` | `LIN(a, c)` | `a ≠ c`
`val_xabm` | `LIN(b, c)` | `LIN((b - a) [+] a, c)` | `a ≠ c`, `b ≠ c`
`add_mibm` | `LIN((a + b) - (c + d), e)` | `LIN((a - c) [+] (b - d), e)` | `a ≠ c`, `b ≠ d`
`add_film` | `LIN((a + b) - (a + c), d)` | `LIN(b - c, d)` | `b ≠ c`
`add_firm` | `LIN((a + b) - (c + b), d)` | `LIN(a - c, d)` | `a ≠ c`
`sub_mibm` | `LIN((a - b) - (c - d), e)` | `LIN((a - c) [-] (b - d), e)` | `a ≠ c`, `b ≠ d`
`sub_film` | `LIN((a - b) - (a - c), d)` | `LIN([-] (b - c), d)` | `b ≠ c`
`sub_firm` | `LIN((a - b) - (c - b), d)` | `LIN(a - c, d)` | `a ≠ c`
`sub_xalm` | `LIN(b - c, d)` | `LIN((b - a) [+] (a - c), d)` | `a ≠ c`, `b ≠ 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`