Deriving a proof of false #

linarith uses an untrusted oracle to produce a certificate of unsatisfiability. It needs to do some proof reconstruction work to turn this into a proof term. This file implements the reconstruction.

Main declarations #

The public facing declaration in this file is prove_false_by_linarith.

Auxiliary functions for assembling proofs #

source

meta def linarith.mul_expr (n : ℕ) (e : expr) :

pexpr

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.

source

meta def linarith.add_exprs :

list pexpr → pexpr

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.

source

meta def linarith.ineq_const_nm :

linarith.ineq → linarith.ineq → name × linarith.ineq

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.

source

meta def linarith.mk_lt_zero_pf_aux (c : linarith.ineq) (pf npf : expr) (coeff : ℕ) :

tactic (linarith.ineq × expr)

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.

source

meta def linarith.mk_lt_zero_pf :

list (expr × ℕ) → tactic expr

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.

source

meta def linarith.term_of_ineq_prf (prf : expr) :

tactic expr

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

source

meta def linarith.ineq_prf_tp (prf : expr) :

tactic expr

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

source

meta def linarith.mk_neg_one_lt_zero_pf (tp : expr) :

tactic expr

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

source

meta def linarith.mk_neg_eq_zero_pf (e : expr) :

tactic expr

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

source

meta def linarith.prove_eq_zero_using (tac : tactic unit) (e : expr) :

tactic expr

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

source

meta def linarith.add_neg_eq_pfs :

list expr → tactic (list expr)

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.

The main method #

source

meta def linarith.prove_false_by_linarith (cfg : linarith.linarith_config) :

list expr → tactic expr

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.