michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/definitional): add brec_on construction, closes #272

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-03 10:39:22 -08:00
parent f948241bb9
commit fca97d5bb2
12 changed files with 278 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/datatypes.lean
View file

@ -36,6 +36,12 @@ mk :: (pr1 : A) (pr2 : B)
inductive and (a b : Prop) : Prop :=
intro : a → b → and a b
definition and.elim_left {a b : Prop} (H : and a b) : a :=
and.rec (λa b, a) H
definition and.elim_right {a b : Prop} (H : and a b) : b :=
and.rec (λa b, b) H
inductive sum (A B : Type) : Type :=
inl : A → sum A B,
inr : B → sum A B

6
library/init/logic.lean
View file

@ -235,12 +235,6 @@ namespace and
theorem elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
rec H₂ H₁
definition elim_left (H : a ∧ b) : a :=
rec (λa b, a) H
definition elim_right (H : a ∧ b) : b :=
rec (λa b, b) H
theorem swap (H : a ∧ b) : b ∧ a :=
intro (elim_right H) (elim_left H)

22
src/frontends/lean/inductive_cmd.cpp
View file

@ -726,26 +726,36 @@ struct inductive_cmd_fn {
for (inductive_decl const & d : decls) {
name const & n = inductive_decl_name(d);
pos_info pos = *m_decl_pos_map.find(n);
env = mk_rec_on(env, inductive_decl_name(d));
env = mk_induction_on(env, inductive_decl_name(d));
env = mk_rec_on(env, n);
env = mk_induction_on(env, n);
save_def_info(name(n, "rec_on"), pos);
save_def_info(name(n, "induction_on"), pos);
if (has_unit) {
env = mk_cases_on(env, inductive_decl_name(d));
env = mk_cases_on(env, n);
save_def_info(name(n, "cases_on"), pos);
if (has_eq && has_heq) {
env = mk_no_confusion(env, inductive_decl_name(d));
env = mk_no_confusion(env, n);
save_if_defined(name{n, "no_confusion_type"}, pos);
save_if_defined(name(n, "no_confusion"), pos);
}
if (has_prod) {
env = mk_below(env, inductive_decl_name(d));
env = mk_ibelow(env, inductive_decl_name(d));
env = mk_below(env, n);
env = mk_ibelow(env, n);
save_if_defined(name{n, "below"}, pos);
save_if_defined(name(n, "ibelow"), pos);
}
}
}
for (inductive_decl const & d : decls) {
name const & n = inductive_decl_name(d);
pos_info pos = *m_decl_pos_map.find(n);
if (has_unit && has_prod) {
env = mk_brec_on(env, n);
env = mk_binduction_on(env, n);
save_if_defined(name{n, "brec_on"}, pos);
save_if_defined(name(n, "binduction_on"), pos);
}
}
return env;
}

240
src/library/definitional/brec_on.cpp
View file

