# mathlib3documentation

tactic.positivity

# positivity tactic #

The positivity tactic in this file solves goals of the form 0 ≤ x, 0 < x and x ≠ 0. 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.positivity.order_rel is a custom inductive type recording whether the goal is 0 ≤ e/e ≥ 0, 0 < e/e > 0, e ≠ 0 or 0 ≠ e.
• 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, e ≠ 0, 0 ≠ e, 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  :
• positive :
• nonnegative :
• nonzero :

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

Instances for tactic.positivity.strictness
@[protected, instance]
@[protected, instance]

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

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

Inductive type recording whether the goal positivity is called on is nonnegativity, positivity or different from 0.

Instances for tactic.positivity.order_rel
@[protected, instance]
@[protected, instance]
@[protected]

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 one reports nonnegative and the other reports nonzero, report positive
• else if at least one reports nonnegative, report nonnegative and one of the expressions giving a proof of nonnegativity
• else if at least one reports nonzero, report nonzero and one of the expressions giving a proof of nonzeroness
• if both fail, fail

This tactic fails with a message saying that positivity couldn't prove anything about e if we only know that a and b are positive/nonnegative/nonzero (according to pa and pb).

### Core logic of the positivity tactic #

meta def tactic.positivity.compare_hyp_le (e a b p₂ : expr) :

Calls norm_num on a to prove positivity/nonnegativity of e assuming b is defeq to e and p₂ : a ≤ b.

meta def tactic.positivity.compare_hyp_lt (e a b p₂ : expr) :

Calls norm_num on a to prove positivity/nonnegativity of e assuming b is defeq to e and p₂ : a < b.

meta def tactic.positivity.compare_hyp_eq (e a b p₂ : expr) :

Calls norm_num on a to prove positivity/nonnegativity/nonzeroness of e assuming b is defeq to e and p₂ : a = b.

meta def tactic.positivity.compare_hyp_ne (e a b p₂ : expr) :

Calls norm_num on a to prove nonzeroness of e assuming b is defeq to e and p₂ : b ≠ a.

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

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

Attribute allowing a user to tag a tactic as an extension for tactic.interactive.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), nonnegativity (nonnegative p), or nonzeroness (nonzero p).

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.

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

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 if then else of two numbers is positive/nonnegative/nonzero if both are.

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, strictly positive if at least one is positive, and nonzero if both are nonzero.

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/positive/nonzero 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: raising a positive number in a canonically ordered semiring gives a positive number.

theorem tactic.abs_pos_of_ne_zero {α : Type u_1} [add_group α] [linear_order α] {a : α} :
a 0 0 < |a|

Alias of the reverse direction of abs_pos.

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

Extension for the positivity tactic: int.nat_abs is positive when its input is.

Since the output type of int.nat_abs is ℕ, the nonnegative case is handled by the default positivity tactic.

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

Extension for the positivity tactic: nat.succ is always positive.

Extension for the positivity tactic: nat.factorial is always positive.

Extension for the positivity tactic: nat.asc_factorial is always positive.

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