Lean4
/-- Extension for the `positivity` tactic: `Int.natAbs` is positive when its input is.
Since the output type of `Int.natAbs` is `ℕ`, the nonnegative case is handled by the default
`positivity` tactic.
-/
@[positivity Int.natAbs _]
def evalNatAbs : PositivityExt where
eval {u α} _zα _pα
e := do
match u, α, e with
| 0, ~q(ℕ), ~q(Int.natAbs $a) =>
let zα' : Q(Zero Int) := q(inferInstance)
let pα' : Q(PartialOrder Int) := q(inferInstance)
let ra ← core zα' pα' a
match ra with
| .positive pa =>
assertInstancesCommute
pure (.positive q(int_natAbs_pos $pa))
| .nonzero pa =>
assertInstancesCommute
pure (.positive q(Int.natAbs_pos.mpr $pa))
| .nonnegative _pa =>
pure .none
| .none =>
pure .none
| _, _, _ =>
throwError"not Int.natAbs"
