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

## Equations

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

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.

## Equations

- instAddRBMap = { add := fun f g => Std.RBMap.filter (Std.RBMap.mergeWith (fun x b b' => b + b') f g) fun x b => decide (b ≠ 0) }

A local abbreviation for `RBMap`

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

each time.

## Equations

- Linarith.Map α β = Std.RBMap α β compare

### Parsing datatypes #

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

## Equations

`1`

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

## Equations

- Linarith.Monom.one = Std.RBMap.empty

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

## Equations

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

## Equations

- Linarith.instOrdMonom = { compare := fun x y => if Linarith.Monom.lt x y = true then Ordering.lt else if (x == y) = true then Ordering.eq else Ordering.gt }

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

## Equations

`1`

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

with coefficient 1.

## Equations

- Linarith.Sum.one = Std.RBMap.insert Std.RBMap.empty Linarith.Monom.one 1

`Sum.scaleByMonom s m`

multiplies every monomial in `s`

by `m`

.

## Equations

- Linarith.Sum.scaleByMonom s m = Std.RBMap.foldr (fun m' coeff sm => Std.RBMap.insert sm (m + m') coeff) Std.RBMap.empty s

`sum.mul s1 s2`

distributes the multiplication of two sums.`

## Equations

- Linarith.Sum.mul s1 s2 = Std.RBMap.foldr (fun mn coeff sm => sm + Std.RBMap.mapVal (fun x v => v * coeff) (Linarith.Sum.scaleByMonom s2 mn)) Std.RBMap.empty s1

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)

`SumOfMonom m`

lifts `m`

to a sum with coefficient `1`

.

## Equations

- Linarith.SumOfMonom m = Std.RBMap.insert Std.RBMap.empty m 1

The unit monomial `one`

is represented by the empty RBMap.

## Equations

- Linarith.one = Std.RBMap.empty

A scalar `z`

is represented by a `sum`

with coefficient `z`

and monomial `one`

## Equations

- Linarith.scalar z = Std.RBMap.insert Std.RBMap.empty Linarith.one z

A single variable `n`

is represented by a sum with coefficient `1`

and monomial `n`

.

## Equations

- Linarith.var n = Std.RBMap.insert Std.RBMap.empty (Std.RBMap.insert Std.RBMap.empty n 1) 1

### Parsing algorithms #

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

.

## Equations

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

`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.

## Equations

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

`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.

## Equations

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

`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)

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

.

## Equations

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