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

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

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-20 23:14:11 -07:00
parent 51d4644832
commit 2164ba6f20
4 changed files with 75 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -157,6 +157,7 @@ class induction_tac {
unsigned first_idx_pos = rec_info.get_first_index_pos();
bool consumed_major = false;
buffer<goal> new_goals;
list<bool> produce_motive = rec_info.get_produce_motive();
while (is_pi(rec_type) && curr_pos < rec_info.get_num_args()) {
if (first_idx_pos == curr_pos) {
for (expr const & idx : indices) {
@ -172,6 +173,8 @@ class induction_tac {
consumed_major = true;
curr_pos++;
} else {
if (!produce_motive)
throw_ill_formed_recursor(rec_info);
buffer<expr> new_goal_hyps;
new_goal_hyps.append(new_hyps);
expr new_type = binding_domain(rec_type);
@ -199,23 +202,26 @@ class induction_tac {
}
new_type = head_beta_reduce(new_type);
buffer<expr> new_deps;
// introduce deps
for (unsigned i = 0; i < num_deps; i++) {
if (!is_pi(new_type)) {
throw_ill_formed_recursor(rec_info);
if (head(produce_motive)) {
// introduce deps
for (unsigned i = 0; i < num_deps; i++) {
if (!is_pi(new_type)) {
throw_ill_formed_recursor(rec_info);
}
expr dep_type = binding_domain(new_type);
expr new_dep = mk_local(m_ngen.next(), get_unused_name(binding_name(new_type), new_goal_hyps),
dep_type, binder_info());
new_deps.push_back(new_dep);
new_goal_hyps.push_back(new_dep);
new_type = instantiate(binding_body(new_type), new_dep);
}
expr dep_type = binding_domain(new_type);
expr new_dep = mk_local(m_ngen.next(), get_unused_name(binding_name(new_type), new_goal_hyps),
dep_type, binder_info());
new_deps.push_back(new_dep);
new_goal_hyps.push_back(new_dep);
new_type = instantiate(binding_body(new_type), new_dep);
}
expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_goal_hyps, new_type)), new_goal_hyps);
goal new_g(new_meta, new_type);
new_goals.push_back(new_g);
rec_arg = Fun(minor_args, Fun(new_deps, new_meta));
}
produce_motive = tail(produce_motive);
rec = mk_app(rec, rec_arg);
rec_type = m_tc.whnf(instantiate(binding_body(rec_type), rec_arg), m_cs);
curr_pos++;

35
src/library/user_recursors.cpp
View file

@ -24,23 +24,27 @@ bool recursor_info::is_minor(unsigned pos) const {
recursor_info::recursor_info(name const & r, name const & I, optional<unsigned> const & motive_univ_pos,
bool dep_elim, unsigned num_args, unsigned major_pos,
list<optional<unsigned>> const & params_pos, list<unsigned> const & indices_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_num_args(num_args), m_major_pos(major_pos), m_params_pos(params_pos), m_indices_pos(indices_pos) {}
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;
write_list(s, m_params_pos);
write_list(s, m_indices_pos);
write_list(s, m_produce_motive);
}
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
>> info.m_num_args >> info.m_major_pos;
info.m_params_pos = read_list<optional<unsigned>>(d);
info.m_indices_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);
return info;
}
@ -64,11 +68,14 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
unsigned num_params = *inductive::get_num_params(env, *I);
unsigned num_minors = *inductive::get_num_minor_premises(env, *I);
unsigned num_args = num_params + 1 /* motive */ + num_minors + num_indices + 1 /* major */;
list<bool> produce_motive;
for (unsigned i = 0; i < num_minors; i++)
produce_motive = cons(true, produce_motive);
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),
num_args, major_pos, params_pos, indices_pos);
num_args, major_pos, params_pos, indices_pos, produce_motive);
}
declaration d = env.get(r);
type_checker tc(env);
@ -204,8 +211,24 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
lean_assert(*C_univ_pos < length(d.get_univ_params()));
}
buffer<bool> produce_motive;
unsigned nparams = params_pos.size();
unsigned nindices = indices_pos.size();
for (unsigned i = nparams+1; i < tele.size(); i++) {
if (i < major_pos - nindices || i > major_pos) {
// i is a minor premise
buffer<expr> tmp;
expr res = get_app_fn(to_telescope(tc, mlocal_type(tele[i]), tmp));
if (is_local(res) && mlocal_name(C) == mlocal_name(res)) {
produce_motive.push_back(true);
} else {
produce_motive.push_back(false);
}
}
}
return recursor_info(r, const_name(I), C_univ_pos, dep_elim, tele.size(), major_pos,
to_list(params_pos), to_list(indices_pos));
to_list(params_pos), to_list(indices_pos), to_list(produce_motive));
}
struct recursor_state {

6
src/library/user_recursors.h
View file

@ -18,11 +18,14 @@ class recursor_info {
// if param is <none>, then it should be resolved by type class resolution
list<optional<unsigned>> m_params_pos; // position of the recursor parameters in the major premise
list<unsigned> m_indices_pos; // position of the recursor indices in the major premise
list<bool> m_produce_motive; // "bit-map" indicating whether the i-th element is true, if
// the i-th minor premise produces the motive
public:
recursor_info(name const & r, name const & I, optional<unsigned> const & motive_univ_pos,
bool dep_elim, unsigned num_args, unsigned major_pos,
list<optional<unsigned>> const & params_pos, list<unsigned> const & indices_pos);
list<optional<unsigned>> const & params_pos, list<unsigned> const & indices_pos,
list<bool> const & produce_motive);
recursor_info();
name const & get_name() const { return m_recursor; }
@ -38,6 +41,7 @@ public:
list<optional<unsigned>> const & get_params_pos() const { return m_params_pos; }
/** \brief Return position of the recursor indices in the major premise. */
list<unsigned> const & get_indices_pos() const { return m_indices_pos; }
list<bool> const & get_produce_motive() const { return m_produce_motive; }
bool has_dep_elim() const { return m_dep_elim; }
bool is_minor(unsigned pos) const;

25
tests/lean/hott/614.hlean Normal file
View file

@ -0,0 +1,25 @@
import hit.circle
open circle eq int
attribute circle.rec [recursor]
protected definition my_decode {x : circle} (c : circle.code x) : base = x :=
begin
induction x,
{ revert c, exact power loop },
{ apply eq_of_homotopy, intro a,
refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
rewrite [transport_code_loop_inv,power_con,succ_pred]
}
end
protected definition my_decode' {x : circle} : circle.code x → base = x :=
begin
induction x,
{ exact power loop},
{ apply eq_of_homotopy, intro a,
refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
rewrite [transport_code_loop_inv,power_con,succ_pred]
}
end