feat(library/tactic): expose conj_tactic, imp_tactic, conj_hyp_tactic in the Lua API

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

src/library/tactic/boolean.cpp

@@ -171,4 +171,25 @@ tactic conj_hyp_tactic(bool all) {
             }
         });
 }
+
+static int mk_conj_tactic(lua_State * L) {
+    int nargs = lua_gettop(L);
+    return push_tactic(L, conj_tactic(nargs == 0 ? true : lua_toboolean(L, 1)));
+}
+
+static int mk_imp_tactic(lua_State * L) {
+    int nargs = lua_gettop(L);
+    return push_tactic(L, imp_tactic(nargs >= 1 ? to_name_ext(L, 1) : name("H"), nargs == 2 ? lua_toboolean(L, 2) : true));
+}
+
+static int mk_conj_hyp_tactic(lua_State * L) {
+    int nargs = lua_gettop(L);
+    return push_tactic(L, conj_hyp_tactic(nargs == 0 ? true : lua_toboolean(L, 1)));
+}
+
+void open_boolean(lua_State * L) {
+    SET_GLOBAL_FUN(mk_conj_tactic,     "conj_tactic");
+    SET_GLOBAL_FUN(mk_imp_tactic,      "imp_tactic");
+    SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tactic");
+}
 }

src/library/tactic/boolean.h

@@ -10,4 +10,5 @@ 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);
+void open_boolean(lua_State * L);
 }

src/library/tactic/register_module.h

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/tactic/cex_builder.h"
 #include "library/tactic/proof_state.h"
 #include "library/tactic/tactic.h"
+#include "library/tactic/boolean.h"
 
 namespace lean {
 inline void open_tactic_module(lua_State * L) {
@@ -19,6 +20,7 @@ inline void open_tactic_module(lua_State * L) {
     open_cex_builder(L);
     open_proof_state(L);
     open_tactic(L);
+    open_boolean(L);
 }
 inline void register_tactic_module() {
     script_state::register_module(open_tactic_module);

tests/lean/tactic1.lean

@@ -0,0 +1,11 @@
+Variables p q r : Bool
+
+(**
+ local env = get_environment()
+ local conjecture = parse_lean('p => q => p && q')
+ local tac = REPEAT(conj_tactic() ^ imp_tactic()) .. assumption_tactic()
+ local proof = tac:solve(env, context(), conjecture)
+ env:add_theorem("T1", conjecture, proof)
+**)
+
+Show Environment 1.

tests/lean/tactic1.lean.expected.out

@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: p
+  Assumed: q
+  Assumed: r
+Theorem T1 : p ⇒ q ⇒ p ∧ q := Discharge (λ H : p, Discharge (λ H::1 : q, Conj H H::1))