feat(library/blast): add basic support for non-recursive recursors/eliminators in the simple_strategy, fix bug at recursor_action

src/library/blast/blast.cpp

@@ -456,6 +456,9 @@ public:
     expr mk_fresh_local(expr const & type, binder_info const & bi) {
         return m_tmp_local_generator.mk_tmp_local(type, bi);
     }
+    bool is_fresh_local(expr const & e) const {
+        return m_tmp_local_generator.is_tmp_local(e);
+    }
     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); }
@@ -611,6 +614,11 @@ expr mk_fresh_local(expr const & type, binder_info const & bi) {
     return g_blastenv->mk_fresh_local(type, bi);
 }
 
+bool is_fresh_local(expr const & e) {
+    lean_assert(g_blastenv);
+    return g_blastenv->is_fresh_local(e);
+}
+
 optional<congr_lemma> mk_congr_lemma_for_simp(expr const & fn, unsigned num_args) {
     lean_assert(g_blastenv);
     return g_blastenv->mk_congr_lemma_for_simp(fn, num_args);

src/library/blast/blast.h

@@ -30,6 +30,7 @@ type_context & get_type_context();
 state & curr_state();
 /** \brief Return a thread local fresh local constant. */
 expr mk_fresh_local(expr const & type, binder_info const & bi = binder_info());
+bool is_fresh_local(expr const & e);
 /** \brief Return true iff the given constant name is marked as reducible in env() */
 bool is_reducible(name const & n);
 /** \brief Return a nonnull projection_info object if \c n is the name of a projection in env() */

src/library/blast/recursor_action.cpp

@@ -94,20 +94,19 @@ struct recursor_proof_step_cell : public proof_step_cell {
         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()) {
+                if (is_fresh_local(proof_args[i])) {
                     lean_assert(new_prs);
                     proof_args[i] = head(new_prs);
                     new_prs       = tail(new_prs);
                 }
             }
-            return action_result::solved(mk_app(rec, proof_args));
+            expr result = mk_app(rec, proof_args);
+            return action_result::solved(result);
         } else {
             s.pop_proof_step();
             s.push_proof_step(new recursor_proof_step_cell(m_dep, m_branch, m_proof, new_goals, new_prs));

src/library/blast/recursor_action.h

@@ -14,6 +14,7 @@ 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);
+bool is_recursive_recursor(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

@@ -45,12 +45,25 @@ class simple_strategy : public strategy {
         }
 
         if (optional<name> R = is_recursor_action_target(*hidx)) {
-            if (get_num_minor_premises(*R) == 1) {
+            unsigned num_minor = get_num_minor_premises(*R);
+            if (num_minor == 1) {
                 action_result r = recursor_action(*hidx, *R);
                 if (!failed(r)) {
                     if (!preprocess) display_action("recursor");
                     return r;
                 }
+            } else {
+                // If the hypothesis recursor has more than 1 minor premise, we
+                // put it in a priority queue.
+                // TODO(Leo): refine
+
+                // TODO(Leo): the following weight computation is too simple...
+                double w = 1.0 / (static_cast<double>(*hidx) + 1.0);
+                if (!is_recursive_recursor(*R)) {
+                    // TODO(Leo): we need a better strategy for handling recursive recursors...
+                    w += static_cast<double>(num_minor);
+                    curr_state().add_to_rec_queue(*hidx, w);
+                }
             }
         }
 
@@ -95,6 +108,16 @@ class simple_strategy : public strategy {
             return action_result::solved(*pr);
         }
 
+        while (auto hidx = curr_state().select_rec_hypothesis()) {
+            if (optional<name> R = is_recursor_action_target(*hidx)) {
+                r = recursor_action(*hidx, *R);
+                if (!failed(r)) {
+                    display_action("recursor");
+                    return r;
+                }
+            }
+        }
+
         r = constructor_action();
         if (!failed(r)) {
             display_action("constructor");

tests/lean/run/blast16.lean

@@ -0,0 +1,11 @@
+set_option blast.init_depth 10
+set_option blast.inc_depth 100
+set_option blast.trace true
+
+example (p q : Prop) : p ∨ q → q ∨ p :=
+by blast
+
+definition lemma1 (p q r s : Prop) (a b : nat) : r ∨ s → p ∨ q → a = b → q ∨ p :=
+by blast
+
+print lemma1