evalAbs — Mathlib

Lean4
/-- The `positivity` extension which identifies expressions of the form `|a|`. -/
@[positivity |_|]
def evalAbs : PositivityExt where
  eval {_u} (α zα pα)
    (e : Q($α)) := do
    let ~q(@abs _ (_) (_) $a) := e |
      throwError"not |·|"
    try
      match ← core zα pα a with
      | .positive pa =>
        let pa' ← mkAppM ``abs_pos_of_pos #[pa]
        pure (.positive pa')
      | .nonzero pa =>
        let pa' ← mkAppM ``abs_pos_of_ne_zero #[pa]
        pure (.positive pa')
      | _ =>
        pure .none
    catch _ =>
      do
        let pa' ← mkAppM ``abs_nonneg #[a]
        pure (.nonnegative pa')
Похожие утверждения