feat(library/blast): add "recursor" (aka elimination/induction) action

src/library/blast/CMakeLists.txt

@@ -2,4 +2,4 @@ add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
   init_module.cpp simplifier.cpp simple_actions.cpp intros_action.cpp proof_expr.cpp
   options.cpp choice_point.cpp simple_strategy.cpp backward_action.cpp util.cpp
   gexpr.cpp revert_action.cpp subst_action.cpp no_confusion_action.cpp
-  simplify_actions.cpp strategy.cpp)
+  simplify_actions.cpp strategy.cpp recursor_action.cpp)

src/library/blast/blast.cpp

@@ -457,6 +457,7 @@ public:
         return m_tmp_local_generator.mk_tmp_local(type, bi);
     }
     expr whnf(expr const & e) { return m_tctx.whnf(e); }
+    expr relaxed_whnf(expr const & e) { return m_tctx.relaxed_whnf(e); }
     expr infer_type(expr const & e) { return m_tctx.infer(e); }
     bool is_prop(expr const & e) { return m_tctx.is_prop(e); }
     bool is_def_eq(expr const & e1, expr const & e2) { return m_tctx.is_def_eq(e1, e2); }
@@ -565,11 +566,21 @@ bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs) {
     return g_blastenv->is_relation(e, rop, lhs, rhs);
 }
 
+bool is_relation(expr const & e) {
+    name rop; expr lhs, rhs;
+    return is_relation(e, rop, lhs, rhs);
+}
+
 expr whnf(expr const & e) {
     lean_assert(g_blastenv);
     return g_blastenv->whnf(e);
 }
 
+expr relaxed_whnf(expr const & e) {
+    lean_assert(g_blastenv);
+    return g_blastenv->relaxed_whnf(e);
+}
+
 expr infer_type(expr const & e) {
     lean_assert(g_blastenv);
     return g_blastenv->infer_type(e);

src/library/blast/blast.h

@@ -37,9 +37,11 @@ projection_info const * get_projection_info(name const & n);
 /** \brief Return true iff \c e is a relation application,
     and store the relation name, lhs and rhs in the output arguments. */
 bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs);
+bool is_relation(expr const & e);
 /** \brief Put the given expression in weak-head-normal-form with respect to the
     current state being processed by the blast tactic. */
 expr whnf(expr const & e);
+expr relaxed_whnf(expr const & e);
 /** \brief Normalize the given expression using the blast type context.
     This procedure caches results.
     \remark This procedure is intended for normalizing instances that are not subsingletons. */
@@ -129,6 +131,15 @@ public:
     tmp_type_context & operator*() { return *m_ctx; }
 };
 
