max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/old_tactic/tactic): remove old tactics that have already been ported to new tactic framework

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-25 13:21:07 -07:00
parent 1590807762
commit fb836d2d75
34 changed files with 0 additions and 2550 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

258
src/library/old_tactic/tactic/apply_tactic.cpp
View file

@ -1,258 +0,0 @@
/*
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include "util/lazy_list_fn.h"
#include "util/sstream.h"
#include "util/name_map.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/error_msgs.h"
#include "library/reducible.h"
#include "library/unifier.h"
#include "library/util.h"
#include "library/constants.h"
#include "library/class_instance_resolution.h"
#include "library/old_type_checker.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/apply_tactic.h"
#ifndef LEAN_DEFAULT_APPLY_CLASS_INSTANCE
#define LEAN_DEFAULT_APPLY_CLASS_INSTANCE true
#endif
namespace lean {
static name * g_apply_class_instance = nullptr;
bool get_apply_class_instance(options const & opts) {
return opts.get_bool(*g_apply_class_instance, LEAN_DEFAULT_APPLY_CLASS_INSTANCE);
}
/**
\brief Given a sequence metas: <tt>(?m_1 ...) (?m_2 ... ) ... (?m_k ...)</tt>,
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) {
buffer<expr> mvars;
for (expr const & m : metas)
mvars.push_back(get_app_fn(m));
unsigned k = 0;
for (unsigned i = 0; i < metas.size(); i++) {
bool found = false;
for (unsigned j = 0; j < metas.size(); j++) {
if (j != i) {
if (occurs(mvars[i], mlocal_type(mvars[j]))) {
found = true;
break;
}
}
}
if (!found) {
metas[k] = metas[i];
k++;
}
}
metas.shrink(k);
}
enum subgoals_action_kind { IgnoreSubgoals, AddRevSubgoals, AddSubgoals, AddAllSubgoals };
enum add_meta_kind { DoNotAdd, AddDiff, AddAll };
static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s,
expr const & _e, buffer<constraint> & cs,
add_meta_kind add_meta, subgoals_action_kind subgoals_action,
optional<unifier_kind> const & uk = optional<unifier_kind>()) {
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return proof_state_seq();
}
bool class_inst = get_apply_class_instance(ios.get_options());
std::shared_ptr<old_type_checker> tc(mk_type_checker(env));
goal g = head(gs);
goals tail_gs = tail(gs);
expr t = g.get_type();
expr e = _e;
auto e_t_cs = tc->infer(e);
e_t_cs.second.linearize(cs);
expr e_t = e_t_cs.first;
buffer<expr> metas;
old_local_context ctx;
bool initialized_ctx = false;
unifier_config cfg(ios.get_options());
if (uk)
cfg.m_kind = *uk;
if (add_meta != DoNotAdd) {
unsigned num_e_t = get_expect_num_args(tc->get_type_context(), e_t);
if (add_meta == AddDiff) {
unsigned num_t = get_expect_num_args(tc->get_type_context(), t);
if (num_t <= num_e_t)
num_e_t -= num_t;
else
num_e_t = 0;
} else {
lean_assert(add_meta == AddAll);
}
for (unsigned i = 0; i < num_e_t; i++) {
auto e_t_cs = tc->whnf(e_t);
e_t_cs.second.linearize(cs);
e_t = e_t_cs.first;
expr meta;
if (class_inst && binding_info(e_t).is_inst_implicit()) {
if (!initialized_ctx) {
ctx = g.to_local_context();
initialized_ctx = true;
}
bool use_local_insts = true;
bool is_strict = false;
auto mc = mk_class_instance_elaborator(
env, ios, ctx, optional<name>(),
use_local_insts, is_strict,
some_expr(head_beta_reduce(binding_domain(e_t))), e.get_tag(), nullptr);
meta = mc.first;
cs.push_back(mc.second);
} else {
meta = g.mk_meta(mk_fresh_name(), head_beta_reduce(binding_domain(e_t)));
}
e = mk_app(e, meta);
e_t = instantiate(binding_body(e_t), meta);
metas.push_back(meta);
}
}
pair<bool, constraint_seq> dcs = tc->is_def_eq(t, e_t);
if (!dcs.first) {
throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {
format r = format("invalid 'apply' tactic, failed to unify");
r += pp_indent_expr(fmt, t);
r += compose(line(), format("with"));
r += pp_indent_expr(fmt, e_t);
return r;
});
return proof_state_seq();
}
dcs.second.linearize(cs);
unify_result_seq rseq = unify(env, cs.size(), cs.data(), s.get_subst(), cfg);
list<expr> meta_lst = to_list(metas.begin(), metas.end());
return map2<proof_state>(rseq, [=](pair<substitution, constraints> const & p) -> proof_state {
substitution const & subst = p.first;
constraints const & postponed = p.second;
substitution new_subst = subst;
expr new_e = new_subst.instantiate_all(e);
assign(new_subst, g, new_e);
goals new_gs = tail_gs;
if (subgoals_action != IgnoreSubgoals) {
buffer<expr> metas;
for (auto m : meta_lst) {
if (!new_subst.is_assigned(get_app_fn(m)))
metas.push_back(m);
}
if (subgoals_action == AddRevSubgoals) {
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);
} else {
lean_assert(subgoals_action == AddSubgoals || subgoals_action == AddAllSubgoals);
if (subgoals_action == AddSubgoals)
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);
}
}
}
return proof_state(s, new_gs, new_subst, postponed);
});
}
proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs) {
buffer<constraint> tmp_cs;
cs.linearize(tmp_cs);
return apply_tactic_core(env, ios, s, e, tmp_cs, AddDiff, AddSubgoals);
}
proof_state_seq fapply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs) {
buffer<constraint> tmp_cs;
cs.linearize(tmp_cs);
return apply_tactic_core(env, ios, s, e, tmp_cs, AddDiff, AddAllSubgoals);
}
tactic apply_tactic_core(expr const & e, constraint_seq const & cs) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
return apply_tactic_core(env, ios, s, e, cs);
});
}
tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, add_meta_kind add_meta, subgoals_action_kind k) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return proof_state_seq();
}
goal const & g = head(gs);
expr new_e; substitution new_subst; constraints cs_;
try {
auto ecs = elab(g, ios.get_options(), e, none_expr(), s.get_subst(), false);
std::tie(new_e, new_subst, cs_) = ecs;
buffer<constraint> cs;
to_buffer(cs_, cs);
to_buffer(s.get_postponed(), cs);
proof_state new_s(s, new_subst, constraints());
return apply_tactic_core(env, ios, new_s, new_e, cs, add_meta, k);
} catch (exception &) {
if (s.report_failure())
throw;
else
return proof_state_seq();
}
});
}
tactic apply_tactic(elaborate_fn const & elab, expr const & e) {
return apply_tactic_core(elab, e, AddDiff, AddSubgoals);
}
tactic fapply_tactic(elaborate_fn const & elab, expr const & e) {
return apply_tactic_core(elab, e, AddDiff, AddAllSubgoals);
}
tactic eapply_tactic(elaborate_fn const & elab, expr const & e) {
return apply_tactic_core(elab, e, AddAll, AddSubgoals);
}
void initialize_apply_tactic() {
g_apply_class_instance = new name{"apply", "class_instance"};
register_bool_option(*g_apply_class_instance, LEAN_DEFAULT_APPLY_CLASS_INSTANCE,
"(apply tactic) if true apply tactic uses class-instances "
"resolution for instance implicit arguments");
register_tac(get_tactic_apply_name(),
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument");
return apply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
});
register_tac(get_tactic_eapply_name(),
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
check_tactic_expr(app_arg(e), "invalid 'eapply' tactic, invalid argument");
return eapply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
});
register_tac(get_tactic_fapply_name(),
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
check_tactic_expr(app_arg(e), "invalid 'fapply' tactic, invalid argument");
return fapply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
});
}
void finalize_apply_tactic() {
delete g_apply_class_instance;
}
}

19
src/library/old_tactic/tactic/apply_tactic.h
View file

@ -1,19 +0,0 @@
/*
Copyright (c) 2013-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 "library/tactic/elaborate.h"
namespace lean {
proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs);
proof_state_seq fapply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs);
tactic apply_tactic_core(expr const & e, constraint_seq const & cs = constraint_seq());
tactic apply_tactic(elaborate_fn const & fn, expr const & e);
tactic fapply_tactic(elaborate_fn const & fn, expr const & e);
tactic eassumption_tactic();
tactic assumption_tactic();
void initialize_apply_tactic();
void finalize_apply_tactic();
}

61
src/library/old_tactic/tactic/assert_tactic.cpp
View file

@ -1,61 +0,0 @@
/*
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 "util/fresh_name.h"
#include "kernel/abstract.h"
#include "library/constants.h"
#include "library/tactic/tactic.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
expr mk_assert_tactic_expr(name const & id, expr const & e) {
return mk_app(mk_constant(get_tactic_assert_hypothesis_name()),
mk_constant(id), e);
}
tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
proof_state new_s = s;
goals const & gs = new_s.get_goals();
if (!gs) {
throw_no_goal_if_enabled(s);
return none_proof_state();
}
bool report_unassigned = true;
if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, none_expr(), report_unassigned)) {
goals const & gs = new_s.get_goals();
goal const & g = head(gs);
expr new_meta1 = g.mk_meta(mk_fresh_name(), *new_e);
goal new_goal1(new_meta1, *new_e);
expr new_local = mk_local(mk_fresh_name(), id, *new_e, binder_info());
buffer<expr> hyps;
g.get_hyps(hyps);
hyps.push_back(new_local);
expr new_mvar2 = mk_metavar(mk_fresh_name(), Pi(hyps, g.get_type()));
hyps.pop_back();
expr new_meta2_core = mk_app(new_mvar2, hyps);
expr new_meta2 = mk_app(new_meta2_core, new_local);
goal new_goal2(new_meta2, g.get_type());
substitution new_subst = new_s.get_subst();
assign(new_subst, g, mk_app(new_meta2_core, new_meta1));
return some_proof_state(proof_state(new_s, cons(new_goal1, cons(new_goal2, tail(gs))), new_subst));
}
return none_proof_state();
});
}
void initialize_assert_tactic() {
register_tac(get_tactic_assert_hypothesis_name(),
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'assert' tactic, argument must be an identifier");
check_tactic_expr(app_arg(e), "invalid 'assert' tactic, argument must be an expression");
return assert_tactic(fn, id, get_tactic_expr_expr(app_arg(e)));
});
}
void finalize_assert_tactic() {
}
}

15
src/library/old_tactic/tactic/assert_tactic.h
View file

@ -1,15 +0,0 @@
/*
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 "library/tactic/tactic.h"
namespace lean {
expr mk_assert_tactic_expr(name const & id, expr const & e);
tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e);
void initialize_assert_tactic();
void finalize_assert_tactic();
}

73
src/library/old_tactic/tactic/clear_tactic.cpp
View file

@ -1,73 +0,0 @@
/*
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 "util/fresh_name.h"
#include "library/constants.h"
#include "kernel/abstract.h"
#include "library/locals.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
tactic clear_tactic(name const & n) {
auto fn = [=](environment const &, io_state const &, proof_state const & _s) -> optional<proof_state> {
if (!_s.get_goals()) {
throw_no_goal_if_enabled(_s);
return none_proof_state();
}
proof_state s = apply_substitution(_s);
goals const & gs = s.get_goals();
goal g = head(gs);
goals tail_gs = tail(gs);
if (auto p = g.find_hyp(n)) {
expr const & h = p->first;
unsigned i = p->second;
buffer<expr> hyps;
g.get_hyps(hyps);
hyps.erase(hyps.size() - i - 1);
if (depends_on(g.get_type(), h)) {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'clear' tactic, conclusion depends on '"
<< n << "'");
return none_proof_state();
}
if (auto h2 = depends_on(i, hyps.end() - i, h)) {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'clear' tactic, hypothesis '" << *h2
<< "' depends on '" << n << "'");
return none_proof_state();
}
expr new_type = g.get_type();
expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps);
goal new_g(new_meta, new_type);
substitution new_subst = s.get_subst();
assign(new_subst, g, new_meta);
proof_state new_s(s, goals(new_g, tail_gs), new_subst);
return some_proof_state(new_s);
} else {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'clear' tactic, goal does not have a hypothesis "
<< " named '" << n << "'");
return none_proof_state();
}
};
return tactic01(fn);
}
void initialize_clear_tactic() {
auto fn = [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
buffer<name> ns;
get_tactic_id_list_elements(app_arg(e), ns, "invalid 'clears' tactic, list of identifiers expected");
tactic r = clear_tactic(ns.back());
ns.pop_back();
while (!ns.empty()) {
r = then(clear_tactic(ns.back()), r);
ns.pop_back();
}
return r;
};
register_tac(get_tactic_clear_name(), fn);
register_tac(get_tactic_clears_name(), fn);
}
void finalize_clear_tactic() {}
}

14
src/library/old_tactic/tactic/clear_tactic.h
View file

@ -1,14 +0,0 @@
/*
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 "library/tactic/tactic.h"
namespace lean {
tactic clear_tactic(name const & n);
void initialize_clear_tactic();
void finalize_clear_tactic();
}

142
src/library/old_tactic/tactic/constructor_tactic.cpp
View file

@ -1,142 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/lazy_list_fn.h"
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "library/constants.h"
#include "library/util.h"
#include "library/reducible.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/apply_tactic.h"
namespace lean {
/**
\brief Implement multiple variations of the constructor tactic.
It tries to solve the goal by applying the i-th constructor.
If \c num_constructors is not none, then the tactic checks wether the inductive datatype has
the expected number of constructors.
If \c given_args is provided, then the tactic fixes the given arguments.
It creates a subgoal for each remaining argument.
*/
tactic constructor_tactic(elaborate_fn const & elab, optional<unsigned> _i, optional<unsigned> num_constructors,
list<expr> const & given_args, bool use_fapply = false) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return proof_state_seq();
}
constraint_seq cs;
auto tc = mk_type_checker(env);
goal const & g = head(gs);
expr t = tc->whnf(g.get_type(), cs);
buffer<expr> I_args;
expr I = get_app_args(t, I_args);
if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I))) {
throw_tactic_exception_if_enabled(s, "invalid 'constructor' tactic, goal is not an inductive datatype");
return proof_state_seq();
}
buffer<name> c_names;
get_intro_rule_names(env, const_name(I), c_names);
if (num_constructors && c_names.size() != *num_constructors) {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, goal is an inductive datatype, "
<< "but it does not have " << *num_constructors << " constructor(s)");
return proof_state_seq();
}
auto try_constructor = [&](proof_state const & s, unsigned i) {
if (i >= c_names.size()) {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, goal is an inductive datatype, "
<< "but it has only " << c_names.size() << " constructor(s)");
return proof_state_seq();
}
expr C = mk_constant(c_names[i], const_levels(I));
unsigned num_params = *inductive::get_num_params(env, const_name(I));
if (I_args.size() < num_params)
return proof_state_seq();
proof_state new_s(s);
C = mk_app(C, num_params, I_args.data());
expr C_type = tc->whnf(tc->infer(C, cs), cs);
bool report_unassigned = true;
bool enforce_type = true;
for (expr const & arg : given_args) {
if (!is_pi(C_type)) {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, "
<< "too many arguments have been provided");
return proof_state_seq();
}
try {
if (auto new_arg = elaborate_with_respect_to(env, ios, elab, new_s, arg, some_expr(binding_domain(C_type)),
report_unassigned, enforce_type)) {
C = mk_app(C, *new_arg);
C_type = tc->whnf(instantiate(binding_body(C_type), *new_arg), cs);
} else {
return proof_state_seq();
}
} catch (exception &) {
if (new_s.report_failure())
throw;
return proof_state_seq();
}
}
if (use_fapply)
return fapply_tactic_core(env, ios, new_s, C, cs);
else
return apply_tactic_core(env, ios, new_s, C, cs);
};
if (_i) {
if (*_i == 0) {
throw_tactic_exception_if_enabled(s, "invalid 'constructor' tactic, index must be greater than zero");
return proof_state_seq();
}
return try_constructor(s, *_i - 1);
} else {
proof_state new_s = s.update_report_failure(false);
proof_state_seq r;
for (unsigned i = 0; i < c_names.size(); i++)
r = append(r, try_constructor(new_s, i));
return r;
}
};
return tactic(fn);
}
void initialize_constructor_tactic() {
register_tac(name{"tactic", "constructor"},
[](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
auto i = get_optional_unsigned(tc, app_arg(e));
return constructor_tactic(fn, i, optional<unsigned>(), list<expr>());
});
register_tac(name{"tactic", "fconstructor"},
[](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
auto i = get_optional_unsigned(tc, app_arg(e));
return constructor_tactic(fn, i, optional<unsigned>(), list<expr>(), true);
});
register_tac(name{"tactic", "split"},
[](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
return constructor_tactic(fn, optional<unsigned>(1), optional<unsigned>(1), list<expr>());
});
register_tac(name{"tactic", "left"},
[](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
return constructor_tactic(fn, optional<unsigned>(1), optional<unsigned>(2), list<expr>());
});
register_tac(name{"tactic", "right"},
[](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
return constructor_tactic(fn, optional<unsigned>(2), optional<unsigned>(2), list<expr>());
});
register_tac(name{"tactic", "existsi"},
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
check_tactic_expr(app_arg(e), "invalid 'existsi' tactic, invalid argument");
expr arg = get_tactic_expr_expr(app_arg(e));
return constructor_tactic(fn, optional<unsigned>(1), optional<unsigned>(1), list<expr>(arg));
});
}
void finalize_constructor_tactic() {
}
}

