feat(kernel): add dependent pairs

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

src/kernel/expr.cpp

@@ -99,7 +99,23 @@ void expr_const::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_type, todelete);
     delete(this);
 }
-
+expr_dep_pair::expr_dep_pair(expr const & f, expr const & s, expr const & t):
+    expr_cell(expr_kind::Pair, ::lean::hash(f.hash(), s.hash()), f.has_metavar() || s.has_metavar() || t.has_metavar()),
+    m_first(f), m_second(s), m_type(t), m_depth(std::max(get_depth(f), get_depth(s))+1) {
+}
+void expr_dep_pair::dealloc(buffer<expr_cell*> & todelete) {
+    dec_ref(m_first,  todelete);
+    dec_ref(m_second, todelete);
+    dec_ref(m_type,   todelete);
+    delete(this);
+}
+expr_proj::expr_proj(bool f, expr const & e):
+    expr_cell(expr_kind::Proj, ::lean::hash(17, e.hash()), e.has_metavar()),
+    m_first(f), m_depth(get_depth(e)+1), m_expr(e) {}
+void expr_proj::dealloc(buffer<expr_cell*> & todelete) {
+    dec_ref(m_expr, todelete);
+    delete(this);
+}
 expr_app::expr_app(unsigned num_args, bool has_mv):
     expr_cell(expr_kind::App, 0, has_mv),
     m_num_args(num_args) {
@@ -161,6 +177,7 @@ void expr_abstraction::dealloc(buffer<expr_cell*> & todelete) {
 }
 expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Lambda, n, t, e) {}
 expr_pi::expr_pi(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Pi, n, t, e) {}
+expr_sigma::expr_sigma(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Sigma, n, t, e) {}
 expr_type::expr_type(level const & l):
     expr_cell(expr_kind::Type, l.hash(), false),
     m_level(l) {
@@ -245,9 +262,12 @@ void expr_cell::dealloc() {
             case expr_kind::MetaVar:    delete static_cast<expr_metavar*>(it); break;
             case expr_kind::Type:       delete static_cast<expr_type*>(it); break;
             case expr_kind::Constant:   static_cast<expr_const*>(it)->dealloc(todo); break;
+            case expr_kind::Pair:       static_cast<expr_dep_pair*>(it)->dealloc(todo); break;
+            case expr_kind::Proj:       static_cast<expr_proj*>(it)->dealloc(todo); break;
             case expr_kind::App:        static_cast<expr_app*>(it)->dealloc(todo); break;
             case expr_kind::Lambda:     static_cast<expr_lambda*>(it)->dealloc(todo); break;
             case expr_kind::Pi:         static_cast<expr_pi*>(it)->dealloc(todo); break;
+            case expr_kind::Sigma:      static_cast<expr_sigma*>(it)->dealloc(todo); break;
             case expr_kind::Let:        static_cast<expr_let*>(it)->dealloc(todo); break;
             }
         }
@@ -282,9 +302,13 @@ unsigned get_depth(expr const & e) {
     case expr_kind::Var:   case expr_kind::Constant:  case expr_kind::Type:
     case expr_kind::Value: case expr_kind::MetaVar:
         return 1;
+    case expr_kind::Pair:
+        return to_pair(e)->m_depth;
+    case expr_kind::Proj:
+        return to_proj(e)->m_depth;
     case expr_kind::App:
         return to_app(e)->m_depth;
-    case expr_kind::Pi: case expr_kind::Lambda:
+    case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Sigma:
         return to_abstraction(e)->m_depth;
     case expr_kind::Let:
         return to_let(e)->m_depth;
@@ -298,9 +322,12 @@ expr copy(expr const & a) {
     case expr_kind::Constant: return mk_constant(const_name(a), const_type(a));
     case expr_kind::Type:     return mk_type(ty_level(a));
     case expr_kind::Value:    return mk_value(static_cast<expr_value*>(a.raw())->m_val);
+    case expr_kind::Pair:     return mk_pair(pair_first(a), pair_second(a), pair_type(a));
+    case expr_kind::Proj:     return mk_proj(proj_first(a), proj_arg(a));
     case expr_kind::App:      return mk_app(num_args(a), begin_args(a));
     case expr_kind::Lambda:   return mk_lambda(abst_name(a), abst_domain(a), abst_body(a));
     case expr_kind::Pi:       return mk_pi(abst_name(a), abst_domain(a), abst_body(a));
+    case expr_kind::Sigma:    return mk_sigma(abst_name(a), abst_domain(a), abst_body(a));
     case expr_kind::Let:      return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
     case expr_kind::MetaVar:  return mk_metavar(metavar_name(a), metavar_lctx(a));
     }
@@ -343,7 +370,8 @@ constexpr char g_first_app_size_kind = 32;
 constexpr char g_small_app_num_args  = 32;
 constexpr bool is_small(expr_kind k) { return 0 <= static_cast<char>(k) && static_cast<char>(k) < g_first_app_size_kind; }
 static_assert(is_small(expr_kind::Var) && is_small(expr_kind::Constant) && is_small(expr_kind::Value) && is_small(expr_kind::App) &&
-              is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Type) &&
+              is_small(expr_kind::Pair) && is_small(expr_kind::Proj) &&
+              is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Sigma) && is_small(expr_kind::Type) &&
               is_small(expr_kind::Let) && is_small(expr_kind::MetaVar), "expr_kind is too big");
 
 class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {
@@ -381,13 +409,16 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
                 case expr_kind::Constant:  s << const_name(a); write_core(const_type(a)); break;
                 case expr_kind::Type:      s << ty_level(a); break;
                 case expr_kind::Value:     to_value(a).write(s); break;
+                case expr_kind::Pair:      write_core(pair_first(a)); write_core(pair_second(a)); write_core(pair_type(a)); break;
+                case expr_kind::Proj:      s << proj_first(a); write_core(proj_arg(a)); break;
                 case expr_kind::App:
                     s << num_args(a);
                     for (unsigned i = 0; i < num_args(a); i++)
                         write_core(arg(a, i));
                     break;
                 case expr_kind::Lambda:
-                case expr_kind::Pi:        s << abst_name(a); write_core(abst_domain(a)); write_core(abst_body(a)); break;
+                case expr_kind::Pi:
+                case expr_kind::Sigma:     s << abst_name(a); write_core(abst_domain(a)); write_core(abst_body(a)); break;
                 case expr_kind::Let:       s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a)); break;
                 case expr_kind::MetaVar:   s << metavar_name(a) << metavar_lctx(a); break;
                 }
@@ -435,6 +466,15 @@ public:
                     break;
                 case expr_kind::Value:
                     return read_value(d);
+                case expr_kind::Pair: {
+                    expr f = read();
+                    expr s = read();
+                    return mk_pair(f, s, read());
+                }
+                case expr_kind::Proj: {
+                    bool f = d.read_bool();
+                    return mk_proj(f, read());
+                }
                 case expr_kind::App: {
                     buffer<expr> args;
                     unsigned num = d.read_unsigned();
@@ -452,6 +492,11 @@ public:
                     expr d = read();
                     return mk_pi(n, d, read());
                 }
