From 208b932583db10dcbd3e30aeff54b818f4149d30 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Sep 2018 14:44:12 -0700 Subject: [PATCH] feat(library/constructions/brec_on): add `brec_on` and `binduction_on` for new inductive datatype module We don't support these constructions for nested inductive types, but we do for mutual inductives. --- src/frontends/lean/inductive_cmds.cpp | 7 + src/library/constructions/brec_on.cpp | 201 ++++++++++++++++++++++++++ src/library/constructions/brec_on.h | 2 + tests/lean/run/new_inductive.lean | 2 + tests/lean/run/new_inductive2.lean | 8 + 5 files changed, 220 insertions(+) diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 823196d4ab..6d52307bd1 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -755,6 +755,13 @@ public: m_env = mk_ibelow(m_env, ind_type.get_name()); } } + + for (inductive_type const & ind_type : ind_types) { + if (has_unit && has_prod) { + m_env = mk_brec_on(m_env, ind_type.get_name()); + m_env = mk_binduction_on(m_env, ind_type.get_name()); + } + } } environment inductive_cmd() { diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index 4757ce2944..75d5675dcf 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -464,4 +464,205 @@ environment mk_below(environment const & env, name const & n) { environment mk_ibelow(environment const & env, name const & n) { return mk_below(env, n, true); } + +static environment mk_brec_on(environment const & env, name const & n, bool ind) { + if (!is_recursive_datatype(env, n)) + return env; + if (is_inductive_predicate(env, n)) + return env; + local_ctx lctx; + constant_info ind_info = env.get(n); + inductive_val ind_val = ind_info.to_inductive_val(); + name_generator ngen = mk_constructions_name_generator(); + unsigned nparams = ind_val.get_nparams(); + constant_info rec_info = env.get(mk_rec_name(n)); + recursor_val rec_val = rec_info.to_recursor_val(); + unsigned nminors = rec_val.get_nminors(); + unsigned ntypeformers = rec_val.get_nmotives(); + unsigned nmutual = length(ind_val.get_all()); + if (ntypeformers != nmutual) { + /* The mutual declaration containing `n` contains nested inductive datatypes. + We don't support this kind of declaration here yet. We will probably never will :) + To support it, we will need to generate an auxiliary `below` for each nested inductive + type since their default `below` is not good here. For example, at + ``` + inductive term + | var : string -> term + | app : string -> list term -> term + ``` + The `list.below` is not useful since it will not allow us to recurse over the nested terms. + We need to generate another one using the auxiliary recursor `term.rec_1` for `list term`. + */ + return env; + } + names lps = rec_info.get_lparams(); + bool is_reflexive = ind_val.is_reflexive(); + level lvl = mk_univ_param(head(lps)); + levels lvls = lparams_to_levels(tail(lps)); + level rlvl; + names blps; + levels blvls; // universe level parameters of brec_on/binduction_on + // The arguments of brec_on (binduction_on) are the ones in the recursor - minor premises. + // The universe we map to is also different (l+1 for below of reflexive types) and (0 fo ibelow). + expr ref_type; + if (ind) { + // we are eliminating to Prop + blps = tail(lps); + blvls = lvls; + rlvl = mk_level_zero(); + ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_level_zero()); + } else if (is_reflexive) { + blps = lps; + blvls = cons(lvl, lvls); + rlvl = get_datatype_level(ind_info.get_type()); + // if rlvl is of the form (max 1 l), then rlvl <- l + if (is_max(rlvl) && is_one(max_lhs(rlvl))) + rlvl = max_rhs(rlvl); + rlvl = mk_max(mk_succ(lvl), rlvl); + // inner_prod, inner_prod_intro, pr1, pr2 do not use the same universe levels for + // reflective datatypes. + ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_succ(lvl)); + } else { + // we can simplify the universe levels for non-reflexive datatypes + blps = lps; + blvls = cons(lvl, lvls); + rlvl = mk_max(mk_level_one(), lvl); + ref_type = rec_info.get_type(); + } + buffer ref_args; + to_telescope(lctx, ngen, ref_type, ref_args); + lean_assert(ref_args.size() != nparams + ntypeformers + nminors + ind_val.get_nindices() + 1); + + // args contains the brec_on/binduction_on arguments + buffer args; + buffer typeformer_names; + // add parameters and typeformers + for (unsigned i = 0; i < nparams; i++) + args.push_back(ref_args[i]); + for (unsigned i = nparams; i < nparams + ntypeformers; i++) { + args.push_back(ref_args[i]); + typeformer_names.push_back(fvar_name(ref_args[i])); + } + // add indices and major premise + for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++) + args.push_back(ref_args[i]); + // create below terms (one per datatype) + // (below.{lvls} params type-formers) + // Remark: it also creates the result type + buffer belows; + expr result_type; + unsigned k = 0; + for (name const & n1 : ind_val.get_all()) { + if (n1 == n) { + result_type = ref_args[nparams + k]; + for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++) + result_type = mk_app(result_type, ref_args[i]); + } + k++; + name bname = name(n1, ind ? "ibelow" : "below"); + expr below = mk_constant(bname, blvls); + for (unsigned i = 0; i < nparams; i++) + below = mk_app(below, ref_args[i]); + for (unsigned i = nparams; i < nparams + ntypeformers; i++) + below = mk_app(below, ref_args[i]); + belows.push_back(below); + } + // create functionals (one for each type former) + // Pi idxs t, below idxs t -> C idxs t + buffer Fs; + name F_name("F"); + for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) { + expr const & C = ref_args[i]; + buffer F_args; + to_telescope(lctx, ngen, lctx.get_type(C), F_args); + expr F_result = mk_app(C, F_args); + expr F_below = mk_app(belows[j], F_args); + F_args.push_back(lctx.mk_local_decl(ngen, "f", F_below)); + expr F_type = lctx.mk_pi(F_args, F_result); + expr F = lctx.mk_local_decl(ngen, F_name.append_after(j+1), F_type); + Fs.push_back(F); + args.push_back(F); + } + + // We define brec_on/binduction_on using the recursor for this type + levels rec_lvls = cons(rlvl, lvls); + expr rec = mk_constant(rec_info.get_name(), rec_lvls); + // add parameters to rec + for (unsigned i = 0; i < nparams; i++) + rec = mk_app(rec, ref_args[i]); + // add type formers to rec + // Pi indices t, prod (C ... t) (below ... t) + for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) { + expr const & C = ref_args[i]; + buffer C_args; + to_telescope(lctx, ngen, lctx.get_type(C), C_args); + expr C_t = mk_app(C, C_args); + expr below_t = mk_app(belows[j], C_args); + type_checker tc(env, lctx); + expr prod = mk_pprod(tc, C_t, below_t, ind); + rec = mk_app(rec, lctx.mk_lambda(C_args, prod)); + } + // add minor premises to rec + for (unsigned i = nparams + ntypeformers, j = 0; i < nparams + ntypeformers + nminors; i++, j++) { + expr minor = ref_args[i]; + expr minor_type = lctx.get_type(minor); + buffer minor_args; + minor_type = to_telescope(lctx, ngen, minor_type, minor_args); + buffer pairs; + for (expr & minor_arg : minor_args) { + buffer minor_arg_args; + expr minor_arg_type = to_telescope(env, lctx, ngen, lctx.get_type(minor_arg), minor_arg_args); + if (auto k = is_typeformer_app(typeformer_names, minor_arg_type)) { + buffer C_args; + get_app_args(minor_arg_type, C_args); + type_checker tc(env, lctx); + expr new_minor_arg_type = mk_pprod(tc, minor_arg_type, mk_app(belows[*k], C_args), ind); + minor_arg = lctx.mk_local_decl(ngen, lctx.get_local_decl(minor_arg).get_user_name(), lctx.mk_pi(minor_arg_args, new_minor_arg_type)); + if (minor_arg_args.empty()) { + pairs.push_back(minor_arg); + } else { + type_checker tc(env, lctx); + expr r = mk_app(minor_arg, minor_arg_args); + expr r_1 = lctx.mk_lambda(minor_arg_args, mk_pprod_fst(tc, r, ind)); + expr r_2 = lctx.mk_lambda(minor_arg_args, mk_pprod_snd(tc, r, ind)); + pairs.push_back(mk_pprod_mk(tc, r_1, r_2, ind)); + } + } + } + type_checker tc(env, lctx); + expr b = foldr([&](expr const & a, expr const & b) { return mk_pprod_mk(tc, a, b, ind); }, + [&]() { return mk_unit_mk(rlvl, ind); }, + pairs.size(), pairs.data()); + unsigned F_idx = *is_typeformer_app(typeformer_names, minor_type); + expr F = Fs[F_idx]; + buffer F_args; + get_app_args(minor_type, F_args); + F_args.push_back(b); + expr new_arg = mk_pprod_mk(tc, mk_app(F, F_args), b, ind); + rec = mk_app(rec, lctx.mk_lambda(minor_args, new_arg)); + } + // add indices and major to rec + for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++) + rec = mk_app(rec, ref_args[i]); + + type_checker tc(env, lctx); + name brec_on_name = name(n, ind ? "binduction_on" : "brec_on"); + expr brec_on_type = lctx.mk_pi(args, result_type); + expr brec_on_value = lctx.mk_lambda(args, mk_pprod_fst(tc, rec, ind)); + + + declaration new_d = mk_definition_inferring_meta(env, brec_on_name, blps, brec_on_type, brec_on_value, + reducibility_hints::mk_abbreviation()); + environment new_env = module::add(env, new_d); + new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible, true); + new_env = add_aux_recursor(new_env, brec_on_name); + return add_protected(new_env, brec_on_name); } + +environment mk_brec_on(environment const & env, name const & n) { + return mk_brec_on(env, n, false); +} + +environment mk_binduction_on(environment const & env, name const & n) { + return mk_brec_on(env, n, true); +}} diff --git a/src/library/constructions/brec_on.h b/src/library/constructions/brec_on.h index bf24facbf6..3d7db9335e 100644 --- a/src/library/constructions/brec_on.h +++ b/src/library/constructions/brec_on.h @@ -21,4 +21,6 @@ environment old_mk_binduction_on(environment const & env, name const & n); environment mk_below(environment const & env, name const & n); environment mk_ibelow(environment const & env, name const & n); +environment mk_brec_on(environment const & env, name const & n); +environment mk_binduction_on(environment const & env, name const & n); } diff --git a/tests/lean/run/new_inductive.lean b/tests/lean/run/new_inductive.lean index bf3b15521e..f11c5aaa98 100644 --- a/tests/lean/run/new_inductive.lean +++ b/tests/lean/run/new_inductive.lean @@ -47,6 +47,8 @@ inductive rbnode (α : Type u) | red_node (lchild : rbnode) (val : α) (rchild : rbnode) : rbnode | black_node (lchild : rbnode) (val : α) (rchild : rbnode) : rbnode +#check @rbnode.brec_on + namespace rbnode variables {α : Type u} diff --git a/tests/lean/run/new_inductive2.lean b/tests/lean/run/new_inductive2.lean index 1422ea7018..03d72a382e 100644 --- a/tests/lean/run/new_inductive2.lean +++ b/tests/lean/run/new_inductive2.lean @@ -11,3 +11,11 @@ inductive foo #print foo.rec set_option pp.all true #print foo.below + +mutual inductive foo2, arrow2 +with foo2 : Type +| mk : arrow2 → foo2 +with arrow2 : Type +| mk : (nat → foo2) → arrow2 + +#print foo2.brec_on