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.
Equations
- Mathlib.Meta.Positivity.instReprQQ = inferInstanceAs (Repr Lean.Expr)
- positive: {u : Lean.Level} → {α : Q(Type u)} → {zα : Q(Zero «$α»)} → {pα : Q(PartialOrder «$α»)} → {e : Q(«$α»)} → Q(0 < «$e») → Mathlib.Meta.Positivity.Strictness zα pα e
- nonnegative: {u : Lean.Level} → {α : Q(Type u)} → {zα : Q(Zero «$α»)} → {pα : Q(PartialOrder «$α»)} → {e : Q(«$α»)} → Q(0 ≤ «$e») → Mathlib.Meta.Positivity.Strictness zα pα e
- nonzero: {u : Lean.Level} → {α : Q(Type u)} → {zα : Q(Zero «$α»)} → {pα : Q(PartialOrder «$α»)} → {e : Q(«$α»)} → Q(«$e» ≠ 0) → Mathlib.Meta.Positivity.Strictness zα pα e
- none: {u : Lean.Level} → {α : Q(Type u)} → {zα : Q(Zero «$α»)} → {pα : Q(PartialOrder «$α»)} → {e : Q(«$α»)} → Mathlib.Meta.Positivity.Strictness zα pα e
The result of positivity running on an expression e of type α.
Instances For
Equations
- Mathlib.Meta.Positivity.instReprStrictness = { reprPrec := Mathlib.Meta.Positivity.reprStrictness✝ }
Gives a generic description of the positivity result.
Equations
- One or more equations did not get rendered due to their size.
Attempts to prove a expression
e : αis>0,≥0≥0, or≠0≠0.eval : {u : Lean.Level} → {α : Q(Type u)} → (zα : Q(Zero «$α»)) → (pα : Q(PartialOrder «$α»)) → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα pα e)
An extension for positivity.
Instances For
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≥ 0 using zero_le in a CanonicallyOrderedAddMonoid.
Equations
- One or more equations did not get rendered due to their size.
A variation on assumption when the hypothesis is lo ≤ e≤ 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 a = b where a 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 [
where a is a numeral.
Equations
- One or more equations did not get rendered due to their size.
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.
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.
The main entry point to the positivity tactic. Given a goal goal of the form 0 [≤/,
attempts to recurse on the structure of e to prove the goal.
It will either close goal or fail.
Equations
- One or more equations did not get rendered due to their size.
Tactic solving goals of the form 0 ≤ x≤ x, 0 < x and x ≠ 0≠ 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
≤ a ^ 3 + a := by positivity
example {a : ℤ} (ha : 1 < a) : 0 < |(3:ℤ) + a| := by positivity
example {b : ℤ} : 0 ≤ max (-3) (b ^ 2) := by positivity
≤ max (-3) (b ^ 2) := by positivity
Equations
- Mathlib.Tactic.Positivity.positivity = Lean.ParserDescr.node `Mathlib.Tactic.Positivity.positivity 1024 (Lean.ParserDescr.nonReservedSymbol "positivity" false)