+class scope_curr_state {
+    state m_saved;
+    bool  m_keep;
+public:
+    scope_curr_state():m_saved(curr_state()), m_keep(false) {}
+    ~scope_curr_state() { if (!m_keep) curr_state() = m_saved; }
+    void commit() { m_keep = true; }
+};
+
 /**
     \brief Convert an external expression into a blast expression
     It converts meta-variables to blast meta-variables, and ensures the expressions

src/library/blast/recursor_action.cpp

@@ -0,0 +1,289 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/instantiate.h"
+#include "kernel/inductive/inductive.h"
+#include "library/user_recursors.h"
+#include "library/blast/revert_action.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+optional<name> is_recursor_action_target(hypothesis_idx hidx) {
+    state & s = curr_state();
+    hypothesis const * h = s.get_hypothesis_decl(hidx);
+    lean_assert(h);
+    expr const & type = h->get_type();
+    if (!is_app(type) && !is_constant(type))
+        return optional<name>();
+    if (is_relation(type))
+        return optional<name>(); // we don't apply recursors to equivalence relations: =, ~, <->, etc.
+    if (!h->is_assumption())
+        return optional<name>(); // we only consider assumptions
+    // TODO(Leo): more restrictions?
+    // TODO(Leo): consider user-provided hints
+    expr const & I    = get_app_fn(type);
+    if (!is_constant(I))
+        return optional<name>();
+    if (inductive::is_inductive_decl(env(), const_name(I)))
+        return optional<name>(name(inductive::get_elim_name(const_name(I)))); // it is builtin recursive datatype
+    list<name> Rs = get_recursors_for(env(), const_name(I));
+    if (!Rs)
+        return optional<name>();
+    else
+        return optional<name>(head(Rs)); // type has user-defined recursors
+}
+
+unsigned get_num_minor_premises(name const & R) {
+    return get_recursor_info(env(), R).get_num_minors();
+}
+
+bool is_recursive_recursor(name const & R) {
+    return get_recursor_info(env(), R).is_recursive();
+}
+
+struct recursor_proof_step_cell : public proof_step_cell {
+    bool       m_dep;
+    branch     m_branch;      // branch for backtracking
+    expr       m_proof;       // recursor-application (the position where the goal-proofs are marked by the local constants).
+    list<expr> m_goals;       // type of each subgoal/branch encoded as a local constant
+    list<expr> m_goal_proofs; // proofs generated so far
+
+    recursor_proof_step_cell(bool dep, branch const & b, expr const & pr, list<expr> const & goals, list<expr> const & goal_proofs):
+        m_dep(dep), m_branch(b), m_proof(pr), m_goals(goals), m_goal_proofs(goal_proofs) {
+    }
+
+    virtual ~recursor_proof_step_cell() {}
+
+    virtual action_result resolve(expr const & pr) const {
+        state & s = curr_state();
+        s.set_branch(m_branch);
+        if (!m_dep) {
+            // It is not a dependent elimination, so if pr did not use new hypothesis,
+            // we don't need to investigate other branches.
+            // This is also a form of non-chronological backtracking.
+            expr const & goal    = head(m_goals);
+            unsigned arity       = get_arity(mlocal_type(goal));
+            expr it              = pr;
+            bool skip            = true;
+            for (unsigned i = 0; i < arity; i++) {
+                if (!is_lambda(it)) {
+                    skip = false;
+                    break;
+                }
+                it = binding_body(it);
+                if (!closed(it)) {
+                    skip = false;
+                    break;
+                }
+            }
+            if (skip) {
+                lean_assert(closed(it));
+                return action_result::solved(it);
+            }
+        }
+        list<expr> new_goals = tail(m_goals);
+        list<expr> new_prs   = cons(pr, m_goal_proofs);
+        if (empty(new_goals)) {
+            buffer<expr> proof_args;
+            buffer<expr> gs;
+            to_buffer(m_goals, gs);
+            expr const & rec = get_app_args(m_proof, proof_args);
+            // update proof_args that are goals with their proofs
+            unsigned i = proof_args.size();
+            while (i > 0) {
+                --i;
+                if (!gs.empty() && proof_args[i] == gs.back()) {
+                    lean_assert(new_prs);
+                    proof_args[i] = head(new_prs);
+                    new_prs       = tail(new_prs);
+                }
+            }
+            return action_result::solved(mk_app(rec, proof_args));
+        } else {
+            s.pop_proof_step();
+            s.push_proof_step(new recursor_proof_step_cell(m_dep, m_branch, m_proof, new_goals, new_prs));
+            s.set_target(mlocal_type(head(new_goals)));
+            return action_result::new_branch();
+        }
+    }
+};
+
+action_result recursor_action(hypothesis_idx hidx, name const & R) {
+    state & s = curr_state();
+    hypothesis const * h = s.get_hypothesis_decl(hidx);
+    lean_assert(h);
+    expr const & type = h->get_type();
+    lean_assert(is_constant(get_app_fn(type)));
+
+    recursor_info rec_info = get_recursor_info(env(), R);
+
+    if (!rec_info.has_dep_elim() && s.target_depends_on(hidx)) {
+        // recursor does does not support dependent elimination, but conclusion
+        // depends on major premise
+        return action_result::failed();
+    }
+
+    buffer<expr> type_args;
+    get_app_args(type, type_args);
+    buffer<optional<expr>> params;
+    for (optional<unsigned> const & pos : rec_info.get_params_pos()) {
+        if (!pos) {
+            params.push_back(none_expr());
+        } else if (*pos >= type_args.size()) {
+            return action_result::failed(); // major premise type is ill-formed
+        } else {
+            params.push_back(some_expr(type_args[*pos]));
+        }
+    }
+
+    buffer<expr> indices;
+    list<unsigned> const & idx_pos = rec_info.get_indices_pos();
+    for (unsigned pos : idx_pos) {
+        if (pos >= type_args.size()) {
+            return action_result::failed(); // major premise type is ill-formed");
+        }
+        expr const & idx = type_args[pos];
+        if (!is_href(idx)) {
+            return action_result::failed(); // argument of major premise type is not a href
+        }
+        for (unsigned i = 0; i < type_args.size(); i++) {
+            if (i != pos && is_local(type_args[i]) && mlocal_name(type_args[i]) == mlocal_name(idx)) {
+                return action_result::failed(); // argument of major premise is an index, but it occurs more than once
+            }
+            if (i > pos && // occurs after idx
+                std::find(idx_pos.begin(), idx_pos.end(), i) != idx_pos.end() && // it is also an index
+                is_href(type_args[i]) && // if it is not an index, it will fail anyway.
+                s.hidx_depends_on(href_index(idx), href_index(type_args[i]))) {
+                // argument of major premise type is an index, but its type depends on another index
+                return action_result::failed();
+            }
+        }
+        indices.push_back(idx);
+    }
+
+    scope_curr_state save_state;
+    hypothesis_idx_buffer_set to_revert;
+    s.collect_direct_forward_deps(hidx, to_revert);
+    for (auto i : indices)
+        s.collect_direct_forward_deps(href_index(i), to_revert);
+    revert_action(to_revert);
+
+    expr target       = s.get_target();
+    auto target_level = get_type_context().get_level_core(target);
+    if (!target_level) return action_result::failed(); // failed to extract universe level of target
+
+    buffer<level> rec_lvls;
+    expr const & I = get_app_fn(type);
+    buffer<level> I_lvls;
+    to_buffer(const_levels(I), I_lvls);
+    bool found_target_lvl = false;
+    for (unsigned idx : rec_info.get_universe_pos()) {
+        if (idx == recursor_info::get_motive_univ_idx()) {
+            rec_lvls.push_back(*target_level);
+            found_target_lvl = true;
+        } else {
+            if (idx >= I_lvls.size())
+                return action_result::failed(); // ill-formed recursor
+            rec_lvls.push_back(I_lvls[idx]);
+        }
+    }
+
+    if (!found_target_lvl && !is_zero(*target_level)) {
+        // recursor can only eliminate into Prop
+        return action_result::failed();
+    }
+    expr rec    = mk_constant(rec_info.get_name(), to_list(rec_lvls));
+
+    for (optional<expr> const & p : params) {
+        if (p) {
+            rec = mk_app(rec, *p);
+        } else {
+            // try type class resolution to synthesize argument
+            expr rec_type = relaxed_whnf(infer_type(rec));
+            if (!is_pi(rec_type))
+                return action_result::failed(); // ill-formed recursor
+            expr arg_type = binding_domain(rec_type);
+            if (auto inst = mk_class_instance(arg_type)) {
+                rec = mk_app(rec, *inst);
+            } else {
+                return action_result::failed(); // failed to generate instance
+            }
+        }
+    }
+
+    expr motive = target;
+    if (rec_info.has_dep_elim())
+        motive  = s.mk_lambda(h->get_self(), motive);
+    motive = s.mk_lambda(indices, motive);
+    rec      = mk_app(rec, motive);
+
+    expr rec_type          = relaxed_whnf(infer_type(rec));
+    unsigned curr_pos      = params.size() + 1 /* motive */;
+    unsigned first_idx_pos = rec_info.get_first_index_pos();
+    bool consumed_major    = false;
+    buffer<expr> new_goals;
+
+    while (is_pi(rec_type) && curr_pos < rec_info.get_num_args()) {
+        if (first_idx_pos == curr_pos) {
+            for (expr const & idx : indices) {
+                rec      = mk_app(rec, idx);
+                rec_type = relaxed_whnf(instantiate(binding_body(rec_type), idx));
+                if (!is_pi(rec_type))
+                    return action_result::failed(); // ill-formed type
+                curr_pos++;
+            }
+            rec      = mk_app(rec, h->get_self());
+            rec_type = relaxed_whnf(instantiate(binding_body(rec_type), h->get_self()));
+            consumed_major = true;
+            curr_pos++;
+        } else {
+            expr new_type  = binding_domain(rec_type);
+            expr rec_arg;
+            if (binding_info(rec_type).is_inst_implicit()) {
+                auto inst = mk_class_instance(new_type);
+                if (!inst) return action_result::failed(); // type class resolution failed
+                rec_arg   = *inst;
+            } else {
+                rec_arg = mk_fresh_local(new_type); // placeholder
+                new_goals.push_back(rec_arg);
+            }
+            rec       = mk_app(rec, rec_arg);
+            rec_type  = relaxed_whnf(instantiate(binding_body(rec_type), rec_arg));
+            curr_pos++;
+        }
+    }
+
+    if (curr_pos != rec_info.get_num_args() || !consumed_major)
+        return action_result::failed(); // ill-formed recursor
+
+    save_state.commit();
+
+    if (new_goals.empty())
+        return action_result::solved(rec);
+    s.del_hypothesis(hidx);
+    s.push_proof_step(new recursor_proof_step_cell(rec_info.has_dep_elim(), s.get_branch(), rec, to_list(new_goals), list<expr>()));
+    s.set_target(mlocal_type(new_goals[0]));
+    return action_result::new_branch();
+}
+
+action_result recursor_action(hypothesis_idx hidx) {
+    state & s = curr_state();
+    hypothesis const * h = s.get_hypothesis_decl(hidx);
+    lean_assert(h);
+    expr const & type = h->get_type();
+    expr const & I    = get_app_fn(type);
+    if (!is_constant(I))
+        return action_result::failed();
+    list<name> Rs = get_recursors_for(env(), const_name(I));
+    for (auto R : Rs) {
+        auto r = recursor_action(hidx, R);
+        if (!failed(r))
+            return r;
+    }
+    return action_result::failed();
+}
+}}

