feat(library/blast/unit): conjunctive conclusions

src/library/blast/unit/unit_action.cpp

@@ -32,11 +32,20 @@ struct unit_branch_extension : public branch_extension {
     virtual ~unit_branch_extension() {}
     virtual branch_extension * clone() override { return new unit_branch_extension(*this); }
 
-    void insert_disjunction(expr const & e, hypothesis_idx hidx) {
+    void insert(expr const & e, hypothesis_idx hidx, bool neg) {
         expr A, B;
         if (is_or(e, A, B)) {
-            insert_disjunction(A, hidx);
-            insert_disjunction(B, hidx);
+            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);
         }
@@ -51,13 +60,11 @@ struct unit_branch_extension : public branch_extension {
         bool has_antecedent = false;
         while (is_pi(type) && is_prop(binding_domain(type)) && closed(binding_body(type))) {
             has_antecedent = true;
-            insert_disjunction(binding_domain(type), hidx);
+            insert(binding_domain(type), hidx, false);
             type = binding_body(type);
         }
         if (has_antecedent && is_prop(type)) {
-            expr not_type;
-            if (blast::is_not(type, not_type)) m_lemma_map.insert(not_type, hidx);
-            else m_lemma_map.insert(get_app_builder().mk_not(type), hidx);
+            insert(type, hidx, true);
         }
     }
 
@@ -71,6 +78,7 @@ public:
     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)) {
@@ -96,6 +104,41 @@ public:
             }
         }
     }
+
+    /* Returns a proof of [false], by either applying a projection of [proof] to a hypothesis or vice versa. */
+    optional<expr> find_live_disproof_of_conjunction(expr const & e, expr const & proof) {
+        expr A, B;
+        if (is_and(e, A, B)) {
+            if (auto A_false = find_live_disproof_of_conjunction(A, get_app_builder().mk_app(get_and_elim_left_name(), {A, B, proof}))) {
+                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}))) {
+                return some_expr(*B_false);
+            } else {
+                return none_expr();
+            }
+        } else {
+            expr not_e;
+            bool not_e_is_not = false;
+            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();
+            }
+        }
+    }
 };
 
 void initialize_unit_action() {
@@ -136,27 +179,13 @@ action_result unit_pi(expr const & _type, expr const & proof) {
         curr_state().mk_hypothesis(type, new_hypothesis);
         return action_result::new_branch();
     } else if (is_prop(type)) {
-        expr not_type;
-        if (blast::is_not(type, not_type)) {
-            optional<expr> fact = ext.find_live_fact_in_disjunction(not_type);
-            if (fact) {
-                // TODO(dhs): if classical, use double negation elimination
-                curr_state().mk_hypothesis(get_app_builder().mk_not(infer_type(local)),
-                                           Fun(local, mk_app(new_hypothesis, *fact)));
-                return action_result::new_branch();
-            } else {
-                return action_result::failed();
-            }
+        optional<expr> disproof = ext.find_live_disproof_of_conjunction(type, new_hypothesis);
+        if (disproof) {
+            curr_state().mk_hypothesis(get_app_builder().mk_not(infer_type(local)),
+                                       Fun(local, *disproof));
+            return action_result::new_branch();
         } else {
-            not_type = get_app_builder().mk_not(type);
-            optional<expr> fact = ext.find_live_fact_in_disjunction(not_type);
-            if (fact) {
-                curr_state().mk_hypothesis(get_app_builder().mk_not(infer_type(local)),
-                                           Fun(local, mk_app(*fact, new_hypothesis)));
-                return action_result::new_branch();
-            } else {
-                return action_result::failed();
-            }
+            return action_result::failed();
         }
     } else {
         return action_result::failed();

src/library/blast/unit/unit_action.h

@@ -8,6 +8,19 @@ Author: Daniel Selsam
 
 namespace lean {
 namespace blast {
+/* \brief Propagates lemmas of the form
+   <tt>(A11 \/ ... \/ ...) -> ... -> (Am1 \/ ... \/ ...) -> (B1 /\ ... /\ ...)</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
+   fully. On the other hand, if we can find one disjunct for all but one
+   antecedents, and one fact that disproves the conjunctive conclusion,
+   we conclude the negation of the missing disjunctive argument.
+
+   Remark: conjunctions in the antecedents and disjunctions in the conclusion are
+   both treated as monolithic propositions, so some pre-processing may be necessary.
+*/
 action_result unit_action(unsigned hidx);
 
 void initialize_unit_action();

tests/lean/run/blast25.lean

@@ -0,0 +1,12 @@
+-- Basic (propositional) forward chaining with conjunctive conclusions
+constants (A B C D E : Prop)
+set_option pp.all true
+
+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

@@ -0,0 +1,10 @@
+-- Basic (propositional) forward chaining with disjunctive antecedents and conjunctive conclusions
+constants (A B C D E F : Prop)
+
+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