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.
theorem ne_of_ne_of_eq' {α : Sort u_1} {a : α} {c : α} {b : α} (hab : a c) (hbc : a = b) :
b c
Equations
inductive Mathlib.Meta.Positivity.Strictness {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (zα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Zero [u]) α)) (pα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `PartialOrder [u]) α)) (e : Qq.QQ α) :

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✝ }

    Gives a generic description of the positivity result.

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

    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.
      @[inline]

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

      Equations
      theorem Mathlib.Meta.Positivity.lt_of_le_of_ne' {A : Type u_1} {a : A} {b : A} [inst : PartialOrder A] :
      a bb aa < b
      theorem Mathlib.Meta.Positivity.pos_of_isNat {A : Type u_1} {e : A} {n : } [inst : StrictOrderedSemiring A] (h : Mathlib.Meta.NormNum.IsNat e n) (w : Nat.ble 1 n = true) :
      0 < e
      theorem Mathlib.Meta.Positivity.pos_of_isRat {A : Type u_1} {e : A} {n : } {d : } [inst : 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 : } [inst : 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 : } [inst : LinearOrderedRing A] :
      Mathlib.Meta.NormNum.IsRat e n ddecide (n < 0) = truee 0

      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.
      def Mathlib.Meta.Positivity.throwNone {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {zα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Zero [u]) α)} {pα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `PartialOrder [u]) α)} {m : TypeType u_1} {e : Qq.QQ α} [inst : Monad m] [inst : 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

      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.

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

      Equations
      • One or more equations did not get rendered due to their size.
      def Mathlib.Meta.Positivity.compareHypLE {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (zα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Zero [u]) α)) (pα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `PartialOrder [u]) α)) (lo : Qq.QQ α) (e : Qq.QQ α) (p₂ : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `LE.le [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Preorder.toLE [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `PartialOrder.toPreorder [u]) α) ))) lo) e)) :

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

      Equations
      • One or more equations did not get rendered due to their size.
      def Mathlib.Meta.Positivity.compareHypLT {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (zα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Zero [u]) α)) (pα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `PartialOrder [u]) α)) (lo : Qq.QQ α) (e : Qq.QQ α) (p₂ : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `LT.lt [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Preorder.toLT [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `PartialOrder.toPreorder [u]) α) ))) 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.

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

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

      A variation on assumption which checks if the hypothesis ldecl is a [ where a is a numeral.

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

      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
      • One or more equations did not get rendered due to their size.

      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.

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

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

      Tactic solving goals of the form 0 ≤ x≤ x, 0 < x and x ≠ 0≠ 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
      ≤ a ^ 3 + a := by positivity
      
      example {a : ℤ} (ha : 1 < a) : 0 < |(3:ℤ) + a| := by positivity
      
      example {b : ℤ} : 0 ≤ max (-3) (b ^ 2) := by positivity
      ≤ max (-3) (b ^ 2) := by positivity
      
      Equations