src/library/blast/recursor_action.h

@@ -0,0 +1,20 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/blast/action_result.h"
+#include "library/blast/hypothesis.h"
+namespace lean {
+namespace blast {
+/** \brief Return the name of the recursor that can be used with the given hypothesis */
+optional<name> is_recursor_action_target(hypothesis_idx hidx);
+
+/** \brief Return the number of minor premises of the given recursor */
+unsigned get_num_minor_premises(name const & R);
+
+action_result recursor_action(hypothesis_idx hidx, name const & R);
+action_result recursor_action(hypothesis_idx hidx);
+}}

src/library/blast/simple_strategy.cpp

@@ -44,6 +44,16 @@ class simple_strategy : public strategy {
             return r;
         }
 
+        if (optional<name> R = is_recursor_action_target(*hidx)) {
+            if (get_num_minor_premises(*R) == 1) {
+                action_result r = recursor_action(*hidx, *R);
+                if (!failed(r)) {
+                    if (!preprocess) display_action("recursor");
+                    return r;
+                }
+            }
+        }
+
         return action_result::new_branch();
     }
 

src/library/blast/state.h

@@ -318,7 +318,8 @@ public:
     void set_target(expr const & t);
     expr const & get_target() const { return m_branch.m_target; }
     /** \brief Return true iff the target depends on the given hypothesis */