+                case expr_kind::Sigma: {
+                    name n = read_name(d);
+                    expr d = read();
+                    return mk_sigma(n, d, read());
+                }
                 case expr_kind::Let: {
                     name n = read_name(d);
                     optional<expr> t = read_opt();

src/kernel/expr.h

@@ -31,8 +31,11 @@ class value;
           |   Constant      name
           |   Value         value
           |   App           [expr]
+          |   Pair          expr expr expr
+          |   Proj          bool expr         The Boolean flag indicates whether is the first/second projection
           |   Lambda        name expr expr
           |   Pi            name expr expr
+          |   Sigma         name expr expr
           |   Type          universe
           |   Let           name expr expr expr
           |   Metavar       name local_context
@@ -51,7 +54,7 @@ The main API is divided in the following sections
 - Miscellaneous
 ======================================= */
 class expr;
-enum class expr_kind { Value, Var, Constant, App, Lambda, Pi, Type, Let, MetaVar };
+enum class expr_kind { Value, Var, Constant, App, Pair, Proj, Lambda, Pi, Sigma, Type, Let, MetaVar };
 class local_entry;
 /**
    \brief A metavariable local context is just a list of local_entries.
@@ -140,9 +143,12 @@ public:
     friend expr mk_var(unsigned idx);
     friend expr mk_constant(name const & n, optional<expr> const & t);
     friend expr mk_value(value & v);
+    friend expr mk_pair(expr const & f, expr const & s, expr const & t);
+    friend expr mk_proj(bool f, expr const & t);
     friend expr mk_app(unsigned num_args, expr const * args);
     friend expr mk_lambda(name const & n, expr const & t, expr const & e);
     friend expr mk_pi(name const & n, expr const & t, expr const & e);
+    friend expr mk_sigma(name const & n, expr const & t, expr const & e);
     friend expr mk_type(level const & l);
     friend expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e);
     friend expr mk_metavar(name const & n, local_context const & ctx);
@@ -213,6 +219,37 @@ public:
     expr const * begin_args() const          { return m_args; }
     expr const * end_args() const            { return m_args + m_num_args; }
 };
+/** \brief dependent pairs */
+class expr_dep_pair : public expr_cell {
+    expr     m_first;
+    expr     m_second;
+    expr     m_type;
+    unsigned m_depth;
+    friend expr_cell;
+    friend expr mk_pair(expr const & f, expr const & s, expr const & t);
+    void dealloc(buffer<expr_cell*> & todelete);
+    friend unsigned get_depth(expr const & e);
+public:
+    expr_dep_pair(expr const & f, expr const & s, expr const & t);
+    expr const & get_first() const { return m_first; }
+    expr const & get_second() const { return m_second; }
+    expr const & get_type() const { return m_type; }
+};
+/** \brief dependent pair projection */
+class expr_proj : public expr_cell {
+    bool     m_first;   // first/second projection
+    unsigned m_depth;
+    expr     m_expr;
+    friend expr_cell;
+    friend expr mk_proj(unsigned idx, expr const & t);
+    void dealloc(buffer<expr_cell*> & todelete);
+    friend unsigned get_depth(expr const & e);
+public:
+    expr_proj(bool first, expr const & e);
+    bool first() const { return m_first; }
+    bool second() const { return !m_first; }
+    expr const & get_arg() const { return m_expr; }
+};
 /** \brief Super class for lambda abstraction and pi (functional spaces). */
 class expr_abstraction : public expr_cell {
     unsigned m_depth;
@@ -238,6 +275,11 @@ class expr_pi : public expr_abstraction {
 public:
     expr_pi(name const & n, expr const & t, expr const & e);
 };
+/** \brief Sigma types (aka the type of dependent pairs) */
+class expr_sigma : public expr_abstraction {
+public:
+    expr_sigma(name const & n, expr const & t, expr const & e);
+};
 /** \brief Let expressions */
 class expr_let : public expr_cell {
     unsigned       m_depth;
@@ -382,9 +424,12 @@ public:
 inline bool is_var(expr_cell * e)         { return e->kind() == expr_kind::Var; }
 inline bool is_constant(expr_cell * e)    { return e->kind() == expr_kind::Constant; }
 inline bool is_value(expr_cell * e)       { return e->kind() == expr_kind::Value; }
+inline bool is_pair(expr_cell * e)        { return e->kind() == expr_kind::Pair; }
+inline bool is_proj(expr_cell * e)        { return e->kind() == expr_kind::Proj; }
 inline bool is_app(expr_cell * e)         { return e->kind() == expr_kind::App; }
 inline bool is_lambda(expr_cell * e)      { return e->kind() == expr_kind::Lambda; }
 inline bool is_pi(expr_cell * e)          { return e->kind() == expr_kind::Pi; }
+inline bool is_sigma(expr_cell * e)       { return e->kind() == expr_kind::Sigma; }
 inline bool is_type(expr_cell * e)        { return e->kind() == expr_kind::Type; }
 inline bool is_let(expr_cell * e)         { return e->kind() == expr_kind::Let; }
 inline bool is_metavar(expr_cell * e)     { return e->kind() == expr_kind::MetaVar; }
@@ -393,10 +438,13 @@ inline bool is_abstraction(expr_cell * e) { return is_lambda(e) || is_pi(e); }
 inline bool is_var(expr const & e)         { return e.kind() == expr_kind::Var; }
 inline bool is_constant(expr const & e)    { return e.kind() == expr_kind::Constant; }
 inline bool is_value(expr const & e)       { return e.kind() == expr_kind::Value; }
+inline bool is_pair(expr const & e)        { return e.kind() == expr_kind::Pair; }
+inline bool is_proj(expr const & e)        { return e.kind() == expr_kind::Proj; }
 inline bool is_app(expr const & e)         { return e.kind() == expr_kind::App; }
 inline bool is_lambda(expr const & e)      { return e.kind() == expr_kind::Lambda; }
 inline bool is_pi(expr const & e)          { return e.kind() == expr_kind::Pi; }
        bool is_arrow(expr const & e);
+inline bool is_sigma(expr const & e)       { return e.kind() == expr_kind::Sigma; }
 inline bool is_type(expr const & e)        { return e.kind() == expr_kind::Type; }
 inline bool is_let(expr const & e)         { return e.kind() == expr_kind::Let; }
 inline bool is_metavar(expr const & e)     { return e.kind() == expr_kind::MetaVar; }
@@ -413,6 +461,10 @@ inline expr mk_constant(name const & n) { return mk_constant(n, none_expr()); }
 inline expr Const(name const & n) { return mk_constant(n); }
 inline expr mk_value(value & v) { return expr(new expr_value(v)); }
 inline expr to_expr(value & v) { return mk_value(v); }
+inline expr mk_pair(expr const & f, expr const & s, expr const & t) { return expr(new expr_dep_pair(f, s, t)); }
+inline expr mk_proj(bool f, expr const & e) { return expr(new expr_proj(f, e)); }
+inline expr mk_proj1(expr const & e) { return mk_proj(true, e); }
+inline expr mk_proj2(expr const & e) { return mk_proj(false, e); }
        expr mk_app(unsigned num_args, expr const * args);
 inline expr mk_app(std::initializer_list<expr> const & l) { return mk_app(l.size(), l.begin()); }
 template<typename T> expr mk_app(T const & args) { return mk_app(args.size(), args.data()); }
@@ -422,6 +474,7 @@ inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const
 inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({e1, e2, e3, e4, e5}); }
 inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); }
 inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
+inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return expr(new expr_sigma(n, t, e)); }
 inline bool is_default_arrow_var_name(name const & n) { return n == "a"; }
 inline expr mk_arrow(expr const & t, expr const & e) { return mk_pi(name("a"), t, e); }
 inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); }
@@ -450,20 +503,26 @@ inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3,
 // Casting (these functions are only needed for low-level code)
 inline expr_var *         to_var(expr_cell * e)         { lean_assert(is_var(e));         return static_cast<expr_var*>(e); }
 inline expr_const *       to_constant(expr_cell * e)    { lean_assert(is_constant(e));    return static_cast<expr_const*>(e); }
+inline expr_dep_pair *    to_pair(expr_cell * e)        { lean_assert(is_pair(e));        return static_cast<expr_dep_pair*>(e); }
+inline expr_proj *        to_proj(expr_cell * e)        { lean_assert(is_proj(e));        return static_cast<expr_proj*>(e); }
 inline expr_app *         to_app(expr_cell * e)         { lean_assert(is_app(e));         return static_cast<expr_app*>(e); }
 inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstraction(e)); return static_cast<expr_abstraction*>(e); }
 inline expr_lambda *      to_lambda(expr_cell * e)      { lean_assert(is_lambda(e));      return static_cast<expr_lambda*>(e); }
 inline expr_pi *          to_pi(expr_cell * e)          { lean_assert(is_pi(e));          return static_cast<expr_pi*>(e); }
