The interval tactic

interval attempts to prove real inequalities between constant expressions by lifting the expressions from ℝ to Interval.

Warning: We use native_decide, so you must trust the compiler.

inductive IntervalTactic.Ineq : Type

• lt : Ineq
• le : Ineq
• gt : Ineq
• ge : Ineq

structure IntervalTactic.Goal : Type

• op : Ineq
• x : Q(Interval)
• y : Q(Interval)

def IntervalTactic.Ineq.str : Ineq → String

Equations

• IntervalTactic.Ineq.lt.str = "<"
• IntervalTactic.Ineq.le.str = "≤"
• IntervalTactic.Ineq.gt.str = ">"
• IntervalTactic.Ineq.ge.str = "≥"

partial def IntervalTactic.lift (e : Q(ℝ)) : Lean.MetaM Q(Interval)

def IntervalTactic.liftGoal (p : Q(Prop)) : Lean.MetaM Goal

Equations

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

def IntervalTactic.Goal.app (g : Goal) : Lean.Expr

Turn a real inequality goal into an Interval goal

Equations

• { op := IntervalTactic.Ineq.lt, x := x, y := y }.app = q(⋯)
• { op := IntervalTactic.Ineq.le, x := x, y := y }.app = q(⋯)
• { op := IntervalTactic.Ineq.gt, x := x, y := y }.app = q(⋯)
• { op := IntervalTactic.Ineq.ge, x := x, y := y }.app = q(⋯)

def IntervalTactic.Ineq.eval (op : Ineq) (x y : Interval) : Bool

Evaluate whether an inequality is known between explicit Intervals

Equations

• IntervalTactic.Ineq.lt.eval x y = decide (x < y)
• IntervalTactic.Ineq.le.eval x y = decide (x ≤ y)
• IntervalTactic.Ineq.gt.eval x y = decide (y < x)
• IntervalTactic.Ineq.ge.eval x y = decide (y ≤ x)

def IntervalTactic.close (g : Lean.MVarId) (tac : Lean.Syntax) : Lean.Elab.Tactic.TacticM Unit

Close a goal using a tactic

Equations

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

instance IntervalTactic.instToMessageDataIneq : Lean.ToMessageData Ineq

Delegate toMessageData to str for Ineq

Equations

• IntervalTactic.instToMessageDataIneq = { toMessageData := fun (i : IntervalTactic.Ineq) => (Lean.MessageData.ofFormat ∘ Std.format) i.str }

@[irreducible]

def Interval.toMessageData (x : Interval) : Lean.MessageData

Necessary to avoid kernel errors for some reason

Equations

• x.toMessageData = Lean.MessageData.ofFormat (repr x)

instance IntervalTactic.instToMessageDataInterval : Lean.ToMessageData Interval

Delegate toMessageData to repr for Interval

Equations

• IntervalTactic.instToMessageDataInterval = { toMessageData := fun (x : Interval) => x.toMessageData }

unsafe def IntervalTactic.eval (x : Q(Interval)) : Lean.MetaM Interval

Unsafe native evaluation of interval expressions

Equations

• IntervalTactic.eval x = Lean.Meta.evalExpr Interval q(Interval) x

def IntervalTactic.tacticInterval : Lean.ParserDescr

Prove a real inequality by lifting from ℝ to Interval. Warning: We use native_decide, so you must trust the compiler.

Equations

• IntervalTactic.tacticInterval = Lean.ParserDescr.node `IntervalTactic.tacticInterval 1024 (Lean.ParserDescr.nonReservedSymbol "interval" false)