The bound attribute

Any lemma tagged with @[bound] is registered as an apply rule for the bound tactic, by converting it to either norm apply or safe apply <priority>. The classification is based on the number and types of the lemma's hypotheses.

def Mathlib.Tactic.Bound.isZero {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) : Lean.MetaM Bool

Check if an expression is zero

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Bound.ineqPriority {u : Lean.Level} {α : Q(Type u)} (a : Q(«$α»)) (b : Q(«$α»)) : Lean.MetaM ℕ

Map the arguments of an inequality expression to a score

Equations

• One or more equations did not get rendered due to their size.

partial def Mathlib.Tactic.Bound.hypPriority (hyp : Q(Prop)) : Lean.MetaM ℕ

Map a hypothesis type to a score

def Mathlib.Tactic.Bound.typePriority (decl : Lean.Name) (type : Lean.Expr) : Lean.MetaM ℕ

Map a type to a score

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Bound.typePriority.argPriority (x : Lean.Expr) : Lean.MetaM ℕ

Score the type of argument x

Equations

• Mathlib.Tactic.Bound.typePriority.argPriority x = do let __do_lift ← Lean.Meta.inferType x Mathlib.Tactic.Bound.hypPriority __do_lift

def Mathlib.Tactic.Bound.typePriority.checkResult (decl : Lean.Name) (type : Lean.Expr) (t : Q(Prop)) : Lean.MetaM Unit

Insist that our conclusion is an inequality

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Bound.declPriority (decl : Lean.Name) : Lean.MetaM ℕ

Map a theorem decl to a score (0 means norm apply, 0 < means safe apply)

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Bound.scoreToConfig (decl : Lean.Name) (score : ℕ) : Aesop.Frontend.RuleConfig

Map a score to either norm apply or safe apply <priority>

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Bound.attrBound_forward : Lean.ParserDescr

Attribute for forward rules for the bound tactic.

@[bound_forward] lemmas should produce inequalities given other hypotheses that might be in the context. A typical example is exposing an inequality field of a structure, such as HasPowerSeriesOnBall.r_pos.

Equations

• Mathlib.Tactic.Bound.attrBound_forward = Lean.ParserDescr.node `Mathlib.Tactic.Bound.attrBound_forward 1024 (Lean.ParserDescr.nonReservedSymbol "bound_forward" false)