# Parsing input expressions into linear form #

`linarith`

computes the linear form of its input expressions,
assuming (without justification) that the type of these expressions
is a commutative semiring.
It identifies atoms up to ring-equivalence: that is, `(y*3)*x`

will be identified `3*(x*y)`

,
where the monomial `x*y`

is the linear atom.

- Variables are represented by natural numbers.
- Monomials are represented by
`Monom := RBMap ℕ ℕ`

. The monomial`1`

is represented by the empty map. - Linear combinations of monomials are represented by
`Sum := RBMap Monom ℤ`

.

All input expressions are converted to `Sum`

s, preserving the map from expressions to variables.
We then discard the monomial information, mapping each distinct monomial to a natural number.
The resulting `RBMap ℕ ℤ`

represents the ring-normalized linear form of the expression.
This is ultimately converted into a `Linexp`

in the obvious way.

`linearFormsAndMaxVar`

is the main entry point into this file. Everything else is contained.

`findDefeq red m e`

looks for a key in `m`

that is defeq to `e`

(up to transparency `red`

),
and returns the value associated with this key if it exists.
Otherwise, it fails.

## Instances For

We introduce a local instance allowing addition of `RBMap`

s,
removing any keys with value zero.
We don't need to prove anything about this addition, as it is only used in meta code.

## Instances For

A local abbreviation for `RBMap`

so we don't need to write `Ord.compare`

each time.

## Instances For

### Parsing datatypes #

Variables (represented by natural numbers) map to their power.

## Instances For

`1`

is represented by the empty monomial, the product of no variables.

## Instances For

Compare monomials by first comparing their keys and then their powers.

## Instances For

Linear combinations of monomials are represented by mapping monomials to coefficients.

## Instances For

`1`

is represented as the singleton sum of the monomial `Monom.one`

with coefficient 1.

## Instances For

`Sum.scaleByMonom s m`

multiplies every monomial in `s`

by `m`

.

## Instances For

`sum.mul s1 s2`

distributes the multiplication of two sums.

## Instances For

The `n`

th power of `s : Sum`

is the `n`

-fold product of `s`

, with `s.pow 0 = Sum.one`

.

## Equations

- Linarith.Sum.pow s 0 = Linarith.Sum.one
- Linarith.Sum.pow s (Nat.succ k) = Linarith.Sum.mul s (Linarith.Sum.pow s k)

## Instances For

`SumOfMonom m`

lifts `m`

to a sum with coefficient `1`

.

## Instances For

The unit monomial `one`

is represented by the empty RBMap.

## Instances For

A single variable `n`

is represented by a sum with coefficient `1`

and monomial `n`

.

## Instances For

### Parsing algorithms #

`ExprMap`

is used to record atomic expressions which have been seen while processing inequality
expressions.

## Instances For

`linearFormOfAtom red map e`

is the atomic case for `linear_form_of_expr`

.
If `e`

appears with index `k`

in `map`

, it returns the singleton sum `var k`

.
Otherwise it updates `map`

, adding `e`

with index `n`

, and returns the singleton sum `var n`

.

## Instances For

`linearFormOfExpr red map e`

computes the linear form of `e`

.

`map`

is a lookup map from atomic expressions to variable numbers.
If a new atomic expression is encountered, it is added to the map with a new number.
It matches atomic expressions up to reducibility given by `red`

.

Because it matches up to definitional equality, this function must be in the `MetaM`

monad,
and forces some functions that call it into `MetaM`

as well.

`elimMonom s map`

eliminates the monomial level of the `Sum`

`s`

.

`map`

is a lookup map from monomials to variable numbers.
The output `RBMap ℕ ℤ`

has the same structure as `s : Sum`

,
but each monomial key is replaced with its index according to `map`

.
If any new monomials are encountered, they are assigned variable numbers and `map`

is updated.

## Instances For

`toComp red e e_map monom_map`

converts an expression of the form `t < 0`

, `t ≤ 0`

, or `t = 0`

into a `comp`

object.

`e_map`

maps atomic expressions to indices; `monom_map`

maps monomials to indices.
Both of these are updated during processing and returned.

## Instances For

`toCompFold red e_map exprs monom_map`

folds `toComp`

over `exprs`

,
updating `e_map`

and `monom_map`

as it goes.

## Equations

- One or more equations did not get rendered due to their size.
- Linarith.toCompFold red x [] x = pure ([], x, x)

## Instances For

`linearFormsAndMaxVar red pfs`

is the main interface for computing the linear forms of a list
of expressions. Given a list `pfs`

of proofs of comparisons, it produces a list `c`

of `Comp`

s of
the same length, such that `c[i]`

represents the linear form of the type of `pfs[i]`

.

It also returns the largest variable index that appears in comparisons in `c`

.