feat(library/tactic): use _tac suffix instead of _tactic like Isabelle

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

src/library/tactic/apply_tactic.cpp

@@ -149,6 +149,6 @@ int mk_apply_tactic(lua_State * L) {
 }
 
 void open_apply_tactic(lua_State * L) {
-    SET_GLOBAL_FUN(mk_apply_tactic,     "apply_tactic");
+    SET_GLOBAL_FUN(mk_apply_tactic,     "apply_tac");
 }
 }

src/library/tactic/boolean_tactics.cpp

@@ -387,11 +387,11 @@ static int mk_absurd_tactic(lua_State * L) {
 }
 
 void open_boolean_tactics(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");
-    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");
+    SET_GLOBAL_FUN(mk_conj_tactic,     "conj_tac");
+    SET_GLOBAL_FUN(mk_imp_tactic,      "imp_tac");
+    SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tac");
+    SET_GLOBAL_FUN(mk_disj_hyp_tactic, "disj_hyp_tac");
+    SET_GLOBAL_FUN(mk_disj_tactic,     "disj_tac");
+    SET_GLOBAL_FUN(mk_absurd_tactic,   "absurd_tac");
 }
 }

src/library/tactic/tactic.cpp

@@ -803,15 +803,14 @@ void open_tactic(lua_State * L) {
     setfuncs(L, tactic_m, 0);
 
     SET_GLOBAL_FUN(tactic_pred,           "is_tactic");
-    SET_GLOBAL_FUN(mk_trace_tactic,       "trace_tactic");
-    SET_GLOBAL_FUN(mk_id_tactic,          "id_tactic");
-    SET_GLOBAL_FUN(mk_now_tactic,         "now_tactic");
-    SET_GLOBAL_FUN(mk_fail_tactic,        "fail_tactic");
-    SET_GLOBAL_FUN(mk_trace_state_tactic, "show_tactic");
-    SET_GLOBAL_FUN(mk_assumption_tactic,  "assumption_tactic");
-    SET_GLOBAL_FUN(mk_assumption_tactic,  "assump_tactic");
-    SET_GLOBAL_FUN(mk_unfold_tactic,      "unfold_tactic");
-    SET_GLOBAL_FUN(mk_beta_tactic,        "beta_tactic");
+    SET_GLOBAL_FUN(mk_trace_tactic,       "trace_tac");
+    SET_GLOBAL_FUN(mk_id_tactic,          "id_tac");
+    SET_GLOBAL_FUN(mk_now_tactic,         "now_tac");
+    SET_GLOBAL_FUN(mk_fail_tactic,        "fail_tac");
+    SET_GLOBAL_FUN(mk_trace_state_tactic, "show_tac");
+    SET_GLOBAL_FUN(mk_assumption_tactic,  "assumption_tac");
+    SET_GLOBAL_FUN(mk_unfold_tactic,      "unfold_tac");
+    SET_GLOBAL_FUN(mk_beta_tactic,        "beta_tac");
     SET_GLOBAL_FUN(mk_lua_tactic01,       "tactic");
 
     // HOL-like tactic names

tests/lean/apply_tac1.lean

@@ -2,14 +2,14 @@ Variable f : Int -> Int -> Bool
 Variable P : Int -> Int -> Bool
 Axiom Ax1 (x y : Int) (H : P x y) : (f x y)
 Theorem T1 (a : Int) : (P a a) => (f a a).
-      apply imp_tactic
-      apply (** apply_tactic("Ax1") **)
-      apply assumption_tactic
+      apply (** imp_tac **)
+      apply (Ax1)
+      assumption
       done
 Variable b : Int
 Axiom Ax2 (x : Int) : (f x b)
 (**
-simple_tac = REPEAT(ORELSE(imp_tactic, assumption_tactic, apply_tactic("Ax2"), apply_tactic("Ax1")))
+simple_tac = REPEAT(ORELSE(imp_tac, assumption_tac, apply_tac("Ax2"), apply_tac("Ax1")))
 **)
 Theorem T2 (a : Int) : (P a a) => (f a a).
      apply simple_tac

tests/lean/disj1.lean

@@ -1,15 +1,15 @@
 Theorem T1 (a b : Bool) : a \/ b => b \/ a.
-    apply imp_tactic
-    apply disj_hyp_tactic
-    apply disj_tactic
+    apply imp_tac
+    apply disj_hyp_tac
+    apply disj_tac
     back
-    apply assumption_tactic
-    apply disj_tactic
-    apply assumption_tactic
+    apply assumption_tac
+    apply disj_tac
+    apply assumption_tac
     done
 
 (**
-simple_tac = REPEAT(ORELSE(imp_tactic, assumption_tactic, disj_hyp_tactic, disj_tactic)) .. now_tactic
+simple_tac = REPEAT(ORELSE(imp_tac, assumption_tac, disj_hyp_tac, disj_tac)) .. now_tac
 **)
 
 Theorem T2 (a b : Bool) : a \/ b => b \/ a.

tests/lean/interactive/t1.lean

@@ -1,12 +1,12 @@
 Theorem T2 (a b : Bool) : a => b => a /\ b.
 done.
 done.
-apply imp_tactic.
-apply imp_tactic2.
+apply imp_tac.
+apply imp_tac2.
 foo.
-apply imp_tactic.
-apply imp_tactic.
-apply conj_tactic.
+apply imp_tac.
+apply imp_tac.
+apply conj_tac.
 back.
-apply assumption_tactic.
+apply assumption_tac.
 done.

tests/lean/interactive/t1.lean.expected.out

@@ -11,7 +11,7 @@ Proof state:
 a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
 ## Proof state:
 H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
-## Error (line: 8, pos: 0) unknown tactic 'imp_tactic2'
+## Error (line: 8, pos: 0) unknown tactic 'imp_tac2'
 Proof state:
 H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
 ## Error (line: 9, pos: 0) invalid tactic command 'foo'

tests/lean/interactive/t2.lean

@@ -1,8 +1,8 @@
 Theorem T2 (a b : Bool) : a => b => a /\ b.
-apply imp_tactic.
-apply imp_tactic2.
+apply imp_tac.
+apply imp_tac2.
 foo.
-apply imp_tactic.
+apply imp_tac.
 abort.
 
 Variables a b : Bool.

tests/lean/interactive/t2.lean.expected.out

@@ -5,7 +5,7 @@ Proof state:
 a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
 ## Proof state:
 H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
-## Error (line: 6, pos: 0) unknown tactic 'imp_tactic2'
+## Error (line: 6, pos: 0) unknown tactic 'imp_tac2'
 Proof state:
 H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
 ## Error (line: 7, pos: 0) invalid tactic command 'foo'

tests/lean/interactive/t3.lean

@@ -1,9 +1,9 @@
 Theorem T2 (a b : Bool) : b => a \/ b.
-apply imp_tactic.
-apply disj_tactic.
+apply imp_tac.
+apply disj_tac.
 back.
 back.
-apply assumption_tactic.
+assumption.
 done.
 
 Show Environment 1.

tests/lean/interactive/t5.lean

@@ -1,7 +1,7 @@
 Axiom magic (a : Bool) : a.
 
 Theorem T (a : Bool) : a.
-    apply (** apply_tactic("magic") **).
+    apply (** apply_tac("magic") **).
     done.
 
 Show Environment 1.

tests/lean/interactive/t6.lean

@@ -1,6 +1,6 @@
 Theorem T1 (a b : Bool) : a => b => a /\ b.
-    apply imp_tactic.
-    apply imp_tactic.
+    apply imp_tac.
+    apply imp_tac.
     apply Conj.
-    apply assumption_tactic.
+    assumption.
     done.

tests/lean/tactic1.lean

@@ -3,7 +3,7 @@ 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 tac = REPEAT(conj_tac() ^ imp_tac() ^ assumption_tac())
  local proof = tac:solve(env, context(), conjecture)
  env:add_theorem("T1", conjecture, proof)
 **)

