# 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.

Instances For
theorem ne_of_ne_of_eq' {α : Sort u_1} {a : α} {c : α} {b : α} (hab : a c) (hbc : a = b) :
b c
instance Mathlib.Meta.Positivity.instReprStrictness :
{u : Lean.Level} → {α : Q(Type u)} → { : Q(Zero «$α»)} → { : Q(PartialOrder «$α»)} → {e : Q(«$α»)} → Repr () • eval : {u : Lean.Level} → {α : Q(Type u)} → ( : Q(Zero «$α»)) → ( : Q(PartialOrder «$α»)) → (e : Q(«$α»)) →

Attempts to prove an expression e : α is >0, ≥0, or ≠0.

An extension for positivity.

Instances For

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

Instances For
@[inline, reducible]

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

Instances For

Environment extensions for positivity declarations

theorem Mathlib.Meta.Positivity.lt_of_le_of_ne' {A : Type u_1} {a : A} {b : A} [] :
a bb aa < b
theorem Mathlib.Meta.Positivity.pos_of_isNat {A : Type u_1} {e : A} {n : } (h : ) (w : Nat.ble 1 n = true) :
0 < e
theorem Mathlib.Meta.Positivity.nonneg_of_isNat {A : Type u_1} {e : A} {n : } [] (h : ) :
0 e
theorem Mathlib.Meta.Positivity.nz_of_isNegNat {A : Type u_1} {e : A} {n : } (h : ) (w : Nat.ble 1 n = true) :
e 0
theorem Mathlib.Meta.Positivity.pos_of_isRat {A : Type u_1} {e : A} {n : } {d : } :
decide (0 < n) = true0 < e
theorem Mathlib.Meta.Positivity.nonneg_of_isRat {A : Type u_1} {e : A} {n : } {d : } :
decide (n = 0) = true0 e
theorem Mathlib.Meta.Positivity.nz_of_isRat {A : Type u_1} {e : A} {n : } {d : } :
decide (n < 0) = truee 0

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

Instances For
def Mathlib.Meta.Positivity.positivity (goal : Lean.MVarId) :Lean.MetaM Unit

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.

Instances For
def Mathlib.Tactic.Positivity.positivity :Lean.ParserDescr

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

Instances For