feat: more positivity extensions (#28791)

Add `positivity` extensions for:

- `Nat.gcd`, `Nat.lcm`, `Int.gcd`, `Int.lcm`;
- `Nat.sqrt`, `Nat.totient`.



Co-authored-by: Yury Kudryashov <162619279+yury-harmonic@users.noreply.github.com>

Author: yury-harmonic

Mathlib/Data/Nat/Totient.lean

@@ -370,3 +370,19 @@ theorem totient_mul_of_prime_of_not_dvd {p n : ℕ} (hp : p.Prime) (h : ¬p ∣
   simpa [h] using coprime_or_dvd_of_prime hp n
 
 end Nat
+
+namespace Mathlib.Meta.Positivity
+open Lean Meta Qq
+
+/-- Extension for `Nat.totient`. -/
+@[positivity Nat.totient _]
+def evalNatTotient : PositivityExt where eval {u α} z p e := do
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(Nat.totient $n) =>
+    assumeInstancesCommute
+    match ← core z p n with
+    | .positive pa => return .positive q(Nat.totient_pos.mpr $pa)
+    | _ => failure
+  | _, _, _ => throwError "not Nat.totient"
+
+end Mathlib.Meta.Positivity

Mathlib/Tactic/Positivity/Basic.lean

@@ -443,6 +443,82 @@ def evalAscFactorial : PositivityExt where eval {u α} _ _ e := do
     pure (.positive q(Nat.ascFactorial_pos $n $k))
   | _, _, _ => throwError "failed to match Nat.ascFactorial"
 
+/-- Extension for `Nat.gcd`.
+Uses positivity of the left term, if available, then tries the right term.
+
+The implementation relies on the fact that `Positivity.core` on `ℕ` never returns `nonzero`. -/
+@[positivity Nat.gcd _ _]
+def evalNatGCD : PositivityExt where eval {u α} z p e := do
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(Nat.gcd $a $b) =>
+    assertInstancesCommute
+    match ← core z p a with
+    | .positive pa => return .positive q(Nat.gcd_pos_of_pos_left $b $pa)
+    | _ =>
+      match ← core z p b with
+      | .positive pb => return .positive q(Nat.gcd_pos_of_pos_right $a $pb)
+      | _ => failure
+  | _, _, _ => throwError "not Nat.gcd"
+
+/-- Extension for `Nat.lcm`. -/
+@[positivity Nat.lcm _ _]
+def evalNatLCM : PositivityExt where eval {u α} z p e := do
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(Nat.lcm $a $b) =>
+    assertInstancesCommute
+    match ← core z p a with
+    | .positive pa =>
+      match ← core z p b with
+      | .positive pb =>
+        return .positive q(Nat.lcm_pos $pa $pb)
+      | _ => failure
+    | _ => failure
+  | _, _, _ => throwError "not Nat.lcm"
+
+/-- Extension for `Nat.sqrt`. -/
+@[positivity Nat.sqrt _]
+def evalNatSqrt : PositivityExt where eval {u α} z p e := do
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(Nat.sqrt $n) =>
+    assumeInstancesCommute
+    match ← core z p n with
+    | .positive pa => return .positive q(Nat.sqrt_pos.mpr $pa)
+    | _ => failure
+  | _, _, _ => throwError "not Nat.sqrt"
+
+/-- Extension for `Int.gcd`.
+Uses positivity of the left term, if available, then tries the right term. -/
+@[positivity Int.gcd _ _]
+def evalIntGCD : PositivityExt where eval {u α} _ _ e := do
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(Int.gcd $a $b) =>
+    let z ← synthInstanceQ (q(Zero ℤ) : Q(Type))
+    let p ← synthInstanceQ (q(PartialOrder ℤ) : Q(Type))
+    assertInstancesCommute
+    match (← catchNone (core z p a)).toNonzero with
+    | some na => return .positive q(Int.gcd_pos_of_ne_zero_left $b $na)
+    | none =>
+      match (← core z p b).toNonzero with
+      | some nb => return .positive q(Int.gcd_pos_of_ne_zero_right $a $nb)
+      | none => failure
+  | _, _, _ => throwError "not Int.gcd"
+
+/-- Extension for `Int.lcm`. -/
+@[positivity Int.lcm _ _]
+def evalIntLCM : PositivityExt where eval {u α} _ _ e := do
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(Int.lcm $a $b) =>
+    let z ← synthInstanceQ (q(Zero ℤ) : Q(Type))
+    let p ← synthInstanceQ (q(PartialOrder ℤ) : Q(Type))
+    assertInstancesCommute
+    match (← core z p a).toNonzero with
+    | some na =>
+      match (← core z p b).toNonzero with
+      | some nb => return .positive q(Int.lcm_pos $na $nb)
+      | _ => failure
+    | _ => failure
+  | _, _, _ => throwError "not Int.lcm"
+
 section NNRat
 open NNRat
 

MathlibTest/positivity.lean

@@ -234,6 +234,14 @@ example (hq : 0 ≤ q) : 0 ≤ q.num := by positivity
 
 end
 
+example (a b : ℕ) (ha : a ≠ 0) : 0 < a.gcd b := by positivity
+example (a b : ℤ) (ha : a ≠ 0) : 0 < a.gcd b := by positivity
+example (a b : ℕ) (hb : b ≠ 0) : 0 < a.gcd b := by positivity
+example (a b : ℤ) (hb : b ≠ 0) : 0 < a.gcd b := by positivity
+example (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a.lcm b := by positivity
+example (a b : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a.lcm b := by positivity
+example (a : ℕ) (ha : a ≠ 0) : 0 < a.sqrt := by positivity
+example (a : ℕ) (ha : a ≠ 0) : 0 < a.totient := by positivity
 
 section ENNReal