feat(library/tactic): add focus tactical

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

src/library/tactic/cex_builder.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/sstream.h"
 #include "util/script_state.h"
 #include "util/luaref.h"
 #include "library/kernel_bindings.h"
@@ -14,6 +15,15 @@ namespace lean {
 cex_builder & cex_builder::operator=(cex_builder const & s) { LEAN_COPY_REF(cex_builder, s); }
 cex_builder & cex_builder::operator=(cex_builder && s) { LEAN_MOVE_REF(cex_builder, s); }
 
+cex_builder mk_cex_builder_for(name const & gname) {
+    return mk_cex_builder(
+        [=](name const & n, optional<counterexample> const & cex, assignment const &) -> counterexample {
+            if (n != gname || !cex)
+                throw exception(sstream() << "failed to build counterexample for '" << gname << "' goal");
+            return *cex;
+        });
+}
+
 DECL_UDATA(cex_builder)
 
 static int mk_cex_builder(lua_State * L) {

src/library/tactic/cex_builder.h

@@ -68,6 +68,11 @@ cex_builder mk_cex_builder(F && f) {
     return cex_builder(new cex_builder_tpl<F>(std::forward<F>(f)));
 }
 
+/**
+   \brief Return a counterexample builder that expects a counterexample for the given goal.
+*/
+cex_builder mk_cex_builder_for(name const & gname);
+
 UDATA_DEFS(cex_builder)
 void open_cex_builder(lua_State * L);
 }

src/library/tactic/proof_state.cpp

@@ -51,6 +51,12 @@ bool proof_state::is_cex_final_state() const {
     }
 }
 
+void proof_state::get_goal_names(name_set & r) const {
+    for (auto const & p : get_goals()) {
+        r.insert(p.first);
+    }
+}
+
 static name g_main("main");
 
 proof_state to_proof_state(environment const & env, context const & ctx, expr const & t) {
@@ -61,12 +67,7 @@ proof_state to_proof_state(environment const & env, context const & ctx, expr co
         [=](proof_map const & m, assignment const &) -> expr {
             return fn(find(m, g_main));
         });
-    cex_builder cex_builder = mk_cex_builder(
+    cex_builder cex_builder = mk_cex_builder_for(g_main);
-        [](name const & n, optional<counterexample> const & cex, assignment const &) -> counterexample {
-            if (n != g_main || !cex)
-                throw exception(sstream() << "failed to build counterexample for '" << g_main << "' goal");
-            return *cex;
-        });
     return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder, cex_builder);
 }
 

src/library/tactic/proof_state.h

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "util/rc.h"
 #include "util/interrupt.h"
 #include "util/optional.h"
+#include "util/name_set.h"
 #include "library/io_state.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
@@ -52,8 +53,14 @@ public:
     proof_state(proof_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
     proof_state(goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c):
         m_ptr(new cell(gs, menv, p, c)) {}
+    proof_state(precision prec, goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c):
+        m_ptr(new cell(prec, gs, menv, p, c)) {}
     proof_state(proof_state const & s, goals const & gs, proof_builder const & p):
         m_ptr(new cell(s.get_precision(), gs, s.get_menv(), p, s.get_cex_builder())) {}
+    proof_state(proof_state const & s, goals const & gs):
+        m_ptr(new cell(s.get_precision(), gs, s.get_menv(), s.get_proof_builder(), s.get_cex_builder())) {}
+    proof_state(proof_state const & s, goals const & gs, proof_builder const & p, cex_builder const & c):
+        m_ptr(new cell(s.get_precision(), gs, s.get_menv(), p, c)) {}
     ~proof_state() { if (m_ptr) m_ptr->dec_ref(); }
     friend void swap(proof_state & a, proof_state & b) { std::swap(a.m_ptr, b.m_ptr); }
     proof_state & operator=(proof_state const & s) { LEAN_COPY_REF(proof_state, s); }
@@ -73,6 +80,10 @@ public:
        and the precision is \c Precise or \c Under
     */
     bool is_cex_final_state() const;
+    /**
+       \brief Store in \c r the goal names
+    */
+    void get_goal_names(name_set & r) const;
     format pp(formatter const & fmt, options const & opts) const;
 };
 

src/library/tactic/tactic.cpp

@@ -64,6 +64,36 @@ tactic & tactic::operator=(tactic && s) {
     LEAN_MOVE_REF(tactic, s);
 }
 
