max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library): do not generate C.destruct (for structures), and C.induction_on (for structures and inductive datatypes)

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-15 14:45:13 -07:00
parent 7f56f23e70
commit 36770119b6
8 changed files with 7 additions and 86 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/data/list/lemmas.lean
View file

@ -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),

6
library/init/data/sigma/lex.lean
View file

@ -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

2
library/init/wf.lean
View file

@ -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 :=

6
src/frontends/lean/structure_cmd.cpp
View file

@ -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));

2
src/library/constructions/CMakeLists.txt
View file

@ -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)

50
src/library/constructions/induction_on.cpp
View file

@ -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);
}
}

19
src/library/constructions/induction_on.h
View file

@ -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
<tt>n.induction_on</tt> to the environment.
\remark Throws an exception if \c n is not an inductive datatype.
\remark Throws an exception if <tt>n.rec_on</tt> is not defined in the given environment.
*/
environment mk_induction_on(environment const & env, name const & n);
}

4
src/library/inductive_compiler/basic.cpp
View file

@ -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);