Add Real arithmetic. Fix elaborator for coercions. Now, two overloads are considered ambiguous if they need the same number of coercions. Improve pretty printer for nest infix operators with same precedence and associativity.

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

src/frontends/lean/lean_elaborator.cpp

@@ -199,52 +199,54 @@ class elaborator::imp {
                 context const & ctx, expr const & src) {
         lean_assert(f_choices.size() == f_choice_types.size());
         buffer<unsigned> good_choices;
+        unsigned best_num_coercions = std::numeric_limits<unsigned>::max();
         unsigned num_choices = f_choices.size();
         unsigned num_args    = args.size();
-        for (unsigned round = 0; round < 2; round++) {
+        // We consider two overloads ambiguous if they need the same number of coercions.
-            // In the first round we only select perfect matches without considering
+        for (unsigned j = 0; j < num_choices; j++) {
-            // overloads. This is the same approach used in C++.
+            expr f_t = f_choice_types[j];
-            // If a perfect match does not exist, then we try again using coercions.
+            unsigned num_coercions = 0; // number of coercions needed by current choice
-            for (unsigned j = 0; j < num_choices; j++) {
+            try {
-                expr f_t = f_choice_types[j];
+                unsigned i = 1;
-                try {
+                for (; i < num_args; i++) {
-                    unsigned i = 1;
+                    f_t = check_pi(f_t, ctx, src, ctx);
-                    for (; i < num_args; i++) {
+                    expr expected = abst_domain(f_t);
-                        f_t = check_pi(f_t, ctx, src, ctx);
+                    expr given    = types[i];
-                        expr expected = abst_domain(f_t);
+                    if (!has_metavar(expected) && !has_metavar(given)) {
-                        expr given    = types[i];
+                        if (is_convertible(expected, given, ctx)) {
-                        if (!has_metavar(expected) && !has_metavar(given)) {
+                            // compatible
-                            if (!is_convertible(expected, given, ctx) &&
+                        } else if (m_frontend.get_coercion(given, expected)) {
-                                // remark, we only consider coercions in the second round
+                            // compatible if using coercion
-                                (round == 0 || !m_frontend.get_coercion(given, expected)))
+                            num_coercions++;
-                                break; // failed to use this overload
+                        } else {
+                            break; // failed
                         }
-                        f_t = instantiate_free_var_mmv(abst_body(f_t), 0, args[i]);
                     }
-                    if (i == num_args) {
+                    f_t = instantiate_free_var_mmv(abst_body(f_t), 0, args[i]);
-                        if (good_choices.empty()) {
-                            // first good choice
-                            args[0]  = f_choices[j];
-                            types[0] = f_choice_types[j];
-                        }
-                        good_choices.push_back(j);
-                    }
-                } catch (exception & ex) {
-                    // candidate failed
-                    // do nothing
                 }
+                if (i == num_args) {
+                    if (num_coercions < best_num_coercions) {
+                        // found best choice
+                        args[0]  = f_choices[j];
+                        types[0] = f_choice_types[j];
+                        good_choices.clear();
+                    }
+                    good_choices.push_back(j);
+                }
+            } catch (exception & ex) {
+                // candidate failed
+                // do nothing
             }
-            if (good_choices.size() == 0) {
+        }
-                // TODO add information to the exception
+        if (good_choices.size() == 0) {
-                if (round == 1)
+            // TODO add information to the exception
-                    throw exception("none of the overloads are good");
+            throw exception("none of the overloads are good");
-            } else if (good_choices.size() == 1) {
+        } else if (good_choices.size() == 1) {
-                // found overload
+            // found overload
-                return;
+            return;
-            } else {
+        } else {
-                // TODO add information to the exception
+            // TODO add information to the exception
-                throw exception("ambiguous overload");
+            throw exception("ambiguous overload");
-            }
         }
     }
 

src/frontends/lean/lean_notation.cpp

@@ -42,7 +42,7 @@ void init_builtin_notation(frontend & f) {
     f.add_infixl("+", 65, mk_int_add_fn());
     f.add_infixl("-", 65, mk_int_sub_fn());
     f.add_infixl("*", 70, mk_int_mul_fn());
-    f.add_infixl("/", 70, mk_int_div_fn());
+    f.add_infixl("div", 70, mk_int_div_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());
@@ -50,7 +50,20 @@ void init_builtin_notation(frontend & f) {
     f.add_infix("<", 50, mk_int_lt_fn());
     f.add_infix(">", 50, mk_int_gt_fn());
 
+    f.add_infixl("+", 65, mk_real_add_fn());
+    f.add_infixl("-", 65, mk_real_sub_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());
+    f.add_infix("\u2264", 50, mk_real_le_fn());  // ≤
+    f.add_infix(">=", 50, mk_real_ge_fn());
+    f.add_infix("\u2265", 50, mk_real_ge_fn());  // ≥
+    f.add_infix("<", 50, mk_real_lt_fn());
+    f.add_infix(">", 50, mk_real_gt_fn());
+
     f.add_coercion(mk_nat_to_int_fn());
+    f.add_coercion(mk_int_to_real_fn());
+    f.add_coercion(mk_nat_to_real_fn());
 
     // implicit arguments for builtin axioms
     f.mark_implicit_arguments(mk_mp_fn(), {true, true, false, false});

src/frontends/lean/lean_parser.cpp

@@ -253,8 +253,9 @@ class parser::imp {
         m_builtins["false"]  = False;
         m_builtins["\u22A4"] = True;
         m_builtins["\u22A5"] = False;
-        m_builtins["Int"]    = Int;
         m_builtins["Nat"]    = Nat;
+        m_builtins["Int"]    = Int;
+        m_builtins["Real"]   = Real;
     }
 
     unsigned parse_unsigned(char const * msg) {

src/frontends/lean/lean_pp.cpp

@@ -169,6 +169,10 @@ class pp_fn {
 
     typedef std::pair<format, unsigned> result;
 
+    bool is_coercion(expr const & e) {
+        return is_app(e) && num_args(e) == 2 && m_frontend.is_coercion(arg(e,0));
+    }
+
     /**
        \brief Return true iff \c e is an atomic operation.
     */
@@ -176,7 +180,12 @@ class pp_fn {
         switch (e.kind()) {
         case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type:
             return true;
-        case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let:
+        case expr_kind::App:
+            if (!m_coercion && is_coercion(e))
+                return is_atomic(arg(e,1));
+            else
+                return false;
+        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let:
             return false;
         }
         return false;
@@ -399,6 +408,22 @@ class pp_fn {
         }
     }
 
+    /**
+       \brief Return true iff the given expression has the given fixity.
+    */
+    bool has_fixity(expr const & e, fixity fx) {
+        operator_info op = get_operator(e);
+        if (op) {
+            return op.get_fixity() == fx;
+        } else if (is_eq(e)) {
+            return fixity::Infix == fx;
+        } else if (is_arrow(e)) {
+            return fixity::Infixr == fx;
+        } else {
+            return false;
+        }
+    }
+
     /**
         \brief Pretty print the child of an infix, prefix, postfix or
         mixfix operator. It will add parethesis when needed.
@@ -418,11 +443,14 @@ class pp_fn {
         \brief Pretty print the child of an associative infix
         operator. It will add parethesis when needed.
     */
-    result pp_infix_child(operator_info const & op, expr const & e, unsigned depth) {
+    result pp_infix_child(operator_info const & op, expr const & e, unsigned depth, fixity fx) {
         if (is_atomic(e)) {
             return pp(e, depth + 1);
         } else {
-            if (op.get_precedence() < get_operator_precedence(e) || op == get_operator(e))
+            unsigned e_prec = get_operator_precedence(e);
+            if (op.get_precedence() < e_prec)
+                return pp(e, depth + 1);
+            else if (op.get_precedence() == e_prec && has_fixity(e, fx))
                 return pp(e, depth + 1);
             else
                 return pp_child_with_paren(e, depth);
@@ -543,7 +571,7 @@ class pp_fn {
        \brief Pretty print an application.
     */
     result pp_app(expr const & e, unsigned depth) {
-        if (!m_coercion && num_args(e) == 2 && m_frontend.is_coercion(arg(e,0)))
+        if (!m_coercion && is_coercion(e))
             return pp(arg(e,1), depth);
         application app(e, *this, m_implict);
         operator_info op;
@@ -556,11 +584,11 @@ class pp_fn {
             case fixity::Infix:
                 return mk_infix(op, pp_mixfix_child(op, app.get_arg(0), depth), pp_mixfix_child(op, app.get_arg(1), depth));
             case fixity::Infixr:
-                return mk_infix(op, pp_mixfix_child(op, app.get_arg(0), depth), pp_infix_child(op, app.get_arg(1), depth));
+                return mk_infix(op, pp_mixfix_child(op, app.get_arg(0), depth), pp_infix_child(op, app.get_arg(1), depth, fixity::Infixr));
             case fixity::Infixl:
-                return mk_infix(op, pp_infix_child(op, app.get_arg(0), depth),  pp_mixfix_child(op, app.get_arg(1), depth));
+                return mk_infix(op, pp_infix_child(op, app.get_arg(0), depth, fixity::Infixl),  pp_mixfix_child(op, app.get_arg(1), depth));
             case fixity::Prefix:
-                p_arg = pp_infix_child(op, app.get_arg(0), depth);
+                p_arg = pp_infix_child(op, app.get_arg(0), depth, fixity::Prefix);
                 sz  = op.get_op_name().size();
                 return mk_result(group(format{format(op.get_op_name()), nest(sz+1, format{line(), p_arg.first})}),
                                  p_arg.second + 1);

src/kernel/arith/arith.cpp

@@ -247,7 +247,131 @@ MK_BUILTIN(int_le_fn, int_le_value);
 MK_CONSTANT(int_ge_fn, name(name("Int"), "ge"));
 MK_CONSTANT(int_lt_fn, name(name("Int"), "lt"));
 MK_CONSTANT(int_gt_fn, name(name("Int"), "gt"));
+// =======================================
 
+// =======================================
+// Reals
+class real_type_value : public num_type_value {
+public:
+    real_type_value():num_type_value("Real") {}
+    virtual bool operator==(value const & other) const { return dynamic_cast<real_type_value const*>(&other) != nullptr; }
+};
+expr const Real = mk_value(*(new real_type_value()));
+expr mk_real_type() { return Real; }
+
+class real_value_value : public value {
+    mpq m_val;
+public:
+    real_value_value(mpq const & v):m_val(v) {}
+    virtual ~real_value_value() {}
+    virtual expr get_type() const { return Real; }
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
+    virtual bool operator==(value const & other) const {
+        real_value_value const * _other = dynamic_cast<real_value_value const*>(&other);
+        return _other && _other->m_val == m_val;
+    }
+    virtual void display(std::ostream & out) const { out << m_val; }
+    virtual format pp() const { return format(m_val); }
+    virtual unsigned hash() const { return m_val.hash(); }
+    mpq const & get_num() const { return m_val; }
+};
+
+expr mk_real_value(mpq const & v) {
+    return mk_value(*(new real_value_value(v)));
+}
+
+bool is_real_value(expr const & e) {
+    return is_value(e) && dynamic_cast<real_value_value const *>(&to_value(e)) != nullptr;
+}
+
+mpq const & real_value_numeral(expr const & e) {
+    lean_assert(is_real_value(e));
+    return static_cast<real_value_value const &>(to_value(e)).get_num();
+}
+
+template<char const * Name, typename F>
+class real_bin_op : public value {
+    expr     m_type;
+    name     m_name;
+public:
+    real_bin_op() {
+        m_type = Real >> (Real >> Real);
+        m_name = name("Real", Name);
+    }
+    virtual ~real_bin_op() {}
+    virtual expr get_type() const { return m_type; }
+    virtual bool operator==(value const & other) const { return dynamic_cast<real_bin_op const*>(&other) != nullptr; }
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
+            r = mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2])));
+            return true;
+        } else {
+            return false;
+        }
+    }
+    virtual void display(std::ostream & out) const { out << m_name; }
+    virtual format pp() const { return format(m_name); }
+    virtual unsigned hash() const { return m_name.hash(); }
+};
+
+constexpr char real_add_name[] = "add";
+struct real_add_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 + v2; }; };
+typedef real_bin_op<real_add_name, real_add_eval> real_add_value;
+MK_BUILTIN(real_add_fn, real_add_value);
+
+constexpr char real_sub_name[] = "sub";
+struct real_sub_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 - v2; }; };
+typedef real_bin_op<real_sub_name, real_sub_eval> real_sub_value;
+MK_BUILTIN(real_sub_fn, real_sub_value);
+
+constexpr char real_mul_name[] = "mul";
+struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 * v2; }; };
+typedef real_bin_op<real_mul_name, real_mul_eval> real_mul_value;
+MK_BUILTIN(real_mul_fn, real_mul_value);
+
+constexpr char real_div_name[] = "div";
+struct real_div_eval {
+    mpq operator()(mpq const & v1, mpq const & v2) {
+        if (v2.is_zero())
+            return v2;
+        else
+            return v1 / v2;
+    };
+};
+typedef real_bin_op<real_div_name, real_div_eval> real_div_value;
+MK_BUILTIN(real_div_fn, real_div_value);
+
+class real_le_value : public value {
+    expr m_type;
+    name m_name;
+public:
+    real_le_value() {
+        m_type = Real >> (Real >> Bool);
+        m_name = name{"Real", "le"};
+    }
+    virtual ~real_le_value() {}
+    virtual expr get_type() const { return m_type; }
+    virtual bool operator==(value const & other) const { return dynamic_cast<real_le_value const*>(&other) != nullptr; }
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
+            r = mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2]));
+            return true;
+        } else {
+            return false;
+        }
+    }
+    virtual void display(std::ostream & out) const { out << m_name; }
+    virtual format pp() const { return format(m_name); }
+    virtual unsigned hash() const { return m_name.hash(); }
+};
+MK_BUILTIN(real_le_fn, real_le_value);
+MK_CONSTANT(real_ge_fn, name(name("Real"), "ge"));
+MK_CONSTANT(real_lt_fn, name(name("Real"), "lt"));
+MK_CONSTANT(real_gt_fn, name(name("Real"), "gt"));
+// =======================================
+
+// =======================================
+// Coercions
 class nat_to_int_value : public value {
     expr m_type;
     name m_name;
@@ -273,11 +397,37 @@ public:
 };
 MK_BUILTIN(nat_to_int_fn, nat_to_int_value);
 
