From 5508e4b132cbc89202c269b6bf223e1bc2c44582 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 May 2015 20:48:33 -0700 Subject: [PATCH] feat(library/tactic/induction_tactic): type class inference for minor premises closes #611 --- src/library/tactic/induction_tactic.cpp | 87 ++++++++++++++----------- tests/lean/hott/611.hlean | 9 +++ 2 files changed, 57 insertions(+), 39 deletions(-) create mode 100644 tests/lean/hott/611.hlean diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index 1a9dc6ac3..3e2813d79 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -71,11 +71,7 @@ class induction_tac { << "' is ill-formed"); } - expr mk_type_class_param(goal const & g, expr const & rec, recursor_info const & rec_info) { - expr rec_type = m_tc.whnf(m_tc.infer(rec, m_cs), m_cs); - if (!is_pi(rec_type)) { - throw_ill_formed_recursor(rec_info); - } + expr mk_type_class_param(goal const & g, expr const & type) { bool use_local_insts = true; bool is_strict = false; local_context ctx = g.to_local_context(); @@ -83,11 +79,19 @@ class induction_tac { auto mc = mk_class_instance_elaborator( m_env, m_ios, ctx, m_ngen.next(), optional(), use_local_insts, is_strict, - some_expr(binding_domain(rec_type)), m_ref.get_tag(), cfg, nullptr); + some_expr(type), m_ref.get_tag(), cfg, nullptr); m_cs += mc.second; return mc.first; } + expr mk_type_class_param(goal const & g, expr const & rec, recursor_info const & rec_info) { + expr rec_type = m_tc.whnf(m_tc.infer(rec, m_cs), m_cs); + if (!is_pi(rec_type)) { + throw_ill_formed_recursor(rec_info); + } + return mk_type_class_param(g, binding_domain(rec_type)); + } + goals apply_recursor(goal const & g, unsigned num_deps, expr const & h, expr const & h_type, buffer> const & params, buffer const & indices, recursor_info const & rec_info) { @@ -160,42 +164,47 @@ class induction_tac { buffer new_goal_hyps; new_goal_hyps.append(new_hyps); expr new_type = binding_domain(rec_type); - unsigned arity = get_arity(new_type); - // introduce minor arguments - buffer minor_args; - for (unsigned i = 0; i < arity; i++) { - expr arg_type = head_beta_reduce(binding_domain(new_type)); - name arg_name; - if (m_ids) { - arg_name = head(m_ids); - m_ids = tail(m_ids); - } else { - arg_name = binding_name(new_type); + expr rec_arg; + if (binding_info(rec_type).is_inst_implicit()) { + rec_arg = mk_type_class_param(g, binding_domain(rec_type)); + } else { + unsigned arity = get_arity(new_type); + // introduce minor arguments + buffer minor_args; + for (unsigned i = 0; i < arity; i++) { + expr arg_type = head_beta_reduce(binding_domain(new_type)); + name arg_name; + if (m_ids) { + arg_name = head(m_ids); + m_ids = tail(m_ids); + } else { + arg_name = binding_name(new_type); + } + expr new_h = mk_local(m_ngen.next(), get_unused_name(arg_name, new_goal_hyps), + arg_type, binder_info()); + minor_args.push_back(new_h); + new_goal_hyps.push_back(new_h); + new_type = instantiate(binding_body(new_type), new_h); } - expr new_h = mk_local(m_ngen.next(), get_unused_name(arg_name, new_goal_hyps), - arg_type, binder_info()); - minor_args.push_back(new_h); - new_goal_hyps.push_back(new_h); - new_type = instantiate(binding_body(new_type), new_h); - } - 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); + 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); + } + 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)); } - 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); - expr rec_arg = Fun(minor_args, Fun(new_deps, new_meta)); 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/tests/lean/hott/611.hlean b/tests/lean/hott/611.hlean new file mode 100644 index 000000000..a6271b1ab --- /dev/null +++ b/tests/lean/hott/611.hlean @@ -0,0 +1,9 @@ +open is_trunc +attribute trunc.rec [recursor] + +definition my_elim {n : trunc_index} {A : Type} {P : Type} + [Pt : is_trunc n P] (H : A → P) : trunc n A → P := +begin + intro x, induction x, + apply H, assumption +end