Define divides, and add examples

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

src/frontends/lean/lean_notation.cpp

@@ -47,6 +47,7 @@ void init_builtin_notation(frontend & f) {
     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_divides_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());

src/kernel/arith/arith.cpp

@@ -245,6 +245,7 @@ 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_divides_fn, name({"Int", "divides"}));
 MK_CONSTANT(int_ge_fn, name({"Int", "ge"}));
 MK_CONSTANT(int_lt_fn, name({"Int", "lt"}));
 MK_CONSTANT(int_gt_fn, name({"Int", "gt"}));
@@ -459,6 +460,7 @@ void add_arith_theory(environment & env) {
     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_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), mk_int_value(0))));
     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))));

src/kernel/arith/arith.h

@@ -86,6 +86,9 @@ inline expr iDiv(expr const & e1, expr const & e2) { return mk_app(mk_int_div_fn
 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_divides_fn();
+inline expr iDivides(expr const & e1, expr const & e2) { return mk_app(mk_int_divides_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); }
 

tests/lean/arith6.lean

@@ -0,0 +1,12 @@
+Set pp::unicode false
+Show 3 | 6
+Eval 3 | 6
+Eval 3 | 7
+Eval 2 | 6
+Eval 1 | 6
+Variable x : Int
+Eval x | 3
+Eval 3 | x
+Eval 6 | 3
+Set pp::notation false
+Show 3 | x

tests/lean/arith6.lean.expected.out

@@ -0,0 +1,14 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Set: pp::unicode
+3 | 6
+true
+false
+true
+true
+  Assumed: x
+3 + -1 * (x * (3 div x)) = 0
+x + -1 * (3 * (x div 3)) = 0
+false
+  Set: lean::pp::notation
+Int::divides 3 x