# 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)→ 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∧ Q`

hypotheses with the pair `P`

and `Q`

.

## Equations

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

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.

Implementation of the `filterComparisons`

preprocessor.

## Equations

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

If `prf`

is a proof of `¬ e¬ e`

, where `e`

is a comparison,
`flipNegatedComparison prf e`

flips the comparison in `e`

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

, `flipNegatedComparison prf q(a < b)`

returns a proof of `a ≥ b≥ b`

.

## Equations

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

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

will become a proof of `a ≥ b≥ b`

.

## Equations

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

`isNatProp tp`

is true iff `tp`

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

If `e`

is of the form `((n : ℕ) : ℤ)`

, `isNatIntCoe e`

returns `n : ℕ`

.

## Equations

- Linarith.isNatIntCoe e = match Lean.Expr.getAppFnArgs e with | (`Nat.cast, #[Lean.Expr.const `Int [], head, n]) => some n | x => none

If `e : ℕ`

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

.

## Equations

- Linarith.mk_coe_nat_nonneg_prf e = Lean.Meta.mkAppM `Int.coe_nat_nonneg #[e]

Ordering on `Expr`

.

## Equations

- Linarith.Expr.compare a b = if Lean.Expr.lt a b = true then Ordering.lt else if Lean.Expr.equal a b = true then Ordering.eq else Ordering.gt

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.

`isStrictIntComparison tp`

is true iff `tp`

is a strict inequality between integers
or the negation of a weak inequality between integers.

## Equations

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

If `pf`

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

,
`mkNonstrictIntProof pf`

returns a proof of `a + 1 ≤ b≤ b`

,
and similarly if `pf`

proves a negated weak inequality.

## Equations

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

`strengthenStrictInt h`

turns a proof `h`

of a strict integer inequality `t1 < t2`

into a proof of `t1 ≤ t2 + 1≤ t2 + 1`

.

## Equations

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

`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

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

- Linarith.compWithZero = { name := "make comparisons with zero", transform := fun e => do let __do_lift ← Linarith.rearrangeComparison e pure [__do_lift] }

`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≥ 0`

or`t*t ≥ 0≥ 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.

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.

`preprocess pps l`

takes a list `l`

of proofs of propositions.
It maps each preprocessor `pp ∈ pps∈ 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.