Add helper functions for creating Let expressions. Add simple type checking test for Let expressions.

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

src/kernel/abstract.cpp

@@ -40,24 +40,19 @@ expr abstract_p(expr const & e, unsigned n, expr const * s) {
 
     return replace_fn<decltype(f)>(f)(e);
 }
-expr Fun(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b) {
-    expr r = b;
-    auto it = l.end();
-    while (it != l.begin()) {
-        --it;
-        auto const & p = *it;
-        r = Fun(p.first, p.second, r);
-    }
-    return r;
-}
-expr Pi(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b) {
-    expr r = b;
-    auto it = l.end();
-    while (it != l.begin()) {
-        --it;
-        auto const & p = *it;
-        r = Pi(p.first, p.second, r);
-    }
-    return r;
+#define MkBinder(FName)                                                 \
+expr FName(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b) { \
+    expr r = b;                                                         \
+    auto it = l.end();                                                  \
+    while (it != l.begin()) {                                           \
+        --it;                                                           \
+        auto const & p = *it;                                           \
+        r = FName(p.first, p.second, r);                                \
+    }                                                                   \
+    return r;                                                           \
 }
+
+MkBinder(Fun);
+MkBinder(Pi);
+MkBinder(Let);
 }

src/kernel/abstract.h

@@ -43,4 +43,12 @@ inline expr Pi(name const & n, expr const & t, expr const & b) { return mk_pi(n,
 inline expr Pi(expr const & n, expr const & t, expr const & b) { return mk_pi(const_name(n), t, abstract(b, n)); }
 inline expr Pi(std::pair<expr const &, expr const &> const & p, expr const & b) { return Pi(p.first, p.second, b); }
        expr Pi(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
+
+/**
+   \brief Create a Let expression (Let x := v in b), the term b is abstracted using abstract(b, x).
+*/
+inline expr Let(name const & x, expr const & v, expr const & b) { return mk_let(x, v, abstract(b, mk_constant(x))); }
+inline expr Let(expr const & x, expr const & v, expr const & b) { return mk_let(const_name(x), v, abstract(b, x)); }
+inline expr Let(std::pair<expr const &, expr const &> const & p, expr const & b) { return Let(p.first, p.second, b); }
+       expr Let(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
 }

src/kernel/expr.h

@@ -275,7 +275,6 @@ inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(
 inline expr arrow(expr const & t, expr const & e) { return mk_pi(name("_"), t, e); }
 inline expr operator>>(expr const & t, expr const & e) { return arrow(t, e); }
 inline expr mk_let(name const & n, expr const & v, expr const & e) { return expr(new expr_let(n, v, e)); }
-inline expr Let(name const & n, expr const & v, expr const & e) { return mk_let(n, v, e); }
 inline expr mk_type(level const & l) { return expr(new expr_type(l)); }
        expr mk_type();
 inline expr Type(level const & l) { return mk_type(l); }

src/kernel/expr_formatter.cpp

@@ -117,7 +117,7 @@ class simple_expr_formatter : public expr_formatter {
             break;
         case expr_kind::Let:
             out() << "let " << let_name(a) << " := ";
-            print_child(let_value(a), c);
+            print(let_value(a), c);
             out() << " in ";
             print_child(let_body(a), extend(c, let_name(a), let_value(a)));
             break;

src/tests/kernel/type_check.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "basic_thms.h"
 #include "builtin.h"
 #include "arith.h"
+#include "normalize.h"
 #include "trace.h"
 #include "test.h"
 using namespace lean;
@@ -167,6 +168,22 @@ static void tst9() {
     }
 }
 
+static void tst10() {
+    environment env = mk_toplevel();
+    env.add_var("f", arrow(Int, Int));
+    env.add_var("b", Int);
+    expr f = Const("f");
+    expr a = Const("a");
+    expr b = Const("b");
+    expr t1 = Let({{a, f(b)}, {a, f(a)}}, f(a));
+    expr t2 = f(f(f(b)));
+    std::cout << t1 << " --> " << normalize(t1, env) << "\n";
+    expr prop  = Eq(t1, t2);
+    expr proof = Refl(Int, t1);
+    env.add_theorem("simp_eq", prop, proof);
+    std::cout << env.get_object("simp_eq").pp(env) << "\n";
+}
+
 int main() {
     tst1();
     tst2();
@@ -177,5 +194,6 @@ int main() {
     tst7();
     tst8();
     tst9();
+    tst10();
     return has_violations() ? 1 : 0;
 }