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

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

Instances for tactic.positivity.strictness
source
@[protected, instance]
meta def tactic.positivity.strictness.has_to_string  :
has_to_string tactic.positivity.strictness
source
@[protected, instance]
meta def tactic.positivity.strictness.has_to_format  :
has_to_format tactic.positivity.strictness
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, nonnegative or non-zero.

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

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

source
inductive tactic.positivity.order_rel  :
Type

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

Instances for tactic.positivity.order_rel
source
@[protected, instance]
def tactic.positivity.order_rel.inhabited  :
inhabited tactic.positivity.order_rel
source
@[protected, instance]
meta def tactic.positivity.order_rel.has_to_format  :
has_to_format tactic.positivity.order_rel
source
@[protected]
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 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
source
meta def tactic.positivity.positivity_fail {α : Type} (e a b : expr) (pa pb : tactic.positivity.strictness) :
tactic α

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 #

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

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

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

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

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

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

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

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

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

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.

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

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), nonnegativity (nonnegative p), or nonzeroness (nonzero p).

source
meta def tactic.interactive.positivity  :
tactic unit

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
```
source
def tactic_doc.tactic.positivity  :
tactic_doc_entry

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 #

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

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/positive/nonzero 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/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.

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

Extension for the positivity tactic: raising a positive number in a canonically ordered semiring gives a positive number.

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

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

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

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.

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

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

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

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

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

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

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

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

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

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