# Linarith preprocessing #

This file contains methods used to preprocess inputs to `linarith`

.

In particular, `linarith`

works over comparisons of the form `t R 0`

, where `R ∈ {<,≤,=}`

.
It assumes that expressions in `t`

have integer coefficients and that the type of `t`

has
well-behaved subtraction.

## Implementation details #

A `GlobalPreprocessor`

is a function `List Expr → TacticM (List Expr)`

. Users can add custom
preprocessing steps by adding them to the `LinarithConfig`

object. `Linarith.defaultPreprocessors`

is the main list, and generally none of these should be skipped unless you know what you're doing.

### Preprocessing #

Processor that recursively replaces `P ∧ Q`

hypotheses with the pair `P`

and `Q`

.

## Equations

- Linarith.splitConjunctions = { name := "split conjunctions", transform := Linarith.splitConjunctions.aux }

## Instances For

Implementation of the `splitConjunctions`

preprocessor.

Removes any expressions that are not proofs of inequalities, equalities, or negations thereof.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Implementation of the `filterComparisons`

preprocessor.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

If `prf`

is a proof of `¬ e`

, where `e`

is a comparison,
`flipNegatedComparison prf e`

flips the comparison in `e`

and returns a proof.
For example, if `prf : ¬ a < b`

, `flipNegatedComparison prf q(a < b)`

returns a proof of `a ≥ b`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Replaces proofs of negations of comparisons with proofs of the reversed comparisons.
For example, a proof of `¬ a < b`

will become a proof of `a ≥ b`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`isNatProp tp`

is true iff `tp`

is an inequality or equality between natural numbers
or the negation thereof.

`getNatComparisons e`

returns a list of all subexpressions of `e`

of the form `((t : ℕ) : C)`

.

If `e : ℕ`

, returns a proof of `0 ≤ (e : C)`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Ordering on `Expr`

.

## Equations

- Linarith.Expr.Ord = { compare := fun (a b : Lean.Expr) => if a.lt b = true then Ordering.lt else if a.equal b = true then Ordering.eq else Ordering.gt }

## Instances For

If `h`

is an equality or inequality between natural numbers,
`natToInt`

lifts this inequality to the integers.
It also adds the facts that the integers involved are nonnegative.
To avoid adding the same nonnegativity facts many times, it is a global preprocessor.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

If `pf`

is a proof of a strict inequality `(a : ℤ) < b`

,
`mkNonstrictIntProof pf`

returns a proof of `a + 1 ≤ b`

,
and similarly if `pf`

proves a negated weak inequality.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`strengthenStrictInt h`

turns a proof `h`

of a strict integer inequality `t1 < t2`

into a proof of `t1 ≤ t2 + 1`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`rearrangeComparison e`

takes a proof `e`

of an equality, inequality, or negation thereof,
and turns it into a proof of a comparison `_ R 0`

, where `R ∈ {=, ≤, <}`

.

## Equations

- Linarith.rearrangeComparison e = do let __do_lift ← Lean.Meta.inferType e let __do_lift ← Lean.instantiateMVars __do_lift Linarith.rearrangeComparison.aux e __do_lift

## Instances For

Implementation of `rearrangeComparison`

, after type inference.

`compWithZero h`

takes a proof `h`

of an equality, inequality, or negation thereof,
and turns it into a proof of a comparison `_ R 0`

, where `R ∈ {=, ≤, <}`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`normalizeDenominatorsLHS h lhs`

assumes that `h`

is a proof of `lhs R 0`

.
It creates a proof of `lhs' R 0`

, where all numeric division in `lhs`

has been cancelled.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`cancelDenoms pf`

assumes `pf`

is a proof of `t R 0`

. If `t`

contains the division symbol `/`

,
it tries to scale `t`

to cancel out division by numerals.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`findSquares s e`

collects all terms of the form `a ^ 2`

and `a * a`

that appear in `e`

and adds them to the set `s`

.
A pair `(a, true)`

is added to `s`

when `a^2`

appears in `e`

,
and `(a, false)`

is added to `s`

when `a*a`

appears in `e`

.

`nlinarithExtras`

is the preprocessor corresponding to the `nlinarith`

tactic.

- For every term
`t`

such that`t^2`

or`t*t`

appears in the input, adds a proof of`t^2 ≥ 0`

or`t*t ≥ 0`

. - For every pair of comparisons
`t1 R1 0`

and`t2 R2 0`

, adds a proof of`t1*t2 R 0`

.

This preprocessor is typically run last, after all inputs have been canonized.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`removeNe_aux`

case splits on any proof `h : a ≠ b`

in the input,
turning it into `a < b ∨ a > b`

.
This produces `2^n`

branches when there are `n`

such hypotheses in the input.

`removeNe`

case splits on any proof `h : a ≠ b`

in the input, turning it into `a < b ∨ a > b`

,
by calling `linarith.removeNe_aux`

.
This produces `2^n`

branches when there are `n`

such hypotheses in the input.

## Equations

- Linarith.removeNe = { name := "removeNe", transform := Linarith.removeNe_aux }

## Instances For

The default list of preprocessors, in the order they should typically run.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`preprocess pps l`

takes a list `l`

of proofs of propositions.
It maps each preprocessor `pp ∈ pps`

over this list.
The preprocessors are run sequentially: each receives the output of the previous one.
Note that a preprocessor may produce multiple or no expressions from each input expression,
so the size of the list may change.

## Equations

- One or more equations did not get rendered due to their size.