From b1ece388a6c64e0988d064f27ecb94cedb3d1f35 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 May 2015 09:25:07 -0700 Subject: [PATCH] feat(frontends/lean,library/tactic/induction_tactic): improve induction tactic notation, expand induction tactic implementation --- hott/init/tactic.hlean | 8 +- library/init/tactic.lean | 8 +- src/frontends/lean/elaborator.cpp | 3 +- src/frontends/lean/parser.cpp | 16 ++ src/frontends/lean/parser.h | 1 + src/library/constants.cpp | 8 + src/library/constants.h | 2 + src/library/constants.txt | 2 + src/library/tactic/expr_to_tactic.cpp | 4 + src/library/tactic/expr_to_tactic.h | 1 + src/library/tactic/induction_tactic.cpp | 251 ++++++++++++++++++++++-- src/library/user_recursors.cpp | 3 + src/library/user_recursors.h | 8 + 13 files changed, 293 insertions(+), 22 deletions(-) diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index a2a92b37e..7a7326c80 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -67,6 +67,11 @@ definition identifier := expr definition identifier_list := expr_list definition opt_identifier_list := expr_list +-- Marker for instructing the parser to parse it as '?(using )' +definition using_expr := expr +-- Constant used to denote the case were no expression was provided +definition none_expr : expr := expr.builtin + definition apply (e : expr) : tactic := builtin definition eapply (e : expr) : tactic := builtin definition fapply (e : expr) : tactic := builtin @@ -88,8 +93,7 @@ definition rewrite_tac (e : expr_list) : tactic := builtin definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin -definition induction (h : identifier) (ids : opt_identifier_list) : tactic := builtin -definition induction_using (h : identifier) (rec : expr) (ids : opt_identifier_list) : tactic := builtin +definition induction (h : identifier) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin definition intros (ids : opt_identifier_list) : tactic := builtin diff --git a/library/init/tactic.lean b/library/init/tactic.lean index c823f17fe..fe05fbf69 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -67,6 +67,11 @@ definition identifier := expr definition identifier_list := expr_list definition opt_identifier_list := expr_list +-- Marker for instructing the parser to parse it as '?(using )' +definition using_expr := expr +-- Constant used to denote the case were no expression was provided +definition none_expr : expr := expr.builtin + definition apply (e : expr) : tactic := builtin definition eapply (e : expr) : tactic := builtin definition fapply (e : expr) : tactic := builtin @@ -88,8 +93,7 @@ definition rewrite_tac (e : expr_list) : tactic := builtin definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin -definition induction (h : identifier) (ids : opt_identifier_list) : tactic := builtin -definition induction_using (h : identifier) (rec : expr) (ids : opt_identifier_list) : tactic := builtin +definition induction (h : identifier) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin definition intros (ids : opt_identifier_list) : tactic := builtin diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index bd1f09ebd..eab75a74d 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -605,7 +605,8 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) { } constraint_seq a_cs; expr d_type = binding_domain(f_type); - if (d_type == get_tactic_expr_type() || d_type == get_tactic_identifier_type()) { + if (d_type == get_tactic_expr_type() || d_type == get_tactic_identifier_type() || + d_type == get_tactic_using_expr_type()) { expr const & a = app_arg(e); expr r; if (is_local(a) && diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 06e22da92..8a8657d08 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1415,6 +1415,10 @@ static bool is_tactic_opt_identifier_list_type(expr const & e) { return is_constant(e) && const_name(e) == get_tactic_opt_identifier_list_name(); } +static bool is_tactic_using_expr(expr const & e) { + return is_constant(e) && const_name(e) == get_tactic_using_expr_name(); +} + static bool is_option_num(expr const & e) { return is_app(e) && is_constant(app_fn(e)) && const_name(app_fn(e)) == get_option_name() && is_constant(app_arg(e)) && const_name(app_arg(e)) == get_num_name(); @@ -1526,6 +1530,16 @@ expr parser::parse_tactic_option_num() { } } +expr parser::parse_tactic_using_expr() { + auto p = pos(); + if (curr_is_token(get_using_tk())) { + next(); + return parse_expr(); + } else { + return save_pos(mk_constant(get_tactic_none_expr_name()), p); + } +} + expr parser::parse_tactic_nud() { if (curr_is_identifier()) { auto id_pos = pos(); @@ -1555,6 +1569,8 @@ expr parser::parse_tactic_nud() { r = mk_app(r, parse_tactic_id_list(), id_pos); } else if (is_tactic_opt_identifier_list_type(d)) { r = mk_app(r, parse_tactic_opt_id_list(), id_pos); + } else if (is_tactic_using_expr(d)) { + r = mk_app(r, parse_tactic_using_expr(), id_pos); } else if (arity == 1 && is_option_num(d)) { r = mk_app(r, parse_tactic_option_num(), id_pos); } else { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index aebadf06c..05dcf83d7 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -243,6 +243,7 @@ class parser { expr parse_tactic_opt_expr_list(); expr parse_tactic_id_list(); expr parse_tactic_opt_id_list(); + expr parse_tactic_using_expr(); public: parser(environment const & env, io_state const & ios, diff --git a/src/library/constants.cpp b/src/library/constants.cpp index d51872194..fb72afed9 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -95,6 +95,8 @@ name const * g_tactic_expr_builtin = nullptr; name const * g_tactic_expr_list = nullptr; name const * g_tactic_expr_list_cons = nullptr; name const * g_tactic_expr_list_nil = nullptr; +name const * g_tactic_using_expr = nullptr; +name const * g_tactic_none_expr = nullptr; name const * g_tactic_identifier = nullptr; name const * g_tactic_identifier_list = nullptr; name const * g_tactic_opt_expr = nullptr; @@ -225,6 +227,8 @@ void initialize_constants() { g_tactic_expr_list = new name{"tactic", "expr_list"}; g_tactic_expr_list_cons = new name{"tactic", "expr_list", "cons"}; g_tactic_expr_list_nil = new name{"tactic", "expr_list", "nil"}; + g_tactic_using_expr = new name{"tactic", "using_expr"}; + g_tactic_none_expr = new name{"tactic", "none_expr"}; g_tactic_identifier = new name{"tactic", "identifier"}; g_tactic_identifier_list = new name{"tactic", "identifier_list"}; g_tactic_opt_expr = new name{"tactic", "opt_expr"}; @@ -356,6 +360,8 @@ void finalize_constants() { delete g_tactic_expr_list; delete g_tactic_expr_list_cons; delete g_tactic_expr_list_nil; + delete g_tactic_using_expr; + delete g_tactic_none_expr; delete g_tactic_identifier; delete g_tactic_identifier_list; delete g_tactic_opt_expr; @@ -486,6 +492,8 @@ name const & get_tactic_expr_builtin_name() { return *g_tactic_expr_builtin; } name const & get_tactic_expr_list_name() { return *g_tactic_expr_list; } name const & get_tactic_expr_list_cons_name() { return *g_tactic_expr_list_cons; } name const & get_tactic_expr_list_nil_name() { return *g_tactic_expr_list_nil; } +name const & get_tactic_using_expr_name() { return *g_tactic_using_expr; } +name const & get_tactic_none_expr_name() { return *g_tactic_none_expr; } name const & get_tactic_identifier_name() { return *g_tactic_identifier; } name const & get_tactic_identifier_list_name() { return *g_tactic_identifier_list; } name const & get_tactic_opt_expr_name() { return *g_tactic_opt_expr; } diff --git a/src/library/constants.h b/src/library/constants.h index 7c4cbe151..e90b95472 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -97,6 +97,8 @@ name const & get_tactic_expr_builtin_name(); name const & get_tactic_expr_list_name(); name const & get_tactic_expr_list_cons_name(); name const & get_tactic_expr_list_nil_name(); +name const & get_tactic_using_expr_name(); +name const & get_tactic_none_expr_name(); name const & get_tactic_identifier_name(); name const & get_tactic_identifier_list_name(); name const & get_tactic_opt_expr_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index e03222e90..dad6536cf 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -90,6 +90,8 @@ tactic.expr.builtin tactic.expr_list tactic.expr_list.cons tactic.expr_list.nil +tactic.using_expr +tactic.none_expr tactic.identifier tactic.identifier_list tactic.opt_expr diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index d019703ad..0e127b1c4 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -64,11 +64,13 @@ static expr * g_tactic_expr_type = nullptr; static expr * g_tactic_expr_builtin = nullptr; static expr * g_tactic_expr_list_type = nullptr; static expr * g_tactic_identifier_type = nullptr; +static expr * g_tactic_using_expr_type = nullptr; expr const & get_tactic_expr_type() { return *g_tactic_expr_type; } expr const & get_tactic_expr_builtin() { return *g_tactic_expr_builtin; } expr const & get_tactic_expr_list_type() { return *g_tactic_expr_list_type; } expr const & get_tactic_identifier_type() { return *g_tactic_identifier_type; } +expr const & get_tactic_using_expr_type() { return *g_tactic_using_expr_type; } static std::string * g_tactic_expr_opcode = nullptr; static std::string * g_tactic_opcode = nullptr; @@ -366,6 +368,7 @@ void initialize_expr_to_tactic() { g_tactic_expr_builtin = new expr(mk_constant(get_tactic_expr_builtin_name())); g_tactic_expr_list_type = new expr(mk_constant(get_tactic_expr_list_name())); g_tactic_identifier_type = new expr(mk_constant(get_tactic_identifier_name())); + g_tactic_using_expr_type = new expr(mk_constant(get_tactic_using_expr_name())); g_tactic_expr_opcode = new std::string("TACE"); g_tactic_expr_macro = new macro_definition(new tactic_expr_macro_definition_cell()); @@ -437,6 +440,7 @@ void finalize_expr_to_tactic() { delete g_tactic_expr_builtin; delete g_tactic_expr_list_type; delete g_tactic_identifier_type; + delete g_tactic_using_expr_type; delete g_tactic_expr_opcode; delete g_tactic_expr_macro; delete g_fixpoint_tac; diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index d4fb55bec..370d5641e 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -39,6 +39,7 @@ bool is_tactic_expr(expr const & e); expr const & get_tactic_expr_expr(expr const & e); void check_tactic_expr(expr const & e, char const * msg); expr const & get_tactic_expr_list_type(); +expr const & get_tactic_using_expr_type(); expr mk_expr_list(unsigned num, expr const * args); diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index 60c4c8aa7..cdc11fab4 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -4,36 +4,253 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "kernel/abstract.h" +#include "kernel/inductive/inductive.h" +#include "library/util.h" +#include "library/user_recursors.h" +#include "library/constants.h" +#include "library/reducible.h" +#include "library/locals.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" namespace lean { -tactic induction_tactic(name const & H, optional const & rec, list const & ids) { - // TODO(Leo) +class has_rec_opaque_converter : public default_converter { + has_recursors_pred m_pred; +public: + has_rec_opaque_converter(environment const & env):default_converter(env), m_pred(env) {} + virtual bool is_opaque(declaration const & d) const { + if (m_pred(d.get_name())) + return true; + return default_converter::is_opaque(d); + } +}; + +class induction_tac { + environment const & m_env; + io_state const & m_ios; + type_checker & m_tc; + name m_h_name; + optional m_rec_name; + list m_ids; + name_generator m_ngen; + substitution m_subst; + bool m_throw_ex; + bool m_standard; + + void assign(goal const & g, expr const & val) { + ::lean::assign(m_subst, g, val); + } + + /** \brief Split hyps into two "telescopes". + - non_deps : hypotheses that do not depend on H nor its indices + - deps : hypotheses that depend on H or its indices (directly or indirectly) + */ + void split_deps(buffer const & hyps, expr const & h, buffer const & indices, buffer & non_deps, buffer & deps) { + for (expr const & hyp : hyps) { + if (hyp == h) { + // we clear h + } else if (std::find(indices.begin(), indices.end(), hyp) != indices.end()) { + // hyp is an index + non_deps.push_back(hyp); + } else if (depends_on(hyp, h) || depends_on_any(hyp, indices) || depends_on_any(hyp, deps)) { + deps.push_back(hyp); + } else { + non_deps.push_back(hyp); + } + } + } + + bool validate_rec_info(goal const & g, expr const & h, expr const & h_type, recursor_info const & rec_info) { + unsigned nindices = rec_info.get_num_indices(); + if (nindices == 0) + return true; + buffer args; + get_app_args(h_type, args); + if (rec_info.get_num_params() + nindices != args.size()) + return false; + unsigned fidx = args.size() - nindices; + for (unsigned i = fidx; i < args.size(); i++) { + if (!is_local(args[i])) + return false; // the indices must be local constants + for (unsigned j = 0; j < i; j++) { + if (is_local(args[j]) && mlocal_name(args[j]) == mlocal_name(args[i])) + return false; // the indices must be distinct local constants + } + } + if (!rec_info.has_dep_elim() && depends_on(g.get_type(), h)) + return false; + return true; + } + + goals apply_recursor(goal const & g, expr const & h, expr const & h_type, recursor_info const & rec_info) { + expr const & g_type = g.get_type(); + level g_lvl = sort_level(m_tc.ensure_type(g_type).first); + buffer I_args; + expr const & I = get_app_args(h_type, I_args); + buffer params; + params.append(rec_info.get_num_params(), I_args.data()); + buffer indices; + indices.append(rec_info.get_num_indices(), I_args.data() + params.size()); + levels rec_levels; + if (auto lpos = rec_info.get_motive_univ_pos()) { + buffer ls; + unsigned i = 0; + for (level const & l : ls) { + if (i == *lpos) + ls.push_back(g_lvl); + ls.push_back(l); + i++; + } + 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); + rec = mk_app(rec, params); + expr motive = g_type; + if (rec_info.has_dep_elim()) + motive = Fun(h, motive); + motive = Fun(indices, motive); + rec = mk_app(rec, motive); + + // TODO(Leo): + regular(m_env, m_ios) << ">> rec: " << rec << "\n"; + + return goals(); + } + + optional execute(goal const & g, expr const & h, expr const & h_type, name const & rec) { + try { + recursor_info rec_info = get_recursor_info(m_env, rec); + if (!validate_rec_info(g, h, h_type, rec_info)) { + throw tactic_exception(sstream() << "invalid 'induction' tactic, indices occurring in the hypothesis '" + << h << "' must be distinct variables"); + } + unsigned nindices = rec_info.get_num_indices(); + buffer h_type_args; + get_app_args(h_type, h_type_args); + buffer indices; + indices.append(nindices, h_type_args.end() - nindices); + buffer hyps, non_deps, deps; + g.get_hyps(hyps); + split_deps(hyps, h, indices, non_deps, deps); + buffer & new_hyps = non_deps; + new_hyps.push_back(h); + expr new_type = Pi(deps, g.get_type()); + expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)), new_hyps); + goal new_g(new_meta, new_type); + expr val = mk_app(new_meta, deps); + assign(g, val); + regular(m_env, m_ios) << new_g << "\n"; + goals new_gs = apply_recursor(new_g, h, h_type, rec_info); + // TODO(Leo): finish + return optional(); + } catch (exception const & ex) { + throw tactic_exception(sstream() << "invalid 'induction' tactic, " << ex.what()); + } + } + +public: + induction_tac(environment const & env, io_state const & ios, name_generator const & ngen, + type_checker & tc, substitution const & subst, name const & h_name, + optional const & rec_name, list const & ids, + bool throw_ex): + m_env(env), m_ios(ios), m_tc(tc), m_h_name(h_name), m_rec_name(rec_name), m_ids(ids), + m_ngen(ngen), m_subst(subst), m_throw_ex(throw_ex) { + m_standard = is_standard(env); + } + + name_generator const & get_ngen() const { return m_ngen; } + + substitution const & get_subst() const { return m_subst; } + + expr normalize_H_type(expr const & H) { + lean_assert(is_local(H)); + type_checker aux_tc(m_env, m_ngen.mk_child(), std::unique_ptr(new has_rec_opaque_converter(m_env))); + return aux_tc.whnf(mlocal_type(H)).first; + } + + optional execute(goal const & g) { + try { + auto p = g.find_hyp(m_h_name); + if (!p) + throw tactic_exception(sstream() << "invalid 'induction' tactic, unknown hypothesis '" << m_h_name << "'"); + expr H = p->first; + expr H_type = normalize_H_type(H); + expr I = get_app_fn(H_type); + if (is_constant(I)) { + if (m_rec_name) { + return execute(g, H, H_type, *m_rec_name); + } else if (inductive::is_inductive_decl(m_env, const_name(I))) { + return execute(g, H, H_type, inductive::get_elim_name(const_name(I))); + } else if (auto rs = get_recursors_for(m_env, const_name(I))) { + return execute(g, H, H_type, head(rs)); + } + } + throw tactic_exception(sstream() << "invalid 'induction' tactic, hypothesis '" << m_h_name + << "' must have a type that is associated with a recursor"); + } catch (tactic_exception & ex) { + if (m_throw_ex) + throw; + return optional(); + } + } +}; + +tactic induction_tactic(name const & H, optional rec, list const & ids) { name rec1 = "unknown"; if (rec) rec1 = *rec; std::cout << "induction: " << H << " " << rec1 << " " << ids << "\n"; - return id_tactic(); + + auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) -> optional { + goals const & gs = ps.get_goals(); + if (empty(gs)) { + throw_no_goal_if_enabled(ps); + return none_proof_state(); + } + goal g = head(gs); + goals tail_gs = tail(gs); + name_generator ngen = ps.get_ngen(); + std::unique_ptr tc = mk_type_checker(env, ngen.mk_child()); + induction_tac tac(env, ios, ngen, *tc, ps.get_subst(), H, rec, ids, ps.report_failure()); + if (auto res = tac.execute(g)) { + proof_state new_s(ps, append(*res, tail_gs), tac.get_subst(), tac.get_ngen()); + return some_proof_state(new_s); + } else { + return none_proof_state(); + } + }; + return tactic01(fn); } void initialize_induction_tactic() { register_tac(name{"tactic", "induction"}, [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - name H = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'induction' tactic, argument must be an identifier"); + buffer args; + get_app_args(e, args); + if (args.size() != 3) + throw expr_to_tactic_exception(e, "invalid 'induction' tactic, insufficient number of arguments"); + name H = tactic_expr_to_id(args[0], "invalid 'induction' tactic, argument must be an identifier"); buffer ids; - get_tactic_id_list_elements(app_arg(e), ids, "invalid 'induction' tactic, list of identifiers expected"); - return induction_tactic(H, optional(), to_list(ids.begin(), ids.end())); - }); - register_tac(name{"tactic", "induction_using"}, - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - name H = tactic_expr_to_id(app_arg(app_fn(app_fn(e))), "invalid 'induction' tactic, argument must be an identifier"); - check_tactic_expr(app_arg(app_fn(e)), "invalid 'induction' tactic, invalid argument"); - expr rec = get_tactic_expr_expr(app_arg(app_fn(e))); - if (!is_constant(rec)) - throw expr_to_tactic_exception(app_arg(app_fn(e)), "invalid 'induction' tactic, constant expected"); - buffer ids; - get_tactic_id_list_elements(app_arg(e), ids, "invalid 'induction' tactic, list of identifiers expected"); - return induction_tactic(H, optional(const_name(rec)), to_list(ids.begin(), ids.end())); + get_tactic_id_list_elements(args[2], ids, "invalid 'induction' tactic, list of identifiers expected"); + check_tactic_expr(args[1], "invalid 'induction' tactic, invalid argument"); + expr rec = get_tactic_expr_expr(args[1]); + if (!is_constant(rec)) { + throw expr_to_tactic_exception(args[1], "invalid 'induction' tactic, constant expected"); + } + name const & cname = const_name(rec); + if (cname == get_tactic_none_expr_name()) { + return induction_tactic(H, optional(), to_list(ids.begin(), ids.end())); + } else { + return induction_tactic(H, optional(cname), to_list(ids.begin(), ids.end())); + } }); } void finalize_induction_tactic() { diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index c6fa8c135..83c6524b5 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -243,6 +243,9 @@ list get_recursors_for(environment const & env, name const & I) { return list(); } +has_recursors_pred::has_recursors_pred(environment const & env): + m_type2recursors(recursor_ext::get_state(env).m_type2recursors) {} + void initialize_user_recursors() { g_class_name = new name("recursor"); g_key = new std::string("urec"); diff --git a/src/library/user_recursors.h b/src/library/user_recursors.h index 1b4c80849..4a31c370e 100644 --- a/src/library/user_recursors.h +++ b/src/library/user_recursors.h @@ -40,6 +40,14 @@ public: environment add_user_recursor(environment const & env, name const & r, bool persistent); recursor_info get_recursor_info(environment const & env, name const & r); list get_recursors_for(environment const & env, name const & I); + +class has_recursors_pred { + name_map> m_type2recursors; +public: + has_recursors_pred(environment const & env); + bool operator()(name const & n) const { return m_type2recursors.contains(n); } +}; + void initialize_user_recursors(); void finalize_user_recursors(); }