From 0c059a9917e25d1a771495d25b8e96f6fe7886fe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Dec 2013 20:00:20 -0800 Subject: [PATCH] feat(library/tactic): use _tac suffix instead of _tactic like Isabelle Signed-off-by: Leonardo de Moura --- src/library/tactic/apply_tactic.cpp | 2 +- src/library/tactic/boolean_tactics.cpp | 12 ++++---- src/library/tactic/tactic.cpp | 17 ++++++----- tests/lean/apply_tac1.lean | 8 +++--- tests/lean/disj1.lean | 14 ++++----- tests/lean/interactive/t1.lean | 12 ++++---- tests/lean/interactive/t1.lean.expected.out | 2 +- tests/lean/interactive/t2.lean | 6 ++-- tests/lean/interactive/t2.lean.expected.out | 2 +- tests/lean/interactive/t3.lean | 6 ++-- tests/lean/interactive/t5.lean | 2 +- tests/lean/interactive/t6.lean | 6 ++-- tests/lean/tactic1.lean | 2 +- tests/lean/tactic10.lean | 14 ++++----- tests/lean/tactic11.lean | 8 +++--- tests/lean/tactic12.lean | 14 ++++----- tests/lean/tactic2.lean | 10 +++---- tests/lean/tactic3.lean | 2 +- tests/lean/tactic4.lean | 2 +- tests/lean/tactic5.lean | 2 +- tests/lean/tactic6.lean | 32 ++++++++++----------- tests/lean/tactic8.lean | 10 +++---- tests/lean/tactic9.lean | 12 ++++---- tests/lua/tactic1.lua | 4 +-- 24 files changed, 100 insertions(+), 101 deletions(-) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 39cc3a18c..f674f981b 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/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"); } } diff --git a/src/library/tactic/boolean_tactics.cpp b/src/library/tactic/boolean_tactics.cpp index 1e842184e..08fdf63aa 100644 --- a/src/library/tactic/boolean_tactics.cpp +++ b/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"); } } diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 23f288371..16742afd9 100644 --- a/src/library/tactic/tactic.cpp +++ b/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 diff --git a/tests/lean/apply_tac1.lean b/tests/lean/apply_tac1.lean index c79a9908b..4473dd273 100644 --- a/tests/lean/apply_tac1.lean +++ b/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 diff --git a/tests/lean/disj1.lean b/tests/lean/disj1.lean index 9d8662e55..8b6f55a8a 100644 --- a/tests/lean/disj1.lean +++ b/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. diff --git a/tests/lean/interactive/t1.lean b/tests/lean/interactive/t1.lean index 941e49b9f..0934f8f2e 100644 --- a/tests/lean/interactive/t1.lean +++ b/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. diff --git a/tests/lean/interactive/t1.lean.expected.out b/tests/lean/interactive/t1.lean.expected.out index bc063c9b2..06f0b0a73 100644 --- a/tests/lean/interactive/t1.lean.expected.out +++ b/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' diff --git a/tests/lean/interactive/t2.lean b/tests/lean/interactive/t2.lean index 412e2cacc..544eb7dd6 100644 --- a/tests/lean/interactive/t2.lean +++ b/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. diff --git a/tests/lean/interactive/t2.lean.expected.out b/tests/lean/interactive/t2.lean.expected.out index b1fb4114f..25c2a63d6 100644 --- a/tests/lean/interactive/t2.lean.expected.out +++ b/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' diff --git a/tests/lean/interactive/t3.lean b/tests/lean/interactive/t3.lean index 37ca5de17..38152b7d3 100644 --- a/tests/lean/interactive/t3.lean +++ b/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. \ No newline at end of file diff --git a/tests/lean/interactive/t5.lean b/tests/lean/interactive/t5.lean index e25a4e163..f2b60881c 100644 --- a/tests/lean/interactive/t5.lean +++ b/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. \ No newline at end of file diff --git a/tests/lean/interactive/t6.lean b/tests/lean/interactive/t6.lean index b75744509..502ab937c 100644 --- a/tests/lean/interactive/t6.lean +++ b/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. diff --git a/tests/lean/tactic1.lean b/tests/lean/tactic1.lean index 7821b926e..553200448 100644 --- a/tests/lean/tactic1.lean +++ b/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) **) diff --git a/tests/lean/tactic10.lean b/tests/lean/tactic10.lean index a3fad3442..683eae5db 100644 --- a/tests/lean/tactic10.lean +++ b/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. diff --git a/tests/lean/tactic11.lean b/tests/lean/tactic11.lean index 7da506544..234f7022d 100644 --- a/tests/lean/tactic11.lean +++ 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. diff --git a/tests/lean/tactic12.lean b/tests/lean/tactic12.lean index eea54de00..19fd69918 100644 --- a/tests/lean/tactic12.lean +++ b/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. \ No newline at end of file diff --git a/tests/lean/tactic2.lean b/tests/lean/tactic2.lean index 8e8ead156..659ac5152 100644 --- a/tests/lean/tactic2.lean +++ b/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 \ No newline at end of file diff --git a/tests/lean/tactic3.lean b/tests/lean/tactic3.lean index 8d09e1efc..d439aa124 100644 --- a/tests/lean/tactic3.lean +++ b/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 *) diff --git a/tests/lean/tactic4.lean b/tests/lean/tactic4.lean index d897cf33c..28cb96071 100644 --- a/tests/lean/tactic4.lean +++ b/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 := _. diff --git a/tests/lean/tactic5.lean b/tests/lean/tactic5.lean index 5e0538385..09ffc63f9 100644 --- a/tests/lean/tactic5.lean +++ 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 := _. diff --git a/tests/lean/tactic6.lean b/tests/lean/tactic6.lean index 001c4e9d1..44a5a9874 100644 --- a/tests/lean/tactic6.lean +++ b/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 \ No newline at end of file diff --git a/tests/lean/tactic8.lean b/tests/lean/tactic8.lean index 37fb0357d..191d1dbb6 100644 --- a/tests/lean/tactic8.lean +++ b/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. \ No newline at end of file diff --git a/tests/lean/tactic9.lean b/tests/lean/tactic9.lean index 9d18c4643..a50e896a9 100644 --- a/tests/lean/tactic9.lean +++ b/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. \ No newline at end of file diff --git a/tests/lua/tactic1.lua b/tests/lua/tactic1.lua index 517dedeca..d6bff9cf9 100644 --- a/tests/lua/tactic1.lua +++ b/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