From fc9e3958186ebfa876edca456712c813be5a5a56 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Sep 2013 20:39:54 -0700 Subject: [PATCH] Define absolute value function and notation for it. Add new example. Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_frontend.h | 4 ++++ src/frontends/lean/lean_notation.cpp | 3 +++ src/kernel/arith/arith.cpp | 34 ++++++++++++++++------------ src/kernel/arith/arith.h | 9 ++++++++ tests/lean/arith7.lean | 16 +++++++++++++ tests/lean/arith7.lean.expected.out | 13 +++++++++++ 6 files changed, 65 insertions(+), 14 deletions(-) create mode 100644 tests/lean/arith7.lean create mode 100644 tests/lean/arith7.lean.expected.out diff --git a/src/frontends/lean/lean_frontend.h b/src/frontends/lean/lean_frontend.h index 12ae8ebdd..7e63bfb4f 100644 --- a/src/frontends/lean/lean_frontend.h +++ b/src/frontends/lean/lean_frontend.h @@ -85,6 +85,10 @@ public: void add_mixfixr(unsigned sz, name const * opns, unsigned precedence, expr const & d); void add_mixfixc(unsigned sz, name const * opns, unsigned precedence, expr const & d); void add_mixfixo(unsigned sz, name const * opns, unsigned precedence, expr const & d); + void add_mixfixl(std::initializer_list const & l, unsigned p, expr const & d) { add_mixfixl(l.size(), l.begin(), p, d); } + void add_mixfixr(std::initializer_list const & l, unsigned p, expr const & d) { add_mixfixr(l.size(), l.begin(), p, d); } + void add_mixfixc(std::initializer_list const & l, unsigned p, expr const & d) { add_mixfixc(l.size(), l.begin(), p, d); } + void add_mixfixo(std::initializer_list const & l, unsigned p, expr const & d) { add_mixfixo(l.size(), l.begin(), p, d); } /** \brief Return the operator (if one exists) associated with the given expression. diff --git a/src/frontends/lean/lean_notation.cpp b/src/frontends/lean/lean_notation.cpp index b2e61f396..272e45d55 100644 --- a/src/frontends/lean/lean_notation.cpp +++ b/src/frontends/lean/lean_notation.cpp @@ -40,6 +40,7 @@ void init_builtin_notation(frontend & f) { f.add_infix("\u2265", 50, mk_nat_ge_fn()); // ≥ f.add_infix("<", 50, mk_nat_lt_fn()); f.add_infix(">", 50, mk_nat_gt_fn()); + f.add_mixfixc({"|","|"}, 55, mk_nat_id_fn()); // absolute value for naturals is the identity function f.add_infixl("+", 65, mk_int_add_fn()); f.add_infixl("-", 65, mk_int_sub_fn()); @@ -48,6 +49,7 @@ void init_builtin_notation(frontend & f) { 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_mixfixc({"|","|"}, 55, mk_int_abs_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()); @@ -60,6 +62,7 @@ void init_builtin_notation(frontend & f) { 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_mixfixc({"|","|"}, 55, mk_real_abs_fn()); f.add_infix("<=", 50, mk_real_le_fn()); f.add_infix("\u2264", 50, mk_real_le_fn()); // ≤ f.add_infix(">=", 50, mk_real_ge_fn()); diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp index 204984fb2..5796211e1 100644 --- a/src/kernel/arith/arith.cpp +++ b/src/kernel/arith/arith.cpp @@ -128,6 +128,7 @@ MK_CONSTANT(nat_lt_fn, name({"Nat", "lt"})); MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"})); MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"})); MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"})); +MK_CONSTANT(nat_id_fn, name({"Nat", "id"})); // ======================================= // ======================================= @@ -246,6 +247,7 @@ 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_abs_fn, name({"Int", "abs"})); MK_CONSTANT(int_ge_fn, name({"Int", "ge"})); MK_CONSTANT(int_lt_fn, name({"Int", "lt"})); MK_CONSTANT(int_gt_fn, name({"Int", "gt"})); @@ -365,6 +367,7 @@ 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_abs_fn, name({"Real", "abs"})); MK_CONSTANT(real_ge_fn, name({"Real", "ge"})); MK_CONSTANT(real_lt_fn, name({"Real", "lt"})); MK_CONSTANT(real_gt_fn, name({"Real", "gt"})); @@ -456,20 +459,23 @@ void add_arith_theory(environment & env) { env.add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x))); env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x)))); env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y)))); + env.add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x)); - 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_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y)))); + env.add_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-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_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(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)))); + env.add_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x)))); env.add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y)))); env.add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x)))); - 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_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y)))); + env.add_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(rVal(-1), x))); + env.add_definition(real_abs_fn_name, r_r, Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(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)))); @@ -480,20 +486,20 @@ void add_arith_theory(environment & env) { env.add_var(real_pi_name, Real); env.add_definition(name("pi"), Real, mk_real_pi()); // alias for pi env.add_var(sin_fn_name, r_r); - env.add_definition(cos_fn_name, r_r, Fun({x,Real}, Sin(rSub(x, rDiv(mk_real_pi(), mk_real_value(2)))))); + env.add_definition(cos_fn_name, r_r, Fun({x,Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2)))))); env.add_definition(tan_fn_name, r_r, Fun({x,Real}, rDiv(Sin(x), Cos(x)))); env.add_definition(cot_fn_name, r_r, Fun({x,Real}, rDiv(Cos(x), Sin(x)))); - env.add_definition(sec_fn_name, r_r, Fun({x,Real}, rDiv(mk_real_value(1), Cos(x)))); - env.add_definition(csc_fn_name, r_r, Fun({x,Real}, rDiv(mk_real_value(1), Sin(x)))); + env.add_definition(sec_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cos(x)))); + env.add_definition(csc_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sin(x)))); - env.add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(mk_real_value(1), Exp(rMul(mk_real_value(-2), x))), - rMul(mk_real_value(2), Exp(rNeg(x)))))); - env.add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(mk_real_value(1), Exp(rMul(mk_real_value(-2), x))), - rMul(mk_real_value(2), Exp(rNeg(x)))))); + env.add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))), + rMul(rVal(2), Exp(rNeg(x)))))); + env.add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))), + rMul(rVal(2), Exp(rNeg(x)))))); env.add_definition(tanh_fn_name, r_r, Fun({x,Real}, rDiv(Sinh(x), Cosh(x)))); env.add_definition(coth_fn_name, r_r, Fun({x,Real}, rDiv(Cosh(x), Sinh(x)))); - env.add_definition(sech_fn_name, r_r, Fun({x,Real}, rDiv(mk_real_value(1), Cosh(x)))); - env.add_definition(csch_fn_name, r_r, Fun({x,Real}, rDiv(mk_real_value(1), Sinh(x)))); + env.add_definition(sech_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cosh(x)))); + env.add_definition(csch_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sinh(x)))); env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x)))); } diff --git a/src/kernel/arith/arith.h b/src/kernel/arith/arith.h index 8c1716f9e..efd5938df 100644 --- a/src/kernel/arith/arith.h +++ b/src/kernel/arith/arith.h @@ -54,6 +54,9 @@ inline expr nLt(expr const & e1, expr const & e2) { return mk_app(mk_nat_lt_fn() expr mk_nat_gt_fn(); inline expr nGt(expr const & e1, expr const & e2) { return mk_app(mk_nat_gt_fn(), e1, e2); } +expr mk_nat_id_fn(); +inline expr nId(expr const & e) { return mk_app(mk_nat_id_fn(), e); } + inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(Nat, c, t, e); } // ======================================= @@ -89,6 +92,9 @@ inline expr iMod(expr const & e1, expr const & e2) { return mk_app(mk_int_mod_fn 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_abs_fn(); +inline expr iAbs(expr const & e) { return mk_app(mk_int_abs_fn(), e); } + expr mk_int_le_fn(); inline expr iLe(expr const & e1, expr const & e2) { return mk_app(mk_int_le_fn(), e1, e2); } @@ -130,6 +136,9 @@ inline expr rMul(expr const & e1, expr const & e2) { return mk_app(mk_real_mul_f expr mk_real_div_fn(); inline expr rDiv(expr const & e1, expr const & e2) { return mk_app(mk_real_div_fn(), e1, e2); } +expr mk_real_abs_fn(); +inline expr rAbs(expr const & e) { return mk_app(mk_real_abs_fn(), e); } + expr mk_real_le_fn(); inline expr rLe(expr const & e1, expr const & e2) { return mk_app(mk_real_le_fn(), e1, e2); } diff --git a/tests/lean/arith7.lean b/tests/lean/arith7.lean new file mode 100644 index 000000000..e4485dac3 --- /dev/null +++ b/tests/lean/arith7.lean @@ -0,0 +1,16 @@ +Eval | -2 | +(* + Unfortunately, we can't write |-2|, because |- is considered a single token. + It is not wise to change that since the symbol |- can be used as the notation for + entailment relation in Lean. +*) +Eval |3| +Definition x : Int := -3 +Eval |x + 1| +Eval |x + 1| > 0 +Variable y : Int +Eval |x + y| +Show |x + y| > x +Set pp::notation false +Show |x + y| > x +Show |x + y| + |y + x| > x \ No newline at end of file diff --git a/tests/lean/arith7.lean.expected.out b/tests/lean/arith7.lean.expected.out new file mode 100644 index 000000000..db3d0aa9e --- /dev/null +++ b/tests/lean/arith7.lean.expected.out @@ -0,0 +1,13 @@ + Set: pp::colors + Set: pp::unicode +2 +3 + Defined: x +2 +⊤ + Assumed: y +ite Int (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y)) +| x + y | > x + Set: lean::pp::notation +Int::gt (Int::abs (Int::add x y)) x +Int::gt (Int::add (Int::abs (Int::add x y)) (Int::abs (Int::add y x))) x