Given a comp_source cs, cs.flatten maps an assumption index to the number of copies of that assumption that appear in the history of cs.

For example, suppose cs is produced by scaling assumption 2 by 5, and adding to that the sum of assumptions 1 and 2. cs.flatten maps 1 ↦ 1, 2 ↦ 6.

Any comparison whose history is not minimal is redundant, and need not be included in the new set of comparisons. elimed_ge : ℕ is a natural number such that all variables with index ≥ elimed_ge have been removed from the system.

This test is an overapproximation to minimality. It gives necessary but not sufficient conditions. If the history of c is minimal, then c.maybe_minimal is true, but c.maybe_minimal may also be true for some c with minimal history. Thus, if c.maybe_minimal is false, c is known not to be minimal and must be redundant. See https://doi.org/10.1016/B978-0-444-88771-9.50019-2 (Theorem 13). The condition described there considers only implicitly eliminated variables that have been officially eliminated from the system. This is not the case for every implicitly eliminated variable. Consider eliminating z from {x + y + z < 0, x - y - z < 0}. The result is the set {2*x < 0}; y is implicitly but not officially eliminated.

This implementation of Fourier-Motzkin elimination processes variables in decreasing order of indices. Immediately after a step that eliminates variable k, variable k' has been eliminated iff k' ≥ k. Thus we can compute the intersection of officially and implicitly eliminated variables by taking the set of implicitly eliminated variables with indices ≥ elimed_ge.

The comp_source field is ignored when comparing pcomps. Two pcomps proving the same comparison, with different sources, are considered equivalent.

pcomp.scale c n scales the coefficients of c by n and notes this in the comp_source.

pcomp.add c1 c2 elim_var creates the result of summing the linear comparisons c1 and c2, during the process of eliminating the variable elim_var. The computation assumes, but does not enforce, that elim_var appears in both c1 and c2 and does not appear in the sum. Computing the sum of the two comparisons is easy; the complicated details lie in tracking the additional fields of pcomp.

• The historical set pcomp.history of c1 + c2 is the union of the two historical sets.
• vars is the union of c1.vars and c2.vars.
• The effectively eliminated variables of c1 + c2 are the union of the two effective sets, with elim_var inserted.
• The implicitly eliminated variables of c1 + c2 are those that appear in vars but not c.vars or effective. (Note that the description of the implicitly eliminated variables of c1 + c2 in the algorithm described in Section 6 of https://doi.org/10.1016/B978-0-444-88771-9.50019-2 seems to be wrong: that says it should be (c1.implicit.union c2.implicit).sdiff explicit. Since the implicitly eliminated sets start off empty for the assumption, this formula would leave them always empty.)

pcomp.assump c n creates a pcomp whose comparison is c and whose source is comp_source.assump n, that is, c is derived from the nth hypothesis. The history is the singleton set {n}. No variables have been eliminated (effectively or implicitly).

Creates an empty set of pcomps, sorted using pcomp.cmp. This should always be used instead of mk_rb_map for performance reasons.

If c1 and c2 both contain variable a with opposite coefficients, produces v1 and v2 such that a has been cancelled in v1*c1 + v2*c2.

pelim_var p1 p2 calls elim_var on the comp components of p1 and p2. If this returns v1 and v2, it creates a new pcomp equal to v1*p1 + v2*p2, and tracks this in the comp_source.

A pcomp represents a contradiction if its comp field represents a contradiction.

elim_var_with_set a p comps collects the result of calling pelim_var p p' a for every p' ∈ comps.

The linarith monad extends an exceptional monad with a linarith_structure state. An exception produces a contradictory pcomp.

Returns the current max variable.

Return the current comparison set.

Throws an exception if a contradictory pcomp is contained in the current state.

Updates the current state with a new max variable and comparisons, and calls validate to check for a contradiction.

split_set_by_var_sign a comps partitions the set comps into three parts.

• pos contains the elements of comps in which a has a positive coefficient.
• neg contains the elements of comps in which a has a negative coefficient.
• not_present contains the elements of comps in which a has coefficient 0.

Returns (pos, neg, not_present).

monad.elim_var a performs one round of Fourier-Motzkin elimination, eliminating the variable a from the linarith state.

elim_all_vars eliminates all variables from the linarith state, leaving it with a set of ground comparisons. If this succeeds without exception, the original linarith state is consistent.

mk_linarith_structure hyps vars takes a list of hypotheses and the largest variable present in those hypotheses. It produces an initial state for the elimination monad.

produce_certificate hyps vars tries to derive a contradiction from the comparisons in hyps by eliminating all variables ≤ max_var. If successful, it returns a map coeff : ℕ → ℕ as a certificate. This map represents that we can find a contradiction by taking the sum ∑ (coeff i) * hyps[i].