11
src/library/old_tactic/tactic/constructor_tactic.h
View file

@ -1,11 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
namespace lean {
void initialize_constructor_tactic();
void finalize_constructor_tactic();
}

94
src/library/old_tactic/tactic/contradiction_tactic.cpp
View file

@ -1,94 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/inductive/inductive.h"
#include "library/constants.h"
#include "library/util.h"
#include "library/reducible.h"
#include "library/tactic/intros_tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "kernel/kernel_exception.h"
namespace lean {
tactic contradiction_tactic() {
auto fn = [=](environment const & env, io_state const &, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return optional<proof_state>();
}
goal const & g = head(gs);
expr const & t = g.get_type();
substitution subst = s.get_subst();
auto tc = mk_type_checker(env);
auto conserv_tc = mk_type_checker(env, UnfoldReducible);
buffer<expr> hyps;
g.get_hyps(hyps);
for (expr const & h : hyps) {
expr h_type = mlocal_type(h);
h_type = tc->whnf(h_type).first;
expr lhs, rhs, arg;
if (is_false(env, h_type)) {
assign(subst, g, mk_false_rec(*tc, h, t));
return some_proof_state(proof_state(s, tail(gs), subst));
} else if (is_not(env, h_type, arg)) {
optional<expr> h_pos;
for (expr const & h_prime : hyps) {
constraint_seq cs;
if (conserv_tc->is_def_eq(arg, mlocal_type(h_prime), justification(), cs) && !cs) {
h_pos = h_prime;
break;
}
}
if (h_pos) {
assign(subst, g, mk_absurd(*tc, t, *h_pos, h));
return some_proof_state(proof_state(s, tail(gs), subst));
}
} else if (is_eq(h_type, lhs, rhs)) {
lhs = tc->whnf(lhs).first;
rhs = tc->whnf(rhs).first;
optional<name> lhs_c = is_constructor_app(env, lhs);
optional<name> rhs_c = is_constructor_app(env, rhs);
if (lhs_c && rhs_c && *lhs_c != *rhs_c) {
if (optional<name> I_name = inductive::is_intro_rule(env, *lhs_c)) {
name no_confusion(*I_name, "no_confusion");
try {
expr I = tc->whnf(tc->infer(lhs).first).first;
buffer<expr> args;
expr I_fn = get_app_args(I, args);
if (is_constant(I_fn)) {
level t_lvl = sort_level(tc->ensure_type(t).first);
expr V = mk_app(mk_app(mk_constant(no_confusion, cons(t_lvl, const_levels(I_fn))), args),
t, lhs, rhs, h);
if (auto r = lift_down_if_hott(*tc, V)) {
check_term(*tc, *r);
assign(subst, g, *r);
return some_proof_state(proof_state(s, tail(gs), subst));
}
}
} catch (kernel_exception & ex) {
// TODO(Leo)
// regular(env, ios) << ex << "\n";
}
}
}
}
}
return none_proof_state();
};
return tactic01(fn);
}
void initialize_contradiction_tactic() {
register_tac(name{"tactic", "contradiction"},
[](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
list<name> empty;
return then(orelse(intros_tactic(empty), id_tactic()), contradiction_tactic());
});
}
void finalize_contradiction_tactic() {
}
}

