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

src/library/blast/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
   init_module.cpp simplifier.cpp simple_actions.cpp intros.cpp proof_expr.cpp
   options.cpp choice_point.cpp simple_strategy.cpp backward.cpp util.cpp
-  gexpr.cpp revert.cpp subst.cpp)
+  gexpr.cpp revert.cpp subst.cpp no_confusion.cpp)

src/library/blast/no_confusion.cpp

@@ -0,0 +1,105 @@
+/*
+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/inductive/inductive.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+struct no_confusion_proof_step_cell : public proof_step_cell {
+    name m_I_name;
+    expr m_target;
+    expr m_eq_href;
+    unsigned m_num_new_eqs;
+    no_confusion_proof_step_cell(name const & I_name, expr const & t, expr const & e, unsigned n):
+        m_I_name(I_name), m_target(t), m_eq_href(e), m_num_new_eqs(n) {}
+    virtual ~no_confusion_proof_step_cell() {}
+
+    virtual action_result resolve(expr const & pr) const {
+        try {
+            expr it   = pr;
+            bool skip = true;
+            for (unsigned i = 0; i < m_num_new_eqs; i++) {
+                if (!is_lambda(it)) {
+                    break;
+                    skip = false;
+                }
+                it = binding_body(it);
+            }
+            if (skip && closed(it)) {
+                // new eq hypotheses were not used
+                return action_result::solved(it);
+            }
+            state & s = curr_state();
+            app_builder & b = get_app_builder();
+            hypothesis const * h = s.get_hypothesis_decl(href_index(m_eq_href));
+            lean_assert(h);
+            expr type = h->get_type();
+            expr lhs, rhs;
+            lean_verify(is_eq(type, lhs, rhs));
+            name nc_name(m_I_name, "no_confusion");
+            expr new_pr = mk_app(b.mk_app(nc_name, {m_target, lhs, rhs, m_eq_href}), pr);
+            return action_result::solved(new_pr);
+        } catch (app_builder_exception &) {
+            return action_result::failed();
+        }
+    }
+};
+
+action_result no_confusion_action(hypothesis_idx hidx) {
+    try {
+        state & s       = curr_state();
+        app_builder & b = get_app_builder();
+        hypothesis const * h = s.get_hypothesis_decl(hidx);
+        lean_assert(h);
+        expr type = h->get_type();
+        expr lhs, rhs;
+        if (!is_eq(type, lhs, rhs))
+            return action_result::failed();
+        lhs = whnf(lhs);
+        rhs = whnf(rhs);
+        optional<name> c1 = is_constructor_app(env(), lhs);
+        optional<name> c2 = is_constructor_app(env(), rhs);
+        if (!c1 || !c2)
+            return action_result::failed();
+        expr A = whnf(infer_type(lhs));
+        expr I = get_app_fn(A);
+        if (!is_constant(I) || !inductive::is_inductive_decl(env(), const_name(I)))
+            return action_result::failed();
+        name nct_name(const_name(I), "no_confusion_type");
+        if (!env().find(nct_name))
+            return action_result::failed();
+        expr target  = s.get_target();
+        expr nct     = whnf(b.mk_app(nct_name, target, lhs, rhs));
+        if (c1 == c2) {
+            if (!is_pi(nct))
+                return action_result::failed();
+            if (s.has_target_forward_deps(hidx)) {
+                // TODO(Leo): we currently do not handle this case.
+                // To avoid non-termination we remove the given hypothesis, if there
+                // forward dependencies, we would also have to remove them.
+                // Remark: this is a low priority refinement since it will not happen
+                // very often in practice.
+                return action_result::failed();
+            }
+            unsigned num_params  = *inductive::get_num_params(env(), const_name(I));
+            unsigned cnstr_arity = get_arity(env().get(*c1).get_type());
+            lean_assert(cnstr_arity >= num_params);
+            unsigned num_new_eqs = cnstr_arity - num_params;
+            s.push_proof_step(new no_confusion_proof_step_cell(const_name(I), target, h->get_self(), num_new_eqs));
+            s.set_target(binding_domain(nct));
+            s.del_hypothesis(hidx);
+            return action_result::new_branch();
+        } else {
+            name nc_name(const_name(I), "no_confusion");
+            expr pr = b.mk_app(nc_name, {target, lhs, rhs, h->get_self()});
+            return action_result::solved(pr);
+        }
+    } catch (app_builder_exception &) {
+        return action_result::failed();
+    }
+}
+}}

src/library/blast/no_confusion.h

@@ -0,0 +1,14 @@
+/*
+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 {
+action_result no_confusion_action(hypothesis_idx hidx);
+}}

src/library/blast/simple_strategy.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/blast/intros.h"
 #include "library/blast/subst.h"
 #include "library/blast/backward.h"
+#include "library/blast/no_confusion.h"
 
 namespace lean {
 namespace blast {
@@ -65,6 +66,12 @@ class simple_strategy {
             }
             if (subst_action(*hidx)) {
                 display_action("subst");
+                return action_result::new_branch();
+            }
+            action_result r = no_confusion_action(*hidx);
+            if (!failed(r)) {
+                display_action("no_confusion");
+                return r;
             }
             return action_result::new_branch();
         }

src/library/blast/state.h

@@ -221,6 +221,11 @@ public:
 
     /** \brief Return the set of hypotheses that (directly) depend on the given one */
     hypothesis_idx_set get_direct_forward_deps(hypothesis_idx hidx) const;
