refactor(library/blast/unit): simplify module

library/init/logic.lean

@@ -27,6 +27,8 @@ false.rec b (H2 H1)
 theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
 assume Ha : a, absurd (H1 Ha) H2
 
+definition implies.resolve {a b : Prop} (H : a → b) (nb : ¬ b) : ¬ a := assume Ha, nb (H Ha)
+
 /- not -/
 
 theorem not_false : ¬false :=
@@ -37,6 +39,8 @@ definition non_contradictory (a : Prop) : Prop := ¬¬a
 theorem non_contradictory_intro {a : Prop} (Ha : a) : ¬¬a :=
 assume Hna : ¬a, absurd Ha Hna
 
+definition not.wrap {a : Prop} (na : a → false) : ¬ a := na
+
 /- false -/
 
 theorem false.elim {c : Prop} (H : false) : c :=
@@ -459,6 +463,20 @@ iff.trans or.comm !or_false
 theorem or_self [simp] (a : Prop) : a ∨ a ↔ a :=
 iff.intro (or.rec id id) or.inl
 
+/- or resolution rulse -/
+
+definition or.resolve_left {a b : Prop} (H : a ∨ b) (na : ¬ a) : b :=
+  or.elim H (λ Ha, absurd Ha na) id
+
+definition or.neg_resolve_left {a b : Prop} (H : ¬ a ∨ b) (Ha : a) : b :=
+  or.elim H (λ na, absurd Ha na) id
+
+definition or.resolve_right {a b : Prop} (H : a ∨ b) (nb : ¬ b) : a :=
+  or.elim H id (λ Hb, absurd Hb nb)
+
+definition or.neg_resolve_right {a b : Prop} (H : a ∨ ¬ b) (Hb : b) : a :=
+  or.elim H id (λ nb, absurd Hb nb)
+
 /- iff simp rules -/
 
 theorem iff_true [simp] (a : Prop) : (a ↔ true) ↔ a :=

src/library/blast/unit/unit_action.cpp

