feat(library/blast): add "trivial" action

src/library/blast/blast.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/normalize.h"
 #include "library/class.h"
 #include "library/type_context.h"
+#include "library/relation_manager.h"
 #include "library/congr_lemma_manager.h"
 #include "library/projection.h"
 #include "library/tactic/goal.h"
@@ -47,6 +48,7 @@ class blastenv {
     name_predicate             m_class_pred;
     name_predicate             m_instance_pred;
     name_map<projection_info>  m_projection_info;
+    is_relation_pred           m_is_relation_pred;
     state                      m_curr_state;   // current state
     tmp_type_context_pool      m_tmp_ctx_pool;
     tmp_type_context_ptr       m_tmp_ctx; // for app_builder and congr_lemma_manager
@@ -402,6 +404,7 @@ public:
         m_not_reducible_pred(mk_not_reducible_pred(env)),
         m_class_pred(mk_class_pred(env)),
         m_instance_pred(mk_instance_pred(env)),
+        m_is_relation_pred(mk_is_relation_pred(env)),
         m_tmp_ctx(mk_tmp_type_context()),
         m_app_builder(*m_tmp_ctx),
         m_fun_info_manager(*m_tmp_ctx),
@@ -506,6 +509,10 @@ public:
         m_norm_cache.insert(mk_pair(e, r));
         return r;
     }
+
+    bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs) {
+        return m_is_relation_pred(e, rop, lhs, rhs);
+    }
 };
 
 LEAN_THREAD_PTR(blastenv, g_blastenv);
@@ -551,6 +558,11 @@ projection_info const * get_projection_info(name const & n) {
     return g_blastenv->get_projection_info(n);
 }
 
+bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs) {
+    lean_assert(g_blastenv);
+    return g_blastenv->is_relation(e, rop, lhs, rhs);
+}
+
 expr whnf(expr const & e) {
     lean_assert(g_blastenv);
     return g_blastenv->whnf(e);

src/library/blast/blast.h

@@ -34,6 +34,9 @@ expr mk_fresh_local(expr const & type, binder_info const & bi = binder_info());
 bool is_reducible(name const & n);
 /** \brief Return a nonnull projection_info object if \c n is the name of a projection in env() */
 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);
 /** \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);

src/library/blast/simple_actions.cpp

@@ -55,4 +55,29 @@ optional<expr> assumption_contradiction_actions(hypothesis_idx hidx) {
     }
     return none_expr();
 }
+
+optional<expr> trivial_action() {
+    try {
+        state s = curr_state();
+        expr target = s.get_target();
+        /* ignore if target contains meta-variables */
+        if (has_expr_metavar(target))
+            return none_expr();
+
+        /* true */
+        if (target == mk_true()) {
+            return some_expr(mk_true_intro());
+        }
+
+        /* a ~ a */
+        name rop; expr lhs, rhs;
+        if (is_relation(target, rop, lhs, rhs) && is_def_eq(lhs, rhs)) {
+            return some_expr(get_app_builder().mk_refl(rop, lhs));
+        }
+
+        return none_expr();
+    } catch (app_builder_exception &) {
+        return none_expr();
+    }
+}
 }}

src/library/blast/simple_actions.h

@@ -12,4 +12,6 @@ optional<expr> assumption_action();
 /** \brief Apply assumption and contradiction actions using the given hypothesis.
     \remark This action is supposed to be applied when a hypothesis is activated. */
 optional<expr> assumption_contradiction_actions(hypothesis_idx hidx);
+/** \brief Solve trivial targets (e.g., true, a = a, a <-> a, etc). */
+optional<expr> trivial_action();
 }}

src/library/blast/simple_strategy.cpp

@@ -76,6 +76,11 @@ class simple_strategy {
             return action_result::new_branch();
         }
 
+        if (auto pr = trivial_action()) {
+            display_action("trivial");
+            return action_result::solved(*pr);
+        }
+
         if (auto pr = assumption_action()) {
             // Remark: this action is only relevant
             // when the target has been modified.

tests/lean/run/blast10.lean

@@ -0,0 +1,14 @@
+import data.list
+
+set_option blast.trace true
+
+definition lemma1 : true :=
+by blast
+
+open perm
+
+definition lemma2 (l : list nat) : l ~ l :=
+by blast
+
+print lemma1
+print lemma2