feat(tactic/positivity): Extension for int.nat_abs (#16787)

Add `positivity_nat_abs`, a positivity extension for `int.nat_abs`.

src/tactic/positivity.lean

@@ -413,6 +413,21 @@ meta def positivity_abs : expr → tactic strictness
   nonnegative <$> mk_app ``abs_nonneg [a] -- else report nonnegativity
 | _ := failed
 
+private lemma int_nat_abs_pos {n : ℤ} (hn : 0 < n) : 0 < n.nat_abs :=
+int.nat_abs_pos_of_ne_zero hn.ne'
+
+/-- Extension for the `positivity` tactic: `int.nat_abs` is positive when its input is.
+
+Since the output type of `int.nat_abs` is `ℕ`, the nonnegative case is handled by the default
+`positivity` tactic.
+-/
+@[positivity]
+meta def positivity_nat_abs : expr → tactic strictness
+| `(int.nat_abs %%a) := do
+    positive p ← core a,
+    positive <$> mk_app ``int_nat_abs_pos [p]
+| _ := failed
+
 private lemma nat_cast_pos [ordered_semiring α] [nontrivial α] {n : ℕ} : 0 < n → 0 < (n : α) :=
 nat.cast_pos.2
 

test/positivity.lean

@@ -105,6 +105,8 @@ example {a : ℤ} : 0 ≤ |a| := by positivity
 
 example {a : ℤ} : 0 < |a| + 3 := by positivity
 
+example {n : ℤ} (hn : 0 < n) : 0 < n.nat_abs := by positivity
+
 example {a : ℤ} (ha : 1 < a) : 0 < |(3:ℤ) + a| := by positivity
 
 example {a : ℝ} (ha : 0 ≤ a) : 0 ≤ real.sqrt a := by positivity