refactor(frontends/lean): remove notation for creating tuples

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

src/builtin/kernel.lean

@@ -778,8 +778,6 @@ theorem proj2_congr {A B : (Type U)} {a b : A # B} (H : a = b) : proj2 a = proj2
 theorem hproj2_congr {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj2 a == proj2 b
 := subst (hrefl (proj2 a)) H
 
-definition pair {A : (Type U)} {B : A → (Type U)} (a : A) (b : B a) := tuple (sig x : A, B x) : a, b
-
 -- Up to this point, we proved all theorems using just reflexivity, substitution and case (proof by cases)
 
 -- Function extensionality

src/builtin/subtype.lean

@@ -14,7 +14,7 @@ definition abst {A : (Type U)} {P : A → Bool} (r : A) (H : inhabited (subtype
 
 theorem subtype_inhabited {A : (Type U)} {P : A → Bool} (H : ∃ x, P x) : inhabited (subtype A P)
 := obtain (w : A) (Hw : P w), from H,
-     inhabited_intro (tuple (subtype A P) : w, Hw)
+     inhabited_intro (pair w Hw)
 
 theorem P_rep {A : (Type U)} {P : A → Bool} (a : subtype A P) : P (rep a)
 := proj2 a
@@ -23,7 +23,7 @@ theorem rep_inj {A : (Type U)} {P : A → Bool} {a b : subtype A P} (H : rep a =
 := pairext _ _ H (hproof_irrel (proj2 a) (proj2 b))
 
 theorem ex_abst {A : (Type U)} {P : A → Bool} {r : A} (H : P r) : ∃ a, rep a = r
-:= exists_intro (tuple (subtype A P) : r, H) (refl r)
+:= exists_intro (pair r H) (refl r)
 
 theorem abst_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) (a : subtype A P)
                  : abst (rep a) H = a
@@ -33,7 +33,7 @@ theorem abst_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) (
 
 theorem rep_abst {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : ∀ r, P r → rep (abst r H) = r
 := take r, assume Hl : P r,
-     @eps_ax (subtype A P) H (λ x, rep x = r) (tuple (subtype A P) : r, Hl) (refl r)
+     @eps_ax (subtype A P) H (λ x, rep x = r) (pair r Hl) (refl r)
 
 theorem abst_inj {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) {r r' : A} :
                  P r → P r' → abst r H = abst r' H → r = r'

src/frontends/lean/parser_expr.cpp

@@ -861,61 +861,26 @@ expr parser_imp::parse_type(bool level_expected) {
     }
 }
 
-expr parser_imp::parse_tuple() {
+expr parser_imp::parse_pair() {
     auto p = pos();
     next();
     buffer<expr> args;
-    expr first = parse_expr();
+    expr first  = parse_expr(g_app_precedence);
+    expr second = parse_expr(g_app_precedence);
     expr type;
     if (curr_is_colon()) {
         next();
-        type = first;
+        type = parse_expr();
-        args.push_back(parse_expr());
     } else {
-        args.push_back(first);
         type = save(mk_placeholder(), p);
     }
-    while (curr_is_comma()) {
+    return save(mk_pair(first, second, type), p);
-        next();
-        args.push_back(parse_expr());
-    }
-    unsigned num = args.size();
-    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-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, type), p);
-            } else {
-                r = save(mk_pair(args[i], r, save(mk_placeholder(), p)), p);
-            }
-        }
-    }
 }
 
 expr parser_imp::parse_proj(bool first) {
     auto p = pos();
     next();
-    unsigned i = 0;
-    if (curr() == scanner::token::IntVal) {
-        i = parse_unsigned("invalid tuple/pair projection, index does not fit in a machine integer");
-        if (i == 0)
-            throw parser_error("invalid tuple/pair projection, optional index must be >= 1", p);
-        if (i > LEAN_MAX_PROJECTION)
-            throw parser_error(sstream() << "invalid tuple/pair projection, optional index is >= "
-                               << LEAN_MAX_PROJECTION << " (internal limit)", p);
-    }
     expr t = parse_expr(g_app_precedence);
-    while (i > 0) {
-        --i;
-        t = save(mk_proj2(t), p);
-    }
     if (first)
         return save(mk_proj1(t), p);
     else
@@ -1069,7 +1034,7 @@ expr parser_imp::parse_nud() {
     case scanner::token::Show:        return parse_show_expr();
     case scanner::token::Have:        return parse_have_expr();
     case scanner::token::By:          return parse_by_expr();
-    case scanner::token::Tuple:       return parse_tuple();
+    case scanner::token::Pair:        return parse_pair();
     case scanner::token::Proj1:       return parse_proj(true);
     case scanner::token::Proj2:       return parse_proj(false);
     default:

src/frontends/lean/parser_imp.h

@@ -326,7 +326,7 @@ private:
     expr parse_exists();
     expr parse_let();
     expr parse_type(bool level_expected);
-    expr parse_tuple();
+    expr parse_pair();
     expr parse_proj(bool first);
     tactic parse_tactic_macro(name tac_id, pos_info const & p);
     expr parse_show_expr();

src/frontends/lean/pp.cpp

@@ -76,7 +76,7 @@ static format g_ellipsis_n_fmt= highlight(format("\u2026"));
 static format g_ellipsis_fmt  = highlight(format("..."));
 static format g_let_fmt       = highlight_keyword(format("let"));
 static format g_in_fmt        = highlight_keyword(format("in"));
-static format g_tuple_fmt     = highlight_keyword(format("tuple"));
+static format g_pair_fmt      = highlight_keyword(format("pair"));
 static format g_proj1_fmt     = highlight_keyword(format("proj1"));
 static format g_proj2_fmt     = highlight_keyword(format("proj2"));
 static format g_assign_fmt    = highlight_keyword(format(":="));
@@ -1120,33 +1120,24 @@ class pp_fn {
         }
     }
 
-    result pp_tuple(expr a, unsigned depth) {
+    result pp_pair(expr a, unsigned depth) {
         buffer<expr> args;
-        args.push_back(pair_first(a));
+        unsigned indent   = 5;
-        expr t = pair_type(a);
+        format r_format   = g_pair_fmt;
-        bool cartesian = is_cartesian(t);
-        while (is_dep_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));
-        unsigned indent   = 6;
-        format r_format   = g_tuple_fmt;
         unsigned r_weight = 1;
-        if (!cartesian) {
+
+        auto f_r = pp_child(pair_first(a), depth);
+        auto s_r = pp_child(pair_second(a), depth);
+        r_format += nest(indent, compose(line(), f_r.first));
+        r_format += nest(indent, compose(line(), s_r.first));
+        r_weight += f_r.second + s_r.second;
+
+        expr t = pair_type(a);
+        if (!is_cartesian(t)) {
             auto t_r = pp_child(t, depth);
-            r_format += nest(indent, compose(line(), format{t_r.first, space(), colon()}));
+            r_format += nest(indent, compose(line(), format{colon(), space(), t_r.first}));
             r_weight += t_r.second;
         }
-        for (unsigned i = 0; i < args.size(); i++) {
-            auto arg_r = pp_child(args[i], depth);
-            if (i > 0)
-                r_format += comma();
-            r_format += nest(indent, compose(line(), arg_r.first));
-            r_weight += arg_r.second;
-        }
         return result(group(r_format), r_weight);
     }
 
@@ -1211,7 +1202,7 @@ class pp_fn {
                 case expr_kind::Let:        r = pp_let(e, depth);         break;
                 case expr_kind::MetaVar:    r = pp_metavar(e, depth);     break;
                 case expr_kind::HEq:        r = pp_heq(e, depth);         break;
-                case expr_kind::Pair:       r = pp_tuple(e, depth);       break;
+                case expr_kind::Pair:       r = pp_pair(e, depth);        break;
                 case expr_kind::Proj:       r = pp_proj(e, depth);        break;
                 }
             }

src/frontends/lean/scanner.cpp

@@ -32,7 +32,7 @@ static name g_have_name("have");
 static name g_show_name("show");
 static name g_by_name("by");
 static name g_sig_name("sig");
-static name g_tuple_name("tuple");
+static name g_pair_name("pair");
 static name g_proj1_name("proj1");
 static name g_proj2_name("proj2");
 static name g_cartesian_product_unicode("\u2A2F");
@@ -215,8 +215,8 @@ scanner::token scanner::read_a_symbol() {
                 return token::In;
             } else if (m_name_val == g_sig_name) {
                 return token::Sig;
-            } else if (m_name_val == g_tuple_name) {
+            } else if (m_name_val == g_pair_name) {
-                return token::Tuple;
+                return token::Pair;
             } else if (m_name_val == g_proj1_name) {
                 return token::Proj1;
             } else if (m_name_val == g_proj2_name) {
@@ -471,7 +471,7 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
     case scanner::token::Sig:               out << "sig"; break;
     case scanner::token::Proj1:             out << "proj1"; break;
     case scanner::token::Proj2:             out << "proj2"; break;
-    case scanner::token::Tuple:             out << "tuple"; break;
+    case scanner::token::Pair:              out << "pair"; break;
     case scanner::token::Placeholder:       out << "_"; break;
     case scanner::token::ScriptBlock:       out << "Script"; break;
     case scanner::token::CartesianProduct:  out << "#"; break;

src/frontends/lean/scanner.h

@@ -20,7 +20,7 @@ class scanner {
 public:
     enum class token {
         LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
-        HEq, Sig, Tuple, Proj1, Proj2, Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Assign, Type, Placeholder,
+        HEq, Sig, Pair, Proj1, Proj2, Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Assign, Type, Placeholder,
         Have, Show, By, ScriptBlock, Ellipsis, CartesianProduct, Eof
     };
 protected:

src/kernel/kernel_decls.cpp

@@ -167,7 +167,6 @@ MK_CONSTANT(allext_fn, name("allext"));
 MK_CONSTANT(proj1_congr_fn, name("proj1_congr"));
 MK_CONSTANT(proj2_congr_fn, name("proj2_congr"));
 MK_CONSTANT(hproj2_congr_fn, name("hproj2_congr"));
-MK_CONSTANT(pair_fn, name("pair"));
 MK_CONSTANT(funext_fn, name("funext"));
 MK_CONSTANT(eta_fn, name("eta"));
 MK_CONSTANT(eps_fn, name("eps"));

src/kernel/kernel_decls.h

@@ -485,10 +485,6 @@ inline expr mk_proj2_congr_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_hproj2_congr_fn();
 bool is_hproj2_congr_fn(expr const & e);
 inline expr mk_hproj2_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hproj2_congr_fn(), e1, e2, e3, e4, e5}); }
-expr mk_pair_fn();
-bool is_pair_fn(expr const & e);
-inline bool is_pair(expr const & e) { return is_app(e) && is_pair_fn(arg(e, 0)) && num_args(e) == 5; }
-inline expr mk_pair(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_pair_fn(), e1, e2, e3, e4}); }
 expr mk_funext_fn();
 bool is_funext_fn(expr const & e);
 inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_funext_fn(), e1, e2, e3, e4, e5}); }