+    bool has_forward_deps(hypothesis_idx hidx) const { return !get_direct_forward_deps(hidx).empty(); }
+    /** \brief Return true iff other hypotheses or the target type depends on hidx. */
+    bool has_target_forward_deps(hypothesis_idx hidx) const {
+        return has_forward_deps(hidx) || m_branch.m_target_deps.contains(hidx);
+    }
     /** \brief Collect in \c result the hypotheses that (directly) depend on \c hidx and satisfy \c pred. */
     template<typename P>
     void collect_direct_forward_deps(hypothesis_idx hidx, hypothesis_idx_buffer_set & result, P && pred) {

src/library/blast/subst.cpp

@@ -96,7 +96,7 @@ bool subst_action(hypothesis_idx hidx) {
     if (is_href(rhs)) {
         return subst_core(hidx);
     } else if (is_href(lhs)) {
-        if (!s.get_direct_forward_deps(href_index(lhs)).empty()) {
+        if (s.has_forward_deps(href_index(lhs))) {
             // TODO(Leo): we don't handle this case yet.
             // Other hypotheses depend on this equality.
             return false;

tests/lean/run/blast8.lean

@@ -0,0 +1,23 @@
+open nat
+set_option blast.init_depth 10
+set_option blast.max_depth 10
+
+lemma l1 (a : nat) : zero = succ a → a = a → false :=
+by blast
+
+lemma l2 (p : Prop) (a : nat) : zero = succ a → a = a → p :=
+by blast
+
+lemma l3 (a b : nat) : succ (succ a) = succ (succ b) → a = b :=
+by blast
+
+lemma l4 (a b : nat) : succ a = succ b → a = b :=
+by blast
+
+lemma l5 (a b c : nat) : succ (succ a) = succ (succ b) → c = c :=
+by blast
+
+reveal l3 l4 l5
+print l3
+print l4
+print l5

tests/lean/run/blast9.lean

@@ -0,0 +1,11 @@
+import data.list
+open list
+
+example (p : Prop) (a b c : nat) : [a, b, c] = [] → p :=
+by blast
+
+lemma l1 (a b c d e f : nat) : [a, b, c] = [d, e, f] → a = d ∧ b = e ∧ c = f :=
+by blast
+
+reveal l1
+print l1