Documentation

Mathlib.Tactic.Linarith.Verification

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} (α : let u := u; Q(Type u)) :
Q(Semiring «$α»)(n : ) → Q(«$α»)

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

Equations
    Instances For

      Auxiliary functions for assembling proofs #

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

      A typesafe version of mulExpr.

      Equations
        Instances For

          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
            Instances For
              def Linarith.addExprs' {u : Lean.Level} {α : let u := u; Q(Type u)} (_inst : Q(AddMonoid «$α»)) :
              List Q(«$α»)Q(«$α»)

              A type-safe analogue of addExprs.

              Equations
                Instances For
                  def Linarith.addExprs'.go {u : Lean.Level} {α : let u := u; Q(Type u)} (_inst : Q(AddMonoid «$α»)) (p : Q(«$α»)) :
                  List Q(«$α»)Q(«$α»)

                  Inner loop for addExprs'.

                  Equations
                    Instances For

                      addExprs L creates an Expr representing the sum of the elements of L, associated left.

                      Equations
                        Instances For

                          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
                            Instances For

                              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
                                Instances For

                                  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
                                    Instances For

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

                                      Equations
                                        Instances For

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

                                          Equations
                                            Instances For

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

                                              Equations
                                                Instances For

                                                  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
                                                    Instances For

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

                                                      Equations
                                                        Instances For

                                                          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.

                                                          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
                                                            Instances For

                                                              Log f under linarith.detail, with exception emojis and the provided name.

                                                              Equations
                                                                Instances For