11
src/library/old_tactic/tactic/contradiction_tactic.h
View file

@ -1,11 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
namespace lean {
void initialize_contradiction_tactic();
void finalize_contradiction_tactic();
}

171
src/library/old_tactic/tactic/exact_tactic.cpp
View file

@ -1,171 +0,0 @@
/*
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 "kernel/type_checker.h"
#include "kernel/for_each_fn.h"
#include "kernel/error_msgs.h"
#include "library/util.h"
#include "library/constants.h"
#include "library/reducible.h"
#include "library/tactic/tactic.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
// Return true iff \c e is of the form (?m l_1 ... l_n), where ?m is a metavariable and l_i's local constants
bool is_meta_placeholder(expr const & e) {
if (!is_meta(e))
return false;
buffer<expr> args;
get_app_args(e, args);
return std::all_of(args.begin(), args.end(), is_local);
}
tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type_during_elaboration, bool allow_metavars,
bool conservative) {
return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
proof_state new_s = s;
goals const & gs = new_s.get_goals();
if (!gs) {
throw_no_goal_if_enabled(s);
return none_proof_state();
}
expr t = head(gs).get_type();
bool report_unassigned = !allow_metavars && enforce_type_during_elaboration && s.report_failure();
optional<expr> new_e;
try {
new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t),
report_unassigned, enforce_type_during_elaboration,
conservative);
} catch (exception &) {
if (s.report_failure())
throw;
else
return none_proof_state();
}
if (new_e) {
goals const & gs = new_s.get_goals();
if (gs) {
goal const & g = head(gs);
if (!allow_metavars && has_expr_metavar_relaxed(*new_e)) {
throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {
format r = format("invalid 'exact' tactic, term still contains metavariables "
"after elaboration");
r += pp_indent_expr(fmt, *new_e);
return r;
});
return none_proof_state();
}
substitution subst = new_s.get_subst();
assign(subst, g, *new_e);
if (allow_metavars) {
buffer<goal> new_goals;
auto tc = mk_type_checker(env);
for_each(*new_e, [&](expr const & m, unsigned) {
if (!has_expr_metavar(m))
return false;
if (is_meta_placeholder(m)) {
new_goals.push_back(goal(m, tc->infer(m).first));
return false;
}
return !is_metavar(m) && !is_local(m);
});
goals new_gs = to_list(new_goals.begin(), new_goals.end(), tail(gs));
return some(proof_state(new_s, new_gs, subst));
} else {
return some(proof_state(new_s, tail(gs), subst));
}
} else {
return some_proof_state(new_s);
}
}
return none_proof_state();
});
}
static tactic assumption_tactic_core(bool conservative) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return proof_state_seq();
}
proof_state new_s = s.update_report_failure(false);
optional<tactic> tac;
goal g = head(gs);
buffer<expr> hs;
g.get_hyps(hs);
auto elab = [](goal const &, options const &, expr const & H,
optional<expr> const &, substitution const & s, bool) -> elaborate_result {
return elaborate_result(H, s, constraints());
};
unsigned i = hs.size();
while (i > 0) {
--i;
expr const & h = hs[i];
tactic curr = exact_tactic(elab, h, false, false, conservative);
if (tac) {
tac = orelse(*tac, curr);
} else {
tac = curr;
}
}
if (tac) {
return (*tac)(env, ios, s);
} else {
return proof_state_seq();
}
});
}
tactic eassumption_tactic() {
return assumption_tactic_core(false);
}
tactic assumption_tactic() {
return assumption_tactic_core(true);
}
static expr * g_exact_tac_fn = nullptr;
static expr * g_rexact_tac_fn = nullptr;
static expr * g_refine_tac_fn = nullptr;
expr const & get_exact_tac_fn() { return *g_exact_tac_fn; }
expr const & get_rexact_tac_fn() { return *g_rexact_tac_fn; }
expr const & get_refine_tac_fn() { return *g_refine_tac_fn; }
void initialize_exact_tactic() {
name const & exact_tac_name = get_tactic_exact_name();
name const & rexact_tac_name = get_tactic_rexact_name();
name const & refine_tac_name = get_tactic_refine_name();
g_exact_tac_fn = new expr(Const(exact_tac_name));
g_rexact_tac_fn = new expr(Const(rexact_tac_name));
g_refine_tac_fn = new expr(Const(refine_tac_name));
register_tac(exact_tac_name,
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument");
return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true, false, false);
});
register_tac(rexact_tac_name,
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
check_tactic_expr(app_arg(e), "invalid 'rexact' tactic, invalid argument");
return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), false, false, false);
});
register_tac(refine_tac_name,
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
check_tactic_expr(app_arg(e), "invalid 'refine' tactic, invalid argument");
return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true, true, false);
});
register_simple_tac(get_tactic_eassumption_name(),
[]() { return eassumption_tactic(); });
register_simple_tac(get_tactic_assumption_name(),
[]() { return assumption_tactic(); });
}
void finalize_exact_tactic() {
delete g_exact_tac_fn;
delete g_rexact_tac_fn;
delete g_refine_tac_fn;
}
}

16
src/library/old_tactic/tactic/exact_tactic.h
View file

@ -1,16 +0,0 @@
/*
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 "library/tactic/tactic.h"
namespace lean {
expr const & get_exact_tac_fn();
expr const & get_rexact_tac_fn();
/** \brief Solve first goal iff it is definitionally equal to type of \c e */
void initialize_exact_tactic();
void finalize_exact_tactic();
}

43
src/library/old_tactic/tactic/exfalso_tactic.cpp
View file

@ -1,43 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/inductive/inductive.h"
#include "library/constants.h"
#include "library/util.h"
#include "library/reducible.h"
#include "library/tactic/intros_tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "kernel/kernel_exception.h"
namespace lean {
tactic exfalso_tactic() {
auto fn = [=](environment const & env, io_state const &, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return optional<proof_state>();
}
goal const & g = head(gs);
expr const & t = g.get_type();
substitution subst = s.get_subst();
auto tc = mk_type_checker(env);
expr false_expr = mk_false(env);
expr new_meta = g.mk_meta(mk_fresh_name(), false_expr);
goal new_goal(new_meta, false_expr);
assign(subst, g, mk_false_rec(*tc, new_meta, t));
return some(proof_state(s, goals(new_goal, tail(gs)), subst));
};
return tactic01(fn);
}
void initialize_exfalso_tactic() {
register_tac(name{"tactic", "exfalso"},
[](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
return exfalso_tactic();
});
}
void finalize_exfalso_tactic() {
}
}

11
src/library/old_tactic/tactic/exfalso_tactic.h
View file

@ -1,11 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
namespace lean {
void initialize_exfalso_tactic();
void finalize_exfalso_tactic();
}

246
src/library/old_tactic/tactic/injection_tactic.cpp
View file

