feat(library/blast): add simple indexing data-structure for active hypotheses

src/library/app_builder.cpp

@@ -301,19 +301,17 @@ struct app_builder::imp {
         }
     }
 
-    optional<level> get_level(expr const & A) {
+    level get_level(expr const & A) {
         expr Type = m_ctx->whnf(m_ctx->infer(A));
         if (!is_sort(Type))
-            return none_level();
-        return some_level(sort_level(Type));
+            throw app_builder_exception();
+        return sort_level(Type);
     }
 
     expr mk_eq(expr const & a, expr const & b) {
         expr A    = m_ctx->infer(a);
-        auto lvl  = get_level(A);
-        if (!lvl)
-            throw app_builder_exception();
-        return ::lean::mk_app(mk_constant(get_eq_name(), {*lvl}), A, a, b);
+        level lvl = get_level(A);
+        return ::lean::mk_app(mk_constant(get_eq_name(), {lvl}), A, a, b);
     }
 
     expr mk_iff(expr const & a, expr const & b) {
@@ -322,10 +320,8 @@ struct app_builder::imp {
 
     expr mk_eq_refl(expr const & a) {
         expr A     = m_ctx->infer(a);
-        auto lvl  = get_level(A);
-        if (!lvl)
-            throw app_builder_exception();
-        return ::lean::mk_app(mk_constant(get_eq_refl_name(), {*lvl}), A, a);
+        level lvl  = get_level(A);
+        return ::lean::mk_app(mk_constant(get_eq_refl_name(), {lvl}), A, a);
     }
 
     expr mk_iff_refl(expr const & a) {
@@ -338,10 +334,8 @@ struct app_builder::imp {
         if (!is_eq(p, lhs, rhs))
             throw app_builder_exception();
         expr A    = m_ctx->infer(lhs);
-        auto lvl  = get_level(A);
-        if (!lvl)
-            throw app_builder_exception();
-        return ::lean::mk_app(mk_constant(get_eq_symm_name(), {*lvl}), A, lhs, rhs, H);
+        level lvl = get_level(A);
+        return ::lean::mk_app(mk_constant(get_eq_symm_name(), {lvl}), A, lhs, rhs, H);
     }
 
     expr mk_iff_symm(expr const & H) {
@@ -359,10 +353,8 @@ struct app_builder::imp {
         if (!is_eq(p1, lhs1, rhs1) || !is_eq(p2, lhs2, rhs2))
             throw app_builder_exception();
         expr A     = m_ctx->infer(lhs1);
-        auto lvl  = get_level(A);
-        if (!lvl)
-            throw app_builder_exception();
-        return ::lean::mk_app({mk_constant(get_eq_trans_name(), {*lvl}), A, lhs1, rhs1, rhs2, H1, H2});
+        level lvl  = get_level(A);
+        return ::lean::mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, lhs1, rhs1, rhs2, H1, H2});
     }
 
     expr mk_iff_trans(expr const & H1, expr const & H2) {
@@ -428,13 +420,13 @@ struct app_builder::imp {
         if (!is_eq(p, lhs, rhs))
             throw app_builder_exception();
         expr A      = m_ctx->infer(lhs);
-        auto A_lvl  = get_level(A);
+        level A_lvl = get_level(A);
         expr mtype  = m_ctx->whnf(m_ctx->infer(motive));
         if (!is_pi(mtype) || !is_sort(binding_body(mtype)))
             throw app_builder_exception();
         level l_1    = sort_level(binding_body(mtype));
         name const & eqrec = is_standard(m_ctx->env()) ? get_eq_rec_name() : get_eq_nrec_name();
-        return ::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2});
+        return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2});
     }
 
     expr mk_eq_drec(expr const & motive, expr const & H1, expr const & H2) {
@@ -443,18 +435,17 @@ struct app_builder::imp {
         if (!is_eq(p, lhs, rhs))
             throw app_builder_exception();
         expr A      = m_ctx->infer(lhs);
-        auto A_lvl  = get_level(A);
+        level A_lvl = get_level(A);
         expr mtype  = m_ctx->whnf(m_ctx->infer(motive));
         if (!is_pi(mtype) || !is_pi(binding_body(mtype)) || !is_sort(binding_body(binding_body(mtype))))
             throw app_builder_exception();
         level l_1    = sort_level(binding_body(binding_body(mtype)));
         name const & eqrec = is_standard(m_ctx->env()) ? get_eq_drec_name() : get_eq_rec_name();
-        return ::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2});
+        return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2});
     }
 
     expr mk_congr_arg(expr const & f, expr const & H) {
         // TODO(Leo): efficient version
-
         return mk_app(get_congr_arg_name(), {f, H});
     }
 