+/**
+   \brief Try to extract a proof from the given proof state
+*/
+optional<expr> to_proof(proof_state const & s) {
+    if (s.is_proof_final_state()) {
+        try {
+            assignment a(s.get_menv());
+            proof_map  m;
+            return some(s.get_proof_builder()(m, a));
+        } catch (...) {
+        }
+    }
+    return optional<expr>();
+}
+
+/**
+   \brief Try to extract a counterexample from the given proof state.
+*/
+optional<counterexample> to_counterexample(proof_state const & s) {
+    if (s.is_cex_final_state()) {
+        assignment a(s.get_menv());
+        name goal_name(head(s.get_goals()).first);
+        try {
+            return some(s.get_cex_builder()(goal_name, optional<counterexample>(), a));
+        } catch (...) {
+        }
+    }
+    return optional<counterexample>();
+}
+
 solve_result tactic::solve(environment const & env, io_state const & io, proof_state const & s1) {
     proof_state_seq r   = operator()(env, io, s1);
     list<proof_state> failures;
@@ -75,17 +105,12 @@ solve_result tactic::solve(environment const & env, io_state const & io, proof_s
         } else {
             proof_state s2 = p->first;
             r              = p->second;
-            try {
+            optional<expr> pr = to_proof(s2);
-                if (s2.is_proof_final_state()) {
+            if (pr)
-                    assignment a(s2.get_menv());
+                return solve_result(*pr);
-                    proof_map  m;
+            optional<counterexample> cex = to_counterexample(s2);
-                    return solve_result(s2.get_proof_builder()(m, a));
+            if (cex)
-                } else if (s2.is_cex_final_state()) {
+                return solve_result(*cex);
-                    assignment a(s2.get_menv());
-                    name goal_name(head(s2.get_goals()).first);
-                    return solve_result(s2.get_cex_builder()(goal_name, optional<counterexample>(), a));
-                }
-            } catch (exception & ex) {}
             failures = cons(s2, failures);
         }
     }
@@ -137,7 +162,7 @@ tactic trace_state_tactic() {
     return mk_tactic1([=](environment const &, io_state const & io, proof_state const & s) -> proof_state {
             options opts = io.get_options();
             format fmt   = s.pp(io.get_formatter(), opts);
-            io.get_diagnostic_channel() << mk_pair(fmt, opts) << "\n";
+            io.get_diagnostic_channel() << "Proof state:\n" << mk_pair(fmt, opts) << "\n";
             io.get_diagnostic_channel().get_stream().flush();
             return s;
         });
@@ -258,6 +283,81 @@ tactic take(tactic const & t, unsigned k) {
         });
 }
 
