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.

def Qq.ofNatQ {u : Lean.Level} (α : have u := u; Q(Type u)) : Q(Semiring «$α») → (n : ℕ) → Q(«$α»)

Typesafe conversion of n : ℕ to Q($α).

Auxiliary functions for assembling proofs

def Mathlib.Tactic.Linarith.mulExpr' {u : Lean.Level} (n : ℕ) {α : have u := u; Q(Type u)} (inst : Q(Semiring «$α»)) (e : Q(«$α»)) : Q(«$α»)

A typesafe version of mulExpr.

Equations

• Mathlib.Tactic.Linarith.mulExpr' n inst e = if n = 1 then e else have n := Qq.ofNatQ α inst n; q(«$n» * «$e»)

def Mathlib.Tactic.Linarith.mulExpr (n : ℕ) (e : Lean.Expr) : Lean.MetaM Lean.Expr

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.

def Mathlib.Tactic.Linarith.addExprs' {u : Lean.Level} {α : have u := u; Q(Type u)} (_inst : Q(AddMonoid «$α»)) : List Q(«$α») → Q(«$α»)

A type-safe analogue of addExprs.

Equations

• Mathlib.Tactic.Linarith.addExprs' _inst [] = q(0)
• Mathlib.Tactic.Linarith.addExprs' _inst (h :: t) = Mathlib.Tactic.Linarith.addExprs'.go✝ _inst h t

def Mathlib.Tactic.Linarith.addExprs : List Lean.Expr → Lean.MetaM Lean.Expr

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.
• Mathlib.Tactic.Linarith.addExprs [] = pure q(0)

def Mathlib.Tactic.Linarith.addIneq : Ineq → Ineq → Lean.Name × Ineq

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

• Mathlib.Tactic.Linarith.addIneq Mathlib.Ineq.eq Mathlib.Ineq.eq = (`Mathlib.Tactic.Linarith.eq_of_eq_of_eq, Mathlib.Ineq.eq)
• Mathlib.Tactic.Linarith.addIneq Mathlib.Ineq.eq Mathlib.Ineq.le = (`Mathlib.Tactic.Linarith.le_of_eq_of_le, Mathlib.Ineq.le)
• Mathlib.Tactic.Linarith.addIneq Mathlib.Ineq.eq Mathlib.Ineq.lt = (`Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Ineq.lt)
• Mathlib.Tactic.Linarith.addIneq Mathlib.Ineq.le Mathlib.Ineq.eq = (`Mathlib.Tactic.Linarith.le_of_le_of_eq, Mathlib.Ineq.le)
• Mathlib.Tactic.Linarith.addIneq Mathlib.Ineq.le Mathlib.Ineq.le = (`Mathlib.Tactic.Linarith.add_nonpos, Mathlib.Ineq.le)
• Mathlib.Tactic.Linarith.addIneq Mathlib.Ineq.le Mathlib.Ineq.lt = (`Mathlib.Tactic.Linarith.add_lt_of_le_of_neg, Mathlib.Ineq.lt)
• Mathlib.Tactic.Linarith.addIneq Mathlib.Ineq.lt Mathlib.Ineq.eq = (`Mathlib.Tactic.Linarith.lt_of_lt_of_eq, Mathlib.Ineq.lt)
• Mathlib.Tactic.Linarith.addIneq Mathlib.Ineq.lt Mathlib.Ineq.le = (`Mathlib.Tactic.Linarith.add_lt_of_neg_of_le, Mathlib.Ineq.lt)
• Mathlib.Tactic.Linarith.addIneq Mathlib.Ineq.lt Mathlib.Ineq.lt = (`Mathlib.Tactic.Linarith.add_neg, Mathlib.Ineq.lt)

def Mathlib.Tactic.Linarith.mkLTZeroProof : List (Lean.Expr × ℕ) → Lean.MetaM Lean.Expr

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, where R is as strong as possible.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Linarith.mkLTZeroProof [] = Lean.throwError (Lean.toMessageData "no linear hypotheses found")
• Mathlib.Tactic.Linarith.mkLTZeroProof [(h, c)] = do let __discr ← Mathlib.Tactic.Linarith.mkSingleCompZeroOf c h match __discr with | (fst, t) => pure t

def Mathlib.Tactic.Linarith.leftOfIneqProof (prf : Lean.Expr) : Lean.MetaM Lean.Expr

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

Equations

• Mathlib.Tactic.Linarith.leftOfIneqProof prf = do let __do_lift ← Lean.Meta.inferType prf let __discr ← __do_lift.ineq? match __discr with | (fst, fst_1, t, snd) => pure t

def Mathlib.Tactic.Linarith.typeOfIneqProof (prf : Lean.Expr) : Lean.MetaM Lean.Expr

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

Equations

• Mathlib.Tactic.Linarith.typeOfIneqProof prf = do let __do_lift ← Lean.Meta.inferType prf let __discr ← __do_lift.ineq? match __discr with | (fst, ty, snd) => pure ty

def Mathlib.Tactic.Linarith.mkNegOneLtZeroProof (tp : Lean.Expr) : Lean.MetaM Lean.Expr

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

Equations

• One or more equations did not get rendered due to their size.

partial def Mathlib.Tactic.Linarith.addNegEqProofsIdx : List (Lean.Expr × ℕ) → Lean.MetaM (List (Lean.Expr × ℕ))

addNegEqProofsIdx l inspects a list l of pairs (h, i) where h proves tᵢ Rᵢ 0 and i records the original index of the hypothesis. For each equality proof t = 0 in the list, it appends a proof of -t = 0 with the same index i. All other entries are preserved.

def Mathlib.Tactic.Linarith.proveEqZeroUsing (tac : Lean.Elab.Tactic.TacticM Unit) (e : Lean.Expr) : Lean.MetaM Lean.Expr

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

def Mathlib.Tactic.Linarith.proveFalseByLinarith (transparency : Lean.Meta.TransparencyMode) (oracle : CertificateOracle) (discharger : Lean.Elab.Tactic.TacticM Unit) : Lean.MVarId → List Lean.Expr → Lean.MetaM (Lean.Expr × List ℕ)

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.

oracle : CertificateOracle is used to search for a certificate of unsatisfiability.

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 provided discharger tactic, which is typically ring. We prove (2) by folding over the set of hypotheses.

transparency : TransparencyMode controls the transparency level with which atoms are identified.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Linarith.proveFalseByLinarith transparency oracle discharger x✝ [] = Lean.throwError (Lean.toMessageData "no args to linarith")