feat(frontends/lean,library/tactic/induction_tactic): improve induction tactic notation, expand induction tactic implementation

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 <expr>)'
+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 (h : identifier) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin
-definition induction_using (h : identifier) (rec : expr) (ids : opt_identifier_list) : tactic := builtin
 
 definition intros (ids : opt_identifier_list) : tactic := builtin
 

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 <expr>)'
+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 (h : identifier) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin
-definition induction_using (h : identifier) (rec : expr) (ids : opt_identifier_list) : tactic := builtin
 
 definition intros (ids : opt_identifier_list) : tactic := builtin
 

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) &&

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 {

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,

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; }

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();

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

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;

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);
 

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<name> const & rec, list<name> const & ids) {
+class has_rec_opaque_converter : public default_converter {
-    // TODO(Leo)
+    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<name>        m_rec_name;
+    list<name>            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<expr> const & hyps, expr const & h, buffer<expr> const & indices, buffer<expr> & non_deps, buffer<expr> & 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<expr> 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<expr> I_args;
+        expr const & I = get_app_args(h_type, I_args);
+        buffer<expr> params;
+        params.append(rec_info.get_num_params(), I_args.data());
+        buffer<expr> 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<level> 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<goals> 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<expr> h_type_args;
+            get_app_args(h_type, h_type_args);
+            buffer<expr> indices;
+            indices.append(nindices, h_type_args.end() - nindices);
+            buffer<expr> hyps, non_deps, deps;
+            g.get_hyps(hyps);
+            split_deps(hyps, h, indices, non_deps, deps);
+            buffer<expr> & 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<goals>();
+        } 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<name> const & rec_name, list<name> 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<converter>(new has_rec_opaque_converter(m_env)));
+        return aux_tc.whnf(mlocal_type(H)).first;
+    }
+
+    optional<goals> 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<goals>();
+        }
+    }
+};
+
+tactic induction_tactic(name const & H, optional<name> rec, list<name> 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<proof_state> {
+        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<type_checker> 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<expr> 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<name> ids;
-                     get_tactic_id_list_elements(app_arg(e), ids, "invalid 'induction' tactic, list of identifiers expected");
+                     get_tactic_id_list_elements(args[2], ids, "invalid 'induction' tactic, list of identifiers expected");
-                     return induction_tactic(H, optional<name>(), to_list(ids.begin(), ids.end()));
+                     check_tactic_expr(args[1], "invalid 'induction' tactic, invalid argument");
-                 });
+                     expr rec = get_tactic_expr_expr(args[1]);
-    register_tac(name{"tactic", "induction_using"},
+                     if (!is_constant(rec)) {
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                         throw expr_to_tactic_exception(args[1], "invalid 'induction' tactic, constant expected");
-                     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");
+                     name const & cname = const_name(rec);
-                     expr rec = get_tactic_expr_expr(app_arg(app_fn(e)));
+                     if (cname == get_tactic_none_expr_name()) {
-                     if (!is_constant(rec))
+                         return induction_tactic(H, optional<name>(), to_list(ids.begin(), ids.end()));
-                         throw expr_to_tactic_exception(app_arg(app_fn(e)), "invalid 'induction' tactic, constant expected");
+                     } else {
-                     buffer<name> ids;
+                         return induction_tactic(H, optional<name>(cname), to_list(ids.begin(), ids.end()));
-                     get_tactic_id_list_elements(app_arg(e), ids, "invalid 'induction' tactic, list of identifiers expected");
+                     }
-                     return induction_tactic(H, optional<name>(const_name(rec)), to_list(ids.begin(), ids.end()));
                  });
 }
 void finalize_induction_tactic() {

src/library/user_recursors.cpp

@@ -243,6 +243,9 @@ list<name> get_recursors_for(environment const & env, name const & I) {
         return list<name>();
 }
 
+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");

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<name> get_recursors_for(environment const & env, name const & I);
+
+class has_recursors_pred {
+    name_map<list<name>>    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();
 }