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

fix(library/tactic/induction_tactic): fixes #619

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-21 18:18:56 -07:00
parent f830bf54c2
commit b83b0c0017
6 changed files with 89 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/frontends/lean/builtin_cmds.cpp
View file

@ -235,11 +235,16 @@ static void print_recursor_info(parser & p) {
recursor_info info = get_recursor_info(p.env(), c);
out << "recursor information\n"
<< " num. parameters: " << info.get_num_params() << "\n"
<< " num. indices: " << info.get_num_indices() << "\n";
if (auto r = info.get_motive_univ_pos())
out << " motive univ. pos.: " << *r << "\n";
else
out << " recursor eliminate only to Prop\n";
<< " num. indices: " << info.get_num_indices() << "\n"
<< " universe param pos.: ";
for (unsigned idx : info.get_universe_pos()) {
if (idx == recursor_info::get_motive_univ_idx()) {
out << " [motive univ]";
} else {
out << " " << idx;
}
}
out << "\n";
out << " motive pos.: " << info.get_motive_pos() + 1 << "\n"
<< " major premise pos.: " << info.get_major_pos() + 1 << "\n"
<< " dep. elimination: " << info.has_dep_elim() << "\n";

36
src/library/tactic/induction_tactic.cpp
View file

@ -108,28 +108,26 @@ class induction_tac {
recursor_info const & rec_info) {
expr const & g_type = g.get_type();
level g_lvl = sort_level(m_tc.ensure_type(g_type, m_cs));
levels rec_levels;
buffer<level> rec_lvls;
expr const & I = get_app_fn(h_type);
if (auto lpos = rec_info.get_motive_univ_pos()) {
buffer<level> ls;
unsigned i = 0;
for (level const & l : const_levels(I)) {
if (i == *lpos)
ls.push_back(g_lvl);
ls.push_back(l);
i++;
buffer<level> I_lvls;
to_buffer(const_levels(I), I_lvls);
bool found_g_lvl = false;
for (unsigned idx : rec_info.get_universe_pos()) {
if (idx == recursor_info::get_motive_univ_idx()) {
rec_lvls.push_back(g_lvl);
found_g_lvl = true;
} else {
if (idx >= I_lvls.size())
throw_ill_formed_recursor(rec_info);
rec_lvls.push_back(I_lvls[idx]);
}
if (i == *lpos)
ls.push_back(g_lvl);
rec_levels = to_list(ls);
} else {
if (!is_zero(g_lvl)) {
throw tactic_exception(sstream() << "invalid 'induction' tactic, recursor '" << rec_info.get_name()
<< "' can only eliminate into Prop");
}
rec_levels = const_levels(I);
}
expr rec = mk_constant(rec_info.get_name(), rec_levels);
if (!found_g_lvl && !is_zero(g_lvl)) {
throw tactic_exception(sstream() << "invalid 'induction' tactic, recursor '" << rec_info.get_name()
<< "' can only eliminate into Prop");
}
expr rec = mk_constant(rec_info.get_name(), to_list(rec_lvls));
for (optional<expr> const & p : params) {
if (p) {
rec = mk_app(rec, *p);

63
src/library/user_recursors.cpp
View file

@ -22,17 +22,18 @@ bool recursor_info::is_minor(unsigned pos) const {
return true;
}
recursor_info::recursor_info(name const & r, name const & I, optional<unsigned> const & motive_univ_pos,
recursor_info::recursor_info(name const & r, name const & I, list<unsigned> const & univ_pos,
bool dep_elim, unsigned num_args, unsigned major_pos,
list<optional<unsigned>> const & params_pos, list<unsigned> const & indices_pos,
list<bool> const & produce_motive):
m_recursor(r), m_type_name(I), m_motive_univ_pos(motive_univ_pos), m_dep_elim(dep_elim),
m_recursor(r), m_type_name(I), m_universe_pos(univ_pos), m_dep_elim(dep_elim),
m_num_args(num_args), m_major_pos(major_pos), m_params_pos(params_pos), m_indices_pos(indices_pos),
m_produce_motive(produce_motive) {}
recursor_info::recursor_info() {}
void recursor_info::write(serializer & s) const {
s << m_recursor << m_type_name << m_motive_univ_pos << m_dep_elim << m_num_args << m_major_pos;
s << m_recursor << m_type_name << m_dep_elim << m_num_args << m_major_pos;
write_list(s, m_universe_pos);
write_list(s, m_params_pos);
write_list(s, m_indices_pos);
write_list(s, m_produce_motive);
@ -40,8 +41,9 @@ void recursor_info::write(serializer & s) const {
recursor_info recursor_info::read(deserializer & d) {
recursor_info info;
d >> info.m_recursor >> info.m_type_name >> info.m_motive_univ_pos >> info.m_dep_elim
d >> info.m_recursor >> info.m_type_name >> info.m_dep_elim
>> info.m_num_args >> info.m_major_pos;
info.m_universe_pos = read_list<unsigned>(d);
info.m_params_pos = read_list<optional<unsigned>>(d);
info.m_indices_pos = read_list<unsigned>(d);
info.m_produce_motive = read_list<bool>(d);
@ -60,9 +62,10 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
if (auto I = inductive::is_elim_rule(env, r)) {
if (*inductive::get_num_type_formers(env, *I) > 1)
throw exception(sstream() << "unsupported recursor '" << r << "', it has multiple motives");
optional<unsigned> motive_univ_pos;
if (env.get(name(*I, "rec")).get_num_univ_params() != env.get(name(*I)).get_num_univ_params())
motive_univ_pos = 0;
unsigned num_univ_params = env.get(*I).get_num_univ_params();
list<unsigned> universe_pos = mk_list_range(0, num_univ_params);
if (env.get(name(*I, "rec")).get_num_univ_params() != num_univ_params)
universe_pos = cons(recursor_info::get_motive_univ_idx(), universe_pos);
unsigned major_pos = *inductive::get_elim_major_idx(env, r);
unsigned num_indices = *inductive::get_num_indices(env, *I);
unsigned num_params = *inductive::get_num_params(env, *I);
@ -74,7 +77,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
list<optional<unsigned>> params_pos = map2<optional<unsigned>>(mk_list_range(0, num_params),
[](unsigned i) { return optional<unsigned>(i); });
list<unsigned> indices_pos = mk_list_range(num_params, num_params + num_indices);
return recursor_info(r, *I, motive_univ_pos, inductive::has_dep_elim(env, *I),
return recursor_info(r, *I, universe_pos, inductive::has_dep_elim(env, *I),
num_args, major_pos, params_pos, indices_pos, produce_motive);
}
declaration d = env.get(r);
@ -183,16 +186,12 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
if (!is_sort(C_rtype) || C_tele.size() != C_args.size()) {
throw_invalid_motive(C);
}
// Calculate position of the motive's universe.
level motive_lvl = sort_level(C_rtype);
// Remark: if we are in the standard environment, then the motive may be a proposition, and be fixed at 0.
// The following pragma is for avoiding gcc bogus warning
#if defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
#endif
optional<unsigned> C_univ_pos;
level C_lvl = sort_level(C_rtype);
if (!is_standard(env) || !is_zero(C_lvl)) {
if (!is_param(C_lvl)) {
if (!is_standard(env) || !is_zero(motive_lvl)) {
if (!is_param(motive_lvl)) {
if (is_standard(env))
throw exception("invalid user defined recursor, "
"motive result sort must be Prop or Type.{l} where l is a universe parameter");
@ -200,15 +199,29 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
throw exception("invalid user defined recursor, "
"motive result sort must be Type.{l} where l is a universe parameter");
}
name l = param_id(C_lvl);
unsigned uni_pos = 0;
for (name const & l_curr : d.get_univ_params()) {
if (l_curr == l)
break;
uni_pos++;
}
// A universe parameter must occur in the major premise or in the motive
buffer<unsigned> univ_param_pos;
for (name const & p : d.get_univ_params()) {
if (!is_zero(motive_lvl) && param_id(motive_lvl) == p) {
univ_param_pos.push_back(recursor_info::get_motive_univ_idx());
} else {
bool found = false;
unsigned i = 0;
for (level const & l : const_levels(I)) {
if (is_param(l) && param_id(l) == p) {
univ_param_pos.push_back(i);
found = true;
break;
}
i++;
}
if (!found) {
throw exception(sstream() << "invalid user defined recursor, major premise '"
<< major << "' does not contain universe parameter '" << p << "'");
}
}
C_univ_pos = uni_pos;
lean_assert(*C_univ_pos < length(d.get_univ_params()));
}
buffer<bool> produce_motive;
@ -227,7 +240,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
}
}
return recursor_info(r, const_name(I), C_univ_pos, dep_elim, tele.size(), major_pos,
return recursor_info(r, const_name(I), to_list(univ_param_pos), dep_elim, tele.size(), major_pos,
to_list(params_pos), to_list(indices_pos), to_list(produce_motive));
}

11
src/library/user_recursors.h
View file

@ -11,7 +11,7 @@ namespace lean {
class recursor_info {
name m_recursor;
name m_type_name;
optional<unsigned> m_motive_univ_pos; // if none, then recursor can only eliminate to Prop
list<unsigned> m_universe_pos; // position of the recursor universe level parameters.
bool m_dep_elim;
unsigned m_num_args; // total number of arguments
unsigned m_major_pos;
@ -22,12 +22,18 @@ class recursor_info {
// the i-th minor premise produces the motive
public:
recursor_info(name const & r, name const & I, optional<unsigned> const & motive_univ_pos,
recursor_info(name const & r, name const & I, list<unsigned> const & univ_pos,
bool dep_elim, unsigned num_args, unsigned major_pos,
list<optional<unsigned>> const & params_pos, list<unsigned> const & indices_pos,
list<bool> const & produce_motive);
recursor_info();
/** \brief Return a list containing the position of the recursor universe parameters in the major premise.
The value get_motive_univ_idx() is used to identify the position of the motive universe. */
list<unsigned> const & get_universe_pos() const { return m_universe_pos; }
static unsigned get_motive_univ_idx() { return static_cast<unsigned>(-1); }
name const & get_name() const { return m_recursor; }
name const & get_type_name() const { return m_type_name; }
unsigned get_num_args() const { return m_num_args; }
@ -36,7 +42,6 @@ public:
unsigned get_motive_pos() const { return get_num_params(); }
unsigned get_first_index_pos() const { return m_major_pos - get_num_indices(); }
unsigned get_major_pos() const { return m_major_pos; }
optional<unsigned> const & get_motive_univ_pos() const { return m_motive_univ_pos; }
/** \brief Return position of the recursor parameters in the major premise. */
list<optional<unsigned>> const & get_params_pos() const { return m_params_pos; }
/** \brief Return position of the recursor indices in the major premise. */

12
tests/lean/hott/619.hlean Normal file
View file

@ -0,0 +1,12 @@
-- HoTT
open is_equiv equiv eq
definition my_rec_on_ua [recursor] {A B : Type} {P : A ≃ B → Type}
(f : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P f :=
right_inv equiv_of_eq f ▸ H (ua f)
theorem foo {A B : Type} (f : A ≃ B) : A = B :=
begin
induction f using my_rec_on_ua,
assumption
end

8
tests/lean/urec.lean.expected.out
View file

@ -7,7 +7,7 @@ myrec.{l_1 l_2} :
recursor information
num. parameters: 1
num. indices: 0
motive univ. pos.: 1
universe param pos.: 0 [motive univ]
motive pos.: 2
major premise pos.: 3
dep. elimination: 1
@ -15,7 +15,7 @@ recursor information
recursor information
num. parameters: 0
num. indices: 0
recursor eliminate only to Prop
universe param pos.:
motive pos.: 1
major premise pos.: 2
dep. elimination: 1
@ -27,7 +27,7 @@ vector.induction_on.{l_1} :
recursor information
num. parameters: 1
num. indices: 1
recursor eliminate only to Prop
universe param pos.: 0
motive pos.: 2
major premise pos.: 4
dep. elimination: 1
@ -39,7 +39,7 @@ Exists.rec.{l_1} :
recursor information
num. parameters: 2
num. indices: 0
recursor eliminate only to Prop
universe param pos.: 0
motive pos.: 3
major premise pos.: 5
dep. elimination: 0