From 4773a3be5fbde336468f2e2fb271c51e00cad9fc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Sep 2018 09:55:13 -0700 Subject: [PATCH] feat(library/constructions/no_confusion): add `no_confusion_type` for new inductive datatype module --- src/frontends/lean/elaborator.cpp | 24 +++- src/frontends/lean/inductive_cmds.cpp | 13 ++- src/frontends/lean/structure_cmd.cpp | 2 +- src/library/constructions/no_confusion.cpp | 121 ++++++++++++++++++++- src/library/constructions/no_confusion.h | 1 + src/library/inductive_compiler/basic.cpp | 2 +- src/library/util.cpp | 47 +++++++- src/library/util.h | 25 ++++- tests/lean/run/new_inductive.lean | 1 + 9 files changed, 218 insertions(+), 18 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index f4e9c47d87..6074ac4438 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -402,11 +402,25 @@ auto elaborator::get_elim_info_for_builtin(name const & fn) -> elim_info { only works for dependent elimination. */ lean_assert(!fn.is_atomic()); name const & I_name = fn.get_prefix(); - optional decl = inductive::is_inductive_decl(m_env, I_name); - lean_assert(decl); - unsigned nparams = decl->m_num_params; - unsigned nindices = *inductive::get_num_indices(m_env, I_name); - unsigned nminors = length(decl->m_intro_rules); + + unsigned nparams; + unsigned nindices; + unsigned nminors; + + // TODO(Leo): delete "then"-branch + if (optional decl = inductive::is_inductive_decl(m_env, I_name)) { + nparams = decl->m_num_params; + nindices = *inductive::get_num_indices(m_env, I_name); + nminors = length(decl->m_intro_rules); + } else { + constant_info I_info = m_env.get(I_name); + lean_assert(I_info.is_inductive()); + inductive_val I_val = I_info.to_inductive_val(); + nparams = I_val.get_nparams(); + nindices = I_val.get_nindices(); + nminors = length(I_val.get_cnstrs()); + } + elim_info r; if (fn.get_string() == "brec_on" || fn.get_string() == "binduction_on") { r.m_arity = nparams + 1 /* motive */ + nindices + 1 /* major */ + 1; diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 3381b5f95f..6257f4cfce 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -33,6 +33,7 @@ Authors: Daniel Selsam, Leonardo de Moura #include "library/tactic/tactic_evaluator.h" #include "library/constructions/cases_on.h" #include "library/constructions/rec_on.h" +#include "library/constructions/no_confusion.h" #include "frontends/lean/decl_cmds.h" #include "frontends/lean/decl_util.h" #include "frontends/lean/util.h" @@ -734,9 +735,19 @@ public: ind_types.push_back(inductive_type(local_name_p(r.m_inds[i]), Pi(r.m_params, local_type_p(r.m_inds[i])), constructors(cnstrs))); } m_env = m_env.add(mk_inductive_decl(names(m_lp_names), nat(num_params), inductive_types(ind_types), m_meta_info.m_modifiers.m_is_meta)); + + bool has_eq = has_eq_decls(m_env); + bool has_heq = has_heq_decls(m_env); + bool has_unit = has_punit_decls(m_env); + // bool has_prod = has_pprod_decls(m_env); + for (inductive_type const & ind_type : ind_types) { m_env = mk_rec_on(m_env, ind_type.get_name()); - m_env = mk_cases_on(m_env, ind_type.get_name()); + if (has_unit) { + m_env = mk_cases_on(m_env, ind_type.get_name()); + if (has_eq && has_heq) + m_env = mk_no_confusion(m_env, ind_type.get_name()); + } } } diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index c565814644..bc3682f368 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -1272,7 +1272,7 @@ struct structure_cmd_fn { return; if (!has_heq_decls(m_env)) return; - m_env = mk_no_confusion(m_env, m_name); + m_env = old_mk_no_confusion(m_env, m_name); name no_confusion_name(m_name, "no_confusion"); add_alias(no_confusion_name); } diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index 1720e8edbc..53267a1f45 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/inductive/inductive.h" #include "kernel/old_type_checker.h" +#include "kernel/type_checker.h" #include "library/protected.h" #include "library/module.h" #include "library/util.h" @@ -19,12 +20,14 @@ Author: Leonardo de Moura #include "library/aux_recursors.h" #include "library/constructions/util.h" +#include "library/trace.h" + namespace lean { static void throw_corrupted(name const & n) { throw exception(sstream() << "error in 'no_confusion' generation, '" << n << "' inductive datatype declaration is corrupted"); } -optional mk_no_confusion_type(environment const & env, name const & n) { +static optional old_mk_no_confusion_type(environment const & env, name const & n) { optional decl = inductive::is_inductive_decl(env, n); if (!decl) throw exception(sstream() << "error in 'no_confusion' generation, '" << n << "' is not an inductive datatype"); @@ -128,8 +131,8 @@ optional mk_no_confusion_type(environment const & env, name const & return some(add_protected(new_env, no_confusion_type_name)); } -environment mk_no_confusion(environment const & env, name const & n) { - optional env1 = mk_no_confusion_type(env, n); +environment old_mk_no_confusion(environment const & env, name const & n) { + optional env1 = old_mk_no_confusion_type(env, n); if (!env1) return env; environment new_env = *env1; @@ -238,4 +241,116 @@ environment mk_no_confusion(environment const & env, name const & n) { new_env = add_no_confusion(new_env, no_confusion_name); return add_protected(new_env, no_confusion_name); } + + +static optional mk_no_confusion_type(environment const & env, name const & n) { + constant_info ind_info = env.get(n); + if (!ind_info.is_inductive() || !can_elim_to_type(env, n)) + return optional(); + inductive_val ind_val = ind_info.to_inductive_val(); + local_ctx lctx; + name_generator ngen = mk_constructions_name_generator(); + unsigned nparams = ind_val.get_nparams(); + constant_info cases_info = env.get(name(n, "cases_on")); + names lps = cases_info.get_lparams(); + level plvl = mk_univ_param(head(lps)); + levels ilvls = lparams_to_levels(tail(lps)); + level rlvl = plvl; + expr ind_type = instantiate_type_lparams(ind_info, ilvls); + /* All inductive datatype parameters and indices are arguments */ + buffer args; + ind_type = to_telescope(lctx, ngen, ind_type, args, some(mk_implicit_binder_info())); + if (!is_sort(ind_type) || args.size() < nparams) + throw_corrupted(n); + level ind_lvl = sort_level(ind_type); + unsigned nindices = ind_val.get_nindices(); + lean_assert(nindices == args.size() - nparams); + /* Create inductive datatype */ + expr I = mk_app(mk_constant(n, ilvls), args); + /* Add (P : Type) */ + expr P = lctx.mk_local_decl(ngen, "P", mk_sort(plvl), mk_binder_info()); + args.push_back(P); + /* Add v1 and v2 elements of the inductive type */ + expr v1 = lctx.mk_local_decl(ngen, "v1", I, mk_binder_info()); + expr v2 = lctx.mk_local_decl(ngen, "v2", I, mk_binder_info()); + args.push_back(v1); + args.push_back(v2); + expr R = mk_sort(rlvl); + expr Pres = P; + name no_confusion_type_name{n, "no_confusion_type"}; + expr no_confusion_type_type = lctx.mk_pi(args, R); + /* Create type former */ + buffer type_former_args; + for (unsigned i = nparams; i < nparams + nindices; i++) + type_former_args.push_back(args[i]); + type_former_args.push_back(v1); + expr type_former = lctx.mk_lambda(type_former_args, R); + /* Create cases_on */ + levels clvls = levels(mk_succ(rlvl), ilvls); + expr cases_on = mk_app(mk_app(mk_constant(cases_info.get_name(), clvls), nparams, args.data()), type_former); + cases_on = mk_app(cases_on, nindices, args.data() + nparams); + expr cases_on1 = mk_app(cases_on, v1); + expr cases_on2 = mk_app(cases_on, v2); + expr t1 = type_checker(env, lctx).infer(cases_on1); + expr t2 = type_checker(env, lctx).infer(cases_on2); + buffer outer_cases_on_args; + unsigned idx1 = 0; + while (is_pi(t1)) { + buffer minor1_args; + expr minor1 = to_telescope(env, lctx, ngen, binding_domain(t1), minor1_args); + expr curr_t2 = t2; + buffer inner_cases_on_args; + unsigned idx2 = 0; + while (is_pi(curr_t2)) { + buffer minor2_args; + expr minor2 = to_telescope(env, lctx, ngen, binding_domain(curr_t2), minor2_args); + if (idx1 != idx2) { + // infeasible case, constructors do not match + inner_cases_on_args.push_back(lctx.mk_lambda(minor2_args, Pres)); + } else { + if (minor1_args.size() != minor2_args.size()) + throw_corrupted(n); + buffer rtype_hyp; + // add equalities + for (unsigned i = 0; i < minor1_args.size(); i++) { + expr lhs = minor1_args[i]; + expr rhs = minor2_args[i]; + expr lhs_type = lctx.get_type(lhs); + if (!type_checker(env, lctx).is_prop(lhs_type)) { + expr rhs_type = lctx.get_type(rhs); + level l = sort_level(type_checker(env, lctx).ensure_type(lhs_type)); + expr h_type; + if (type_checker(env, lctx).is_def_eq(lhs_type, rhs_type)) { + h_type = mk_app(mk_constant(get_eq_name(), levels(l)), lhs_type, lhs, rhs); + } else { + h_type = mk_app(mk_constant(get_heq_name(), levels(l)), lhs_type, lhs, rhs_type, rhs); + } + name lhs_user_name = lctx.get_local_decl(lhs).get_user_name(); + rtype_hyp.push_back(lctx.mk_local_decl(ngen, lhs_user_name.append_after("_eq"), h_type, mk_binder_info())); + } + } + inner_cases_on_args.push_back(lctx.mk_lambda(minor2_args, mk_arrow(lctx.mk_pi(rtype_hyp, P), Pres))); + } + idx2++; + curr_t2 = binding_body(curr_t2); + } + outer_cases_on_args.push_back(lctx.mk_lambda(minor1_args, mk_app(cases_on2, inner_cases_on_args))); + idx1++; + t1 = binding_body(t1); + } + expr no_confusion_type_value = lctx.mk_lambda(args, mk_app(cases_on1, outer_cases_on_args)); + declaration new_d = mk_definition_inferring_meta(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value, + reducibility_hints::mk_abbreviation()); + environment new_env = module::add(env, new_d); + new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible, true); + return some(add_protected(new_env, no_confusion_type_name)); +} + +environment mk_no_confusion(environment const & env, name const & n) { + optional env1 = mk_no_confusion_type(env, n); + if (!env1) + return env; + // TODO(Leo) + return *env1; +} } diff --git a/src/library/constructions/no_confusion.h b/src/library/constructions/no_confusion.h index 579241ecb9..c82c2b6109 100644 --- a/src/library/constructions/no_confusion.h +++ b/src/library/constructions/no_confusion.h @@ -15,5 +15,6 @@ namespace lean { If the environment has an impredicative Prop, it also assumes heq is defined. If the environment does not have an impredicative Prop, then it also assumes lift is defined. */ +environment old_mk_no_confusion(environment const & env, name const & n); environment mk_no_confusion(environment const & env, name const & n); } diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp index ee84ad0f81..c010ee69a9 100644 --- a/src/library/inductive_compiler/basic.cpp +++ b/src/library/inductive_compiler/basic.cpp @@ -91,7 +91,7 @@ class add_basic_inductive_decl_fn { if (gen_cases_on && gen_no_confusion && has_eq && has_heq) { lean_trace(name({"inductive_compiler"}), tout() << ">> generate no_confusion\n";); - m_env = mk_no_confusion(m_env, ind_name); + m_env = old_mk_no_confusion(m_env, ind_name); } if (gen_brec_on && has_prod) { diff --git a/src/library/util.cpp b/src/library/util.cpp index dd96b2b178..57b4ef4554 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -10,8 +10,10 @@ Author: Leonardo de Moura #include "kernel/find_fn.h" #include "kernel/instantiate.h" #include "kernel/old_type_checker.h" +#include "kernel/type_checker.h" #include "kernel/abstract.h" #include "kernel/abstract_type_context.h" +#include "kernel/inductive.h" #include "kernel/inductive/inductive.h" #include "library/error_msgs.h" #include "library/locals.h" @@ -272,10 +274,16 @@ bool is_inductive_predicate(environment const & env, name const & n) { } bool can_elim_to_type(environment const & env, name const & n) { - if (!inductive::is_inductive_decl(env, n)) - return false; // n is not inductive datatype + // TODO(Leo): delete following if-statement + if (inductive::is_inductive_decl(env, n)) { + constant_info ind_info = env.get(n); + constant_info rec_info = env.get(inductive::get_elim_name(n)); + return rec_info.get_num_lparams() > ind_info.get_num_lparams(); + } + constant_info ind_info = env.get(n); - constant_info rec_info = env.get(inductive::get_elim_name(n)); + if (!ind_info.is_inductive()) return false; + constant_info rec_info = env.get(mk_rec_name(n)); return rec_info.get_num_lparams() > ind_info.get_num_lparams(); } @@ -437,6 +445,39 @@ expr to_telescope(old_type_checker & ctx, expr type, buffer & telescope, o return type; } +expr to_telescope(bool pi, local_ctx & lctx, name_generator & ngen, expr e, buffer & telescope, optional const & binfo) { + while ((pi && is_pi(e)) || (!pi && is_lambda(e))) { + expr local; + if (binfo) + local = lctx.mk_local_decl(ngen, binding_name(e), binding_domain(e), *binfo); + else + local = lctx.mk_local_decl(ngen, binding_name(e), binding_domain(e), binding_info(e)); + telescope.push_back(local); + e = instantiate(binding_body(e), local); + } + return e; +} + +expr to_telescope(local_ctx & lctx, name_generator & ngen, expr const & type, buffer & telescope, optional const & binfo) { + return to_telescope(true, lctx, ngen, type, telescope, binfo); +} + +expr to_telescope(environment const & env, local_ctx & lctx, name_generator & ngen, expr type, buffer & telescope, optional const & binfo) { + expr new_type = type_checker(env, lctx).whnf(type); + while (is_pi(new_type)) { + type = new_type; + expr local; + if (binfo) + local = lctx.mk_local_decl(ngen, binding_name(type), binding_domain(type), *binfo); + else + local = lctx.mk_local_decl(ngen, binding_name(type), binding_domain(type), binding_info(type)); + telescope.push_back(local); + type = instantiate(binding_body(type), local); + new_type = type_checker(env, lctx).whnf(type); + } + return type; +} + /* ---------------------------------------------- Helper functions for creating basic operations diff --git a/src/library/util.h b/src/library/util.h index 6c29546fcb..81f71ca24f 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -141,24 +141,41 @@ unsigned get_expect_num_args(abstract_type_context & ctx, expr e); /** \brief "Consume" Pi-type \c type. This procedure creates local constants based on the domain of \c type and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given binder_info, otherwise the procedure uses the one attached in the domain. - The procedure returns the "body" of type. */ + The procedure returns the "body" of type. + + TODO(Leo): delete because it uses old APIs */ expr to_telescope(expr const & type, buffer & telescope, optional const & binfo = optional()); /** \brief "Consume" fun/lambda. This procedure creates local constants based on the arguments of \c e and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given binder_info, otherwise the procedure uses the one attached to the arguments. - The procedure returns the "body" of function. */ + The procedure returns the "body" of function. + + TODO(Leo): delete because it uses old APIs */ expr fun_to_telescope(expr const & e, buffer & telescope, optional const & binfo); -/** \brief Similar to previous procedure, but puts \c type in whnf */ +/** \brief Similar to previous procedure, but puts \c type in whnf + + TODO(Leo): delete because it uses old APIs */ expr to_telescope(old_type_checker & ctx, expr type, buffer & telescope, optional const & binfo = optional()); /** \brief Return the universe where inductive datatype resides - \pre \c ind_type is of the form Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl} */ + \pre \c ind_type is of the form Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl} + + TODO(Leo): delete because it uses old APIs */ level get_datatype_level(environment const & env, expr const & ind_type); +/** \brief "Consume" Pi-type `type`. This procedure creates free variables based on the domain of `type` using `lctx`, + and store them in telescope and updates . If `binfo` is provided, then the free variables are annotated with + the given `binder_info`, otherwise the procedure uses the one attached in the domain. + The procedure returns the "body" of type. */ +expr to_telescope(local_ctx & lctx, name_generator & ngen, expr const & type, buffer & telescope, optional const & binfo); + +/** \brief Similar to previous procedure, but uses whnf to check whether `type` reduces to `Pi` or not. */ +expr to_telescope(environment const & env, local_ctx & lctx, name_generator & ngen, expr type, buffer & telescope, optional const & binfo = optional()); + /** \brief Update the result sort of the given type */ expr update_result_sort(expr t, level const & l); diff --git a/tests/lean/run/new_inductive.lean b/tests/lean/run/new_inductive.lean index 06096d54fd..34f2d3e1db 100644 --- a/tests/lean/run/new_inductive.lean +++ b/tests/lean/run/new_inductive.lean @@ -20,6 +20,7 @@ inductive term (α : Type) (β : Type) | foo (p : nat → my_pair term (my_list term)) (n : β) : my_list (my_list term) → term #check @term.cases_on +#print term.no_confusion_type inductive arrow (α β : Type) | mk (s : nat → my_pair α β) : arrow