feat(library/tactic): add disj_tactic

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

src/library/tactic/boolean.cpp

@@ -239,6 +239,87 @@ tactic disj_hyp_tactic() {
         });
 }
 
+typedef std::pair<proof_state, proof_state> proof_state_pair;
+
+optional<proof_state_pair> disj_tactic(proof_state const & s, name gname) {
+    precision prec = s.get_precision();
+    if (prec != precision::Precise && prec != precision::Over) {
+        // it is pointless to apply this tactic, since it will produce UnderOver
+        optional<proof_state_pair>();
+    }
+    buffer<std::pair<name, goal>> new_goals_buf1, new_goals_buf2;
+    expr conclusion;
+    for (auto const & p : s.get_goals()) {
+        check_interrupted();
+        goal const & g = p.second;
+        expr const & c = g.get_conclusion();
+        if (!conclusion && ((gname.is_anonymous() && is_or(c)) || p.first == gname)) {
+            gname = p.first;
+            conclusion = c;
+            expr c1, c2;
+            if (is_or(c, c1, c2)) {
+                new_goals_buf1.emplace_back(gname, update(g, c1));
+                new_goals_buf2.emplace_back(gname, update(g, c2));
+            } else {
+                return optional<proof_state_pair>(); // failed
+            }
+        } else {
+            new_goals_buf1.push_back(p);
+            new_goals_buf2.push_back(p);
+        }
+    }
+    if (!conclusion) {
+        return optional<proof_state_pair>(); // failed
+    } else {
+        goals new_gs1 = to_list(new_goals_buf1.begin(), new_goals_buf1.end());
+        goals new_gs2 = to_list(new_goals_buf2.begin(), new_goals_buf2.end());
+        proof_builder pb     = s.get_proof_builder();
+        proof_builder new_pb1 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
+                proof_map new_m(m);
+                new_m.insert(gname, Disj1(arg(conclusion, 1), arg(conclusion, 2), find(m, gname)));
+                return pb(new_m, a);
+            });
+        proof_builder new_pb2 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
+                proof_map new_m(m);
+                new_m.insert(gname, Disj2(arg(conclusion, 2), arg(conclusion, 1), find(m, gname)));
+                return pb(new_m, a);
+            });
+        proof_state s1(precision::Over, new_gs1, s.get_menv(), new_pb1, s.get_cex_builder());
+        proof_state s2(precision::Over, new_gs2, s.get_menv(), new_pb2, s.get_cex_builder());
+        return some(mk_pair(s1, s2));
+    }
+}
+
+proof_state_seq disj_tactic_core(proof_state const & s, name const & gname) {
+    return mk_proof_state_seq([=]() {
+            auto p = disj_tactic(s, gname);
+            if (p) {
+                return some(mk_pair(p->first, proof_state_seq(p->second)));
+            } else {
+                return proof_state_seq::maybe_pair();
+            }
+        });
+}
+
+tactic disj_tactic(name const & gname) {
+    return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq {
+            return disj_tactic_core(s, gname);
+        });
+}
+
+tactic disj_tactic() {
+    return disj_tactic(name());
+}
+
+tactic disj_tactic(unsigned i) {
+    return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq {
+            if (optional<name> n = s.get_ith_goal_name(i))
+                return disj_tactic_core(s, *n);
+            else
+                return proof_state_seq();
+        });
+}
+
 tactic absurd_tactic() {
     return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             list<std::pair<name, expr>> proofs;
@@ -291,6 +372,16 @@ static int mk_disj_hyp_tactic(lua_State * L) {
         return push_tactic(L, disj_hyp_tactic(to_name_ext(L, 1), to_name_ext(L, 2)));
 }
 
+static int mk_disj_tactic(lua_State * L) {
+    int nargs = lua_gettop(L);
+    if (nargs == 0)
+        return push_tactic(L, disj_tactic());
+    else if (lua_isnumber(L, 1))
+        return push_tactic(L, disj_tactic(lua_tointeger(L, 1)));
+    else
+        return push_tactic(L, disj_tactic(to_name_ext(L, 1)));
+}
+
 static int mk_absurd_tactic(lua_State * L) {
     return push_tactic(L, absurd_tactic());
 }
@@ -300,6 +391,7 @@ void open_boolean(lua_State * L) {
     SET_GLOBAL_FUN(mk_imp_tactic,      "imp_tactic");
     SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tactic");
     SET_GLOBAL_FUN(mk_disj_hyp_tactic, "disj_hyp_tactic");
+    SET_GLOBAL_FUN(mk_disj_tactic,     "disj_tactic");
     SET_GLOBAL_FUN(mk_absurd_tactic,   "absurd_tactic");
 }
 }

