feat(frontends/lean): support for nary-tuples, improve notation for non-dependent tuples, add support in the elaborator for sigma types

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

src/frontends/lean/notation.h

@@ -8,6 +8,6 @@ Author: Leonardo de Moura
 #include <limits>
 namespace lean {
 constexpr unsigned g_arrow_precedence             = 25;
-constexpr unsigned g_cartesian_product_precedence = 25;
+constexpr unsigned g_cartesian_product_precedence = 30;
 constexpr unsigned g_app_precedence   = std::numeric_limits<unsigned>::max();
 }

src/frontends/lean/parser_expr.cpp

@@ -857,25 +857,33 @@ expr parser_imp::parse_tuple() {
     auto p = pos();
     next();
     buffer<expr> args;
+    expr first = parse_expr();
+    expr type;
+    if (curr_is_colon()) {
+        next();
+        type = first;
         args.push_back(parse_expr());
+    } else {
+        args.push_back(first);
+        type = save(mk_placeholder(), p);
+    }
     while (curr_is_comma()) {
         next();
         args.push_back(parse_expr());
     }
     unsigned num = args.size();
-    if (num < 3)
-        throw parser_error("invalid tuple/pair, it must have at least three arguments", p);
-    expr t = args[num-1];
-    if (num == 3) {
-        return save(mk_pair(args[num-3], args[num-2], t), p);
+    if (num < 2)
+        throw parser_error("invalid tuple/pair, it must have at least two arguments", p);
+    if (num == 2) {
+        return save(mk_pair(args[num-2], args[num-1], type), p);
     } else {
-        expr r = save(mk_pair(args[num-3], args[num-2], save(mk_placeholder(), p)), p);
-        unsigned i = num-3;
+        expr r = save(mk_pair(args[num-2], args[num-1], save(mk_placeholder(), p)), p);
+        unsigned i = num-2;
         while (true) {
             lean_assert(i > 0);
             --i;
             if (i == 0) {
-                return save(mk_pair(args[0], r, t), p);
+                return save(mk_pair(args[0], r, type), p);
             } else {
                 r = save(mk_pair(args[i], r, save(mk_placeholder(), p)), p);
             }

src/frontends/lean/pp.cpp

@@ -1117,15 +1117,23 @@ class pp_fn {
     result pp_tuple(expr a, unsigned depth) {
         buffer<expr> args;
         args.push_back(pair_first(a));
-        while (is_pair(pair_second(a))) {
+        expr t = pair_type(a);
+        bool cartesian = is_cartesian(t);
+        while (is_pair(pair_second(a)) && !has_metavar(pair_second(a))) {
             a = pair_second(a);
+            if (!is_cartesian(pair_type(a)))
+                cartesian = false;
             args.push_back(pair_first(a));
         }
         args.push_back(pair_second(a));
-        args.push_back(pair_type(a));
         unsigned indent   = 6;
         format r_format   = g_tuple_fmt;
         unsigned r_weight = 1;
+        if (!cartesian) {
+            auto t_r = pp_child(t, depth);
+            r_format += nest(indent, compose(line(), format{t_r.first, space(), colon()}));
+            r_weight += t_r.second;
+        }
         for (unsigned i = 0; i < args.size(); i++) {
             auto arg_r = pp_child(args[i], depth);
             if (i > 0)

src/library/elaborator/elaborator.cpp

@@ -1188,7 +1188,7 @@ class elaborator::imp {
                     m_case_splits.push_back(std::move(new_cs));
                     return r;
                 }
-            } else if (is_lambda(b) || is_pi(b)) {
+            } else if (is_abstraction(b)) {
                 imitate_abstraction(a, b, c);
                 return true;
             } else if (is_app(b) && !has_metavar(arg(b, 0))) {
@@ -1472,7 +1472,7 @@ class elaborator::imp {
                 push_new_constraint(eq, new_ctx, abst_body(a), abst_body(b), new_jst);
                 return true;
             }
-            case expr_kind::Lambda: {
+            case expr_kind::Lambda: case expr_kind::Sigma: {
                 justification new_jst(new destruct_justification(c));
                 push_new_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst);
                 context new_ctx = extend(ctx, abst_name(a), abst_domain(a));
@@ -1534,6 +1534,22 @@ class elaborator::imp {
                     m_conflict = mk_failure_justification(c);
                     return false;
                 }
+            case expr_kind::Proj:
+                if (proj_first(a) != proj_first(b)) {
+                    m_conflict = mk_failure_justification(c);
+                    return false;
+                } else {
+                    justification new_jst(new destruct_justification(c));
+                    push_new_eq_constraint(ctx, proj_arg(a), proj_arg(b), new_jst);
+                    return true;
+                }
+            case expr_kind::Pair: {
+                justification new_jst(new destruct_justification(c));
+                push_new_eq_constraint(ctx, pair_first(a), pair_first(b), new_jst);
+                push_new_eq_constraint(ctx, pair_second(a), pair_second(b), new_jst);
+                push_new_eq_constraint(ctx, pair_type(a), pair_type(b), new_jst);
+                return true;
+            }
             case expr_kind::App:
                 if (!is_meta_app(a) && !is_meta_app(b)) {
                     if (num_args(a) == num_args(b)) {
@@ -1550,7 +1566,8 @@ class elaborator::imp {
             case expr_kind::Let:
                 lean_unreachable(); // LCOV_EXCL_LINE
                 return true;
-            default:
+            case expr_kind::Pi: case expr_kind::Lambda:
+            case expr_kind::Sigma: case expr_kind::MetaVar:
                 break;
             }
         }

tests/lean/sig2.lean

@@ -1,12 +1,14 @@
 check sig x : Nat, x > 0
-check tuple 10, 20, (Nat # Nat)
-check tuple 10, true, (Nat # Nat)
-check tuple true, 20, (Nat # Nat)
-check tuple true, 20, (Bool # Nat)
-check tuple true, true, (Bool # Bool)
-check tuple true, true, (Bool ⨯ Bool)
+check tuple 10, 20
+check tuple 10, true
+check tuple true, 20
+check tuple (Bool # Nat) : true, 20
+check tuple true, true
+check tuple Bool ⨯ Bool : true, true
 variable a : Nat
 axiom Ha : 1 ≤ a
 definition NZ : Type := sig x : Nat, 1 ≤ x
 check NZ
-check tuple a, Ha, NZ
+check tuple NZ : a, Ha
+check tuple Nat # Nat : true, 20
+check tuple Bool # Bool : true, 20

tests/lean/sig2.lean.expected.out

@@ -1,24 +1,26 @@
   Set: pp::colors
   Set: pp::unicode
 sig x : ℕ, x > 0 : Type
-tuple 10, 20, (ℕ ⨯ ℕ) : ℕ ⨯ ℕ
-sig2.lean:3:6: error: type mismatch in the 2nd argument of the pair
-    tuple 10, ⊤, (ℕ ⨯ ℕ)
-Pair type:
-    ℕ ⨯ ℕ
-Argument type:
-    Bool
-sig2.lean:4:6: error: type mismatch in the 1st argument of the pair
-    tuple ⊤, 20, (ℕ ⨯ ℕ)
-Pair type:
-    ℕ ⨯ ℕ
-Argument type:
-    Bool
-tuple ⊤, 20, (Bool ⨯ ℕ) : Bool ⨯ ℕ
-tuple ⊤, ⊤, (Bool ⨯ Bool) : Bool ⨯ Bool
-tuple ⊤, ⊤, (Bool ⨯ Bool) : Bool ⨯ Bool
+tuple 10, 20 : ℕ ⨯ ℕ
+tuple 10, ⊤ : ℕ ⨯ Bool
+tuple ⊤, 20 : Bool ⨯ ℕ
+tuple ⊤, 20 : Bool ⨯ ℕ
+tuple ⊤, ⊤ : Bool ⨯ Bool
+tuple ⊤, ⊤ : Bool ⨯ Bool
   Assumed: a
   Assumed: Ha
   Defined: NZ
 NZ : Type
-tuple a, Ha, NZ : sig x : ℕ, 1 ≤ x
+tuple NZ : a, Ha : sig x : ℕ, 1 ≤ x
+sig2.lean:13:6: error: type mismatch in the 1st argument of the pair
+    tuple ⊤, 20
+Pair type:
+    ℕ ⨯ ℕ
+Argument type:
+    Bool
+sig2.lean:14:6: error: type mismatch in the 2nd argument of the pair
+    tuple ⊤, 20
+Pair type:
+    Bool ⨯ Bool
+Argument type:
+    ℕ