positivity

positivity は、0 ≤ x や 0 < x や x ≠ 0 という形のゴールを証明するためのタクティクです。

import Mathlib.Tactic

variable {a b : ℤ}

example (ha : 3 < a) : 0 ≤ a ^ 3 + a := by
  -- linarith では示せない
  fail_if_success linarith

  -- omega でも示せない
  fail_if_success omega

  positivity

example (ha : 1 < a) : 0 < |3 + a| := by
  -- linarith では示せない
  fail_if_success linarith

  -- omega でも示せない
  fail_if_success omega

  positivity

ゴールを構成する式がすべて数値的な下界を持つならば、positivity は再帰的に適用されます。

example : 0 ≤ max (-3) (b ^ 2) := by positivity

example : 0 < max (-3) ((1 + a) ^ 2 + 3) := by positivity

example : 0 < |2 + a| + |3 + b| + |1 + a ^ 2| := by positivity