Define mod and unary minus

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

src/frontends/lean/lean_notation.cpp

@@ -41,8 +41,10 @@ void init_builtin_notation(frontend & f) {
 
     f.add_infixl("+", 65, mk_int_add_fn());
     f.add_infixl("-", 65, mk_int_sub_fn());
+    f.add_prefix("-", 75, mk_int_neg_fn());
     f.add_infixl("*", 70, mk_int_mul_fn());
     f.add_infixl("div", 70, mk_int_div_fn());
+    f.add_infixl("mod", 70, mk_int_mod_fn());
     f.add_infix("<=", 50, mk_int_le_fn());
     f.add_infix("\u2264", 50, mk_int_le_fn());  // ≤
     f.add_infix(">=", 50, mk_int_ge_fn());
@@ -52,6 +54,7 @@ void init_builtin_notation(frontend & f) {
 
     f.add_infixl("+", 65, mk_real_add_fn());
     f.add_infixl("-", 65, mk_real_sub_fn());
+    f.add_prefix("-", 75, mk_real_neg_fn());
     f.add_infixl("*", 70, mk_real_mul_fn());
     f.add_infixl("/", 70, mk_real_div_fn());
     f.add_infix("<=", 50, mk_real_le_fn());

src/kernel/arith/arith.cpp

@@ -203,8 +203,6 @@ struct int_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1
 typedef int_bin_op<int_mul_name, int_mul_eval> int_mul_value;
 MK_BUILTIN(int_mul_fn, int_mul_value);
 
-MK_CONSTANT(int_sub_fn, name({"Int", "sub"}));
-
 constexpr char int_div_name[] = "div";
 struct int_div_eval {
     mpz operator()(mpz const & v1, mpz const & v2) {
@@ -241,6 +239,10 @@ public:
     virtual unsigned hash() const { return m_name.hash(); }
 };
 MK_BUILTIN(int_le_fn, int_le_value);
+
+MK_CONSTANT(int_sub_fn, name({"Int", "sub"}));
+MK_CONSTANT(int_neg_fn, name({"Int", "neg"}));
+MK_CONSTANT(int_mod_fn, name({"Int", "mod"}));
 MK_CONSTANT(int_ge_fn, name({"Int", "ge"}));
 MK_CONSTANT(int_lt_fn, name({"Int", "lt"}));
 MK_CONSTANT(int_gt_fn, name({"Int", "gt"}));
@@ -321,8 +323,6 @@ struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v
 typedef real_bin_op<real_mul_name, real_mul_eval> real_mul_value;
 MK_BUILTIN(real_mul_fn, real_mul_value);
 
-MK_CONSTANT(real_sub_fn, name({"Real", "sub"}));
-
 constexpr char real_div_name[] = "div";
 struct real_div_eval {
     mpq operator()(mpq const & v1, mpq const & v2) {
@@ -359,6 +359,9 @@ public:
     virtual unsigned hash() const { return m_name.hash(); }
 };
 MK_BUILTIN(real_le_fn, real_le_value);
+
+MK_CONSTANT(real_sub_fn, name({"Real", "sub"}));
+MK_CONSTANT(real_neg_fn, name({"Real", "neg"}));
 MK_CONSTANT(real_ge_fn, name({"Real", "ge"}));
 MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
 MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
@@ -424,6 +427,8 @@ void add_arith_theory(environment & env) {
     expr ii_i = Int >> (Int >> Int);
     expr rr_b = Real >> (Real >> Bool);
     expr rr_r = Real >> (Real >> Real);
+    expr i_i  = Int >> Int;
+    expr r_r  = Real >> Real;
     expr x    = Const("x");
     expr y    = Const("y");
 
@@ -432,11 +437,14 @@ void add_arith_theory(environment & env) {
     env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
 
     env.add_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(mk_int_value(-1), y))));
+    env.add_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(mk_int_value(-1), x)));
+    env.add_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y)))));
     env.add_definition(int_ge_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, iLe(y, x)));
     env.add_definition(int_lt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
     env.add_definition(int_gt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
 
     env.add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(mk_real_value(-1), y))));
+    env.add_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(mk_real_value(-1), x)));
     env.add_definition(real_ge_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, rLe(y, x)));
     env.add_definition(real_lt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
     env.add_definition(real_gt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));

src/kernel/arith/arith.h

@@ -60,12 +60,18 @@ inline expr iAdd(expr const & e1, expr const & e2) { return mk_app(mk_int_add_fn
 expr mk_int_sub_fn();
 inline expr iSub(expr const & e1, expr const & e2) { return mk_app(mk_int_sub_fn(), e1, e2); }
 
+expr mk_int_neg_fn();
+inline expr iNeg(expr const & e) { return mk_app(mk_int_neg_fn(), e); }
+
 expr mk_int_mul_fn();
 inline expr iMul(expr const & e1, expr const & e2) { return mk_app(mk_int_mul_fn(), e1, e2); }
 
 expr mk_int_div_fn();
 inline expr iDiv(expr const & e1, expr const & e2) { return mk_app(mk_int_div_fn(), e1, e2); }
 
+expr mk_int_mod_fn();
+inline expr iMod(expr const & e1, expr const & e2) { return mk_app(mk_int_mod_fn(), e1, e2); }
+
 expr mk_int_le_fn();
 inline expr iLe(expr const & e1, expr const & e2) { return mk_app(mk_int_le_fn(), e1, e2); }
 
@@ -98,6 +104,9 @@ inline expr rAdd(expr const & e1, expr const & e2) { return mk_app(mk_real_add_f
 expr mk_real_sub_fn();
 inline expr rSub(expr const & e1, expr const & e2) { return mk_app(mk_real_sub_fn(), e1, e2); }
 
+expr mk_real_neg_fn();
+inline expr rNeg(expr const & e) { return mk_app(mk_real_neg_fn(), e); }
+
 expr mk_real_mul_fn();
 inline expr rMul(expr const & e1, expr const & e2) { return mk_app(mk_real_mul_fn(), e1, e2); }
 

tests/lean/arith3.lean

@@ -0,0 +1,9 @@
+Eval 8 mod 3
+Eval 8 div 4
+Eval 7 div 3
+Eval 7 mod 3
+Show -8 mod 3
+Set lean::pp::notation false
+Show -8 mod 3
+Eval -8 mod 3
+Eval (-8 div 3)*3 + (-8 mod 3)

tests/lean/arith3.lean.expected.out

@@ -0,0 +1,9 @@
+2
+2
+2
+1
+- 8 mod 3
+  Set: lean::pp::notation
+Int::mod (Int::neg 8) 3
+-2
+-8