From c61c049152833b455e7da7a02b73b0d876530522 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 May 2015 14:06:29 -0700 Subject: [PATCH] feat(library/user_recursors): generalize acceptable use-defined recursors see issue #492 --- src/emacs/lean-syntax.el | 3 +- src/frontends/lean/builtin_cmds.cpp | 30 +++-- src/frontends/lean/decl_cmds.cpp | 10 +- src/frontends/lean/token_table.cpp | 5 +- src/frontends/lean/tokens.cpp | 2 +- src/frontends/lean/tokens.txt | 2 +- src/library/user_recursors.cpp | 184 ++++++++++++++++------------ src/library/user_recursors.h | 30 +++-- src/util/CMakeLists.txt | 2 +- src/util/list_fn.h | 2 + tests/lean/hott/id_tac5.hlean | 14 +++ tests/lean/hott/ind_tac3.hlean | 12 ++ tests/lean/hott/ind_tac4.hlean | 6 + tests/lean/run/ind_tac1.lean | 5 + tests/lean/urec.lean.expected.out | 51 ++++---- 15 files changed, 230 insertions(+), 128 deletions(-) create mode 100644 tests/lean/hott/id_tac5.hlean create mode 100644 tests/lean/hott/ind_tac3.hlean create mode 100644 tests/lean/hott/ind_tac4.hlean create mode 100644 tests/lean/run/ind_tac1.lean diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 8e207d358..e97ef81db 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -123,11 +123,12 @@ "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]" "\[none\]" "\[decls\]" "\[declarations\]" "\[coercions\]" "\[classes\]" - "\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]" "\[recursor\]" + "\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]" "\[notations\]" "\[abbreviations\]" "\[begin-end-hints\]" "\[tactic-hints\]" "\[reduce-hints\]" "\[unfold-hints\]" "\[aliases\]" "\[eqv\]" "\[localrefinfo\]")) . 'font-lock-doc-face) (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) + (,(rx "\[recursor" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) (,(rx "\[unfold-c" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) ;; tactics ("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face)) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index c9c80e482..9d67de26c 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -230,17 +230,30 @@ static void print_inductive(parser & p, name const & n, pos_info const & pos) { static void print_recursor_info(parser & p) { name c = p.check_constant_next("invalid 'print [recursor]', constant expected"); + auto out = p.regular_stream(); recursor_info info = get_recursor_info(p.env(), c); - p.regular_stream() << "recursor information\n" - << " num. parameters: " << info.get_num_params() << "\n" - << " num. indices: " << info.get_num_indices() << "\n"; + out << "recursor information\n" + << " num. parameters: " << info.get_num_params() << "\n" + << " num. indices: " << info.get_num_indices() << "\n"; if (auto r = info.get_motive_univ_pos()) - p.regular_stream() << " motive univ. pos. : " << *r << "\n"; + out << " motive univ. pos.: " << *r << "\n"; else - p.regular_stream() << " recursor eliminate only to Prop\n"; - p.regular_stream() << " motive pos.: " << info.get_motive_pos() << "\n" - << " major premise pos.: " << info.get_major_pos() << "\n" - << " dep. elimination: " << info.has_dep_elim() << "\n"; + out << " recursor eliminate only to Prop\n"; + out << " motive pos.: " << info.get_motive_pos() + 1 << "\n" + << " major premise pos.: " << info.get_major_pos() + 1 << "\n" + << " dep. elimination: " << info.has_dep_elim() << "\n"; + if (info.get_num_params() > 0) { + out << " parameters pos. at major:"; + for (unsigned p : info.get_params_pos()) + out << " " << p+1; + out << "\n"; + } + if (info.get_num_indices() > 0) { + out << " indices pos. at major: "; + for (unsigned p : info.get_indices_pos()) + out << " " << p+1; + out << "\n"; + } } bool print_constant(parser & p, char const * kind, declaration const & d) { @@ -406,6 +419,7 @@ environment print_cmd(parser & p) { print_inductive(p, c, pos); } else if (p.curr_is_token(get_recursor_tk())) { p.next(); + p.check_token_next(get_rbracket_tk(), "invalid 'print [recursor]', ']' expected"); print_recursor_info(p); } else if (print_polymorphic(p)) { } else { diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index f36a6f359..4f2150d5e 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -361,6 +361,7 @@ struct decl_attributes { bool m_refl; bool m_subst; bool m_recursor; + optional m_recursor_major_pos; optional m_priority; optional m_unfold_c_hint; @@ -513,6 +514,13 @@ struct decl_attributes { m_subst = true; } else if (p.curr_is_token(get_recursor_tk())) { p.next(); + if (!p.curr_is_token(get_rbracket_tk())) { + unsigned r = p.parse_small_nat(); + if (r == 0) + throw parser_error("invalid '[recursor]' attribute, value must be greater than 0", pos); + m_recursor_major_pos = r - 1; + } + p.check_token_next(get_rbracket_tk(), "invalid 'recursor', ']' expected"); m_recursor = true; } else { break; @@ -570,7 +578,7 @@ struct decl_attributes { if (m_subst) env = add_subst(env, d, m_persistent); if (m_recursor) - env = add_user_recursor(env, d, m_persistent); + env = add_user_recursor(env, d, m_recursor_major_pos, m_persistent); if (m_is_class) env = add_class(env, d, m_persistent); if (m_has_multiple_instances) diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index b74ef6887..5411b0dc3 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -107,7 +107,7 @@ void init_token_table(token_table & t) { "definition", "example", "coercion", "abbreviation", "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]", - "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor]", + "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor", "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-f]", "[constructor]", "[unfold-c", "print", "end", "namespace", "section", "prelude", "help", @@ -117,7 +117,8 @@ void init_token_table(token_table & t) { "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", "multiple_instances", "find_decl", "attribute", "persistent", - "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq", nullptr}; + "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq", + nullptr}; pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index a59c78ada..c787d4491 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -244,7 +244,7 @@ void initialize_tokens() { g_trans_tk = new name{"[trans]"}; g_refl_tk = new name{"[refl]"}; g_subst_tk = new name{"[subst]"}; - g_recursor_tk = new name{"[recursor]"}; + g_recursor_tk = new name{"[recursor"}; g_attribute_tk = new name{"attribute"}; g_with_tk = new name{"with"}; g_class_tk = new name{"[class]"}; diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index cefc57779..42e8e94e5 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -106,7 +106,7 @@ symm [symm] trans [trans] refl [refl] subst [subst] -recursor [recursor] +recursor [recursor attribute attribute with with class [class] diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index 44586b690..ceff1361f 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -22,20 +22,25 @@ bool recursor_info::is_minor(unsigned pos) const { return true; } -recursor_info::recursor_info(name const & r, name const & I, unsigned num_params, unsigned num_indices, unsigned major, - optional const & motive_univ_pos, bool dep_elim): - m_recursor(r), m_type_name(I), m_num_params(num_params), m_num_indices(num_indices), m_major_pos(major), - m_motive_univ_pos(motive_univ_pos), m_dep_elim(dep_elim) {} +recursor_info::recursor_info(name const & r, name const & I, optional const & motive_univ_pos, + bool dep_elim, unsigned major_pos, list const & params_pos, + list const & indices_pos): + m_recursor(r), m_type_name(I), m_motive_univ_pos(motive_univ_pos), m_dep_elim(dep_elim), + m_major_pos(major_pos), m_params_pos(params_pos), m_indices_pos(indices_pos) {} recursor_info::recursor_info() {} void recursor_info::write(serializer & s) const { - s << m_recursor << m_type_name << m_num_params << m_num_indices << m_major_pos << m_motive_univ_pos << m_dep_elim; + s << m_recursor << m_type_name << m_motive_univ_pos << m_dep_elim << m_major_pos; + write_list(s, m_params_pos); + write_list(s, m_indices_pos); } recursor_info recursor_info::read(deserializer & d) { recursor_info info; - d >> info.m_recursor >> info.m_type_name >> info.m_num_params >> info.m_num_indices >> info.m_major_pos - >> info.m_motive_univ_pos >> info.m_dep_elim; + d >> info.m_recursor >> info.m_type_name >> info.m_motive_univ_pos >> info.m_dep_elim + >> info.m_major_pos; + info.m_params_pos = read_list(d); + info.m_indices_pos = read_list(d); return info; } @@ -47,30 +52,19 @@ static void throw_invalid_motive(expr const & C) { "and I is a constant"); } -static void throw_invalid_major(buffer const & tele, expr const & I, unsigned num_params, - unsigned num_indices, unsigned major_pos) { - sstream msg; - msg << "invalid user defined recursor, major premise '" << tele[major_pos] << "' is expected to have type " << I; - for (unsigned i = 0; i < num_params; i++) - msg << " " << tele[i]; - for (unsigned i = major_pos - num_indices; i < major_pos; i++) - msg << " " << tele[i]; - throw exception(msg); -} - -recursor_info mk_recursor_info(environment const & env, name const & r) { +recursor_info mk_recursor_info(environment const & env, name const & r, optional const & given_major_pos) { if (auto I = inductive::is_elim_rule(env, r)) { if (*inductive::get_num_type_formers(env, *I) > 1) throw exception(sstream() << "unsupported recursor '" << r << "', it has multiple motives"); optional motive_univ_pos; if (env.get(name(*I, "rec")).get_num_univ_params() != env.get(name(*I)).get_num_univ_params()) motive_univ_pos = 0; - return recursor_info(r, *I, - *inductive::get_num_params(env, *I), - *inductive::get_num_indices(env, *I), - *inductive::get_elim_major_idx(env, r), - motive_univ_pos, - inductive::has_dep_elim(env, *I)); + unsigned major_pos = *inductive::get_elim_major_idx(env, r); + unsigned num_indices = *inductive::get_num_indices(env, *I); + list params_pos = mk_list_range(0, *inductive::get_num_params(env, *I)); + list indices_pos = mk_list_range(major_pos - num_indices, major_pos); + return recursor_info(r, *I, motive_univ_pos, inductive::has_dep_elim(env, *I), + major_pos, params_pos, indices_pos); } declaration d = env.get(r); type_checker tc(env); @@ -78,22 +72,99 @@ recursor_info mk_recursor_info(environment const & env, name const & r) { expr rtype = to_telescope(tc, d.get_type(), tele); buffer C_args; expr C = get_app_args(rtype, C_args); - if (!is_local(C) || !std::all_of(C_args.begin(), C_args.end(), is_local) || C_args.empty()) { - throw exception("invalid user defined recursor, result type must be of the form (C i t), " - "where C and t are bound variables, and i is a (possibly empty) sequence of bound variables"); + if (!is_local(C) || !std::all_of(C_args.begin(), C_args.end(), is_local)) { + throw exception("invalid user defined recursor, result type must be of the form (C t), " + "where C is a bound variable, and t is a (possibly empty) sequence of bound variables"); } - unsigned num_indices = C_args.size() - 1; + + // Compute number of parameters. + // We assume a parameter is anything that occurs before the motive. unsigned num_params = 0; for (expr const & x : tele) { if (mlocal_name(x) == mlocal_name(C)) break; num_params++; } + + // Locate major premise, and check whether the recursor supports dependent elimination or not. + expr major; + unsigned major_pos = 0; + bool dep_elim; + if (given_major_pos) { + if (*given_major_pos >= tele.size()) + throw exception(sstream() << "invalid user defined recursor, invalid major premise position, " + "recursor has only " << tele.size() << "arguments"); + major = tele[*given_major_pos]; + major_pos = *given_major_pos; + if (!C_args.empty() && tc.is_def_eq(C_args.back(), major).first) + dep_elim = true; + else + dep_elim = false; + } else { + major = C_args.back(); + dep_elim = true; + for (expr const & x : tele) { + if (tc.is_def_eq(x, major).first) + break; + major_pos++; + } + } + + // Number of indices + unsigned num_indices = C_args.size(); + if (dep_elim) + num_indices--; // when we have dependent elimination, the last element is the major premise. + if (major_pos < num_indices) + throw exception(sstream() << "invalid user defined recursor, indices must occur before major premise '" + << major << "'"); + + buffer I_args; + expr I = get_app_args(mlocal_type(major), I_args); + if (!is_constant(I)) { + throw exception(sstream() << "invalid user defined recursor, type of the major premise '" << major + << "' must be for the form (I ...), where I is a constant"); + } + + // Store position of the recursor parameters in the major premise. + buffer params_pos; + for (unsigned i = 0; i < num_params; i++) { + expr const & A = tele[i]; + unsigned j = 0; + for (; j < I_args.size(); j++) { + if (tc.is_def_eq(I_args[j], A).first) + break; + } + if (j == I_args.size()) { + throw exception(sstream() << "invalid user defined recursor, type of the major premise '" << major + << "' does not contain the recursor parameter '" << A << "'"); + } + params_pos.push_back(j); + } + + // Store position of the recursor indices in the major premise + buffer indices_pos; + for (unsigned i = major_pos - num_indices; i < major_pos; i++) { + expr const & idx = tele[i]; + unsigned j = 0; + for (; j < I_args.size(); j++) { + if (tc.is_def_eq(I_args[j], idx).first) + break; + } + if (j == I_args.size()) { + throw exception(sstream() << "invalid user defined recursor, type of the major premise '" << major + << "' does not contain the recursor index '" << idx << "'"); + } + indices_pos.push_back(j); + } + + buffer C_tele; expr C_rtype = to_telescope(tc, mlocal_type(C), C_tele); if (!is_sort(C_rtype) || C_tele.size() != C_args.size()) { throw_invalid_motive(C); } + // Calculate position of the motive's universe. + // Remark: if we are in the standard environment, then the motive may be a proposition, and be fixed at 0. // The following pragma is for avoiding gcc bogus warning #if defined(__GNUC__) && !defined(__CLANG__) #pragma GCC diagnostic ignored "-Wmaybe-uninitialized" @@ -120,52 +191,8 @@ recursor_info mk_recursor_info(environment const & env, name const & r) { lean_assert(*C_univ_pos < length(d.get_univ_params())); } - buffer I_args; - expr I = get_app_args(mlocal_type(C_tele.back()), I_args); - if (!is_constant(I) || I_args.size() != num_params + num_indices) { - throw_invalid_motive(C); - } - for (unsigned i = 0; i < num_params; i++) { - if (!tc.is_def_eq(I_args[i], tele[i]).first) - throw_invalid_motive(C); - } - for (unsigned i = 0; i < num_indices; i++) { - if (!tc.is_def_eq(I_args[num_params + i], C_tele[i]).first) { - throw_invalid_motive(C); - } - } - expr const & major = C_args.back(); - unsigned major_pos = 0; - for (expr const & x : tele) { - if (mlocal_name(x) == mlocal_name(major)) - break; - major_pos++; - } - lean_assert(major_pos < tele.size()); - if (major_pos < num_indices) - throw exception(sstream() << "invalid user defined recursor, indices must occur before major premise '" - << major << "'"); - recursor_info info(r, const_name(I), num_params, num_indices, major_pos, C_univ_pos, true); - unsigned first_index_pos = info.get_first_index_pos(); - for (unsigned i = 0; i < num_indices; i++) { - if (!tc.is_def_eq(tele[first_index_pos+i], C_args[i]).first) { - throw exception(sstream() << "invalid user defined recursor, index '" << C_args[i] - << "' expected, but got '" << tele[i] << "'"); - } - } - buffer I_args_major; - expr I_major = get_app_args(mlocal_type(tele[major_pos]), I_args_major); - if (I != I_major) - throw_invalid_major(tele, I, num_params, num_indices, major_pos); - for (unsigned i = 0; i < num_params; i++) { - if (!tc.is_def_eq(I_args_major[i], tele[i]).first) - throw_invalid_major(tele, I, num_params, num_indices, major_pos); - } - for (unsigned i = 0; i < num_indices; i++) { - if (!tc.is_def_eq(I_args_major[num_params + i], tele[first_index_pos + i]).first) - throw_invalid_major(tele, I, num_params, num_indices, major_pos); - } - return info; + return recursor_info(r, const_name(I), C_univ_pos, dep_elim, major_pos, + to_list(params_pos), to_list(indices_pos)); } struct recursor_state { @@ -214,17 +241,18 @@ struct recursor_config { template class scoped_ext; typedef scoped_ext recursor_ext; -environment add_user_recursor(environment const & env, name const & r, bool persistent) { +environment add_user_recursor(environment const & env, name const & r, optional const & major_pos, + bool persistent) { if (inductive::is_elim_rule(env, r)) throw exception(sstream() << "invalid user defined recursor, '" << r << "' is a builtin recursor"); - recursor_info info = mk_recursor_info(env, r); + recursor_info info = mk_recursor_info(env, r, major_pos); return recursor_ext::add_entry(env, get_dummy_ios(), info, persistent); } recursor_info get_recursor_info(environment const & env, name const & r) { if (auto info = recursor_ext::get_state(env).m_recursors.find(r)) return *info; - return mk_recursor_info(env, r); + return mk_recursor_info(env, r, optional()); } list get_recursors_for(environment const & env, name const & I) { diff --git a/src/library/user_recursors.h b/src/library/user_recursors.h index 4a31c370e..b4a697871 100644 --- a/src/library/user_recursors.h +++ b/src/library/user_recursors.h @@ -11,25 +11,33 @@ namespace lean { class recursor_info { name m_recursor; name m_type_name; - unsigned m_num_params; - unsigned m_num_indices; - unsigned m_major_pos; optional m_motive_univ_pos; // if none, then recursor can only eliminate to Prop bool m_dep_elim; + unsigned m_major_pos; + list m_params_pos; // position of the recursor parameters in the major premise + list m_indices_pos; // position of the recursor indices in the major premise public: - recursor_info(name const & r, name const & I, unsigned num_params, unsigned num_indices, unsigned major, - optional const & motive_univ_pos, bool dep_elim); + recursor_info(name const & r, name const & I, + optional const & motive_univ_pos, + bool dep_elim, + unsigned major_pos, + list const & params_pos, + list const & indices_pos); recursor_info(); name const & get_name() const { return m_recursor; } name const & get_type_name() const { return m_type_name; } - unsigned get_num_params() const { return m_num_params; } - unsigned get_num_indices() const { return m_num_indices; } - unsigned get_motive_pos() const { return m_num_params; } - unsigned get_first_index_pos() const { return m_major_pos - m_num_indices; } + unsigned get_num_params() const { return length(m_params_pos); } + unsigned get_num_indices() const { return length(m_indices_pos); } + unsigned get_motive_pos() const { return get_num_params(); } + unsigned get_first_index_pos() const { return m_major_pos - get_num_indices(); } unsigned get_major_pos() const { return m_major_pos; } - optional get_motive_univ_pos() const { return m_motive_univ_pos; } + optional const & get_motive_univ_pos() const { return m_motive_univ_pos; } + /** \brief Return position of the recursor parameters in the major premise. */ + list const & get_params_pos() const { return m_params_pos; } + /** \brief Return position of the recursor indices in the major premise. */ + list const & get_indices_pos() const { return m_indices_pos; } bool has_dep_elim() const { return m_dep_elim; } bool is_minor(unsigned pos) const; @@ -37,7 +45,7 @@ public: static recursor_info read(deserializer & d); }; -environment add_user_recursor(environment const & env, name const & r, bool persistent); +environment add_user_recursor(environment const & env, name const & r, optional const & major_pos, bool persistent); recursor_info get_recursor_info(environment const & env, name const & r); list get_recursors_for(environment const & env, name const & I); diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index ebc53b331..2982f2112 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -4,6 +4,6 @@ add_library(util trace.cpp debug.cpp name.cpp name_set.cpp realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp thread_script_state.cpp bitap_fuzzy_search.cpp - init_module.cpp thread.cpp memory_pool.cpp utf8.cpp name_map.cpp) + init_module.cpp thread.cpp memory_pool.cpp utf8.cpp name_map.cpp list_fn.cpp) target_link_libraries(util ${LEAN_LIBS}) diff --git a/src/util/list_fn.h b/src/util/list_fn.h index 91a71708d..3ed994c27 100644 --- a/src/util/list_fn.h +++ b/src/util/list_fn.h @@ -302,4 +302,6 @@ template T const & get_ith(list const & l, unsigned idx) { return idx == 0 ? head(l) : get_ith(tail(l), idx - 1); } + +list mk_list_range(unsigned from, unsigned to); } diff --git a/tests/lean/hott/id_tac5.hlean b/tests/lean/hott/id_tac5.hlean new file mode 100644 index 000000000..e23ad67e1 --- /dev/null +++ b/tests/lean/hott/id_tac5.hlean @@ -0,0 +1,14 @@ +open equiv + +constant rec_on_ua {A B : Type} {P : A ≃ B → Type} + (f : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P f + +set_option pp.universes true +set_option pp.implicit true +set_option pp.notation false + +check @rec_on_ua + +attribute rec_on_ua [recursor] + +print [recursor] rec_on_ua diff --git a/tests/lean/hott/ind_tac3.hlean b/tests/lean/hott/ind_tac3.hlean new file mode 100644 index 000000000..ea604357f --- /dev/null +++ b/tests/lean/hott/ind_tac3.hlean @@ -0,0 +1,12 @@ +import cubical.pathover +open cubical + +set_option pp.implicit true +set_option pp.universes true +set_option pp.notation false + +check @idp_rec_on + +attribute idp_rec_on [recursor] + +print [recursor] idp_rec_on diff --git a/tests/lean/hott/ind_tac4.hlean b/tests/lean/hott/ind_tac4.hlean new file mode 100644 index 000000000..b35a6f49d --- /dev/null +++ b/tests/lean/hott/ind_tac4.hlean @@ -0,0 +1,6 @@ +import hit.circle +open circle + +attribute circle.elim_on [recursor 2] + +print [recursor] circle.elim_on diff --git a/tests/lean/run/ind_tac1.lean b/tests/lean/run/ind_tac1.lean new file mode 100644 index 000000000..ef4d534e4 --- /dev/null +++ b/tests/lean/run/ind_tac1.lean @@ -0,0 +1,5 @@ +check @heq.rec_on + +attribute heq.rec_on [recursor 6] + +print [recursor] heq.rec_on diff --git a/tests/lean/urec.lean.expected.out b/tests/lean/urec.lean.expected.out index 8ab087d2d..737b9ed49 100644 --- a/tests/lean/urec.lean.expected.out +++ b/tests/lean/urec.lean.expected.out @@ -1,43 +1,46 @@ -urec.lean:3:0: error: invalid user defined recursor, result type must be of the form (C i t), where C and t are bound variables, and i is a (possibly empty) sequence of bound variables +urec.lean:3:0: error: invalid user defined recursor, result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables urec.lean:5:0: error: invalid user defined recursor, 'nat.rec' is a builtin recursor -urec.lean:19:0: error: invalid user defined recursor, motive 'C' must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of bound variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant -urec.lean:23:0: error: invalid user defined recursor, resultant type of minor premise 'a' must be of the form (M ...) +urec.lean:19:0: error: invalid user defined recursor, type of the major premise 'a' must be for the form (I ...), where I is a constant myrec.{l_1 l_2} : Π (A : Type.{l_1}) (M : list.{l_1} A → Type.{l_2}) (l : list.{l_1} A), M (@nil.{l_1} A) → (Π (a : A), M [a]) → (Π (a₁ a₂ : A), M [a₁, a₂]) → M l recursor information - num. parameters: 1 - num. indices: 0 - motive univ. pos. : 1 - motive pos.: 1 - major premise pos.: 2 - dep. elimination: 1 + num. parameters: 1 + num. indices: 0 + motive univ. pos.: 1 + motive pos.: 2 + major premise pos.: 3 + dep. elimination: 1 + parameters pos. at major: 1 recursor information - num. parameters: 0 - num. indices: 0 + num. parameters: 0 + num. indices: 0 recursor eliminate only to Prop - motive pos.: 0 - major premise pos.: 1 - dep. elimination: 1 + motive pos.: 1 + major premise pos.: 2 + dep. elimination: 1 vector.induction_on.{l_1} : ∀ {A : Type.{l_1}} {C : Π (a : nat), vector.{l_1} A a → Prop} {a : nat} (n : vector.{l_1} A a), C nat.zero (@vector.nil.{l_1} A) → (∀ {n : nat} (a : A) (a_1 : vector.{l_1} A n), C n a_1 → C (nat.succ n) (@vector.cons.{l_1} A n a a_1)) → C a n recursor information - num. parameters: 1 - num. indices: 1 + num. parameters: 1 + num. indices: 1 recursor eliminate only to Prop - motive pos.: 1 - major premise pos.: 3 - dep. elimination: 1 + motive pos.: 2 + major premise pos.: 4 + dep. elimination: 1 + parameters pos. at major: 1 + indices pos. at major: 2 Exists.rec.{l_1} : ∀ {A : Type.{l_1}} {P : A → Prop} {C : Prop}, (∀ (a : A), P a → C) → @Exists.{l_1} A P → C recursor information - num. parameters: 2 - num. indices: 0 + num. parameters: 2 + num. indices: 0 recursor eliminate only to Prop - motive pos.: 2 - major premise pos.: 4 - dep. elimination: 0 + motive pos.: 3 + major premise pos.: 5 + dep. elimination: 0 + parameters pos. at major: 1 2