refactor(library/tactic): remove duplicate code, add add_proofs

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/tactic/boolean.cpp

@@ -261,14 +261,7 @@ tactic absurd_tactic() {
                 });
             if (empty(proofs))
                 return none_proof_state(); // tactic failed
-            proof_builder pb     = s.get_proof_builder();
+            proof_builder new_pb = add_proofs(s.get_proof_builder(), proofs);
-            proof_builder new_pb = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
-                    proof_map new_m(m);
-                    for (auto const & np : proofs) {
-                        new_m.insert(np.first, np.second);
-                    }
-                    return pb(new_m, a);
-                });
             return some(proof_state(s, new_gs, new_pb));
         });
 }

src/library/tactic/proof_builder.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <utility>
 #include "util/script_state.h"
 #include "util/exception.h"
 #include "util/sstream.h"
@@ -19,6 +20,16 @@ expr find(proof_map const & m, name const & n) {
     throw exception(sstream() << "proof for goal '" << n << "' not found");
 }
 
+proof_builder add_proofs(proof_builder const & pb, list<std::pair<name, expr>> const & prs) {
+    return mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
+            proof_map new_m(m);
+            for (auto const & np : prs) {
+                new_m.insert(np.first, np.second);
+            }
+            return pb(new_m, a);
+        });
+}
+
 DECL_UDATA(proof_map)
 
 static int mk_proof_map(lua_State * L) {

src/library/tactic/proof_builder.h

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <utility>
 #include <algorithm>
 #include "util/lua.h"
 #include "util/debug.h"
@@ -68,6 +69,8 @@ proof_builder mk_proof_builder(F && f) {
     return proof_builder(new proof_builder_tpl<F>(std::forward<F>(f)));
 }
 
+proof_builder add_proofs(proof_builder const & pb, list<std::pair<name, expr>> const & prs);
+
 UDATA_DEFS_CORE(proof_map)
 UDATA_DEFS(assignment)
 UDATA_DEFS(proof_builder)

src/library/tactic/tactic.cpp

@@ -180,7 +180,6 @@ tactic suppress_trace(tactic const & t) {
 tactic assumption_tactic() {
     return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             list<std::pair<name, expr>> proofs;
-            bool found = false;
             goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
                     expr const & c  = g.get_conclusion();
                     expr pr;
@@ -193,24 +192,15 @@ tactic assumption_tactic() {
                     }
                     if (pr) {
                         proofs.emplace_front(ng, pr);
-                        found = true;
                         return goal();
                     } else {
                         return g;
                     }
                 });
-            proof_builder pr_builder     = s.get_proof_builder();
+            if (empty(proofs))
-            proof_builder new_pr_builder = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
-                    proof_map new_m(m);
-                    for (auto const & np : proofs) {
-                        new_m.insert(np.first, np.second);
-                    }
-                    return pr_builder(new_m, a);
-                });
-            if (found)
-                return some(proof_state(s, new_goals, new_pr_builder));
-            else
                 return none_proof_state();
+            proof_builder new_pb = add_proofs(s.get_proof_builder(), proofs);
+            return some(proof_state(s, new_goals, new_pb));
         });
 }