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

source
def positivity :
Lean.ParserDescr

Attribute for identifying `positivity` extensions.

Equations

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

Instances For

source
theorem ne_of_ne_of_eq' {α : Sort u_1} {a c b : α} (hab : a ≠ c) (hbc : a = b) :
b ≠ c
source
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

Instances For

source
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
Equations

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

Instances For

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

- Mathlib.Meta.Positivity.instReprStrictness = { reprPrec := Mathlib.Meta.Positivity.instReprStrictness.repr }

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

Equations

- Mathlib.Meta.Positivity.Strictness.toString zα pα (Mathlib.Meta.Positivity.Strictness.positive a) = "positive"
- Mathlib.Meta.Positivity.Strictness.toString zα pα (Mathlib.Meta.Positivity.Strictness.nonnegative a) = "nonnegative"
- Mathlib.Meta.Positivity.Strictness.toString zα pα (Mathlib.Meta.Positivity.Strictness.nonzero a) = "nonzero"
- Mathlib.Meta.Positivity.Strictness.toString zα pα Mathlib.Meta.Positivity.Strictness.none = "none"

Instances For

source
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`.

Equations

- Mathlib.Meta.Positivity.Strictness.toPositive zα pα (Mathlib.Meta.Positivity.Strictness.positive pf) = some pf
- Mathlib.Meta.Positivity.Strictness.toPositive zα pα x✝ = none

Instances For

source
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`.

Equations

- Mathlib.Meta.Positivity.Strictness.toNonneg zα pα (Mathlib.Meta.Positivity.Strictness.positive pf) = some q(⋯)
- Mathlib.Meta.Positivity.Strictness.toNonneg zα pα (Mathlib.Meta.Positivity.Strictness.nonnegative pf) = some pf
- Mathlib.Meta.Positivity.Strictness.toNonneg zα pα x✝ = none

Instances For

source
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`.

Equations

- Mathlib.Meta.Positivity.Strictness.toNonzero zα pα (Mathlib.Meta.Positivity.Strictness.positive pf) = some q(⋯)
- Mathlib.Meta.Positivity.Strictness.toNonzero zα pα (Mathlib.Meta.Positivity.Strictness.nonzero pf) = some pf
- Mathlib.Meta.Positivity.Strictness.toNonzero zα pα x✝ = none

Instances For

source
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`.

Instances For

source
def Mathlib.Meta.Positivity.mkPositivityExt (n : Lean.Name) :
Lean.ImportM 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.

Instances For

source
@[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.

Equations

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

Instances For

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

Environment extensions for `positivity` declarations

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

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.throwNone {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {m : Type → Type u_2} {e : Q(«$α»)} [Monad m] [Alternative m] (t : m (Strictness zα pα e)) :
m (Strictness zα pα e)

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

Equations

- Mathlib.Meta.Positivity.throwNone t = do let __do_lift ← t match __do_lift with | Mathlib.Meta.Positivity.Strictness.none => failure | r => pure r

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Instances For

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

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Meta.Positivity.orElse Mathlib.Meta.Positivity.Strictness.none t₂ = Mathlib.Meta.Positivity.catchNone t₂
- Mathlib.Meta.Positivity.orElse (Mathlib.Meta.Positivity.Strictness.positive pf) t₂ = pure (Mathlib.Meta.Positivity.Strictness.positive pf)

Instances For

source
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`.

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

- Mathlib.Meta.Positivity.positivity goal = do let t ← Lean.Meta.withReducible goal.getType' let p ← Mathlib.Meta.Positivity.solve t goal.assign p

Instances For

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

`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]

Equations

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

Instances For

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

We register `positivity` with the `hint` tactic.