# mathlibdocumentation

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

• by a hypothesis such as 5 ≤ 3 * a ^ 2 + b * c which directly implies the nonegativity of 3 * a ^ 2 + b * c; or,
• by the application of the lemma add_nonneg and the success of the positivity tactic on the two sub-expressions 3 * a ^ 2 and b * c.

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 #

• tactic.norm_num.positivity tries to prove positivity of an expression by running norm_num on it. This is one of the base cases of the recursion.
• tactic.positivity.compare_hyp tries to prove positivity of an expression by comparing with a provided hypothesis. If the hypothesis is of the form a ≤ b or similar, with b matching the expression whose proof of positivity is desired, then it will check whether a can be proved positive via tactic.norm_num.positivity and if so apply a transitivity lemma. This is the other base case of the recursion.
• tactic.positivity.attr creates the positivity user attribute for tagging the extension tactics handling specific operations, and specifies the behaviour for a single step of the recursion
• tactic.positivity.core collects the list of tactics with the @[positivity] attribute and calls the first recursion step as specified in tactic.positivity.attr. Its input is e : expr and its output (if it succeeds) is a term of a custom inductive type tactic.positivity.strictness, containing an expr which is a proof of the strict-positivity/nonnegativity of e as well as an indication of whether what could be proved was strict-positivity or nonnegativity
• tactic.interactive.positivity is the user-facing tactic. It parses the goal and, if it is of one of the forms 0 ≤ e, 0 < e, e > 0, e ≥ 0, it sends e to tactic.positivity.core.

## TODO #

Implement extensions for other operations (raising to non-numeral powers, log).

@[protected, instance]
meta inductive tactic.positivity.strictness  :
Type
• positive :
• nonnegative :

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

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

Second base case of the positivity tactic: Any element of a canonically ordered additive monoid is nonnegative.

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 #

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

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

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.

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

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

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



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 #

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

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.

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

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

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

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

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

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

Extension for the positivity tactic: casts from ℕ, ℤ, ℚ.

Extension for the positivity tactic: finset.card s is positive if s is nonempty.