+inline expr_sigma *       to_sigma(expr_cell * e)       { lean_assert(is_sigma(e));       return static_cast<expr_sigma*>(e); }
 inline expr_type *        to_type(expr_cell * e)        { lean_assert(is_type(e));        return static_cast<expr_type*>(e); }
 inline expr_let *         to_let(expr_cell * e)         { lean_assert(is_let(e));         return static_cast<expr_let*>(e); }
 inline expr_metavar *     to_metavar(expr_cell * e)     { lean_assert(is_metavar(e));     return static_cast<expr_metavar*>(e); }
 
 inline expr_var *         to_var(expr const & e)         { return to_var(e.raw()); }
 inline expr_const *       to_constant(expr const & e)    { return to_constant(e.raw()); }
+inline expr_dep_pair *    to_pair(expr const & e)        { return to_pair(e.raw()); }
+inline expr_proj *        to_proj(expr const & e)        { return to_proj(e.raw()); }
 inline expr_app *         to_app(expr const & e)         { return to_app(e.raw()); }
 inline expr_abstraction * to_abstraction(expr const & e) { return to_abstraction(e.raw()); }
 inline expr_lambda *      to_lambda(expr const & e)      { return to_lambda(e.raw()); }
 inline expr_pi *          to_pi(expr const & e)          { return to_pi(e.raw()); }
+inline expr_sigma *       to_sigma(expr const & e)       { return to_sigma(e.raw()); }
 inline expr_let *         to_let(expr const & e)         { return to_let(e.raw()); }
 inline expr_type *        to_type(expr const & e)        { return to_type(e.raw()); }
 inline expr_metavar *     to_metavar(expr const & e)     { return to_metavar(e.raw()); }
@@ -479,6 +538,11 @@ inline bool          is_var(expr_cell * e, unsigned i)   { return is_var(e) && v
 inline name const &  const_name(expr_cell * e)           { return to_constant(e)->get_name(); }
 // Remark: the following function should not be exposed in the internal API.
 inline optional<expr> const &  const_type(expr_cell * e) { return to_constant(e)->get_type(); }
+inline expr const &  pair_first(expr_cell * e)           { return to_pair(e)->get_first(); }
+inline expr const &  pair_second(expr_cell * e)          { return to_pair(e)->get_second(); }
+inline expr const &  pair_type(expr_cell * e)            { return to_pair(e)->get_type(); }
+inline bool          proj_first(expr_cell * e)           { return to_proj(e)->first(); }
+inline expr const &  proj_arg(expr_cell * e)             { return to_proj(e)->get_arg(); }
 inline value const & to_value(expr_cell * e)             { lean_assert(is_value(e)); return static_cast<expr_value*>(e)->get_value(); }
 inline unsigned      num_args(expr_cell * e)             { return to_app(e)->get_num_args(); }
 inline expr const &  arg(expr_cell * e, unsigned idx)    { return to_app(e)->get_arg(idx); }
@@ -509,6 +573,11 @@ inline bool          is_constant(expr const & e, name const & n) {
     return is_constant(e) && const_name(e) == n;
 }
 inline value const & to_value(expr const & e)             { return to_value(e.raw()); }
+inline expr const &  pair_first(expr const & e)           { return to_pair(e)->get_first(); }
+inline expr const &  pair_second(expr const & e)          { return to_pair(e)->get_second(); }
+inline expr const &  pair_type(expr const & e)            { return to_pair(e)->get_type(); }
+inline bool          proj_first(expr const & e)           { return to_proj(e)->first(); }
+inline expr const &  proj_arg(expr const & e)             { return to_proj(e)->get_arg(); }
 inline unsigned      num_args(expr const & e)             { return to_app(e)->get_num_args(); }
 inline expr const &  arg(expr const & e, unsigned idx)    { return to_app(e)->get_arg(idx); }
 inline expr const *  begin_args(expr const & e)           { return to_app(e)->begin_args(); }
@@ -613,7 +682,12 @@ template<typename F> expr update_abst(expr const & e, F f) {
     std::pair<expr, expr> p = f(old_t, old_b);
     if (!is_eqp(p.first, old_t) || !is_eqp(p.second, old_b)) {
         name const & n = abst_name(e);
-        return is_pi(e) ? mk_pi(n, p.first, p.second) : mk_lambda(n, p.first, p.second);
+        switch (e.kind()) {
+        case expr_kind::Pi:     return mk_pi(n, p.first, p.second);
+        case expr_kind::Lambda: return mk_lambda(n, p.first, p.second);
+        case expr_kind::Sigma:  return mk_sigma(n, p.first, p.second);
+        default: lean_unreachable();
+        }
     } else {
         return e;
     }
@@ -673,6 +747,25 @@ inline expr update_const(expr const & e, optional<expr> const & t) {
     else
         return e;
 }
+template<typename F> expr update_pair(expr const & e, F f) {
+    expr const & old_f  = pair_first(e);
+    expr const & old_s  = pair_second(e);
+    expr const & old_t  = pair_type(e);
+    auto r = f(old_f, old_s, old_t);
+    if (!is_eqp(std::get<0>(r), old_t) || !is_eqp(std::get<1>(r), old_s) || !is_eqp(std::get<2>(r), old_t))
+        return mk_pair(std::get<0>(r), std::get<1>(r), std::get<2>(r));
+    else
+        return e;
+}
+inline expr update_pair(expr const & e, expr const & new_f, expr const & new_s, expr const & new_t) {
+    return update_pair(e, [&](expr const &, expr const &, expr const &) { return std::make_tuple(new_f, new_s, new_t); });
+}
+inline expr update_proj(expr const & e, expr const & new_arg) {
+    if (!is_eqp(proj_arg(e), new_arg))
+        return mk_proj(proj_first(e), new_arg);
+    else
+        return e;
+}
 // =======================================
 
 

src/kernel/expr_eq.h

@@ -64,6 +64,9 @@ class expr_eq_fn {
                 if (!apply(arg(a, i), arg(b, i)))
                     return false;
             return true;
+        case expr_kind::Pair:     return pair_first(a) == pair_first(b) && pair_second(a) == pair_second(b) && pair_type(a) == pair_type(b);
+        case expr_kind::Proj:     return proj_first(a) == proj_first(b) && proj_arg(a) == proj_arg(b);
+        case expr_kind::Sigma:
         case expr_kind::Lambda:   // Remark: we ignore get_abs_name because we want alpha-equivalence
         case expr_kind::Pi:       return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b));
         case expr_kind::Type:     return ty_level(a) == ty_level(b);

src/kernel/for_each_fn.h

@@ -85,8 +85,17 @@ class for_each_fn {
                 }
                 goto begin_loop;
             }
+            case expr_kind::Pair:
+                todo.emplace_back(pair_first(e), offset);
+                todo.emplace_back(pair_second(e), offset);
+                todo.emplace_back(pair_type(e), offset);
+                goto begin_loop;
+            case expr_kind::Proj:
+                todo.emplace_back(proj_arg(e), offset);
+                goto begin_loop;
             case expr_kind::Lambda:
             case expr_kind::Pi:
+            case expr_kind::Sigma:
                 todo.emplace_back(abst_body(e), offset + 1);
                 todo.emplace_back(abst_domain(e), offset);
                 goto begin_loop;

src/kernel/free_vars.cpp

@@ -40,7 +40,9 @@ protected:
             return true;
         case expr_kind::Var:
             return var_idx(e) >= offset;
-        case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
+        case expr_kind::App: case expr_kind::Lambda:
+        case expr_kind::Pi: case expr_kind::Let: case expr_kind::Sigma:
+        case expr_kind::Proj: case expr_kind::Pair:
             break;
         }
 
@@ -78,13 +80,18 @@ protected:
         case expr_kind::App:
             result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
             break;
-        case expr_kind::Lambda:
+        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
-        case expr_kind::Pi:
             result = apply(abst_domain(e), offset) || apply(abst_body(e), offset + 1);
             break;
         case expr_kind::Let:
             result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1);
             break;
