michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/inductive): use nondependent elimination when the datatype is in Bool/Prop

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-18 15:39:48 -07:00
parent 45252e2229
commit 28b70b4e04
2 changed files with 45 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/kernel/inductive/inductive.cpp
View file

@ -34,6 +34,7 @@ struct add_inductive_fn {
type_checker m_tc;
level m_elim_level; // extra universe level for eliminator.
bool m_dep_elim; // true if using dependent elimination
buffer<expr> m_param_consts; // local constants used to represent global parameters
buffer<level> m_it_levels; // the levels for each inductive datatype in m_decls
@ -300,6 +301,14 @@ struct add_inductive_fn {
}
}
/** \brief Initialize m_dep_elim flag */
void set_dep_elim() {
if (m_env.impredicative() && is_zero(m_it_levels[0]))
m_dep_elim = false;
else
m_dep_elim = true;
}
/**
\brief Given t of the form (I As is) where I is one of the inductive datatypes being defined,
As are the global parameters, and is the actual indices provided to it.
@ -334,10 +343,14 @@ struct add_inductive_fn {
i++;
}
info.m_major_premise = mk_local(mk_fresh_name(), "n", mk_app(mk_app(m_it_consts[d_idx], m_param_consts), info.m_indices));
name C("C");
expr C_ty = mk_sort(m_elim_level);
if (m_dep_elim)
C_ty = Pi(info.m_major_premise, C_ty);
C_ty = Pi(info.m_indices, C_ty);
name C_name("C");
if (get_num_its() > 1)
C = name(C).append_after(d_idx+1);
info.m_C = mk_local(mk_fresh_name(), C, Pi(info.m_indices, Pi(info.m_major_premise, mk_sort(m_elim_level))));
C_name = name(C_name).append_after(d_idx+1);
info.m_C = mk_local(mk_fresh_name(), C_name, C_ty);
m_elim_info.push_back(info);
d_idx++;
}
@ -366,8 +379,11 @@ struct add_inductive_fn {
}
buffer<expr> it_indices;
unsigned it_idx = get_I_indices(t, it_indices);
expr C_app = mk_app(m_elim_info[it_idx].m_C, it_indices);
if (m_dep_elim) {
expr intro_app = mk_app(mk_app(mk_app(mk_constant(intro_rule_name(ir), m_levels), m_param_consts), b), u);
expr C_app = mk_app(mk_app(m_elim_info[it_idx].m_C, it_indices), intro_app);
C_app = mk_app(C_app, intro_app);
}
// populate v using u
for (unsigned i = 0; i < u.size(); i++) {
expr u_i = u[i];
@ -380,8 +396,11 @@ struct add_inductive_fn {
}
buffer<expr> it_indices;
unsigned it_idx = get_I_indices(u_i_ty, it_indices);
expr C_app = mk_app(m_elim_info[it_idx].m_C, it_indices);
if (m_dep_elim) {
expr u_app = mk_app(u_i, xs);
expr C_app = mk_app(mk_app(m_elim_info[it_idx].m_C, it_indices), u_app);
C_app = mk_app(C_app, u_app);
}
expr v_i_ty = Pi(xs, C_app);
expr v_i = mk_local(mk_fresh_name(), name("v").append_after(i), v_i_ty);
v.push_back(v_i);
@ -398,7 +417,9 @@ struct add_inductive_fn {
/** \brief Declare elimination rule */
void declare_elim_rule(inductive_decl const & d, unsigned d_idx) {
elim_info const & info = m_elim_info[d_idx];
expr C_app = mk_app(mk_app(info.m_C, info.m_indices), info.m_major_premise);
expr C_app = mk_app(info.m_C, info.m_indices);
if (m_dep_elim)
C_app = mk_app(C_app, info.m_major_premise);
expr elim_ty = Pi(info.m_indices, Pi(info.m_major_premise, C_app));
// abstract all introduction rules
unsigned i = get_num_its();
@ -428,6 +449,7 @@ struct add_inductive_fn {
/** \brief Declare the eliminator/recursor for each datatype */
void declare_elim_rules() {
set_dep_elim();
mk_elim_level();
mk_elim_info();
unsigned i = 0;

19
tests/lua/ind1.lua
View file

@ -29,7 +29,7 @@ env = add_inductive(env,
-- 1 is the number of parameters.
-- The Boolean true in {A, U_l, true} is marking that this argument is implicit.
env = add_inductive(env,
"list", {l}, 1, mk_arrow(U_l, U_l1),
"list", {l}, 1, Pi(A, U_l, U_l1),
"nil", Pi({{A, U_l, true}}, list_l(A)),
"cons", Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A))))
env = add_inductive(env,
@ -46,17 +46,17 @@ env = add_inductive(env, "false", Bool)
-- Datatype with a single constructor.
env = add_inductive(env, "true", Bool, "trivial", Const("true"))
env = add_inductive(env,
"and", mk_arrow(Bool, Bool, Bool),
"and", 2, Pi({{A, Bool}, {B, Bool}}, Bool),
"and_intro", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(A, B, And(A, B))))
env = add_inductive(env,
"or", mk_arrow(Bool, Bool, Bool),
"or", 2, Pi({{A, Bool}, {B, Bool}}, Bool),
"or_intro_left", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(A, Or(A, B))),
"or_intro_right", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(B, Or(A, B))))
local P = Const("P")
local a = Const("a")
local exists_l = Const("exists", {l})
env = add_inductive(env,
"exists", {l}, 2, Pi({{A, U_l}}, mk_arrow(mk_arrow(A, Bool), Bool)),
"exists", {l}, 2, Pi({{A, U_l}, {P, mk_arrow(A, Bool)}}, Bool),
"exists_intro", Pi({{A, U_l, true}, {P, mk_arrow(A, Bool), true}, {a, A}}, mk_arrow(P(a), exists_l(A, P))))
env = add_inductive(env, {l}, 1,
@ -73,6 +73,7 @@ display_type(env, Const("vcons", {mk_level_zero()}))
display_type(env, Const("consf", {mk_level_zero()}))
display_type(env, Const("forest_rec", {v, u}))
display_type(env, Const("nat_rec", {v}))
display_type(env, Const("or_rec"))
local Even = Const("Even")
local Odd = Const("Odd")
@ -89,3 +90,13 @@ env = add_inductive(env,
"flist", {l}, 1, mk_arrow(U_l, U_l1),
"fnil", Pi({{A, U_l, true}}, flist_l(A)),
"fcons", Pi({{A, U_l, true}}, mk_arrow(A, mk_arrow(Nat, flist_l(A)), flist_l(A))))
local eq_l = Const("eq", {l})
env = add_inductive(env,
"eq", {l}, 2, Pi({{A, U_l}, {a, A}, {b, A}}, Bool),
"refl", Pi({{A, U_l}, {a, A}}, eq_l(A, a, a)))
display_type(env, Const("eq_rec", {v, u}))
display_type(env, Const("exists_rec", {v, u}))
display_type(env, Const("list_rec", {v, u}))
display_type(env, Const("Even_rec"))
display_type(env, Const("Odd_rec"))