bestResult — Mathlib

Lean4
/-- 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. -/
def bestResult (e : Expr) : MetaM (Bool × Expr) := do
  let ⟨u, α, _⟩ ← inferTypeQ' e
  let zα ← synthInstanceQ q(Zero $α)
  let pα ← synthInstanceQ q(PartialOrder $α)
  match ← try? (Meta.Positivity.core zα pα e) with
  | some (.positive pf) =>
    pure (true, pf)
  | some (.nonnegative pf) =>
    pure (false, pf)
  | _ =>
    throwError "could not establish the nonnegativity of {e}"
Похожие утверждения