mathlib3 documentation

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

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

meta inductive tactic.positivity.strictness  :

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

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]

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 #

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

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

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

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

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.

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 α] [covariant_class α α has_add.add has_le.le] {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.