tests/lean/sig2.lean

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

tests/lean/sig2.lean.expected.out

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

tests/lean/sig3.lean

@@ -1,3 +1,3 @@
-check tuple 10, 20
+check pair 10 20
-check tuple 10, 20, 30
+check pair 10 (pair 20 30)
-check tuple 10, true, (λ x : Nat, x > 10)
+check pair 10 (pair true (λ x : Nat, x > 10))

tests/lean/sig3.lean.expected.out

@@ -1,5 +1,5 @@
   Set: pp::colors
   Set: pp::unicode
-tuple 10, 20 : ℕ ⨯ ℕ
+pair 10 20 : ℕ ⨯ ℕ
-tuple 10, 20, 30 : ℕ ⨯ ℕ ⨯ ℕ
+pair 10 (pair 20 30) : ℕ ⨯ ℕ ⨯ ℕ
-tuple 10, ⊤, (λ x : ℕ, x > 10) : ℕ ⨯ Bool ⨯ (ℕ → Bool)
+pair 10 (pair ⊤ (λ x : ℕ, x > 10)) : ℕ ⨯ Bool ⨯ (ℕ → Bool)

tests/lean/sig4.lean

@@ -1,10 +1,10 @@
-check proj1 (tuple 10, 20)
+check proj1 (pair 10 20)
-eval proj1 (tuple 10, 20)
+eval proj1 (pair 10 20)
-eval proj2 (tuple 10, 20)
+eval proj2 (pair 10 20)
-eval proj2 (tuple 10, 20, 30)
+eval proj2 (pair 10 (pair 20 30))
-eval proj1 1 (tuple 10, 20, 30, 40)
+eval proj1  (pair 10 (pair 20 30))
-eval proj1 2 (tuple 10, 20, 30, 40)
+eval proj1 (proj2 (pair 10 (pair 20 30)))
-eval proj2 2 (tuple 10, 20, 30, 40)
+eval proj2 (proj2 (proj2 (pair 10 (pair 20 (pair 30 40)))))
 definition NZ : Type := sig x : Nat, 1 ≤ x
 variable t : NZ
 check proj1 t

