From 6bc89f09168dd97ab31ee3587b66184a1ad20097 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Nov 2014 16:38:46 -0800 Subject: [PATCH] feat(library/definitional): define ibelow and below These are helper definitions for brec_on and binduction_on --- library/data/vector.lean | 20 +--- src/frontends/lean/inductive_cmd.cpp | 11 ++- src/library/definitional/brec_on.cpp | 139 +++++++++++++++++++++------ src/library/definitional/brec_on.h | 1 + src/library/definitional/util.cpp | 4 +- tests/lean/run/confuse_ind.lean | 3 +- tests/lean/run/forest.lean | 2 + tests/lean/run/ftree_brec.lean | 42 ++++---- tests/lean/run/tree.lean | 18 ++++ tests/lean/run/tree2.lean | 2 + tests/lean/run/tree3.lean | 2 + tests/lean/run/vector.lean | 24 ++--- 12 files changed, 179 insertions(+), 89 deletions(-) diff --git a/library/data/vector.lean b/library/data/vector.lean index b2b2b3c97..57d382ec6 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -114,23 +114,13 @@ namespace vector section universe variables l₁ l₂ variable {A : Type.{l₁}} - variable C : Π (n : nat), vector A n → Type.{l₂} - definition below {n : nat} (v : vector A n) := - rec_on v unit.{max 1 l₂} (λ (a₁ : A) (n₁ : nat) (v₁ : vector A n₁) (r₁ : Type.{max 1 l₂}), C n₁ v₁ × r₁) - - definition bw {n : nat} {A : Type} {C : Π (n : nat), vector A n → Type} (v : vector A n) := @below A C n v - end - - section - universe variables l₁ l₂ - variable {A : Type.{l₁}} - variable {C : Π (n : nat), vector A n → Type.{l₂}} - definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), below C v → C n v) : C n v := - have general : C n v × below C v, from + variable {C : Π (n : nat), vector A n → Type.{l₂+1}} + definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @below A C n v → C n v) : C n v := + have general : C n v × @below A C n v, from rec_on v (pair (H zero nil unit.star) unit.star) - (λ (a₁ : A) (n₁ : nat) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × below C v₁), - have b : below C (a₁ :: v₁), from + (λ (a₁ : A) (n₁ : nat) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @below A C n₁ v₁), + have b : @below A C _ (a₁ :: v₁), from r₁, have c : C (succ n₁) (a₁ :: v₁), from H (succ n₁) (a₁ :: v₁) b, diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 1483fb583..c9ffdbb09 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -695,7 +695,7 @@ struct inductive_cmd_fn { bool has_unit = has_unit_decls(env); bool has_eq = has_eq_decls(env); bool has_heq = has_heq_decls(env); - // bool has_prod = has_prod_decls(env); + bool has_prod = has_prod_decls(env); for (inductive_decl const & d : decls) { name const & n = inductive_decl_name(d); pos_info pos = *m_decl_pos_map.find(n); @@ -711,9 +711,12 @@ struct inductive_cmd_fn { 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)); - // } + if (has_prod) { + env = mk_below(env, inductive_decl_name(d)); + env = mk_ibelow(env, inductive_decl_name(d)); + save_if_defined(name{n, "below"}, pos); + save_if_defined(name(n, "ibelow"), pos); + } } } return env; diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp index 4017f240e..12136315f 100644 --- a/src/library/definitional/brec_on.cpp +++ b/src/library/definitional/brec_on.cpp @@ -8,7 +8,12 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" +#include "kernel/type_checker.h" #include "kernel/inductive/inductive.h" +#include "library/protected.h" +#include "library/reducible.h" +#include "library/module.h" +#include "library/bin_app.h" #include "library/definitional/util.h" namespace lean { @@ -16,12 +21,24 @@ static void throw_corrupted(name const & n) { throw exception(sstream() << "error in 'brec_on' generation, '" << n << "' inductive datatype declaration is corrupted"); } -environment mk_below(environment const & env, name const & n) { +static bool is_typeformer_app(buffer const & typeformer_names, expr const & e) { + expr const & fn = get_app_fn(e); + if (!is_local(fn)) + return false; + for (name const & n : typeformer_names) { + if (mlocal_name(fn) == n) + return true; + } + return false; +} + +static environment mk_below(environment const & env, name const & n, bool ibelow) { 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); @@ -32,29 +49,54 @@ environment mk_below(environment const & env, name const & n) { level_param_names lps = rec_decl.get_univ_params(); level lvl = mk_param_univ(head(lps)); // universe we are eliminating too levels lvls = param_names_to_levels(tail(lps)); - levels blvls = cons(lvl, lvls); - level rlvl = mk_max(mk_level_one(), lvl); // max 1 lvl: result universe of below - expr Type_max_1_l = mk_sort(rlvl); - buffer rec_args; - expr type = rec_decl.get_type(); - - name prod_name("prod"); - name unit_name("unit"); - expr inner_prod = mk_constant(prod_name, {lvl, rlvl}); - expr outer_prod = mk_constant(prod_name, {rlvl, rlvl}); - expr unit = mk_constant(unit_name, {rlvl}); - - to_telescope(ngen, type, rec_args); - if (rec_args.size() != nparams + ntypeformers + nminors + nindices + 1) + levels blvls; + level rlvl; + name prod_name; + expr unit, outer_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). + expr ref_type; + if (ibelow) { + // we are eliminating to Prop + blvls = lvls; + rlvl = mk_level_zero(); + unit = mk_constant("true"); + prod_name = name("and"); + outer_prod = mk_constant(prod_name); + ref_type = instantiate_univ_param(rec_decl.get_type(), param_id(lvl), mk_level_zero()); + } else { + 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); + 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)); + } + expr Type_result = mk_sort(rlvl); + buffer ref_args; + to_telescope(ngen, ref_type, ref_args); + if (ref_args.size() != nparams + ntypeformers + nminors + nindices + 1) throw_corrupted(n); - buffer args; - for (unsigned i = 0; i < nparams + ntypeformers; i++) - args.push_back(rec_args[i]); - // we ignore minor premises in the below type - for (unsigned i = nparams + ntypeformers + nminors; i < rec_args.size(); i++) - args.push_back(rec_args[i]); - // create recursor application + // args contains the below/ibelow 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])); + } + // we ignore minor premises in below/ibelow + for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++) + args.push_back(ref_args[i]); + + // We define below/ibelow using the recursor for this type levels rec_lvls = cons(mk_succ(rlvl), lvls); expr rec = mk_constant(rec_decl.get_name(), rec_lvls); for (unsigned i = 0; i < nparams; i++) @@ -63,27 +105,60 @@ environment mk_below(environment const & env, name const & n) { for (unsigned i = nparams; i < nparams + ntypeformers; i++) { buffer targs; to_telescope(ngen, mlocal_type(args[i]), targs); - rec = mk_app(rec, Fun(targs, Type_max_1_l)); + rec = mk_app(rec, Fun(targs, Type_result)); } // add minor premises for (unsigned i = nparams + ntypeformers; i < nparams + ntypeformers + nminors; i++) { - // TODO(Leo) + expr minor = ref_args[i]; + expr minor_type = mlocal_type(minor); + buffer minor_args; + minor_type = to_telescope(ngen, minor_type, minor_args); + buffer prod_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 (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)); + expr inner_prod; + if (ibelow) { + inner_prod = outer_prod; // and + } else { + 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 new_arg = mk_bin_rop(outer_prod, unit, prod_pairs.size(), prod_pairs.data()); + rec = mk_app(rec, Fun(minor_args, new_arg)); } + // add indices and major premise for (unsigned i = nparams + ntypeformers; i < args.size(); i++) { rec = mk_app(rec, args[i]); } - - name below_name = name{n, "below"}; - expr below_type = Pi(args, Type_max_1_l); + name below_name = ibelow ? name{n, "ibelow"} : name{n, "below"}; + expr below_type = Pi(args, Type_result); expr below_value = Fun(args, rec); - // TODO(Leo): declare below - std::cout << " >> " << below_name << "\n"; - std::cout << " " << below_type << "\n"; - std::cout << " " << below_value << "\n"; + 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, + 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); + return add_protected(new_env, below_name); +} - return env; +environment mk_below(environment const & env, name const & n) { + return mk_below(env, n, false); +} + +environment mk_ibelow(environment const & env, name const & n) { + return mk_below(env, n, true); } } diff --git a/src/library/definitional/brec_on.h b/src/library/definitional/brec_on.h index a1064f76f..262709e7a 100644 --- a/src/library/definitional/brec_on.h +++ b/src/library/definitional/brec_on.h @@ -12,4 +12,5 @@ namespace lean { 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); } diff --git a/src/library/definitional/util.cpp b/src/library/definitional/util.cpp index 5d853f0f4..c17c30e14 100644 --- a/src/library/definitional/util.cpp +++ b/src/library/definitional/util.cpp @@ -88,7 +88,7 @@ expr to_telescope(name_generator & ngen, expr type, buffer & telescope, op if (binfo) local = mk_local(ngen.next(), binding_name(type), binding_domain(type), *binfo); else - local = mk_local(ngen.next(), binding_name(type), binding_domain(type), binder_info(type)); + local = mk_local(ngen.next(), binding_name(type), binding_domain(type), binding_info(type)); telescope.push_back(local); type = instantiate(binding_body(type), local); } @@ -102,7 +102,7 @@ expr to_telescope(type_checker & tc, expr type, buffer & telescope, option if (binfo) local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), *binfo); else - local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), binder_info(type)); + local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), binding_info(type)); telescope.push_back(local); type = tc.whnf(instantiate(binding_body(type), local)).first; } diff --git a/tests/lean/run/confuse_ind.lean b/tests/lean/run/confuse_ind.lean index e2fd83b5c..6df5c3a42 100644 --- a/tests/lean/run/confuse_ind.lean +++ b/tests/lean/run/confuse_ind.lean @@ -4,7 +4,8 @@ definition mk_arrow (A : Type) (B : Type) := A → A → B inductive confuse (A : Type) := -lean : confuse A, +leaf1 : confuse A, +leaf2 : num → confuse A, node : mk_arrow A (confuse A) → confuse A check confuse.cases_on diff --git a/tests/lean/run/forest.lean b/tests/lean/run/forest.lean index 1fca1dc33..3215cc578 100644 --- a/tests/lean/run/forest.lean +++ b/tests/lean/run/forest.lean @@ -7,6 +7,7 @@ with forest : Type := nil : forest A, cons : tree A → forest A → forest A +namespace manual definition tree.below.{l₁ l₂} (A : Type.{l₁}) (C₁ : tree A → Type.{l₂}) @@ -106,3 +107,4 @@ have general : prod.{l₂ (max 1 l₂)} (C₂ f) (forest.below A C₁ C₂ f), f F₂ (forest.cons t f) b, prod.mk.{l₂ (max 1 l₂)} c b), pr₁ general +end manual diff --git a/tests/lean/run/ftree_brec.lean b/tests/lean/run/ftree_brec.lean index 2be3c8aa8..5edbf08c0 100644 --- a/tests/lean/run/ftree_brec.lean +++ b/tests/lean/run/ftree_brec.lean @@ -4,8 +4,12 @@ inductive ftree (A : Type) (B : Type) : Type := leafa : ftree A B, node : (A → B → ftree A B) → (B → ftree A B) → ftree A B +set_option pp.universes true +check @ftree + namespace ftree +namespace manual definition below.{l l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (C : ftree A B → Type.{l+1}) (t : ftree A B) : Type.{max l₁ l₂ (l+1)} := @rec.{(max l₁ l₂ (l+1))+1 l₁ l₂} @@ -45,30 +49,31 @@ 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) - (F : Π (t : ftree A B), below C t → C t) + (F : Π (t : ftree A B), @below A B C t → C t) : C t := -have gen : prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (below C t), from +have gen : prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (@below A B C t), from @rec.{(max l₁ l₂ (l+1)) l₁ l₂} A B - (λ t : ftree A B, prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (below C t)) - (have b : below C (leafa A B), from + (λ t : ftree A B, prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (@below A B C t)) + (have b : @below A B C (leafa A B), from unit.star.{max l₁ l₂ (l+1)}, have c : C (leafa A B), from F (leafa A B) b, prod.mk.{(l+1) (max l₁ l₂ (l+1))} c b) (λ (f₁ : A → B → ftree A B) (f₂ : B → ftree A B) - (r₁ : Π (a : A) (b : B), prod.{(l+1) (max l₁ l₂ (l+1))} (C (f₁ a b)) (below C (f₁ a b))) - (r₂ : Π (b : B), prod.{(l+1) (max l₁ l₂ (l+1))} (C (f₂ b)) (below C (f₂ b))), + (r₁ : Π (a : A) (b : B), prod.{(l+1) (max l₁ l₂ (l+1))} (C (f₁ a b)) (@below A B C (f₁ a b))) + (r₂ : Π (b : B), prod.{(l+1) (max l₁ l₂ (l+1))} (C (f₂ b)) (@below A B C (f₂ b))), let fc₁ : Π (a : A) (b : B), C (f₁ a b) := λ (a : A) (b : B), prod.pr1 (r₁ a b) in - let fr₁ : Π (a : A) (b : B), below C (f₁ a b) := λ (a : A) (b : B), prod.pr2 (r₁ a b) in + let fr₁ : Π (a : A) (b : B), @below A B C (f₁ a b) := λ (a : A) (b : B), prod.pr2 (r₁ a b) in let fc₂ : Π (b : B), C (f₂ b) := λ (b : B), prod.pr1 (r₂ b) in - let fr₂ : Π (b : B), below C (f₂ b) := λ (b : B), prod.pr2 (r₂ b) in - have b : below C (node f₁ f₂), from + let fr₂ : Π (b : B), @below A B C (f₂ b) := λ (b : B), prod.pr2 (r₂ b) in + have b : @below A B C (node f₁ f₂), from prod.mk (prod.mk fc₁ fr₁) (prod.mk fc₂ fr₂), have c : C (node f₁ f₂), from F (node f₁ f₂) b, @@ -78,32 +83,31 @@ prod.pr1 gen definition binduction_on.{l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} {C : ftree A B → Prop} (t : ftree A B) - (F : Π (t : ftree A B), pbelow C t → C t) + (F : Π (t : ftree A B), @ibelow A B C t → C t) : C t := -have gen : C t ∧ pbelow C t, from +have gen : C t ∧ @ibelow A B C t, from @rec.{0 l₁ l₂} A B - (λ t : ftree A B, C t ∧ pbelow C t) - (have b : pbelow C (leafa A B), from + (λ t : ftree A B, C t ∧ @ibelow A B C t) + (have b : @ibelow A B C (leafa A B), from true.intro, have c : C (leafa A B), from F (leafa A B) b, and.intro c b) (λ (f₁ : A → B → ftree A B) (f₂ : B → ftree A B) - (r₁ : ∀ (a : A) (b : B), C (f₁ a b) ∧ pbelow C (f₁ a b)) - (r₂ : ∀ (b : B), C (f₂ b) ∧ pbelow C (f₂ b)), + (r₁ : ∀ (a : A) (b : B), C (f₁ a b) ∧ @ibelow A B C (f₁ a b)) + (r₂ : ∀ (b : B), C (f₂ b) ∧ @ibelow A B C (f₂ b)), let fc₁ : ∀ (a : A) (b : B), C (f₁ a b) := λ (a : A) (b : B), and.elim_left (r₁ a b) in - let fr₁ : ∀ (a : A) (b : B), pbelow C (f₁ a b) := λ (a : A) (b : B), and.elim_right (r₁ a b) in + let fr₁ : ∀ (a : A) (b : B), @ibelow A B C (f₁ a b) := λ (a : A) (b : B), and.elim_right (r₁ a b) in let fc₂ : ∀ (b : B), C (f₂ b) := λ (b : B), and.elim_left (r₂ b) in - let fr₂ : ∀ (b : B), pbelow C (f₂ b) := λ (b : B), and.elim_right (r₂ b) in - have b : pbelow C (node f₁ f₂), from + let fr₂ : ∀ (b : B), @ibelow A B C (f₂ b) := λ (b : B), and.elim_right (r₂ b) in + have b : @ibelow A B C (node f₁ f₂), from and.intro (and.intro fc₁ fr₁) (and.intro fc₂ fr₂), have c : C (node f₁ f₂), from F (node f₁ f₂) b, and.intro c b) t, and.elim_left gen - end ftree diff --git a/tests/lean/run/tree.lean b/tests/lean/run/tree.lean index 775268e98..caf4af0cb 100644 --- a/tests/lean/run/tree.lean +++ b/tests/lean/run/tree.lean @@ -11,6 +11,7 @@ star : one set_option pp.universes true namespace tree +namespace manual section universe variables l₁ l₂ variable {A : Type.{l₁}} @@ -35,6 +36,23 @@ namespace tree (c, b)), pr₁ general end +end manual + section + universe variables l₁ l₂ + variable {A : Type.{l₁}} + variable {C : tree A → Type.{l₂+1}} + definition below_rec_on (t : tree A) (H : Π (n : tree A), @below A C n → C n) : C t + := have general : C t × @below A C t, from + rec_on t + (λa, (H (leaf a) unit.star, unit.star)) + (λ (l r : tree A) (Hl : C l × @below A C l) (Hr : C r × @below A C r), + have b : @below A C (node l r), from + ((pr₁ Hl, pr₂ Hl), (pr₁ Hr, pr₂ Hr)), + have c : C (node l r), from + H (node l r) b, + (c, b)), + pr₁ general + end set_option pp.universes true diff --git a/tests/lean/run/tree2.lean b/tests/lean/run/tree2.lean index 80b8ae53b..7d1a6841e 100644 --- a/tests/lean/run/tree2.lean +++ b/tests/lean/run/tree2.lean @@ -11,6 +11,7 @@ star : one set_option pp.universes true namespace tree + namespace manual section universe variables l₁ l₂ variable {A : Type.{l₁}} @@ -35,6 +36,7 @@ namespace tree (c, b)), pr₁ general end + end manual check no_confusion diff --git a/tests/lean/run/tree3.lean b/tests/lean/run/tree3.lean index 40163f510..2d90f878d 100644 --- a/tests/lean/run/tree3.lean +++ b/tests/lean/run/tree3.lean @@ -11,6 +11,7 @@ star : one set_option pp.universes true namespace tree + namespace manual section universe variables l₁ l₂ variable {A : Type.{l₁}} @@ -35,6 +36,7 @@ namespace tree (c, b)), pr₁ general end + end manual check no_confusion diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean index 8a14f4ead..c2d1ea297 100644 --- a/tests/lean/run/vector.lean +++ b/tests/lean/run/vector.lean @@ -22,23 +22,13 @@ namespace vector section universe variables l₁ l₂ variable {A : Type.{l₁}} - variable C : Π (n : nat), vector A n → Type.{l₂} - definition below {n : nat} (v : vector A n) := - rec_on v unit.{max 1 l₂} (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : Type.{max 1 l₂}), C n₁ v₁ × r₁) - - definition bw {n : nat} {A : Type} {C : Π (n : nat), vector A n → Type} (v : vector A n) := @below A C n v - end - - section - universe variables l₁ l₂ - variable {A : Type.{l₁}} - variable {C : Π (n : nat), vector A n → Type.{l₂}} - definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), below C v → C n v) : C n v := - have general : C n v × below C v, from + variable {C : Π (n : nat), vector A n → Type.{l₂+1}} + definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @below A C n v → C n v) : C n v := + have general : C n v × @below A C n v, from rec_on v (pair (H zero vnil unit.star) unit.star) - (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × below C v₁), - have b : below C (vcons a₁ v₁), from + (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @below A C n₁ v₁), + have b : @below A C _ (vcons a₁ v₁), from r₁, have c : C (succ n₁) (vcons a₁ v₁), from H (succ n₁) (vcons a₁ v₁) b, @@ -48,6 +38,8 @@ namespace vector check brec_on + definition bw := @below + definition sum {n : nat} (v : vector nat n) : nat := brec_on v (λ (n : nat) (v : vector nat n), cases_on v @@ -68,7 +60,7 @@ namespace vector example : addk (1 :: 2 :: vnil) 3 = 4 :: 5 :: vnil := rfl - definition append {A : Type} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) := + definition append.{l} {A : Type.{l+1}} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) := brec_on w (λ (n : nat) (w : vector A n), cases_on w (λ (B : bw vnil), v)