Lean4
/-- Extension for the `positivity` tactic: `Complex.ofReal` is positive/nonnegative/nonzero if its
input is. -/
@[positivity Complex.ofReal _, Complex.ofReal _]
def evalComplexOfReal : PositivityExt where
eval {u α} _ _
e := do
-- TODO: Can we avoid duplicating the code?
match u, α, e with
| 0, ~q(ℂ), ~q(Complex.ofReal $a) =>
assumeInstancesCommute
match ← core q(inferInstance) q(inferInstance) a with
| .positive pa =>
return .positive q(ofReal_pos $pa)
| .nonnegative pa =>
return .nonnegative q(ofReal_nonneg $pa)
| .nonzero pa =>
return .nonzero q(ofReal_ne_zero_of_ne_zero $pa)
| _ =>
return .none
| 0, ~q(ℂ), ~q(Complex.ofReal $a) =>
assumeInstancesCommute
match ← core q(inferInstance) q(inferInstance) a with
| .positive pa =>
return .positive q(ofReal_pos $pa)
| .nonnegative pa =>
return .nonnegative q(ofReal_nonneg $pa)
| .nonzero pa =>
return .nonzero q(ofReal_ne_zero_of_ne_zero $pa)
| _ =>
return .none
| _, _ =>
throwError"not Complex.ofReal"
