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(«$α»)} → 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
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.
Extract a proof that e is nonnegative, if possible, from Strictness information about e.
Equations
- One or more equations did not get rendered due to their size.
Extract a proof that e is nonzero, if possible, from Strictness information about e.
Equations
- One or more equations did not get rendered due to their size.
An extension for positivity.
- 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.
Read a positivity extension from a declaration of the right type.
Equations
- One or more equations did not get rendered due to their size.
Configuration for DiscrTree.
Equations
- Mathlib.Meta.Positivity.discrTreeConfig = { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }
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 CanonicallyOrderedAddCommMonoid.
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.
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.
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.
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 (Lean.MVarId.getType' goal) let p ← Mathlib.Meta.Positivity.solve t Lean.MVarId.assign goal 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)