@ -1,246 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/fresh_name.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/inductive/inductive.h"
#include "library/constants.h"
#include "library/util.h"
#include "library/old_util.h"
#include "library/reducible.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/apply_tactic.h"
#include "library/tactic/clear_tactic.h"
namespace lean {
tactic injection_tactic_core(expr const & e, unsigned num, list<name> const & ids, bool report_errors);
// Return true iff lhs and rhs are of the form (f ...) f is a constructor
bool is_injection_target(old_type_checker & tc, expr lhs, expr rhs) {
environment const & env = tc.env();
lhs = tc.whnf(lhs).first;
rhs = tc.whnf(rhs).first;
expr A = tc.whnf(tc.infer(lhs).first).first;
expr const & I = get_app_fn(A);
if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I)))
return false;
expr lhs_fn = get_app_fn(lhs);
expr rhs_fn = get_app_fn(rhs);
return
is_constant(lhs_fn) && is_constant(rhs_fn) &&
const_name(lhs_fn) == const_name(rhs_fn) &&
inductive::is_intro_rule(env, const_name(lhs_fn));
}
/** \brief Introduce num hypotheses, if _ns is not nil use it to name the hypothesis,
New hypothesis of the form (a = a) and (a == a) are discarded.
New hypothesis of the form (a == b) where (a b : A), are converted into (a = b).
*/
tactic intros_num_tactic(unsigned num, list<name> _ns) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
if (num == 0)
return proof_state_seq(s);
list<name> ns = _ns;
goals const & gs = s.get_goals();
if (empty(gs))
return proof_state_seq();
goal const & g = head(gs);
auto tc = mk_type_checker(env);
expr t = g.get_type();
expr m = g.get_meta();
auto mk_name = [&](name const & n) {
if (is_nil(ns)) {
return g.get_unused_name(n);
} else {
name r = head(ns);
ns = tail(ns);
return r;
}
};
auto keep_hyp = [&]() {
expr H = mk_local(mk_name(binding_name(t)), binding_domain(t));
t = instantiate(binding_body(t), H);
m = mk_app(m, H);
proof_state new_s(s, cons(goal(m, t), tail(gs)));
return intros_num_tactic(num-1, ns)(env, ios, new_s);
};
auto discard_hyp = [&]() {
expr new_meta = g.mk_meta(mk_fresh_name(), binding_body(t));
goal new_goal(new_meta, binding_body(t));
substitution new_subst = s.get_subst();
assign(new_subst, g, mk_lambda(binding_name(t), binding_domain(t), new_meta));
proof_state new_s(s, cons(new_goal, tail(gs)), new_subst);
return intros_num_tactic(num-1, ns)(env, ios, new_s);
};
t = tc->ensure_pi(t).first;
// if goal depends on hypothesis, we keep it
if (!closed(binding_body(t)))
return keep_hyp();
constraint_seq cs;
expr Htype = tc->whnf(binding_domain(t), cs);
// new unification constraints were generated, so we keep hypothesis
if (cs)
return keep_hyp();
expr lhs, rhs;
if (is_eq(Htype, lhs, rhs)) {
// equalities of the form (a = a) are discarded
if (tc->is_def_eq(lhs, rhs, justification(), cs) && !cs) {
return discard_hyp();
} else if (is_injection_target(*tc, lhs, rhs)) {
// apply injection recursively
name Hname = mk_fresh_name();
expr H = mk_local(Hname, binding_domain(t));
t = binding_body(t);
m = mk_app(m, H);
proof_state new_s(s, cons(goal(m, t), tail(gs)));
return then(injection_tactic_core(H, num-1, ns, false),
clear_tactic(Hname))(env, ios, new_s);
} else {
return keep_hyp();
}
}
expr A, B;
if (is_standard(env) && is_heq(Htype, A, lhs, B, rhs)) {
if (tc->is_def_eq(A, B, justification(), cs) && !cs) {
// since types A and B are definitionally equal, we convert to homogeneous
expr new_eq = mk_eq(*tc, lhs, rhs);
expr new_type = mk_pi(binding_name(t), new_eq, binding_body(t));
expr new_meta = g.mk_meta(mk_fresh_name(), new_type);
goal new_goal(new_meta, new_type);
expr H = mk_local(mk_fresh_name(), binding_domain(t));
levels heq_lvl = const_levels(get_app_fn(Htype));
expr arg = mk_app(mk_constant(get_eq_of_heq_name(), heq_lvl), A, lhs, rhs, H);
expr V = Fun(H, mk_app(new_meta, arg));
substitution new_subst = s.get_subst();
assign(new_subst, g, V);
proof_state new_s(s, cons(new_goal, tail(gs)), new_subst);
return intros_num_tactic(num, ns)(env, ios, new_s);
} else {
return keep_hyp();
}
}
// hypothesis is not an equality
return keep_hyp();
};
return tactic(fn);
}
tactic injection_tactic_core(expr const & e, unsigned num, list<name> const & ids, bool report_errors) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
if (!gs) {
throw_no_goal_if_enabled(s);
return proof_state_seq();
}
expr t = head(gs).get_type();
constraint_seq cs;
auto tc = mk_type_checker(env);
expr e_type = tc->whnf(tc->infer(e, cs), cs);
expr lhs, rhs;
if (!is_eq(e_type, lhs, rhs)) {
if (report_errors) {
throw_tactic_exception_if_enabled(s, "invalid 'injection' tactic, "
"given argument is not an equality proof");
return proof_state_seq();
}
return intros_num_tactic(num, ids)(env, ios, s);
}
lhs = tc->whnf(lhs, cs);
rhs = tc->whnf(rhs, cs);
expr A = tc->whnf(tc->infer(lhs, cs), cs);
buffer<expr> I_args;
expr I = get_app_args(A, I_args);
if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I))) {
if (report_errors) {
throw_tactic_exception_if_enabled(s, "invalid 'injection' tactic, "
"it is not an equality between inductive values");
return proof_state_seq();
}
return intros_num_tactic(num, ids)(env, ios, s);
}
expr lhs_fn = get_app_fn(lhs);
expr rhs_fn = get_app_fn(rhs);
if (!is_constant(lhs_fn) || !is_constant(rhs_fn) || const_name(lhs_fn) != const_name(rhs_fn) ||
!inductive::is_intro_rule(env, const_name(lhs_fn))) {
if (report_errors) {
throw_tactic_exception_if_enabled(s, "invalid 'injection' tactic, "
"the given equality is not of the form (f ...) = (f ...) "
"where f is a constructor");
return proof_state_seq();
}
return intros_num_tactic(num, ids)(env, ios, s);
}
unsigned num_params = *inductive::get_num_params(env, const_name(I));
unsigned cnstr_arity = get_arity(env.get(const_name(lhs_fn)).get_type());
lean_assert(cnstr_arity >= num_params);
unsigned num_new_eqs = cnstr_arity - num_params;
level t_lvl = sort_level(tc->ensure_type(t, cs));
expr N = mk_constant(name(const_name(I), "no_confusion"), cons(t_lvl, const_levels(I)));
N = mk_app(mk_app(N, I_args), t, lhs, rhs, e);
proof_state new_s(s);
if (is_standard(env)) {
tactic tac = then(take(apply_tactic_core(N, cs), 1),
intros_num_tactic(num + num_new_eqs, ids));
return tac(env, ios, new_s);
} else {
level n_lvl = mk_meta_univ(mk_fresh_name());
expr lift_down = mk_app(mk_constant(get_lift_down_name(), {t_lvl, n_lvl}), t);
tactic tac = then(take(apply_tactic_core(lift_down), 1),
then(take(apply_tactic_core(N, cs), 1),
intros_num_tactic(num + num_new_eqs, ids)));
return tac(env, ios, new_s);
}
};
return tactic(fn);
};
tactic injection_tactic(elaborate_fn const & elab, expr const & e, list<name> const & ids) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
proof_state new_s = s;
goals const & gs = new_s.get_goals();
if (!gs) {
throw_no_goal_if_enabled(s);
return proof_state_seq();
}
expr t = head(gs).get_type();
bool report_unassigned = true;
bool enforce_type = false;
if (optional<expr> new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, none_expr(),
report_unassigned, enforce_type)) {
return injection_tactic_core(*new_e, 0, ids, true)(env, ios, new_s);
} else {
return proof_state_seq();
}
};
return tactic(fn);
}
void initialize_injection_tactic() {
register_tac(name{"tactic", "injection"},
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
check_tactic_expr(app_arg(app_fn(e)), "invalid 'injection' tactic, invalid argument");
buffer<name> ids;
get_tactic_id_list_elements(app_arg(e), ids, "invalid 'injection' tactic, list of identifiers expected");
return take(injection_tactic(fn, get_tactic_expr_expr(app_arg(app_fn(e))), to_list(ids)), 1);
});
}
void finalize_injection_tactic() {
}
}

11
src/library/old_tactic/tactic/injection_tactic.h
View file

@ -1,11 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
namespace lean {
void initialize_injection_tactic();
void finalize_injection_tactic();
}

92
src/library/old_tactic/tactic/intros_tactic.cpp
View file

@ -1,92 +0,0 @@
/*
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 "util/fresh_name.h"
#include "kernel/instantiate.h"
#include "library/constants.h"
#include "library/reducible.h"
#include "library/tactic/intros_tactic.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
static tactic intro_intros_tactic(list<name> _ns, bool is_intros) {
auto fn = [=](environment const & env, io_state const &, proof_state const & s) {
list<name> ns = _ns;
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return optional<proof_state>();
}
goal const & g = head(gs);
auto tc = mk_type_checker(env);
expr t = g.get_type();
expr m = g.get_meta();
bool gen_names = is_intros && empty(ns);
bool gen_one_name = !is_intros && empty(ns);
bool first = true;
try {
while (true) {
if (!gen_names && (!gen_one_name || !first) && is_nil(ns))
break;
if (!is_pi(t)) {
if (!is_nil(ns)) {
t = tc->ensure_pi(t).first;
} else {
expr new_t = tc->whnf(t).first;
if (!is_pi(new_t))
break;
t = new_t;
}
}
name new_name;
if (!is_nil(ns)) {
new_name = head(ns);
if (new_name == "_")
new_name = get_unused_name(binding_name(t), m);
ns = tail(ns);
} else {
new_name = get_unused_name(binding_name(t), m);
}
expr new_local = mk_local(mk_fresh_name(), new_name, binding_domain(t), binding_info(t));
t = instantiate(binding_body(t), new_local);
m = mk_app(m, new_local);
first = false;
}
goal new_g(m, t);
return some(proof_state(s, goals(new_g, tail(gs))));
} catch (exception &) {
return optional<proof_state>();
}
};
return tactic01(fn);
}
tactic intro_tactic(list<name> const & ns) {
return intro_intros_tactic(ns, false);
}
tactic intros_tactic(list<name> const & ns) {
return intro_intros_tactic(ns, true);
}
void initialize_intros_tactic() {
register_tac(get_tactic_intro_name(),
[](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
buffer<name> ns;
get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intro' tactic, arguments must be identifiers");
return intro_tactic(to_list(ns.begin(), ns.end()));
});
register_tac(get_tactic_intros_name(),
[](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
buffer<name> ns;
get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intros' tactic, arguments must be identifiers");
return intros_tactic(to_list(ns.begin(), ns.end()));
});
}
void finalize_intros_tactic() {
}
}

13
src/library/old_tactic/tactic/intros_tactic.h
View file

@ -1,13 +0,0 @@
/*
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 "library/tactic/tactic.h"
namespace lean {
tactic intros_tactic(list<name> const & ns);
void initialize_intros_tactic();
void finalize_intros_tactic();
}

69
src/library/old_tactic/tactic/norm_num_tactic.cpp
View file

@ -1,69 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Robert Y. Lewis
*/
#include "kernel/type_checker.h"
#include "library/util.h"
#include "library/reducible.h"
#include "library/normalize.h"
#include "library/norm_num.h"
#include "library/old_tmp_type_context.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
tactic norm_num_tactic() {
return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return none_proof_state();
}
goal const & g = head(gs);
expr const & c = g.get_type();
expr lhs, rhs;
if (!is_eq(c, lhs, rhs)) {
throw_tactic_exception_if_enabled(s, "norm_num tactic failed, conclusion is not an equality");
return none_proof_state();
}
old_type_checker_ptr rtc = mk_type_checker(env, UnfoldReducible);
lhs = normalize(*rtc, lhs);
rhs = normalize(*rtc, rhs);
buffer<expr> hyps;
g.get_hyps(hyps);
try {
old_tmp_type_context ctx(env, ios.get_options());
ctx.set_local_instances(to_list(hyps));
pair<expr, expr> p = mk_norm_num(ctx, lhs);
expr new_lhs = p.first;
expr new_lhs_pr = p.second;
pair<expr, expr> p2 = mk_norm_num(ctx, rhs);
expr new_rhs = p2.first;
expr new_rhs_pr = p2.second;
mpq v_lhs = mpq_of_expr(ctx, new_lhs), v_rhs = mpq_of_expr(ctx, new_rhs);
if (v_lhs == v_rhs) {
old_type_checker tc(env);
expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr));
substitution new_subst = s.get_subst();
assign(new_subst, g, g_prf);
return some_proof_state(proof_state(s, tail(gs), new_subst));
} else {
throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs doesn't match rhs");
return none_proof_state();
}
} catch (exception & ex) {
throw_tactic_exception_if_enabled(s, ex.what());
return none_proof_state();
}
});
}
void initialize_norm_num_tactic() {
register_tac(name{"tactic", "norm_num"},
[](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
return norm_num_tactic();
});
}
void finalize_norm_num_tactic() {
}
}

