fix(builtin/kernel): rename generalized proof_irrel axiom to hproof_irrel, and derive the restricted one

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

src/builtin/kernel.lean

@@ -898,4 +898,7 @@ axiom pairext {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x}
 -- In this model, the interpretation of Bool is the set {{*}, {}}.
 -- Thus, if A : Bool is inhabited, then its interpretation must be {*}.
 -- So, the interpretation of H1 and H2 must be *.
-axiom proof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
+axiom hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
+
+theorem proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
+:= to_eq (hproof_irrel H1 H2)

src/builtin/subtype.lean

@@ -19,7 +19,7 @@ theorem P_rep {A : (Type U)} {P : A → Bool} (a : subtype A P) : P (rep a)
 := proj2 a
 
 theorem rep_inj {A : (Type U)} {P : A → Bool} {a b : subtype A P} (H : rep a = rep b) : a = b
-:= pairext H (proof_irrel (proj2 a) (proj2 b))
+:= 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)

src/frontends/lean/parser_expr.cpp

@@ -857,19 +857,19 @@ expr parser_imp::parse_tuple() {
     auto p = pos();
     next();
     buffer<expr> args;
-    expr first = parse_expr(g_app_precedence);
+    expr first = parse_expr();
     expr type;
     if (curr_is_colon()) {
         next();
         type = first;
-        args.push_back(parse_expr(g_app_precedence));
+        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(g_app_precedence));
+        args.push_back(parse_expr());
     }
     unsigned num = args.size();
     if (num < 2)

src/kernel/kernel_decls.cpp

@@ -187,5 +187,6 @@ MK_CONSTANT(non_surjective_fn, name("non_surjective"));
 MK_CONSTANT(ind, name("ind"));
 MK_CONSTANT(infinity, name("infinity"));
 MK_CONSTANT(pairext_fn, name("pairext"));
+MK_CONSTANT(hproof_irrel_fn, name("hproof_irrel"));
 MK_CONSTANT(proof_irrel_fn, name("proof_irrel"));
 }

src/kernel/kernel_decls.h

@@ -547,7 +547,10 @@ bool is_infinity(expr const & e);
 expr mk_pairext_fn();
 bool is_pairext_fn(expr const & e);
 inline expr mk_pairext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_pairext_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_hproof_irrel_fn();
+bool is_hproof_irrel_fn(expr const & e);
+inline expr mk_hproof_irrel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_hproof_irrel_fn(), e1, e2, e3, e4}); }
 expr mk_proof_irrel_fn();
 bool is_proof_irrel_fn(expr const & e);
-inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3, e4}); }
+inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3}); }
 }

tests/lean/sig1.lean

@@ -0,0 +1,9 @@
+check sig (x y : Nat) (z : Bool), x > y ∧ z
+check sig a : Nat, Nat
+check Nat ⨯ Bool ⨯ Nat
+check Nat # Bool # Nat
+check Nat # Type # Nat
+set_option pp::unicode false
+check sig x : Nat, Nat
+check Nat ⨯ Bool ⨯ Nat
+set_option pp::unicode true

tests/lean/sig1.lean.expected.out

@@ -0,0 +1,11 @@
+  Set: pp::colors
+  Set: pp::unicode
+sig (x y : ℕ) (z : Bool), x > y ∧ z : Type
+ℕ ⨯ ℕ : Type
+ℕ ⨯ Bool ⨯ ℕ : Type
+ℕ ⨯ Bool ⨯ ℕ : Type
+ℕ ⨯ Type ⨯ ℕ : (Type 1)
+  Set: pp::unicode
+Nat # Nat : Type
+Nat # Bool # Nat : Type
+  Set: pp::unicode