## `positivity` core extensions #

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

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalIntDiv :
PositivityExt

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalAbs :
PositivityExt

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

Equations

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

Instances For

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

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalNatCast :
PositivityExt

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

Instances For

source
def Mathlib.Meta.Positivity.evalIntCast :
PositivityExt

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

Instances For

source
def Mathlib.Meta.Positivity.evalNatSucc :
PositivityExt

Extension for `Nat.succ`.

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalPNatVal :
PositivityExt

Extension for `PNat.val`.

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalFactorial :
PositivityExt

Extension for `Nat.factorial`.

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalAscFactorial :
PositivityExt

Extension for `Nat.ascFactorial`.

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalNatGCD :
PositivityExt

Extension for `Nat.gcd`. Uses positivity of the left term, if available, then tries the right term.

The implementation relies on the fact that `Positivity.core` on `ℕ` never returns `nonzero`.

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalNatLCM :
PositivityExt

Extension for `Nat.lcm`.

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalNatSqrt :
PositivityExt

Extension for `Nat.sqrt`.

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalIntGCD :
PositivityExt

Extension for `Int.gcd`. Uses positivity of the left term, if available, then tries the right term.

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalIntLCM :
PositivityExt

Extension for `Int.lcm`.

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalNNRatNum :
PositivityExt

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

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalNNRatDen :
PositivityExt

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

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalRatNum :
PositivityExt

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

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalRatDen :
PositivityExt

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

Equations

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

Instances For

source
def Mathlib.Meta.Positivity.evalPosPart :
PositivityExt

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

Instances For

source
def Mathlib.Meta.Positivity.evalNegPart :
PositivityExt

Extension for `negPart`. `a⁻` is always nonnegative.

Instances For

source
def Mathlib.Meta.Positivity.evalMap :
PositivityExt

Extension for the `positivity` tactic: nonnegative maps take nonnegative values.

Equations

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

Instances For