+        case expr_kind::Proj:
+            result = apply(proj_arg(e), offset);
+            break;
+        case expr_kind::Pair:
+            result = apply(pair_first(e), offset) || apply(pair_second(e), offset) || apply(pair_type(e), offset);
+            break;
         }
 
         if (!result) {
@@ -168,7 +175,9 @@ class free_var_range_fn {
         case expr_kind::Var:
             return var_idx(e) + 1;
         case expr_kind::MetaVar: case expr_kind::App:
-        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
+        case expr_kind::Lambda: case expr_kind::Pi:
+        case expr_kind::Let: case expr_kind::Sigma:
+        case expr_kind::Proj: case expr_kind::Pair:
             break;
         }
 
@@ -200,13 +209,18 @@ class free_var_range_fn {
             for (auto const & c : args(e))
                 result = std::max(result, apply(c));
             break;
-        case expr_kind::Lambda:
+        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
-        case expr_kind::Pi:
             result = std::max(apply(abst_domain(e)), dec(apply(abst_body(e))));
             break;
         case expr_kind::Let:
             result = std::max({apply(let_type(e)), apply(let_value(e)), dec(apply(let_body(e)))});
             break;
+        case expr_kind::Proj:
+            result = apply(proj_arg(e));
+            break;
+        case expr_kind::Pair:
+            result = std::max({apply(pair_first(e)), apply(pair_second(e)), apply(pair_type(e))});
+            break;
         }
 
         if (shared)
@@ -284,7 +298,9 @@ protected:
                 return true; // assume that any free variable can occur in the metavariable
         case expr_kind::Var:
             return in_interval(var_idx(e), offset);
-        case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
+        case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi:
+        case expr_kind::Let:  case expr_kind::Sigma:
+        case expr_kind::Proj: case expr_kind::Pair:
             break;
         }
 
@@ -323,13 +339,18 @@ protected:
         case expr_kind::App:
             result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
             break;
-        case expr_kind::Lambda:
+        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
-        case expr_kind::Pi:
             result = apply(abst_domain(e), offset) || apply(abst_body(e), offset + 1);
             break;
         case expr_kind::Let:
             result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1);
             break;
