positivity core extensions

This file sets up the basic positivity extensions tagged with the @[positivity] attribute.

def Mathlib.Meta.Positivity.evalIte : PositivityExt

The positivity extension which identifies expressions of the form ite p a b, such that positivity successfully recognises both a and b.

def Mathlib.Meta.Positivity.evalMin : PositivityExt

The positivity extension which identifies expressions of the form min a b, such that positivity successfully recognises both a and b.

def Mathlib.Meta.Positivity.evalMax : PositivityExt

Extension for the max operator. The max of two numbers is nonnegative if at least one is nonnegative, strictly positive if at least one is positive, and nonzero if both are nonzero.

def Mathlib.Meta.Positivity.evalAdd : PositivityExt

The positivity extension which identifies expressions of the form a + b, such that positivity successfully recognises both a and b.

def Mathlib.Meta.Positivity.evalMul : PositivityExt

The positivity extension which identifies expressions of the form a * b, such that positivity successfully recognises both a and b.

def Mathlib.Meta.Positivity.evalIntDiv : PositivityExt

The positivity extension which identifies expressions of the form a / b, where a and b are integers.

def Mathlib.Meta.Positivity.evalPowZeroNat : PositivityExt

The positivity extension which identifies expressions of the form a ^ (0 : ℕ). This extension is run in addition to the general a ^ b extension (they are overlapping).

def Mathlib.Meta.Positivity.evalPow : PositivityExt

The positivity extension which identifies expressions of the form a ^ (b : ℕ), such that positivity successfully recognises both a and b.

def Mathlib.Meta.Positivity.evalAbs : PositivityExt

The positivity extension which identifies expressions of the form |a|.

def Mathlib.Meta.Positivity.evalNatAbs : PositivityExt

Extension for the positivity tactic: Int.natAbs is positive when its input is. Since the output type of Int.natAbs is ℕ, the nonnegative case is handled by the default positivity tactic.

def Mathlib.Meta.Positivity.evalNatCast : PositivityExt

Extension for the positivity tactic: Nat.cast is always non-negative, and positive when its input is.

def Mathlib.Meta.Positivity.evalIntCast : PositivityExt

Extension for the positivity tactic: Int.cast is positive (resp. non-negative) if its input is.

def Mathlib.Meta.Positivity.evalNatSucc : PositivityExt

Extension for Nat.succ.

def Mathlib.Meta.Positivity.evalPNatVal : PositivityExt

Extension for PNat.val.

def Mathlib.Meta.Positivity.evalFactorial : PositivityExt

Extension for Nat.factorial.

def Mathlib.Meta.Positivity.evalAscFactorial : PositivityExt

Extension for Nat.ascFactorial.

def Mathlib.Meta.Positivity.evalNNRatNum : PositivityExt

The positivity extension which identifies expressions of the form NNRat.num q, such that positivity successfully recognises q.

def Mathlib.Meta.Positivity.evalNNRatDen : PositivityExt

The positivity extension which identifies expressions of the form Rat.den a.

def Mathlib.Meta.Positivity.evalRatNum : PositivityExt

The positivity extension which identifies expressions of the form Rat.num a, such that positivity successfully recognises a.

def Mathlib.Meta.Positivity.evalRatDen : PositivityExt

The positivity extension which identifies expressions of the form Rat.den a.

def Mathlib.Meta.Positivity.evalPosPart : PositivityExt

Extension for posPart. a⁺ is always nonegative, and positive if a is.

def Mathlib.Meta.Positivity.evalNegPart : PositivityExt

Extension for negPart. a⁻ is always nonegative.