mul_expr n e creates a pexpr representing n*e. When elaborated, the coefficient will be a native numeral of the same type as e.

add_exprs l creates a pexpr representing the sum of the elements of l, associated left. If l is empty, it will be the pexpr 0. Otherwise, it does not include 0 in the sum.

If our goal is to add together two inequalities t1 R1 0 and t2 R2 0, ineq_const_nm R1 R2 produces the strength of the inequality in the sum R, along with the name of a lemma to apply in order to conclude t1 + t2 R 0.

mk_lt_zero_pf_aux c pf npf coeff assumes that pf is a proof of t1 R1 0 and npf is a proof of t2 R2 0. It uses mk_single_comp_zero_pf to prove t1 + coeff*t2 R 0, and returns R along with this proof.

mk_lt_zero_pf coeffs pfs takes a list of proofs of the form tᵢ Rᵢ 0, paired with coefficients cᵢ. It produces a proof that ∑cᵢ * tᵢ R 0, where R is as strong as possible.

If prf is a proof of t R s, term_of_ineq_prf prf returns t.

If prf is a proof of t R s, ineq_prf_tp prf returns the type of t.

mk_neg_one_lt_zero_pf tp returns a proof of -1 < 0, where the numerals are natively of type tp.

If e is a proof that t = 0, mk_neg_eq_zero_pf e returns a proof that -t = 0.

prove_eq_zero_using tac e tries to use tac to construct a proof of e = 0.

add_neg_eq_pfs l inspects the list of proofs l for proofs of the form t = 0. For each such proof, it adds a proof of -t = 0 to the list.

prove_false_by_linarith is the main workhorse of linarith. Given a list l of proofs of tᵢ Rᵢ 0, it tries to derive a contradiction from l and use this to produce a proof of false.

An oracle is used to search for a certificate of unsatisfiability. In the current implementation, this is the Fourier Motzkin elimination routine in elimination.lean, but other oracles could easily be swapped in.

The returned certificate is a map m from hypothesis indices to natural number coefficients. If our set of hypotheses has the form {tᵢ Rᵢ 0}, then the elimination process should have guaranteed that 1.\ ∑ (m i)*tᵢ = 0, with at least one i such that m i > 0 and Rᵢ is <.

We have also that 2.\ ∑ (m i)*tᵢ < 0, since for each i, (m i)*tᵢ ≤ 0 and at least one is strictly negative. So we conclude a contradiction 0 < 0.

It remains to produce proofs of (1) and (2). (1) is verified by calling the discharger tactic of the linarith_config object, which is typically ring. We prove (2) by folding over the set of hypotheses.