michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-26 15:54:53 -08:00
parent ef18cc4a92
commit f1b97b18b4
47 changed files with 360 additions and 299 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
examples/lean/tactic1.lean
View file

@ -4,8 +4,14 @@ This example demonstrates how to specify a proof skeleton that contains
*)
(**
-- Import useful macros for creating tactics
import("tactic.lua")
-- Define a simple tactic using Lua
auto = REPEAT(ORELSE(assumption_tac, conj_tac, conj_hyp_tac))
auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
conj_hyp = conj_hyp_tac()
conj = conj_tac()
**)
(*
@ -35,9 +41,9 @@ Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
in _. (* third hole *)
apply auto. done. (* tactic command sequence for the first hole *)
apply auto. done. (* tactic command sequence for the second hole *)
apply auto. done. (* tactic command sequence for the third hole *)
auto. done. (* tactic command sequence for the first hole *)
auto. done. (* tactic command sequence for the second hole *)
auto. done. (* tactic command sequence for the third hole *)
(*
In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics.
@ -47,9 +53,9 @@ Theorem T3 (A B : Bool) : A /\ B -> B /\ A :=
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
in _. (* third hole *)
apply conj_hyp_tac. apply assumption_tac. done. (* tactic command sequence for the first hole *)
apply conj_hyp_tac. apply assumption_tac. done. (* tactic command sequence for the second hole *)
apply conj_tac. apply assumption_tac. done. (* tactic command sequence for the third hole *)
conj_hyp. exact. done. (* tactic command sequence for the first hole *)
conj_hyp. exact. done. (* tactic command sequence for the second hole *)
conj. exact. done. (* tactic command sequence for the third hole *)
(*
We can also mix the two styles (hints and command sequences)
@ -59,7 +65,5 @@ Theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
in (show B /\ A by auto).
apply conj_hyp_tac. apply assumption_tac. done. (* tactic command sequence for the first hole *)
apply conj_hyp_tac. apply assumption_tac. done. (* tactic command sequence for the second hole *)
auto. done. (* tactic command sequence for the first hole *)
auto. done. (* tactic command sequence for the second hole *)

2
examples/lean/tactic_in_lua.lean
View file

@ -65,7 +65,7 @@
**)
Theorem T (a b : Bool) : a => b => a /\ b := _.
apply (** THEN(REPEAT(ORELSE(imp_tac, conj_in_lua)), assumption_tac) **)
(** Then(Repeat(OrElse(imp_tac(), conj_in_lua)), assumption_tac()) **)
done
(* Show proof created using our script *)

18
src/extra/tactic.lua Normal file
View file

@ -0,0 +1,18 @@
-- Define macros for simplifying Tactic creation
local unary_combinator = function (name, fn) tactic_macro(name, { macro_arg.Tactic }, function (env, t) return fn(t) end) end
local nary_combinator = function (name, fn) tactic_macro(name, { macro_arg.Tactics }, function (env, ts) return fn(unpack(ts)) end) end
local const_tactic = function (name, fn) tactic_macro(name, {}, function (env) return fn() end) end
unary_combinator("Repeat", Repeat)
unary_combinator("Try", Try)
nary_combinator("Then", Then)
nary_combinator("OrElse", OrElse)
const_tactic("exact", assumption_tac)
const_tactic("trivial", trivial_tac)
const_tactic("absurd", absurd_tac)
const_tactic("conj_hyp", conj_hyp_tac)
const_tactic("disj_hyp", disj_hyp_tac)
const_tactic("unfold_all", unfold_tac)
const_tactic("beta", beta_tac)
tactic_macro("apply", { macro_arg.Expr }, function (env, e) return apply_tac(e) end)
tactic_macro("unfold", { macro_arg.Id }, function (env, id) return unfold_tac(id) end)

139
src/frontends/lean/parser.cpp
View file

@ -131,7 +131,7 @@ static unsigned g_level_cup_prec = 5;
// are syntax sugar for (Pi (_ : A), B)
static name g_unused = name::mk_internal_unique_name();
enum class macro_arg_kind { Expr, Exprs, Bindings, Id, String, Comma, Assign, Tactic };
enum class macro_arg_kind { Expr, Exprs, Bindings, Id, String, Comma, Assign, Tactic, Tactics };
struct macro {
list<macro_arg_kind> m_arg_kinds;
luaref m_fn;
@ -140,6 +140,7 @@ struct macro {
};
typedef name_map<macro> macros;
macros & get_expr_macros(lua_State * L);
macros & get_tactic_macros(lua_State * L);
macros & get_cmd_macros(lua_State * L);
static char g_set_parser_key;
@ -207,6 +208,7 @@ class parser::imp {
frontend_elaborator m_elaborator;
macros const * m_expr_macros;
macros const * m_cmd_macros;
macros const * m_tactic_macros;
scanner::token m_curr;
bool m_use_exceptions;
bool m_interactive;
@ -966,6 +968,13 @@ class parser::imp {
}
}
bool is_curr_begin_tactic() const {
switch (curr()) {
case scanner::token::LeftParen: case scanner::token::Id: return true;
default: return false;
}
}
typedef buffer<std::pair<macro_arg_kind, void*>> macro_arg_stack;
struct macro_result {
optional<expr> m_expr;
@ -1024,6 +1033,14 @@ class parser::imp {
tactic t = parse_tactic_expr();
args.emplace_back(k, &t);
return parse_macro(tail(arg_kinds), fn, prec, args, p);
}
case macro_arg_kind::Tactics: {
buffer<tactic> tactics;
while (is_curr_begin_tactic()) {
tactics.push_back(parse_tactic_expr());
}
args.emplace_back(k, &tactics);
return parse_macro(tail(arg_kinds), fn, prec, args, p);
}}
lean_unreachable();
} else {
@ -1074,6 +1091,17 @@ class parser::imp {
case macro_arg_kind::Tactic:
push_tactic(L, *static_cast<tactic*>(arg));
break;
case macro_arg_kind::Tactics: {
auto const & tactics = *static_cast<buffer<tactic>*>(arg);
lua_newtable(L);
int i = 1;
for (auto t : tactics) {
push_tactic(L, t);
lua_rawseti(L, -2, i);
i = i + 1;
}
break;
}
default:
lean_unreachable();
}
@ -1461,6 +1489,20 @@ class parser::imp {
return save(mk_placeholder(), p);
}
tactic parse_tactic_macro(name tac_id, pos_info const & p) {
lean_assert(m_tactic_macros && m_tactic_macros->find(tac_id) != m_tactic_macros->end());
next();
auto m = m_tactic_macros->find(tac_id)->second;
macro_arg_stack args;
flet<bool> set(m_check_identifiers, false);
auto r = parse_macro(m.m_arg_kinds, m.m_fn, m.m_precedence, args, p);
if (r.m_tactic) {
return *(r.m_tactic);
} else {
throw parser_error("failed to execute macro, unexpected result type, a tactic was expected", p);
}
}
/** \brief Parse a tactic expression, it can be
1) A Lua Script Block expression that returns a tactic
@ -1473,35 +1515,35 @@ class parser::imp {
parse_script_expr();
return using_script([&](lua_State * L) {
try {
return to_tactic_ext(L, -1);
return to_tactic(L, -1);
} catch (...) {
throw parser_error("invalid script-block, it must return a tactic", p);
}
});
} else if (curr_is_identifier() && m_tactic_macros && m_tactic_macros->find(curr_name()) != m_tactic_macros->end()) {
return parse_tactic_macro(curr_name(), p);
} else if (curr_is_lparen()) {
next();
flet<bool> set(m_check_identifiers, false);
expr pr = parse_expr();
check_rparen_next("invalid apply command, ')' expected");
return ::lean::apply_tactic(pr);
tactic r = parse_tactic_expr();
check_rparen_next("invalid tactic, ')' expected");
return r;
} else {
name n = check_identifier_next("invalid apply command, identifier, '(' expr ')', or 'script-block' expected");
optional<object> o = m_env->find_object(n);
if (o && (o->is_theorem() || o->is_axiom())) {
return ::lean::apply_tactic(n);
} else {
return using_script([&](lua_State * L) {
lua_getglobal(L, n.to_string().c_str());
try {
tactic t = to_tactic_ext(L, -1);
name n = check_identifier_next("invalid tactic, identifier, tactic macro, '(', or 'script-block' expected");
return using_script([&](lua_State * L) {
lua_getglobal(L, n.to_string().c_str());
try {
if (is_tactic(L, -1)) {
tactic t = to_tactic(L, -1);
lua_pop(L, 1);
return t;
} catch (...) {
lua_pop(L, 1);
throw parser_error(sstream() << "unknown tactic '" << n << "'", p);
} else {
throw parser_error(sstream() << "invalid tactic, '" << n << "' is not a tactic in script environment", p);
}
});
}
} catch (...) {
lua_pop(L, 1);
throw parser_error(sstream() << "unknown tactic '" << n << "'", p);
}
});
}
}
@ -1734,34 +1776,21 @@ class parser::imp {
}
/**
\brief Execute the <tt>apply [tactic]</tt> tactic command.
\brief Execute the tactic.
This command just applies the tactic to the input state \c s.
If it succeeds, \c s is assigned to the head of the output
state sequence produced by the tactic. The rest/tail of the
output state sequence is stored on the top of the stack \c
stack.
*/
void apply_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s) {
void tactic_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s) {
auto tac_pos = pos();
next();
tactic t = parse_tactic_expr();
auto r = apply_tactic(s, t, tac_pos);
s = r.first;
stack.push_back(r.second);
}
/**
\brief Execute the \c assumption tactic command. This command
is just syntax sugar for <tt>apply assumption_tac</tt>.
*/
void assumption_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s) {
auto tac_pos = pos();
next();
auto r = apply_tactic(s, assumption_tactic(), tac_pos);
s = r.first;
stack.push_back(r.second);
}
/**
\brief Execute the \c done tactic command. It succeeds if
a proof for \c s can be built.
@ -1799,9 +1828,7 @@ class parser::imp {
break;
case scanner::token::Id:
id = curr_name();
if (id == g_apply) {
apply_cmd(stack, s);
} else if (id == g_back) {
if (id == g_back) {
back_cmd(stack, s);
} else if (id == g_done) {
pr = done_cmd(s, ctx, expected_type);
@ -1810,13 +1837,13 @@ class parser::imp {
} else if (id == g_abort) {
next();
st = status::Abort;
} else if (id == g_assumption) {
assumption_cmd(stack, s);
} else {
next();
throw tactic_cmd_error(sstream() << "invalid tactic command '" << id << "'", p, s);
tactic_cmd(stack, s);
}
break;
case scanner::token::ScriptBlock:
tactic_cmd(stack, s);
break;
case scanner::token::CommandId:
st = status::Abort;
break;
@ -2552,15 +2579,17 @@ public:
m_scanner.set_command_keywords(g_command_keywords);
if (m_script_state) {
m_script_state->apply([&](lua_State * L) {
m_expr_macros = &get_expr_macros(L);
m_cmd_macros = &get_cmd_macros(L);
m_expr_macros = &get_expr_macros(L);
m_tactic_macros = &get_tactic_macros(L);
m_cmd_macros = &get_cmd_macros(L);
for (auto const & p : *m_cmd_macros) {
m_scanner.add_command_keyword(p.first);
}
});
} else {
m_expr_macros = nullptr;
m_cmd_macros = nullptr;
m_expr_macros = nullptr;
m_tactic_macros = nullptr;
m_cmd_macros = nullptr;
}
scan();
}
@ -2753,6 +2782,7 @@ expr parse_expr(environment const & env, io_state & ios, std::istream & in, scri
}
static char g_parser_expr_macros_key;
static char g_parser_tactic_macros_key;
static char g_parser_cmd_macros_key;
DECL_UDATA(macros)
@ -2773,13 +2803,9 @@ macros & get_macros(lua_State * L, char * key) {
return r;
}
macros & get_expr_macros(lua_State * L) {
return get_macros(L, &g_parser_expr_macros_key);
}
macros & get_cmd_macros(lua_State * L) {
return get_macros(L, &g_parser_cmd_macros_key);
}
macros & get_expr_macros(lua_State * L) { return get_macros(L, &g_parser_expr_macros_key); }
macros & get_tactic_macros(lua_State * L) { return get_macros(L, &g_parser_tactic_macros_key); }
macros & get_cmd_macros(lua_State * L) { return get_macros(L, &g_parser_cmd_macros_key); }
void mk_macro(lua_State * L, macros & mtable) {
int nargs = lua_gettop(L);
@ -2816,6 +2842,11 @@ int mk_cmd_macro(lua_State * L) {
return 0;
}
int mk_tactic_macro(lua_State * L) {
mk_macro(L, get_tactic_macros(L));
return 0;
}
static const struct luaL_Reg macros_m[] = {
{"__gc", macros_gc}, // never throws
{0, 0}
@ -2829,6 +2860,7 @@ void open_macros(lua_State * L) {
SET_GLOBAL_FUN(macros_pred, "is_macros");
SET_GLOBAL_FUN(mk_macro, "macro");
SET_GLOBAL_FUN(mk_cmd_macro, "cmd_macro");
SET_GLOBAL_FUN(mk_tactic_macro, "tactic_macro");
lua_newtable(L);
SET_ENUM("Expr", macro_arg_kind::Expr);
@ -2839,6 +2871,7 @@ void open_macros(lua_State * L) {
SET_ENUM("Comma", macro_arg_kind::Comma);
SET_ENUM("Assign", macro_arg_kind::Assign);
SET_ENUM("Tactic", macro_arg_kind::Tactic);
SET_ENUM("Tactics", macro_arg_kind::Tactics);
lua_setglobal(L, "macro_arg");
}
}

109
src/library/tactic/tactic.cpp
View file

@ -545,35 +545,6 @@ DECL_UDATA(tactic)
throw exception(sstream() << "arg #" << i << " must be a tactic or a function that returns a tactic");
}
/**
\brief We allow functions (that return tactics) to be used where a tactic
is expected. The idea is to be able to write
ORELSE(assumption_tactic, conj_tactic)
instead of
ORELSE(assumption_tactic(), conj_tactic())
*/
tactic to_tactic_ext(lua_State * L, int i) {
if (is_tactic(L, i)) {
return to_tactic(L, i);
} else if (lua_isfunction(L, i)) {
try {
lua_pushvalue(L, i);
pcall(L, 0, 1, 0);
} catch (...) {
throw_tactic_expected(i);
}
if (is_tactic(L, -1)) {
tactic t = to_tactic(L, -1);
lua_pop(L, 1);
return t;
} else {
throw_tactic_expected(i);
}
} else {
throw_tactic_expected(i);
}
}
static void check_ios(io_state * ios) {
if (!ios)
throw exception("failed to invoke tactic, io_state is not available");
@ -590,7 +561,7 @@ static int tactic_call_core(lua_State * L, tactic t, ro_environment env, io_stat
static int tactic_call(lua_State * L) {
int nargs = lua_gettop(L);
tactic t = to_tactic_ext(L, 1);
tactic t = to_tactic(L, 1);
ro_shared_environment env(L, 2);
if (nargs == 3) {
io_state * ios = get_io_state(L);
@ -608,36 +579,36 @@ 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_ext(L, 1), to_tactic_ext(L, 2));
tactic r = F(to_tactic(L, 1), to_tactic(L, 2));
for (int i = 3; i <= nargs; i++)
r = F(r, to_tactic_ext(L, 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_ext(L, 1), to_tactic_ext(L, 2))); }
static int tactic_orelse(lua_State * L) { return push_tactic(L, orelse(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
static int tactic_append(lua_State * L) { return push_tactic(L, append(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
static int tactic_interleave(lua_State * L) { return push_tactic(L, interleave(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
static int tactic_par(lua_State * L) { return push_tactic(L, par(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
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_ext(L, 1))); }
static int tactic_repeat1(lua_State * L) { return push_tactic(L, repeat1(to_tactic_ext(L, 1))); }
static int tactic_repeat_at_most(lua_State * L) { return push_tactic(L, repeat_at_most(to_tactic_ext(L, 1), luaL_checkinteger(L, 2))); }
static int tactic_take(lua_State * L) { return push_tactic(L, take(to_tactic_ext(L, 1), luaL_checkinteger(L, 2))); }
static int tactic_determ(lua_State * L) { return push_tactic(L, determ(to_tactic_ext(L, 1))); }
static int tactic_suppress_trace(lua_State * L) { return push_tactic(L, suppress_trace(to_tactic_ext(L, 1))); }
static int tactic_try_for(lua_State * L) { return push_tactic(L, try_for(to_tactic_ext(L, 1), luaL_checkinteger(L, 2))); }
static int tactic_using_params(lua_State * L) { return push_tactic(L, using_params(to_tactic_ext(L, 1), to_options(L, 2))); }
static int tactic_try(lua_State * L) { return push_tactic(L, orelse(to_tactic_ext(L, 1), id_tactic())); }
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))); }
static int tactic_take(lua_State * L) { return push_tactic(L, take(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
static int tactic_determ(lua_State * L) { return push_tactic(L, determ(to_tactic(L, 1))); }
static int tactic_suppress_trace(lua_State * L) { return push_tactic(L, suppress_trace(to_tactic(L, 1))); }
static int tactic_try_for(lua_State * L) { return push_tactic(L, try_for(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
static int tactic_using_params(lua_State * L) { return push_tactic(L, using_params(to_tactic(L, 1), to_options(L, 2))); }
static int tactic_try(lua_State * L) { return push_tactic(L, orelse(to_tactic(L, 1), id_tactic())); }
static int tactic_focus(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 1)
return push_tactic(L, focus(to_tactic_ext(L, 1)));
return push_tactic(L, focus(to_tactic(L, 1)));
else if (lua_isnumber(L, 2))
return push_tactic(L, focus(to_tactic_ext(L, 1), lua_tointeger(L, 2)));
return push_tactic(L, focus(to_tactic(L, 1), lua_tointeger(L, 2)));
else
return push_tactic(L, focus(to_tactic_ext(L, 1), to_name_ext(L, 2)));
return push_tactic(L, focus(to_tactic(L, 1), to_name_ext(L, 2)));
}
static int push_solve_result(lua_State * L, solve_result const & r) {
@ -677,7 +648,7 @@ static int tactic_solve_core(lua_State * L, tactic t, ro_environment env, io_sta
static int tactic_solve(lua_State * L) {
int nargs = lua_gettop(L);
tactic t = to_tactic_ext(L, 1);
tactic t = to_tactic(L, 1);
ro_shared_environment env(L, 2);
if (nargs == 3) {
io_state * ios = get_io_state(L);
@ -767,11 +738,11 @@ static int mk_lua_cond_tactic(lua_State * L, tactic t1, tactic t2) {
}
static int mk_lua_cond_tactic(lua_State * L) {
return mk_lua_cond_tactic(L, to_tactic_ext(L, 2), to_tactic_ext(L, 3));
return mk_lua_cond_tactic(L, to_tactic(L, 2), to_tactic(L, 3));
}
static int mk_lua_when_tactic(lua_State * L) {
return mk_lua_cond_tactic(L, to_tactic_ext(L, 2), id_tactic());
return mk_lua_cond_tactic(L, to_tactic(L, 2), id_tactic());
}
static int mk_id_tactic(lua_State * L) { return push_tactic(L, id_tactic()); }
@ -856,22 +827,22 @@ void open_tactic(lua_State * L) {
SET_GLOBAL_FUN(mk_lua_tactic01, "tactic");
// HOL-like tactic names
SET_GLOBAL_FUN(nary_tactic<then>, "THEN");
SET_GLOBAL_FUN(nary_tactic<orelse>, "ORELSE");
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(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_using_params, "USING");
SET_GLOBAL_FUN(tactic_using_params, "USING_PARAMS");
SET_GLOBAL_FUN(tactic_determ, "DETERM");
SET_GLOBAL_FUN(tactic_focus, "FOCUS");
SET_GLOBAL_FUN(nary_tactic<then>, "Then");
SET_GLOBAL_FUN(nary_tactic<orelse>, "OrElse");
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, "RepeatAtMost");
SET_GLOBAL_FUN(tactic_repeat1, "Repeat1");
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, "TryFor");
SET_GLOBAL_FUN(tactic_take, "Take");
SET_GLOBAL_FUN(tactic_using_params, "Using");
SET_GLOBAL_FUN(tactic_using_params, "UsingParams");
SET_GLOBAL_FUN(tactic_determ, "Determ");
SET_GLOBAL_FUN(tactic_focus, "Focus");
}
}

1
src/library/tactic/tactic.h
View file

@ -312,6 +312,5 @@ tactic normalize_tactic(bool unfold_opaque = false, bool all = true);
UDATA_DEFS_CORE(proof_state_seq)
UDATA_DEFS(tactic);
tactic to_tactic_ext(lua_State * L, int i);
void open_tactic(lua_State * L);
}

22
tests/lean/apply_tac1.lean
View file

@ -1,18 +1,24 @@
(** import("tactic.lua") **)
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_tac **)
apply (Ax1)
assumption
done
apply Discharge.
apply Ax1.
exact.
done.
Variable b : Int
Axiom Ax2 (x : Int) : (f x b)
(**
simple_tac = REPEAT(ORELSE(imp_tac, assumption_tac, apply_tac("Ax2"), apply_tac("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
done
simple_tac.
done.
Show Environment 1.
Theorem T3 (a : Int) : (P a a) => (f a a).
Repeat (OrElse (apply Discharge) exact (apply Ax2) (apply Ax1)).
done.
Show Environment 2.

2
tests/lean/apply_tac1.lean.expected.out
View file

@ -7,4 +7,6 @@
Assumed: b
Assumed: Ax2
Proved: T2
Proved: T3
Theorem T2 (a : ℤ) : P a a ⇒ f a a := Discharge (λ H : P a a, Ax1 a a H)
Theorem T3 (a : ℤ) : P a a ⇒ f a a := Discharge (λ H : P a a, Ax1 a a H)

3
tests/lean/apply_tac2.lean
View file

@ -1,7 +1,8 @@
(** import("tactic.lua") **)
Check @Discharge
Theorem T (a b : Bool) : a => b => b => a.
apply Discharge.
apply Discharge.
apply Discharge.
assumption.
exact.
done.

3
tests/lean/discharge.lean
View file

@ -1,7 +1,8 @@
(** import("tactic.lua") **)
Check @Discharge
Theorem T (a b : Bool) : a => b => b => a.
apply Discharge.
apply Discharge.
apply Discharge.
assumption.
exact.
done.

22
tests/lean/disj1.lean
View file

@ -1,19 +1,21 @@
(** import("tactic.lua") **)
Theorem T1 (a b : Bool) : a \/ b => b \/ a.
apply imp_tac
apply disj_hyp_tac
apply disj_tac
apply Discharge.
(** disj_hyp_tac() **)
(** disj_tac() **)
back
apply assumption_tac
apply disj_tac
apply assumption_tac
done
exact.
(** disj_tac() **)
exact.
done.
(**
simple_tac = REPEAT(ORELSE(imp_tac, assumption_tac, disj_hyp_tac, disj_tac)) .. now_tac
simple_tac = Repeat(OrElse(imp_tac(), assumption_tac(), disj_hyp_tac(), disj_tac())) .. now_tac()
**)
Theorem T2 (a b : Bool) : a \/ b => b \/ a.
apply simple_tac
done
simple_tac.
done.
Show Environment 1.

5
tests/lean/disjcases.lean
View file

@ -1,10 +1,11 @@
(** import("tactic.lua") **)
Variables a b c : Bool
Axiom H : a \/ b
Theorem T (a b : Bool) : a \/ b => b \/ a.
apply Discharge.
apply (DisjCases H).
apply Disj2.
assumption.
exact.
apply Disj1.
assumption.
exact.
done.

12
tests/lean/interactive/t1.lean
View file

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

6
tests/lean/interactive/t1.lean.expected.out
View file

@ -10,10 +10,8 @@ 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: 6) unknown tactic 'imp_tac2'
## Error (line: 9, pos: 0) invalid tactic command 'foo'
Proof state:
H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
## Error (line: 8, pos: 0) unknown tactic 'imp_tac2'
## Error (line: 9, pos: 0) unknown tactic 'foo'
## Proof state:
H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
## Error (line: 11, pos: 0) tactic failed

8
tests/lean/interactive/t10.lean
View file

@ -1,5 +1,5 @@
(**
simple_tac = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
**)
Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
@ -8,8 +8,8 @@ Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
H2 : B := _,
main : B /\ A := _
in main).
apply simple_tac. done.
apply simple2_tac. done.
apply simple_tac. done.
simple_tac. done.
simple2_tac. done.
simple_tac. done.
Echo "echo command after failure"

4
tests/lean/interactive/t10.lean.expected.out
View file

@ -6,8 +6,8 @@ A : Bool, B : Bool, H : A ∧ B ⊢ A
no goals
## Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
## Error (line: 15, pos: 9) unknown tactic 'simple2_tac'
## Error (line: 15, pos: 22) invalid 'done' command, proof cannot be produced from this state
## Error (line: 15, pos: 3) unknown tactic 'simple2_tac'
## Error (line: 15, pos: 16) invalid 'done' command, proof cannot be produced from this state
Proof state:
A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
## Proof state:

9
tests/lean/interactive/t11.lean
View file

@ -1,5 +1,5 @@
(**
auto = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
auto = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
**)
Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
@ -8,7 +8,6 @@ Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
lemma2 : B := _,
conclusion : B /\ A := _
in conclusion.
apply auto. done.
apply auto. done.
apply auto. done.
auto. done.
auto. done.
auto. done.

21
tests/lean/interactive/t12.lean
View file

@ -1,6 +1,7 @@
(**
import("tactic.lua")
-- Define a simple tactic using Lua
auto = REPEAT(ORELSE(assumption_tac, conj_tac, conj_hyp_tac))
auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
**)
(*
@ -30,9 +31,9 @@ Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
in _. (* third hole *)
apply auto. done. (* tactic command sequence for the first hole *)
apply auto. done. (* tactic command sequence for the second hole *)
apply auto. done. (* tactic command sequence for the third hole *)
auto. done. (* tactic command sequence for the first hole *)
auto. done. (* tactic command sequence for the second hole *)
auto. done. (* tactic command sequence for the third hole *)
(*
In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics.
@ -42,9 +43,9 @@ Theorem T3 (A B : Bool) : A /\ B -> B /\ A :=
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
in _. (* third hole *)
apply conj_hyp_tac. apply assumption_tac. done. (* tactic command sequence for the first hole *)
apply conj_hyp_tac. apply assumption_tac. done. (* tactic command sequence for the second hole *)
apply conj_tac. apply assumption_tac. done. (* tactic command sequence for the third hole *)
conj_hyp. exact. done. (* tactic command sequence for the first hole *)
conj_hyp. exact. done. (* tactic command sequence for the second hole *)
apply Conj. exact. done. (* tactic command sequence for the third hole *)
(*
We can also mix the two styles (hints and command sequences)
@ -54,7 +55,5 @@ Theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
in (show B /\ A by auto).
apply conj_hyp_tac. apply assumption_tac. done. (* tactic command sequence for the first hole *)
apply conj_hyp_tac. apply assumption_tac. done. (* tactic command sequence for the second hole *)
conj_hyp. exact. done. (* tactic command sequence for the first hole *)
conj_hyp. exact. done. (* tactic command sequence for the second hole *)

2
tests/lean/interactive/t13.lean
View file

@ -1,6 +1,6 @@
(**
-- Define a simple tactic using Lua
auto = REPEAT(ORELSE(assumption_tac, conj_tac, conj_hyp_tac))
auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
**)
Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=

6
tests/lean/interactive/t2.lean
View file

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

9
tests/lean/interactive/t2.lean.expected.out
View file

@ -2,14 +2,7 @@
Set: pp::unicode
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: 6) unknown tactic 'imp_tac2'
## Error (line: 7, pos: 0) invalid tactic command 'foo'
Proof state:
H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
## Proof state:
H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
## Error (line: 6, pos: 0) executing external script ([string "return imp_tac2() "]:1), attempt to call global 'imp_tac2' (a nil value)
## Error (line: 9, pos: 5) failed to prove theorem, proof has been aborted
Proof state:
H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b

8
tests/lean/interactive/t3.lean
View file

@ -1,9 +1,11 @@
(** import("tactic.lua") **)
Theorem T2 (a b : Bool) : b => a \/ b.
apply imp_tac.
apply disj_tac.
(** imp_tac() **).
(** disj_tac() **).
back.
back.
assumption.
exact.
done.
Show Environment 1.

2
tests/lean/interactive/t3.lean.expected.out
View file

@ -8,7 +8,7 @@ H : b, a : Bool, b : Bool ⊢ a ∨ b
H : b, a : Bool, b : Bool ⊢ a
## Proof state:
H : b, a : Bool, b : Bool ⊢ b
## Error (line: 8, pos: 0) failed to backtrack
## Error (line: 10, pos: 0) failed to backtrack
Proof state:
H : b, a : Bool, b : Bool ⊢ b
## Proof state:

3
tests/lean/interactive/t5.lean
View file

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

7
tests/lean/interactive/t6.lean
View file

@ -1,6 +1,7 @@
(** import("tactic.lua") **)
Theorem T1 (a b : Bool) : a => b => a /\ b.
apply imp_tac.
apply imp_tac.
(** imp_tac() **).
(** imp_tac() **).
apply Conj.
assumption.
exact.
done.

5
tests/lean/interactive/t7.lean
View file

@ -1,9 +1,10 @@
(** import("tactic.lua") **)
Variable q : Int -> Int -> Bool.
Variable p : Int -> Bool.
Axiom Ax (a b : Int) (H : q a b) : p b.
Variable a : Int.
Theorem T (x : Int) : (q a x) => (p x).
apply imp_tac.
(** imp_tac() **).
apply (Ax a).
assumption.
exact.
done.

5
tests/lean/interactive/t8.lean
View file

@ -1,6 +1,7 @@
(** import("tactic.lua") **)
SetOption tactic::proof_state::goal_names true.
Theorem T (a : Bool) : a => a /\ a.
apply imp_tac.
apply Discharge.
apply Conj.
assumption.
exact.
done.

6
tests/lean/interactive/t8.lean.expected.out
View file

@ -4,10 +4,10 @@
# Proof state:
main: a : Bool ⊢ a ⇒ a ∧ a
## Proof state:
main: H : a, a : Bool ⊢ a ∧ a
main::1: H : a, a : Bool ⊢ a ∧ a
## Proof state:
main::1: H : a, a : Bool ⊢ a
main::2: H : a, a : Bool ⊢ a
main::1::1: H : a, a : Bool ⊢ a
main::1::2: H : a, a : Bool ⊢ a
## Proof state:
no goals
## Proved: T

19
tests/lean/interactive/t9.lean
View file

@ -1,3 +1,4 @@
(** import("tactic.lua") **)
Theorem T1 (A B : Bool) : A /\ B => B /\ A :=
Discharge (fun H : A /\ B,
let main : B /\ A :=
@ -5,18 +6,18 @@ Theorem T1 (A B : Bool) : A /\ B => B /\ A :=
H2 : A := _
in _)
in main).
apply conj_hyp_tac.
assumption.
conj_hyp.
exact.
done.
apply conj_hyp_tac.
assumption.
conj_hyp.
exact.
done.
apply Conj.
assumption.
exact.
done.
(**
simple_tac = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
**)
Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
@ -25,6 +26,6 @@ Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
H2 : B := _,
main : B /\ A := _
in main).
apply simple_tac. done.
apply simple_tac. done.
apply simple_tac. done.
simple_tac. done.
simple_tac. done.
simple_tac. done.

3
tests/lean/norm_tac.lean
View file

@ -1,10 +1,11 @@
(** import("tactic.lua") **)
SetOption pp::implicit true
SetOption pp::coercion true
SetOption pp::notation false
Variable vector (A : Type) (sz : Nat) : Type
Variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A
Variable V1 : vector Int 10
Definition D := read V1 1 (by trivial_tac)
Definition D := read V1 1 (by trivial)
Show Environment 1
Variable b : Bool
Definition a := b

3
tests/lean/pr1.lean
View file

@ -1,5 +1,6 @@
(** import("tactic.lua") **)
Theorem T (C A B : Bool) : C -> A -> B -> A.
assumption.
exact.
done.
Show Environment 1.

16
tests/lean/slow/tactic1.lean
View file

@ -4,29 +4,29 @@ Definition big {A : Type} (f : A -> A) : A -> A := (double (double (double (doub
(**
-- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions
local congr_tac = REPEAT(ORELSE(apply_tac("Refl"), apply_tac("Congr"), assumption_tac))
local congr_tac = Repeat(OrElse(apply_tac("Refl"), apply_tac("Congr"), assumption_tac()))
-- Create an eager tactic that only tries to prove goal after unfolding everything
eager_tac = THEN(-- unfold homogeneous equality
TRY(unfold_tac("eq")),
eager_tac = Then(-- unfold homogeneous equality
Try(unfold_tac("eq")),
-- keep unfolding defintions above and beta-reducing
REPEAT(unfold_tac .. REPEAT(beta_tac)),
Repeat(unfold_tac() .. Repeat(beta_tac())),
congr_tac)
-- The 'lazy' version tries first to prove without unfolding anything
lazy_tac = ORELSE(THEN(TRY(unfold_tac("eq")), congr_tac, now_tac),
lazy_tac = OrElse(Then(Try(unfold_tac("eq")), congr_tac, now_tac()),
eager_tac)
**)
Theorem T1 (a b : Int) (f : Int -> Int) (H : a = b) : (big f a) = (big f b).
apply eager_tac.
eager_tac.
done.
Theorem T2 (a b : Int) (f : Int -> Int) (H : a = b) : (big f a) = (big f b).
apply lazy_tac.
lazy_tac.
done.
Theorem T3 (a b : Int) (f : Int -> Int) (H : a = b) : (big f a) = ((double (double (double (double (double (double (double f))))))) b).
apply lazy_tac.
lazy_tac.
done.

7
tests/lean/subst2.lean
View file

@ -1,10 +1,11 @@
(** import("tactic.lua") **)
Theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) => x = y => x = z => p (f y z).
apply ForallIntro.
apply beta_tac.
beta.
apply ForallIntro.
apply beta_tac.
beta.
apply ForallIntro.
apply beta_tac.
beta.
apply Discharge.
apply Discharge.
apply Discharge.

2
tests/lean/tactic1.lean
View file

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

17
tests/lean/tactic10.lean
View file

@ -1,23 +1,24 @@
(** import("tactic.lua") **)
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_tac
apply imp_tac
apply imp_tac
apply disj_hyp_tac
assumption
apply absurd_tac
unfold_all
apply Discharge
apply Discharge
disj_hyp
exact
absurd
done.
(**
simple_tac = REPEAT(unfold_tac) .. REPEAT(ORELSE(imp_tac, conj_hyp_tac, assumption_tac, absurd_tac, conj_hyp_tac, disj_hyp_tac))
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.
Theorem T2 (a b : Bool) : (h a b) => (f b) => a := _.
apply simple_tac
simple_tac
done.
Show Environment 1.

9
tests/lean/tactic11.lean
View file

@ -1,6 +1,7 @@
(** import("tactic.lua") **)
Theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a) := _ .
apply beta_tac.
apply imp_tac.
apply conj_hyp_tac.
apply assumption_tac.
beta.
apply Discharge.
conj_hyp.
exact.
done.

15
tests/lean/tactic12.lean
View file

@ -1,13 +1,14 @@
(** import("tactic.lua") **)
Theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a).
apply beta_tac.
apply imp_tac.
apply conj_hyp_tac.
apply assumption_tac.
beta.
apply Discharge.
conj_hyp.
exact.
done.
Variables p q : Bool.
Theorem T2 : p /\ q => q.
apply imp_tac.
apply conj_hyp_tac.
apply assumption_tac.
apply Discharge.
conj_hyp.
exact.
done.

7
tests/lean/tactic13.lean
View file

@ -1,3 +1,4 @@
(** import("tactic.lua") **)
Variable f : Int -> Int -> Int
(**
@ -6,15 +7,15 @@ congr_tac = apply_tac("Congr")
symm_tac = apply_tac("Symm")
trans_tac = apply_tac("Trans")
unfold_homo_eq_tac = unfold_tac("eq")
auto = unfold_homo_eq_tac .. REPEAT(ORELSE(refl_tac, congr_tac, assumption_tac, THEN(symm_tac, assumption_tac, now_tac)))
auto = unfold_homo_eq_tac .. Repeat(OrElse(refl_tac, congr_tac, assumption_tac(), Then(symm_tac, assumption_tac(), now_tac())))
**)
Theorem T1 (a b c : Int) (H1 : a = b) (H2 : a = c) : (f (f a a) b) = (f (f b c) a).
apply auto.
auto.
done.
Theorem T2 (a b c : Int) (H1 : a = b) (H2 : a = c) : (f (f a c)) = (f (f b a)).
apply auto.
auto.
done.
Show Environment 2.

2
tests/lean/tactic14.lean
View file

@ -1,7 +1,7 @@
(**
-- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions
congr_tac = TRY(unfold_tac("eq")) .. REPEAT(ORELSE(apply_tac("Refl"), apply_tac("Congr"), assumption_tac))
congr_tac = Try(unfold_tac("eq")) .. Repeat(OrElse(apply_tac("Refl"), apply_tac("Congr"), assumption_tac()))
**)

18
tests/lean/tactic2.lean
View file

@ -1,3 +1,4 @@
(** import("tactic.lua") **)
Variables p q r : Bool
Theorem T1 : p => q => p /\ q :=
@ -7,23 +8,30 @@ Theorem T1 : p => q => p /\ q :=
H2 : q := _
in Conj H1 H2
)).
assumption (* solve first metavar *)
exact (* solve first metavar *)
done
apply assumption_tac (* solve second metavar *)
exact (* solve second metavar *)
done
(**
simple_tac = REPEAT(imp_tac() ^ conj_tac() ^ assumption_tac())
simple_tac = Repeat(imp_tac() ^ conj_tac() ^ assumption_tac())
**)
Theorem T2 : p => q => p /\ q /\ p := _.
apply simple_tac
simple_tac
done
Show Environment 1
Theorem T3 : p => p /\ q => r => q /\ r /\ p := _.
apply (** REPEAT(ORELSE(imp_tac, conj_tac, conj_hyp_tac, assumption_tac)) **)
(** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **)
done
(* Display proof term generated by previous tac *)
Show Environment 1
Theorem T4 : p => p /\ q => r => q /\ r /\ p := _.
Repeat (OrElse (apply Discharge) (apply Conj) conj_hyp exact)
done
(* Display proof term generated by previous tac *)

7
tests/lean/tactic2.lean.expected.out
View file

@ -11,3 +11,10 @@ Theorem T3 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
Discharge
(λ H : p,
Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1)))))
Proved: T4
Theorem T4 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
Discharge
(λ H : p,
Discharge
(λ H::1 : p ∧ q,
Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (let H::1::1 := Conjunct1 H::1 in Conj H::2 H::1::1))))

3
tests/lean/tactic3.lean
View file

@ -1,7 +1,8 @@
(** import("tactic.lua") **)
Variables p q r : Bool
Theorem T1 : p => p /\ q => r => q /\ r /\ p := _.
apply (** REPEAT(ORELSE(imp_tac, conj_tac, conj_hyp_tac, assumption_tac)) **)
(** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **)
done
(* Display proof term generated by previous tactic *)

4
tests/lean/tactic4.lean
View file

@ -1,9 +1,9 @@
(**
simple_tac = REPEAT(ORELSE(imp_tac(), conj_tac())) .. assumption_tac()
simple_tac = Repeat(OrElse(imp_tac(), conj_tac())) .. assumption_tac()
**)
Theorem T4 (a b : Bool) : a => b => a /\ b := _.
apply simple_tac
simple_tac
done
Show Environment 1.

4
tests/lean/tactic5.lean
View file

@ -1,9 +1,9 @@
(**
simple_tac = REPEAT(ORELSE(imp_tac, conj_tac)) .. assumption_tac
simple_tac = Repeat(OrElse(imp_tac(), conj_tac())) .. assumption_tac()
**)
Theorem T4 (a b : Bool) : a => b => a /\ b /\ a := _.
apply simple_tac
simple_tac
done
Show Environment 1.

33
tests/lean/tactic6.lean
View file

@ -1,21 +1,22 @@
(** import("tactic.lua") **)
Theorem T (a b c : Bool): a => b /\ c => c /\ a /\ b := _.
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
apply Discharge
apply Discharge
conj_hyp
apply Conj
(** Focus(Then(show_tac(), conj_tac(), show_tac(), assumption_tac()), 2) **)
exact
done
Theorem T2 (a b c : Bool): a => b /\ c => c /\ a /\ b := _.
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) **)
apply Discharge
apply Discharge
conj_hyp
apply Conj
(** show_tac() **)
(** Focus(Then(show_tac(), conj_tac(), Focus(assumption_tac(), 1)), 2) **)
(** show_tac() **)
(** Focus(assumption_tac(), 1) **)
(** show_tac() **)
(** Focus(assumption_tac(), 1) **)
done

11
tests/lean/tactic8.lean
View file

@ -1,8 +1,9 @@
(** import("tactic.lua") **)
Theorem T (a b : Bool) : a \/ b => (not b) => a := _.
apply imp_tac
apply imp_tac
apply disj_hyp_tac
apply assumption_tac
apply absurd_tac
apply Discharge
apply Discharge
disj_hyp
exact
absurd
done
Show Environment 1.

14
tests/lean/tactic9.lean
View file

@ -1,11 +1,13 @@
(** import("tactic.lua") **)
Definition f(a : Bool) : Bool := not a.
Theorem T (a b : Bool) : a \/ b => (f b) => a := _.
apply imp_tac
apply imp_tac
apply disj_hyp_tac
apply (** unfold_tac("f") **)
apply assumption_tac
apply absurd_tac
apply Discharge
apply Discharge
disj_hyp
unfold f
exact
absurd
done
Show Environment 1.