@@ -21,123 +21,88 @@ Author: Daniel Selsam
 namespace lean {
 namespace blast {
 
+bool is_lemma(expr const & _type) {
+    expr type = _type;
+    bool has_antecedent = false;
+    if (!is_prop(type)) return false;
+    while (is_pi(type) && closed(binding_body(type))) {
+        has_antecedent = true;
+        type = binding_body(type);
+    }
+    if (has_antecedent && !is_pi(type)) return true;
+    else if (is_or(type)) return true;
+    else return false;
+}
+
+bool is_fact(expr const & type) {
+    return is_prop(type) && !is_pi(type) && !is_or(type);
+}
+
+expr flip(expr const & e) {
+    expr not_e;
+    if (!blast::is_not(e, not_e)) not_e = get_app_builder().mk_not(e);
+    return not_e;
+}
+
+bool is_not(expr const & e) {
+    expr not_e;
+    return blast::is_not(e, not_e);
+}
+
 static unsigned g_ext_id = 0;
 struct unit_branch_extension : public branch_extension {
-    rb_multi_map<expr, hypothesis_idx, expr_quick_cmp> m_lemma_map;
+    /* We map each lemma to the two facts that it is watching. */
-    rb_map<expr, hypothesis_idx, expr_quick_cmp> m_fact_map;
+    rb_multi_map<hypothesis_idx, expr, unsigned_cmp> m_lemmas_to_facts;
+
+    /* We map each fact back to the lemma hypotheses that are watching it. */
+    rb_multi_map<expr, hypothesis_idx, expr_quick_cmp> m_facts_to_lemmas;
+
+    /* We map each fact expression to its hypothesis. */
+    rb_map<expr, hypothesis_idx, expr_quick_cmp>       m_facts;
 
     unit_branch_extension() {}
     unit_branch_extension(unit_branch_extension const & b):
-        m_lemma_map(b.m_lemma_map), m_fact_map(b.m_fact_map) {}
+        m_lemmas_to_facts(b.m_lemmas_to_facts),
+        m_facts_to_lemmas(b.m_facts_to_lemmas),
+        m_facts(b.m_facts) {}
     virtual ~unit_branch_extension() {}
     virtual branch_extension * clone() override { return new unit_branch_extension(*this); }
-
-    void insert(expr const & e, hypothesis_idx hidx, bool neg) {
-        expr A, B;
-        if (is_or(e, A, B)) {
-            lean_assert(!neg);
-            insert(A, hidx, neg);
-            insert(B, hidx, neg);
-        } else if (is_and(e, A, B)) {
-            lean_assert(neg);
-            insert(A, hidx, neg);
-            insert(B, hidx, neg);
-        } else if (neg) {
-            expr not_e;
-            if (blast::is_not(e, not_e)) m_lemma_map.insert(not_e, hidx);
-            else m_lemma_map.insert(get_app_builder().mk_not(e), hidx);
-        } else {
-            m_lemma_map.insert(e, hidx);
-        }
-    }
-
     virtual void hypothesis_activated(hypothesis const & h, hypothesis_idx hidx) override {
-        expr type = whnf(h.get_type());
+        if (is_fact(h.get_type())) m_facts.insert(h.get_type(), hidx);
-        if (!is_pi(type)) {
-            if (is_prop(type)) m_fact_map.insert(type, hidx);
-            return;
-        }
-        bool has_antecedent = false;
-        while (is_pi(type) && is_prop(binding_domain(type)) && closed(binding_body(type))) {
-            has_antecedent = true;
-            insert(binding_domain(type), hidx, false);
-            type = binding_body(type);
-        }
-        if (has_antecedent && is_prop(type)) {
-            insert(type, hidx, true);
-        }
     }
-
+    virtual void hypothesis_deleted(hypothesis const & h, hypothesis_idx hidx) override {
-    virtual void hypothesis_deleted(hypothesis const & , hypothesis_idx ) override {
+        if (is_lemma(h.get_type())) {
-        /* We discard opportunistically when we encounter a hypothesis that is dead. */
+            list<expr> const * facts = find_facts_watching_lemma(hidx);
+            if (facts) {
+                for_each(*facts, [&](expr const & fact) {
+                        unwatch(hidx, fact);
+                    });
+            }
+        } else if (is_fact(h.get_type())) {
+            m_facts.erase(h.get_type());
+            lean_assert(!find_lemmas_watching_fact(h.get_type()));
+        }
     }
 
 public:
-    list<hypothesis_idx> const * find_lemmas(expr const & e) { return m_lemma_map.find(e); }
+    list<hypothesis_idx> const * find_lemmas_watching_fact(expr const & fact_type) {
-    template<typename P> void filter_lemmas(expr const & e, P && p) { return m_lemma_map.filter(e, p); }
+        return m_facts_to_lemmas.find(fact_type);
-    hypothesis_idx const * find_fact(expr const & e) { return m_fact_map.find(e); }
-    void erase_fact(expr const & e) { return m_fact_map.erase(e); }
-
-    /* Returns a proof of the disjunction [e] */
-    optional<expr> find_live_fact_in_disjunction(expr const & e) {
-        expr A, B;
-        if (is_or(e, A, B)) {
-            if (auto A_fact = find_live_fact_in_disjunction(A)) {
-                return some_expr(get_app_builder().mk_app(get_or_intro_left_name(), {A, B, *A_fact}));
-            } else if (auto B_fact = find_live_fact_in_disjunction(B)) {
-                return some_expr(get_app_builder().mk_app(get_or_intro_right_name(), {A, B, *B_fact}));
-            } else {
-                return none_expr();
-            }
-        } else {
-            hypothesis_idx const * fact_hidx = find_fact(e);
-            if (fact_hidx) {
-                hypothesis const & fact_h = curr_state().get_hypothesis_decl(*fact_hidx);
-                if (fact_h.is_dead()) {
-                    erase_fact(e);
-                    return none_expr();
-                } else {
-                    return some_expr(fact_h.get_self());
-                }
-            } else {
-                return none_expr();
-            }
-        }
     }
-
+    list<expr> const * find_facts_watching_lemma(hypothesis_idx lemma_hidx) {
-    /* Returns a proof of [false], by either applying a projection of [proof] to a hypothesis or vice versa. */
+        return m_lemmas_to_facts.find(lemma_hidx);
-    optional<expr> find_live_disproof_of_conjunction(expr const & e, expr const & proof) {
+    }
-        expr A, B;
+    void unwatch(hypothesis_idx lemma_hidx, expr const & fact_type) {
-        if (is_and(e, A, B)) {
+        m_lemmas_to_facts.filter(lemma_hidx, [&](expr const & fact_type2) {
-            if (auto A_false = find_live_disproof_of_conjunction(A, get_app_builder().mk_app(get_and_elim_left_name(), {A, B, proof}))) {
+                return fact_type != fact_type2;
-                return some_expr(*A_false);
+            });
-            } else if (auto B_false = find_live_disproof_of_conjunction(B, get_app_builder().mk_app(get_and_elim_right_name(), {A, B, proof}))) {
+        m_facts_to_lemmas.erase(fact_type, lemma_hidx);
-                return some_expr(*B_false);
+    }
-            } else {
+    hypothesis_idx const * find_fact(expr const & fact_type) {
-                return none_expr();
+        return m_facts.find(fact_type);
-            }
+    }
-        } else {
+    void watch(hypothesis_idx lemma_hidx, expr const & fact_type) {
-            expr not_e;
+        m_lemmas_to_facts.insert(lemma_hidx, fact_type);
-            bool not_e_is_not = false;
+        m_facts_to_lemmas.insert(fact_type, lemma_hidx);
-            if (!blast::is_not(e, not_e)) {
-                not_e_is_not = true;
-                not_e = get_app_builder().mk_not(e);
-            }
-
-            hypothesis_idx const * fact_hidx = find_fact(not_e);
-            if (fact_hidx) {
-                hypothesis const & fact_h = curr_state().get_hypothesis_decl(*fact_hidx);
-                if (fact_h.is_dead()) {
-                    erase_fact(e);
-                    return none_expr();
-                } else {
-                    if (not_e_is_not) return some_expr(mk_app(fact_h.get_self(), proof));
-                    else return some_expr(mk_app(proof, fact_h.get_self()));
-                }
-            } else {
-                return none_expr();
-            }
-        }
     }
 };
 
@@ -151,72 +116,178 @@ static unit_branch_extension & get_extension() {
     return static_cast<unit_branch_extension&>(curr_state().get_extension(g_ext_id));
 }
 
-action_result unit_pi(expr const & _type, expr const & proof) {
+/* Recall the general form of the lemmas we handle in this module:
-    unit_branch_extension & ext = get_extension();
+   A_1 -> ... -> A_n -> B_1 \/ (B2 \/ ... \/ B_m)...)
-    bool missing_argument = false;
-    bool has_antecedent = false;
-    expr type = _type;
-    expr new_hypothesis = proof;
-    expr local;
 
-    while (is_pi(type) && is_prop(binding_domain(type)) && closed(binding_body(type))) {
+   There are three different scenarios in which we propagate:
-        has_antecedent = true;
+   (1) We have all of the A_i, and the negations of all but the last B_j.
-        optional<expr> fact = ext.find_live_fact_in_disjunction(binding_domain(type));
+   (2) We are missing an A_i.
-        if (fact) {
+   (3) We are missing a B_j.
-            new_hypothesis = mk_app(new_hypothesis, *fact);
+
-        } else {
+   The first thing we do is check whether or not we are able to propagate.
-            if (missing_argument) return action_result::failed();
+   If so, we start instantiating the A_i. If we hit a missing literal,
-            local = mk_fresh_local(binding_domain(type));
+   we store the proof so far, create a local for the consequent, prove false,
-            new_hypothesis = mk_app(new_hypothesis, local);
+   and then conclude with [lemma imp_right : (A → B) → ¬ B → ¬ A].
-            missing_argument = true;
+
+   If we instantiate all the A_i, we start using [lemma or_resolve_left : A ∨ B → ¬ A → B]
+   to cross of the B_j. If we have all but the last one, we simply return the resulting proof.
+
+   If we are missing a B_j, we store the proof so far, create a local for the right-hand-side of
+   the disjunct, prove false, and then conclude with [lemma or_resolve_right : A ∨ B → ¬ B → A].
+*/
+
+
+bool can_propagate(expr const & _type, buffer<expr, 2> & to_watch) {
+    lean_assert(is_lemma(_type));
+    expr type = _type;
+    unsigned num_watching = 0;
+    unit_branch_extension & ext = get_extension();
+
+    /* Traverse the A_i */
+    while (is_pi(type) && closed(binding_body(type))) {
+        expr arg;
+        hypothesis_idx const * fact_hidx = ext.find_fact(binding_domain(type));
+        if (!fact_hidx) {
+            to_watch.push_back(binding_domain(type));
+            num_watching++;
+            if (num_watching == 2) return false;
         }
         type = binding_body(type);
     }
 
-    if (!has_antecedent) {
+    /* Traverse the B_j */
-        return action_result::failed();
+    expr lhs, rhs;
-    } else if (!missing_argument) {
+    while (is_or(type, lhs, rhs)) {
-        curr_state().mk_hypothesis(type, new_hypothesis);
+        hypothesis_idx const * fact_hidx = ext.find_fact(flip(lhs));
-        return action_result::new_branch();
+        if (!fact_hidx) {
-    } else if (is_prop(type)) {
+            to_watch.push_back(flip(lhs));
-        optional<expr> disproof = ext.find_live_disproof_of_conjunction(type, new_hypothesis);
+            num_watching++;
-        if (disproof) {
+            if (num_watching == 2) return false;
-            curr_state().mk_hypothesis(get_app_builder().mk_not(infer_type(local)),
-                                       Fun(local, *disproof));
-            return action_result::new_branch();
-        } else {
-            return action_result::failed();
         }
-    } else {
+        type = rhs;
+    }
+
+    hypothesis_idx const * fact_hidx = ext.find_fact(flip(type));
+    if (!fact_hidx) {
+        to_watch.push_back(flip(type));
+        num_watching++;
+        if (num_watching == 2) return false;
+    }
+    return true;
+}
+
+action_result unit_lemma(hypothesis_idx hidx, expr const & _type, expr const & _proof) {
+    lean_assert(is_lemma(_type));
+    unit_branch_extension & ext = get_extension();
+
+    /* (1) Find the facts that are watching this lemma and clear them. */
+    list<expr> const * watching = ext.find_facts_watching_lemma(hidx);
+    if (watching) {
+        lean_assert(length(*watching) == 2);
+        // TODO(dhs): is it safe to remove from these lists while I am iterating them with [for_each]?
+        for_each(*watching, [&](expr const & fact) { ext.unwatch(hidx, fact); });
+    }
+
+    /* (2) Check if we can propagate */
+    buffer<expr, 2> to_watch;
+    if (!can_propagate(_type, to_watch)) {
+        for (expr const & e : to_watch) ext.watch(hidx, e);
         return action_result::failed();
     }
-    lean_unreachable();
+
+    expr type = _type;
+    expr proof = _proof;
+    expr final_type;
+    expr proof_left;
+    expr proof_init_right;
+    expr type_init_right;
+    bool missing_A = false;
+    bool missing_B = false;
+
+    /* (3) Traverse the binding domains */
+    while (is_pi(type) && closed(binding_body(type))) {
+        hypothesis_idx const * fact_hidx = ext.find_fact(binding_domain(type));
+        if (fact_hidx) {
+            proof = mk_app(proof, curr_state().get_hypothesis_decl(*fact_hidx).get_self());
+        } else {
+            lean_assert(!missing_A);
+            missing_A = true;
+            final_type = get_app_builder().mk_not(binding_domain(type));
+            proof_left = proof;
+            type_init_right = binding_body(type);
+            proof_init_right = mk_fresh_local(type_init_right);
+            proof = proof_init_right;
+        }
+        type = binding_body(type);
+    }
+
+    /* (4) Traverse the conclusion */
+    expr lhs, rhs;
+    while (is_or(type, lhs, rhs)) {
+        hypothesis_idx const * fact_hidx = ext.find_fact(flip(lhs));
+        if (fact_hidx) {
+            expr arg = curr_state().get_hypothesis_decl(*fact_hidx).get_self();
+            if (is_not(lhs)) {
+                proof = get_app_builder().mk_app(get_or_neg_resolve_left_name(),
+                                                 proof, arg);
+            } else {
+                proof = get_app_builder().mk_app(get_or_resolve_left_name(),
+                                                 proof, arg);
+            }
+        } else {
+            lean_assert(!missing_A);
+            lean_assert(!missing_B);
+            missing_B = true;
+            final_type = lhs;
+            proof_left = proof;
+            type_init_right = rhs;
+            proof_init_right = mk_fresh_local(type_init_right);
+            proof = proof_init_right;
+        }
+        type = rhs;
+    }
+
+    expr final_proof;
+    if (missing_A || missing_B) {
+        hypothesis_idx const * fact_hidx = ext.find_fact(flip(type));
+        lean_assert(fact_hidx);
+        expr arg = curr_state().get_hypothesis_decl(*fact_hidx).get_self();
+        if (is_not(type)) proof = mk_app(proof, arg);
+        else proof = mk_app(arg, proof);
+        expr proof_right = get_app_builder().mk_app(get_not_wrap_name(), type_init_right, Fun(proof_init_right, proof));
+        if (missing_A) {
+            final_proof = get_app_builder().mk_app(get_implies_resolve_name(), proof_left, proof_right);
+        } else {
+            final_proof = get_app_builder().mk_app(get_or_resolve_right_name(), proof_left, proof_right);
+        }
+    } else {
+        final_type = type;
+        final_proof = proof;
+    }
+
+    curr_state().mk_hypothesis(final_type, final_proof);
+    return action_result::new_branch();
 }
 
 action_result unit_fact(expr const & type) {
     unit_branch_extension & ext = get_extension();
-    list<hypothesis_idx> const * lemmas = ext.find_lemmas(type);
+    list<hypothesis_idx> const * lemmas = ext.find_lemmas_watching_fact(type);
     if (!lemmas) return action_result::failed();
     bool success = false;
-    ext.filter_lemmas(type, [&](hypothesis_idx const & hidx) {
+    for_each(*lemmas, [&](hypothesis_idx const & hidx) {
             hypothesis const & h = curr_state().get_hypothesis_decl(hidx);
-            if (h.is_dead()) {
+            action_result r = unit_lemma(hidx, whnf(h.get_type()), h.get_self());
-                return false;
+            success = success || (r.get_kind() == action_result::NewBranch);
-            } else {
-                action_result r = unit_pi(whnf(h.get_type()), h.get_self());
-                success = success || (r.get_kind() == action_result::NewBranch);
-                return true;
-            }
         });
     if (success) return action_result::new_branch();
     else return action_result::failed();
 }
 
-action_result unit_action(unsigned _hidx) {
+action_result unit_action(unsigned hidx) {
-    hypothesis const & h = curr_state().get_hypothesis_decl(_hidx);
+    hypothesis const & h = curr_state().get_hypothesis_decl(hidx);
     expr type = whnf(h.get_type());
-    if (is_pi(type)) return unit_pi(type, h.get_self());
+    if (is_lemma(type)) return unit_lemma(hidx, type, h.get_self());
-    else if (is_prop(type)) return unit_fact(type);
+    else if (is_fact(type)) return unit_fact(type);
     else return action_result::failed();
 }
 }}

src/library/blast/unit/unit_action.h

@@ -8,18 +8,15 @@ Author: Daniel Selsam
 
 namespace lean {
 namespace blast {
-/* \brief Propagates lemmas of the form
+/* \brief The unit module handles lemmas of the form
-   <tt>(A11 \/ ... \/ ...) -> ... -> (Am1 \/ ... \/ ...) -> (B1 /\ ... /\ ...)</tt>
+   <tt>A_1 -> ... -> A_n -> B_1 \/ (B2 \/ ... \/ B_m)...)</tt>
-   where each <tt>A</tt> and <tt>B</tt> can be any propositions, and can optionally
-   be negated.
 
-   If we can find one disjunct for every antecedent, we instantiate the lemma
+   Whenever all but one of the literals is present as a hypothesis with
-   fully. On the other hand, if we can find one disjunct for all but one
+   the appropriate polarity, we instantiate and resolve and necessary
-   antecedents, and one fact that disproves the conjunctive conclusion,
+   to conclude a new literal.
-   we conclude the negation of the missing disjunctive argument.
 
-   Remark: conjunctions in the antecedents and disjunctions in the conclusion are
+   Remark: we assume that a pre-processing step will put lemmas
-   both treated as monolithic propositions, so some pre-processing may be necessary.
+   into the above form when possible.
 */
 action_result unit_action(unsigned hidx);
 

src/library/constants.cpp

@@ -66,6 +66,7 @@ name const * g_iff_elim_left = nullptr;
 name const * g_iff_elim_right = nullptr;
 name const * g_iff_false_intro = nullptr;
 name const * g_iff_true_intro = nullptr;
+name const * g_implies_resolve = nullptr;
 name const * g_implies = nullptr;
 name const * g_implies_of_if_pos = nullptr;
 name const * g_implies_of_if_neg = nullptr;
@@ -81,6 +82,7 @@ name const * g_nat_succ = nullptr;
 name const * g_nat_zero = nullptr;
 name const * g_neg = nullptr;
 name const * g_not = nullptr;
+name const * g_not_wrap = nullptr;
 name const * g_not_of_iff_false = nullptr;
 name const * g_num = nullptr;
 name const * g_num_zero = nullptr;
@@ -94,6 +96,11 @@ name const * g_or = nullptr;
 name const * g_or_elim = nullptr;
 name const * g_or_intro_left = nullptr;
 name const * g_or_intro_right = nullptr;
+name const * g_or_rec = nullptr;
+name const * g_or_resolve_left = nullptr;
+name const * g_or_resolve_right = nullptr;
+name const * g_or_neg_resolve_left = nullptr;
+name const * g_or_neg_resolve_right = nullptr;
 name const * g_poly_unit = nullptr;
 name const * g_poly_unit_star = nullptr;
 name const * g_pos_num = nullptr;
@@ -245,6 +252,7 @@ void initialize_constants() {
     g_iff_elim_right = new name{"iff", "elim_right"};
     g_iff_false_intro = new name{"iff_false_intro"};
     g_iff_true_intro = new name{"iff_true_intro"};
+    g_implies_resolve = new name{"implies", "resolve"};
     g_implies = new name{"implies"};
     g_implies_of_if_pos = new name{"implies_of_if_pos"};
     g_implies_of_if_neg = new name{"implies_of_if_neg"};
@@ -260,6 +268,7 @@ void initialize_constants() {
     g_nat_zero = new name{"nat", "zero"};
     g_neg = new name{"neg"};
     g_not = new name{"not"};
+    g_not_wrap = new name{"not", "wrap"};
     g_not_of_iff_false = new name{"not_of_iff_false"};
     g_num = new name{"num"};
     g_num_zero = new name{"num", "zero"};
@@ -273,6 +282,11 @@ void initialize_constants() {
     g_or_elim = new name{"or", "elim"};
     g_or_intro_left = new name{"or", "intro_left"};
     g_or_intro_right = new name{"or", "intro_right"};
+    g_or_rec = new name{"or", "rec"};
+    g_or_resolve_left = new name{"or", "resolve_left"};
+    g_or_resolve_right = new name{"or", "resolve_right"};
+    g_or_neg_resolve_left = new name{"or", "neg_resolve_left"};
+    g_or_neg_resolve_right = new name{"or", "neg_resolve_right"};
     g_poly_unit = new name{"poly_unit"};
     g_poly_unit_star = new name{"poly_unit", "star"};
     g_pos_num = new name{"pos_num"};
@@ -425,6 +439,7 @@ void finalize_constants() {
     delete g_iff_elim_right;
     delete g_iff_false_intro;
     delete g_iff_true_intro;
+    delete g_implies_resolve;
     delete g_implies;
     delete g_implies_of_if_pos;
     delete g_implies_of_if_neg;
@@ -440,6 +455,7 @@ void finalize_constants() {
     delete g_nat_zero;
     delete g_neg;
     delete g_not;
+    delete g_not_wrap;
     delete g_not_of_iff_false;
     delete g_num;
     delete g_num_zero;
@@ -453,6 +469,11 @@ void finalize_constants() {
     delete g_or_elim;
     delete g_or_intro_left;
     delete g_or_intro_right;
+    delete g_or_rec;
+    delete g_or_resolve_left;
+    delete g_or_resolve_right;
+    delete g_or_neg_resolve_left;
+    delete g_or_neg_resolve_right;
     delete g_poly_unit;
     delete g_poly_unit_star;
     delete g_pos_num;
@@ -604,6 +625,7 @@ name const & get_iff_elim_left_name() { return *g_iff_elim_left; }
 name const & get_iff_elim_right_name() { return *g_iff_elim_right; }
 name const & get_iff_false_intro_name() { return *g_iff_false_intro; }
 name const & get_iff_true_intro_name() { return *g_iff_true_intro; }
+name const & get_implies_resolve_name() { return *g_implies_resolve; }
 name const & get_implies_name() { return *g_implies; }
 name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; }
 name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; }
@@ -619,6 +641,7 @@ name const & get_nat_succ_name() { return *g_nat_succ; }
 name const & get_nat_zero_name() { return *g_nat_zero; }
 name const & get_neg_name() { return *g_neg; }
 name const & get_not_name() { return *g_not; }
+name const & get_not_wrap_name() { return *g_not_wrap; }
 name const & get_not_of_iff_false_name() { return *g_not_of_iff_false; }
 name const & get_num_name() { return *g_num; }
 name const & get_num_zero_name() { return *g_num_zero; }
@@ -632,6 +655,11 @@ name const & get_or_name() { return *g_or; }
 name const & get_or_elim_name() { return *g_or_elim; }
 name const & get_or_intro_left_name() { return *g_or_intro_left; }
 name const & get_or_intro_right_name() { return *g_or_intro_right; }
+name const & get_or_rec_name() { return *g_or_rec; }
+name const & get_or_resolve_left_name() { return *g_or_resolve_left; }
+name const & get_or_resolve_right_name() { return *g_or_resolve_right; }
+name const & get_or_neg_resolve_left_name() { return *g_or_neg_resolve_left; }
+name const & get_or_neg_resolve_right_name() { return *g_or_neg_resolve_right; }
 name const & get_poly_unit_name() { return *g_poly_unit; }
 name const & get_poly_unit_star_name() { return *g_poly_unit_star; }
 name const & get_pos_num_name() { return *g_pos_num; }

src/library/constants.h

@@ -68,6 +68,7 @@ name const & get_iff_elim_left_name();
 name const & get_iff_elim_right_name();
 name const & get_iff_false_intro_name();
 name const & get_iff_true_intro_name();
+name const & get_implies_resolve_name();
 name const & get_implies_name();
 name const & get_implies_of_if_pos_name();
 name const & get_implies_of_if_neg_name();
@@ -83,6 +84,7 @@ name const & get_nat_succ_name();
 name const & get_nat_zero_name();
 name const & get_neg_name();
 name const & get_not_name();
+name const & get_not_wrap_name();
 name const & get_not_of_iff_false_name();
 name const & get_num_name();
 name const & get_num_zero_name();
@@ -96,6 +98,11 @@ name const & get_or_name();
 name const & get_or_elim_name();
 name const & get_or_intro_left_name();
 name const & get_or_intro_right_name();
+name const & get_or_rec_name();
+name const & get_or_resolve_left_name();
+name const & get_or_resolve_right_name();
+name const & get_or_neg_resolve_left_name();
+name const & get_or_neg_resolve_right_name();
 name const & get_poly_unit_name();
 name const & get_poly_unit_star_name();
 name const & get_pos_num_name();

src/library/constants.txt

@@ -61,6 +61,7 @@ iff.elim_left
 iff.elim_right
 iff_false_intro
 iff_true_intro
+implies.resolve
 implies
 implies_of_if_pos
 implies_of_if_neg
@@ -76,6 +77,7 @@ nat.succ
 nat.zero
 neg
 not
+not.wrap
 not_of_iff_false
 num
 num.zero
@@ -89,6 +91,11 @@ or
 or.elim
 or.intro_left
 or.intro_right
+or.rec
+or.resolve_left
+or.resolve_right
+or.neg_resolve_left
+or.neg_resolve_right
 poly_unit
 poly_unit.star
 pos_num

src/library/util.cpp

@@ -304,6 +304,13 @@ expr mk_false_rec(type_checker & tc, expr const & f, expr const & t) {
     }
 }
 
+bool is_or(expr const & e) {
+    buffer<expr> args;
+    expr const & fn = get_app_args(e, args);
+    if (is_constant(fn) && const_name(fn) == get_or_name() && args.size() == 2) return true;
+    else return false;
+}
+
 bool is_or(expr const & e, expr & A, expr & B) {
     buffer<expr> args;
     expr const & fn = get_app_args(e, args);

src/library/util.h

@@ -143,6 +143,7 @@ bool is_false(environment const & env, expr const & e);
 /** \brief Return an element of type t given an element \c f : false (in standard mode) and empty (in HoTT) mode */
 expr mk_false_rec(type_checker & tc, expr const & f, expr const & t);
 
+bool is_or(expr const & e);
 bool is_or(expr const & e, expr & A, expr & B);
 
 /** \brief Return true if \c e is of the form <tt>(not arg)</tt>, and store \c arg in \c a.

tests/lean/run/blast22.lean

@@ -1,13 +0,0 @@
--- Basic (propositional) forward chaining
-constants (A B C D : Prop)
-
-definition lemma1 : A → (A → B) → B := by blast
-definition lemma2 : ¬ B → (A → B) → ¬ A := by blast
-definition lemma3 : ¬ C → A → (A → B → C) → ¬ B := by blast
-definition lemma4 : C → A → (A → B → ¬ C) → ¬ B := by blast
--- TODO(dhs): [forward_action] is responsible for
--- eliminating double negation
-definition lemma5 : C → A → (A → ¬ B → ¬ C) → ¬ ¬ B := by blast
-definition lemma6 : (A → B → ¬ C) → C → A → ¬ B := by blast
-definition lemma7 : ¬ C → (A → B → C) → A → ¬ B := by blast
-definition lemma8 : A → (A → B) → C → B ∧ C := by blast

tests/lean/run/blast23.lean

@@ -1,9 +0,0 @@
--- Basic (propositional) forward chaining with nested backward chaining
-constants (A B C D : Prop)
-set_option blast.trace true
-set_option blast.init_depth 10
-set_option blast.inc_depth 1000
-set_option pp.all true
-
-definition lemma1 : A → (A → B) → C → B ∧ C :=
-by blast

tests/lean/run/blast24.lean

@@ -1,12 +0,0 @@
--- Basic (propositional) forward chaining with clauses
-constants (A B C D E : Prop)
-set_option blast.recursor false
-
-definition lemma1 : A → (A ∨ B → C) → C := by blast
-definition lemma2 : B → (A ∨ B → C) → C := by blast
-definition lemma3 : A → B → (A → B ∨ C → D) → D := by blast
-definition lemma4 : A → B → (A → B ∨ C ∨ C → D) → D := by blast
-definition lemma5 : A → B → (E ∨ A ∨ E → E ∨ B ∨ C ∨ C → D) → D := by blast
-definition lemma6 : A → (A → B → C) → ¬ C → ¬ B := by blast
-definition lemma7 : ¬ D → B → (A → E ∨ B ∨ C ∨ C → D) → ¬ A := by blast
-definition lemma8 : ¬ D → B → (A ∨ E → E ∨ B ∨ C ∨ C → D) → ¬ (A ∨ E) := by blast

tests/lean/run/blast25.lean

@@ -1,12 +0,0 @@
--- Basic (propositional) forward chaining with conjunctive conclusions
-constants (A B C D E : Prop)
-set_option blast.recursor false
-
-definition lemma1 : B → (A → (¬ B) ∧ C) → ¬ A := by blast
-definition lemma2 : ¬ B → (A → B ∧ C) → ¬ A := by blast
-definition lemma3 : B → (A → C ∧ (¬ B)) → ¬ A := by blast
-definition lemma4 : ¬ B → (A → C ∧ B) → ¬ A := by blast
-definition lemma5 : B → (A → (¬ B) ∧ E ∧ C) → ¬ A := by blast
-definition lemma6 : ¬ B → (A → E ∧ B ∧ C) → ¬ A := by blast
-definition lemma7 : B → (A → E ∧ C ∧ (¬ B)) → ¬ A := by blast
-definition lemma8 : ¬ B → (A → C ∧ B ∧ E) → ¬ A := by blast

tests/lean/run/blast26.lean

@@ -1,10 +0,0 @@
--- Basic (propositional) forward chaining with disjunctive antecedents and conjunctive conclusions
-constants (A B C D E F : Prop)
-set_option blast.recursor false
-
-definition lemma1 : B → (A ∨ E → (¬ B) ∧ C) → ¬ (A ∨ E) := by blast
-definition lemma2 : ¬ B → (A ∨ E → B ∧ C) → ¬ (A ∨ E) := by blast
-definition lemma3 : A → ¬ D → (A ∨ E → B → C ∧ D) → ¬ B := by blast
-definition lemma4 : A → ¬ E → (A → B → E ∧ F) → ¬ B := by blast
-definition lemma5 : (A → B) → ¬ B → ¬ A := by blast
-definition lemma6 : (A → B ∧ C) → ¬ B → ¬ A := by blast

tests/lean/run/blast_unit.lean

@@ -0,0 +1,43 @@
+-- Testing all possible cases of [unit_action]
+set_option blast.recursor false
+variables {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Prop}
+
+-- H first, all pos
+example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) : B₄ := by blast
+example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₄) : B₃ := by blast
+example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n3 : ¬ B₃) (n3 : ¬ B₄) : B₂ := by blast
+example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : B₁ := by blast
+
+example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : ¬ A₃ := by blast
+example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : ¬ A₂ := by blast
+example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : ¬ A₁ := by blast
+
+-- H last, all pos
+example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₄ := by blast
+example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₃ := by blast
+example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₂ := by blast
+example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₁ := by blast
+
+example (a1 : A₁) (a2 : A₂) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : ¬ A₃ := by blast
+example (a1 : A₁) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : ¬ A₂ := by blast
+example (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : ¬ A₁ := by blast
+
+-- H first, all neg
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) : ¬ B₄ := by blast
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b4 : B₄) : ¬ B₃ := by blast
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b3 : B₃) (b4 : B₄) : ¬ B₂ := by blast
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ B₁ := by blast
+
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ ¬ A₃ := by blast
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ ¬ A₂ := by blast
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ ¬ A₁ := by blast
+
+-- H last, all neg
+example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₄ := by blast
+example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₃ := by blast
+example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₂ := by blast
+example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₁ := by blast
+
+example (n1 : ¬ A₁) (n2 : ¬ A₂) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₃ := by blast
+example (n1 : ¬ A₁) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₂ := by blast
+example (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₁ := by blast

tests/lean/run/blast_unit_cc.lean

@@ -1,4 +1,4 @@
--- Basic (propositional) forward chaining with conjunctive conclusions
+-- Unit propagation with congruence closure
 constants (a b c d e : nat)
 constants (p : nat → Prop)
 constants (q : nat → nat → Prop)
@@ -6,6 +6,8 @@ constants (f : nat → nat)
 set_option blast.recursor false
 set_option blast.subst    false
 
+-- The following tests require the unit preprocessor to work
+/-
 definition lemma1  : a = d → b = e → p b → (p a → (¬ p e) ∧ p c) → ¬ p d := by blast
 definition lemma2a : ¬ p b → (p d → p b ∧ p c) → d = e → e = a → ¬ p a := by blast
 definition lemma2b : ¬ p (f b) → (p (f a) → p (f d) ∧ p (f c)) → b = d → ¬ p (f a) := by blast
@@ -15,3 +17,4 @@ definition lemma4b : b = f b → ¬ p (f (f b)) → (p a → q c c ∧ q e c ∧
 by blast
 definition lemma5 : p b → (p (f a) → (¬ p b) ∧ p e ∧ p c) → ¬ p (f a) := by blast
 definition lemma6 : ¬ (q b a) → d = a → (p a → p e ∧ (q b d) ∧ p c) → ¬ p a := by blast
+-/