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 Sums, 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.

def List.findDefeq {v : Type} (red : Lean.Meta.TransparencyMode) (m : List (Lean.Expr × v)) (e : Lean.Expr) : Lean.MetaM v

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.

def instAddRBMap {β : Type u_1} {α : Type u_2} {c : α → α → Ordering} [Add β] [Zero β] [DecidableEq β] : Add (Std.RBMap α β c)

We introduce a local instance allowing addition of RBMaps, 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

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

@[inline, reducible]

abbrev Linarith.Map (α : Type u_1) (β : Type u_2) [Ord α] : Type (max u_1 u_2)

A local abbreviation for RBMap so we don't need to write Ord.compare each time.

Equations

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

Parsing datatypes

@[reducible]

def Linarith.Monom : Type

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

Equations

• Linarith.Monom = Linarith.Map ℕ ℕ

def Linarith.Monom.one : Linarith.Monom

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

Equations

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

def Linarith.Monom.lt : Linarith.Monom → Linarith.Monom → Bool

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

Equations

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

instance Linarith.instOrdMonom : Ord Linarith.Monom

Equations

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

@[reducible]

def Linarith.Sum : Type

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

Equations

• Linarith.Sum = Linarith.Map Linarith.Monom ℤ

def Linarith.Sum.one : Linarith.Sum

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

def Linarith.Sum.scaleByMonom (s : Linarith.Sum) (m : Linarith.Monom) : Linarith.Sum

Sum.scaleByMonom s m multiplies every monomial in s by m.

Equations

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

def Linarith.Sum.mul (s1 : Linarith.Sum) (s2 : Linarith.Sum) : Linarith.Sum

sum.mul s1 s2 distributes the multiplication of two sums.

Equations

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

partial def Linarith.Sum.pow (s : Linarith.Sum) : ℕ → Linarith.Sum

The nth power of s : Sum is the n-fold product of s, with s.pow 0 = Sum.one.

def Linarith.SumOfMonom (m : Linarith.Monom) : Linarith.Sum

SumOfMonom m lifts m to a sum with coefficient 1.

Equations

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

def Linarith.one : Linarith.Monom

The unit monomial one is represented by the empty RBMap.

Equations

• Linarith.one = Std.RBMap.empty

def Linarith.scalar (z : ℤ) : Linarith.Sum

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

def Linarith.var (n : ℕ) : Linarith.Sum

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

@[inline, reducible]

abbrev Linarith.ExprMap : Type

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

Equations

• Linarith.ExprMap = List (Lean.Expr × ℕ)

def Linarith.linearFormOfAtom (red : Lean.Meta.TransparencyMode) (m : Linarith.ExprMap) (e : Lean.Expr) : Lean.MetaM (Linarith.ExprMap × Linarith.Sum)

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.

partial def Linarith.linearFormOfExpr (red : Lean.Meta.TransparencyMode) (m : Linarith.ExprMap) (e : Lean.Expr) : Lean.MetaM (Linarith.ExprMap × Linarith.Sum)

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.

def Linarith.elimMonom (s : Linarith.Sum) (m : Linarith.Map Linarith.Monom ℕ) : Linarith.Map Linarith.Monom ℕ × Linarith.Map ℕ ℤ

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.

def Linarith.toComp (red : Lean.Meta.TransparencyMode) (e : Lean.Expr) (e_map : Linarith.ExprMap) (monom_map : Linarith.Map Linarith.Monom ℕ) : Lean.MetaM (Linarith.Comp × Linarith.ExprMap × Linarith.Map Linarith.Monom ℕ)

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.

def Linarith.toCompFold (red : Lean.Meta.TransparencyMode) : Linarith.ExprMap → List Lean.Expr → Linarith.Map Linarith.Monom ℕ → Lean.MetaM (List Linarith.Comp × Linarith.ExprMap × Linarith.Map Linarith.Monom ℕ)

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)

def Linarith.linearFormsAndMaxVar (red : Lean.Meta.TransparencyMode) (pfs : List Lean.Expr) : Lean.MetaM (List Linarith.Comp × ℕ)

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