12
src/library/old_tactic/tactic/norm_num_tactic.h
View file

@ -1,12 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Rob Lewis
*/
#pragma once
namespace lean {
void initialize_norm_num_tactic();
void finalize_norm_num_tactic();
}

63
src/library/old_tactic/tactic/note_tactic.cpp
View file

@ -1,63 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/fresh_name.h"
#include "kernel/abstract.h"
#include "library/constants.h"
#include "library/reducible.h"
#include "library/unifier.h"
#include "library/tactic/tactic.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
expr mk_note_tactic_expr(name const &id, expr const &e) {
return mk_app(mk_constant(get_tactic_note_tac_name()),
mk_constant(id), e);
}
tactic note_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
proof_state new_s = s;
goals const & gs = new_s.get_goals();
if (!gs) {
throw_no_goal_if_enabled(s);
return none_proof_state();
}
goal const & g = head(gs);
bool report_unassigned = true;
elaborate_result esc = elab(g, ios.get_options(), e, none_expr(), new_s.get_subst(), report_unassigned);
expr new_e; substitution new_subst; constraints cs;
std::tie(new_e, new_subst, cs) = esc;
if (cs)
throw_tactic_exception_if_enabled(s, "invalid 'note' tactic, fail to resolve generated constraints");
auto tc = mk_type_checker(env);
expr new_e_type = tc->infer(new_e).first;
expr new_local = mk_local(mk_fresh_name(), id, new_e_type, binder_info());
buffer<expr> hyps;
g.get_hyps(hyps);
hyps.push_back(new_local);
expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, g.get_type()));
hyps.pop_back();
expr new_meta_core = mk_app(new_mvar, hyps);
expr new_meta = mk_app(new_meta_core, new_local);
goal new_goal(new_meta, g.get_type());
assign(new_subst, g, mk_app(new_meta_core, new_e));
return some_proof_state(proof_state(s, cons(new_goal, tail(gs)), new_subst));
});
}
void initialize_note_tactic() {
register_tac(get_tactic_note_tac_name(),
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'note' tactic, argument must be an identifier");
check_tactic_expr(app_arg(e), "invalid 'note' tactic, argument must be an expression");
return note_tactic(fn, id, get_tactic_expr_expr(app_arg(e)));
});
}
void finalize_note_tactic() {
}
}

14
src/library/old_tactic/tactic/note_tactic.h
View file

@ -1,14 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
namespace lean {
expr mk_note_tactic_expr(name const &id, expr const &e);
void initialize_note_tactic();
void finalize_note_tactic();
}

99
src/library/old_tactic/tactic/relation_tactics.cpp
View file

@ -1,99 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/instantiate.h"
#include "library/relation_manager.h"
#include "library/explicit.h"
#include "library/placeholder.h"
#include "library/tactic/apply_tactic.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
// Remark: if no_meta == true, then return none if goal contains metavariables
static optional<name> get_goal_op(proof_state const & s, bool no_meta = false) {
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return optional<name>();
}
goal const & g = head(gs);
if (no_meta && has_metavar(g.get_type()))
return optional<name>();
expr op = get_app_fn(head_beta_reduce(g.get_type()));
if (is_constant(op))
return optional<name>(const_name(op));
else
return optional<name>();
}
tactic refl_tactic(elaborate_fn const & elab, bool no_meta = false) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
auto op = get_goal_op(s, no_meta);
if (!op)
return proof_state_seq();
if (auto refl = get_refl_info(env, *op)) {
return apply_tactic(elab, mk_constant(*refl))(env, ios, s);
} else {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'reflexivity' tactic, operator '" << *op << "' is not marked are reflexive");
return proof_state_seq();
}
};
return tactic(fn);
}
tactic symm_tactic(elaborate_fn const & elab) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
auto op = get_goal_op(s);
if (!op)
return proof_state_seq();
if (auto symm = get_symm_info(env, *op)) {
return apply_tactic(elab, mk_constant(*symm))(env, ios, s);
} else {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'symmetry' tactic, operator '" << *op << "' is not marked are symmetric");
return proof_state_seq();
}
};
return tactic(fn);
}
tactic trans_tactic(elaborate_fn const & elab, expr const & e) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
auto op = get_goal_op(s);
if (!op)
return proof_state_seq();
if (auto info = get_trans_extra_info(env, *op, *op)) {
expr pr = mk_explicit(mk_constant(info->m_name));
unsigned nargs = info->m_num_args;
lean_assert(nargs >= 5);
for (unsigned i = 0; i < nargs - 4; i++)
pr = mk_app(pr, mk_expr_placeholder());
pr = mk_app(pr, e);
return apply_tactic(elab, pr)(env, ios, s);
} else {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'transitivity' tactic, operator '" << *op << "' is not marked are transitive");
return proof_state_seq();
}
};
return tactic(fn);
}
void initialize_relation_tactics() {
register_tac(name{"tactic", "reflexivity"},
[](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
return refl_tactic(fn);
});
register_tac(name{"tactic", "symmetry"},
[](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
return symm_tactic(fn);
});
register_tac(name{"tactic", "transitivity"},
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
check_tactic_expr(app_arg(e), "invalid 'transitivity' tactic, invalid argument");
return trans_tactic(fn, get_tactic_expr_expr(app_arg(e)));
});
}
void finalize_relation_tactics() {}
}

12
src/library/old_tactic/tactic/relation_tactics.h
View file

@ -1,12 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
namespace lean {
tactic refl_tactic(elaborate_fn const & elab, bool no_meta = false);
void initialize_relation_tactics();
void finalize_relation_tactics();
}

62
src/library/old_tactic/tactic/rename_tactic.cpp
View file

