mathlib documentation

tactic.positivity

positivity tactic #

The positivity tactic in this file solves goals of the form 0 ≤ x and 0 < x. The tactic works recursively according to the syntax of the expression x. For example, a goal of the form 0 ≤ 3 * a ^ 2 + b * c can be solved either

For each supported operation, one must write a small tactic, tagged with the attribute @[positivity], which operates only on goals whose leading function application is that operation. Typically, this small tactic will run the full positivity tactic on one or more of the function's arguments (which is where the recursion comes in), and if successful will combine this with an appropriate lemma to give positivity of the full expression.

This file contains the core positivity logic and the small tactics handling the basic operations: min, max, +, *, /, ⁻¹, raising to natural powers, and taking absolute values. Further extensions, e.g. to handle real.sqrt and norms, can be found in the files of the library which introduce these operations.

Main declarations #

TODO #

Implement extensions for other operations (raising to non-numeral powers, exp, log, coercions from ℕ and ℝ≥0).

source
@[protected, instance]
meta def tactic.positivity.strictness.decidable_eq  :
decidable_eq tactic.positivity.strictness
source
meta inductive tactic.positivity.strictness  :
Type

Inductive type recording either positive and an expression (typically a proof of a fact 0 < x) or nonnegative and an expression (typically a proof of a fact 0 ≤ x).

source
meta def tactic.norm_num.positivity (e : expr) :
tactic tactic.positivity.strictness

First base case of the positivity tactic. We try norm_num to prove directly that an expression e is positive or nonnegative.

source
meta def tactic.positivity.orelse' (tac1 tac2 : tactic tactic.positivity.strictness) :
tactic tactic.positivity.strictness

Given two tactics whose result is strictness, report a strictness:

  • if at least one gives positive, report positive and one of the expressions giving a proof of positivity
  • if neither gives pos but at least one gives nonnegative, report nonnegative and one of the expressions giving a proof of nonnegativity
  • if both fail, fail

Core logic of the positivity tactic #

source
meta def tactic.positivity.compare_hyp (e p₂ : expr) :
tactic tactic.positivity.strictness

Second base case of the positivity tactic. Prove an expression e is positive/nonnegative by finding a hypothesis of the form a < e or a ≤ e in which a can be proved positive/nonnegative by norm_num.

source
meta def tactic.positivity.attr  :
(user_attribute (expr → tactic tactic.positivity.strictness))

Attribute allowing a user to tag a tactic as an extension for tactic.positivity. The main (recursive) step of this tactic is to try successively all the extensions tagged with this attribute on the expression at hand, and also to try the two "base case" tactics tactic.norm_num.positivity, tactic.positivity.compare_hyp on the expression at hand.

source
meta def tactic.positivity.core (e : expr) :
tactic tactic.positivity.strictness

Look for a proof of positivity/nonnegativity of an expression e; if found, return the proof together with a strictness stating whether the proof found was for strict positivity (positive p) or only for nonnegativity (nonnegative p).

source
meta def tactic.interactive.positivity  :
tactic unit

Tactic solving goals of the form 0 ≤ x and 0 < x. 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 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
```
source
def tactic_doc.tactic.positivity  :
tactic_doc_entry

Tactic solving goals of the form 0 ≤ x and 0 < x. 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 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
```

positivity extensions for particular arithmetic operations #

source
meta def tactic.positivity_min  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: the min of two numbers is nonnegative if both are nonnegative, and strictly positive if both are.

source
meta def tactic.positivity_max  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: the max of two numbers is nonnegative if at least one is nonnegative, and strictly positive if at least one is positive.

source
meta def tactic.positivity_add  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: addition is nonnegative if both summands are nonnegative, and strictly positive if at least one summand is.

source
meta def tactic.positivity_mul  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: multiplication is nonnegative if both multiplicands are nonnegative, and strictly positive if both multiplicands are.

source
meta def tactic.positivity_div  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: division is nonnegative if both numerator and denominator are nonnegative, and strictly positive if both numerator and denominator are.

source
meta def tactic.positivity_inv  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: an inverse of a positive number is positive, an inverse of a nonnegative number is nonnegative.

source
meta def tactic.positivity_pow  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: raising a number a to a natural number power n is known to be positive if n = 0 (since a ^ 0 = 1) or if 0 < a, and is known to be nonnegative if n = 2 (squares are nonnegative) or if 0 ≤ a.

source
meta def tactic.positivity_abs  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: an absolute value is nonnegative, and is strictly positive if its input is.