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.
Attribute for identifying positivity extensions.
Equations
- One or more equations did not get rendered due to their size.
The result of positivity running on an expression e of type α.
- positive {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} (pf : Q(0 < «$e»)) : Strictness zα pα e
- nonnegative {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} (pf : Q(0 ≤ «$e»)) : Strictness zα pα e
- nonzero {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} (pf : Q(«$e» ≠ 0)) : Strictness zα pα e
- none {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {pα : Q(PartialOrder «$α»)} {e : Q(«$α»)} : Strictness zα pα e
Equations
Gives a generic description of the positivity result.
Equations
- Mathlib.Meta.Positivity.Strictness.toString zα pα (Mathlib.Meta.Positivity.Strictness.positive a) = "positive"
- Mathlib.Meta.Positivity.Strictness.toString zα pα (Mathlib.Meta.Positivity.Strictness.nonnegative a) = "nonnegative"
- Mathlib.Meta.Positivity.Strictness.toString zα pα (Mathlib.Meta.Positivity.Strictness.nonzero a) = "nonzero"
- Mathlib.Meta.Positivity.Strictness.toString zα pα Mathlib.Meta.Positivity.Strictness.none = "none"
Extract a proof that e is nonnegative, if possible, from Strictness information about e.
Extract a proof that e is nonzero, if possible, from Strictness information about e.
An extension for positivity.
- eval {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (pα : Q(PartialOrder «$α»)) (e : Q(«$α»)) : Lean.MetaM (Strictness zα pα e)
Attempts to prove an expression
e : αis>0,≥0, or≠0.
Read a positivity extension from a declaration of the right type.
Equations
- One or more equations did not get rendered due to their size.
Each positivity extension is labelled with a collection of patterns
which determine the expressions to which it should be applied.
Equations
Environment extensions for positivity declarations
Converts a MetaM Strictness which can fail
into one that never fails and returns .none instead.
Equations
- One or more equations did not get rendered due to their size.
Converts a MetaM Strictness which can return .none
into one which never returns .none but fails instead.
Equations
- Mathlib.Meta.Positivity.throwNone t = do let __do_lift ← t match __do_lift with | Mathlib.Meta.Positivity.Strictness.none => failure | r => pure r
Attempts to prove a Strictness result when e evaluates to a literal number.
Equations
- One or more equations did not get rendered due to their size.
Attempts to prove that e ≥ 0 using zero_le in a CanonicallyOrderedAdd monoid.
Equations
- One or more equations did not get rendered due to their size.
A variation on assumption when the hypothesis is lo ≤ e where lo is a numeral.
Equations
- One or more equations did not get rendered due to their size.
A variation on assumption when the hypothesis is lo < e where lo is a numeral.
Equations
- One or more equations did not get rendered due to their size.
A variation on assumption when the hypothesis is x = e where x is a numeral.
Equations
- One or more equations did not get rendered due to their size.
A variation on assumption which checks if the hypothesis ldecl is a [</≤/=] e
where a is a numeral.
The main combinator which combines multiple positivity results.
It assumes t₁ has already been run for a result, and runs t₂ and takes the best result.
It will skip t₂ if t₁ is already a proof of .positive, and can also combine
.nonnegative and .nonzero to produce a .positive result.
Equations
- One or more equations did not get rendered due to their size.
- Mathlib.Meta.Positivity.orElse Mathlib.Meta.Positivity.Strictness.none t₂ = Mathlib.Meta.Positivity.catchNone t₂
- Mathlib.Meta.Positivity.orElse (Mathlib.Meta.Positivity.Strictness.positive pf) t₂ = pure (Mathlib.Meta.Positivity.Strictness.positive pf)
Run each registered positivity extension on an expression, returning a NormNum.Result.
Equations
- One or more equations did not get rendered due to their size.
Given an expression e, use the core method of the positivity tactic to prove it positive,
or, failing that, nonnegative; return a boolean (signalling whether the strict or non-strict
inequality was established) together with the proof as an expression.
Equations
- One or more equations did not get rendered due to their size.
Given an expression e, use the core method of the positivity tactic to prove it nonnegative.
Equations
- One or more equations did not get rendered due to their size.
An auxiliary 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.
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.
Equations
- Mathlib.Meta.Positivity.positivity goal = do let t ← Lean.Meta.withReducible goal.getType' let p ← Mathlib.Meta.Positivity.solve t goal.assign 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
Equations
- Mathlib.Tactic.Positivity.positivity = Lean.ParserDescr.node `Mathlib.Tactic.Positivity.positivity 1024 (Lean.ParserDescr.nonReservedSymbol "positivity" false)