Documentation

Mathlib.Tactic.Positivity.Core

positivity core functionality #

This file sets up the positivity tactic and the @[positivity] attribute, which allow for plugging in new positivity functionality around a positivity-based driver. The actual behavior is in @[positivity]-tagged definitions in Tactic.Positivity.Basic and elsewhere.

Attribute for identifying positivity extensions.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem ne_of_ne_of_eq' {α : Sort u_1} {a : α} {c : α} {b : α} (hab : a c) (hbc : a = b) :
    b c
    inductive Mathlib.Meta.Positivity.Strictness {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (e : Q(«$α»)) :

    The result of positivity running on an expression e of type α.

    Instances For
      instance Mathlib.Meta.Positivity.instReprStrictness :
      {u : Lean.Level} → {α : Q(Type u)} → { : Q(Zero «$α»)} → { : Q(PartialOrder «$α»)} → {e : Q(«$α»)} → Repr (Mathlib.Meta.Positivity.Strictness e)
      Equations
      • Mathlib.Meta.Positivity.instReprStrictness = { reprPrec := Mathlib.Meta.Positivity.reprStrictness✝ }
      def Mathlib.Meta.Positivity.Strictness.toString {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) {e : Q(«$α»)} :

      Gives a generic description of the positivity result.

      Equations
      Instances For
        def Mathlib.Meta.Positivity.Strictness.toNonneg {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) {e : Q(«$α»)} :

        Extract a proof that e is nonnegative, if possible, from Strictness information about e.

        Equations
        Instances For
          def Mathlib.Meta.Positivity.Strictness.toNonzero {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) {e : Q(«$α»)} :

          Extract a proof that e is nonzero, if possible, from Strictness information about e.

          Equations
          Instances For

            An extension for positivity.

            Instances For

              Read a positivity extension from a declaration of the right type.

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

                Configuration for DiscrTree.

                Equations
                Instances For
                  @[reducible, inline]

                  Each positivity extension is labelled with a collection of patterns which determine the expressions to which it should be applied.

                  Equations
                  Instances For
                    theorem Mathlib.Meta.Positivity.lt_of_le_of_ne' {A : Type u_1} {a : A} {b : A} [PartialOrder A] :
                    a bb aa < b
                    theorem Mathlib.Meta.Positivity.pos_of_isRat {A : Type u_1} {e : A} {n : } {d : } [LinearOrderedRing A] :
                    Mathlib.Meta.NormNum.IsRat e n ddecide (0 < n) = true0 < e
                    theorem Mathlib.Meta.Positivity.nonneg_of_isRat {A : Type u_1} {e : A} {n : } {d : } [LinearOrderedRing A] :
                    Mathlib.Meta.NormNum.IsRat e n ddecide (n = 0) = true0 e
                    theorem Mathlib.Meta.Positivity.nz_of_isRat {A : Type u_1} {e : A} {n : } {d : } [LinearOrderedRing A] :
                    Mathlib.Meta.NormNum.IsRat e n ddecide (n < 0) = truee 0
                    def Mathlib.Meta.Positivity.catchNone {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} (t : Lean.MetaM (Mathlib.Meta.Positivity.Strictness e)) :

                    Converts a MetaM Strictness which can fail into one that never fails and returns .none instead.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def Mathlib.Meta.Positivity.throwNone {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {m : TypeType u_2} {e : Q(«$α»)} [Monad m] [Alternative m] (t : m (Mathlib.Meta.Positivity.Strictness e)) :

                      Converts a MetaM Strictness which can return .none into one which never returns .none but fails instead.

                      Equations
                      Instances For
                        def Mathlib.Meta.Positivity.normNumPositivity {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (e : Q(«$α»)) :

                        Attempts to prove a Strictness result when e evaluates to a literal number.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Mathlib.Meta.Positivity.positivityCanon {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (e : Q(«$α»)) :

                          Attempts to prove that e ≥ 0 using zero_le in a CanonicallyOrderedAddCommMonoid.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Mathlib.Meta.Positivity.compareHypLE {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (lo : Q(«$α»)) (e : Q(«$α»)) (p₂ : Q(«$lo» «$e»)) :

                            A variation on assumption when the hypothesis is lo ≤ e where lo is a numeral.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def Mathlib.Meta.Positivity.compareHypLT {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (lo : Q(«$α»)) (e : Q(«$α»)) (p₂ : Q(«$lo» < «$e»)) :

                              A variation on assumption when the hypothesis is lo < e where lo is a numeral.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def Mathlib.Meta.Positivity.compareHypEq {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (e : Q(«$α»)) (x : Q(«$α»)) (p₂ : Q(«$x» = «$e»)) :

                                A variation on assumption when the hypothesis is x = e where x is a numeral.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def Mathlib.Meta.Positivity.compareHyp {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (e : Q(«$α»)) (ldecl : Lean.LocalDecl) :

                                  A variation on assumption which checks if the hypothesis ldecl is a [</≤/=] e where a is a numeral.

                                  Instances For
                                    def Mathlib.Meta.Positivity.orElse {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} (t₁ : Mathlib.Meta.Positivity.Strictness e) (t₂ : Lean.MetaM (Mathlib.Meta.Positivity.Strictness e)) :

                                    The main combinator which combines multiple positivity results. It assumes t₁ has already been run for a result, and runs t₂ and takes the best result. It will skip t₂ if t₁ is already a proof of .positive, and can also combine .nonnegative and .nonzero to produce a .positive result.

                                    Equations
                                    Instances For
                                      def Mathlib.Meta.Positivity.core {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (e : Q(«$α»)) :

                                      Run each registered positivity extension on an expression, returning a NormNum.Result.

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

                                        An auxiliary entry point to the positivity tactic. Given a proposition t of the form 0 [≤/</≠] e, attempts to recurse on the structure of t to prove it. It returns a proof or fails.

                                        Instances For

                                          The main entry point to the positivity tactic. Given a goal goal of the form 0 [≤/</≠] e, attempts to recurse on the structure of e to prove the goal. It will either close goal or fail.

                                          Equations
                                          Instances For

                                            Tactic solving goals of the form 0 ≤ x, 0 < x and x ≠ 0. The tactic works recursively according to the syntax of the expression x, if the atoms composing the expression all have numeric lower bounds which can be proved positive/nonnegative/nonzero by norm_num. This tactic either closes the goal or fails.

                                            Examples:

                                            example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 3 + a := by positivity
                                            
                                            example {a : ℤ} (ha : 1 < a) : 0 < |(3:ℤ) + a| := by positivity
                                            
                                            example {b : ℤ} : 0 ≤ max (-3) (b ^ 2) := by positivity
                                            
                                            Equations
                                            Instances For