feat(library/definitional/util): add telescope equality for HoTT library

This is needed for implementing no_confusion for HoTT.
We can't use heterogeneous equality in HoTT.

src/frontends/lean/builtin_cmds.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "library/print.h"
 #include "library/flycheck.h"
 #include "library/definitional/projection.h"
+#include "library/definitional/util.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/calc.h"
@@ -616,26 +617,46 @@ environment projections_cmd(parser & p) {
     }
 }
 
+environment telescope_eq_cmd(parser & p) {
+    expr e; level_param_names ls;
+    std::tie(e, ls) = parse_local_expr(p);
+    buffer<expr> t;
+    while (is_pi(e)) {
+        expr local = mk_local(p.mk_fresh_name(), binding_name(e), binding_domain(e), binder_info());
+        t.push_back(local);
+        e = instantiate(binding_body(e), local);
+    }
+    auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
+    buffer<expr> eqs;
+    mk_telescopic_eq(*tc, t, eqs);
+    for (expr const & eq : eqs) {
+        regular(p.env(), p.ios()) << local_pp_name(eq) << " : " << mlocal_type(eq) << "\n";
+        tc->check(mlocal_type(eq), ls);
+    }
+    return p.env();
+}
+
 void init_cmd_table(cmd_table & r) {
-    add_cmd(r, cmd_info("open",         "create aliases for declarations, and use objects defined in other namespaces",
+    add_cmd(r, cmd_info("open",          "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
-    add_cmd(r, cmd_info("export",       "create abbreviations for declarations, "
+    add_cmd(r, cmd_info("export",        "create abbreviations for declarations, "
                         "and export objects defined in other namespaces", export_cmd));
-    add_cmd(r, cmd_info("set_option",   "set configuration option", set_option_cmd));
+    add_cmd(r, cmd_info("set_option",    "set configuration option", set_option_cmd));
-    add_cmd(r, cmd_info("exit",         "exit", exit_cmd));
+    add_cmd(r, cmd_info("exit",          "exit", exit_cmd));
-    add_cmd(r, cmd_info("print",        "print a string", print_cmd));
+    add_cmd(r, cmd_info("print",         "print a string", print_cmd));
-    add_cmd(r, cmd_info("section",      "open a new section", section_cmd));
+    add_cmd(r, cmd_info("section",       "open a new section", section_cmd));
-    add_cmd(r, cmd_info("context",      "open a new context", context_cmd));
+    add_cmd(r, cmd_info("context",       "open a new context", context_cmd));
-    add_cmd(r, cmd_info("namespace",    "open a new namespace", namespace_cmd));
+    add_cmd(r, cmd_info("namespace",     "open a new namespace", namespace_cmd));
-    add_cmd(r, cmd_info("end",          "close the current namespace/section", end_scoped_cmd));
+    add_cmd(r, cmd_info("end",           "close the current namespace/section", end_scoped_cmd));
-    add_cmd(r, cmd_info("check",        "type check given expression, and display its type", check_cmd));
+    add_cmd(r, cmd_info("check",         "type check given expression, and display its type", check_cmd));
-    add_cmd(r, cmd_info("eval",         "evaluate given expression", eval_cmd));
+    add_cmd(r, cmd_info("eval",          "evaluate given expression", eval_cmd));
-    add_cmd(r, cmd_info("coercion",     "add a new coercion", coercion_cmd));
+    add_cmd(r, cmd_info("coercion",      "add a new coercion", coercion_cmd));
-    add_cmd(r, cmd_info("reducible",    "mark definitions as reducible/irreducible for automation", reducible_cmd));
+    add_cmd(r, cmd_info("reducible",     "mark definitions as reducible/irreducible for automation", reducible_cmd));
-    add_cmd(r, cmd_info("irreducible",  "mark definitions as irreducible for automation", irreducible_cmd));
+    add_cmd(r, cmd_info("irreducible",   "mark definitions as irreducible for automation", irreducible_cmd));
-    add_cmd(r, cmd_info("find_decl",    "find definitions and/or theorems", find_cmd));
+    add_cmd(r, cmd_info("find_decl",     "find definitions and/or theorems", find_cmd));
-    add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd));
+    add_cmd(r, cmd_info("#erase_cache",  "erase cached definition (for debugging purposes)", erase_cache_cmd));
-    add_cmd(r, cmd_info("#projections", "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
+    add_cmd(r, cmd_info("#projections",  "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
+    add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd));
 
     register_decl_cmds(r);
     register_inductive_cmd(r);

src/frontends/lean/token_table.cpp

@@ -91,7 +91,7 @@ void init_token_table(token_table & t) {
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "find_decl",
-         "include", "omit", "#erase_cache", "#projections", nullptr};
+         "include", "omit", "#erase_cache", "#projections", "#telescope_eq", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

src/library/definitional/util.cpp

@@ -6,8 +6,10 @@ Author: Leonardo de Moura
 */
 #include "kernel/find_fn.h"
 #include "kernel/instantiate.h"
+#include "kernel/abstract.h"
 #include "kernel/type_checker.h"
 #include "kernel/inductive/inductive.h"
+#include "library/locals.h"
 
 namespace lean {
 /** \brief Return true if environment has a constructor named \c c that returns
@@ -145,6 +147,10 @@ static name * g_prod_mk_name = nullptr;
 static name * g_pr1_name = nullptr;
 static name * g_pr2_name = nullptr;
 
+static name * g_eq_name = nullptr;
+static name * g_eq_refl_name = nullptr;
+static name * g_eq_rec_name = nullptr;
+
 void initialize_definitional_util() {
     g_true           = new expr(mk_constant("true"));
     g_true_intro     = new expr(mk_constant(name({"true", "intro"})));
@@ -159,6 +165,10 @@ void initialize_definitional_util() {
     g_prod_mk_name   = new name{"prod", "mk"};
     g_pr1_name       = new name{"prod", "pr1"};
     g_pr2_name       = new name{"prod", "pr2"};
+
+    g_eq_name        = new name("eq");
+    g_eq_refl_name   = new name{"eq", "refl"};
+    g_eq_rec_name    = new name{"eq", "rec"};
 }
 
 void finalize_definitional_util() {
@@ -174,6 +184,9 @@ void finalize_definitional_util() {
     delete g_prod_mk_name;
     delete g_pr1_name;
     delete g_pr2_name;
+    delete g_eq_name;
+    delete g_eq_refl_name;
+    delete g_eq_rec_name;
 }
 
 expr mk_true() {
@@ -246,4 +259,66 @@ expr mk_pair(type_checker & tc, expr const & a, expr const & b, bool prop) {
 }
 expr mk_pr1(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_left(tc, p) : mk_pr1(tc, p); }
 expr mk_pr2(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_right(tc, p) : mk_pr2(tc, p); }
+
+expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs) {
+    expr A    = tc.infer(lhs).first;
+    level lvl = sort_level(tc.ensure_type(A).first);
+    return mk_app(mk_constant(*g_eq_name, {lvl}), A, lhs, rhs);
+}
+
+void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> const & s, buffer<expr> & eqs) {
+    lean_assert(t.size() == s.size());
+    lean_assert(std::all_of(t.begin(), t.end(), is_local));
+    lean_assert(std::all_of(s.begin(), s.end(), is_local));
+    lean_assert(inductive::has_dep_elim(tc.env(), *g_eq_name));
+    buffer<buffer<expr>> t_aux;
+    name e_name("e");
+    for (unsigned i = 0; i < t.size(); i++) {
+        expr t_i = t[i];
+        expr s_i = s[i];
+        expr t_i_ty   = mlocal_type(t_i);
+        expr t_i_ty_a = abstract_locals(t_i_ty, i, t.data());
+        t_aux.push_back(buffer<expr>());
+        t_aux.back().push_back(t_i);
+        for (unsigned j = 0; j < i; j++) {
+            if (depends_on(t_i_ty, t[j])) {
+                // we need to "cast"
+                buffer<expr> ty_inst_args;
+                for (unsigned k = 0; k <= j; k++)
+                    ty_inst_args.push_back(s[k]);
+                for (unsigned k = j + 1; k < i; k++)
+                    ty_inst_args.push_back(t_aux[k][j+1]);
+                lean_assert(ty_inst_args.size() == i);
+                expr t_i_ty = instantiate_rev(t_i_ty_a, i, ty_inst_args.data());
+                buffer<expr> rec_args;
+                rec_args.push_back(mlocal_type(s[j]));
+                rec_args.push_back(t_aux[j][j]);
+                rec_args.push_back(Fun(s[j], Fun(eqs[j], t_i_ty))); // type former ("promise")
+                rec_args.push_back(t_i); // minor premise
+                rec_args.push_back(s[j]);
+                rec_args.push_back(eqs[j]);
+                level rec_l1 = sort_level(tc.ensure_type(t_i_ty).first);
+                level rec_l2 = sort_level(tc.ensure_type(mlocal_type(s[j])).first);
+                t_i = mk_app(mk_constant(*g_eq_rec_name, {rec_l1, rec_l2}), rec_args.size(), rec_args.data());
+            }
+            t_aux.back().push_back(t_i);
+        }
+        expr eq = mk_local(tc.mk_fresh_name(), e_name.append_after(i+1), mk_eq(tc, t_i, s_i), binder_info());
+        eqs.push_back(eq);
+    }
+}
+
+void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> & eqs) {
+    lean_assert(std::all_of(t.begin(), t.end(), is_local));
+    lean_assert(inductive::has_dep_elim(tc.env(), *g_eq_name));
+    buffer<expr> s;
+    for (unsigned i = 0; i < t.size(); i++) {
+        expr ty = mlocal_type(t[i]);
+        ty = abstract_locals(ty, i, t.data());
+        ty = instantiate_rev(ty, i, s.data());
+        expr local = mk_local(tc.mk_fresh_name(), local_pp_name(t[i]).append_after("'"), ty, local_info(t[i]));
+        s.push_back(local);
+    }
+    return mk_telescopic_eq(tc, t, s, eqs);
+}
 }

src/library/definitional/util.h

@@ -74,6 +74,15 @@ expr mk_pair(type_checker & tc, expr const & a, expr const & b, bool prop);
 expr mk_pr1(type_checker & tc, expr const & p, bool prop);
 expr mk_pr2(type_checker & tc, expr const & p, bool prop);
 
+expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs);
+
+/** \brief Create a telescope equality for HoTT library.
+    This procedure assumes eq supports dependent elimination.
+    For HoTT, we can't use heterogeneous equality.
+*/
+void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> const & s, buffer<expr> & eqs);
+void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> & eqs);
+
 void initialize_definitional_util();
 void finalize_definitional_util();
 }

src/shell/CMakeLists.txt

@@ -50,6 +50,15 @@ FOREACH(T ${LEANRUNTESTS})
            COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME})
 ENDFOREACH(T)
 
+# LEAN RUN HoTT TESTS
+file(GLOB LEANRUNHTESTS "${LEAN_SOURCE_DIR}/../tests/lean/hott/*.hlean")
+FOREACH(T ${LEANRUNHTESTS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leanhotttest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/hott"
+           COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME})
+ENDFOREACH(T)
+
 if("${MULTI_THREAD}" MATCHES "ON")
 # LEAN INTERACTIVE TESTS
 file(GLOB LEANITTESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.input")

tests/lean/hott/tele.hlean

@@ -0,0 +1,16 @@
+-- check @eq.rec
+-- universe variable l_1
+-- variables {A A' : Type.{l_1}} {e_1 : A = A'} {a : A}
+-- check @eq.rec.{l_1 l_1+1} Type.{l_1} A (fun (A' : Type.{l_1}) (e_1 : A = A'), A') a A' e_1
+open nat
+
+inductive vec (A : Type) : nat → Type :=
+nil {} : vec A zero,
+cons   : Π {n}, A → vec A n → vec A (succ n)
+
+structure S (A : Type) (a : A) (n : nat) (v : vec A n) :=
+mk :: (fa : A)
+
+set_option pp.implicit true
+
+#telescope_eq Π (A : Type) (a : A) (b : A) (c : nat) (d : vec A c) (e : S A a c d), nat

tests/lean/hott/test_single.sh

@@ -5,7 +5,7 @@ if [ $# -ne 2 ]; then
 fi
 ulimit -s 8192
 LEAN=$1
-export LEAN_PATH=.:../../../library/hott
+export HLEAN_PATH=../../../hott:.
 f=$2
 echo "-- testing $f"
 if $LEAN $f; then