feat(library/blast): add 'discard' action for detecting irrelevant hypotheses

src/library/blast/blast.cpp

@@ -58,6 +58,7 @@ class blastenv {
     fun_info_manager           m_fun_info_manager;
     congr_lemma_manager        m_congr_lemma_manager;
     abstract_expr_manager      m_abstract_expr_manager;
+    refl_info_getter           m_refl_getter;
 
     class tctx : public type_context {
         blastenv &                              m_benv;
@@ -413,6 +414,7 @@ public:
         m_fun_info_manager(*m_tmp_ctx),
         m_congr_lemma_manager(m_app_builder, m_fun_info_manager),
         m_abstract_expr_manager(m_fun_info_manager),
+        m_refl_getter(mk_refl_info_getter(env)),
         m_tctx(*this),
         m_normalizer(m_tctx) {
         init_uref_mref_href_idxs();
@@ -538,6 +540,10 @@ public:
     bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs) {
         return m_is_relation_pred(e, rop, lhs, rhs);
     }
+
+    bool is_reflexive(name const & rop) const {
+        return static_cast<bool>(m_refl_getter(rop));
+    }
 };
 
 LEAN_THREAD_PTR(blastenv, g_blastenv);
@@ -593,6 +599,11 @@ bool is_relation(expr const & e) {
     return is_relation(e, rop, lhs, rhs);
 }
 
+bool is_reflexive(name const & rop) {
+    lean_assert(g_blastenv);
+    return g_blastenv->is_reflexive(rop);
+}
+
 expr whnf(expr const & e) {
     lean_assert(g_blastenv);
     return g_blastenv->whnf(e);

src/library/blast/blast.h

@@ -39,6 +39,7 @@ projection_info const * get_projection_info(name const & n);
     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);
+bool is_reflexive(name const & rop);
 /** \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

@@ -99,4 +99,34 @@ optional<expr> trivial_action() {
         return none_expr();
     }
 }
+
+bool discard(hypothesis_idx hidx) {
+    state s = curr_state();
+    hypothesis const * h = s.get_hypothesis_decl(hidx);
+    lean_assert(h);
+    expr type            = h->get_type();
+    // We only discard a hypothesis if it doesn't have dependencies.
+    if (s.has_target_forward_deps(hidx))
+        return false;
+    // We only discard propositions
+    if (!is_prop(type))
+        return false;
+    // 1- (H : true)
+    if (is_constant(type, get_true_name()))
+        return true;
+    // 2- (H : a ~ a)
+    name rop; expr lhs, rhs;
+    if (is_relation(type, rop, lhs, rhs) && is_def_eq(lhs, rhs) && is_reflexive(rop))
+        return true;
+    // 3- We already have an equivalent hypothesis
+    for (hypothesis_idx hidx2 : s.get_head_related(hidx)) {
+        if (hidx == hidx2)
+            continue;
+        hypothesis const * h2 = s.get_hypothesis_decl(hidx2);
+        expr type2 = h2->get_type();
+        if (is_def_eq(type, type2))
+            return true;
+    }
+    return false;
+}
 }}

src/library/blast/simple_actions.h

@@ -15,4 +15,20 @@ optional<expr> assumption_action();
 optional<expr> assumption_contradiction_actions(hypothesis_idx hidx);
 /** \brief Solve trivial targets (e.g., true, a = a, a <-> a, etc). */
 optional<expr> trivial_action();
+
+/** \brief Return true if the given hypothesis is "redundant". We consider a hypothesis
+    redundant if it is a proposition, no other hypothesis type depends on it,
+    and one of the following holds:
+    1- (H : true)
+    2- (H : a ~ a)  where ~ is a reflexive relation
+    3- There is another hypothesis H' with the same type.
+
+    Remark: 2 is not needed if the simplification rule (a ~ a) <-> true is installed.
+
+    Remark: we may want to generalize the proposition condition. Example: consider any subsingleton type.
+    We don't do it because it seems to add extra cost for very little gain
+    (well, it may be useful for the HoTT library).
+
+    TODO(Leo): subsumption. 3 is just a very simple case of subsumption. */
+bool discard(hypothesis_idx hidx);
 }}

src/library/blast/simple_strategy.cpp

@@ -44,6 +44,12 @@ class simple_strategy : public strategy {
             return r;
         }
 
+        if (discard(*hidx)) {
+            if (!preprocess) display_action("discard redudant hypothesis");
+            curr_state().del_hypothesis(*hidx);
+            return action_result::new_branch();
+        }
+
         if (optional<name> R = is_recursor_action_target(*hidx)) {
             unsigned num_minor = get_num_minor_premises(*R);
             if (num_minor == 1) {

tests/lean/run/blast17.lean

@@ -0,0 +1,2 @@
+example (p q r : Prop) (a b : nat) : true → a = a → q → q → p → p :=
+by blast