positivity
core functionality #
This file sets up the positivity
tactic and the @[positivity]
attribute,
which allow for plugging in new positivity functionality around a positivity-based driver.
The actual behavior is in @[positivity]
-tagged definitions in Tactic.Positivity.Basic
and elsewhere.
- eval : {u : Lean.Level} → {α : Q(Type u)} → (zα : Q(Zero «$α»)) → (pα : Q(PartialOrder «$α»)) → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα pα e)
Attempts to prove an expression
e : α
is>0
,≥0
, or≠0
.
An extension for positivity
.
Instances For
Read a positivity
extension from a declaration of the right type.
Instances For
Each positivity
extension is labelled with a collection of patterns
which determine the expressions to which it should be applied.
Instances For
Environment extensions for positivity
declarations
An auxillary entry point to the positivity
tactic. Given a proposition t
of the form
0 [≤/≠] e
, attempts to recurse on the structure of t
to prove it. It returns a proof
or fails.
Instances For
The main entry point to the positivity
tactic. Given a goal goal
of the form 0 [≤/≠] e
,
attempts to recurse on the structure of e
to prove the goal.
It will either close goal
or fail.
Instances For
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