@@ -467,6 +458,16 @@ struct app_builder::imp {
         // TODO(Leo): efficient version
         return mk_app(get_congr_name(), {H1, H2});
     }
+
+    expr mk_false_rec(expr const & c, expr const & H) {
+        level c_lvl = get_level(c);
+        if (is_standard(m_ctx->env())) {
+            return ::lean::mk_app(mk_constant(get_false_rec_name(), {c_lvl}), c, H);
+        } else {
+            expr H_type = m_ctx->infer(H);
+            return ::lean::mk_app(mk_constant(get_empty_rec_name(), {c_lvl}), mk_lambda("e", H_type, c), H);
+        }
+    }
 };
 
 app_builder::app_builder(environment const & env, io_state const & ios, reducible_behavior b):
@@ -563,6 +564,10 @@ expr app_builder::mk_sorry(expr const & type) {
     return mk_app(get_sorry_name(), type);
 }
 
+expr app_builder::mk_false_rec(expr const & c, expr const & H) {
+    return m_ptr->mk_false_rec(c, H);
+}
+
 void app_builder::set_local_instances(list<expr> const & insts) {
     m_ptr->m_ctx->set_local_instances(insts);
 }

src/library/app_builder.h

@@ -119,6 +119,9 @@ public:
     /** \brief Create (@sorry type) */
     expr mk_sorry(expr const & type);
 
