feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators

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

src/library/tactic/tactic.cpp

@@ -317,11 +317,25 @@ static int tactic_call(lua_State * L) {
     }
 }
 
+typedef tactic (*binary_tactic_fn)(tactic const &, tactic const &);
+
+template<binary_tactic_fn F>
+static int nary_tactic(lua_State * L) {
+    int nargs = lua_gettop(L);
+    if (nargs < 2)
+        throw exception("tactical expects at least two arguments");
+    tactic r = F(to_tactic(L, 1), to_tactic(L, 2));
+    for (int i = 3; i <= nargs; i++)
+        r = F(r, to_tactic(L, i));
+    return push_tactic(L, r);
+}
+
 static int tactic_then(lua_State * L)           {  return push_tactic(L, then(to_tactic(L, 1), to_tactic(L, 2)));   }
 static int tactic_orelse(lua_State * L)         {  return push_tactic(L, orelse(to_tactic(L, 1), to_tactic(L, 2))); }
 static int tactic_append(lua_State * L)         {  return push_tactic(L, append(to_tactic(L, 1), to_tactic(L, 2))); }
 static int tactic_interleave(lua_State * L)     {  return push_tactic(L, interleave(to_tactic(L, 1), to_tactic(L, 2))); }
 static int tactic_par(lua_State * L)            {  return push_tactic(L, par(to_tactic(L, 1), to_tactic(L, 2))); }
+
 static int tactic_repeat(lua_State * L)         {  return push_tactic(L, repeat(to_tactic(L, 1))); }
 static int tactic_repeat1(lua_State * L)        {  return push_tactic(L, repeat1(to_tactic(L, 1))); }
 static int tactic_repeat_at_most(lua_State * L) {  return push_tactic(L, repeat_at_most(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
@@ -522,19 +536,19 @@ void open_tactic(lua_State * L) {
     SET_GLOBAL_FUN(mk_assumption_tactic, "assump_tactic");
     SET_GLOBAL_FUN(mk_lua_tactic01,      "tactic");
     // HOL-like tactic names
-    SET_GLOBAL_FUN(tactic_then,           "THEN");
+    SET_GLOBAL_FUN(nary_tactic<then>,       "THEN");
-    SET_GLOBAL_FUN(tactic_orelse,         "ORELSE");
+    SET_GLOBAL_FUN(nary_tactic<orelse>,     "ORELSE");
-    SET_GLOBAL_FUN(tactic_append,         "APPEND");
+    SET_GLOBAL_FUN(nary_tactic<interleave>, "INTERLEAVE");
+    SET_GLOBAL_FUN(nary_tactic<append>,     "APPEND");
+    SET_GLOBAL_FUN(nary_tactic<par>,        "PAR");
     SET_GLOBAL_FUN(tactic_repeat,           "REPEAT");
     SET_GLOBAL_FUN(tactic_repeat_at_most,   "REPEAT_AT_MOST");
     SET_GLOBAL_FUN(tactic_repeat1,          "REPEAT1");
-    SET_GLOBAL_FUN(tactic_interleave,     "INTERLEAVE");
     SET_GLOBAL_FUN(mk_lua_cond_tactic,      "COND");
     SET_GLOBAL_FUN(mk_lua_when_tactic,      "WHEN");
     SET_GLOBAL_FUN(tactic_try,              "TRY");
     SET_GLOBAL_FUN(tactic_try_for,          "TRY_FOR");
     SET_GLOBAL_FUN(tactic_take,             "TAKE");
-    SET_GLOBAL_FUN(tactic_par,            "PAR");
     SET_GLOBAL_FUN(tactic_using_params,     "USING");
     SET_GLOBAL_FUN(tactic_using_params,     "USING_PARAMS");
     SET_GLOBAL_FUN(tactic_determ,           "DETERM");

src/library/tactic/tactic.h

@@ -222,7 +222,8 @@ tactic interleave(tactic const & t1, tactic const & t2);
    \remark \c check_ms is how often the main thread checks whether the children
    threads finished.
 */
-tactic par(tactic const & t1, tactic const & t2, unsigned check_ms = 1);
+tactic par(tactic const & t1, tactic const & t2, unsigned check_ms);
+inline tactic par(tactic const & t1, tactic const & t2) { return par(t1, t2, 1); }
 
 /**
    \brief Return a tactic that keeps applying \c t until it fails.

tests/lean/tactic3.lean

@@ -0,0 +1,8 @@
+Variables p q r : Bool
+
+Theorem T1 : p => p /\ q => r => q /\ r /\ p := _.
+    apply (** return REPEAT(ORELSE(imp_tactic(), conj_tactic(), conj_hyp_tactic(), assumption_tactic())) **)
+    done
+
+(* Display proof term generated by previous tactic *)
+Show Environment 1

tests/lean/tactic3.lean.expected.out

@@ -0,0 +1,15 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: p
+  Assumed: q
+  Assumed: r
+  Proved: T1
+Theorem T1 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
+    Discharge
+        (λ H : p,
+           Discharge
+               (λ H::1 : p ∧ q,
+                  Discharge
+                      (λ H::2 : r,
+                         Conj (let H::1::2 := Conjunct2 H::1 in H::1::2)
+                              (Conj H::2 (let H::1::1 := Conjunct1 H::1 in H::1::1)))))