refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44, fixes #70
This commit is contained in:
Leonardo de Moura
parent
0f5d88517d
commit
58c9421bab
36 changed files with 626 additions and 251 deletions
|
|
@ -4,6 +4,6 @@ open tactic
|
|||
namespace fake_simplifier
|
||||
|
||||
-- until we have the simplifier...
|
||||
opaque definition simp : tactic := apply @sorry
|
||||
opaque definition simp : tactic := apply sorry
|
||||
|
||||
end fake_simplifier
|
||||
|
|
|
|||
|
|
@ -12,6 +12,6 @@ import .tactic
|
|||
open tactic
|
||||
|
||||
namespace helper_tactics
|
||||
definition apply_refl := apply @eq.refl
|
||||
definition apply_refl := apply eq.refl
|
||||
tactic_hint apply_refl
|
||||
end helper_tactics
|
||||
|
|
|
|||
|
|
@ -36,7 +36,6 @@ opaque definition state : tactic := builtin
|
|||
opaque definition fail : tactic := builtin
|
||||
opaque definition id : tactic := builtin
|
||||
opaque definition beta : tactic := builtin
|
||||
opaque definition apply {B : Type} (b : B) : tactic := builtin
|
||||
opaque definition unfold {B : Type} (b : B) : tactic := builtin
|
||||
opaque definition exact {B : Type} (b : B) : tactic := builtin
|
||||
opaque definition trace (s : string) : tactic := builtin
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp
|
|||
theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp
|
||||
extra_info.cpp local_context.cpp choice_iterator.cpp
|
||||
placeholder_elaborator.cpp coercion_elaborator.cpp
|
||||
proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp)
|
||||
proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp
|
||||
builtin_tactics.cpp)
|
||||
|
||||
target_link_libraries(lean_frontend ${LEAN_LIBS})
|
||||
|
|
|
|||
|
|
@ -15,6 +15,7 @@ Author: Leonardo de Moura
|
|||
#include "library/choice.h"
|
||||
#include "library/let.h"
|
||||
#include "frontends/lean/builtin_exprs.h"
|
||||
#include "frontends/lean/builtin_tactics.h"
|
||||
#include "frontends/lean/token_table.h"
|
||||
#include "frontends/lean/calc.h"
|
||||
#include "frontends/lean/begin_end_ext.h"
|
||||
|
|
@ -117,12 +118,21 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
|
|||
return p.mk_by(t, pos);
|
||||
}
|
||||
|
||||
static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) {
|
||||
static expr parse_begin_end_core(parser & p, pos_info const & pos) {
|
||||
if (!p.has_tactic_decls())
|
||||
throw parser_error("invalid 'begin-end' expression, tactic module has not been imported", pos);
|
||||
optional<expr> pre_tac = get_begin_end_pre_tactic(p.env());
|
||||
optional<expr> r;
|
||||
while (true) {
|
||||
buffer<expr> tacs;
|
||||
bool first = true;
|
||||
while (!p.curr_is_token(get_end_tk())) {
|
||||
if (first)
|
||||
first = false;
|
||||
else
|
||||
p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected");
|
||||
if (p.curr_is_token(get_end_tk())) {
|
||||
p.next();
|
||||
throw parser_error("invalid 'begin-end' expression, tactic or expression expected", p.pos());
|
||||
}
|
||||
bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||
|
||||
p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
|
||||
p.curr_is_token(get_fun_tk()));
|
||||
|
|
@ -133,17 +143,25 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const &
|
|||
if (pre_tac)
|
||||
tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
|
||||
tac = p.mk_app(get_determ_tac_fn(), tac, pos);
|
||||
r = r ? p.mk_app({get_and_then_tac_fn(), *r, tac}, pos) : tac;
|
||||
if (p.curr_is_token(get_end_tk())) {
|
||||
auto pos = p.pos();
|
||||
p.next();
|
||||
return p.mk_by(*r, pos);
|
||||
} else if (p.curr_is_token(get_comma_tk())) {
|
||||
p.next();
|
||||
} else {
|
||||
throw parser_error("invalid begin-end, ',' or 'end' expected", p.pos());
|
||||
tacs.push_back(tac);
|
||||
}
|
||||
auto end_pos = p.pos();
|
||||
p.next();
|
||||
if (tacs.empty()) {
|
||||
expr tac = get_id_tac_fn();
|
||||
if (pre_tac)
|
||||
tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, end_pos);
|
||||
tacs.push_back(tac);
|
||||
}
|
||||
expr r = tacs[0];
|
||||
for (unsigned i = 1; i < tacs.size(); i++) {
|
||||
r = p.mk_app({get_and_then_tac_fn(), r, tacs[i]}, end_pos);
|
||||
}
|
||||
return p.mk_by(r, end_pos);
|
||||
}
|
||||
|
||||
static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) {
|
||||
return parse_begin_end_core(p, pos);
|
||||
}
|
||||
|
||||
static expr parse_proof_qed_core(parser & p, pos_info const & pos) {
|
||||
|
|
@ -161,6 +179,10 @@ static expr parse_proof(parser & p, expr const & prop) {
|
|||
auto pos = p.pos();
|
||||
p.next();
|
||||
return parse_proof_qed_core(p, pos);
|
||||
} else if (p.curr_is_token(get_begin_tk())) {
|
||||
auto pos = p.pos();
|
||||
p.next();
|
||||
return parse_begin_end_core(p, pos);
|
||||
} else if (p.curr_is_token(get_by_tk())) {
|
||||
// parse: 'by' tactic
|
||||
auto pos = p.pos();
|
||||
|
|
@ -386,6 +408,7 @@ parse_table init_nud_table() {
|
|||
r = r.add({transition("begin", mk_ext_action(parse_begin_end))}, x0);
|
||||
r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0);
|
||||
r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0);
|
||||
init_nud_tactic_table(r);
|
||||
return r;
|
||||
}
|
||||
|
||||
|
|
|
|||
33
src/frontends/lean/builtin_tactics.cpp
Normal file
33
src/frontends/lean/builtin_tactics.cpp
Normal file
|
|
@ -0,0 +1,33 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <limits>
|
||||
#include "library/explicit.h"
|
||||
#include "library/tactic/expr_to_tactic.h"
|
||||
#include "frontends/lean/parser.h"
|
||||
#include "frontends/lean/parse_table.h"
|
||||
|
||||
namespace lean {
|
||||
using notation::transition;
|
||||
using notation::mk_ext_action;
|
||||
|
||||
static expr parse_apply(parser & p, unsigned, expr const *, pos_info const & pos) {
|
||||
parser::no_undef_id_error_scope scope(p);
|
||||
expr e = p.parse_expr(std::numeric_limits<unsigned>::max());
|
||||
return p.save_pos(mk_apply_tactic_macro(e), pos);
|
||||
}
|
||||
|
||||
void init_nud_tactic_table(parse_table & r) {
|
||||
expr x0 = mk_var(0);
|
||||
r = r.add({transition("apply", mk_ext_action(parse_apply))}, x0);
|
||||
}
|
||||
|
||||
void initialize_builtin_tactics() {
|
||||
}
|
||||
|
||||
void finalize_builtin_tactics() {
|
||||
}
|
||||
}
|
||||
14
src/frontends/lean/builtin_tactics.h
Normal file
14
src/frontends/lean/builtin_tactics.h
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "frontends/lean/parse_table.h"
|
||||
|
||||
namespace lean {
|
||||
void init_nud_tactic_table(parse_table & r);
|
||||
void initialize_builtin_tactics();
|
||||
void finalize_builtin_tactics();
|
||||
}
|
||||
|
|
@ -91,8 +91,9 @@ elaborator::elaborator(elaborator_context & ctx, name_generator const & ngen):
|
|||
m_context(),
|
||||
m_full_context(),
|
||||
m_unifier_config(ctx.m_ios.get_options(), true /* use exceptions */, true /* discard */) {
|
||||
m_has_sorry = has_sorry(m_ctx.m_env),
|
||||
m_has_sorry = has_sorry(m_ctx.m_env);
|
||||
m_relax_main_opaque = false;
|
||||
m_use_tactic_hints = true;
|
||||
m_no_info = false;
|
||||
m_tc[0] = mk_type_checker(ctx.m_env, m_ngen.mk_child(), false);
|
||||
m_tc[1] = mk_type_checker(ctx.m_env, m_ngen.mk_child(), true);
|
||||
|
|
@ -601,6 +602,8 @@ expr elaborator::visit_sort(expr const & e) {
|
|||
expr elaborator::visit_macro(expr const & e, constraint_seq & cs) {
|
||||
if (is_as_is(e)) {
|
||||
return get_as_is_arg(e);
|
||||
} else if (is_tactic_macro(e)) {
|
||||
return e;
|
||||
} else {
|
||||
buffer<expr> args;
|
||||
for (unsigned i = 0; i < macro_num_args(e); i++)
|
||||
|
|
@ -882,25 +885,12 @@ void elaborator::display_unsolved_proof_state(expr const & mvar, proof_state con
|
|||
}
|
||||
}
|
||||
|
||||
// For each occurrence of \c exact_tac in \c pre_tac, display its unassigned metavariables.
|
||||
// This is a trick to improve the quality of the error messages.
|
||||
void elaborator::check_exact_tacs(expr const & pre_tac, substitution const & s) {
|
||||
for_each(pre_tac, [&](expr const & e, unsigned) {
|
||||
expr const & f = get_app_fn(e);
|
||||
if (is_constant(f) && const_name(f) == const_name(get_exact_tac_fn())) {
|
||||
display_unassigned_mvars(e, s);
|
||||
return false;
|
||||
} else {
|
||||
return true;
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
optional<expr> elaborator::get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited) {
|
||||
if (auto it = m_local_tactic_hints.find(mlocal_name(mvar))) {
|
||||
expr pre_tac = subst.instantiate(*it);
|
||||
// TODO(Leo): after we move to new apply/exact, we will not need the following
|
||||
// command anymore.
|
||||
pre_tac = solve_unassigned_mvars(subst, pre_tac, visited);
|
||||
check_exact_tacs(pre_tac, subst);
|
||||
return some_expr(pre_tac);
|
||||
} else {
|
||||
return none_expr();
|
||||
|
|
@ -909,7 +899,15 @@ optional<expr> elaborator::get_pre_tactic_for(substitution & subst, expr const &
|
|||
|
||||
optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac, expr const & mvar) {
|
||||
try {
|
||||
return optional<tactic>(expr_to_tactic(env(), pre_tac, pip()));
|
||||
bool relax = m_relax_main_opaque;
|
||||
auto fn = [=](goal const & g, name_generator const & ngen, expr const & e) {
|
||||
elaborator aux_elaborator(m_ctx, ngen);
|
||||
// Disable tactic hints when processing expressions nested in tactics.
|
||||
// We must do it otherwise, it is easy to make the system loop.
|
||||
bool use_tactic_hints = false;
|
||||
return aux_elaborator.elaborate_nested(g.to_context(), e, relax, use_tactic_hints);
|
||||
};
|
||||
return optional<tactic>(expr_to_tactic(env(), fn, pre_tac, pip()));
|
||||
} catch (expr_to_tactic_exception & ex) {
|
||||
auto out = regular(env(), ios());
|
||||
display_error_pos(out, pip(), mvar);
|
||||
|
|
@ -980,12 +978,12 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
|
|||
expr type = m_tc[m_relax_main_opaque]->infer(*meta).first;
|
||||
// first solve unassigned metavariables in type
|
||||
type = solve_unassigned_mvars(subst, type, visited);
|
||||
proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child());
|
||||
proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child());
|
||||
if (auto local_hint = get_local_tactic_hint(subst, mvar, visited)) {
|
||||
// using user provided tactic
|
||||
bool show_failure = true;
|
||||
try_using(subst, mvar, ps, *local_hint, show_failure);
|
||||
} else {
|
||||
} else if (m_use_tactic_hints) {
|
||||
// using tactic_hints
|
||||
for (expr const & pre_tac : get_tactic_hints(env())) {
|
||||
if (auto tac = pre_tactic_to_tactic(pre_tac, mvar)) {
|
||||
|
|
@ -1022,8 +1020,8 @@ void elaborator::display_unassigned_mvars(expr const & e, substitution const & s
|
|||
expr meta = tmp_s.instantiate(*it);
|
||||
expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first);
|
||||
goal g(meta, meta_type);
|
||||
display_unsolved_proof_state(e, proof_state(goals(g), substitution(), m_ngen),
|
||||
"don't know how to synthesize it");
|
||||
proof_state ps(goals(g), substitution(), m_ngen, constraints());
|
||||
display_unsolved_proof_state(e, ps, "don't know how to synthesize it");
|
||||
}
|
||||
return false;
|
||||
});
|
||||
|
|
@ -1078,8 +1076,8 @@ std::tuple<expr, level_param_names> elaborator::apply(substitution & s, expr con
|
|||
return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
|
||||
}
|
||||
|
||||
std::tuple<expr, level_param_names> elaborator::operator()(list<expr> const & ctx, expr const & e, bool _ensure_type,
|
||||
bool relax_main_opaque) {
|
||||
auto elaborator::operator()(list<expr> const & ctx, expr const & e, bool _ensure_type, bool relax_main_opaque)
|
||||
-> std::tuple<expr, level_param_names> {
|
||||
m_context.set_ctx(ctx);
|
||||
m_full_context.set_ctx(ctx);
|
||||
flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque);
|
||||
|
|
@ -1126,6 +1124,62 @@ std::tuple<expr, expr, level_param_names> elaborator::operator()(
|
|||
return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end()));
|
||||
}
|
||||
|
||||
// Auxiliary procedure for #translate
|
||||
static expr translate_local_name(environment const & env, list<expr> const & ctx, name const & local_name,
|
||||
expr const & src) {
|
||||
for (expr const & local : ctx) {
|
||||
if (mlocal_name(local) == local_name)
|
||||
return local;
|
||||
}
|
||||
// TODO(Leo): we should create an elaborator exception.
|
||||
// Using kernel_exception here is just a dirty hack.
|
||||
throw_kernel_exception(env, sstream() << "unknown identifier '" << local_name << "'", src);
|
||||
}
|
||||
|
||||
/** \brief Translated local constants (and undefined constants) occurring in \c e into
|
||||
local constants provided by \c ctx.
|
||||
Throw exception is \c ctx does not contain the local constant.
|
||||
*/
|
||||
static expr translate(environment const & env, list<expr> const & ctx, expr const & e) {
|
||||
auto fn = [&](expr const & e) {
|
||||
if (is_placeholder(e)) {
|
||||
return some_expr(e); // ignore placeholders
|
||||
} else if (is_constant(e)) {
|
||||
if (!env.find(const_name(e))) {
|
||||
return some_expr(translate_local_name(env, ctx, const_name(e), e));
|
||||
} else {
|
||||
return none_expr();
|
||||
}
|
||||
} else if (is_local(e)) {
|
||||
return some_expr(translate_local_name(env, ctx, mlocal_name(e), e));
|
||||
} else {
|
||||
return none_expr();
|
||||
}
|
||||
};
|
||||
return replace(e, fn);
|
||||
}
|
||||
|
||||
/** \brief Elaborate expression \c e in context \c ctx. */
|
||||
pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, expr const & n,
|
||||
bool relax, bool use_tactic_hints) {
|
||||
expr e = translate(env(), ctx, n);
|
||||
m_context.set_ctx(ctx);
|
||||
m_full_context.set_ctx(ctx);
|
||||
flet<bool> set_relax(m_relax_main_opaque, relax);
|
||||
flet<bool> set_discard(m_unifier_config.m_discard, false);
|
||||
flet<bool> set_use_hints(m_use_tactic_hints, use_tactic_hints);
|
||||
constraint_seq cs;
|
||||
expr r = visit(e, cs);
|
||||
auto p = solve(cs).pull();
|
||||
lean_assert(p);
|
||||
substitution s = p->first.first;
|
||||
constraints rcs = p->first.second;
|
||||
r = s.instantiate(r);
|
||||
r = solve_unassigned_mvars(s, r);
|
||||
copy_info_to_manager(s);
|
||||
return mk_pair(r, rcs);
|
||||
}
|
||||
|
||||
static name * g_tmp_prefix = nullptr;
|
||||
|
||||
std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
|
||||
|
|
|
|||
|
|
@ -50,10 +50,10 @@ class elaborator : public coercion_info_manager {
|
|||
// if m_no_info is true, we do not collect information when true,
|
||||
// we set is to true whenever we find no_info annotation.
|
||||
bool m_no_info;
|
||||
bool m_use_tactic_hints;
|
||||
info_manager m_pre_info_data;
|
||||
bool m_has_sorry;
|
||||
unifier_config m_unifier_config;
|
||||
|
||||
struct choice_expr_elaborator;
|
||||
|
||||
environment const & env() const { return m_ctx.m_env; }
|
||||
|
|
@ -122,7 +122,6 @@ class elaborator : public coercion_info_manager {
|
|||
expr visit(expr const & e, constraint_seq & cs);
|
||||
unify_result_seq solve(constraint_seq const & cs);
|
||||
void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg);
|
||||
void check_exact_tacs(expr const & pre_tac, substitution const & s);
|
||||
optional<expr> get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited);
|
||||
optional<tactic> pre_tactic_to_tactic(expr const & pre_tac, expr const & mvar);
|
||||
optional<tactic> get_local_tactic_hint(substitution & subst, expr const & mvar, name_set & visited);
|
||||
|
|
@ -135,9 +134,10 @@ class elaborator : public coercion_info_manager {
|
|||
void check_sort_assignments(substitution const & s);
|
||||
expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params);
|
||||
std::tuple<expr, level_param_names> apply(substitution & s, expr const & e);
|
||||
pair<expr, constraints> elaborate_nested(list<expr> const & g, expr const & e,
|
||||
bool relax, bool use_tactic_hints);
|
||||
public:
|
||||
elaborator(elaborator_context & ctx, name_generator const & ngen);
|
||||
|
||||
std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type,
|
||||
bool relax_main_opaque);
|
||||
std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque);
|
||||
|
|
|
|||
|
|
@ -18,6 +18,7 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/begin_end_ext.h"
|
||||
#include "frontends/lean/builtin_cmds.h"
|
||||
#include "frontends/lean/builtin_exprs.h"
|
||||
#include "frontends/lean/builtin_tactics.h"
|
||||
#include "frontends/lean/inductive_cmd.h"
|
||||
#include "frontends/lean/structure_cmd.h"
|
||||
#include "frontends/lean/info_manager.h"
|
||||
|
|
@ -33,6 +34,7 @@ void initialize_frontend_lean_module() {
|
|||
initialize_token_table();
|
||||
initialize_parse_table();
|
||||
initialize_builtin_cmds();
|
||||
initialize_builtin_tactics();
|
||||
initialize_builtin_exprs();
|
||||
initialize_elaborator_context();
|
||||
initialize_elaborator();
|
||||
|
|
@ -71,6 +73,7 @@ void finalize_frontend_lean_module() {
|
|||
finalize_elaborator();
|
||||
finalize_elaborator_context();
|
||||
finalize_builtin_exprs();
|
||||
finalize_builtin_tactics();
|
||||
finalize_builtin_cmds();
|
||||
finalize_parse_table();
|
||||
finalize_token_table();
|
||||
|
|
|
|||
|
|
@ -30,7 +30,6 @@ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr cons
|
|||
constraint_seq new_cs = cs + tcs.second + dcs.second;
|
||||
buffer<constraint> cs_buffer;
|
||||
new_cs.linearize(cs_buffer);
|
||||
|
||||
metavar_closure cls(meta);
|
||||
cls.add(meta_type);
|
||||
cls.mk_constraints(s, j, relax, cs_buffer);
|
||||
|
|
|
|||
|
|
@ -76,7 +76,7 @@ void init_token_table(token_table & t) {
|
|||
{".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
|
||||
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
|
||||
{"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"local", 0},
|
||||
{nullptr, 0}};
|
||||
{"apply", 0}, {nullptr, 0}};
|
||||
|
||||
char const * commands[] =
|
||||
{"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion",
|
||||
|
|
|
|||
|
|
@ -60,6 +60,7 @@ static name * g_then = nullptr;
|
|||
static name * g_by = nullptr;
|
||||
static name * g_proof = nullptr;
|
||||
static name * g_qed = nullptr;
|
||||
static name * g_begin = nullptr;
|
||||
static name * g_end = nullptr;
|
||||
static name * g_definition = nullptr;
|
||||
static name * g_theorem = nullptr;
|
||||
|
|
@ -143,6 +144,7 @@ void initialize_tokens() {
|
|||
g_by = new name("by");
|
||||
g_proof = new name("proof");
|
||||
g_qed = new name("qed");
|
||||
g_begin = new name("begin");
|
||||
g_end = new name("end");
|
||||
g_definition = new name("definition");
|
||||
g_theorem = new name("theorem");
|
||||
|
|
@ -210,6 +212,7 @@ void finalize_tokens() {
|
|||
delete g_by;
|
||||
delete g_proof;
|
||||
delete g_qed;
|
||||
delete g_begin;
|
||||
delete g_end;
|
||||
delete g_raw;
|
||||
delete g_true;
|
||||
|
|
@ -310,6 +313,7 @@ name const & get_then_tk() { return *g_then; }
|
|||
name const & get_by_tk() { return *g_by; }
|
||||
name const & get_proof_tk() { return *g_proof; }
|
||||
name const & get_qed_tk() { return *g_qed; }
|
||||
name const & get_begin_tk() { return *g_begin; }
|
||||
name const & get_end_tk() { return *g_end; }
|
||||
name const & get_definition_tk() { return *g_definition; }
|
||||
name const & get_theorem_tk() { return *g_theorem; }
|
||||
|
|
|
|||
|
|
@ -61,6 +61,7 @@ name const & get_using_tk();
|
|||
name const & get_then_tk();
|
||||
name const & get_by_tk();
|
||||
name const & get_proof_tk();
|
||||
name const & get_begin_tk();
|
||||
name const & get_qed_tk();
|
||||
name const & get_end_tk();
|
||||
name const & get_definition_tk();
|
||||
|
|
|
|||
|
|
@ -322,7 +322,7 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const &
|
|||
substitution tmp(subst);
|
||||
expr new_m = instantiate_meta(m, tmp);
|
||||
expr new_type = type_checker(env).infer(new_m).first;
|
||||
proof_state ps(goals(goal(new_m, new_type)), substitution(), name_generator("dontcare"));
|
||||
proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"));
|
||||
return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
|
||||
});
|
||||
}
|
||||
|
|
|
|||
|
|
@ -13,15 +13,16 @@ Author: Leonardo de Moura
|
|||
#include "kernel/instantiate.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "library/reducible.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/unifier.h"
|
||||
#include "library/occurs.h"
|
||||
#include "library/metavar_closure.h"
|
||||
#include "library/type_util.h"
|
||||
#include "library/tactic/apply_tactic.h"
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief Traverse \c e and collect metavariable applications (?m l1 ... ln), and store in result.
|
||||
/** \brief Traverse \c e and collect metavariable applications (?m l1 ... ln), and store in result.
|
||||
The function only succeeds if all metavariable applications are "simple", i.e., the arguments
|
||||
are distinct local constants.
|
||||
*/
|
||||
|
|
@ -58,7 +59,7 @@ void collect_simple_meta(expr const & e, buffer<expr> & metas) {
|
|||
we say ?m_i is "redundant" if it occurs in the type of some ?m_j.
|
||||
This procedure removes from metas any redundant element.
|
||||
*/
|
||||
static void remove_redundant_metas(buffer<expr> & metas) {
|
||||
void remove_redundant_metas(buffer<expr> & metas) {
|
||||
buffer<expr> mvars;
|
||||
for (expr const & m : metas)
|
||||
mvars.push_back(get_app_fn(m));
|
||||
|
|
@ -81,65 +82,78 @@ static void remove_redundant_metas(buffer<expr> & metas) {
|
|||
metas.shrink(k);
|
||||
}
|
||||
|
||||
proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e,
|
||||
bool add_meta, bool add_subgoals, bool relax_main_opaque) {
|
||||
// TODO(Leo): we are ignoring constraints produces by type checker
|
||||
static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e,
|
||||
buffer<constraint> & cs, bool add_meta, bool add_subgoals, bool relax_main_opaque) {
|
||||
goals const & gs = s.get_goals();
|
||||
if (empty(gs))
|
||||
return proof_state_seq();
|
||||
name_generator ngen = s.get_ngen();
|
||||
type_checker tc(env, ngen.mk_child());
|
||||
std::unique_ptr<type_checker> tc = mk_type_checker(env, ngen.mk_child(), relax_main_opaque);
|
||||
goal g = head(gs);
|
||||
goals tail_gs = tail(gs);
|
||||
expr t = g.get_type();
|
||||
expr e = _e;
|
||||
expr e_t = tc.infer(e).first;
|
||||
auto e_t_cs = tc->infer(e);
|
||||
e_t_cs.second.linearize(cs);
|
||||
expr e_t = e_t_cs.first;
|
||||
buffer<expr> metas;
|
||||
collect_simple_meta(e, metas);
|
||||
if (add_meta) {
|
||||
unsigned num_t = get_expect_num_args(tc, t);
|
||||
unsigned num_e_t = get_expect_num_args(tc, e_t);
|
||||
unsigned num_t = get_expect_num_args(*tc, t);
|
||||
unsigned num_e_t = get_expect_num_args(*tc, e_t);
|
||||
if (num_t > num_e_t)
|
||||
return proof_state_seq(); // no hope to unify then
|
||||
for (unsigned i = 0; i < num_e_t - num_t; i++) {
|
||||
e_t = tc.whnf(e_t).first;
|
||||
auto e_t_cs = tc->whnf(e_t);
|
||||
e_t_cs.second.linearize(cs);
|
||||
e_t = e_t_cs.first;
|
||||
expr meta = g.mk_meta(ngen.next(), binding_domain(e_t));
|
||||
e = mk_app(e, meta);
|
||||
e_t = instantiate(binding_body(e_t), meta);
|
||||
metas.push_back(meta);
|
||||
}
|
||||
}
|
||||
metavar_closure cls(t);
|
||||
cls.mk_constraints(s.get_subst(), justification(), relax_main_opaque);
|
||||
pair<bool, constraint_seq> dcs = tc->is_def_eq(t, e_t);
|
||||
if (!dcs.first)
|
||||
return proof_state_seq();
|
||||
dcs.second.linearize(cs);
|
||||
unifier_config cfg(ios.get_options());
|
||||
unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), s.get_subst(), cfg);
|
||||
list<expr> meta_lst = to_list(metas.begin(), metas.end());
|
||||
unify_result_seq rseq = unify(env, t, e_t, ngen.mk_child(), relax_main_opaque, s.get_subst(),
|
||||
unifier_config(ios.get_options()));
|
||||
return map2<proof_state>(rseq, [=](pair<substitution, constraints> const & p) -> proof_state {
|
||||
substitution const & subst = p.first;
|
||||
// TODO(Leo): save postponed constraints
|
||||
constraints const & postponed = p.second;
|
||||
name_generator new_ngen(ngen);
|
||||
type_checker tc(env, new_ngen.mk_child());
|
||||
substitution new_subst = subst;
|
||||
expr new_e = new_subst.instantiate_all(e);
|
||||
expr new_p = g.abstract(new_e);
|
||||
check_has_no_local(new_p, _e, "apply");
|
||||
new_subst.assign(g.get_name(), new_p);
|
||||
// std::cout << g.get_name() << " := " << new_p << "\n";
|
||||
goals new_gs = tail_gs;
|
||||
if (add_subgoals) {
|
||||
// TODO(Leo): if mk_type_checker should return a shared_ptr, then we can reuse the tc defined
|
||||
// before
|
||||
std::unique_ptr<type_checker> tc = mk_type_checker(env, new_ngen.mk_child(), relax_main_opaque);
|
||||
buffer<expr> metas;
|
||||
for (auto m : meta_lst) {
|
||||
if (!new_subst.is_assigned(get_app_fn(m)))
|
||||
metas.push_back(m);
|
||||
}
|
||||
remove_redundant_metas(metas);
|
||||
unsigned i = metas.size();
|
||||
while (i > 0) {
|
||||
--i;
|
||||
new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc.infer(metas[i]).first)), new_gs);
|
||||
for (unsigned i = 0; i < metas.size(); i++)
|
||||
new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc->infer(metas[i]).first)), new_gs);
|
||||
}
|
||||
}
|
||||
return proof_state(new_gs, new_subst, new_ngen);
|
||||
return proof_state(new_gs, new_subst, new_ngen, postponed);
|
||||
});
|
||||
}
|
||||
|
||||
static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e,
|
||||
bool add_meta, bool add_subgoals, bool relax_main_opaque) {
|
||||
buffer<constraint> cs;
|
||||
return apply_tactic_core(env, ios, s, e, cs, add_meta, add_subgoals, relax_main_opaque);
|
||||
}
|
||||
|
||||
|
||||
level refresh_univ_metavars(level const & l, name_generator & ngen, name_map<level> & level_map) {
|
||||
return replace(l, [&](level const & l) {
|
||||
|
|
@ -182,7 +196,7 @@ tactic apply_tactic(expr const & e, bool relax_main_opaque, bool refresh_univ_mv
|
|||
name_generator ngen = s.get_ngen();
|
||||
substitution new_subst = s.get_subst();
|
||||
expr new_e = refresh_univ_metavars(new_subst.instantiate_all(e), ngen);
|
||||
proof_state new_s(s.get_goals(), new_subst, ngen);
|
||||
proof_state new_s(s.get_goals(), new_subst, ngen, s.get_postponed());
|
||||
return apply_tactic_core(env, ios, new_s, new_e, true, true, relax_main_opaque);
|
||||
} else {
|
||||
return apply_tactic_core(env, ios, s, e, true, true, relax_main_opaque);
|
||||
|
|
@ -206,6 +220,26 @@ tactic eassumption_tactic(bool relax_main_opaque) {
|
|||
});
|
||||
}
|
||||
|
||||
tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool relax_main_opaque) {
|
||||
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
|
||||
goals const & gs = s.get_goals();
|
||||
if (empty(gs))
|
||||
return proof_state_seq();
|
||||
goal const & g = head(gs);
|
||||
name_generator ngen = s.get_ngen();
|
||||
expr new_e;
|
||||
buffer<constraint> cs;
|
||||
// std::cout << "new apply tactic: " << e << "\n";
|
||||
auto ecs = elab(g, ngen.mk_child(), e);
|
||||
new_e = ecs.first;
|
||||
to_buffer(ecs.second, cs);
|
||||
// std::cout << "after elaboration: " << new_e << "\n";
|
||||
to_buffer(s.get_postponed(), cs);
|
||||
proof_state new_s(s.get_goals(), s.get_subst(), ngen, constraints());
|
||||
return apply_tactic_core(env, ios, new_s, new_e, cs, true, true, relax_main_opaque);
|
||||
});
|
||||
}
|
||||
|
||||
int mk_apply_tactic(lua_State * L) { return push_tactic(L, apply_tactic(to_expr(L, 1))); }
|
||||
int mk_eassumption_tactic(lua_State * L) { return push_tactic(L, eassumption_tactic()); }
|
||||
void open_apply_tactic(lua_State * L) {
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ Author: Leonardo de Moura
|
|||
#include "library/tactic/tactic.h"
|
||||
namespace lean {
|
||||
tactic apply_tactic(expr const & e, bool relax_main_opaque = true, bool refresh_univ_mvars = true);
|
||||
tactic apply_tactic(elaborate_fn const & fn, expr const & e, bool relax_main_opaque = true);
|
||||
tactic eassumption_tactic(bool relax_main_opaque = true);
|
||||
void open_apply_tactic(lua_State * L);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -7,15 +7,35 @@ Author: Leonardo de Moura
|
|||
#include <unordered_map>
|
||||
#include <string>
|
||||
#include "util/sstream.h"
|
||||
#include "util/optional.h"
|
||||
#include "kernel/instantiate.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "library/annotation.h"
|
||||
#include "library/string.h"
|
||||
#include "library/num.h"
|
||||
#include "library/kernel_serializer.h"
|
||||
#include "library/tactic/expr_to_tactic.h"
|
||||
#include "library/tactic/apply_tactic.h"
|
||||
|
||||
namespace lean {
|
||||
static expr * g_exact_tac_fn = nullptr;
|
||||
static expr * g_and_then_tac_fn = nullptr;
|
||||
static expr * g_or_else_tac_fn = nullptr;
|
||||
static expr * g_id_tac_fn = nullptr;
|
||||
static expr * g_repeat_tac_fn = nullptr;
|
||||
static expr * g_determ_tac_fn = nullptr;
|
||||
static expr * g_tac_type = nullptr;
|
||||
static expr * g_builtin_tac = nullptr;
|
||||
static expr * g_fixpoint_tac = nullptr;
|
||||
expr const & get_exact_tac_fn() { return *g_exact_tac_fn; }
|
||||
expr const & get_and_then_tac_fn() { return *g_and_then_tac_fn; }
|
||||
expr const & get_or_else_tac_fn() { return *g_or_else_tac_fn; }
|
||||
expr const & get_id_tac_fn() { return *g_id_tac_fn; }
|
||||
expr const & get_determ_tac_fn() { return *g_determ_tac_fn; }
|
||||
expr const & get_repeat_tac_fn() { return *g_repeat_tac_fn; }
|
||||
expr const & get_tactic_type() { return *g_tac_type; }
|
||||
expr const & get_builtin_tac() { return *g_builtin_tac; }
|
||||
|
||||
typedef std::unordered_map<name, expr_to_tactic_fn, name_hash, name_eq> expr_to_tactic_map;
|
||||
static expr_to_tactic_map * g_map = nullptr;
|
||||
|
||||
|
|
@ -27,21 +47,6 @@ void register_tac(name const & n, expr_to_tactic_fn const & fn) {
|
|||
get_expr_to_tactic_map().insert(mk_pair(n, fn));
|
||||
}
|
||||
|
||||
static expr * g_exact_tac_fn = nullptr;
|
||||
static expr * g_and_then_tac_fn = nullptr;
|
||||
static expr * g_or_else_tac_fn = nullptr;
|
||||
static expr * g_repeat_tac_fn = nullptr;
|
||||
static expr * g_determ_tac_fn = nullptr;
|
||||
static expr * g_tac_type = nullptr;
|
||||
static expr * g_builtin_tac = nullptr;
|
||||
static expr * g_fixpoint_tac = nullptr;
|
||||
expr const & get_exact_tac_fn() { return *g_exact_tac_fn; }
|
||||
expr const & get_and_then_tac_fn() { return *g_and_then_tac_fn; }
|
||||
expr const & get_or_else_tac_fn() { return *g_or_else_tac_fn; }
|
||||
expr const & get_determ_tac_fn() { return *g_determ_tac_fn; }
|
||||
expr const & get_repeat_tac_fn() { return *g_repeat_tac_fn; }
|
||||
expr const & get_tactic_type() { return *g_tac_type; }
|
||||
|
||||
bool has_tactic_decls(environment const & env) {
|
||||
try {
|
||||
type_checker tc(env);
|
||||
|
|
@ -55,6 +60,93 @@ bool has_tactic_decls(environment const & env) {
|
|||
}
|
||||
}
|
||||
|
||||
static name * g_tactic_name = nullptr;
|
||||
static std::string * g_tactic_opcode = nullptr;
|
||||
|
||||
name const & get_tactic_name() { return *g_tactic_name; }
|
||||
std::string const & get_tactic_opcode() { return *g_tactic_opcode; }
|
||||
|
||||
LEAN_THREAD_VALUE(bool, g_unfold_tactic_macros, true);
|
||||
|
||||
/** \brief We use macros to wrap some builtin tactics that would not type check otherwise.
|
||||
Example: in the tactic `apply t`, `t` is a pre-term (i.e., a term before elaboration).
|
||||
Moreover its context depends on the goal it is applied to.
|
||||
*/
|
||||
class tactic_macro_definition_cell : public macro_definition_cell {
|
||||
name m_name;
|
||||
expr_to_tactic_fn m_fn;
|
||||
public:
|
||||
tactic_macro_definition_cell(name const & n, expr_to_tactic_fn const & fn):
|
||||
m_name(n), m_fn(fn) {}
|
||||
name const & get_tatic_kind() const { return m_name; }
|
||||
expr_to_tactic_fn const & get_fn() const { return m_fn; }
|
||||
virtual name get_name() const { return get_tactic_name(); }
|
||||
virtual format pp(formatter const &) const { return format(m_name); }
|
||||
virtual void display(std::ostream & out) const { out << m_name; }
|
||||
virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const {
|
||||
return mk_pair(get_tactic_type(), constraint_seq());
|
||||
}
|
||||
virtual optional<expr> expand(expr const &, extension_context &) const {
|
||||
// Remark: small hack for conditionally expanding tactic macros.
|
||||
// When processing type checking a macro definition, we want to unfold it,
|
||||
// otherwise the kernel will not accept it.
|
||||
// When converting it to a tactic object, we don't want to unfold it.
|
||||
// The procedure expr_to_tactic temporarily sets g_unfold_tactic_macros to false.
|
||||
// This is a thread local storage. So, there is no danger.
|
||||
if (g_unfold_tactic_macros)
|
||||
return some_expr(get_builtin_tac());
|
||||
else
|
||||
return none_expr();
|
||||
}
|
||||
virtual void write(serializer & s) const {
|
||||
s.write_string(get_tactic_opcode());
|
||||
s << m_name;
|
||||
}
|
||||
};
|
||||
|
||||
typedef std::unordered_map<name, macro_definition, name_hash, name_eq> tactic_macros;
|
||||
static tactic_macros * g_tactic_macros = nullptr;
|
||||
tactic_macros & get_tactic_macros() { return *g_tactic_macros; }
|
||||
|
||||
void register_tactic_macro(name const & n, expr_to_tactic_fn const & fn) {
|
||||
tactic_macros & ms = get_tactic_macros();
|
||||
lean_assert(ms.find(n) == ms.end());
|
||||
ms.insert(mk_pair(n, macro_definition(new tactic_macro_definition_cell(n, fn))));
|
||||
}
|
||||
|
||||
static void register_tacm(name const & n, expr_to_tactic_fn const & fn) {
|
||||
register_tactic_macro(n, fn);
|
||||
}
|
||||
|
||||
expr mk_tactic_macro(name const & kind, unsigned num_args, expr const * args) {
|
||||
tactic_macros & ms = get_tactic_macros();
|
||||
auto it = ms.find(kind);
|
||||
if (it != ms.end()) {
|
||||
return mk_macro(it->second, num_args, args);
|
||||
} else {
|
||||
throw exception(sstream() << "unknown builtin tactic '" << kind << "'");
|
||||
}
|
||||
}
|
||||
|
||||
expr mk_tactic_macro(name const & kind, expr const & e) {
|
||||
return mk_tactic_macro(kind, 1, &e);
|
||||
}
|
||||
|
||||
bool is_tactic_macro(expr const & e) {
|
||||
return is_macro(e) && macro_def(e).get_name() == get_tactic_name();
|
||||
}
|
||||
|
||||
static name * g_apply_tactic_name = nullptr;
|
||||
|
||||
expr mk_apply_tactic_macro(expr const & e) {
|
||||
return mk_tactic_macro(*g_apply_tactic_name, e);
|
||||
}
|
||||
|
||||
expr_to_tactic_fn const & get_tactic_macro_fn(expr const & e) {
|
||||
lean_assert(is_tactic_macro(e));
|
||||
return static_cast<tactic_macro_definition_cell const*>(macro_def(e).raw())->get_fn();
|
||||
}
|
||||
|
||||
static void throw_failed(expr const & e) {
|
||||
throw expr_to_tactic_exception(e, "failed to convert expression into tactic");
|
||||
}
|
||||
|
|
@ -69,8 +161,11 @@ static bool is_builtin_tactic(expr const & v) {
|
|||
return false;
|
||||
}
|
||||
|
||||
tactic expr_to_tactic(type_checker & tc, expr e, pos_info_provider const * p) {
|
||||
tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p) {
|
||||
e = tc.whnf(e).first;
|
||||
if (is_tactic_macro(e)) {
|
||||
return get_tactic_macro_fn(e)(tc, fn, e, p);
|
||||
} else {
|
||||
expr f = get_app_fn(e);
|
||||
if (!is_constant(f))
|
||||
throw_failed(e);
|
||||
|
|
@ -82,9 +177,10 @@ tactic expr_to_tactic(type_checker & tc, expr e, pos_info_provider const * p) {
|
|||
auto const & map = get_expr_to_tactic_map();
|
||||
auto it2 = map.find(const_name(f));
|
||||
if (it2 != map.end())
|
||||
return it2->second(tc, e, p);
|
||||
return it2->second(tc, fn, e, p);
|
||||
else
|
||||
throw expr_to_tactic_exception(e, sstream() << "implementation for builtin tactic '" << const_name(f) << "' was not found");
|
||||
throw expr_to_tactic_exception(e, sstream() << "implementation for builtin tactic '" <<
|
||||
const_name(f) << "' was not found");
|
||||
} else {
|
||||
// unfold definition
|
||||
buffer<expr> locals;
|
||||
|
|
@ -104,7 +200,8 @@ tactic expr_to_tactic(type_checker & tc, expr e, pos_info_provider const * p) {
|
|||
}
|
||||
v = instantiate_univ_params(v, ps, ls);
|
||||
v = apply_beta(v, locals.size(), locals.data());
|
||||
return expr_to_tactic(tc, v, p);
|
||||
return expr_to_tactic(tc, fn, v, p);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -116,19 +213,21 @@ static name_generator next_name_generator() {
|
|||
return name_generator(name(*g_tmp_prefix, r));
|
||||
}
|
||||
|
||||
tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const * p) {
|
||||
tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
|
||||
// std::cout << "expr_to_tactic: " << e << "\n";
|
||||
flet<bool> let(g_unfold_tactic_macros, false);
|
||||
type_checker tc(env, next_name_generator());
|
||||
return expr_to_tactic(tc, e, p);
|
||||
return expr_to_tactic(tc, fn, e, p);
|
||||
}
|
||||
|
||||
tactic fixpoint(expr const & b) {
|
||||
tactic fixpoint(expr const & b, elaborate_fn const & fn) {
|
||||
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
|
||||
return expr_to_tactic(env, b, nullptr)(env, ios, s);
|
||||
return expr_to_tactic(env, fn, b, nullptr)(env, ios, s);
|
||||
});
|
||||
}
|
||||
|
||||
void register_simple_tac(name const & n, std::function<tactic()> f) {
|
||||
register_tac(n, [=](type_checker &, expr const & e, pos_info_provider const *) {
|
||||
register_tac(n, [=](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
|
||||
if (!is_constant(e))
|
||||
throw expr_to_tactic_exception(e, "invalid constant tactic");
|
||||
return f();
|
||||
|
|
@ -136,40 +235,42 @@ void register_simple_tac(name const & n, std::function<tactic()> f) {
|
|||
}
|
||||
|
||||
void register_bin_tac(name const & n, std::function<tactic(tactic const &, tactic const &)> f) {
|
||||
register_tac(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) {
|
||||
register_tac(n, [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
|
||||
buffer<expr> args;
|
||||
get_app_args(e, args);
|
||||
if (args.size() != 2)
|
||||
throw expr_to_tactic_exception(e, "invalid binary tactic, it must have two arguments");
|
||||
return f(expr_to_tactic(tc, args[0], p),
|
||||
expr_to_tactic(tc, args[1], p));
|
||||
return f(expr_to_tactic(tc, fn, args[0], p),
|
||||
expr_to_tactic(tc, fn, args[1], p));
|
||||
});
|
||||
}
|
||||
|
||||
void register_unary_tac(name const & n, std::function<tactic(tactic const &)> f) {
|
||||
register_tac(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) {
|
||||
register_tac(n, [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
|
||||
buffer<expr> args;
|
||||
get_app_args(e, args);
|
||||
if (args.size() != 1)
|
||||
throw expr_to_tactic_exception(e, "invalid unary tactic, it must have one argument");
|
||||
return f(expr_to_tactic(tc, args[0], p));
|
||||
return f(expr_to_tactic(tc, fn, args[0], p));
|
||||
});
|
||||
}
|
||||
|
||||
void register_unary_num_tac(name const & n, std::function<tactic(tactic const &, unsigned k)> f) {
|
||||
register_tac(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) {
|
||||
register_tac(n, [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
|
||||
buffer<expr> args;
|
||||
get_app_args(e, args);
|
||||
if (args.size() != 2)
|
||||
throw expr_to_tactic_exception(e, "invalid tactic, it must have two arguments");
|
||||
tactic t = expr_to_tactic(tc, args[0], p);
|
||||
tactic t = expr_to_tactic(tc, fn, args[0], p);
|
||||
optional<mpz> k = to_num(args[1]);
|
||||
if (!k)
|
||||
k = to_num(tc.whnf(args[1]).first);
|
||||
if (!k)
|
||||
throw expr_to_tactic_exception(e, "invalid tactic, second argument must be a numeral");
|
||||
if (!k->is_unsigned_int())
|
||||
throw expr_to_tactic_exception(e, "invalid tactic, second argument does not fit in a machine unsigned integer");
|
||||
throw expr_to_tactic_exception(e,
|
||||
"invalid tactic, second argument does not fit in "
|
||||
"a machine unsigned integer");
|
||||
return f(t, k->get_unsigned_int());
|
||||
});
|
||||
}
|
||||
|
|
@ -180,6 +281,11 @@ expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); }
|
|||
bool is_by(expr const & e) { return is_annotation(e, *g_by_name); }
|
||||
expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); }
|
||||
|
||||
static void check_macro_args(expr const & e, unsigned num_args, char const * msg) {
|
||||
if (macro_num_args(e) != num_args)
|
||||
throw expr_to_tactic_exception(e, msg);
|
||||
}
|
||||
|
||||
void initialize_expr_to_tactic() {
|
||||
g_tmp_prefix = new name(name::mk_internal_unique_name());
|
||||
|
||||
|
|
@ -188,42 +294,71 @@ void initialize_expr_to_tactic() {
|
|||
|
||||
g_map = new expr_to_tactic_map();
|
||||
|
||||
name g_tac("tactic");
|
||||
name g_builtin_tac_name(g_tac, "builtin");
|
||||
name g_exact_tac_name(g_tac, "exact");
|
||||
name g_and_then_tac_name(g_tac, "and_then");
|
||||
name g_or_else_tac_name(g_tac, "or_else");
|
||||
name g_repeat_tac_name(g_tac, "repeat");
|
||||
name g_fixpoint_name(g_tac, "fixpoint");
|
||||
name g_determ_tac_name(g_tac, "determ");
|
||||
g_exact_tac_fn = new expr(Const(g_exact_tac_name));
|
||||
g_and_then_tac_fn = new expr(Const(g_and_then_tac_name));
|
||||
g_or_else_tac_fn = new expr(Const(g_or_else_tac_name));
|
||||
g_repeat_tac_fn = new expr(Const(g_repeat_tac_name));
|
||||
g_determ_tac_fn = new expr(Const(g_determ_tac_name));
|
||||
g_tac_type = new expr(Const(g_tac));
|
||||
g_builtin_tac = new expr(Const(g_builtin_tac_name));
|
||||
g_fixpoint_tac = new expr(Const(g_fixpoint_name));
|
||||
g_tactic_name = new name("tactic");
|
||||
g_tactic_opcode = new std::string("TAC");
|
||||
|
||||
register_simple_tac(name(g_tac, "id"), []() { return id_tactic(); });
|
||||
register_simple_tac(name(g_tac, "now"), []() { return now_tactic(); });
|
||||
register_simple_tac(name(g_tac, "assumption"), []() { return assumption_tactic(); });
|
||||
register_simple_tac(name(g_tac, "eassumption"), []() { return eassumption_tactic(); });
|
||||
register_simple_tac(name(g_tac, "fail"), []() { return fail_tactic(); });
|
||||
register_simple_tac(name(g_tac, "beta"), []() { return beta_tactic(); });
|
||||
register_bin_tac(g_and_then_tac_name, [](tactic const & t1, tactic const & t2) { return then(t1, t2); });
|
||||
register_bin_tac(name(g_tac, "append"), [](tactic const & t1, tactic const & t2) { return append(t1, t2); });
|
||||
register_bin_tac(name(g_tac, "interleave"), [](tactic const & t1, tactic const & t2) { return interleave(t1, t2); });
|
||||
register_bin_tac(name(g_tac, "par"), [](tactic const & t1, tactic const & t2) { return par(t1, t2); });
|
||||
register_bin_tac(g_or_else_tac_name, [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
|
||||
register_unary_tac(g_repeat_tac_name, [](tactic const & t1) { return repeat(t1); });
|
||||
register_tac(name(g_tac, "state"), [](type_checker &, expr const & e, pos_info_provider const * p) {
|
||||
g_tactic_macros = new tactic_macros();
|
||||
|
||||
register_macro_deserializer(*g_tactic_opcode,
|
||||
[](deserializer & d, unsigned num, expr const * args) {
|
||||
name kind;
|
||||
d >> kind;
|
||||
return mk_tactic_macro(kind, num, args);
|
||||
});
|
||||
|
||||
g_apply_tactic_name = new name(*g_tactic_name, "apply");
|
||||
|
||||
name builtin_tac_name(*g_tactic_name, "builtin");
|
||||
name exact_tac_name(*g_tactic_name, "exact");
|
||||
name and_then_tac_name(*g_tactic_name, "and_then");
|
||||
name or_else_tac_name(*g_tactic_name, "or_else");
|
||||
name repeat_tac_name(*g_tactic_name, "repeat");
|
||||
name fixpoint_name(*g_tactic_name, "fixpoint");
|
||||
name determ_tac_name(*g_tactic_name, "determ");
|
||||
name id_tac_name(*g_tactic_name, "id");
|
||||
g_exact_tac_fn = new expr(Const(exact_tac_name));
|
||||
g_and_then_tac_fn = new expr(Const(and_then_tac_name));
|
||||
g_or_else_tac_fn = new expr(Const(or_else_tac_name));
|
||||
g_id_tac_fn = new expr(Const(id_tac_name));
|
||||
g_repeat_tac_fn = new expr(Const(repeat_tac_name));
|
||||
g_determ_tac_fn = new expr(Const(determ_tac_name));
|
||||
g_tac_type = new expr(Const(*g_tactic_name));
|
||||
g_builtin_tac = new expr(Const(builtin_tac_name));
|
||||
g_fixpoint_tac = new expr(Const(fixpoint_name));
|
||||
|
||||
register_simple_tac(id_tac_name,
|
||||
[]() { return id_tactic(); });
|
||||
register_simple_tac(name(*g_tactic_name, "now"),
|
||||
[]() { return now_tactic(); });
|
||||
register_simple_tac(name(*g_tactic_name, "assumption"),
|
||||
[]() { return assumption_tactic(); });
|
||||
register_simple_tac(name(*g_tactic_name, "eassumption"),
|
||||
[]() { return eassumption_tactic(); });
|
||||
register_simple_tac(name(*g_tactic_name, "fail"),
|
||||
[]() { return fail_tactic(); });
|
||||
register_simple_tac(name(*g_tactic_name, "beta"),
|
||||
[]() { return beta_tactic(); });
|
||||
register_bin_tac(and_then_tac_name,
|
||||
[](tactic const & t1, tactic const & t2) { return then(t1, t2); });
|
||||
register_bin_tac(name(*g_tactic_name, "append"),
|
||||
[](tactic const & t1, tactic const & t2) { return append(t1, t2); });
|
||||
register_bin_tac(name(*g_tactic_name, "interleave"),
|
||||
[](tactic const & t1, tactic const & t2) { return interleave(t1, t2); });
|
||||
register_bin_tac(name(*g_tactic_name, "par"),
|
||||
[](tactic const & t1, tactic const & t2) { return par(t1, t2); });
|
||||
register_bin_tac(or_else_tac_name,
|
||||
[](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
|
||||
register_unary_tac(repeat_tac_name,
|
||||
[](tactic const & t1) { return repeat(t1); });
|
||||
register_tac(name(*g_tactic_name, "state"),
|
||||
[](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const * p) {
|
||||
if (p)
|
||||
if (auto it = p->get_pos_info(e))
|
||||
return trace_state_tactic(std::string(p->get_file_name()), *it);
|
||||
return trace_state_tactic();
|
||||
});
|
||||
register_tac(name(g_tac, "trace"), [](type_checker & tc, expr const & e, pos_info_provider const *) {
|
||||
register_tac(name(*g_tactic_name, "trace"),
|
||||
[](type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) {
|
||||
buffer<expr> args;
|
||||
get_app_args(e, args);
|
||||
if (args.size() != 1)
|
||||
|
|
@ -235,28 +370,39 @@ void initialize_expr_to_tactic() {
|
|||
else
|
||||
throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected");
|
||||
});
|
||||
register_tac(name(g_tac, "apply"), [](type_checker &, expr const & e, pos_info_provider const *) {
|
||||
return apply_tactic(app_arg(e));
|
||||
register_tacm(*g_apply_tactic_name,
|
||||
[](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
|
||||
// std::cout << "gen apply: " << e << "\n";
|
||||
check_macro_args(e, 1, "invalid 'apply' tactic, it must have one argument");
|
||||
return apply_tactic(fn, macro_arg(e, 0));
|
||||
});
|
||||
register_tac(g_exact_tac_name, [](type_checker &, expr const & e, pos_info_provider const *) {
|
||||
register_tac(exact_tac_name,
|
||||
[](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
|
||||
// TODO(Leo): use elaborate_fn
|
||||
return exact_tactic(app_arg(e));
|
||||
});
|
||||
register_tac(name(g_tac, "unfold"), [](type_checker &, expr const & e, pos_info_provider const *) {
|
||||
register_tac(name(*g_tactic_name, "unfold"),
|
||||
[](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
|
||||
expr id = get_app_fn(app_arg(e));
|
||||
if (!is_constant(id))
|
||||
return fail_tactic();
|
||||
else
|
||||
return unfold_tactic(const_name(id));
|
||||
});
|
||||
register_unary_num_tac(name(g_tac, "at_most"), [](tactic const & t, unsigned k) { return take(t, k); });
|
||||
register_unary_num_tac(name(g_tac, "discard"), [](tactic const & t, unsigned k) { return discard(t, k); });
|
||||
register_unary_num_tac(name(g_tac, "focus_at"), [](tactic const & t, unsigned k) { return focus(t, k); });
|
||||
register_unary_num_tac(name(g_tac, "try_for"), [](tactic const & t, unsigned k) { return try_for(t, k); });
|
||||
register_tac(g_fixpoint_name, [](type_checker & tc, expr const & e, pos_info_provider const *) {
|
||||
register_unary_num_tac(name(*g_tactic_name, "at_most"),
|
||||
[](tactic const & t, unsigned k) { return take(t, k); });
|
||||
register_unary_num_tac(name(*g_tactic_name, "discard"),
|
||||
[](tactic const & t, unsigned k) { return discard(t, k); });
|
||||
register_unary_num_tac(name(*g_tactic_name, "focus_at"),
|
||||
[](tactic const & t, unsigned k) { return focus(t, k); });
|
||||
register_unary_num_tac(name(*g_tactic_name, "try_for"),
|
||||
[](tactic const & t, unsigned k) { return try_for(t, k); });
|
||||
register_tac(fixpoint_name,
|
||||
[](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
|
||||
if (!is_constant(app_fn(e)))
|
||||
throw expr_to_tactic_exception(e, "invalid fixpoint tactic, it must have one argument");
|
||||
expr r = tc.whnf(mk_app(app_arg(e), e)).first;
|
||||
return fixpoint(r);
|
||||
return fixpoint(r, fn);
|
||||
});
|
||||
}
|
||||
|
||||
|
|
@ -268,8 +414,13 @@ void finalize_expr_to_tactic() {
|
|||
delete g_repeat_tac_fn;
|
||||
delete g_or_else_tac_fn;
|
||||
delete g_and_then_tac_fn;
|
||||
delete g_id_tac_fn;
|
||||
delete g_exact_tac_fn;
|
||||
delete g_apply_tactic_name;
|
||||
delete g_tactic_macros;
|
||||
delete g_map;
|
||||
delete g_tactic_name;
|
||||
delete g_tactic_opcode;
|
||||
delete g_by_name;
|
||||
delete g_tmp_prefix;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ bool has_tactic_decls(environment const & env);
|
|||
and definitions marked as 'tactic.builtin' are handled by the code registered using
|
||||
\c register_expr_to_tactic.
|
||||
*/
|
||||
tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const *p);
|
||||
tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p);
|
||||
|
||||
/**
|
||||
\brief Create an expression `by t`, where \c t is an expression of type `tactic`.
|
||||
|
|
@ -44,9 +44,15 @@ expr const & get_tactic_type();
|
|||
expr const & get_exact_tac_fn();
|
||||
expr const & get_and_then_tac_fn();
|
||||
expr const & get_or_else_tac_fn();
|
||||
expr const & get_id_tac_fn();
|
||||
expr const & get_repeat_tac_fn();
|
||||
expr const & get_determ_tac_fn();
|
||||
|
||||
expr mk_tactic_macro(name const & kind, unsigned num_args, expr const * args);
|
||||
expr mk_tactic_macro(name const & kind, expr const & e);
|
||||
bool is_tactic_macro(expr const & e);
|
||||
expr mk_apply_tactic_macro(expr const & e);
|
||||
|
||||
/** \brief Exception used to report a problem when an expression is being converted into a tactic. */
|
||||
class expr_to_tactic_exception : public tactic_exception {
|
||||
public:
|
||||
|
|
@ -54,7 +60,8 @@ public:
|
|||
expr_to_tactic_exception(expr const & e, sstream const & strm):tactic_exception(e, strm) {}
|
||||
};
|
||||
|
||||
typedef std::function<tactic(type_checker & tc, expr const & e, pos_info_provider const *)> expr_to_tactic_fn;
|
||||
typedef std::function<tactic(type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *)>
|
||||
expr_to_tactic_fn;
|
||||
|
||||
/** \brief Register a new "procedural attachment" for expr_to_tactic. */
|
||||
void register_tac(name const & n, expr_to_tactic_fn const & fn);
|
||||
|
|
|
|||
|
|
@ -92,6 +92,12 @@ bool goal::validate(environment const & env) const {
|
|||
}
|
||||
}
|
||||
|
||||
list<expr> goal::to_context() const {
|
||||
buffer<expr> locals;
|
||||
get_app_rev_args(m_meta, locals);
|
||||
return to_list(locals.begin(), locals.end());
|
||||
}
|
||||
|
||||
DECL_UDATA(goal)
|
||||
|
||||
static int mk_goal(lua_State * L) { return push_goal(L, goal(to_expr(L, 1), to_expr(L, 2))); }
|
||||
|
|
|
|||
|
|
@ -44,32 +44,34 @@ public:
|
|||
|
||||
expr get_mvar() const { return get_app_fn(m_meta); }
|
||||
|
||||
/**
|
||||
\brief Given a term \c v with type get_type(), build a lambda abstraction
|
||||
/** \brief Given a term \c v with type get_type(), build a lambda abstraction
|
||||
that is the solution for the metavariable associated with this goal.
|
||||
*/
|
||||
expr abstract(expr const & v) const;
|
||||
|
||||
/**
|
||||
\brief Create a metavariable application <tt>(?m l_1 ... l_n)</tt> with the given type,
|
||||
/** \brief Create a metavariable application <tt>(?m l_1 ... l_n)</tt> with the given type,
|
||||
and the locals from this goal. If <tt>only_contextual == true</tt>, then we only include
|
||||
the local constants that are marked as contextual.
|
||||
*/
|
||||
expr mk_meta(name const & m, expr const & type, bool only_contextual = true) const;
|
||||
|
||||
/**
|
||||
brief Return true iff get_type() only contains local constants that arguments
|
||||
/** \brief Return true iff get_type() only contains local constants that arguments
|
||||
of get_meta(), and each argument of get_meta() only contains local constants
|
||||
that are previous arguments.
|
||||
*/
|
||||
bool validate_locals() const;
|
||||
|
||||
/**
|
||||
\brief Return true iff \c validate_locals() return true and type of \c get_meta() in
|
||||
/** \brief Return true iff \c validate_locals() return true and type of \c get_meta() in
|
||||
\c env is get_type()
|
||||
*/
|
||||
bool validate(environment const & env) const;
|
||||
|
||||
/** \brief Return the goal's "context".
|
||||
That is, given <tt>?m l_1 ... l_n</tt>, return the list
|
||||
<tt>[l_n, ..., l_1]</tt>
|
||||
*/
|
||||
list<expr> to_context() const;
|
||||
|
||||
format pp(formatter const & fmt) const;
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -30,6 +30,15 @@ bool get_proof_state_goal_names(options const & opts) {
|
|||
return opts.get_bool(*g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES);
|
||||
}
|
||||
|
||||
proof_state::proof_state(goals const & gs, substitution const & s,
|
||||
name_generator const & ngen, constraints const & postponed):
|
||||
m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed) {
|
||||
if (std::any_of(gs.begin(), gs.end(),
|
||||
[&](goal const & g) { return s.is_assigned(g.get_mvar()); })) {
|
||||
m_goals = filter(gs, [&](goal const & g) { return !s.is_assigned(g.get_mvar()); });
|
||||
}
|
||||
}
|
||||
|
||||
format proof_state::pp(formatter const & fmt) const {
|
||||
options const & opts = fmt.get_options();
|
||||
bool show_goal_names = get_proof_state_goal_names(opts);
|
||||
|
|
@ -67,8 +76,12 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state cons
|
|||
return out;
|
||||
}
|
||||
|
||||
proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen) {
|
||||
return proof_state(goals(goal(meta, type)), subst, ngen, constraints());
|
||||
}
|
||||
|
||||
proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen) {
|
||||
return proof_state(goals(goal(meta, type)), substitution(), ngen);
|
||||
return to_proof_state(meta, type, substitution(), ngen);
|
||||
}
|
||||
|
||||
DECL_UDATA(goals)
|
||||
|
|
@ -148,10 +161,11 @@ static int mk_proof_state(lua_State * L) {
|
|||
int nargs = lua_gettop(L);
|
||||
if (nargs == 2) {
|
||||
return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2)));
|
||||
} else if (nargs == 3) {
|
||||
} else if (nargs == 3 && is_proof_state(L, 1)) {
|
||||
return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3)));
|
||||
} else if (nargs == 4) {
|
||||
return push_proof_state(L, proof_state(to_goals(L, 1), to_substitution(L, 2), to_name_generator(L, 3)));
|
||||
} else if (nargs == 3) {
|
||||
return push_proof_state(L, proof_state(to_goals(L, 1), to_substitution(L, 2), to_name_generator(L, 3),
|
||||
constraints()));
|
||||
} else {
|
||||
throw exception("proof_state invalid number of arguments");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -19,16 +19,20 @@ class proof_state {
|
|||
goals m_goals;
|
||||
substitution m_subst;
|
||||
name_generator m_ngen;
|
||||
constraints m_postponed;
|
||||
public:
|
||||
proof_state(goals const & gs, substitution const & s, name_generator const & ngen):
|
||||
m_goals(gs), m_subst(s), m_ngen(ngen) {}
|
||||
proof_state(proof_state const & s, goals const & gs, substitution const & subst):proof_state(gs, subst, s.m_ngen) {}
|
||||
proof_state(proof_state const & s, goals const & gs):proof_state(s, gs, s.m_subst) {}
|
||||
proof_state(proof_state const & s, name_generator const & ngen):proof_state(s.m_goals, s.m_subst, ngen) {}
|
||||
proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed);
|
||||
proof_state(proof_state const & s, goals const & gs, substitution const & subst):
|
||||
proof_state(gs, subst, s.m_ngen, s.m_postponed) {}
|
||||
proof_state(proof_state const & s, goals const & gs):
|
||||
proof_state(s, gs, s.m_subst) {}
|
||||
proof_state(proof_state const & s, name_generator const & ngen):
|
||||
proof_state(s.m_goals, s.m_subst, ngen, s.m_postponed) {}
|
||||
|
||||
goals const & get_goals() const { return m_goals; }
|
||||
substitution const & get_subst() const { return m_subst; }
|
||||
name_generator const & get_ngen() const { return m_ngen; }
|
||||
constraints const & get_postponed() const { return m_postponed; }
|
||||
|
||||
/** \brief Return true iff this state does not have any goals left */
|
||||
bool is_final_state() const { return empty(m_goals); }
|
||||
|
|
@ -38,6 +42,7 @@ public:
|
|||
inline optional<proof_state> some_proof_state(proof_state const & s) { return some(s); }
|
||||
inline optional<proof_state> none_proof_state() { return optional<proof_state> (); }
|
||||
|
||||
proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen);
|
||||
proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen);
|
||||
|
||||
goals map_goals(proof_state const & s, std::function<optional<goal>(goal const & g)> f);
|
||||
|
|
|
|||
|
|
@ -14,6 +14,11 @@ Author: Leonardo de Moura
|
|||
#include "library/tactic/proof_state.h"
|
||||
|
||||
namespace lean {
|
||||
/** \brief Function for elaborating expressions nested in tactics.
|
||||
Some tactics contain nested expression (aka pre-terms) that need to be elaborated.
|
||||
*/
|
||||
typedef std::function<pair<expr, constraints>(goal const &, name_generator const &, expr const &)> elaborate_fn;
|
||||
|
||||
/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */
|
||||
void check_has_no_local(expr const & v, expr const & e, char const * tac_name);
|
||||
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ axiom H1 : a = b
|
|||
axiom H2 : b = c
|
||||
|
||||
check have e1 [visible] : a = b, from H1,
|
||||
have e2 : a = c, by apply trans; apply e1; apply H2,
|
||||
have e2 : a = c, by apply trans; apply H2; apply e1,
|
||||
have e3 : c = a, from e2⁻¹,
|
||||
have e4 [visible] : b = a, from e1⁻¹,
|
||||
have e5 : b = c, from e4 ⬝ e2,
|
||||
|
|
|
|||
9
tests/lean/run/beginend.lean
Normal file
9
tests/lean/run/beginend.lean
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
import tools.tactic
|
||||
open tactic
|
||||
|
||||
theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
|
||||
begin
|
||||
apply eq.trans,
|
||||
apply Hbc,
|
||||
apply Hab
|
||||
end
|
||||
|
|
@ -3,7 +3,7 @@ open tactic
|
|||
|
||||
theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
|
||||
:= by apply iff.intro;
|
||||
apply (assume Hb, iff.elim_right H Hb);
|
||||
apply (assume Ha, iff.elim_left H Ha)
|
||||
apply (assume Ha, iff.elim_left H Ha);
|
||||
apply (assume Hb, iff.elim_right H Hb)
|
||||
|
||||
check tst
|
||||
|
|
|
|||
|
|
@ -5,5 +5,14 @@ theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
|
|||
:= have H1 [visible] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics
|
||||
from iff.elim_left H,
|
||||
by apply iff.intro;
|
||||
apply (assume Hb, iff.elim_right H Hb);
|
||||
apply (assume Ha, H1 Ha)
|
||||
apply (assume Ha, H1 Ha);
|
||||
apply (assume Hb, iff.elim_right H Hb)
|
||||
|
||||
theorem tst2 (a b : Prop) (H : a ↔ b) : b ↔ a
|
||||
:= have H1 [visible] : a → b,
|
||||
from iff.elim_left H,
|
||||
begin
|
||||
apply iff.intro,
|
||||
apply (assume Ha, H1 Ha),
|
||||
apply (assume Hb, iff.elim_right H Hb)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -3,9 +3,9 @@ open tactic
|
|||
|
||||
theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b
|
||||
:= by apply and.intro;
|
||||
assumption;
|
||||
apply not_intro;
|
||||
exact
|
||||
(assume Ha, or.elim H
|
||||
(assume Hna, @absurd _ false Ha Hna)
|
||||
(assume Hnb, @absurd _ false Hb Hnb));
|
||||
assumption
|
||||
(assume Hnb, @absurd _ false Hb Hnb))
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ open tactic
|
|||
theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
|
||||
begin
|
||||
apply and.intro,
|
||||
assumption,
|
||||
apply not_intro,
|
||||
assume Ha, or.elim H
|
||||
(assume Hna, @absurd _ false Ha Hna)
|
||||
(assume Hnb, @absurd _ false Hb Hnb),
|
||||
assumption
|
||||
(assume Hnb, @absurd _ false Hb Hnb)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -4,7 +4,10 @@ open tactic
|
|||
constant A : Type.{1}
|
||||
constant f : A → A → A
|
||||
|
||||
theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
|
||||
:= by apply (@congr A A _ _ (f a) (f b));
|
||||
apply (congr_arg f);
|
||||
!assumption
|
||||
theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c :=
|
||||
begin
|
||||
apply (@congr A A _ _ (f a) (f b)),
|
||||
assumption,
|
||||
apply (congr_arg f),
|
||||
assumption
|
||||
end
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ constant A : Type.{1}
|
|||
constant f : A → A → A
|
||||
|
||||
theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
|
||||
:= by apply (@congr A A);
|
||||
:= by apply (eq.subst H1);
|
||||
apply (eq.subst H2);
|
||||
apply eq.refl;
|
||||
assumption
|
||||
apply eq.refl
|
||||
|
|
|
|||
|
|
@ -2,7 +2,6 @@ import logic
|
|||
open tactic
|
||||
|
||||
theorem tst {A : Type} {f : A → A → A} {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
|
||||
:= by apply congr;
|
||||
apply (eq.subst H2);
|
||||
apply eq.refl;
|
||||
assumption
|
||||
:= by apply (eq.subst H2);
|
||||
apply (eq.subst H1);
|
||||
apply eq.refl
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ section
|
|||
check H
|
||||
check H2
|
||||
theorem test : a = b ∧ a = a
|
||||
:= by apply and.intro; apply H; apply eq.refl
|
||||
:= by apply and.intro; apply eq.refl; apply H
|
||||
end
|
||||
|
||||
check @test
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
import logic
|
||||
open tactic
|
||||
|
||||
theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A
|
||||
:= by (apply @and.intro;
|
||||
apply (show A, from H1);
|
||||
apply (show B ∧ A, from and.intro H2 H1))
|
||||
theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A :=
|
||||
by apply @and.intro;
|
||||
apply (show B ∧ A, from and.intro H2 H1);
|
||||
apply (show A, from H1)
|
||||
|
||||
check @tst
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ axiom H2 : b = c
|
|||
check show a = c, from H1 ⬝ H2
|
||||
print "------------"
|
||||
check have e1 [visible] : a = b, from H1,
|
||||
have e2 : a = c, by apply eq.trans; apply e1; apply H2,
|
||||
have e2 : a = c, by apply eq.trans; apply H2; apply e1,
|
||||
have e3 : c = a, from e2⁻¹,
|
||||
have e4 [visible] : b = a, from e1⁻¹,
|
||||
show b = c, from e1⁻¹ ⬝ e2
|
||||
|
|
|
|||
Loading…
Reference in a new issue