feat(library/tactic): add conj_hyp_tactic

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

src/library/tactic/boolean.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/interrupt.h"
 #include "kernel/builtin.h"
 #include "kernel/abstract.h"
+#include "kernel/occurs.h"
 #include "library/basic_thms.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
@@ -95,4 +96,63 @@ tactic imp_tactic(name const & H_name, bool all) {
             }
         });
 }
+tactic conj_hyp_tactic(bool all) {
+    return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
+            expr andfn = mk_and_fn();
+            bool found = false;
+            list<std::pair<name, list<std::pair<name, expr>>>> proof_info; // goal name, list(hypothesis name, hypothesis prop)
+            goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
+                    if (all || !found) {
+                        buffer<std::pair<name, expr>> new_hyp_buf;
+                        list<std::pair<name, expr>> proof_info_data;
+                        for (auto const & p : g.get_hypotheses()) {
+                            name const & H_name = p.first;
+                            expr const & H_prop = p.second;
+                            if ((all || !found) && is_app_of(H_prop, andfn)) {
+                                found       = true;
+                                proof_info_data.emplace_front(H_name, H_prop);
+                                new_hyp_buf.emplace_back(name(H_name, 1), arg(H_prop, 1));
+                                new_hyp_buf.emplace_back(name(H_name, 2), arg(H_prop, 2));
+                            } else {
+                                new_hyp_buf.push_back(p);
+                            }
+                        }
+                        if (proof_info_data) {
+                            proof_info.emplace_front(ng, proof_info_data);
+                            return goal(to_list(new_hyp_buf.begin(), new_hyp_buf.end()), g.get_conclusion());
+                        } else {
+                            return g;
+                        }
+                    } else {
+                        return g;
+                    }
+                });
+            if (found) {
+                proof_builder p     = s.get_proof_builder();
+                proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr {
+                        proof_map new_m(m);
+                        for (auto const & info : proof_info) {
+                            name const & goal_name    = info.first;
+                            auto const & expanded_hyp = info.second;
+                            expr pr                   = find(m, goal_name); // proof for the new conclusion
+                            for (auto const & H_name_prop : expanded_hyp) {
+                                name const & H_name   = H_name_prop.first;
+                                expr const & H_prop   = H_name_prop.second;
+                                expr const & H_1      = mk_constant(name(H_name, 1), arg(H_prop, 1));
+                                expr const & H_2      = mk_constant(name(H_name, 2), arg(H_prop, 2));
+                                if (occurs(H_1, pr))
+                                    pr = Let(H_1, Conjunct1(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
+                                if (occurs(H_2, pr))
+                                    pr = Let(H_2, Conjunct2(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
+                            }
+                            new_m.insert(goal_name, pr);
+                        }
+                        return p(new_m, env, a);
+                    });
+                return some(proof_state(s, new_goals, new_p));
+            } else {
+                return optional<proof_state>();
+            }
+        });
+}
 }

src/library/tactic/boolean.h

@@ -8,5 +8,6 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic.h"
 namespace lean {
 tactic conj_tactic(bool all = true);
+tactic conj_hyp_tactic(bool all = true);
 tactic imp_tactic(name const & H_name = name("H"), bool all = true);
 }

src/library/tactic/goal.cpp

@@ -47,7 +47,7 @@ name goal::mk_unique_hypothesis_name(name const & suggestion) const {
     while (true) {
         bool ok = true;
         for (auto const & p : m_hypotheses) {
-            if (n == p.first) {
+            if (is_prefix_of(n, p.first)) {
                 ok = false;
                 break;
             }

src/tests/library/tactic/tactic.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "util/interrupt.h"
 #include "kernel/builtin.h"
+#include "kernel/kernel_exception.h"
 #include "library/all/all.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
@@ -121,8 +122,12 @@ static void tst2() {
     import_all(env);
     env.add_var("p", Bool);
     env.add_var("q", Bool);
+    env.add_var("r", Bool);
+    env.add_var("s", Bool);
     expr p = Const("p");
     expr q = Const("q");
+    expr r = Const("r");
+    expr s = Const("s");
     context ctx;
     ctx = extend(ctx, "H1", p);
     ctx = extend(ctx, "H2", q);
@@ -130,9 +135,9 @@ static void tst2() {
               << "\n";
     std::cout << "-------------\n";
     // Theorem to be proved
-    expr F   = Implies(p, Implies(q, And(And(p, q), And(p, p))));
+    expr F   = Implies(And(p, And(r, s)), Implies(q, And(And(p, q), And(r, p))));
     // Tactic
-    tactic T = repeat(conj_tactic() || imp_tactic()) << trace_state_tactic() << assumption_tactic();
+    tactic T = repeat(conj_tactic() || conj_hyp_tactic() || imp_tactic()) << trace_state_tactic() << assumption_tactic();
     // Generate proof using tactic
     expr pr  = T.solve(env, io, context(), F);
     // Print proof