+    /** \brief False elimination */
+    expr mk_false_rec(expr const & c, expr const & H);
+
     /** \brief Set the local instances. This method is relevant when we want to expose local class instances
         to the app_builder.
 

src/library/blast/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
-  init_module.cpp simplifier.cpp assumption.cpp intros.cpp proof_expr.cpp
-  options.cpp choice_point.cpp simple_strategy.cpp backward.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)

src/library/blast/assumption.cpp

@@ -1,24 +0,0 @@
-/*
-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 "library/blast/blast.h"
-
-namespace lean {
-namespace blast {
-optional<expr> assumption_action() {
-    // TODO(Leo): this is a very naive implementation that just traverses the set of
-    // active hypothesis
-    state const & s     = curr_state();
-    expr const & target = s.get_target();
-    auto hidx = s.find_active_hypothesis([&](unsigned, hypothesis const & h) {
-            return is_def_eq(h.get_type(), target);
-        });
-    if (!hidx)
-        return none_expr();
-    hypothesis const * h = s.get_hypothesis_decl(*hidx);
-    return some_expr(h->get_self());
-}
-}}

src/library/blast/hypothesis.h

@@ -15,6 +15,7 @@ class hypothesis;
 class branch;
 class state;
 
+typedef unsigned                        hypothesis_idx;
 typedef rb_tree<unsigned, unsigned_cmp> hypothesis_idx_set;
 typedef list<unsigned>                  hypothesis_idx_list;
 typedef buffer<unsigned>                hypothesis_idx_buffer;

src/library/blast/simple_actions.cpp

@@ -0,0 +1,58 @@
+/*
+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 "library/constants.h"
+#include "library/blast/util.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+// TODO(Leo): we should create choice points when there are meta-variables
+optional<expr> assumption_action() {
+    state const & s     = curr_state();
+    expr const & target = s.get_target();
+    for (hypothesis_idx hidx : s.get_head_related()) {
+        hypothesis const * h = s.get_hypothesis_decl(hidx);
+        lean_assert(h);
+        if (is_def_eq(h->get_type(), target))
+            return some_expr(h->get_self());
+    }
+    return none_expr();
+}
+
+optional<expr> assumption_contradiction_actions(hypothesis_idx hidx) {
+    state const & s      = curr_state();
+    app_builder & b      = get_app_builder();
+    hypothesis const * h = s.get_hypothesis_decl(hidx);
+    lean_assert(h);
+    expr const & type    = h->get_type();
+    if (blast::is_false(type)) {
+        return some_expr(b.mk_false_rec(s.get_target(), h->get_self()));
+    }
+    if (is_def_eq(type, s.get_target())) {
+        return some_expr(h->get_self());
+    }
+    expr p1 = type;
+    bool is_neg1 = is_not(type, p1);
+    for (hypothesis_idx hidx2 : s.get_head_related(hidx)) {
+        hypothesis const * h2 = s.get_hypothesis_decl(hidx2);
+        expr type2 = h2->get_type();
+        expr p2    = type2;
+        bool is_neg2 = is_not(type2, p2);
+        if (is_neg1 != is_neg2) {
+            if (is_def_eq(p1, p2)) {
+                if (is_neg1) {
+                    return some_expr(b.mk_app(get_absurd_name(), {s.get_target(), h2->get_self(), h->get_self()}));
+                } else {
+                    lean_assert(is_neg2);
+                    return some_expr(b.mk_app(get_absurd_name(), {s.get_target(), h->get_self(), h2->get_self()}));
+                }
+            }
+        }
+    }
+    return none_expr();
+}
+}}

src/library/blast/simple_actions.h

@@ -0,0 +1,15 @@
+/*
+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 "kernel/expr.h"
+namespace lean {
+namespace blast {
+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);
+}}

src/library/blast/simple_strategy.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "library/blast/blast.h"
 #include "library/blast/options.h"
 #include "library/blast/choice_point.h"
-#include "library/blast/assumption.h"
+#include "library/blast/simple_actions.h"
 #include "library/blast/intros.h"
 #include "library/blast/backward.h"
 
@@ -22,7 +22,7 @@ class simple_strategy {
 
     enum status { NoAction, ClosedBranch, Continue };
 
-    optional<unsigned> activate_hypothesis() {
+    optional<hypothesis_idx> activate_hypothesis() {
         return curr_state().activate_hypothesis();
     }
 
@@ -30,12 +30,15 @@ class simple_strategy {
         if (intros_action())
             return action_result::new_branch();
 
-        if (activate_hypothesis()) {
-            // TODO(Leo): we should probably eagerly simplify the activated hypothesis.
+        if (auto hidx = activate_hypothesis()) {
+            if (auto pr = assumption_contradiction_actions(*hidx))
+                return action_result::solved(*pr);
             return action_result::new_branch();
         }
 
         if (auto pr = assumption_action()) {
+            // Remark: this action is only relevant
+            // when the target has been modified.
             return action_result::solved(*pr);
         }
 

src/library/blast/state.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
 #include "library/replace_visitor.h"
+#include "library/blast/util.h"
 #include "library/blast/state.h"
 
 namespace lean {
@@ -433,9 +434,50 @@ expr state::mk_hypothesis(expr const & type) {
     return mk_hypothesis(hidx, name(*g_prefix, hidx), type, none_expr());
 }
 
-void state::update_indices(unsigned /* hidx */) {
-    // TODO(Leo): we need to update the indexing data-structures and send
-    // the hypothesis if to the congruence closure module after it is implemented.
+static optional<head_index> to_head_index(expr type) {
+    is_not(type, type);
+    expr const & f = get_app_fn(type);
+    if (is_constant(f) || is_local(f))
+        return optional<head_index>(head_index(f));
+    else
+        return optional<head_index>();
+}
+
+static optional<head_index> to_head_index(hypothesis const & h) {
+    return to_head_index(h.get_type());
+}
+
+list<hypothesis_idx> state::get_occurrences_of(head_index const & h) const {
+    if (auto r = m_branch.m_head_to_hyps.find(h))
+        return *r;
+    else
+        return list<hypothesis_idx>();
+}
+
+list<hypothesis_idx> state::get_head_related(hypothesis_idx hidx) const {
+    hypothesis const * h = get_hypothesis_decl(hidx);
+    lean_assert(h);
+    /* update m_head_to_hyps */
+    if (auto i = to_head_index(*h))
+        return get_occurrences_of(*i);
+    else
+        return list<hypothesis_idx>();
+}
+
+list<hypothesis_idx> state::get_head_related() const {
+    if (auto i = to_head_index(m_branch.m_target))
+        return get_occurrences_of(*i);
+    else
+        return list<hypothesis_idx>();
+}
+
+void state::update_indices(hypothesis_idx hidx) {
+    hypothesis const * h = get_hypothesis_decl(hidx);
+    lean_assert(h);
+    /* update m_head_to_hyps */
+    if (auto i = to_head_index(*h))
+        m_branch.m_head_to_hyps.insert(*i, hidx);
+    /* TODO(Leo): update congruence closure indices */
 }
 
 optional<unsigned> state::activate_hypothesis() {

src/library/blast/state.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/rb_map.h"
 #include "kernel/expr.h"
+#include "library/head_map.h"
 #include "library/tactic/goal.h"
 #include "library/blast/action_result.h"
 #include "library/blast/hypothesis.h"
@@ -90,7 +91,7 @@ public:
 class branch {
     friend class state;
     typedef hypothesis_idx_map<hypothesis_idx_set> forward_deps;
-    typedef rb_map<double, unsigned, double_cmp>   todo_queue;
+    typedef rb_map<double, hypothesis_idx, double_cmp>   todo_queue;
     // Hypothesis/facts in the current state
     hypothesis_decls   m_hyp_decls;
     // We break the set of hypotheses in m_context in 3 sets that are not necessarily disjoint:
@@ -110,6 +111,7 @@ class branch {
     hypothesis_idx_set       m_assumption;
     hypothesis_idx_set       m_active;
     todo_queue               m_todo_queue;
+    head_map<hypothesis_idx> m_head_to_hyps;
     forward_deps             m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h.
     expr                     m_target;
     hypothesis_idx_set       m_target_deps;
@@ -128,20 +130,20 @@ class state {
     proof_steps        m_proof_steps;
     branch             m_branch;
 
-    void add_forward_dep(unsigned hidx_user, unsigned hidx_provider);
-    void add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user);
-    void add_deps(hypothesis & h_user, unsigned hidx_user);
+    void add_forward_dep(hypothesis_idx hidx_user, hypothesis_idx hidx_provider);
+    void add_deps(expr const & e, hypothesis & h_user, hypothesis_idx hidx_user);
+    void add_deps(hypothesis & h_user, hypothesis_idx hidx_user);
 
     /** \brief Compute the weight of a hypothesis with the given type
         We use this weight to update the todo_queue. */
-    double compute_weight(unsigned hidx, expr const & type);
+    double compute_weight(hypothesis_idx hidx, expr const & type);
 
     /** \brief This method is invoked when a hypothesis move from todo to active.
 
         We will update indices and data-structures (e.g., congruence closure). */
-    void update_indices(unsigned hidx);
+    void update_indices(hypothesis_idx hidx);
 
-    expr mk_hypothesis(unsigned new_hidx, name const & n, expr const & type, optional<expr> const & value);
+    expr mk_hypothesis(hypothesis_idx new_hidx, name const & n, expr const & type, optional<expr> const & value);
 
     unsigned add_metavar_decl(metavar_decl const & decl);
     goal to_goal(branch const &) const;
@@ -149,8 +151,8 @@ class state {
     expr mk_binding(bool is_lambda, unsigned num, expr const * hrefs, expr const & b) const;
 
     #ifdef LEAN_DEBUG
-    bool check_hypothesis(expr const & e, unsigned hidx, hypothesis const & h) const;
-    bool check_hypothesis(unsigned hidx, hypothesis const & h) const;
+    bool check_hypothesis(expr const & e, hypothesis_idx hidx, hypothesis const & h) const;
+    bool check_hypothesis(hypothesis_idx hidx, hypothesis const & h) const;
     bool check_target() const;
     #endif
 public:
@@ -168,7 +170,7 @@ public:
         The context of this metavariable will be all assumption hypotheses occurring
         in the current branch. */
     expr mk_metavar(expr const & type);
-    metavar_decl const * get_metavar_decl(unsigned idx) const { return m_metavar_decls.find(idx); }
+    metavar_decl const * get_metavar_decl(hypothesis_idx idx) const { return m_metavar_decls.find(idx); }
     metavar_decl const * get_metavar_decl(expr const & e) const { return get_metavar_decl(mref_index(e)); }
 
     /************************
@@ -188,20 +190,20 @@ public:
 
     /** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index
         \c hidx_provider. */
-    bool hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const;
+    bool hidx_depends_on(hypothesis_idx hidx_user, hypothesis_idx hidx_provider) const;
 
-    hypothesis const * get_hypothesis_decl(unsigned hidx) const { return m_branch.m_hyp_decls.find(hidx); }
+    hypothesis const * get_hypothesis_decl(hypothesis_idx hidx) const { return m_branch.m_hyp_decls.find(hidx); }
     hypothesis const * get_hypothesis_decl(expr const & h) const { return get_hypothesis_decl(href_index(h)); }
 
-    void for_each_hypothesis(std::function<void(unsigned, hypothesis const &)> const & fn) const { m_branch.m_hyp_decls.for_each(fn); }
-    optional<unsigned> find_active_hypothesis(std::function<bool(unsigned, hypothesis const &)> const & fn) const { // NOLINT
-        return m_branch.m_active.find_if([&](unsigned hidx) {
+    void for_each_hypothesis(std::function<void(hypothesis_idx, hypothesis const &)> const & fn) const { m_branch.m_hyp_decls.for_each(fn); }
+    optional<unsigned> find_active_hypothesis(std::function<bool(hypothesis_idx, hypothesis const &)> const & fn) const { // NOLINT
+        return m_branch.m_active.find_if([&](hypothesis_idx hidx) {
                 return fn(hidx, *get_hypothesis_decl(hidx));
             });
     }
 
     /** \brief Activate the next hypothesis in the TODO queue, return none if the TODO queue is empty. */
-    optional<unsigned> activate_hypothesis();
+    optional<hypothesis_idx> activate_hypothesis();
 
     /** \brief Store in \c r the hypotheses in this branch sorted by dependency depth */
     void get_sorted_hypotheses(hypothesis_idx_buffer & r) const;
@@ -210,6 +212,15 @@ public:
 
     hypothesis_idx_set get_assumptions() const { return m_branch.m_assumption; }
 
+    /** \brief Return (active) hypotheses whose head symbol is h or (not h) */
+    list<hypothesis_idx> get_occurrences_of(head_index const & h) const;
+
+    /** \brief Return (active) hypotheses whose head symbol is equal to the of hidx or it is the negation of */
+    list<hypothesis_idx> get_head_related(hypothesis_idx hidx) const;
+
+    /** \brief Return (active) hypotheses whose head symbol is equal to target or it is the negation of */
+    list<hypothesis_idx> get_head_related() const;
+
     /************************
        Abstracting hypotheses
     *************************/

src/library/blast/util.cpp

@@ -0,0 +1,18 @@
+/*
+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 "library/util.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+bool is_not(expr const & e, expr & a) {
+    return ::lean::is_not(env(), e, a);
+}
+bool is_false(expr const & e) {
+    return ::lean::is_false(env(), e);
+}
+}}

src/library/blast/util.h

@@ -8,5 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 namespace lean {
 namespace blast {
-optional<expr> assumption_action();
+/** \brief Return true iff \c e is of the form (not a) or (a -> false), and false otherwise */
+bool is_not(expr const & e, expr & a);
+bool is_false(expr const & e);
 }}

tests/lean/run/blast4.lean

@@ -0,0 +1,17 @@
+lemma T1 (a b : Prop) : false → a :=
+by blast
+
+reveal T1
+print T1
+
+lemma T2 (a b c : Prop) : ¬ a → b → a → c :=
+by blast
+
+reveal T2
+print T2
+
+example (a b c : Prop) : a → b → ¬ a → c :=
+by blast
+
+example (a b c : Prop) : a → b → b → ¬ a → c :=
+by blast