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 proveFalseByLinarith.
Typesafe conversion of n : ℕ to Q($α).
Equations
- One or more equations did not get rendered due to their size.
Analogue of inferTypeQ, but that gets universe levels right for our application.
Equations
- One or more equations did not get rendered due to their size.
Auxiliary functions for assembling proofs #
A typesafe version of mulExpr.
Equations
- One or more equations did not get rendered due to their size.
mulExpr n e creates an Expr representing n*e.
When elaborated, the coefficient will be a native numeral of the same type as e.
Equations
- One or more equations did not get rendered due to their size.
A type-safe analogue of addExprs.
Equations
- One or more equations did not get rendered due to their size.
Inner loop for addExprs'.
Equations
- One or more equations did not get rendered due to their size.
- Linarith.addExprs'.go _inst p [] = p
addExprs L creates an Expr representing the sum of the elements of L, associated left.
Equations
- One or more equations did not get rendered due to their size.
If our goal is to add together two inequalities t1 R1 0 and t2 R2 0,
addIneq 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.
Equations
- One or more equations did not get rendered due to their size.
mkLTZeroProof 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∑cᵢ * tᵢ R 0, where R is as strong as possible.
Equations
- One or more equations did not get rendered due to their size.
step 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 mkSingleCompZeroOf to prove t1 + coeff*t2 R 0, and returns R
along with this proof.
Equations
- One or more equations did not get rendered due to their size.
If prf is a proof of t R s, leftOfIneqProof prf returns t.
Equations
- Linarith.leftOfIneqProof prf = do let __do_lift ← Lean.Meta.inferType prf let __discr ← Linarith.getRelSides __do_lift match __discr with | (t, snd) => pure t
If prf is a proof of t R s, typeOfIneqProof prf returns the type of t.
Equations
- Linarith.typeOfIneqProof prf = do let __do_lift ← Linarith.leftOfIneqProof prf Lean.Meta.inferType __do_lift
mkNegOneLtZeroProof tp returns a proof of -1 < 0,
where the numerals are natively of type tp.
Equations
- Linarith.mkNegOneLtZeroProof tp = do let zero_lt_one ← Lean.Meta.mkAppOptM `zero_lt_one #[some tp, none, none, none, none, none] Lean.Meta.mkAppM `neg_neg_of_pos #[zero_lt_one]
addNegEqProofs 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.
Equations
- One or more equations did not get rendered due to their size.
- Linarith.addNegEqProofs [] = pure []
proveEqZeroUsing tac e tries to use tac to construct a proof of e = 0.
Equations
- One or more equations did not get rendered due to their size.
The main method #
proveFalseByLinarith 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∑ (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∑ (m i)*tᵢ < 0,
since for each i, (m i)*tᵢ ≤ 0≤ 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 LinarithConfig object, which is typically ring. We prove (2) by folding over the
set of hypotheses.
Equations
- One or more equations did not get rendered due to their size.