+        case expr_kind::Proj:
+            result = apply(proj_arg(e), offset);
+            break;
+        case expr_kind::Pair:
+            result = apply(pair_first(e), offset) || apply(pair_second(e), offset) || apply(pair_type(e), offset);
+            break;
         }
 
         if (!result && shared) {

src/kernel/kernel_exception.cpp

@@ -56,11 +56,32 @@ format app_type_mismatch_exception::pp(formatter const & fmt, options const & op
     return r;
 }
 
-format function_expected_exception::pp(formatter const & fmt, options const & opts) const {
+format pair_type_mismatch_exception::pp(formatter const & fmt, options const & opts) const {
+    unsigned indent     = get_pp_indent(opts);
+    context const & ctx = get_context();
+    expr const & pair   = get_pair();
+    format pair_fmt     = fmt(ctx, pair, false, opts);
+    format r = format("type mismatch in the ");
+    if (m_first)
+        r += format("1st");
+    else
+        r += format("2nd");
+    r += format(" argument of the pair");
+    r += nest(indent, compose(line(), pair_fmt));
+    r += compose(line(), format("Pair type:"));
+    r += nest(indent, compose(line(), fmt(ctx, m_sig_type, false, opts)));
+    r += line();
+    r += format("Arguments type:");
+    r += nest(indent, compose(line(), fmt(ctx, m_arg_type, false, opts)));
+    return r;
+}
+
+format abstraction_expected_exception::pp(formatter const & fmt, options const & opts) const {
     unsigned indent = get_pp_indent(opts);
     format expr_fmt = fmt(get_context(), get_expr(), false, opts);
     format r;
-    r += format("function expected at");
+    r += format(what());
+    r += format(" at");
     r += nest(indent, compose(line(), expr_fmt));
     return r;
 }

src/kernel/kernel_exception.h

@@ -145,30 +145,67 @@ public:
     virtual void rethrow() const { throw *this; }
 };
 
+class pair_type_mismatch_exception : public type_checker_exception {
+    context     m_context;
+    expr        m_pair;
+    bool        m_first;
+    expr        m_arg_type;
+    expr        m_sig_type;
+public:
+    pair_type_mismatch_exception(ro_environment const & env, context const & ctx, expr const & pair,
+                                 bool first, expr const & arg_type, expr const & sig_type):
+        type_checker_exception(env), m_context(ctx), m_pair(pair), m_first(first), m_arg_type(arg_type), m_sig_type(sig_type) {}
+    virtual ~pair_type_mismatch_exception() {}
+    context const & get_context() const { return m_context; }
+    expr const & get_pair() const { return m_pair; }
+    virtual optional<expr> get_main_expr() const { return some_expr(get_pair()); }
+    bool first() const { return m_first; }
+    virtual char const * what() const noexcept { return "pair argument type mismatch"; }
+    virtual format pp(formatter const & fmt, options const & opts) const;
+    virtual exception * clone() const { return new pair_type_mismatch_exception(m_env, m_context, m_pair, m_first, m_arg_type, m_sig_type); }
+    virtual void rethrow() const { throw *this; }
+};
+
 /**
    \brief Exception used to report than an expression that is not a
-   function is being used as a function.
+   function (pair) is being used as a function (pair)
 
    Explanation:
    In the environment get_environment() and local context
-   get_context(), the expression get_expr() is expected to be a function.
+   get_context(), the expression get_expr() is expected to be a function (pair).
 */
-class function_expected_exception : public type_checker_exception {
+class abstraction_expected_exception : public type_checker_exception {
+protected:
     context m_context;
     expr    m_expr;
 public:
-    function_expected_exception(ro_environment const & env, context const & ctx, expr const & e):
+    abstraction_expected_exception(ro_environment const & env, context const & ctx, expr const & e):
         type_checker_exception(env), m_context(ctx), m_expr(e) {}
-    virtual ~function_expected_exception() {}
+    virtual ~abstraction_expected_exception() {}
     context const & get_context() const { return m_context; }
     expr const & get_expr() const { return m_expr; }
     virtual optional<expr> get_main_expr() const { return some_expr(get_expr()); }
-    virtual char const * what() const noexcept { return "function expected"; }
     virtual format pp(formatter const & fmt, options const & opts) const;
+};
+
+class function_expected_exception : public abstraction_expected_exception {
+public:
+    function_expected_exception(ro_environment const & env, context const & ctx, expr const & e):
+        abstraction_expected_exception(env, ctx, e) {}
+    virtual char const * what() const noexcept { return "function expected"; }
     virtual exception * clone() const { return new function_expected_exception(m_env, m_context, m_expr); }
     virtual void rethrow() const { throw *this; }
 };
 
+class pair_expected_exception : public abstraction_expected_exception {
+public:
+    pair_expected_exception(ro_environment const & env, context const & ctx, expr const & e):
+        abstraction_expected_exception(env, ctx, e) {}
+    virtual char const * what() const noexcept { return "pair expected"; }
+    virtual exception * clone() const { return new pair_expected_exception(m_env, m_context, m_expr); }
+    virtual void rethrow() const { throw *this; }
+};
+
 /**
    \brief Exception used to report than an expression that is not a
    type is being used where a type is expected.

src/kernel/max_sharing.cpp

@@ -44,44 +44,46 @@ struct max_sharing_fn::imp {
             m_cache.insert(a);
             return a;
         }
+        expr res;
         switch (a.kind()) {
-        case expr_kind::Constant: {
+        case expr_kind::Constant:
-            expr r = update_const(a, apply(const_type(a)));
+            res = update_const(a, apply(const_type(a)));
-            cache(r);
+            break;
-            return r;
-        }
         case expr_kind::Var: case expr_kind::Type: case expr_kind::Value:
-            cache(a);
+            res = a;
-            return a;
+            break;
-        case expr_kind::App: {
+        case expr_kind::Pair:
-            expr r = update_app(a, [=](expr const & c) { return apply(c); });
+            res = update_pair(a, [=](expr const & f, expr const & s, expr const & t) {
-            cache(r);
+                    return std::make_tuple(apply(f), apply(s), apply(t));
-            return r;
+                });
-        }
+            break;
+        case expr_kind::Proj:
+            res = update_proj(a, apply(proj_arg(a)));
+            break;
+        case expr_kind::App:
+            res = update_app(a, [=](expr const & c) { return apply(c); });
+            break;
+        case expr_kind::Sigma:
         case expr_kind::Lambda:
-        case expr_kind::Pi: {
+        case expr_kind::Pi:
-            expr r = update_abst(a, [=](expr const & t, expr const & b) { return std::make_pair(apply(t), apply(b)); });
+            res = update_abst(a, [=](expr const & t, expr const & b) { return std::make_pair(apply(t), apply(b)); });
-            cache(r);
+            break;
-            return r;
+        case expr_kind::Let:
-        }
+            res = update_let(a, [=](optional<expr> const & t, expr const & v, expr const & b) {
-        case expr_kind::Let: {
-            expr r = update_let(a, [=](optional<expr> const & t, expr const & v, expr const & b) {
                     return std::make_tuple(apply(t), apply(v), apply(b));
                 });
-            cache(r);
+            break;
-            return r;
-        }
         case expr_kind::MetaVar: {
-            expr r = update_metavar(a, [=](local_entry const & e) -> local_entry {
+            res = update_metavar(a, [=](local_entry const & e) -> local_entry {
                     if (e.is_inst())
                         return mk_inst(e.s(), apply(e.v()));
                     else
                         return e;
                 });
-            cache(r);
+            break;
-            return r;
         }}
-        lean_unreachable(); // LCOV_EXCL_LINE
+        cache(res);
+        return res;
     }
     expr operator()(expr const & a) { return apply(a); }
 };

src/kernel/normalizer.cpp

@@ -232,9 +232,7 @@ class normalizer::imp {
 
         expr r;
         switch (a.kind()) {
-        case expr_kind::Pi:
+        case expr_kind::Sigma: case expr_kind::Pi:
-            r = mk_closure(a, m_ctx, s);
-            break;
         case expr_kind::MetaVar: case expr_kind::Lambda:
             r = mk_closure(a, m_ctx, s);
             break;
@@ -251,6 +249,25 @@ class normalizer::imp {
             }
             break;
         }
+        case expr_kind::Pair: {
+            expr new_first  = normalize(pair_first(a), s, k);
+            expr new_second = normalize(pair_second(a), s, k);
+            expr new_type   = normalize(pair_type(a), s, k);
+            r = update_pair(a, new_first, new_second, new_type);
+            break;
+        }
+        case expr_kind::Proj: {
+            expr new_arg = normalize(proj_arg(a), s, k);
+            if (is_pair(new_arg)) {
+                if (proj_first(a))
+                    r = pair_first(new_arg);
+                else
+                    r = pair_second(new_arg);
+            } else {
+                r = update_proj(a, new_arg);
+            }
+            break;
+        }
         case expr_kind::Type: case expr_kind::Value:
             r = a;
             break;

src/kernel/replace_fn.h

@@ -144,6 +144,22 @@ public:
             switch (e.kind()) {
             case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
                 lean_unreachable(); // LCOV_EXCL_LINE
+            case expr_kind::Pair:
+                if (check_index(f, 0) && !visit(pair_first(e), offset))
+                    goto begin_loop;
+                if (check_index(f, 1) && !visit(pair_second(e), offset))
+                    goto begin_loop;
+                if (check_index(f, 2) && !visit(pair_type(e), offset))
+                    goto begin_loop;
+                r = update_pair(e, rs(-3), rs(-2), rs(-1));
+                pop_rs(3);
+                break;
+            case expr_kind::Proj:
+                if (check_index(f, 0) && !visit(proj_arg(e), offset))
+                    goto begin_loop;
+                r = update_proj(e, rs(-1));
+                pop_rs(1);
+                break;
             case expr_kind::App: {
                 unsigned num = num_args(e);
                 while (f.m_index < num) {
@@ -156,7 +172,7 @@ public:
                 pop_rs(num);
                 break;
             }
-            case expr_kind::Pi: case expr_kind::Lambda:
+            case expr_kind::Sigma: case expr_kind::Pi: case expr_kind::Lambda:
                 if (check_index(f, 0) && !visit(abst_domain(e), offset))
                     goto begin_loop;
                 if (check_index(f, 1) && !visit(abst_body(e), offset + 1))

src/kernel/replace_visitor.cpp

@@ -18,6 +18,15 @@ expr replace_visitor::visit_constant(expr const & e, context const & ctx) {
     lean_assert(is_constant(e));
     return update_const(e, visit(const_type(e), ctx));
 }
+expr replace_visitor::visit_pair(expr const & e, context const & ctx) {
+    lean_assert(is_pair(e));
+    return update_pair(e, [&](expr const & f, expr const & s, expr const & t) {
+            return std::make_tuple(visit(f, ctx), visit(s, ctx), visit(t, ctx));
+        });
+}
+expr replace_visitor::visit_proj(expr const & e, context const & ctx) {
+    return update_proj(e, visit(proj_arg(e), ctx));
+}
 expr replace_visitor::visit_app(expr const & e, context const & ctx) {
     lean_assert(is_app(e));
     return update_app(e, [&](expr const & c) { return visit(c, ctx); });
@@ -41,7 +50,10 @@ expr replace_visitor::visit_pi(expr const & e, context const & ctx) {
     lean_assert(is_pi(e));
     return visit_abst(e, ctx);
 }
-
+expr replace_visitor::visit_sigma(expr const & e, context const & ctx) {
+    lean_assert(is_pi(e));
+    return visit_abst(e, ctx);
+}
 expr replace_visitor::visit_let(expr const & e, context const & ctx) {
     lean_assert(is_let(e));
     return update_let(e, [&](optional<expr> const & t, expr const & v, expr const & b) {
@@ -75,9 +87,12 @@ expr replace_visitor::visit(expr const & e, context const & ctx) {
     case expr_kind::Constant:  return save_result(e, visit_constant(e, ctx), shared);
     case expr_kind::Var:       return save_result(e, visit_var(e, ctx), shared);
     case expr_kind::MetaVar:   return save_result(e, visit_metavar(e, ctx), shared);
+    case expr_kind::Pair:      return save_result(e, visit_pair(e, ctx), shared);
+    case expr_kind::Proj:      return save_result(e, visit_proj(e, ctx), shared);
     case expr_kind::App:       return save_result(e, visit_app(e, ctx), shared);
     case expr_kind::Lambda:    return save_result(e, visit_lambda(e, ctx), shared);
     case expr_kind::Pi:        return save_result(e, visit_pi(e, ctx), shared);
+    case expr_kind::Sigma:     return save_result(e, visit_sigma(e, ctx), shared);
     case expr_kind::Let:       return save_result(e, visit_let(e, ctx), shared);
     }
 

src/kernel/replace_visitor.h

@@ -30,10 +30,13 @@ protected:
     virtual expr visit_constant(expr const &, context const &);
     virtual expr visit_var(expr const &, context const &);
     virtual expr visit_metavar(expr const &, context const &);
+    virtual expr visit_pair(expr const &, context const &);
+    virtual expr visit_proj(expr const &, context const &);
     virtual expr visit_app(expr const &, context const &);
     virtual expr visit_abst(expr const &, context const &);
     virtual expr visit_lambda(expr const &, context const &);
     virtual expr visit_pi(expr const &, context const &);
+    virtual expr visit_sigma(expr const &, context const &);
     virtual expr visit_let(expr const &, context const &);
     virtual expr visit(expr const &, context const &);
     optional<expr> visit(optional<expr> const &, context const &);

src/kernel/type_checker.cpp

@@ -89,6 +89,30 @@ class type_checker::imp {
         throw function_expected_exception(env(), ctx, s);
     }
 
+    // TODO(Leo): we should consider merging check_pi and check_sigma.
+    // They are very similar
+    expr check_sigma(expr const & e, expr const & s, context const & ctx) {
+        if (is_sigma(e))
+            return e;
+        expr r = normalize(e, ctx, false);
+        if (is_sigma(r))
+            return r;
+        if (has_metavar(r) && m_menv && m_uc) {
+            // Create two fresh variables A and B,
+            // and assign r == (Pi(x : A), B)
+            expr A   = m_menv->mk_metavar(ctx);
+            expr B   = m_menv->mk_metavar(extend(ctx, g_x_name, A));
+            expr p   = mk_sigma(g_x_name, A, B);
+            justification jst = mk_pair_expected_justification(ctx, s);
+            m_uc->push_back(mk_eq_constraint(ctx, e, p, jst));
+            return p;
+        }
+        r = normalize(e, ctx, true);
+        if (is_sigma(r))
+            return r;
+        throw pair_expected_exception(env(), ctx, s);
+    }
+
     /**
        \brief Given \c t (a Pi term), this method returns the body (aka range)
        of the function space for the element e in the domain of the Pi.
@@ -188,6 +212,8 @@ class type_checker::imp {
             return mk_type(ty_level(e) + 1);
         case expr_kind::App: case expr_kind::Lambda:
         case expr_kind::Pi:  case expr_kind::Let:
+        case expr_kind::Sigma: case expr_kind::Proj:
+        case expr_kind::Pair:
             break; // expensive cases
         }
 
@@ -242,6 +268,35 @@ class type_checker::imp {
                     f_t = check_pi(f_t, e, ctx);
                 }
             }
+        case expr_kind::Pair:
+            if (m_infer_only) {
+                return pair_type(e);
+            } else {
+                expr const & t = pair_type(e);
+                expr sig       = check_sigma(infer_type_core(t, ctx), e, ctx);
+                expr f_t       = infer_type_core(pair_first(e), ctx);
+                expr s_t       = infer_type_core(pair_second(e), ctx);
+                auto mk_fst_justification = [&]() { return mk_pair_type_match_justification(ctx, e, true); };
+                if (!is_convertible(f_t, abst_domain(sig), ctx, mk_fst_justification))
+                    throw pair_type_mismatch_exception(env(), ctx, e, true, f_t, sig);
+                auto mk_snd_justification = [&]() { return mk_pair_type_match_justification(ctx, e, false); };
+                expr expected  = instantiate(abst_body(sig), f_t);
+                if (!is_convertible(s_t, expected, ctx, mk_snd_justification))
+                    throw pair_type_mismatch_exception(env(), ctx, e, false, s_t, sig);
+                return sig;
+            }
+        case expr_kind::Proj: {
+            expr t = check_sigma(infer_type_core(proj_arg(e), ctx), e, ctx);
+            if (proj_first(t)) {
+                return abst_domain(t);
+            } else {
+                expr const & b = abst_body(t);
+                if (closed(b))
+                    return b;
+                else
+                    return instantiate(b, mk_proj1(e));
+            }
+        }
         case expr_kind::Lambda:
             if (!m_infer_only) {
                 expr d = infer_type_core(abst_domain(e), ctx);
@@ -253,7 +308,7 @@ class type_checker::imp {
                                    mk_pi(abst_name(e), abst_domain(e), infer_type_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)))),
                                    shared);
             }
-        case expr_kind::Pi: {
+        case expr_kind::Sigma: case expr_kind::Pi: {
             expr t1  = check_type(infer_type_core(abst_domain(e), ctx), abst_domain(e), ctx);
             if (is_bool(t1))
                 t1 = Type();
@@ -263,7 +318,7 @@ class type_checker::imp {
                 freset<cache> reset(m_cache);
                 t2 = check_type(infer_type_core(abst_body(e), new_ctx), abst_body(e), new_ctx);
             }
-            if (is_bool(t2))
+            if (is_pi(e) && is_bool(t2))
                 return t2;
             if (is_type(t1) && is_type(t2)) {
                 return save_result(e, mk_type(max(ty_level(t1), ty_level(t2))), shared);
@@ -455,6 +510,16 @@ public:
         }
     }
 
+    expr ensure_sigma(expr const & e, context const & ctx, optional<metavar_env> const & menv) {
+        set_ctx(ctx);
+        update_menv(menv);
+        try {
+            return check_sigma(e, expr(), ctx);
+        } catch (exception &) {
+            throw exception("internal bug, expression is not a Sigma");
+        }
+    }
+
     void clear_cache() {
         m_cache.clear();
         m_normalizer.clear();
@@ -523,6 +588,12 @@ expr type_checker::ensure_pi(expr const & e, context const & ctx, optional<ro_me
 expr type_checker::ensure_pi(expr const & e, context const & ctx) {
     return m_ptr->ensure_pi(e, ctx, none_menv());
 }
+expr type_checker::ensure_sigma(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
+    return m_ptr->ensure_sigma(e, ctx, ro_metavar_env::to_rw(menv));
+}
+expr type_checker::ensure_sigma(expr const & e, context const & ctx) {
+    return m_ptr->ensure_sigma(e, ctx, none_menv());
+}
 bool type_checker::is_proposition(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
     return m_ptr->is_proposition(e, ctx, ro_metavar_env::to_rw(menv));
 }

src/kernel/type_checker.h

@@ -109,6 +109,10 @@ public:
     expr ensure_pi(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv);
     expr ensure_pi(expr const & e, context const & ctx = context());
 
+    /** \brief Return a Sigma if \c e is convertible to Sigma. Throw an exception otherwise. */
+    expr ensure_sigma(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv);
+    expr ensure_sigma(expr const & e, context const & ctx = context());
+
     /** \brief Reset internal caches */
     void clear();
 

src/kernel/type_checker_justification.cpp

@@ -8,25 +8,30 @@ Author: Leonardo de Moura
 #include "kernel/metavar.h"
 
 namespace lean {
-function_expected_justification_cell::~function_expected_justification_cell() {
+abstraction_expected_justification_cell::~abstraction_expected_justification_cell() {
 }
 
-format function_expected_justification_cell::pp_header(formatter const & fmt, options const & opts, optional<metavar_env> const & menv) const {
+format abstraction_expected_justification_cell::pp_header(formatter const & fmt, options const & opts, optional<metavar_env> const & menv) const {
     unsigned indent = get_pp_indent(opts);
-    format expr_fmt = fmt(instantiate_metavars(menv, m_ctx), instantiate_metavars(menv, m_app), false, opts);
+    format expr_fmt = fmt(instantiate_metavars(menv, m_ctx), instantiate_metavars(menv, m_expr), false, opts);
     format r;
-    r += format("Function expected at");
+    r += format(get_abst_str());
+    r += format(" expected at");
     r += nest(indent, compose(line(), expr_fmt));
     return r;
 }
 
-void function_expected_justification_cell::get_children(buffer<justification_cell*> &) const {
+void abstraction_expected_justification_cell::get_children(buffer<justification_cell*> &) const {
 }
 
-optional<expr> function_expected_justification_cell::get_main_expr() const {
+optional<expr> abstraction_expected_justification_cell::get_main_expr() const {
-    return some_expr(m_app);
+    return some_expr(m_expr);
 }
 
+char const * function_expected_justification_cell::get_abst_str() const { return "Function"; }
+
+char const * pair_expected_justification_cell::get_abst_str() const { return "Pair"; }
+
 app_type_match_justification_cell::~app_type_match_justification_cell() {
 }
 
@@ -56,6 +61,30 @@ optional<expr> app_type_match_justification_cell::get_main_expr() const {
     return some_expr(m_app);
 }
 
+pair_type_match_justification_cell::~pair_type_match_justification_cell() {
+}
+
+format pair_type_match_justification_cell::pp_header(formatter const & fmt, options const & opts, optional<metavar_env> const & menv) const {
+    unsigned indent = get_pp_indent(opts);
+    format r;
+    r += format("Type of ");
+    if (m_first)
+        r += format("1st");
+    else
+        r += format("2nd");
+    r += format(" component must be convertible to the expected type in the pair");
+    expr new_expr = instantiate_metavars(menv, m_expr);
+    r += nest(indent, compose(line(), fmt(instantiate_metavars(menv, m_ctx), new_expr, false, opts)));
+    return r;
+}
+
+void pair_type_match_justification_cell::get_children(buffer<justification_cell*> &) const {
+}
+
+optional<expr> pair_type_match_justification_cell::get_main_expr() const {
+    return some_expr(m_expr);
+}
+
 type_expected_justification_cell::~type_expected_justification_cell() {
 }
 

src/kernel/type_checker_justification.h

@@ -12,37 +12,56 @@ Author: Leonardo de Moura
 namespace lean {
 class metavar_env;
 /**
-   \brief Justification produced by the type checker when the application \c m_app
+   \brief Justification produced by the type checker when processing applications and pairs.
-   is an application <tt>(f ...)</tt>, the type \c T of \c f contains metavariables, and
+   Suppose \c m_expr is an application <tt>(f ...)</tt>, the type \c T of \c f contains metavariables, and
    it is not clear whether it is a Pi or not. In this case, the type checker adds
    the constraint
 
-       <tt>ctx |- T == Pi (x : ?A), ?B x</tt>
+       <tt>ctx |- T == Pi (x : ?A), ?B</tt>
 
    where, \c ?A and \c ?B are fresh metavariables.
    This justification cell is used to justify the new constraint.
+
+   Similarly, suppose \c m_expr is a projection <tt>(proj_i t)</tt>, and it is not clear whether
+   type of \c t is a Sigma type because it contains metavariables. In this case, the type checker
+   adds the constraints
+
+      <tt>ctx |- T == Sigma (x : ?A), ?B</tt>
 */
-class function_expected_justification_cell : public justification_cell {
+class abstraction_expected_justification_cell : public justification_cell {
     context m_ctx;
-    expr    m_app;
+    expr    m_expr;
+    virtual char const * get_abst_str() const = 0;
 public:
-    function_expected_justification_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {}
+    abstraction_expected_justification_cell(context const & c, expr const & e):m_ctx(c), m_expr(e) {}
-    virtual ~function_expected_justification_cell();
+    virtual ~abstraction_expected_justification_cell();
     virtual format pp_header(formatter const & fmt, options const & opts, optional<metavar_env> const & menv) const;
     virtual void get_children(buffer<justification_cell*> &) const;
     virtual optional<expr> get_main_expr() const;
     context const & get_context() const { return m_ctx; }
-    expr const & get_app() const { return m_app; }
+    expr const & get_expr() const { return m_expr; }
+};
+
+class function_expected_justification_cell : public abstraction_expected_justification_cell {
+    virtual char const * get_abst_str() const;
+public:
+    function_expected_justification_cell(context const & c, expr const & e):abstraction_expected_justification_cell(c, e) {}
+};
+
+class pair_expected_justification_cell : public abstraction_expected_justification_cell {
+    virtual char const * get_abst_str() const;
+public:
+    pair_expected_justification_cell(context const & c, expr const & e):abstraction_expected_justification_cell(c, e) {}
 };
 
 /**
    \brief Justification produced by the type checker for application argument type matching.
    When checking an application <tt>(f a_1 ... a_i ...)</tt>, the type
-   \c T_inferred of \c a_i must be convertible to the expected type \c T_expected.  If
+   inferred for \c a_i must be convertible to the expected type.
-   \c T_expected or \c T_inferred contain metavariables, and it is not clear whether
+   If the expected or inferred type contain metavariables, and it is not clear whether
-   \c T_inferred is convertible to \c T_expected, then the type checker adds the constraint
+   the inferred is convertible to expected, then the type checker adds the constraint
 
-      <tt>ctx |- T_inferred << T_expected</tt>
+      <tt>ctx |- inferred << expected</tt>
 
    This justification cell is used to justify this constraint.
 */
@@ -61,12 +80,38 @@ public:
     unsigned get_arg_pos() const { return m_i; }
 };
 
+/**
+   \brief Justification produced by the type checker for pairs.
+   When checking a pair <tt>(pair f s t)</tt>, the type
+   inferred for \c f (\c s) must be convertible to the expected type in the sigma type \c t.
+   If the expected or inferred type contain metavariables, and it is not clear whether
+   the inferred is convertible to expected, then the type checker adds the constraint
+
+      <tt>ctx |- inferred << expected</tt>
+
+   This justification cell is used to justify this constraint.
+*/
+class pair_type_match_justification_cell : public justification_cell {
+    context  m_ctx;
+    expr     m_expr;
+    bool     m_first; // first/second component
+public:
+    pair_type_match_justification_cell(context const & c, expr const & a, bool f):m_ctx(c), m_expr(a), m_first(f) {}
+    virtual ~pair_type_match_justification_cell();
+    virtual format pp_header(formatter const & fmt, options const & opts, optional<metavar_env> const & menv) const;
+    virtual void get_children(buffer<justification_cell*> &) const;
+    virtual optional<expr> get_main_expr() const;
+    context const & get_context() const { return m_ctx; }
+    expr const & get_expr() const { return m_expr; }
+    bool first() const { return m_first; }
+};
+
 /**
    \brief Justification produced by the type checker when the type \c T of \c type must be of the form
    <tt>Type l</tt>, and \c T constains metavariables, and it is not of this form.
    The type checker adds the following constraint
 
-      <tt>ctx |- T << Type U</tt>
+      <tt>ctx |- T << Type U+1</tt>
 
    This justification cell is used to justify these constraints.
 */
@@ -141,7 +186,9 @@ public:
 };
 
 inline justification mk_function_expected_justification(context const & ctx, expr const & app) { return justification(new function_expected_justification_cell(ctx, app)); }
+inline justification mk_pair_expected_justification(context const & ctx, expr const & app) { return justification(new pair_expected_justification_cell(ctx, app)); }
 inline justification mk_app_type_match_justification(context const & ctx, expr const & app, unsigned i) { return justification(new app_type_match_justification_cell(ctx, app, i)); }
+inline justification mk_pair_type_match_justification(context const & ctx, expr const & e, bool first) { return justification(new pair_type_match_justification_cell(ctx, e, first)); }
 inline justification mk_type_expected_justification(context const & ctx, expr const & type) { return justification(new type_expected_justification_cell(ctx, type)); }
 inline justification mk_max_type_justification(context const & ctx, expr const & type) { return justification(new max_type_justification_cell(ctx, type)); }
 inline justification mk_def_type_match_justification(context const & ctx, name const & n, expr const & v) { return justification(new def_type_match_justification_cell(ctx, n, v)); }

src/library/deep_copy.cpp

@@ -43,8 +43,11 @@ class deep_copy_fn {
                 new_args.push_back(apply(old_arg));
             return save_result(a, mk_app(new_args), sh);
         }
+        case expr_kind::Pair:     return save_result(a, mk_pair(apply(pair_first(a)), apply(pair_second(a)), apply(pair_type(a))), sh);
+        case expr_kind::Proj:     return save_result(a, mk_proj(proj_first(a), apply(proj_arg(a))), sh);
         case expr_kind::Lambda:   return save_result(a, mk_lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
         case expr_kind::Pi:       return save_result(a, mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
+        case expr_kind::Sigma:    return save_result(a, mk_sigma(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
         case expr_kind::Let:      return save_result(a, mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))), sh);
         case expr_kind::MetaVar:
             return save_result(a,

src/library/expr_lt.cpp

@@ -41,8 +41,21 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) {
                 return is_lt(arg(a, i), arg(b, i), use_hash);
         }
         lean_unreachable(); // LCOV_EXCL_LINE
-    case expr_kind::Lambda:   // Remark: we ignore get_abs_name because we want alpha-equivalence
+    case expr_kind::Pair:
-    case expr_kind::Pi:
+        if (pair_first(a) != pair_first(b))
+            return is_lt(pair_first(a), pair_first(b), use_hash);
+        else if (pair_second(a) != pair_second(b))
+            return is_lt(pair_second(a), pair_second(b), use_hash);
+        else
+            return is_lt(pair_type(a), pair_type(b), use_hash);
+    case expr_kind::Proj:
+        if (proj_first(a) != proj_first(b))
+            return proj_first(a) && !proj_first(b); // first projection is smaller than the second one.
+        else
+            return is_lt(proj_arg(a), proj_arg(b), use_hash);
+    case expr_kind::Sigma:
+    case expr_kind::Lambda:
+    case expr_kind::Pi: // Remark: we ignore get_abs_name because we want alpha-equivalence
         if (abst_domain(a) != abst_domain(b))
             return is_lt(abst_domain(a), abst_domain(b), use_hash);
         else

src/library/fo_unify.cpp

@@ -62,7 +62,17 @@ optional<substitution> fo_unify(expr e1, expr e2) {
                         }
                     }
                     break;
-                case expr_kind::Lambda: case expr_kind::Pi:
+                case expr_kind::Proj:
+                    if (proj_first(e1) != proj_first(e2))
+                        return optional<substitution>();
+                    todo.emplace_back(proj_arg(e1), proj_arg(e2));
+                    break;
+                case expr_kind::Pair:
+                    todo.emplace_back(pair_first(e1), pair_first(e2));
+                    todo.emplace_back(pair_second(e1), pair_second(e2));
+                    todo.emplace_back(pair_type(e1), pair_type(e2));
+                    break;
+                case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
                     todo.emplace_back(abst_body(e1), abst_body(e2));
                     todo.emplace_back(abst_domain(e1), abst_domain(e2));
                     break;

src/library/hop_match.cpp

@@ -304,7 +304,14 @@ class hop_match_fn {
             }
             return true;
         }
-        case expr_kind::Lambda: case expr_kind::Pi:
+        case expr_kind::Proj:
+            return proj_first(p) == proj_first(t) && match(proj_arg(p), proj_arg(t), ctx, ctx_size);
+        case expr_kind::Pair:
+            return
+                match(pair_first(p),  pair_first(t), ctx, ctx_size) &&
+                match(pair_second(p), pair_second(t), ctx, ctx_size) &&
+                match(pair_type(p),   pair_type(t), ctx, ctx_size);
+        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
             if (m_name_subst)
                 (*m_name_subst)[abst_name(p)] = abst_name(t);
             return

src/library/kernel_bindings.cpp

@@ -495,8 +495,11 @@ static int expr_fields(lua_State * L) {
     case expr_kind::Type:     return push_level(L, ty_level(e));
     case expr_kind::Value:    return to_value(e).push_lua(L);
     case expr_kind::App:      lua_pushinteger(L, num_args(e)); expr_args(L); return 2;
+    case expr_kind::Pair:     push_expr(L, pair_first(e)); push_expr(L, pair_second(e)); push_expr(L, pair_type(e)); return 3;
+    case expr_kind::Proj:     lua_pushboolean(L, proj_first(e)); push_expr(L, proj_arg(e)); return 2;
     case expr_kind::Lambda:
     case expr_kind::Pi:
+    case expr_kind::Sigma:
         push_name(L, abst_name(e)); push_expr(L, abst_domain(e)); push_expr(L, abst_body(e)); return 3;
     case expr_kind::Let:
         push_name(L, let_name(e));  push_optional_expr(L, let_type(e)); push_expr(L, let_value(e)); push_expr(L, let_body(e)); return 4;

src/library/printer.cpp

@@ -18,7 +18,8 @@ bool is_atomic(expr const & e) {
     case expr_kind::Type: case expr_kind::MetaVar:
         return true;
     case expr_kind::App:  case expr_kind::Lambda: case expr_kind::Pi:
-    case expr_kind::Let:
+    case expr_kind::Let:  case expr_kind::Sigma:  case expr_kind::Proj:
+    case expr_kind::Pair:
         return false;
     }
     return false;
@@ -89,6 +90,15 @@ struct print_expr_fn {
         }
     }
 
+    void print_pair(expr const & e, context const & c) {
+        out() << "pair ";
+        print_child(pair_first(e), c);
+        out() << " ";
+        print_child(pair_second(e), c);
+        out() << " ";
+        print_child(pair_type(e), c);
+    }
+
     void print(expr const & a, context const & c) {
         switch (a.kind()) {
         case expr_kind::MetaVar:
@@ -108,6 +118,19 @@ struct print_expr_fn {
         case expr_kind::App:
             print_app(a, c);
             break;
+        case expr_kind::Pair:
+            print_pair(a, c);
+            break;
+        case expr_kind::Proj:
+            out() << "proj" << (proj_first(a) ? "1" : "2") << " ";
+            print_child(proj_arg(a), c);
+            break;
+        case expr_kind::Sigma:
+            out() << "Sigma " << abst_name(a) << " : ";
+            print_child(abst_domain(a), c);
+            out() << ", ";
+            print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a)));
+            break;
         case expr_kind::Lambda:
             out() << "fun " << abst_name(a) << " : ";
             print_child(abst_domain(a), c);

src/library/rewriter/fo_match.cpp

@@ -173,6 +173,9 @@ bool fo_match::match_main(expr const & p, expr const & t, unsigned o, subst_map
         return match_let(p, t, o, s);
     case expr_kind::MetaVar:
         return match_metavar(p, t, o, s);
+    case expr_kind::Proj: case expr_kind::Pair: case expr_kind::Sigma:
+        // TODO(Leo):
+        break;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }

src/library/rewriter/rewriter.h

@@ -384,6 +384,9 @@ class apply_rewriter_fn {
             }
         }
             break;
+        case expr_kind::Proj: case expr_kind::Pair: case expr_kind::Sigma:
+            // TODO(Leo):
+            break;
         case expr_kind::Lambda: {
             name const & n = abst_name(v);
             expr const & ty = abst_domain(v);

src/library/simplifier/ceq.cpp

@@ -209,7 +209,14 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset,
         } else {
             return lhs == rhs; // free variable
         }
-    case expr_kind::Lambda: case expr_kind::Pi:
+    case expr_kind::Proj:
+        return proj_first(lhs) == proj_first(rhs) && is_permutation(proj_arg(lhs), proj_arg(rhs), offset, p);
+    case expr_kind::Pair:
+        return
+            is_permutation(pair_first(lhs),  pair_first(rhs), offset, p) &&
+            is_permutation(pair_second(lhs), pair_second(rhs), offset, p) &&
+            is_permutation(pair_type(lhs),   pair_type(rhs), offset, p);
+    case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
         return
             is_permutation(abst_domain(lhs), abst_domain(rhs), offset, p) &&
             is_permutation(abst_body(lhs), abst_body(rhs), offset+1, p);

src/tests/kernel/expr.cpp

@@ -76,10 +76,14 @@ static unsigned depth2(expr const & e) {
             std::accumulate(begin_args(e), end_args(e), 0,
                             [](unsigned m, expr const & arg){ return std::max(depth2(arg), m); })
             + 1;
-    case expr_kind::Lambda: case expr_kind::Pi:
+    case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
         return std::max(depth2(abst_domain(e)), depth2(abst_body(e))) + 1;
     case expr_kind::Let:
         return std::max(depth2(let_value(e)), depth2(let_body(e))) + 1;
+    case expr_kind::Proj:
+        return depth2(proj_arg(e)) + 1;
+    case expr_kind::Pair:
+        return std::max(depth2(pair_first(e)), depth2(pair_second(e))) + 1;
     }
     return 0;
 }
@@ -133,10 +137,14 @@ static unsigned count_core(expr const & a, expr_set & s) {
     case expr_kind::App:
         return std::accumulate(begin_args(a), end_args(a), 1,
                           [&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
-    case expr_kind::Lambda: case expr_kind::Pi:
+    case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
         return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1;
     case expr_kind::Let:
         return count_core(let_value(a), s) + count_core(let_body(a), s) + 1;
+    case expr_kind::Proj:
+        return count_core(proj_arg(a), s) + 1;
+    case expr_kind::Pair:
+        return count_core(pair_first(a), s) + count_core(pair_second(a), s) + count_core(pair_type(a), s) + 1;
     }
     return 0;
 }

src/tests/kernel/normalizer.cpp

@@ -77,10 +77,14 @@ unsigned count_core(expr const & a, expr_set & s) {
     case expr_kind::App:
         return std::accumulate(begin_args(a), end_args(a), 1,
                                [&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
-    case expr_kind::Lambda: case expr_kind::Pi:
+    case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
         return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1;
     case expr_kind::Let:
         return count_core(let_value(a), s) + count_core(let_body(a), s) + 1;
+    case expr_kind::Proj:
+        return count_core(proj_arg(a), s) + 1;
+    case expr_kind::Pair:
+        return count_core(pair_first(a), s) + count_core(pair_second(a), s) + count_core(pair_type(a), s) + 1;
     }
     return 0;
 }