@ -21,15 +21,17 @@ static void throw_corrupted(name const & n) {
throw exception(sstream() << "error in 'brec_on' generation, '" << n << "' inductive datatype declaration is corrupted");
}
static bool is_typeformer_app(buffer<name> const & typeformer_names, expr const & e) {
static optional<unsigned> is_typeformer_app(buffer<name> const & typeformer_names, expr const & e) {
expr const & fn = get_app_fn(e);
if (!is_local(fn))
return false;
return optional<unsigned>();
unsigned r = 0;
for (name const & n : typeformer_names) {
if (mlocal_name(fn) == n)
return true;
return optional<unsigned>(r);
r++;
}
return false;
return optional<unsigned>();
}
static environment mk_below(environment const & env, name const & n, bool ibelow) {
@ -48,49 +50,34 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
unsigned ntypeformers = length(std::get<2>(decls));
level_param_names lps = rec_decl.get_univ_params();
bool is_reflexive = is_reflexive_datatype(tc, n);
level lvl = mk_param_univ(head(lps)); // universe we are eliminating to
level lvl = mk_param_univ(head(lps));
levels lvls = param_names_to_levels(tail(lps));
levels blvls; // universe level parameters of ibelow/below
level_param_names blvls; // universe level parameters of ibelow/below
level rlvl; // universe level of the resultant type
name prod_name;
expr unit, outer_prod, inner_prod;
// The arguments of below (ibelow) are the ones in the recursor - minor premises.
// The universe we map to is also different (l+1 for below) and (0 fo ibelow).
// The universe we map to is also different (l+1 for below of reflexive types) and (0 fo ibelow).
expr ref_type;
expr Type_result;
if (ibelow) {
// we are eliminating to Prop
blvls = lvls;
blvls = tail(lps);
rlvl = mk_level_zero();
unit = mk_constant("true");
prod_name = name("and");
outer_prod = mk_constant(prod_name);
inner_prod = outer_prod;
ref_type = instantiate_univ_param(rec_decl.get_type(), param_id(lvl), mk_level_zero());
Type_result = mk_sort(rlvl);
} else if (is_reflexive) {
blvls = cons(lvl, lvls);
blvls = lps;
rlvl = get_datatype_level(ind_decl.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);
unit = mk_constant("unit", rlvl);
prod_name = name("prod");
outer_prod = mk_constant(prod_name, {rlvl, rlvl});
ref_type = instantiate_univ_param(rec_decl.get_type(), param_id(lvl), mk_succ(lvl));
Type_result = mk_sort(rlvl);
} else {
// we can simplify the universe levels for non-reflexive datatypes
blvls = cons(lvl, lvls);
blvls = lps;
rlvl = mk_max(mk_level_one(), lvl);
unit = mk_constant("unit", rlvl);
prod_name = name("prod");
outer_prod = mk_constant(prod_name, {rlvl, rlvl});
inner_prod = mk_constant(prod_name, {lvl, rlvl});
ref_type = rec_decl.get_type();
Type_result = mk_sort(rlvl);
}
Type_result = mk_sort(rlvl);
buffer<expr> ref_args;
to_telescope(ngen, ref_type, ref_args);
if (ref_args.size() != nparams + ntypeformers + nminors + nindices + 1)
@ -132,19 +119,15 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
buffer<expr> minor_arg_args;
expr minor_arg_type = to_telescope(tc, mlocal_type(minor_arg), minor_arg_args);
if (is_typeformer_app(typeformer_names, minor_arg_type)) {
expr r = minor_arg;
expr fst = mlocal_type(minor_arg);
expr snd = Pi(minor_arg_args, mk_app(r, minor_arg_args));
if (!ibelow && is_reflexive) {
// inner product is not constant
level fst_lvl = sort_level(tc.ensure_type(fst).first);
inner_prod = mk_constant(prod_name, {fst_lvl, rlvl});
}
prod_pairs.push_back(mk_app(inner_prod, fst, snd));
minor_arg = update_mlocal(minor_arg, Pi(minor_arg_args, Type_result));
expr snd = Pi(minor_arg_args, mk_app(minor_arg, minor_arg_args));
prod_pairs.push_back(mk_prod(tc, fst, snd, ibelow));
}
}
expr new_arg = mk_bin_rop(outer_prod, unit, prod_pairs.size(), prod_pairs.data());
expr new_arg = foldr([&](expr const & a, expr const & b) { return mk_prod(tc, a, b, ibelow); },
[&]() { return mk_unit(rlvl, ibelow); },
prod_pairs.size(), prod_pairs.data());
rec = mk_app(rec, Fun(minor_args, new_arg));
}
@ -159,7 +142,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(env, below_name, rec_decl.get_univ_params(), below_type, below_value,
declaration new_d = mk_definition(env, below_name, blvls, below_type, below_value,
opaque, rec_decl.get_module_idx(), use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, below_name, reducible_status::On);
@ -173,4 +156,189 @@ 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;
inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n);
type_checker tc(env);
name_generator ngen;
unsigned nparams = std::get<1>(decls);
declaration ind_decl = env.get(n);
declaration rec_decl = env.get(inductive::get_elim_name(n));
// declaration below_decl = env.get(name(n, ind ? "ibelow" : "below"));
unsigned nindices = *inductive::get_num_indices(env, n);
unsigned nminors = *inductive::get_num_minor_premises(env, n);
unsigned ntypeformers = length(std::get<2>(decls));
level_param_names lps = rec_decl.get_univ_params();
bool is_reflexive = is_reflexive_datatype(tc, n);
level lvl = mk_param_univ(head(lps));
levels lvls = param_names_to_levels(tail(lps));
level rlvl;
level_param_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_univ_param(rec_decl.get_type(), param_id(lvl), mk_level_zero());
} else if (is_reflexive) {
blps = lps;
blvls = cons(lvl, lvls);
rlvl = get_datatype_level(ind_decl.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_univ_param(rec_decl.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_decl.get_type();
}
buffer<expr> ref_args;
to_telescope(ngen, ref_type, ref_args);
if (ref_args.size() != nparams + ntypeformers + nminors + nindices + 1)
throw_corrupted(n);
// 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(mlocal_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 (auto const & decl : std::get<2>(decls)) {
name const & n1 = inductive::inductive_decl_name(decl);
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(ngen, mlocal_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(mk_local(ngen.next(), "f", F_below, binder_info()));
expr F_type = Pi(F_args, F_result);
expr F = mk_local(ngen.next(), F_name.append_after(j+1), F_type, binder_info());
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_decl.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(ngen, mlocal_type(C), C_args);
expr C_t = mk_app(C, C_args);
expr below_t = mk_app(belows[j], C_args);
expr prod = mk_prod(tc, C_t, below_t, ind);
rec = mk_app(rec, Fun(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 = mlocal_type(minor);
buffer<expr> minor_args;
minor_type = to_telescope(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(tc, mlocal_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);
expr new_minor_arg_type = mk_prod(tc, minor_arg_type, mk_app(belows[*k], C_args), ind);
minor_arg = update_mlocal(minor_arg, Pi(minor_arg_args, new_minor_arg_type));
if (minor_arg_args.empty()) {
pairs.push_back(minor_arg);
} else {
expr r = mk_app(minor_arg, minor_arg_args);
expr r_1 = Fun(minor_arg_args, mk_pr1(tc, r, ind));
expr r_2 = Fun(minor_arg_args, mk_pr2(tc, r, ind));
pairs.push_back(mk_pair(tc, r_1, r_2, ind));
}
}
}
expr b = foldr([&](expr const & a, expr const & b) { return mk_pair(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_pair(tc, mk_app(F, F_args), b, ind);
rec = mk_app(rec, Fun(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]);
name brec_on_name = name(n, ind ? "binduction_on" : "brec_on");
expr brec_on_type = Pi(args, result_type);
expr brec_on_value = Fun(args, mk_pr1(tc, rec, ind));
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(env, brec_on_name, blps, brec_on_type, brec_on_value,
opaque, rec_decl.get_module_idx(), use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, brec_on_name, reducible_status::On);
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);
}
}

6
src/library/definitional/brec_on.h
View file

@ -9,8 +9,12 @@ Author: Leonardo de Moura
namespace lean {
/** \brief Given an inductive datatype \c n in \c env, add
<tt>n.brec_on</tt> (aka below recursion on) to the environment.
<tt>n.below</tt> auxiliary construction for <tt>n.brec_on</t>
(aka below recursion on) to the environment.
*/
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);
}

39
src/library/definitional/util.cpp
View file

@ -132,12 +132,14 @@ expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, option
}
static expr * g_true = nullptr;
static expr * g_true_intro = nullptr;
static expr * g_and = nullptr;
static expr * g_and_intro = nullptr;
static expr * g_and_elim_left = nullptr;
static expr * g_and_elim_right = nullptr;
static name * g_unit = nullptr;
static name * g_unit_name = nullptr;
static name * g_unit_mk_name = nullptr;
static name * g_prod_name = nullptr;
static name * g_prod_mk_name = nullptr;
static name * g_pr1_name = nullptr;
@ -145,12 +147,14 @@ static name * g_pr2_name = nullptr;
void initialize_definitional_util() {
g_true = new expr(mk_constant("true"));
g_true_intro = new expr(mk_constant(name({"true", "intro"})));
g_and = new expr(mk_constant("and"));
g_and_intro = new expr(mk_constant({"and", "intro"}));
g_and_elim_left = new expr(mk_constant({"and", "elim_left"}));
g_and_elim_right = new expr(mk_constant({"and", "elim_right"}));
g_and_intro = new expr(mk_constant(name({"and", "intro"})));
g_and_elim_left = new expr(mk_constant(name({"and", "elim_left"})));
g_and_elim_right = new expr(mk_constant(name({"and", "elim_right"})));
g_unit = new name("unit");
g_unit_name = new name("unit");
g_unit_mk_name = new name{"unit", "star"};
g_prod_name = new name("prod");
g_prod_mk_name = new name{"prod", "mk"};
g_pr1_name = new name{"prod", "pr1"};
@ -159,11 +163,13 @@ void initialize_definitional_util() {
void finalize_definitional_util() {
delete g_true;
delete g_true_intro;
delete g_and;
delete g_and_intro;
delete g_and_elim_left;
delete g_and_elim_right;
delete g_unit;
delete g_unit_name;
delete g_unit_mk_name;
delete g_prod_name;
delete g_prod_mk_name;
delete g_pr1_name;
@ -174,6 +180,10 @@ expr mk_true() {
return *g_true;
}
expr mk_true_intro() {
return *g_true_intro;
}
expr mk_and(expr const & a, expr const & b) {
return mk_app(*g_and, a, b);
}
@ -193,7 +203,11 @@ expr mk_and_elim_right(type_checker & tc, expr const & H) {
}
expr mk_unit(level const & l) {
return mk_constant(*g_unit, {l});
return mk_constant(*g_unit_name, {l});
}
expr mk_unit_mk(level const & l) {
return mk_constant(*g_unit_mk_name, {l});
}
expr mk_prod(type_checker & tc, expr const & A, expr const & B) {
@ -214,14 +228,14 @@ expr mk_pr1(type_checker & tc, expr const & p) {
expr AxB = tc.whnf(tc.infer(p).first).first;
expr const & A = app_arg(app_fn(AxB));
expr const & B = app_arg(AxB);
return mk_app(mk_constant(*g_pr1_name, const_levels(AxB)), A, B, p);
return mk_app(mk_constant(*g_pr1_name, const_levels(get_app_fn(AxB))), A, B, p);
}
expr mk_pr2(type_checker & tc, expr const & p) {
expr AxB = tc.whnf(tc.infer(p).first).first;
expr const & A = app_arg(app_fn(AxB));
expr const & B = app_arg(AxB);
return mk_app(mk_constant(*g_pr2_name, const_levels(AxB)), A, B, p);
return mk_app(mk_constant(*g_pr2_name, const_levels(get_app_fn(AxB))), A, B, p);
}
expr mk_unit(level const & l, bool prop) {
@ -231,6 +245,13 @@ expr mk_unit(level const & l, bool prop) {
return mk_unit(l);
}
expr mk_unit_mk(level const & l, bool prop) {
if (prop)
return mk_true_intro();
else
return mk_unit_mk(l);
}
expr mk_prod(type_checker & tc, expr const & a, expr const & b, bool prop) {
if (prop)
return mk_and(a, b);

3
src/library/definitional/util.h
View file

@ -54,18 +54,21 @@ level get_datatype_level(expr ind_type);
expr instantiate_univ_param (expr const & e, name const & p, level const & l);
expr mk_true();
expr mk_true_intro();
expr mk_and(expr const & a, expr const & b);
expr mk_and_intro(type_checker & tc, expr const & Ha, expr const & Hb);
expr mk_and_elim_left(type_checker & tc, expr const & H);
expr mk_and_elim_right(type_checker & tc, expr const & H);
expr mk_unit(level const & l);
expr mk_unit_mk(level const & l);
expr mk_prod(type_checker & tc, expr const & A, expr const & B);
expr mk_pair(type_checker & tc, expr const & a, expr const & b);
expr mk_pr1(type_checker & tc, expr const & p);
expr mk_pr2(type_checker & tc, expr const & p);
expr mk_unit(level const & l, bool prop);
expr mk_unit_mk(level const & l, bool prop);
expr mk_prod(type_checker & tc, expr const & a, expr const & b, bool prop);
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);

6
tests/lean/interactive/num2.input.expected.out
View file

@ -9,6 +9,7 @@ pos_num.is_inhabited|inhabited pos_num
pos_num.is_one|pos_num → bool
pos_num.inc|pos_num → pos_num
pos_num.ibelow|pos_num → Prop
pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
pos_num.succ|pos_num → pos_num
pos_num.bit1|pos_num → pos_num
@ -22,6 +23,7 @@ pos_num.no_confusion_type|Type → pos_num → pos_num → Type
pos_num.num_bits|pos_num → pos_num
pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n
pos_num.add|pos_num → pos_num → pos_num
pos_num|Type
-- ENDFINDP
@ -36,6 +38,7 @@ pos_num.is_inhabited|inhabited pos_num
pos_num.is_one|pos_num → bool
pos_num.inc|pos_num → pos_num
pos_num.ibelow|pos_num → Prop
pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
pos_num.succ|pos_num → pos_num
pos_num.bit1|pos_num → pos_num
@ -48,6 +51,7 @@ pos_num.mul|pos_num → pos_num → pos_num
pos_num.no_confusion_type|Type → pos_num → pos_num → Type
pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n
pos_num.add|pos_num → pos_num → pos_num
pos_num|Type
-- ENDFINDP
@ -58,6 +62,7 @@ pos_num.is_inhabited|inhabited pos_num
pos_num.is_one|pos_num → bool
pos_num.inc|pos_num → pos_num
pos_num.ibelow|pos_num → Prop
pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
pos_num.succ|pos_num → pos_num
pos_num.bit1|pos_num → pos_num
@ -70,6 +75,7 @@ pos_num.mul|pos_num → pos_num → pos_num
pos_num.no_confusion_type|Type → pos_num → pos_num → Type
pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n
pos_num.add|pos_num → pos_num → pos_num
pos_num|Type
-- ENDFINDP

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

@ -2,6 +2,7 @@ import data.nat.basic data.prod
open prod
namespace nat
namespace manual
definition brec_on {C : nat → Type} (n : nat) (F : Π (n : nat), @below C n → C n) : C n :=
have general : C n × @below C n, from
rec_on n
@ -13,6 +14,7 @@ namespace nat
F (succ n₁) b,
pair c b),
pr₁ general
end manual
definition fib (n : nat) :=
brec_on n (λ (n : nat),

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

@ -49,7 +49,6 @@ definition pbelow.{l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (C : ftree A B
let p₂ : Prop := fc₂ ∧ fr₂ in
p₁ ∧ p₂)
t
end manual
definition brec_on.{l l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} {C : ftree A B → Type.{l+1}}
(t : ftree A B)
@ -110,4 +109,5 @@ have gen : C t ∧ @ibelow A B C t, from
and.intro c b)
t,
and.elim_left gen
end manual
end ftree

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

@ -9,6 +9,7 @@ namespace vector
print definition no_confusion
infixr `::` := vcons
namespace play
section
universe variables l₁ l₂
variable {A : Type.{l₁}}
@ -25,6 +26,7 @@ namespace vector
pair c b),
pr₁ general
end
end play
print "====================="
definition append {A : Type} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) :=

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

@ -22,6 +22,7 @@ namespace vector
set_option pp.universes true
check @below
namespace manual
section
universe variables l₁ l₂
variable {A : Type.{l₁}}
@ -38,6 +39,7 @@ namespace vector
pair c b),
pr₁ general
end
end manual
-- check brec_on