tests/lean/tactic10.lean

@@ -2,16 +2,16 @@ Definition f(a : Bool) : Bool := not a.
 Definition g(a b : Bool) : Bool := a \/ b.
 
 Theorem T1 (a b : Bool) : (g a b) => (f b) => a := _.
-     apply unfold_tactic
-     apply imp_tactic
-     apply imp_tactic
-     apply disj_hyp_tactic
-     apply assumption_tactic
-     apply absurd_tactic
+     apply unfold_tac
+     apply imp_tac
+     apply imp_tac
+     apply disj_hyp_tac
+     assumption
+     apply absurd_tac
      done.
 
 (**
-simple_tac   = REPEAT(unfold_tactic) .. REPEAT(ORELSE(imp_tactic, conj_hyp_tactic, assumption_tactic, absurd_tactic, conj_hyp_tactic, disj_hyp_tactic))
+simple_tac   = REPEAT(unfold_tac) .. REPEAT(ORELSE(imp_tac, conj_hyp_tac, assumption_tac, absurd_tac, conj_hyp_tac, disj_hyp_tac))
 **)
 
 Definition h(a b : Bool) : Bool := g a b.

tests/lean/tactic11.lean

@@ -1,6 +1,6 @@
 Theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a) := _ .
-   apply beta_tactic.
-   apply imp_tactic.
-   apply conj_hyp_tactic.
-   apply assumption_tactic.
+   apply beta_tac.
+   apply imp_tac.
+   apply conj_hyp_tac.
+   apply assumption_tac.
    done.

