feat(numerics/zpz): add numeric_traits for zpz numerals

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/util/numerics/power.h

@@ -12,8 +12,9 @@ namespace lean {
 template<typename T>
 T power(T const & a, unsigned k) {
     unsigned mask = 1;
-    T power = a;
+    T power(a);
-    T b     = 1;
+    T b(a);
+    b = 1;
     while (mask <= k) {
         if (mask & k)
             b *= power;

src/util/numerics/zpz.cpp

@@ -18,4 +18,9 @@ void zpz::inv() {
     gcdext(g, a, b, static_cast<int64>(m_value), static_cast<int64>(m_p));
     m_value = remainder(a, static_cast<int64>(m_p));
 }
+
+static zpz g_zero;
+zpz const & numeric_traits<zpz>::zero() {
+    return g_zero;
+}
 }

src/util/numerics/zpz.h

@@ -9,6 +9,8 @@ Author: Leonardo de Moura
 #include "util/int64.h"
 #include "util/numerics/remainder.h"
 #include "util/numerics/primes.h"
+#include "util/numerics/power.h"
+#include "util/numerics/numeric_traits.h"
 
 namespace lean {
 /**
@@ -98,4 +100,19 @@ public:
 
     friend std::ostream & operator<<(std::ostream & out, zpz const & z) { out << z.m_value; return out; }
 };
+
+template<>
+class numeric_traits<zpz> {
+public:
+    static bool precise() { return true; }
+    static bool is_zero(zpz const & v) { return v == 0; }
+    static bool is_pos(zpz const & v)  { return v > 0; }
+    static bool is_neg(zpz const & )  { return false; }
+    static void set_rounding(bool ) {}
+    static void neg(zpz & v)   { v.neg(); }
+    static void reset(zpz & v) { v = 0; }
+    // v <- v^k
+    static void power(zpz & v, unsigned k) { v = lean::power(v, k); }
+    static zpz const & zero();
+};
 }