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.

def positivity : Lean.ParserDescr

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

instance Mathlib.Meta.Positivity.instReprStrictness : {u : Lean.Level} → {α : Q(Type u)} → {zα : Q(Zero «$α»)} → {pα : Q(PartialOrder «$α»)} → {e : Q(«$α»)} → Repr (Mathlib.Meta.Positivity.Strictness zα pα e)

Equations

• Mathlib.Meta.Positivity.instReprStrictness = { reprPrec := Mathlib.Meta.Positivity.reprStrictness✝ }

structure Mathlib.Meta.Positivity.PositivityExt : Type

• eval : {u : Lean.Level} → {α : Q(Type u)} → (zα : Q(Zero «$α»)) → (pα : Q(PartialOrder «$α»)) → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα pα e)

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

An extension for positivity.

def Mathlib.Meta.Positivity.mkPositivityExt (n : Lean.Name) : Lean.ImportM Mathlib.Meta.Positivity.PositivityExt

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, reducible]

abbrev Mathlib.Meta.Positivity.Entry : Type

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

Equations

• Mathlib.Meta.Positivity.Entry = (Array (Array (Lean.Meta.DiscrTree.Key true)) × Lean.Name)

opaque Mathlib.Meta.Positivity.positivityExt : Lean.PersistentEnvExtension Mathlib.Meta.Positivity.Entry (Mathlib.Meta.Positivity.Entry × Mathlib.Meta.Positivity.PositivityExt) (List Mathlib.Meta.Positivity.Entry × Lean.Meta.DiscrTree Mathlib.Meta.Positivity.PositivityExt true)

Environment extensions for positivity declarations

theorem Mathlib.Meta.Positivity.lt_of_le_of_ne' {A : Type u_1} {a : A} {b : A} [PartialOrder A] : a ≤ b → b ≠ a → a < b

theorem Mathlib.Meta.Positivity.pos_of_isNat {A : Type u_1} {e : A} {n : ℕ} [StrictOrderedSemiring A] (h : Mathlib.Meta.NormNum.IsNat e n) (w : Nat.ble 1 n = true) : 0 < e

theorem Mathlib.Meta.Positivity.nonneg_of_isNat {A : Type u_1} {e : A} {n : ℕ} [OrderedSemiring A] (h : Mathlib.Meta.NormNum.IsNat e n) : 0 ≤ e

theorem Mathlib.Meta.Positivity.nz_of_isNegNat {A : Type u_1} {e : A} {n : ℕ} [StrictOrderedRing A] (h : Mathlib.Meta.NormNum.IsInt e (Int.negOfNat n)) (w : Nat.ble 1 n = true) : e ≠ 0

theorem Mathlib.Meta.Positivity.pos_of_isRat {A : Type u_1} {e : A} {n : ℤ} {d : ℕ} [LinearOrderedRing A] : Mathlib.Meta.NormNum.IsRat e n d → decide (0 < n) = true → 0 < e

theorem Mathlib.Meta.Positivity.nonneg_of_isRat {A : Type u_1} {e : A} {n : ℤ} {d : ℕ} [LinearOrderedRing A] : Mathlib.Meta.NormNum.IsRat e n d → decide (n = 0) = true → 0 ≤ e

theorem Mathlib.Meta.Positivity.nz_of_isRat {A : Type u_1} {e : A} {n : ℤ} {d : ℕ} [LinearOrderedRing A] : Mathlib.Meta.NormNum.IsRat e n d → decide (n < 0) = true → e ≠ 0

def Mathlib.Meta.Positivity.solve (t : Q(Prop)) : Lean.MetaM Lean.Expr

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.

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.

Equations

• Mathlib.Meta.Positivity.positivity goal = do let t ← Lean.Meta.withReducible (Lean.MVarId.getType' goal) let p ← Mathlib.Meta.Positivity.solve t Lean.MVarId.assign goal p

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

Equations

• Mathlib.Tactic.Positivity.positivity = Lean.ParserDescr.node `Mathlib.Tactic.Positivity.positivity 1024 (Lean.ParserDescr.nonReservedSymbol "positivity" false)