From 36770119b69432ea10be8afcc4596ec60fd8b3d4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Mar 2017 14:45:13 -0700 Subject: [PATCH] feat(library): do not generate `C.destruct` (for structures), and `C.induction_on` (for structures and inductive datatypes) --- library/init/data/list/lemmas.lean | 4 +- library/init/data/sigma/lex.lean | 6 +-- library/init/wf.lean | 2 +- src/frontends/lean/structure_cmd.cpp | 6 --- src/library/constructions/CMakeLists.txt | 2 +- src/library/constructions/induction_on.cpp | 50 ---------------------- src/library/constructions/induction_on.h | 19 -------- src/library/inductive_compiler/basic.cpp | 4 -- 8 files changed, 7 insertions(+), 86 deletions(-) delete mode 100644 src/library/constructions/induction_on.cpp delete mode 100644 src/library/constructions/induction_on.h diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean index fc6eba0a3b..f719451179 100644 --- a/library/init/data/list/lemmas.lean +++ b/library/init/data/list/lemmas.lean @@ -234,7 +234,7 @@ lemma mem_or_mem_of_mem_append {a : α} : ∀ {s t : list α}, a ∈ s ++ t → end lemma mem_append_of_mem_or_mem {a : α} {s t : list α} : a ∈ s ∨ a ∈ t → a ∈ s ++ t := -list.induction_on s +list.rec_on s (take h, or.elim h false.elim id) (take b s, assume ih : a ∈ s ∨ a ∈ t → a ∈ s ++ t, @@ -268,7 +268,7 @@ lemma length_pos_of_mem {a : α} : ∀ {l : list α}, a ∈ l → 0 < length l | (b::l) := suppose a ∈ b::l, nat.zero_lt_succ _ lemma mem_split {a : α} {l : list α} : a ∈ l → ∃ s t : list α, l = s ++ (a::t) := -list.induction_on l +list.rec_on l (suppose a ∈ [], begin simp at this, contradiction end) (take b l, assume ih : a ∈ l → ∃ s t : list α, l = s ++ (a::t), diff --git a/library/init/data/sigma/lex.lean b/library/init/data/sigma/lex.lean index b01ac062f5..5f8225223d 100644 --- a/library/init/data/sigma/lex.lean +++ b/library/init/data/sigma/lex.lean @@ -48,7 +48,7 @@ section -- The lexicographical order of well founded relations is well-founded def lex_wf (ha : well_founded r) (hb : ∀ x, well_founded (s x)) : well_founded (lex r s) := - well_founded.intro (λ p, destruct p (λ a b, lex_accessible (well_founded.apply ha a) hb b)) + well_founded.intro (λ p, cases_on p (λ a b, lex_accessible (well_founded.apply ha a) hb b)) end section @@ -59,7 +59,7 @@ section def lex_ndep_wf {r : α → α → Prop} {s : β → β → Prop} (ha : well_founded r) (hb : well_founded s) : well_founded (lex_ndep r s) := - well_founded.intro (λ p, destruct p (λ a b, lex_accessible (well_founded.apply ha a) (λ x, hb) b)) + well_founded.intro (λ p, cases_on p (λ a b, lex_accessible (well_founded.apply ha a) (λ x, hb) b)) end section @@ -100,7 +100,7 @@ section aux rfl rfl))) def rev_lex_wf (ha : well_founded r) (hb : well_founded s) : well_founded (rev_lex r s) := - well_founded.intro (λ p, destruct p (λ a b, rev_lex_accessible (apply hb b) (well_founded.apply ha) a)) + well_founded.intro (λ p, cases_on p (λ a b, rev_lex_accessible (apply hb b) (well_founded.apply ha) a)) end section diff --git a/library/init/wf.lean b/library/init/wf.lean index 7b6c4fafd8..39a7592554 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -172,7 +172,7 @@ section -- The lexicographical order of well founded relations is well-founded def lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra rb) := - ⟨λ p, destruct p (λ a b, lex_accessible (apply ha a) (well_founded.apply hb) b)⟩ + ⟨λ p, cases_on p (λ a b, lex_accessible (apply ha a) (well_founded.apply hb) b)⟩ -- relational product is a subrelation of the lex def rprod_sub_lex : ∀ a b, rprod ra rb a b → lex ra rb a b := diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 182346d160..64a509dda4 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -42,7 +42,6 @@ Author: Leonardo de Moura #include "library/documentation.h" #include "library/compiler/vm_compiler.h" #include "library/constructions/rec_on.h" -#include "library/constructions/induction_on.h" #include "library/constructions/cases_on.h" #include "library/constructions/projection.h" #include "library/constructions/no_confusion.h" @@ -972,10 +971,6 @@ struct structure_cmd_fn { name rec_on_name(m_name, "rec_on"); add_rec_alias(rec_on_name); m_env = add_aux_recursor(m_env, rec_on_name); - m_env = mk_induction_on(m_env, m_name); - name induction_on_name(m_name, "induction_on"); - add_alias(induction_on_name); - add_rec_on_alias(name(m_name, "destruct")); name cases_on_name(m_name, "cases_on"); add_rec_on_alias(cases_on_name); m_env = add_aux_recursor(m_env, cases_on_name); @@ -1080,7 +1075,6 @@ struct structure_cmd_fn { return; if (!has_and_decls(m_env)) return; - m_env = mk_injective_lemmas(m_env, m_name); add_alias(mk_injective_name(m_name)); add_alias(mk_injective_arrow_name(m_name)); diff --git a/src/library/constructions/CMakeLists.txt b/src/library/constructions/CMakeLists.txt index a6aa07ecfb..b36d988a9a 100644 --- a/src/library/constructions/CMakeLists.txt +++ b/src/library/constructions/CMakeLists.txt @@ -1,3 +1,3 @@ -add_library(constructions OBJECT rec_on.cpp induction_on.cpp cases_on.cpp +add_library(constructions OBJECT rec_on.cpp cases_on.cpp no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp has_sizeof.cpp constructor.cpp drec.cpp injective.cpp) diff --git a/src/library/constructions/induction_on.cpp b/src/library/constructions/induction_on.cpp deleted file mode 100644 index 6663aeb541..0000000000 --- a/src/library/constructions/induction_on.cpp +++ /dev/null @@ -1,50 +0,0 @@ -/* -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/type_checker.h" -#include "library/module.h" -#include "library/protected.h" -#include "library/util.h" -#include "library/aux_recursors.h" - -namespace lean { -environment mk_induction_on(environment const & env, name const & n) { - if (!inductive::is_inductive_decl(env, n)) - throw exception(sstream() << "error in 'induction_on' generation, '" << n << "' is not an inductive datatype"); - name rec_on_name(n, "rec_on"); - name induction_on_name(n, "induction_on"); - declaration rec_on_decl = env.get(rec_on_name); - declaration ind_decl = env.get(n); - unsigned rec_on_num_univs = rec_on_decl.get_num_univ_params(); - unsigned ind_num_univs = ind_decl.get_num_univ_params(); - environment new_env = env; - if (rec_on_num_univs == ind_num_univs) { - // easy case, induction_on is just an alias for rec_on - certified_declaration cdecl = check(new_env, - mk_definition_inferring_trusted(new_env, induction_on_name, rec_on_decl.get_univ_params(), - rec_on_decl.get_type(), rec_on_decl.get_value(), - reducibility_hints::mk_opaque())); - new_env = add_aux_recursor(new_env, induction_on_name); - new_env = module::add(new_env, cdecl); - } else { - level_param_names induction_on_univs = tail(rec_on_decl.get_univ_params()); - name from = head(rec_on_decl.get_univ_params()); - level to = mk_level_zero(); - expr induction_on_type = instantiate_univ_param(rec_on_decl.get_type(), from, to); - expr induction_on_value = instantiate_univ_param(rec_on_decl.get_value(), from, to); - certified_declaration cdecl = check(new_env, - mk_definition_inferring_trusted(new_env, induction_on_name, induction_on_univs, - induction_on_type, induction_on_value, - reducibility_hints::mk_opaque())); - new_env = add_aux_recursor(new_env, induction_on_name); - new_env = module::add(new_env, cdecl); - } - return add_protected(new_env, induction_on_name); -} -} diff --git a/src/library/constructions/induction_on.h b/src/library/constructions/induction_on.h deleted file mode 100644 index e67881ebd2..0000000000 --- a/src/library/constructions/induction_on.h +++ /dev/null @@ -1,19 +0,0 @@ -/* -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.induction_on to the environment. - - \remark Throws an exception if \c n is not an inductive datatype. - - \remark Throws an exception if n.rec_on is not defined in the given environment. -*/ -environment mk_induction_on(environment const & env, name const & n); -} diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp index 72958ed72e..c208ebced5 100644 --- a/src/library/inductive_compiler/basic.cpp +++ b/src/library/inductive_compiler/basic.cpp @@ -16,7 +16,6 @@ Author: Daniel Selsam #include "library/inductive_compiler/util.h" #include "library/constructions/drec.h" #include "library/constructions/rec_on.h" -#include "library/constructions/induction_on.h" #include "library/constructions/cases_on.h" #include "library/constructions/brec_on.h" #include "library/constructions/no_confusion.h" @@ -91,9 +90,6 @@ class add_basic_inductive_decl_fn { if (gen_rec_on) m_env = mk_rec_on(m_env, ind_name); - if (gen_rec_on) - m_env = mk_induction_on(m_env, ind_name); - if (has_unit) { if (gen_cases_on) m_env = mk_cases_on(m_env, ind_name);