Documentation

Mathlib.Tactic.Linarith.Preprocessing

Linarith preprocessing #

This file contains methods used to preprocess inputs to linarith.

In particular, linarith works over comparisons of the form t R 0, where R ∈ {<,≤,=}. It assumes that expressions in t have integer coefficients and that the type of t has well-behaved subtraction.

Implementation details #

A GlobalPreprocessor is a function List Expr → TacticM (List Expr). Users can add custom preprocessing steps by adding them to the LinarithConfig object. Linarith.defaultPreprocessors is the main list, and generally none of these should be skipped unless you know what you're doing.

Preprocessing #

Processor that recursively replaces P ∧ Q hypotheses with the pair P and Q.

Equations
Instances For

    Implementation of the splitConjunctions preprocessor.

    Removes any expressions that are not proofs of inequalities, equalities, or negations thereof.

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

      Implementation of the filterComparisons preprocessor.

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

        If prf is a proof of ¬ e, where e is a comparison, flipNegatedComparison prf e flips the comparison in e and returns a proof. For example, if prf : ¬ a < b, flipNegatedComparison prf q(a < b) returns a proof of a ≥ b.

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

          Replaces proofs of negations of comparisons with proofs of the reversed comparisons. For example, a proof of ¬ a < b will become a proof of a ≥ b.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            partial def Linarith.isNatProp (e : Lean.Expr) :

            isNatProp tp is true iff tp is an inequality or equality between natural numbers or the negation thereof.

            If e is of the form ((n : ℕ) : C), isNatCoe e returns ⟨n, C⟩.

            Equations
            • Linarith.isNatCoe e = match e.getAppFnArgs with | (`Nat.cast, #[target, head, n]) => some (n, target) | x => none
            Instances For

              getNatComparisons e returns a list of all subexpressions of e of the form ((t : ℕ) : C).

              If e : ℕ, returns a proof of 0 ≤ (e : C).

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

                Ordering on Expr.

                Equations
                Instances For

                  If h is an equality or inequality between natural numbers, natToInt lifts this inequality to the integers. It also adds the facts that the integers involved are nonnegative. To avoid adding the same nonnegativity facts many times, it is a global preprocessor.

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

                    If pf is a proof of a strict inequality (a : ℤ) < b, mkNonstrictIntProof pf returns a proof of a + 1 ≤ b, and similarly if pf proves a negated weak inequality.

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

                      strengthenStrictInt h turns a proof h of a strict integer inequality t1 < t2 into a proof of t1 ≤ t2 + 1.

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

                        rearrangeComparison e takes a proof e of an equality, inequality, or negation thereof, and turns it into a proof of a comparison _ R 0, where R ∈ {=, ≤, <}.

                        Equations
                        Instances For

                          Implementation of rearrangeComparison, after type inference.

                          compWithZero h takes a proof h of an equality, inequality, or negation thereof, and turns it into a proof of a comparison _ R 0, where R ∈ {=, ≤, <}.

                          Equations
                          Instances For
                            theorem Linarith.without_one_mul {M : Type u_1} [MulOneClass M] {a : M} {b : M} (h : 1 * a = b) :
                            a = b

                            normalizeDenominatorsLHS h lhs assumes that h is a proof of lhs R 0. It creates a proof of lhs' R 0, where all numeric division in lhs has been cancelled.

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

                              cancelDenoms pf assumes pf is a proof of t R 0. If t contains the division symbol /, it tries to scale t to cancel out division by numerals.

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

                                findSquares s e collects all terms of the form a ^ 2 and a * a that appear in e and adds them to the set s. A pair (i, true) is added to s when atoms[i]^2 appears in e, and (i, false) is added to s when atoms[i]*atoms[i] appears in e.

                                nlinarithExtras is the preprocessor corresponding to the nlinarith tactic.

                                • For every term t such that t^2 or t*t appears in the input, adds a proof of t^2 ≥ 0 or t*t ≥ 0.
                                • For every pair of comparisons t1 R1 0 and t2 R2 0, adds a proof of t1*t2 R 0.

                                This preprocessor is typically run last, after all inputs have been canonized.

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

                                  removeNe_aux case splits on any proof h : a ≠ b in the input, turning it into a < b ∨ a > b. This produces 2^n branches when there are n such hypotheses in the input.

                                  removeNe case splits on any proof h : a ≠ b in the input, turning it into a < b ∨ a > b, by calling linarith.removeNe_aux. This produces 2^n branches when there are n such hypotheses in the input.

                                  Equations
                                  Instances For

                                    The default list of preprocessors, in the order they should typically run.

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

                                      preprocess pps l takes a list l of proofs of propositions. It maps each preprocessor pp ∈ pps over this list. The preprocessors are run sequentially: each receives the output of the previous one. Note that a preprocessor may produce multiple or no expressions from each input expression, so the size of the list may change.

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