The main datatype for FM elimination. Variables are represented by natural numbers, each of which has an integer coefficient. Index 0 is reserved for constants, i.e. coeffs.find 0 is the coefficient of 1. The represented term is coeffs.keys.sum (λ i, coeffs.find i * Var[i]). str determines the direction of the comparison -- is it < 0, ≤ 0, or = 0?

If c1 and c2 both contain variable a with opposite coefficients, produces v1, v2, and c such that a has been cancelled in c := v1c1 + v2c2

The state for the elimination monad. vars: the set of variables present in comps comps: a set of comparisons inputs: a set of pairs of exprs (t, pf), where t is a term and pf is a proof that t {<, ≤, =} 0, indexed by ℕ. has_false: stores a pcomp of 0 < 0 if one has been found TODO: is it more efficient to store comps as a list, to avoid comparisons?

Turns an expression into a map from ℕ to ℤ, for use in a comp object. The expr_map ℕ argument identifies which expressions have already been assigned numbers. Returns a new map.

Takes a list of proofs of props of the form t {<, ≤, =} 0, and creates a linarith_structure.

Takes a list of coefficients [c] and list of expressions, of equal length. Each expression is a proof of a prop of the form t {<, ≤, =} 0. Produces a proof that the sum of (c*t) {<, ≤, =} 0, where the comp is as strong as possible.

Assumes e is a proof that t = 0. Creates a proof that -t = 0.

Takes a list of proofs of propositions of the form t {<, ≤, =} 0, and tries to prove the goal false.

e is a term with rational division. produces a natural number n and a proof that n*e = e', where e' has no division.

Takes a list of proofs of propositions. Filters out the proofs of linear (in)equalities, and tries to use them to prove false. If pref_type is given, starts by working over this type

linarith.interactive_aux cfg o_goal restrict_hyps args:

• cfg is a linarith_config object
• o_goal : option expr is the local constant corresponding to the former goal, if there was one
• restrict_hyps : bool is tt if linarith only [...] was used
• args : option (list pexpr) is the optional list of arguments in linarith [...]

Tries to prove a goal of false by linear arithmetic on hypotheses. If the goal is a linear (in)equality, tries to prove it by contradiction. If the goal is not false or an inequality, applies exfalso and tries linarith on the hypotheses. linarith will use all relevant hypotheses in the local context. linarith [t1, t2, t3] will add proof terms t1, t2, t3 to the local context. linarith only [h1, h2, h3, t1, t2, t3] will use only the goal (if relevant), local hypotheses h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context. linarith! will use a stronger reducibility setting to identify atoms.

Config options: linarith {exfalso := ff} will fail on a goal that is neither an inequality nor false linarith {restrict_type := T} will run only on hypotheses that are inequalities over T linarith {discharger := tac} will use tac instead of ring for normalization. Options: ring2, ring SOP, simp