From 3992c4b8f965c81ed2e638a3fbfee85d5460d661 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Sep 2013 20:18:20 -0700 Subject: [PATCH] Define divides, and add examples Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_notation.cpp | 1 + src/kernel/arith/arith.cpp | 2 ++ src/kernel/arith/arith.h | 3 +++ tests/lean/arith6.lean | 12 ++++++++++++ tests/lean/arith6.lean.expected.out | 14 ++++++++++++++ 5 files changed, 32 insertions(+) create mode 100644 tests/lean/arith6.lean create mode 100644 tests/lean/arith6.lean.expected.out diff --git a/src/frontends/lean/lean_notation.cpp b/src/frontends/lean/lean_notation.cpp index d67156cee..b2e61f396 100644 --- a/src/frontends/lean/lean_notation.cpp +++ b/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()); diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp index a8474570c..204984fb2 100644 --- a/src/kernel/arith/arith.cpp +++ b/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)))); diff --git a/src/kernel/arith/arith.h b/src/kernel/arith/arith.h index 050088973..8c1716f9e 100644 --- a/src/kernel/arith/arith.h +++ b/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); } diff --git a/tests/lean/arith6.lean b/tests/lean/arith6.lean new file mode 100644 index 000000000..42798cc1d --- /dev/null +++ b/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 \ No newline at end of file diff --git a/tests/lean/arith6.lean.expected.out b/tests/lean/arith6.lean.expected.out new file mode 100644 index 000000000..37825dc8a --- /dev/null +++ b/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