tests/lean/sig4.lean.expected.out

@@ -1,11 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
-proj1 (tuple 10, 20) : ℕ
+proj1 (pair 10 20) : ℕ
 10
 20
-tuple 20, 30
+pair 20 30
+10
 20
-30
 40
   Defined: NZ
   Assumed: t

tests/lean/sig5.lean

@@ -2,8 +2,8 @@ variable vec : Nat → Type
 definition vec_with_len := sig len, vec len
 variable n : Nat
 variable v : vec n
-check tuple n, v
+check pair n v
-check (show vec_with_len, from tuple n, v)
+check (show vec_with_len, from pair n v)
-check (let v2 : vec_with_len := tuple n, v
+check (let v2 : vec_with_len := pair n v
        in v2)
-check (tuple vec_with_len : n, v)
+check (pair n v : vec_with_len)

tests/lean/sig5.lean.expected.out

@@ -4,7 +4,7 @@
   Defined: vec_with_len
   Assumed: n
   Assumed: v
-tuple n, v : ℕ ⨯ vec n
+pair n v : ℕ ⨯ vec n
-let H_show : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in H_show : vec_with_len
+let H_show : vec_with_len := pair n v : (sig x : ℕ, vec x) in H_show : vec_with_len
-let v2 : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in v2 : vec_with_len
+let v2 : vec_with_len := pair n v : (sig x : ℕ, vec x) in v2 : vec_with_len
-tuple vec_with_len : n, v : sig len : ℕ, vec len
+pair n v : vec_with_len : sig len : ℕ, vec len

tests/lean/sig6.lean

@@ -1,8 +1,8 @@
 variables A B : (Type U)
 variables t1 t2 : A ⨯ B
-axiom pair_Ax {A : (Type U)} {B : A → (Type U)} (p : sig x, B x) : (tuple (sig x, B x) : (proj1 p), (proj2 p)) = p
+axiom pair_Ax {A : (Type U)} {B : A → (Type U)} (p : sig x, B x) : (pair (proj1 p) (proj2 p) : sig x, B x) = p
 theorem spairext {A B : (Type U)} {p1 p2 : A ⨯ B} (H1 : proj1 p1 = proj1 p2) (H2 : proj2 p1 = proj2 p2) : p1 = p2
-:= calc p1  = tuple (proj1 p1), (proj2 p1)  :  symm (pair_Ax p1)
+:= calc p1  = (pair (proj1 p1) (proj2 p1))  :  symm (pair_Ax p1)
-        ... = tuple (proj1 p2), (proj2 p1)  :  { H1 }
+        ... = (pair (proj1 p2) (proj2 p1))  :  { H1 }
-        ... = tuple (proj1 p2), (proj2 p2)  :  { H2 }
+        ... = (pair (proj1 p2) (proj2 p2))  :  { H2 }
         ... = p2                            :  pair_Ax p2