tests/lean/tactic12.lean

@@ -1,13 +1,13 @@
 Theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a).
-   apply beta_tactic.
-   apply imp_tactic.
-   apply conj_hyp_tactic.
-   apply assumption_tactic.
+   apply beta_tac.
+   apply imp_tac.
+   apply conj_hyp_tac.
+   apply assumption_tac.
    done.
 
 Variables p q : Bool.
 Theorem T2 : p /\ q => q.
-   apply imp_tactic.
-   apply conj_hyp_tactic.
-   apply assumption_tactic.
+   apply imp_tac.
+   apply conj_hyp_tac.
+   apply assumption_tac.
    done.

tests/lean/tactic2.lean

@@ -7,13 +7,13 @@ Theorem T1 : p => q => p /\ q :=
                 H2 : q := _
             in Conj H1 H2
          )).
-    apply assumption_tactic (* solve first metavar *)
+    assumption (* solve first metavar *)
     done
-    apply assumption_tactic (* solve second metavar *)
+    apply assumption_tac (* solve second metavar *)
     done
 
 (**
-simple_tac = REPEAT(imp_tactic() ^ conj_tactic() ^ assumption_tactic())
+simple_tac = REPEAT(imp_tac() ^ conj_tac() ^ assumption_tac())
 **)
 
 Theorem T2 : p => q => p /\ q /\ p := _.
@@ -23,8 +23,8 @@ Theorem T2 : p => q => p /\ q /\ p := _.
 Show Environment 1
 
 Theorem T3 : p => p /\ q => r => q /\ r /\ p := _.
-    apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
+    apply (** REPEAT(ORELSE(imp_tac, conj_tac, conj_hyp_tac, assumption_tac)) **)
     done
 
-(* Display proof term generated by previous tactic *)
+(* Display proof term generated by previous tac *)
 Show Environment 1

tests/lean/tactic3.lean

@@ -1,7 +1,7 @@
 Variables p q r : Bool
 
 Theorem T1 : p => p /\ q => r => q /\ r /\ p := _.