+class int_to_real_value : public value {
+    expr m_type;
+    name m_name;
+public:
+    int_to_real_value() {
+        m_type = Int >> Real;
+        m_name = "int_to_real";
+    }
+    virtual ~int_to_real_value() {}
+    virtual expr get_type() const { return m_type; }
+    virtual bool operator==(value const & other) const { return dynamic_cast<int_to_real_value const*>(&other) != nullptr; }
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 2 && is_int_value(args[1])) {
+            r = mk_real_value(mpq(int_value_numeral(args[1])));
+            return true;
+        } else {
+            return false;
+        }
+    }
+    virtual void display(std::ostream & out) const { out << m_name; }
+    virtual format pp() const { return format(m_name); }
+    virtual unsigned hash() const { return m_name.hash(); }
+};
+MK_BUILTIN(int_to_real_fn,  int_to_real_value);
+MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
 // =======================================
 
-void add_int_theory(environment & env) {
+void add_arith_theory(environment & env) {
-    expr p_ii = Int >> (Int >> Bool);
     expr p_nn = Nat >> (Nat >> Bool);
+    expr p_ii = Int >> (Int >> Bool);
+    expr p_rr = Real >> (Real >> Bool);
     expr x    = Const("x");
     expr y    = Const("y");
 
@@ -288,5 +438,11 @@ void add_int_theory(environment & env) {
     env.add_definition(int_ge_fn_name, p_ii, Fun({{x, Int}, {y, Int}}, iLe(y, x)));
     env.add_definition(int_lt_fn_name, p_ii, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
     env.add_definition(int_gt_fn_name, p_ii, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
+
+    env.add_definition(real_ge_fn_name, p_rr, Fun({{x, Real}, {y, Real}}, rLe(y, x)));
+    env.add_definition(real_lt_fn_name, p_rr, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
+    env.add_definition(real_gt_fn_name, p_rr, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
+
+    env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x))));
 }
 }

src/kernel/arith/arith.h

@@ -11,6 +11,8 @@ Author: Leonardo de Moura
 #include "mpq.h"
 
 namespace lean {
+// =======================================
+// Natural numbers
 expr mk_nat_type();
 extern expr const Nat;
 
@@ -39,7 +41,10 @@ expr mk_nat_gt_fn();
 inline expr nGt(expr const & e1, expr const & e2) { return mk_app(mk_nat_gt_fn(), e1, e2); }
 
 inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(Nat, c, t, e); }
+// =======================================
 
+// =======================================
+// Integers
 expr mk_int_type();
 extern expr const Int;
 
@@ -74,10 +79,56 @@ expr mk_int_gt_fn();
 inline expr iGt(expr const & e1, expr const & e2) { return mk_app(mk_int_gt_fn(), e1, e2); }
 
 inline expr iIf(expr const & c, expr const & t, expr const & e) { return mk_if(Int, c, t, e); }
+// =======================================
 
+// =======================================
+// Reals
+expr mk_real_type();
+extern expr const Real;
+
+expr mk_real_value(mpq const & v);
+inline expr mk_real_value(int v) { return mk_real_value(mpq(v)); }
+inline expr rVal(int v) { return mk_real_value(v); }
+bool is_real_value(expr const & e);
+mpq const & real_value_numeral(expr const & e);
+
+expr mk_real_add_fn();
+inline expr rAdd(expr const & e1, expr const & e2) { return mk_app(mk_real_add_fn(), e1, e2); }
+
+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_mul_fn();
+inline expr rMul(expr const & e1, expr const & e2) { return mk_app(mk_real_mul_fn(), e1, e2); }
+
+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_le_fn();
+inline expr rLe(expr const & e1, expr const & e2) { return mk_app(mk_real_le_fn(), e1, e2); }
+
+expr mk_real_ge_fn();
+inline expr rGe(expr const & e1, expr const & e2) { return mk_app(mk_real_ge_fn(), e1, e2); }
+
+expr mk_real_lt_fn();
+inline expr rLt(expr const & e1, expr const & e2) { return mk_app(mk_real_lt_fn(), e1, e2); }
+
+expr mk_real_gt_fn();
+inline expr rGt(expr const & e1, expr const & e2) { return mk_app(mk_real_gt_fn(), e1, e2); }
+
+inline expr rIf(expr const & c, expr const & t, expr const & e) { return mk_if(Real, c, t, e); }
+// =======================================
+
+// =======================================
+// Coercions
 expr mk_nat_to_int_fn();
 inline expr n2i(expr const & e) { return mk_app(mk_nat_to_int_fn(), e); }
+expr mk_int_to_real_fn();
+inline expr i2r(expr const & e) { return mk_app(mk_int_to_real_fn(), e); }
+expr mk_nat_to_real_fn();
+inline expr n2r(expr const & e) { return mk_app(mk_nat_to_real_fn(), e); }
+// =======================================
 
 class environment;
-void add_int_theory(environment & env);
+void add_arith_theory(environment & env);
 }

src/library/toplevel.cpp

@@ -13,7 +13,7 @@ namespace lean {
 void init_toplevel(environment & env) {
     add_basic_theory(env);
     add_basic_thms(env);
-    add_int_theory(env);
+    add_arith_theory(env);
 }
 environment mk_toplevel() {
     environment r;

tests/lean/arith2.lean

@@ -0,0 +1,14 @@
+Show 1/2
+Eval 4/6
+Show 3 div 2
+Variable x : Real
+Variable i : Int
+Variable n : Nat
+Show x + i + 1 + n
+Set lean::pp::coercion true
+Show x + i + 1 + n
+Show x * i + x
+Show x - i + x - x >= 0
+Show x < x
+Show x <= x
+Show x > x

tests/lean/arith2.lean.expected.out

@@ -0,0 +1,14 @@
+1 / 2
+2/3
+3 div 2
+  Assumed: x
+  Assumed: i
+  Assumed: n
+x + i + 1 + n
+  Set: lean::pp::coercion
+x + (int_to_real i) + (nat_to_real 1) + (nat_to_real n)
+x * (int_to_real i) + x
+x - (int_to_real i) + x - x ≥ (nat_to_real 0)
+x < x
+x ≤ x
+x > x