Lean4
/-- Extension for the `positivity` tactic: `Nat.cast` is always non-negative,
and positive when its input is. -/
@[positivity Nat.cast _]
def evalNatCast : PositivityExt where
eval {u α} _zα _pα
e := do
let ~q(@Nat.cast _ (_) ($a : ℕ)) := e |
throwError"not Nat.cast"
let zα' : Q(Zero Nat) := q(inferInstance)
let pα' : Q(PartialOrder Nat) := q(inferInstance)
let (_i1 : Q(AddMonoidWithOne $α)) ← synthInstanceQ q(AddMonoidWithOne $α)
let (_i2 : Q(AddLeftMono $α)) ← synthInstanceQ q(AddLeftMono $α)
let (_i3 : Q(ZeroLEOneClass $α)) ← synthInstanceQ q(ZeroLEOneClass $α)
assumeInstancesCommute
match ← core zα' pα' a with
| .positive pa =>
let _nz ← synthInstanceQ q(NeZero (1 : $α))
pure (.positive q(Nat.cast_pos'.2 $pa))
| _ =>
pure (.nonnegative q(Nat.cast_nonneg' _))