-    apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
+    apply (** REPEAT(ORELSE(imp_tac, conj_tac, conj_hyp_tac, assumption_tac)) **)
     done
 
 (* Display proof term generated by previous tactic *)

tests/lean/tactic4.lean

@@ -1,5 +1,5 @@
 (**
-simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic()
+simple_tac = REPEAT(ORELSE(imp_tac(), conj_tac())) .. assumption_tac()
 **)
 
 Theorem T4 (a b : Bool) : a => b => a /\ b := _.

tests/lean/tactic5.lean

@@ -1,5 +1,5 @@
 (**
-simple_tac = REPEAT(ORELSE(imp_tactic, conj_tactic)) .. assumption_tactic
+simple_tac = REPEAT(ORELSE(imp_tac, conj_tac)) .. assumption_tac
 **)
 
 Theorem T4 (a b : Bool) : a => b => a /\ b /\ a := _.

tests/lean/tactic6.lean

@@ -1,21 +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
+   apply imp_tac
+   apply imp_tac
+   apply conj_hyp_tac
+   apply conj_tac
+   apply (** FOCUS(THEN(show_tac, conj_tac, show_tac, assumption_tac), 2) **)
+   apply assumption_tac
    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) **)
+   apply imp_tac
+   apply imp_tac
+   apply conj_hyp_tac
+   apply conj_tac
+   apply show_tac
+   apply (** FOCUS(THEN(show_tac, conj_tac, FOCUS(assumption_tac, 1)), 2) **)
+   apply show_tac
+   apply (** FOCUS(assumption_tac, 1) **)
+   apply show_tac
+   apply (** FOCUS(assumption_tac, 1) **)
    done

tests/lean/tactic8.lean

@@ -1,8 +1,8 @@
 Theorem T (a b : Bool) : a \/ b => (not b) => a := _.
-     apply imp_tactic
-     apply imp_tactic
-     apply disj_hyp_tactic
-     apply assumption_tactic
-     apply absurd_tactic
+     apply imp_tac
+     apply imp_tac
+     apply disj_hyp_tac
+     apply assumption_tac
+     apply absurd_tac
      done
 Show Environment 1.

tests/lean/tactic9.lean

@@ -1,11 +1,11 @@
 Definition f(a : Bool) : Bool := not a.
 
 Theorem T (a b : Bool) : a \/ b => (f b) => a := _.
-     apply imp_tactic
-     apply imp_tactic
-     apply disj_hyp_tactic
-     apply (** unfold_tactic("f") **)
-     apply assumption_tactic
-     apply absurd_tactic
+     apply imp_tac
+     apply imp_tac
+     apply disj_hyp_tac
+     apply (** unfold_tac("f") **)
+     apply assumption_tac
+     apply absurd_tac
      done
 Show Environment 1.

tests/lua/tactic1.lua

@@ -14,7 +14,7 @@ local ltac = tactic(function(env, ios, s)
                        print("FIRST tactic in Lua, current state: " .. tostring(s));
                        return s
 end)
-local t = (trace_tactic("hello") .. trace_tactic("world")) + (trace_tactic("again") .. ltac .. assumption_tactic())
+local t = (trace_tac("hello") .. trace_tac("world")) + (trace_tac("again") .. ltac .. assumption_tac())
 for s in t(env, ios, ps) do
    if s:is_proof_final_state() then
       local m = proof_map()
@@ -29,7 +29,7 @@ print(t:solve(env, ios, ps))
 print(t:solve(env, ios, ctx, p))
 assert(t:solve(env, ios, ps) == Var(1))
 assert(t:solve(env, ios, ctx, q) == Var(0))
-local t2 = id_tactic() + id_tactic() + id_tactic()
+local t2 = id_tac() + id_tac() + id_tac()
 local r  = t2:solve(env, ios, ps)
 assert(#r == 3)
 for i, out_state in ipairs(r) do