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

refactor(library/tactic): add hsubstitution module

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-29 08:19:05 -07:00
parent 71916acbf0
commit b317d4bc58
10 changed files with 145 additions and 116 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/library/equations_compiler/elim_match.cpp
View file

@ -54,7 +54,7 @@ struct elim_match_fn {
list<expr> m_patterns;
expr m_rhs;
/* m_renames map variables in this->m_lctx to problem local context */
substitutions m_substs;
hsubstitution m_subst;
expr m_ref; /* for producing error messages */
unsigned m_eqn_idx; /* for producing error message */
};
@ -72,7 +72,7 @@ struct elim_match_fn {
list<expr> m_hs;
list<expr> m_args;
expr m_rhs;
substitutions m_substs;
hsubstitution m_subst;
unsigned m_eqn_idx;
};
@ -108,7 +108,7 @@ struct elim_match_fn {
bool check_equation(problem const & P, equation const & eqn) {
lean_assert(length(eqn.m_patterns) == length(P.m_var_stack));
local_context const & lctx = get_local_context(P);
eqn.m_substs.for_each([&](name const & n, expr const & e) {
eqn.m_subst.for_each([&](name const & n, expr const & e) {
lean_assert(eqn.m_lctx.get_local_decl(n));
lean_assert(check_locals_decl_at(e, lctx));
});
@ -430,11 +430,11 @@ struct elim_match_fn {
lean_unreachable();
}
substitutions add_subst(substitutions substs, expr const & src, expr const & target) {
hsubstitution add_subst(hsubstitution subst, expr const & src, expr const & target) {
lean_assert(is_local(src));
if (!substs.contains(mlocal_name(src)))
substs.insert(mlocal_name(src), target);
return substs;
if (!subst.contains(mlocal_name(src)))
subst.insert(mlocal_name(src), target);
return subst;
}
/* Variable and Inaccessible transition are very similar, this method implements both. */
@ -450,7 +450,7 @@ struct elim_match_fn {
equation new_eqn = eqn;
new_eqn.m_patterns = tail(eqn.m_patterns);
if (is_var_transition) {
new_eqn.m_substs = add_subst(eqn.m_substs, head(eqn.m_patterns), head(P.m_var_stack));
new_eqn.m_subst = add_subst(eqn.m_subst, head(eqn.m_patterns), head(P.m_var_stack));
}
new_eqns.push_back(new_eqn);
}
@ -505,26 +505,26 @@ struct elim_match_fn {
/* Append `ilist` and `var_stack`. Due to dependent pattern matching, ilist may contain terms that
are not local constants. */
list<expr> update_var_stack(list<expr> const & ilist, list<expr> const & var_stack, substitutions const & substs) {
list<expr> update_var_stack(list<expr> const & ilist, list<expr> const & var_stack, hsubstitution const & subst) {
buffer<expr> new_var_stack;
for (expr const & e : ilist) {
new_var_stack.push_back(e);
}
for (expr const & v : var_stack) {
new_var_stack.push_back(apply_substitutions(v, substs));
new_var_stack.push_back(apply(v, subst));
}
return to_list(new_var_stack);
}
/* eqns is the data-structured returned by distribute_constructor_equations.
This method selects the ones such that eqns[i].first == C.
It also updates eqns[i].second.m_substs using \c new_substs.
It also updates eqns[i].second.m_subst using \c new_subst.
It also "replaces" the next pattern (a constructor) with its fields.
The map \c new_substs is produced by the `cases` tactic.
The map \c new_subst is produced by the `cases` tactic.
It is needed because the `cases` tactic may revert and reintroduce hypothesis that
depend on the hypothesis being destructed. */
list<equation> get_equations_for(name const & C, unsigned nparams, substitutions const & new_substs,
list<equation> get_equations_for(name const & C, unsigned nparams, hsubstitution const & new_subst,
local_context const & lctx, list<equation> const & eqns) {
buffer<equation> R;
for (equation const & eqn : eqns) {
@ -533,7 +533,7 @@ struct elim_match_fn {
expr const & C2 = get_app_args(pattern, pattern_args);
if (!is_constant(C2, C)) continue;
equation new_eqn = eqn;
new_eqn.m_substs = apply_substitutions(eqn.m_substs, new_substs);
new_eqn.m_subst = apply(eqn.m_subst, new_subst);
/* Update patterns */
type_context ctx = mk_type_context(eqn.m_lctx);
new_eqn.m_patterns = to_list(pattern_args.begin() + nparams, pattern_args.end(), tail(eqn.m_patterns));
@ -579,7 +579,7 @@ struct elim_match_fn {
name I_name = const_name(get_app_fn(x_type));
unsigned I_nparams = get_inductive_num_params(I_name);
intros_list ilist;
substitutions_list slist;
hsubstitution_list slist;
list<expr> new_goals;
list<name> new_goal_cnames;
try {
@ -711,7 +711,7 @@ struct elim_match_fn {
new_var_stack.push_back(C_args[i]);
to_buffer(tail(P.m_var_stack), new_var_stack);
new_P.m_var_stack = to_list(new_var_stack);
new_P.m_equations = get_equations_for(const_name(C), I_nparams, substitutions(),
new_P.m_equations = get_equations_for(const_name(C), I_nparams, hsubstitution(),
get_local_context(P.m_goal), eqns);
list<lemma> Ls = process(new_P);
buffer<lemma> new_Ls;
@ -728,7 +728,7 @@ struct elim_match_fn {
}
equation const & eqn = head(P.m_equations);
m_used_eqns[eqn.m_eqn_idx] = true;
expr rhs = apply_substitutions(eqn.m_rhs, eqn.m_substs);
expr rhs = apply(eqn.m_rhs, eqn.m_subst);
m_mctx.assign(P.m_goal, rhs);
if (m_lemmas) {
lemma L;

3
src/library/tactic/CMakeLists.txt
View file

@ -5,4 +5,5 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp
fun_info_tactics.cpp congr_lemma_tactics.cpp match_tactic.cpp
ac_tactics.cpp induction_tactic.cpp cases_tactic.cpp
generalize_tactic.cpp rewrite_tactic.cpp unfold_tactic.cpp
gexpr.cpp elaborate.cpp init_module.cpp simp_result.cpp user_attribute.cpp)
hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp
simp_result.cpp user_attribute.cpp)

59
src/library/tactic/cases_tactic.cpp
View file

@ -237,15 +237,15 @@ struct cases_tactic_fn {
return tmp.pp_goal(mvar);
}
list<expr> elim_aux_indices(list<expr> const & goals, buffer<name> const & aux_indices_H, substitutions_list & slist) {
list<expr> elim_aux_indices(list<expr> const & goals, buffer<name> const & aux_indices_H, hsubstitution_list & slist) {
lean_assert(!slist || length(goals) == length(slist));
buffer<expr> new_goals;
buffer<substitutions> new_slist;
buffer<hsubstitution> new_slist;
list<expr> it1 = goals;
substitutions_list it2 = slist;
hsubstitution_list it2 = slist;
while (it1 && it2) {
expr mvar = head(it1);
substitutions substs = head(it2);
hsubstitution subst = head(it2);
name_set removed;
lean_assert(aux_indices_H.size() > 1);
unsigned i = aux_indices_H.size() - 1; /* last element is the auxiliary major premise */
@ -253,23 +253,23 @@ struct cases_tactic_fn {
--i;
name idx_name = aux_indices_H[i];
removed.insert(idx_name);
if (auto ridx = substs.find(idx_name)) {
if (auto ridx = subst.find(idx_name)) {
lean_assert(is_local(*ridx));
name new_name = mlocal_name(*ridx);
substs.erase(idx_name);
subst.erase(idx_name);
idx_name = new_name;
}
expr H_idx = m_mctx.get_hypothesis_of(mvar, idx_name)->mk_ref();
mvar = clear(m_mctx, mvar, H_idx);
}
substitutions new_substs;
substs.for_each([&](name const & from, expr const & to) {
hsubstitution new_subst;
subst.for_each([&](name const & from, expr const & to) {
lean_assert(is_local(to));
if (!removed.contains(mlocal_name(to)))
new_substs.insert(from, to);
new_subst.insert(from, to);
});
new_goals.push_back(mvar);
new_slist.push_back(new_substs);
new_slist.push_back(new_subst);
it1 = tail(it1);
it2 = tail(it2);
}
@ -278,7 +278,7 @@ struct cases_tactic_fn {
}
optional<expr> unify_eqs(expr mvar, unsigned num_eqs, bool updating,
list<expr> & new_intros, substitutions & substs) {
list<expr> & new_intros, hsubstitution & subst) {
if (num_eqs == 0) {
lean_cases_trace(mvar, tout() << "solved equalities\n" << pp_goal(mvar) << "\n";);
return some_expr(mvar);
@ -322,17 +322,17 @@ struct cases_tactic_fn {
expr val = mk_app(mvar2, mk_eq_of_heq(ctx, H));
m_mctx.assign(*mvar1, val);
lean_cases_trace(mvar, tout() << "converted heq => eq\n";);
return unify_eqs(mvar2, num_eqs, updating, new_intros, substs);
return unify_eqs(mvar2, num_eqs, updating, new_intros, subst);
} else if (is_eq(H_type, A, lhs, rhs)) {
if (is_local(rhs) || is_local(lhs)) {
lean_cases_trace(mvar, tout() << "substitute\n";);
substitutions extra_substs;
hsubstitution extra_subst;
bool symm = !is_local(lhs) && is_local(rhs);
expr mvar2 = subst(m_env, m_opts, m_mode, m_mctx, *mvar1, H, symm,
updating ? &extra_substs : nullptr);
new_intros = apply_substitutions(new_intros, extra_substs);
substs = merge(apply_substitutions(substs, extra_substs), extra_substs);
return unify_eqs(mvar2, num_eqs - 1, updating, new_intros, substs);
expr mvar2 = ::lean::subst(m_env, m_opts, m_mode, m_mctx, *mvar1, H, symm,
updating ? &extra_subst : nullptr);
new_intros = apply(new_intros, extra_subst);
subst = merge(apply(subst, extra_subst), extra_subst);
return unify_eqs(mvar2, num_eqs - 1, updating, new_intros, subst);
} else {
optional<name> c1 = is_constructor_app(m_env, lhs);
optional<name> c2 = is_constructor_app(m_env, rhs);
@ -360,7 +360,7 @@ struct cases_tactic_fn {
unsigned A_nparams = *inductive::get_num_params(m_env, const_name(A_fn));
lean_assert(get_app_num_args(lhs) >= A_nparams);
return unify_eqs(mvar2, num_eqs - 1 + get_app_num_args(lhs) - A_nparams,
updating, new_intros, substs);
updating, new_intros, subst);
} else {
/* conflict, closes the goal */
lean_cases_trace(*mvar1, tout() << "conflicting equality detected, "
@ -377,25 +377,25 @@ struct cases_tactic_fn {
}
pair<list<expr>, list<name>> unify_eqs(list<expr> const & mvars, list<name> const & cnames, unsigned num_eqs,
intros_list * ilist, substitutions_list * slist) {
intros_list * ilist, hsubstitution_list * slist) {
lean_assert((ilist == nullptr) == (slist == nullptr));
buffer<expr> new_goals;
buffer<list<expr>> new_ilist;
buffer<substitutions> new_slist;
buffer<hsubstitution> new_slist;
buffer<name> new_cnames;
list<expr> it1 = mvars;
list<name> itn = cnames;
intros_list const * it2 = ilist;
substitutions_list const * it3 = slist;
hsubstitution_list const * it3 = slist;
while (it1) {
list<expr> new_intros;
substitutions substs;
hsubstitution subst;
if (ilist) {
new_intros = head(*it2);
substs = head(*it3);
subst = head(*it3);
}
bool updating = ilist != nullptr;
optional<expr> new_mvar = unify_eqs(head(it1), num_eqs, updating, new_intros, substs);
optional<expr> new_mvar = unify_eqs(head(it1), num_eqs, updating, new_intros, subst);
if (new_mvar) {
new_goals.push_back(*new_mvar);
new_cnames.push_back(head(itn));
@ -407,7 +407,7 @@ struct cases_tactic_fn {
it3 = &tail(*it3);
if (new_mvar) {
new_ilist.push_back(new_intros);
new_slist.push_back(substs);
new_slist.push_back(subst);
}
}
}
@ -427,7 +427,8 @@ struct cases_tactic_fn {
m_ids(ids){
}
pair<list<expr>, list<name>> operator()(expr const & mvar, expr const & H, intros_list * ilist, substitutions_list * slist) {
pair<list<expr>, list<name>> operator()(expr const & mvar, expr const & H,
intros_list * ilist, hsubstitution_list * slist) {
lean_assert((ilist != nullptr) == (slist != nullptr));
lean_assert(is_metavar(mvar));
lean_assert(m_mctx.get_metavar_decl(mvar));
@ -454,7 +455,7 @@ struct cases_tactic_fn {
lean_cases_trace(mvar1, tout() << "after generalize_indices:\n" << pp_goal(mvar1) << "\n";);
expr H1 = m_mctx.get_metavar_decl(mvar1)->get_context().get_last_local_decl()->mk_ref();
intros_list tmp_ilist;
substitutions_list tmp_slist;
hsubstitution_list tmp_slist;
list<expr> new_goals1 = induction(m_env, m_opts, m_mode, m_mctx, mvar1, H1, m_cases_on_decl.get_name(),
m_ids, &tmp_ilist, &tmp_slist);
lean_cases_trace(mvar1, tout() << "after applying cases_on:";
@ -474,7 +475,7 @@ struct cases_tactic_fn {
pair<list<expr>, list<name>>
cases(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
expr const & mvar, expr const & H, list<name> & ids, intros_list * ilist, substitutions_list * slist) {
expr const & mvar, expr const & H, list<name> & ids, intros_list * ilist, hsubstitution_list * slist) {
auto r = cases_tactic_fn(env, opts, m, mctx, ids)(mvar, H, ilist, slist);
lean_assert(length(r.first) == length(r.second));
return r;

3
src/library/tactic/cases_tactic.h
View file

@ -6,7 +6,6 @@ Author: Leonardo de Moura
*/
#pragma once
#include "library/tactic/induction_tactic.h"
#include "library/tactic/subst_tactic.h"
namespace lean {
/** \brief Similar to induction, but applies 'cases_on' and has bettern support for dependent types. Failures are reported using exceptions.
@ -29,7 +28,7 @@ namespace lean {
since some of the goals are discarded. */
pair<list<expr>, list<name>>
cases(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
expr const & mvar, expr const & H, list<name> & ids, intros_list * ilist, substitutions_list * slist);
expr const & mvar, expr const & H, list<name> & ids, intros_list * ilist, hsubstitution_list * slist);
void initialize_cases_tactic();
void finalize_cases_tactic();

47
src/library/tactic/hsubstitution.cpp Normal file
View file

@ -0,0 +1,47 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/replace_fn.h"
#include "library/tactic/hsubstitution.h"
namespace lean {
expr apply(expr const & e, hsubstitution const & s) {
if (s.empty()) return e;
if (!has_local(e)) return e;
return replace(e, [&](expr const & e, unsigned) {
if (!has_local(e)) return some_expr(e);
if (is_local(e)) {
if (auto r = s.find(mlocal_name(e)))
return some_expr(*r);
}
return none_expr();
});
}
list<expr> apply(list<expr> const & es, hsubstitution const & s) {
if (s.empty()) return es;
return map(es, [&](expr const & e) { return apply(e, s); });
}
hsubstitution apply(hsubstitution const & s1, hsubstitution const & s2) {
if (s2.empty()) return s1;
hsubstitution R;
s1.for_each([&](name const & x, expr const & e) {
R.insert(x, apply(e, s2));
});
return R;
}
hsubstitution merge(hsubstitution const & s1, hsubstitution const & s2) {
if (s1.empty()) return s2;
if (s2.empty()) return s1;
hsubstitution R = s1;
s2.for_each([&](name const & x, expr const & e) {
R.insert(x, e);
});
return R;
}
}

30
src/library/tactic/hsubstitution.h Normal file
View file

@ -0,0 +1,30 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "util/name_map.h"
#include "kernel/expr.h"
namespace lean {
/* Some tactics substitute hypotheses with new ones and/or terms.
We track these substitutions using hsubstitution datastructure.
It is just a mapping from the hypothesis original (internal) name
to an expression. The new expression should be well-formed with
respect to the new goal. */
typedef name_map<expr> hsubstitution;
/* \brief Given `e`, for each (x := v) in `s` replace `x` with `v` in `e` */
expr apply(expr const & e, hsubstitution const & s);
/* \brief (map es apply) */
list<expr> apply(list<expr> const & es, hsubstitution const & s);
/* \brief Return a new hsubstitution containing (x := apply(v, s2)) for
each (x := v) in `s1`. */
hsubstitution apply(hsubstitution const & s1, hsubstitution const & s2);
/* \brief Return a new hsubstitution containing the entries of `s1` and `s2`.
\remark the entries in `s2` have precedence over the ones in `s1`. */
hsubstitution merge(hsubstitution const & s1, hsubstitution const & s2);
}

14
src/library/tactic/induction_tactic.cpp
View file

@ -63,7 +63,7 @@ static unsigned get_expr_arity(expr type) {
list<expr> induction(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
expr const & mvar, expr const & H, name const & rec_name, list<name> & ns,
intros_list * ilist, substitutions_list * slist) {
intros_list * ilist, hsubstitution_list * slist) {
lean_assert(is_metavar(mvar));
lean_assert(is_local(H));
lean_assert((ilist == nullptr) == (slist == nullptr));
@ -128,12 +128,12 @@ list<expr> induction(environment const & env, options const & opts, transparency
optional<expr> mvar2 = intron(env, opts, mctx, mvar1, indices.size() + 1, indices_H);
if (!mvar2)
throw exception("induction tactic failed, failed to reintroduce major premise");
substitutions base_substs; /* substitutions for all branches */
hsubstitution base_subst; /* substitutions for all branches */
if (slist) {
local_context lctx = mctx.get_metavar_decl(*mvar2)->get_context();
/* store old index name -> new index name */
for (unsigned i = 0; i < indices.size(); i++) {
base_substs.insert(mlocal_name(indices[i]), lctx.get_local_decl(indices_H[i])->mk_ref());
base_subst.insert(mlocal_name(indices[i]), lctx.get_local_decl(indices_H[i])->mk_ref());
}
}
optional<metavar_decl> g2 = mctx.get_metavar_decl(*mvar2);
@ -205,7 +205,7 @@ list<expr> induction(environment const & env, options const & opts, transparency
bool consumed_major = false;
buffer<expr> new_goals;
buffer<list<expr>> params_buffer;
buffer<substitutions> substs_buffer;
buffer<hsubstitution> subst_buffer;
list<bool> produce_motive = rec_info.get_produce_motive();
while (is_pi(rec_type) && curr_pos < rec_info.get_num_args()) {
if (first_idx_pos == curr_pos) {
@ -257,12 +257,12 @@ list<expr> induction(environment const & env, options const & opts, transparency
}
if (slist) {
/* Save renaming for hypothesis that depend on indices and/or major premise. */
substitutions S = base_substs;
hsubstitution S = base_subst;
lean_assert(extra_names.size() == nextra);
for (unsigned i = indices.size() + 1, j = 0; i < to_revert.size(); i++, j++) {
S.insert(mlocal_name(to_revert[i]), aux_M_lctx.get_local_decl(extra_names[j])->mk_ref());
}
substs_buffer.push_back(S);
subst_buffer.push_back(S);
}
/* Clear hypothesis in the new goal. */
set_clear(aux_M, ctx2, aux_M, H2);
@ -283,7 +283,7 @@ list<expr> induction(environment const & env, options const & opts, transparency
if (ilist) {
lean_assert(slist);
*ilist = to_list(params_buffer);
*slist = to_list(substs_buffer);
*slist = to_list(subst_buffer);
}
return to_list(new_goals);
}

6
src/library/tactic/induction_tactic.h
View file

@ -6,11 +6,11 @@ Author: Leonardo de Moura
*/
#pragma once
#include "library/tactic/tactic_state.h"
#include "library/tactic/subst_tactic.h"
#include "library/tactic/hsubstitution.h"
namespace lean {
typedef list<list<expr>> intros_list;
typedef list<substitutions> substitutions_list;
typedef list<hsubstitution> hsubstitution_list;
/** \brief Apply the induction lemma \c rec_name on the hypothesis \c H at goal \c mvar.
The tactic uses ns (if available) to name parameters associated with minor premises.
@ -28,7 +28,7 @@ typedef list<substitutions> substitutions_list;
\post slist != nullptr ==> length(*slist) == length(result) */
list<expr> induction(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
expr const & mvar, expr const & H, name const & rec_name, list<name> & ns,
intros_list * ilist, substitutions_list * slist);
intros_list * ilist, hsubstitution_list * slist);
void initialize_induction_tactic();
void finalize_induction_tactic();

49
src/library/tactic/subst_tactic.cpp
View file

@ -21,43 +21,6 @@ Author: Leonardo de Moura
#include "library/tactic/app_builder_tactics.h"
namespace lean {
expr apply_substitutions(expr const & e, substitutions const & s) {
if (s.empty()) return e;
if (!has_local(e)) return e;
return replace(e, [&](expr const & e, unsigned) {
if (!has_local(e)) return some_expr(e);
if (is_local(e)) {
if (auto r = s.find(mlocal_name(e)))
return some_expr(*r);
}
return none_expr();
});
}
list<expr> apply_substitutions(list<expr> const & es, substitutions const & s) {
if (s.empty()) return es;
return map(es, [&](expr const & e) { return apply_substitutions(e, s); });
}
substitutions apply_substitutions(substitutions const & s1, substitutions const & s2) {
if (s2.empty()) return s1;
substitutions R;
s1.for_each([&](name const & x, expr const & e) {
R.insert(x, apply_substitutions(e, s2));
});
return R;
}
substitutions merge(substitutions const & s1, substitutions const & s2) {
if (s1.empty()) return s2;
if (s2.empty()) return s1;
substitutions R = s1;
s2.for_each([&](name const & x, expr const & e) {
R.insert(x, e);
});
return R;
}
/* For debugging purposes, make sure H is in the local context for mvar */
bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar, name const & H) {
local_context lctx = mctx.get_metavar_decl(mvar)->get_context();
@ -69,7 +32,7 @@ bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar
}
expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
expr const & mvar, expr const & H, bool symm, substitutions * substs) {
expr const & mvar, expr const & H, bool symm, hsubstitution * subst) {
#define lean_subst_trace(CODE) lean_trace(name({"tactic", "subst"}), CODE)
#define lean_subst_trace_state(MVAR, MSG) lean_trace(name({"tactic", "subst"}), tactic_state S(env, opts, mctx, to_list(MVAR), MVAR); type_context TMP_CTX = mk_type_context_for(S, m); scope_trace_env _scope1(env, TMP_CTX); tout() << MSG << S.pp() << "\n";)
@ -125,16 +88,16 @@ expr subst(environment const & env, options const & opts, transparency_mode cons
optional<expr> mvar6 = intron(env, opts, mctx, mvar5, to_revert.size() - 2, new_Hnames);
if (!mvar6) throw exception("subst tactic failed, unexpected failure when re-introducing dependencies");
lean_assert(new_Hnames.size() == to_revert.size() - 2);
if (substs) {
if (subst) {
local_context lctx = mctx.get_metavar_decl(*mvar6)->get_context();
substitutions new_substs;
hsubstitution new_subst;
for (unsigned i = 0; i < to_revert.size() - 2; i++) {
lean_assert(check_hypothesis_in_context(mctx, mvar, mlocal_name(to_revert[i+2])));
lean_assert(check_hypothesis_in_context(mctx, *mvar6, new_Hnames[i]));
new_substs.insert(mlocal_name(to_revert[i+2]), lctx.get_local_decl(new_Hnames[i])->mk_ref());
new_subst.insert(mlocal_name(to_revert[i+2]), lctx.get_local_decl(new_Hnames[i])->mk_ref());
}
new_substs.insert(mlocal_name(init_lhs), apply_substitutions(rhs, new_substs));
*substs = new_substs;
new_subst.insert(mlocal_name(init_lhs), apply(rhs, new_subst));
*subst = new_subst;
}
lean_subst_trace_state(*mvar6, "after intro remaining reverted hypotheses:\n");
return *mvar6;

16
src/library/tactic/subst_tactic.h
View file

@ -6,21 +6,9 @@ Author: Leonardo de Moura
*/
#pragma once
#include "library/tactic/tactic_state.h"
#include "library/tactic/hsubstitution.h"
namespace lean {
typedef name_map<expr> substitutions;
/* \brief Given `e`, for each (x := v) in `s` replace `x` with `v` in `e` */
expr apply_substitutions(expr const & e, substitutions const & s);
list<expr> apply_substitutions(list<expr> const & es, substitutions const & s);
/* \brief Return a new set of substitutions containing (x := apply_substitutions(v, s2)) for
each (x := v) in `s1`. */
substitutions apply_substitutions(substitutions const & s1, substitutions const & s2);
/* \brief Return a new set of substitutions containing the entries of `s1` and `s2`. */
substitutions merge(substitutions const & s1, substitutions const & s2);
/** \brief Given (H : lhs = rhs), replace lhs with rhs in the goal \c mvar. If symm == true, then replace rhs with lhs.
The replaced term must be a local constant. If substs is not nullptr, then hypotheses renamed by revert/intro
are stored in \c substs, and the actual substitution.
@ -32,7 +20,7 @@ substitutions merge(substitutions const & s1, substitutions const & s2);
\pre symm == false ==> is_local(lhs(typeof(H)))
\pre symm == false ==> is_local(rhs(typeof(H))) */
expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
expr const & mvar, expr const & H, bool symm, substitutions * substs);
expr const & mvar, expr const & H, bool symm, hsubstitution * substs);
void initialize_subst_tactic();
void finalize_subst_tactic();