Lean4
/-- Extension for the `positivity` tactic: `Int.cast` is positive (resp. non-negative)
if its input is. -/
@[positivity Int.cast _]
def evalIntCast : PositivityExt where
eval {u α} _zα _pα
e := do
let ~q(@Int.cast _ (_) ($a : ℤ)) := e |
throwError"not Int.cast"
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 =>
let _rα ← synthInstanceQ q(Ring $α)
let _oα ← synthInstanceQ q(IsOrderedRing $α)
let _nt ← synthInstanceQ q(Nontrivial $α)
assumeInstancesCommute
pure (.positive q(Int.cast_pos.mpr $pa))
| .nonnegative pa =>
let _rα ← synthInstanceQ q(Ring $α)
let _oα ← synthInstanceQ q(IsOrderedRing $α)
let _nt ← synthInstanceQ q(Nontrivial $α)
assumeInstancesCommute
pure (.nonnegative q(Int.cast_nonneg.mpr $pa))
| .nonzero pa =>
let _oα ← synthInstanceQ q(AddGroupWithOne $α)
let _nt ← synthInstanceQ q(CharZero $α)
assumeInstancesCommute
pure (.nonzero q(Int.cast_ne_zero.mpr $pa))
| .none =>
pure .none
