From 2164ba6f201077b6c336f9efbadf156f04ce688e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 May 2015 23:14:11 -0700 Subject: [PATCH] fix(library/tactic/induction_tactic): fixes #614 --- src/library/tactic/induction_tactic.cpp | 26 +++++++++++------- src/library/user_recursors.cpp | 35 ++++++++++++++++++++----- src/library/user_recursors.h | 6 ++++- tests/lean/hott/614.hlean | 25 ++++++++++++++++++ 4 files changed, 75 insertions(+), 17 deletions(-) create mode 100644 tests/lean/hott/614.hlean diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index fd1dd20bb..8cb2c56ec 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -157,6 +157,7 @@ class induction_tac { unsigned first_idx_pos = rec_info.get_first_index_pos(); bool consumed_major = false; buffer new_goals; + list 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 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 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++; diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index 6e79daf7c..2f991ab75 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -24,23 +24,27 @@ bool recursor_info::is_minor(unsigned pos) const { recursor_info::recursor_info(name const & r, name const & I, optional const & motive_univ_pos, bool dep_elim, unsigned num_args, unsigned major_pos, - list> const & params_pos, list const & indices_pos): + list> const & params_pos, list const & indices_pos, + list 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>(d); - info.m_indices_pos = read_list(d); + info.m_params_pos = read_list>(d); + info.m_indices_pos = read_list(d); + info.m_produce_motive = read_list(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 produce_motive; + for (unsigned i = 0; i < num_minors; i++) + produce_motive = cons(true, produce_motive); list> params_pos = map2>(mk_list_range(0, num_params), [](unsigned i) { return optional(i); }); list 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 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 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 { diff --git a/src/library/user_recursors.h b/src/library/user_recursors.h index a928f93a5..add786842 100644 --- a/src/library/user_recursors.h +++ b/src/library/user_recursors.h @@ -18,11 +18,14 @@ class recursor_info { // if param is , then it should be resolved by type class resolution list> m_params_pos; // position of the recursor parameters in the major premise list m_indices_pos; // position of the recursor indices in the major premise + list 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 const & motive_univ_pos, bool dep_elim, unsigned num_args, unsigned major_pos, - list> const & params_pos, list const & indices_pos); + list> const & params_pos, list const & indices_pos, + list const & produce_motive); recursor_info(); name const & get_name() const { return m_recursor; } @@ -38,6 +41,7 @@ public: list> const & get_params_pos() const { return m_params_pos; } /** \brief Return position of the recursor indices in the major premise. */ list const & get_indices_pos() const { return m_indices_pos; } + list const & get_produce_motive() const { return m_produce_motive; } bool has_dep_elim() const { return m_dep_elim; } bool is_minor(unsigned pos) const; diff --git a/tests/lean/hott/614.hlean b/tests/lean/hott/614.hlean new file mode 100644 index 000000000..c61c1a826 --- /dev/null +++ b/tests/lean/hott/614.hlean @@ -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