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

A definition of type PositivityExt tagged @[positivity t] extends the positivity tactic. The term (with underscores) t indicates which expressions this extension accepts. An extension will be given an expression e : α, together with hypotheses [Zero α] [PartialOrder α] and attempts to prove e > 0, e ≥ 0, or e ≠ 0.

When Positivity.core calls this extension on an expression e, it does not guarantee that e matches t perfectly: validate the form of the expression (using e.g. match_expr (← withReducible (whnf e))) before building a proof. See also the let .app ... ← withReducible (whnf e) | throwError ... lines in the example below.

An extension can call Mathlib.Meta.Positivity.core to recursively solve subgoals.

Example:

@[positivity ite _ _ _] def evalIte : PositivityExt where eval {u α} zα pα e := do
  let .app (.app (.app (.app f (p : Q(Prop))) (_ : Q(Decidable $p))) (a : Q($α))) (b : Q($α))
    ← withReducible (whnf e) | throwError "not ite"
  haveI' : $e =Q ite $p $a $b := ⟨⟩
  guard <| ← withDefault <| withNewMCtxDepth <| isDefEq f q(ite (α := $α))
  let ra ← core zα pα a; let rb ← core zα pα b
  ...

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(«$α»)) : Type

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

• positive {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} (pf : Q(0 < «$e»)) : Strictness zα pα e
• nonnegative {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} (pf : Q(0 ≤ «$e»)) : Strictness zα pα e
• nonzero {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} (pf : Q(«$e» ≠ 0)) : Strictness zα pα e
• none {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} : Strictness zα pα e

def Mathlib.Meta.Positivity.instReprStrictness.repr {u✝ : Lean.Level} {α✝ : Q(Type u✝)} {zα✝ : Q(Zero $α✝)} {pα✝ : Q(PartialOrder $α✝)} {e✝ : Q($α✝)} : Strictness zα✝ pα✝ e✝ → ℕ → Std.Format

@[implicit_reducible]

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

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

Gives a generic description of the positivity result.

def Mathlib.Meta.Positivity.Strictness.toPositive {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) {e : Q(«$α»)} : Strictness zα pα e → Option Q(0 < «$e»)

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

def Mathlib.Meta.Positivity.Strictness.toNonneg {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) {e : Q(«$α»)} : Strictness zα pα e → Option Q(0 ≤ «$e»)

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

def Mathlib.Meta.Positivity.Strictness.toNonzero {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) {e : Q(«$α»)} : Strictness zα pα e → Option Q(«$e» ≠ 0)

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

structure Mathlib.Meta.Positivity.PositivityExt : Type

An extension for positivity.

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

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

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

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

@[reducible, inline]

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.

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

Environment extensions for positivity declarations

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

theorem Mathlib.Meta.Positivity.pos_of_isNat' {A : Type u_1} {e : A} {n : ℕ} [AddMonoidWithOne A] [PartialOrder A] [AddLeftMono A] [ZeroLEOneClass A] [h'' : NeZero 1] (h : 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 : ℕ} [Semiring A] [PartialOrder A] [IsOrderedRing A] (h : NormNum.IsNat e n) : 0 ≤ e

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

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

theorem Mathlib.Meta.Positivity.pos_of_isNNRat {A : Type u_1} {e : A} {n d : ℕ} [Semiring A] [LinearOrder A] [IsStrictOrderedRing A] : NormNum.IsNNRat e n d → decide (0 < n) = true → 0 < e

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

theorem Mathlib.Meta.Positivity.nonneg_of_isNNRat {A : Type u_1} {e : A} {n d : ℕ} [Semiring A] [LinearOrder A] : NormNum.IsNNRat e n d → decide (n = 0) = true → 0 ≤ e

theorem Mathlib.Meta.Positivity.nonneg_of_isRat {A : Type u_1} {e : A} {n : ℤ} {d : ℕ} [Ring A] [LinearOrder A] : 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 : ℕ} [Ring A] [LinearOrder A] [IsStrictOrderedRing A] : NormNum.IsRat e n d → decide (n < 0) = true → e ≠ 0

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

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

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

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

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

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

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

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

def Mathlib.Meta.Positivity.compareHypLE {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (lo e : Q(«$α»)) (p₂ : Q(«$lo» ≤ «$e»)) : Lean.MetaM (Strictness zα pα e)

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

def Mathlib.Meta.Positivity.compareHypLT {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (lo e : Q(«$α»)) (p₂ : Q(«$lo» < «$e»)) : Lean.MetaM (Strictness zα pα e)

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

def Mathlib.Meta.Positivity.compareHypEq {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (e x : Q(«$α»)) (p₂ : Q(«$x» = «$e»)) : Lean.MetaM (Strictness zα pα e)

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

def Mathlib.Meta.Positivity.compareHyp {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (e : Q(«$α»)) (ldecl : Lean.LocalDecl) : Lean.MetaM (Strictness zα pα e)

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

def Mathlib.Meta.Positivity.orElse {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} (t₁ : Strictness zα pα e) (t₂ : Lean.MetaM (Strictness zα pα e)) : Lean.MetaM (Strictness zα pα 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.

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

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

def Mathlib.Meta.Positivity.bestResult (e : Lean.Expr) : Lean.MetaM (Bool × Lean.Expr)

Given an expression e, use the core method of the positivity tactic to prove it positive, or, failing that, nonnegative; return a Boolean (signalling whether the strict or non-strict inequality was established) together with the proof as an expression.

def Mathlib.Meta.Positivity.proveNonneg (e : Lean.Expr) : Lean.MetaM Lean.Expr

Given an expression e, use the core method of the positivity tactic to prove it nonnegative.

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

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.

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 [≤/</≠] e, attempts to recurse on the structure of e to prove the goal. It will either close goal or fail.

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

positivity solves goals of the form 0 ≤ x, 0 < x and x ≠ 0. The tactic works recursively according to the syntax of the expression x, by attempting to prove subexpressions are positive/nonnegative/nonzero and combining this into a final proof. This tactic either closes the goal or fails.

For each subexpression e, positivity will try to:

• try @[positivity]-tagged extensions to recursively prove e is positive/nonnegative/nonzero based on its subexpressions (see the positivity attribute for more details), or
• try the norm_num tactic to prove e is positive/nonnegative/nonzero, or
• try showing e : t is nonnegative because there is a CanonicallyOrderedAdd t instance, or
• use a local hypothesis of the form 0 ≤ e, 0 < e or e ≠ 0.

This tactic is extensible. See the positivity attribute documentation for more details.

• positivity [t₁, …, tₙ] first executes have := t₁; …; have := tₙ in the current goal, then runs positivity. This is useful when positivity needs derived premises such as 0 < y for division/reciprocal, or 0 ≤ x for real powers.

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

example {a b c d : ℝ} (hab : 0 < a * b) (hb : 0 ≤ b) (hcd : c < d) :
    0 < a ^ c + 1 / (d - c) := by
  positivity [sub_pos_of_lt hcd, pos_of_mul_pos_left hab hb]

We set up positivity as a first-pass discharger for gcongr side goals.

We register positivity with the hint tactic.