From c7f6a6b94e6216fba26ffb3b8b0aba41e20da787 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Oct 2014 17:22:02 -0700 Subject: [PATCH] feat(library/definitional/cases_on): automatically add 'cases_on' --- library/data/bool.lean | 3 - library/data/list/basic.lean | 4 - library/data/sum.lean | 2 - library/logic/eq.lean | 2 +- src/frontends/lean/inductive_cmd.cpp | 5 + src/library/definitional/CMakeLists.txt | 2 +- src/library/definitional/cases_on.cpp | 180 ++++++++++++++++++ src/library/definitional/cases_on.h | 17 ++ src/library/definitional/unit.cpp | 21 ++ src/library/definitional/unit.h | 11 ++ .../lean/interactive/num2.input.expected.out | 3 + tests/lean/run/sum_bug.lean | 4 - tests/lean/run/tree.lean | 6 - 13 files changed, 239 insertions(+), 21 deletions(-) create mode 100644 src/library/definitional/cases_on.cpp create mode 100644 src/library/definitional/cases_on.h create mode 100644 src/library/definitional/unit.cpp create mode 100644 src/library/definitional/unit.h diff --git a/library/data/bool.lean b/library/data/bool.lean index c100df27fd..e509b59f3b 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -10,9 +10,6 @@ inductive bool : Type := ff : bool, tt : bool namespace bool - protected definition cases_on {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b := - rec H₁ H₂ b - definition cond {A : Type} (b : bool) (t e : A) := rec_on b e t diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 84db7b4393..e7cd3009bd 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -21,10 +21,6 @@ notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l variable {T : Type} -protected theorem cases_on {P : list T → Prop} (l : list T) (Hnil : P nil) - (Hcons : ∀ (x : T) (l : list T), P (x::l)) : P l := -induction_on l Hnil (take x l IH, Hcons x l) - -- Concat -- ------ diff --git a/library/data/sum.lean b/library/data/sum.lean index d49a7945a8..74ea09b596 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -20,8 +20,6 @@ namespace sum variables {A B : Type} variables {a a₁ a₂ : A} {b b₁ b₂ : B} - protected definition cases_on {P : (A ⊎ B) → Prop} (s : A ⊎ B) (H₁ : ∀a : A, P (inl B a)) (H₂ : ∀b : B, P (inr A b)) : P s := - rec H₁ H₂ s -- Here is the trick for the theorems that follow: -- Fixing a₁, "f s" is a recursive description of "inl B a₁ = s". diff --git a/library/logic/eq.lean b/library/logic/eq.lean index b84321ca94..614c4780f3 100644 --- a/library/logic/eq.lean +++ b/library/logic/eq.lean @@ -1,7 +1,7 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -import general_notation .prop +import general_notation logic.prop data.unit.decl -- logic.eq -- ==================== diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index ab50f1f8e3..8e3ce1409c 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -23,6 +23,8 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/definitional/rec_on.h" #include "library/definitional/induction_on.h" +#include "library/definitional/cases_on.h" +#include "library/definitional/unit.h" #include "frontends/lean/decl_cmds.h" #include "frontends/lean/util.h" #include "frontends/lean/class.h" @@ -649,9 +651,12 @@ struct inductive_cmd_fn { } environment mk_aux_decls(environment env, buffer const & decls) { + bool has_unit = has_unit_decls(env); for (inductive_decl const & d : decls) { env = mk_rec_on(env, inductive_decl_name(d)); env = mk_induction_on(env, inductive_decl_name(d)); + if (has_unit) + env = mk_cases_on(env, inductive_decl_name(d)); } return env; } diff --git a/src/library/definitional/CMakeLists.txt b/src/library/definitional/CMakeLists.txt index 4716f9a51a..ddf3809c74 100644 --- a/src/library/definitional/CMakeLists.txt +++ b/src/library/definitional/CMakeLists.txt @@ -1,3 +1,3 @@ -add_library(definitional rec_on.cpp induction_on.cpp) +add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp unit.cpp) target_link_libraries(definitional ${LEAN_LIBS}) diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp new file mode 100644 index 0000000000..8c2e62c10d --- /dev/null +++ b/src/library/definitional/cases_on.cpp @@ -0,0 +1,180 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/sstream.h" +#include "kernel/environment.h" +#include "kernel/instantiate.h" +#include "kernel/abstract.h" +#include "kernel/inductive/inductive.h" +#include "kernel/type_checker.h" +#include "library/module.h" +#include "library/protected.h" + +namespace lean { +static void throw_corrupted(name const & n) { + throw exception(sstream() << "error in 'cases_on' generation, '" << n << "' inductive datatype declaration is corrupted"); +} + +/** \brief Given a C := As -> Type, return (fun (xs : As), unit) */ +static expr mk_fun_unit(expr const & C, expr const & unit) { + if (is_pi(C)) { + return mk_lambda(binding_name(C), binding_domain(C), mk_fun_unit(binding_body(C), unit)); + } else { + return unit; + } +} + +static bool is_type_former_arg(buffer const & C_names, expr const & arg) { + expr const & fn = get_app_fn(arg); + return is_local(fn) && std::find(C_names.begin(), C_names.end(), mlocal_name(fn)) != C_names.end(); +} + +/** \brief Given minor premise (Pi (a_1 : A_1) ... (a_n : A_n), B) + return fun (a_1 : A_1') ... (a_n : A_n'), star), + and A_i' is A_i if A_i is not the main type former C_main. +*/ +static expr mk_fun_star(expr const & minor, buffer const & C_names, name const & C_main, + expr const & unit, expr const & star) { + if (is_pi(minor)) { + expr const & domain = binding_domain(minor); + expr const & body = binding_body(minor); + if (is_type_former_arg(C_names, domain) && mlocal_name(get_app_fn(domain)) != C_main) + return mk_lambda(binding_name(minor), unit, mk_fun_star(body, C_names, C_main, unit, star)); + else + return mk_lambda(binding_name(minor), binding_domain(minor), mk_fun_star(body, C_names, C_main, unit, star)); + } else { + return star; + } +} + +environment mk_cases_on(environment const & env, name const & n) { + optional decls = inductive::is_inductive_decl(env, n); + if (!decls) + throw exception(sstream() << "error in 'cases_on' generation, '" << n << "' is not an inductive datatype"); + name cases_on_name(n, "cases_on"); + name_generator ngen; + name rec_name = inductive::get_elim_name(n); + declaration rec_decl = env.get(rec_name); + declaration ind_decl = env.get(n); + unsigned num_idx_major = *inductive::get_num_indices(env, n) + 1; + unsigned num_minors = *inductive::get_num_minor_premises(env, n); + auto idecls = std::get<2>(*decls); + unsigned num_types = length(idecls); + unsigned num_params = std::get<1>(*decls); + buffer rec_params; + expr rec_type = rec_decl.get_type(); + while (is_pi(rec_type)) { + expr local = mk_local(ngen.next(), binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type)); + rec_type = instantiate(binding_body(rec_type), local); + rec_params.push_back(local); + } + + levels lvls = param_names_to_levels(rec_decl.get_univ_params()); + bool elim_to_prop = length(rec_decl.get_univ_params()) == length(ind_decl.get_univ_params()); + level elim_univ = elim_to_prop ? mk_level_zero() : head(lvls); + + optional unit; + optional star; + // we use unit if num_types > 1 + if (num_types > 1) { + unit = mk_constant(name("unit"), to_list(elim_univ)); + star = mk_constant(name({"unit", "star"}), to_list(elim_univ)); + } + + // rec_params order + // As Cs minor_premises indices major-premise + + // cases_on has + // As C[i] indices major-premise minor_premises[i] + // That is, it only contains its type former and minor_premises + + buffer cases_on_params; + expr rec_cnst = mk_constant(rec_name, lvls); + buffer rec_args; // arguments for rec used to define cases_on + + // Add params: As + for (unsigned i = 0; i < num_params; i++) { + cases_on_params.push_back(rec_params[i]); + rec_args.push_back(rec_params[i]); + } + + // Add C[i] + buffer C_names; + bool found = false; + unsigned i = num_params; + name C_main; // name of the main type former + for (auto const & d : idecls) { + C_names.push_back(mlocal_name(rec_params[i])); + if (inductive::inductive_decl_name(d) == n) { + cases_on_params.push_back(rec_params[i]); + rec_args.push_back(rec_params[i]); + C_main = mlocal_name(rec_params[i]); + found = true; + } else { + rec_args.push_back(mk_fun_unit(mlocal_type(rec_params[i]), *unit)); + } + i++; + } + if (!found) + throw_corrupted(n); + + // Add indices and major-premise to rec_params + for (unsigned i = 0; i < num_idx_major; i++) + cases_on_params.push_back(rec_params[num_params + num_types + num_minors + i]); + + // Ad minor premises to rec_params and rec_args + i = num_params + num_types; + for (auto const & d : idecls) { + bool is_main = inductive::inductive_decl_name(d) == n; + for (auto ir : inductive::inductive_decl_intros(d)) { + expr const & minor = rec_params[i]; + if (is_main) { + // A cases_on minor premise does not contain "recursive" arguments + buffer minor_non_rec_params; + buffer minor_params; + expr minor_type = mlocal_type(minor); + while (is_pi(minor_type)) { + expr local = mk_local(ngen.next(), binding_name(minor_type), binding_domain(minor_type), + binding_info(minor_type)); + if (is_type_former_arg(C_names, binding_domain(minor_type))) { + if (mlocal_name(get_app_fn(binding_domain(minor_type))) == C_main) { + minor_params.push_back(local); + } else { + minor_params.push_back(update_mlocal(local, *unit)); + } + } else { + minor_params.push_back(local); + minor_non_rec_params.push_back(local); + } + minor_type = instantiate(binding_body(minor_type), local); + } + expr new_C = update_mlocal(minor, Pi(minor_non_rec_params, minor_type)); + cases_on_params.push_back(new_C); + expr new_C_app = mk_app(new_C, minor_non_rec_params); + expr rec_arg = Fun(minor_params, new_C_app); + rec_args.push_back(rec_arg); + } else { + rec_args.push_back(mk_fun_star(mlocal_type(minor), C_names, C_main, *unit, *star)); + } + i++; + } + } + + // Add indices and major-premise to rec_args + for (unsigned i = 0; i < num_idx_major; i++) + rec_args.push_back(rec_params[num_params + num_types + num_minors + i]); + + expr cases_on_type = Pi(cases_on_params, rec_type); + expr cases_on_value = Fun(cases_on_params, mk_app(rec_cnst, rec_args)); + + bool opaque = false; + bool use_conv_opt = true; + declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value, + opaque, rec_decl.get_module_idx(), use_conv_opt); + environment new_env = module::add(env, check(env, new_d)); + return add_protected(new_env, cases_on_name); +} +} diff --git a/src/library/definitional/cases_on.h b/src/library/definitional/cases_on.h new file mode 100644 index 0000000000..d01ca45f82 --- /dev/null +++ b/src/library/definitional/cases_on.h @@ -0,0 +1,17 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" + +namespace lean { +/** \brief Given an inductive datatype \c n in \c env, add + n.cases_on to the environment. + + \remark Throws an exception if \c n is not an inductive datatype. +*/ +environment mk_cases_on(environment const & env, name const & n); +} diff --git a/src/library/definitional/unit.cpp b/src/library/definitional/unit.cpp new file mode 100644 index 0000000000..a42cbf3103 --- /dev/null +++ b/src/library/definitional/unit.cpp @@ -0,0 +1,21 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/environment.h" + +namespace lean { +bool has_unit_decls(environment const & env) { + auto d = env.find(name({"unit", "star"})); + if (!d) + return false; + if (length(d->get_univ_params()) != 1) + return false; + expr const & type = d->get_type(); + if (!is_constant(type)) + return false; + return const_name(type) == "unit"; +} +} diff --git a/src/library/definitional/unit.h b/src/library/definitional/unit.h new file mode 100644 index 0000000000..3e36381df3 --- /dev/null +++ b/src/library/definitional/unit.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" +namespace lean { +bool has_unit_decls(environment const & env); +} diff --git a/tests/lean/interactive/num2.input.expected.out b/tests/lean/interactive/num2.input.expected.out index 9f4c2df679..8793f98f06 100644 --- a/tests/lean/interactive/num2.input.expected.out +++ b/tests/lean/interactive/num2.input.expected.out @@ -10,6 +10,7 @@ pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C pos_num.bit1|pos_num → pos_num pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n) pos_num.one|pos_num +pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n pos_num.num_bits|pos_num → pos_num 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|Type @@ -27,6 +28,7 @@ pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C pos_num.bit1|pos_num → pos_num pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n) pos_num.one|pos_num +pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n 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|Type -- ENDFINDP @@ -39,6 +41,7 @@ pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C pos_num.bit1|pos_num → pos_num pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n) pos_num.one|pos_num +pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n 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|Type -- ENDFINDP diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean index 2e92bc5266..bccb6d5ca9 100644 --- a/tests/lean/run/sum_bug.lean +++ b/tests/lean/run/sum_bug.lean @@ -21,10 +21,6 @@ have H1 : f (inl B a1), from rfl, have H2 : f (inl B a2), from subst H H1, H2 -definition cases_on {A B : Type} {P : (A + B) → Prop} (s : A + B) - (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s := -sum.rec H1 H2 s - theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false := let f := λs, rec_on s (λa', a = a') (λb, false) in have H1 : f (inl B a), from rfl, diff --git a/tests/lean/run/tree.lean b/tests/lean/run/tree.lean index 0a23eb94f0..7ac5009fbe 100644 --- a/tests/lean/run/tree.lean +++ b/tests/lean/run/tree.lean @@ -11,12 +11,6 @@ star : one set_option pp.universes true namespace tree - section - variables {A : Type} {C : tree A → Type} - definition cases_on (t : tree A) (e₁ : Πa, C (leaf a)) (e₂ : Πt₁ t₂, C (node t₁ t₂)) : C t := - rec e₁ (λt₁ t₂ r₁ r₂, e₂ t₁ t₂) t - end - section universe variables l₁ l₂ variable {A : Type.{l₁}}