-    bool target_depends_on(expr const & h) const { return m_branch.m_target_deps.contains(href_index(h)); }
+    bool target_depends_on(hypothesis_idx hidx) const { return m_branch.m_target_deps.contains(hidx); }
+    bool target_depends_on(expr const & h) const { return target_depends_on(href_index(h)); }
 
     /************************
        Proof steps

src/library/type_context.cpp

@@ -1052,10 +1052,18 @@ expr type_context::infer_lambda(expr e) {
     return r;
 }
 
-/** \brief Make sure \c e is a sort, if it is not throw an exception using \c ref as a reference */
-void type_context::ensure_sort(expr const & e, expr const & /* ref */) {
-    // Remark: for simplicity reasons, we just fail if \c e is not a sort.
-    if (!is_sort(e))
+optional<level> type_context::get_level_core(expr const & A) {
+    expr A_type = relaxed_whnf(infer(A));
+    if (is_sort(A_type))
+        return some_level(sort_level(A_type));
+    else
+        return none_level();
+}
+
+level type_context::get_level(expr const & A) {
+    if (auto r = get_level_core(A))
+        return *r;
+    else
         throw exception("infer type failed, sort expected");
 }
 
@@ -1065,17 +1073,13 @@ expr type_context::infer_pi(expr const & e0) {
     expr e = e0;
     while (is_pi(e)) {
         expr d      = instantiate_rev(binding_domain(e), ls.size(), ls.data());
-        expr d_type = relaxed_whnf(infer(d));
-        ensure_sort(d_type, e0);
-        us.push_back(sort_level(d_type));
+        us.push_back(get_level(d));
         expr l  = mk_tmp_local(d, binding_info(e));
         ls.push_back(l);
         e = binding_body(e);
     }
     e = instantiate_rev(e, ls.size(), ls.data());
-    expr e_type = relaxed_whnf(infer(e));
-    ensure_sort(e_type, e0);
-    level r = sort_level(e_type);
+    level r = get_level(e);
     unsigned i = ls.size();
     bool imp = m_env.impredicative();
     while (i > 0) {

src/library/type_context.h

@@ -443,6 +443,11 @@ public:
      */
     bool is_def_eq(expr const & e1, expr const & e2);
 
+    /** \brief Return the universe level for type A. If A is not a type return none. */
+    optional<level> get_level_core(expr const & A);
+    /** \brief Similar to previous method, but throws exception instead */
+    level get_level(expr const & A);
+
     /** \brief If \c type is a type class, return its name */
     optional<name> is_class(expr const & type);
 

tests/lean/run/blast14.lean

@@ -0,0 +1,13 @@
+set_option blast.init_depth 10
+set_option blast.inc_depth 1000
+
+definition lemma1 (p q : Prop) : p ∧ q → q ∧ p :=
+by blast
+
+definition lemma2 (p q r s : Prop) : r ∧ s → p ∧ q → q ∧ p :=
+by blast
+
+print lemma2 -- unnecessary and.rec's are not included
+
+example (p q : Prop) : p ∧ p ∧ q ∧ q → q ∧ p :=
+by blast