@ -1,62 +0,0 @@
/*
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 "library/constants.h"
#include "kernel/replace_fn.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
tactic rename_tactic(name const & from, name const & to) {
return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return none_proof_state();
}
goal const & g = head(gs);
goals const & rest_gs = tail(gs);
buffer<expr> locals;
get_app_args(g.get_meta(), locals);
unsigned i = locals.size();
optional<expr> from_local;
while (i > 0) {
--i;
expr const & local = locals[i];
if (local_pp_name(local) == from) {
from_local = local;
break;
}
}
if (!from_local)
return none_proof_state();
expr to_local = mk_local(mlocal_name(*from_local), to, mlocal_type(*from_local), local_info(*from_local));
auto fn = [&](expr const & e) {
if (is_local(e) && mlocal_name(e) == mlocal_name(*from_local))
return some_expr(to_local);
else
return none_expr();
};
goal new_g(replace(g.get_meta(), fn), replace(g.get_type(), fn));
return some(proof_state(s, goals(new_g, rest_gs)));
});
}
static name const & get_rename_arg(expr const & e) {
return tactic_expr_to_id(e, "invalid 'rename' tactic, arguments must be identifiers");
}
void initialize_rename_tactic() {
auto fn = [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
return rename_tactic(get_rename_arg(app_arg(app_fn(e))),
get_rename_arg(app_arg(e)));
};
register_tac(get_tactic_rename_name(), fn);
}
void finalize_rename_tactic() {
}
}

14
src/library/old_tactic/tactic/rename_tactic.h
View file

@ -1,14 +0,0 @@
/*
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 "library/tactic/tactic.h"
namespace lean {
tactic rename_tactic(name const & from, name const & to);
void initialize_rename_tactic();
void finalize_rename_tactic();
}

124
src/library/old_tactic/tactic/replace_tactic.cpp
View file

@ -1,124 +0,0 @@
/*
Copyright (c) 2015 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Robert Y. Lewis
*/
#include "util/fresh_name.h"
#include "util/lazy_list_fn.h"
#include "kernel/error_msgs.h"
#include "kernel/instantiate.h"
#include "library/constants.h"
#include "library/reducible.h"
#include "library/unifier.h"
#include "library/tactic/replace_tactic.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
static expr * g_replace_tac = nullptr;
expr substitute_at_occurrences(environment const & env, expr const & t, expr const & nexpr, expr const & oexpr, occurrence const & occ) {
bool has_dep_elim = inductive::has_dep_elim(env, get_eq_name());
unsigned vidx = has_dep_elim ? 1 : 0;
optional<expr> nt = replace_occurrences(t, oexpr, occ, vidx);
if (!nt) {
return t;
}
expr t2 = instantiate(*nt, vidx, nexpr);
return t2;
}
tactic mk_replace_tactic(elaborate_fn const & elab, expr const & e) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
buffer<expr> e_args;
get_app_args(e, e_args);
expr t1, t2; // replace t2 with t1
location loc;
if (e_args.size() == 3) {
t1 = get_tactic_expr_expr(e_args[1]);
t2 = get_tactic_expr_expr(e_args[0]);
if (is_location_expr(get_tactic_expr_expr(e_args[2]))) {
loc = get_location_expr_location(get_tactic_expr_expr(e_args[2]));
} else {
loc = location();
}
} else {
throw_tactic_exception_if_enabled(s, "malformed arguments to replace");
return proof_state_seq();
}
proof_state new_s = s;
goals const & gs = new_s.get_goals();
if (!gs) {
throw_no_goal_if_enabled(s);
return proof_state_seq();
}
expr t = head(gs).get_type();
bool report_unassigned = true;
auto new_t1 = elaborate_with_respect_to(env, ios, elab, new_s, t1, none_expr(), report_unassigned);
auto new_t2 = elaborate_with_respect_to(env, ios, elab, new_s, t2, none_expr(), report_unassigned);
if (new_t1 && new_t2) {
goals const & gs = new_s.get_goals();
goal const & g = head(gs);
substitution subst = new_s.get_subst();
auto tc = mk_type_checker(env);
constraint_seq cs;
if (tc->is_def_eq(*new_t1, *new_t2, justification(), cs)) {
auto nocc = loc.includes_goal();
expr new_goal;
if (nocc) {
new_goal = substitute_at_occurrences(env, g.get_type(), *new_t1, *new_t2, *nocc);
} else {
throw_tactic_exception_if_enabled(s, "replacing in hypotheses not implemented");
return proof_state_seq();
}
if (cs) {
unifier_config cfg(ios.get_options());
buffer<constraint> cs_buf;
cs.linearize(cs_buf);
to_buffer(new_s.get_postponed(), cs_buf);
unify_result_seq rseq = unify(env, cs_buf.size(), cs_buf.data(), subst, cfg);
return map2<proof_state>(rseq, [=](pair<substitution, constraints> const & p) -> proof_state {
substitution const & subst = p.first;
constraints const & postponed = p.second;
substitution new_subst = subst;
expr M = g.mk_meta(mk_fresh_name(), new_goal);
goal new_g(M, new_goal);
assign(new_subst, g, M);
return proof_state(new_s, cons(new_g, tail(gs)), new_subst, postponed);
});
}
expr M = g.mk_meta(mk_fresh_name(), new_goal);
goal new_g(M, new_goal);
assign(subst, g, M);
return proof_state_seq(proof_state(new_s, cons(new_g, tail(gs)), subst));
} else {
throw_tactic_exception_if_enabled(new_s, [=](formatter const & fmt) {
format r = format("invalid 'replace' tactic, the new type");
r += pp_indent_expr(fmt, *new_t1);
r += compose(line(), format("does not match the old type"));
r += pp_indent_expr(fmt, *new_t2);
return r;
});
return proof_state_seq();
}
}
return proof_state_seq();
});
}
void initialize_replace_tactic() {
name replace_tac_name{"tactic", "replace"};
g_replace_tac = new expr(Const(replace_tac_name));
register_tac(replace_tac_name,
[](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
return mk_replace_tactic(elab, e);
});
}
void finalize_replace_tactic() {
delete g_replace_tac;
}
}

15
src/library/old_tactic/tactic/replace_tactic.h
View file

@ -1,15 +0,0 @@
/*
Copyright (c) 2015 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Robert Y. Lewis
*/
#pragma once
#include "library/tactic/tactic.h"
#include "library/tactic/location.h"
namespace lean {
void initialize_replace_tactic();
void finalize_replace_tactic();
}

63
src/library/old_tactic/tactic/revert_tactic.cpp
View file

