From fca97d5bb219aa29d2f186695e09f0eee87c8634 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Dec 2014 10:39:22 -0800 Subject: [PATCH] feat(library/definitional): add brec_on construction, closes #272 --- library/init/datatypes.lean | 6 + library/init/logic.lean | 6 - src/frontends/lean/inductive_cmd.cpp | 22 +- src/library/definitional/brec_on.cpp | 242 +++++++++++++++--- src/library/definitional/brec_on.h | 6 +- src/library/definitional/util.cpp | 39 ++- src/library/definitional/util.h | 3 + .../lean/interactive/num2.input.expected.out | 6 + tests/lean/run/fib_brec.lean | 2 + tests/lean/run/ftree_brec.lean | 2 +- tests/lean/run/univ_problem.lean | 2 + tests/lean/run/vector.lean | 2 + 12 files changed, 278 insertions(+), 60 deletions(-) diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index a7b8f5bf2..8d50342f6 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -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 diff --git a/library/init/logic.lean b/library/init/logic.lean index d006c5a9e..c6d06da7d 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -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) diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index af8756ef8..96d007e33 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -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; } diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp index f69039b68..9c1352a36 100644 --- a/src/library/definitional/brec_on.cpp +++ b/src/library/definitional/brec_on.cpp @@ -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 const & typeformer_names, expr const & e) { +static optional is_typeformer_app(buffer const & typeformer_names, expr const & e) { expr const & fn = get_app_fn(e); if (!is_local(fn)) - return false; + return optional(); + unsigned r = 0; for (name const & n : typeformer_names) { if (mlocal_name(fn) == n) - return true; + return optional(r); + r++; } - return false; + return optional(); } 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 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 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)); + expr fst = mlocal_type(minor_arg); 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 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 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(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 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 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(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 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 minor_args; + minor_type = to_telescope(ngen, minor_type, minor_args); + buffer pairs; + for (expr & minor_arg : minor_args) { + buffer 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 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 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); +} } diff --git a/src/library/definitional/brec_on.h b/src/library/definitional/brec_on.h index 262709e7a..8103be656 100644 --- a/src/library/definitional/brec_on.h +++ b/src/library/definitional/brec_on.h @@ -9,8 +9,12 @@ Author: Leonardo de Moura namespace lean { /** \brief Given an inductive datatype \c n in \c env, add - n.brec_on (aka below recursion on) to the environment. + n.below auxiliary construction for n.brec_on + (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); } diff --git a/src/library/definitional/util.cpp b/src/library/definitional/util.cpp index 946aea5d4..4f3043ddb 100644 --- a/src/library/definitional/util.cpp +++ b/src/library/definitional/util.cpp @@ -132,12 +132,14 @@ expr to_telescope(type_checker & tc, expr type, buffer & 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); diff --git a/src/library/definitional/util.h b/src/library/definitional/util.h index b3afffba8..10a289cb6 100644 --- a/src/library/definitional/util.h +++ b/src/library/definitional/util.h @@ -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); diff --git a/tests/lean/interactive/num2.input.expected.out b/tests/lean/interactive/num2.input.expected.out index e4cbfc453..81e7502c8 100644 --- a/tests/lean/interactive/num2.input.expected.out +++ b/tests/lean/interactive/num2.input.expected.out @@ -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 diff --git a/tests/lean/run/fib_brec.lean b/tests/lean/run/fib_brec.lean index 71e53a5b4..2f2462c71 100644 --- a/tests/lean/run/fib_brec.lean +++ b/tests/lean/run/fib_brec.lean @@ -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), diff --git a/tests/lean/run/ftree_brec.lean b/tests/lean/run/ftree_brec.lean index 5edbf08c0..6cb01353b 100644 --- a/tests/lean/run/ftree_brec.lean +++ b/tests/lean/run/ftree_brec.lean @@ -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 diff --git a/tests/lean/run/univ_problem.lean b/tests/lean/run/univ_problem.lean index d846183a2..08d91e52b 100644 --- a/tests/lean/run/univ_problem.lean +++ b/tests/lean/run/univ_problem.lean @@ -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) := diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean index 019729dc6..5b381f9ce 100644 --- a/tests/lean/run/vector.lean +++ b/tests/lean/run/vector.lean @@ -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