+proof_state_seq focus_core(tactic const & t, name const & gname, environment const & env, io_state const & io, proof_state const & s) {
+    for (auto const & p : s.get_goals()) {
+        if (p.first == gname) {
+            proof_builder pb = mk_proof_builder(
+                [=](proof_map const & m, assignment const &) -> expr {
+                    return find(m, gname);
+                });
+            cex_builder cb = mk_cex_builder_for(gname);
+            proof_state new_s(s, goals(p), pb, cb); // new state with singleton goal
+            return map(t(env, io, new_s), [=](proof_state const & s2) {
+                    // we have to put back the goals that were not selected
+                    list<std::pair<name, name>> renamed_goals;
+                    goals new_gs = map_append(s.get_goals(), [&](std::pair<name, goal> const & p) {
+                            if (p.first == gname) {
+                                name_set used_names;
+                                s.get_goal_names(used_names);
+                                used_names.erase(gname);
+                                return map(s2.get_goals(), [&](std::pair<name, goal> const & p2) -> std::pair<name, goal> {
+                                        name uname = mk_unique(used_names, p2.first);
+                                        used_names.insert(uname);
+                                        renamed_goals.emplace_front(p2.first, uname);
+                                        return mk_pair(uname, p2.second);
+                                    });
+                            } else {
+                                return goals(p);
+                            }
+                        });
+                    proof_builder pb1 = s.get_proof_builder();
+                    proof_builder pb2 = s2.get_proof_builder();
+                    proof_builder new_pb = mk_proof_builder(
+                        [=](proof_map const & m, assignment const & a) -> expr {
+                            proof_map m1(m); // map for pb1
+                            proof_map m2; // map for pb2
+                            for (auto p : renamed_goals) {
+                                m2.insert(p.first, find(m, p.second));
+                                m1.erase(p.first);
+                            }
+                            m1.insert(gname, pb2(m2, a));
+                            return pb1(m1, a);
+                        });
+                    cex_builder cb1 = s.get_cex_builder();
+                    cex_builder cb2 = s2.get_cex_builder();
+                    cex_builder new_cb = mk_cex_builder(
+                        [=](name const & n, optional<counterexample> const & cex, assignment const & a) -> counterexample {
+                            for (auto p : renamed_goals) {
+                                if (p.second == n)
+                                    return cb2(p.first, cex, a);
+                            }
+                            return cb1(n, cex, a);
+                        });
+                    return proof_state(s2, new_gs, new_pb, new_cb);
+                });
+        }
+    }
+    return proof_state_seq(); // tactic is not applicable
+}
+
+tactic focus(tactic const & t, name const & gname) {
+    return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
+            return focus_core(t, gname, env, io, s);
+        });
+}
+
+tactic focus(tactic const & t, int i) {
+    return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
+            int j = 1;
+            for (auto const & p : s.get_goals()) {
+                if (i == j)
+                    return focus_core(t, p.first, env, io, s);
+                j++;
+            }
+            return proof_state_seq();
+        });
+}
+
 DECL_UDATA(proof_state_seq)
 
 static const struct luaL_Reg proof_state_seq_m[] = {
@@ -382,6 +482,16 @@ static int tactic_try_for(lua_State * L)        {  return push_tactic(L, try_for
 static int tactic_using_params(lua_State * L)   {  return push_tactic(L, using_params(to_tactic_ext(L, 1), to_options(L, 2))); }
 static int tactic_try(lua_State * L)            {  return push_tactic(L, orelse(to_tactic_ext(L, 1), id_tactic())); }
 
+static int tactic_focus(lua_State * L) {
+    int nargs = lua_gettop(L);
+    if (nargs == 1)
+        return push_tactic(L, focus(to_tactic_ext(L, 1)));
+    else if (lua_isnumber(L, 2))
+        return push_tactic(L, focus(to_tactic_ext(L, 1), lua_tointeger(L, 2)));
+    else
+        return push_tactic(L, focus(to_tactic_ext(L, 1), to_name_ext(L, 2)));
+}
+
 static int push_solve_result(lua_State * L, solve_result const & r) {
     switch (r.kind()) {
     case solve_result_kind::None:           lua_pushnil(L); break;
@@ -544,6 +654,7 @@ static const struct luaL_Reg tactic_m[] = {
     {"try_for",         safe_function<tactic_try_for>},
     {"using_params",    safe_function<tactic_using_params>},
     {"using",           safe_function<tactic_using_params>},
+    {"focus",           safe_function<tactic_focus>},
     {0, 0}
 };
 
@@ -591,5 +702,6 @@ void open_tactic(lua_State * L) {
     SET_GLOBAL_FUN(tactic_using_params,     "USING");
     SET_GLOBAL_FUN(tactic_using_params,     "USING_PARAMS");
     SET_GLOBAL_FUN(tactic_determ,           "DETERM");
+    SET_GLOBAL_FUN(tactic_focus,            "FOCUS");
 }
 }

src/library/tactic/tactic.h

@@ -276,6 +276,17 @@ tactic cond(P && p, tactic const & t1, tactic const & t2) {
 */
 template<typename P>
 tactic when(P && p, tactic const & t) { return cond(std::forward<P>(p), t, id_tactic()); }
+/**
+   \brief Return a tactic that applies \c t only to the goal named \c gname.
+   The tactic fails if the input state does not have a goal named \c gname.
+*/
+tactic focus(tactic const & t, name const & gname);
+/**
+   \brief Return a tactic that applies \c t only to the i-th goal.
+   The tactic fails if the input state does have at least i goals.
+*/
+tactic focus(tactic const & t, int i);
+inline tactic focus(tactic const & t) { return focus(t, 1); }
 
 UDATA_DEFS_CORE(proof_state_seq)
 UDATA_DEFS(tactic);

tests/lean/tactic6.lean

@@ -0,0 +1,21 @@
+Theorem T (a b c : Bool): a => b /\ c => c /\ a /\ b := _.
+   apply imp_tactic
+   apply imp_tactic
+   apply conj_hyp_tactic
+   apply conj_tactic
+   apply (** FOCUS(THEN(show_tactic, conj_tactic, show_tactic, assumption_tactic), 2) **)
+   apply assumption_tactic
+   done
+
+Theorem T2 (a b c : Bool): a => b /\ c => c /\ a /\ b := _.
+   apply imp_tactic
+   apply imp_tactic
+   apply conj_hyp_tactic
+   apply conj_tactic
+   apply show_tactic
+   apply (** FOCUS(THEN(show_tactic, conj_tactic, FOCUS(assumption_tactic, 1)), 2) **)
+   apply show_tactic
+   apply (** FOCUS(assumption_tactic, 1) **)
+   apply show_tactic
+   apply (** FOCUS(assumption_tactic, 1) **)
+   done

tests/lean/tactic6.lean.expected.out

@@ -0,0 +1,4 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Proved: T
+  Proved: T2