@ -1,63 +0,0 @@
/*
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 "util/fresh_name.h"
#include "kernel/abstract.h"
#include "library/constants.h"
#include "library/locals.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
tactic revert_tactic(name const & n) {
auto fn = [=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return none_proof_state();
}
goal g = head(gs);
goals tail_gs = tail(gs);
if (auto p = g.find_hyp(n)) {
expr const & h = p->first;
unsigned i = p->second;
buffer<expr> hyps;
g.get_hyps(hyps);
hyps.erase(hyps.size() - i - 1);
if (optional<expr> other_h = depends_on(i, hyps.end() - i, h)) {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'revert' tactic, hypothesis '" << local_pp_name(*other_h)
<< "' depends on '" << local_pp_name(h) << "'");
return none_proof_state(); // other hypotheses depend on h
}
expr new_type = Pi(h, g.get_type());
expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps);
goal new_g(new_meta, new_type);
substitution new_subst = s.get_subst();
assign(new_subst, g, mk_app(new_meta, h));
proof_state new_s(s, goals(new_g, tail_gs), new_subst);
return some_proof_state(new_s);
} else {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'revert' tactic, unknown hypothesis '" << n << "'");
return none_proof_state();
}
};
return tactic01(fn);
}
void initialize_revert_tactic() {
auto fn = [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
buffer<name> ns;
get_tactic_id_list_elements(app_arg(e), ns, "invalid 'reverts' tactic, list of identifiers expected");
tactic r = revert_tactic(ns[0]);
for (unsigned i = 1; i < ns.size(); i++)
r = then(revert_tactic(ns[i]), r);
return r;
};
register_tac(get_tactic_revert_name(), fn);
register_tac(get_tactic_reverts_name(), fn);
}
void finalize_revert_tactic() {}
}

14
src/library/old_tactic/tactic/revert_tactic.h
View file

@ -1,14 +0,0 @@
/*
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 "library/tactic/tactic.h"
namespace lean {
tactic revert_tactic(name const & n);
void initialize_revert_tactic();
void finalize_revert_tactic();
}

256
src/library/old_tactic/tactic/subst_tactic.cpp
View file

@ -1,256 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "util/fresh_name.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "kernel/kernel_exception.h"
#include "library/constants.h"
#include "library/reducible.h"
#include "library/util.h"
#include "library/locals.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/relation_tactics.h"
#include "library/tactic/proof_state.h"
namespace lean {
static void split_deps(buffer<expr> const & hyps, expr const & x, expr const & h,
buffer<expr> & non_deps, buffer<expr> & deps, bool & depends_on_h) {
for (expr const & hyp : hyps) {
if (hyp == h || hyp == x) {
// we clear h and x
} else if (depends_on(hyp, h)) {
deps.push_back(hyp);
depends_on_h = true;
} else if (depends_on(hyp, x) || depends_on_any(hyp, deps)) {
deps.push_back(hyp);
} else {
non_deps.push_back(hyp);
}
}
}
optional<proof_state> subst(environment const & env, name const & h_name, bool symm, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs))
return none_proof_state();
goal g = head(gs);
auto opt_h = g.find_hyp_from_internal_name(h_name);
if (!opt_h)
return none_proof_state();
expr const & h = opt_h->first;
expr lhs, rhs;
if (!is_eq(mlocal_type(h), lhs, rhs))
return none_proof_state();
auto tc = mk_type_checker(env);
if (symm)
std::swap(lhs, rhs);
if (!is_local(lhs))
return none_proof_state();
if (depends_on(rhs, lhs)) {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, '" << lhs
<< "' occurs in the other side of the equation");
return none_proof_state();
}
buffer<expr> hyps, deps, non_deps;
g.get_hyps(hyps);
bool depends_on_h = depends_on(g.get_type(), h);
split_deps(hyps, lhs, h, non_deps, deps, depends_on_h);
// revert dependencies
expr type = Pi(deps, g.get_type());
// substitute
bool has_dep_elim = inductive::has_dep_elim(env, get_eq_name());
bool use_dep_elim = has_dep_elim;
if (depends_on_h)
use_dep_elim = true;
expr motive, new_type;
new_type = instantiate(abstract_local(type, mlocal_name(lhs)), rhs);
if (use_dep_elim) {
new_type = instantiate(abstract_local(new_type, mlocal_name(h)), mk_refl(*tc, rhs));
if (symm) {
motive = Fun(lhs, Fun(h, type));
} else {
expr Heq = mk_local(mk_fresh_name(), local_pp_name(h), mk_eq(*tc, rhs, lhs), binder_info());
motive = Fun(lhs, Fun(Heq, type));
}
} else {
motive = Fun(lhs, type);
}
buffer<expr> new_hyps;
buffer<expr> intros_hyps;
new_hyps.append(non_deps);
// reintroduce dependencies
expr new_goal_type = new_type;
for (expr const & d : deps) {
if (!is_pi(new_goal_type))
return none_proof_state();
expr new_h = mk_local(mk_fresh_name(), local_pp_name(d), binding_domain(new_goal_type), binder_info());
new_hyps.push_back(new_h);
intros_hyps.push_back(new_h);
new_goal_type = instantiate(binding_body(new_goal_type), new_h);
}
// create new goal
expr new_metavar = mk_metavar(mk_fresh_name(), Pi(new_hyps, new_goal_type));
expr new_meta_core = mk_app(new_metavar, non_deps);
expr new_meta = mk_app(new_meta_core, intros_hyps);
goal new_g(new_meta, new_goal_type);
// create eqrec term
substitution new_subst = s.get_subst();
expr major = symm ? h : mk_symm(*tc, h);
expr minor = new_meta_core;
expr A = tc->infer(lhs).first;
level l1 = sort_level(tc->ensure_type(new_type).first);
level l2 = sort_level(tc->ensure_type(A).first);
name eq_rec_name;
if (!has_dep_elim && use_dep_elim)
eq_rec_name = get_eq_drec_name();
else
eq_rec_name = get_eq_rec_name();
expr eqrec = mk_app({mk_constant(eq_rec_name, {l1, l2}), A, rhs, motive, minor, lhs, major});
if (use_dep_elim) {
try {
check_term(env, g.abstract(eqrec));
} catch (kernel_exception & ex) {
if (!s.report_failure())
return none_proof_state();
std::shared_ptr<kernel_exception> saved_ex(static_cast<kernel_exception*>(ex.clone()));
throw tactic_exception("rewrite step failed", none_expr(), s,
[=](formatter const & fmt) {
format r;
r += format("invalid 'subst' tactic, "
"produced type incorrect term, details: ");
r += saved_ex->pp(fmt);
r += line();
return r;
});
}
}
expr new_val = mk_app(eqrec, deps);
assign(new_subst, g, new_val);
lean_assert(new_subst.is_assigned(g.get_mvar()));
proof_state new_s(s, goals(new_g, tail(gs)), new_subst);
return some_proof_state(new_s);
}
tactic mk_subst_tactic_core(name const & h_name, bool symm) {
auto fn = [=](environment const & env, io_state const &, proof_state const & s) {
return subst(env, h_name, symm, s);
};
return tactic01(fn);
}
tactic mk_subst_tactic(list<name> const & ids) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
if (!ids)
return proof_state_seq(s);
goals const & gs = s.get_goals();
if (empty(gs))
return proof_state_seq();
goal const & g = head(gs);
name const & id = head(ids);
auto apply_rewrite = [&](expr const & H, bool symm) {
tactic tac = then(mk_subst_tactic_core(mlocal_name(H), symm), mk_subst_tactic(tail(ids)));
return tac(env, ios, s);
};
optional<pair<expr, unsigned>> p = g.find_hyp(id);
if (!p) {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, there is no hypothesis named '"
<< id << "'");
return proof_state_seq();
}
expr const & H = p->first;
expr lhs, rhs;
if (is_eq(mlocal_type(H), lhs, rhs)) {
if (is_local(rhs)) {
return apply_rewrite(H, true);
} else if (is_local(lhs)) {
return apply_rewrite(H, false);
} else {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, hypothesis '"
<< id << "' is not of the form (x = t) or (t = x)");
return proof_state_seq();
}
} else if (is_local(H)) {
expr const & x = H;
buffer<expr> hyps;
g.get_hyps(hyps);
for (expr const & H : hyps) {
expr lhs, rhs;
if (is_eq(mlocal_type(H), lhs, rhs)) {
if (is_local(lhs) && mlocal_name(lhs) == mlocal_name(x) && !depends_on(rhs, lhs)) {
return apply_rewrite(H, false);
} else if (is_local(rhs) && mlocal_name(rhs) == mlocal_name(x) && !depends_on(lhs, rhs)) {
return apply_rewrite(H, true);
}
}
}
}
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, hypothesis '"
<< id << "' is not a variable nor an equation of the form (x = t) or (t = x)");
return proof_state_seq();
};
return tactic(fn);
}
tactic mk_subst_vars_tactic(bool first, unsigned start) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs)) {
if (first)
return proof_state_seq();
else
return proof_state_seq(s);
}
goal const & g = head(gs);
auto apply_rewrite = [&](expr const & H, bool symm, unsigned i) {
tactic tac = orelse(then(mk_subst_tactic_core(mlocal_name(H), symm), mk_subst_vars_tactic(false, 0)),
mk_subst_vars_tactic(false, i+1));
return tac(env, ios, s);
};
buffer<expr> hyps;
g.get_hyps(hyps);
for (unsigned i = start; i < hyps.size(); i++) {
expr const & h = hyps[i];
expr lhs, rhs;
if (is_eq(mlocal_type(h), lhs, rhs)) {
if (is_local(rhs)) {
return apply_rewrite(h, true, i);
} else if (is_local(lhs)) {
return apply_rewrite(h, false, i);
}
}
}
if (first)
return proof_state_seq();
else
return proof_state_seq(s);
};
return tactic(fn);
}
void initialize_subst_tactic() {
register_tac(name{"tactic", "subst"},
[](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
buffer<name> ns;
get_tactic_id_list_elements(app_arg(e), ns, "invalid 'subst' tactic, list of identifiers expected");
return then(mk_subst_tactic(to_list(ns)), try_tactic(refl_tactic(elab)));
});
register_tac(name{"tactic", "substvars"},
[](old_type_checker &, elaborate_fn const & elab, expr const &, pos_info_provider const *) {
return then(mk_subst_vars_tactic(true, 0), try_tactic(refl_tactic(elab)));
});
}
void finalize_subst_tactic() {
}
}

13
src/library/old_tactic/tactic/subst_tactic.h
View file

@ -1,13 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/tactic/proof_state.h"
namespace lean {
optional<proof_state> subst(environment const & env, name const & h_name, bool symm, proof_state const & s);
void initialize_subst_tactic();
void finalize_subst_tactic();
}

279
src/library/old_tactic/tactic/tactic.cpp
View file

@ -1,279 +0,0 @@
/*
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include <chrono>
#include <string>
#include "util/sstream.h"
#include "util/interrupt.h"
#include "util/lazy_list_fn.h"
#include "util/list_fn.h"
#include "kernel/instantiate.h"
#include "kernel/type_checker.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "library/normalize.h"
#include "library/util.h"
#include "library/old_util.h"
#include "library/tactic/tactic.h"
#include "library/io_state_stream.h"
namespace lean {
/** \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) {
if (has_local(v)) {
for_each(v, [&](expr const & l, unsigned) {
if (is_local(l))
throw tactic_exception(e, sstream() << "tactic '" << tac_name << "' contains reference to local '" << local_pp_name(l)
<< "' which is not visible by this tactic "
<< "possible causes: it was not marked as [visible]; it was destructued");
return has_local(l);
});
}
}
tactic_exception::tactic_exception(char const * msg, optional<expr> const & m, pp_fn const & fn):
generic_exception(msg, m, fn) {}
tactic_exception::tactic_exception(char const * msg, optional<expr> const & m, proof_state const & ps, pp_fn const & fn):
generic_exception(msg, m, fn), m_ps(ps) {}
tactic_exception::tactic_exception(expr const & e, std::string const & msg):
generic_exception(msg.c_str(), some_expr(e), [=](formatter const &) { return format(msg); }) {}
tactic_exception::tactic_exception(std::string const & msg):
generic_exception(msg.c_str(), none_expr(), [=](formatter const &) { return format(msg); }) {}
tactic_exception::tactic_exception(char const * msg):tactic_exception(std::string(msg)) {}
tactic_exception::tactic_exception(sstream const & strm):tactic_exception(strm.str()) {}
tactic_exception::tactic_exception(expr const & e, char const * msg):tactic_exception(e, std::string(msg)) {}
tactic_exception::tactic_exception(expr const & e, sstream const & strm):tactic_exception(e, strm.str()) {}
tactic_exception::tactic_exception(expr const & e, pp_fn const & fn):generic_exception("tactic exception", some_expr(e), fn) {}
tactic_exception::tactic_exception(pp_fn const & fn):generic_exception("tactic exception", none_expr(), fn) {}
void throw_no_goal_if_enabled(proof_state const & ps) {
throw_tactic_exception_if_enabled(ps, "invalid tactic, there are no goals to be solved");
}
tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> f) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
return mk_proof_state_seq([=]() {
auto r = f(env, ios, s);
if (r)
return some(mk_pair(*r, proof_state_seq()));
else
return proof_state_seq::maybe_pair();
});
});
}
tactic tactic1(std::function<proof_state(environment const &, io_state const & ios, proof_state const &)> f) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
return mk_proof_state_seq([=]() {
auto r = f(env, ios, s);
return some(mk_pair(r, proof_state_seq()));
});
});
}
tactic id_tactic() {
return tactic1([](environment const &, io_state const &, proof_state const & s) -> proof_state { return s; });
}
tactic fail_tactic() {
return tactic([](environment const &, io_state const &, proof_state const &) -> proof_state_seq { return proof_state_seq(); });
}
tactic now_tactic() {
return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
if (!empty(s.get_goals()))
return none_proof_state();
else
return some(s);
});
}
tactic cond(proof_state_pred p, tactic const & t1, tactic const & t2) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
return mk_proof_state_seq([=]() {
if (p(env, ios, s)) {
return t1(env, ios, s).pull();
} else {
return t2(env, ios, s).pull();
}
});
});
}
tactic then(tactic const & t1, tactic const & t2) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s1) -> proof_state_seq {
return map_append(t1(env, ios, s1), [=](proof_state const & s2) {
check_interrupted();
bool has_meta = false;
goals const & gs = s2.get_goals();
for (goal const & g : gs) {
if (has_expr_metavar_relaxed(g.get_type())) {
has_meta = true;
break;
}
}
if (has_meta) {
buffer<goal> gs;
substitution subst = s2.get_subst();
to_buffer(s2.get_goals(), gs);
for (unsigned i = 0; i < gs.size(); i++) {
gs[i] = gs[i].instantiate(subst);
}
proof_state new_s2(s2, to_list(gs));
return t2(env, ios, new_s2);
} else {
return t2(env, ios, s2);
}
}, "THEN tactical");
});
}
tactic orelse(tactic const & t1, tactic const & t2) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
proof_state s = _s.update_report_failure(false);
return orelse(t1(env, ios, s), t2(env, ios, s), "ORELSE tactical");
});
}
tactic using_params(tactic const & t, options const & opts) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
io_state new_ios(ios);
new_ios.set_options(join(opts, ios.get_options()));
return t(env, new_ios, s);
});
}
proof_state rotate_left(proof_state const & s, unsigned n) {
buffer<goal> gs;
to_buffer(s.get_goals(), gs);
unsigned sz = gs.size();
if (sz == 0)
return s;
n = n%sz;
std::rotate(gs.begin(), gs.begin() + n, gs.end());
return proof_state(s, to_list(gs.begin(), gs.end()));
}
tactic rotate_left(unsigned n) {
return tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state {
return rotate_left(s, n);
});
}
tactic rotate_right(unsigned n) {
return tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state {
unsigned ngoals = length(s.get_goals());
if (ngoals == 0)
return s;
return rotate_left(s, ngoals - n%ngoals);
});
}
tactic try_for(tactic const & t, unsigned ms, unsigned check_ms) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
proof_state s = _s.update_report_failure(false);
return timeout(t(env, ios, s), ms, check_ms);
});
}
tactic par(tactic const & t1, tactic const & t2, unsigned check_ms) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
proof_state s = _s.update_report_failure(false);
return par(t1(env, ios, s), t2(env, ios, s), check_ms);
});
}
tactic repeat(tactic const & t) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & _s1) -> proof_state_seq {
proof_state s1 = _s1.update_report_failure(false);
return repeat(s1, [=](proof_state const & s2) {
return t(env, ios, s2);
}, "REPEAT tactical");
});
}
tactic repeat_at_most(tactic const & t, unsigned k) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & _s1) -> proof_state_seq {
proof_state s1 = _s1.update_report_failure(false);
return repeat_at_most(s1, [=](proof_state const & s2) {
return t(env, ios, s2);
}, k, "REPEAT_AT_MOST tactical");
});
}
tactic take(tactic const & t, unsigned k) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
proof_state s = _s.update_report_failure(false);
return take(k, t(env, ios, s));
});
}
tactic discard(tactic const & t, unsigned k) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq {
proof_state s = _s.update_report_failure(false);
auto r = t(env, ios, s);
for (unsigned i = 0; i < k; i++) {
auto m = r.pull();
if (!m)
return proof_state_seq();
r = m->second;
}
return r;
});
}
tactic beta_tactic() {
return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
bool reduced = false;
goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
expr new_meta = beta_reduce(g.get_meta());
expr new_type = beta_reduce(g.get_type());
if (new_meta != g.get_meta() || new_type != g.get_type())
reduced = true;
return some(goal(new_meta, new_type));
});
return reduced ? some(proof_state(s, new_gs)) : none_proof_state();
});
}
proof_state_seq focus_core(tactic const & t, unsigned i, environment const & env, io_state const & ios, proof_state const & s) {
goals gs = s.get_goals();
if (i >= length(gs))
return proof_state_seq();
goal const & g = get_ith(gs, i);
proof_state new_s(s, goals(g)); // singleton goal
return map(t(env, ios, new_s), [=](proof_state const & s2) {
// we have to put back the goals that were not selected
buffer<goal> tmp;
to_buffer(gs, tmp);
buffer<goal> new_gs;
new_gs.append(i, tmp.data());
for (auto g : s2.get_goals())
new_gs.push_back(g);
new_gs.append(tmp.size()-i-1, tmp.data()+i+1);
return proof_state(s2, to_list(new_gs.begin(), new_gs.end()));
});
}
tactic focus(tactic const & t, unsigned i) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
return focus_core(t, i, env, ios, s);
});
}
tactic all_goals(tactic const & t) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
tactic r = id_tactic();
unsigned i = length(s.get_goals());
while (i > 0) {
--i;
r = then(r, focus(t, i));
}
return r(env, ios, s);
});
}
}

140
src/library/old_tactic/tactic/tactic.h
View file

@ -1,140 +0,0 @@
/*
Copyright (c) 2013-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 <algorithm>
#include <utility>
#include <memory>
#include <string>
#include "util/lazy_list.h"
#include "library/io_state.h"
#include "library/generic_exception.h"
#include "library/tactic/proof_state.h"
namespace lean {
/** \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);
class tactic_exception : public generic_exception {
optional<proof_state> m_ps;
public:
tactic_exception(char const * msg, optional<expr> const & m, pp_fn const & fn);
tactic_exception(char const * msg, optional<expr> const & m, proof_state const & ps, pp_fn const & fn);
tactic_exception(expr const & e, std::string const & msg);
tactic_exception(expr const & e, char const * msg);
tactic_exception(expr const & e, sstream const & strm);
tactic_exception(expr const & e, pp_fn const & fn);
tactic_exception(std::string const & msg);
tactic_exception(char const * msg);
tactic_exception(sstream const & strm);
tactic_exception(pp_fn const & fn);
optional<proof_state> const & get_proof_state() const { return m_ps; }
};
#define throw_tactic_exception_if_enabled(ps, msg) if (ps.report_failure()) throw tactic_exception(msg);
void throw_no_goal_if_enabled(proof_state const & ps);
typedef lazy_list<proof_state> proof_state_seq;
typedef std::function<proof_state_seq(environment const &, io_state const &, proof_state const &)> tactic;
inline optional<tactic> none_tactic() { return optional<tactic>(); }
inline optional<tactic> some_tactic(tactic const & t) { return optional<tactic>(t); }
inline optional<tactic> some_tactic(tactic && t) { return optional<tactic>(std::forward<tactic>(t)); }
template<typename F> inline proof_state_seq mk_proof_state_seq(F && f) { return mk_lazy_list<proof_state>(std::forward<F>(f)); }
tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> f);
tactic tactic1(std::function<proof_state(environment const &, io_state const & ios, proof_state const &)> f);
/** \brief Return a "do nothing" tactic (aka skip). */
tactic id_tactic();
/** \brief Return a tactic the always fails. */
tactic fail_tactic();
/** \brief Return a tactic that fails if there are unsolved goals. */
tactic now_tactic();
/** \brief Return a tactic that performs \c t1 followed by \c t2. */
tactic then(tactic const & t1, tactic const & t2);
inline tactic operator<<(tactic const & t1, tactic const & t2) { return then(t1, t2); }
/** \brief Return a tactic that applies \c t1, and if \c t1 returns the empty sequence of states, then applies \c t2. */
tactic orelse(tactic const & t1, tactic const & t2);
inline tactic operator||(tactic const & t1, tactic const & t2) { return orelse(t1, t2); }
inline tactic try_tactic(tactic const & t) { return orelse(t, id_tactic()); }
/** \brief Return a tactic that appies \c t, but using the additional set of options \c opts. */
tactic using_params(tactic const & t, options const & opts);
/**
\brief Return a tactic that tries the tactic \c t for at most \c ms milliseconds.
If the tactic does not terminate in \c ms milliseconds, then the empty
sequence is returned.
\remark the tactic \c t is executed in a separate execution thread.
\remark \c check_ms is how often the main thread checks whether the child
thread finished.
*/
tactic try_for(tactic const & t, unsigned ms, unsigned check_ms = 1);
/** \brief Return a tactic that rotate goals to the left n steps */
tactic rotate_left(unsigned n);
/** \brief Return a tactic that rotate goals to the right n steps */
tactic rotate_right(unsigned n);
/**
\brief Return a tactic that executes \c t1 and \c t2 in parallel.
This is similar to \c append and \c interleave. The order of
the elements in the output sequence is not deterministic.
It depends on how fast \c t1 and \c t2 produce their output.
\remark \c check_ms is how often the main thread checks whether the children
threads finished.
*/
tactic par(tactic const & t1, tactic const & t2, unsigned check_ms);
inline tactic par(tactic const & t1, tactic const & t2) { return par(t1, t2, 1); }
/**
\brief Return a tactic that keeps applying \c t until it fails.
*/
tactic repeat(tactic const & t);
/**
\brief Similar to \c repeat, but execute \c t at most \c k times.
\remark The value \c k is the depth of the recursion.
For example, if tactic \c t always produce a sequence of size 2,
then tactic \c t will be applied 2^k times.
*/
tactic repeat_at_most(tactic const & t, unsigned k);
/**
\brief Return a tactic that applies \c t, but takes at most \c
\c k elements from the sequence produced by \c t.
*/
tactic take(tactic const & t, unsigned k);
/**
\brief Return a tactic that applies \c t, but discards the first
\c k elements from the sequence produced by \c t.
*/
tactic discard(tactic const & t, unsigned k);
/** \brief Return a tactic that renames hypothesis \c from into \c to in the current goal. */
tactic rename_tactic(name const & from, name const & to);
typedef std::function<bool(environment const & env, io_state const & ios, proof_state const & s)> proof_state_pred; // NOLINT
/**
\brief Return a tactic that applies the predicate \c p to the input state.
If \c p returns true, then applies \c t1. Otherwise, applies \c t2.
*/
tactic cond(proof_state_pred p, tactic const & t1, tactic const & t2);
/** \brief Syntax-sugar for cond(p, t, id_tactic()) */
inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_tactic()); }
/**
\brief Return a tactic that applies \c t only to the i-th goal.
The tactic fails if the input state does have at least i goals.
*/
tactic focus(tactic const & t, unsigned i);
inline tactic focus(tactic const & t) { return focus(t, 0); }
/** \brief Return a tactic that applies beta-reduction. */
tactic beta_tactic();
/** \brief Apply \c t to all goals in the proof state */
tactic all_goals(tactic const & t);
}