src/library/tactic/boolean.h

@@ -13,6 +13,9 @@ tactic imp_tactic(name const & H_name = name("H"), bool all = true);
 tactic disj_hyp_tactic(name const & goal_name, name const & hyp_name);
 tactic disj_hyp_tactic(name const & hyp_name);
 tactic disj_hyp_tactic();
+tactic disj_tactic();
+tactic disj_tactic(unsigned i);
+tactic disj_tactic(name const & gname);
 tactic absurd_tactic();
 void open_boolean(lua_State * L);
 }

src/library/tactic/proof_state.cpp

@@ -10,6 +10,16 @@ Author: Leonardo de Moura
 #include "library/tactic/proof_state.h"
 
 namespace lean {
+optional<name> get_ith_goal_name(goals const & gs, unsigned i) {
+    unsigned j = 1;
+    for (auto const & p : gs) {
+        if (i == j)
+            return some(p.first);
+        j++;
+    }
+    return optional<name>();
+}
+
 precision mk_union(precision p1, precision p2) {
     if (p1 == p2) return p1;
     else if (p1 == precision::Precise) return p2;

src/library/tactic/proof_state.h

@@ -19,6 +19,12 @@ Author: Leonardo de Moura
 
 namespace lean {
 typedef list<std::pair<name, goal>> goals;
+/**
+   \brief Return the name of the i-th goal.
+
+   \remark Return none if i == 0 or i > size(g)
+*/
+optional<name> get_ith_goal_name(goals const & gs, unsigned i);
 
 enum class precision {
     Precise,
@@ -84,6 +90,9 @@ public:
        \brief Store in \c r the goal names
     */
     void get_goal_names(name_set & r) const;
+
+    optional<name> get_ith_goal_name(unsigned i) const { return ::lean::get_ith_goal_name(get_goals(), i); }
+
     format pp(formatter const & fmt, options const & opts) const;
 };
 

src/library/tactic/tactic.cpp

@@ -342,12 +342,9 @@ tactic focus(tactic const & t, name const & gname) {
 
 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++;
-            }
+            if (optional<name> n = s.get_ith_goal_name(i))
+                return focus_core(t, *n, env, io, s);
+            else
                 return proof_state_seq();
         });
 }

tests/lean/disj1.lean

@@ -0,0 +1,19 @@
+Theorem T1 (a b : Bool) : a \/ b => b \/ a.
+    apply imp_tactic
+    apply disj_hyp_tactic
+    apply disj_tactic
+    back
+    apply assumption_tactic
+    apply disj_tactic
+    apply assumption_tactic
+    done
+
+(**
+simple_tac = REPEAT(ORELSE(imp_tactic, assumption_tactic, disj_hyp_tactic, disj_tactic)) .. now_tactic
+**)
+
+Theorem T2 (a b : Bool) : a \/ b => b \/ a.
+    apply simple_tac
+    done
+
+Show Environment 1.

tests/lean/disj1.lean.expected.out

@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Proved: T1
+  Proved: T2
+Theorem T2 (a b : Bool) : a ∨ b ⇒ b ∨ a :=
+    Discharge (λ H : a ∨ b, DisjCases H (λ H : a, Disj2 b H) (λ H : b, Disj1 a H))