max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/constructions/brec_on): add brec_on and binduction_on for new inductive datatype module

Browse source 
We don't support these constructions for nested inductive types, but we
do for mutual inductives.
This commit is contained in:
Leonardo de Moura 2018-09-05 14:44:12 -07:00
parent f335623530
commit 208b932583
5 changed files with 220 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/inductive_cmds.cpp
View file

@ -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() {

201
src/library/constructions/brec_on.cpp
View file

@ -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<expr> 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<expr> args;
buffer<name> 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<expr> 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<expr> Fs;
name F_name("F");
for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) {
expr const & C = ref_args[i];
buffer<expr> 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<expr> 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<expr> minor_args;
minor_type = to_telescope(lctx, ngen, minor_type, minor_args);
buffer<expr> pairs;
for (expr & minor_arg : minor_args) {
buffer<expr> 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<expr> 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<expr> 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);
}}

2
src/library/constructions/brec_on.h
View file

@ -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);
}

2
tests/lean/run/new_inductive.lean
View file

@ -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}

8
tests/lean/run/new_inductive2.lean
View file

@ -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