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

fix(library/tactic/apply_tactic): bug in apply_tac

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-24 15:54:56 -08:00
parent cb95b14332
commit 6cc57cc4b5
5 changed files with 19 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/type_checker.cpp
View file

@ -512,7 +512,13 @@ expr type_check(expr const & e, ro_environment const & env, context const & ctx
bool is_convertible(expr const & given, expr const & expected, ro_environment const & env, context const & ctx) {
return type_checker(env).is_convertible(given, expected, ctx);
}
bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional<metavar_env> const & menv) {
return type_checker(env).is_proposition(e, ctx, menv);
}
bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, metavar_env const & menv) {
return is_proposition(e, env, ctx, some_menv(menv));
}
bool is_proposition(expr const & e, ro_environment const & env, context const & ctx) {
return type_checker(env).is_proposition(e, ctx);
return is_proposition(e, env, ctx, none_menv());
}
}

2
src/kernel/type_checker.h
View file

@ -111,5 +111,7 @@ public:
};
expr type_check(expr const & e, ro_environment const & env, context const & ctx = context());
bool is_convertible(expr const & t1, expr const & t2, ro_environment const & env, context const & ctx = context());
bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional<metavar_env> const & menv);
bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, metavar_env const & menv);
bool is_proposition(expr const & e, ro_environment const & env, context const & ctx = context());
}

2
src/library/tactic/apply_tactic.cpp
View file

@ -81,7 +81,7 @@ static optional<proof_state> apply_tactic(ro_environment const & env, proof_stat
hypotheses extra_hs;
while (is_pi(arg_type)) {
expr d = abst_domain(arg_type);
name n = arg_to_hypothesis_name(env, context(), abst_name(arg_type), d);
name n = arg_to_hypothesis_name(abst_name(arg_type), d, env, context(), new_menv);
n = add_hypothesis(n, d);
extra_hs.emplace_front(n, d);
arg_type = instantiate(abst_body(arg_type), mk_constant(n, d), new_menv);

6
src/library/tactic/proof_state.cpp
View file

@ -88,8 +88,8 @@ void proof_state::get_goal_names(name_set & r) const {
}
}
name arg_to_hypothesis_name(ro_environment const & env, context const & ctx, name const & n, expr const & d) {
if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx))
name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx, optional<metavar_env> const & menv) {
if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx, menv))
return name("H");
else
return n;
@ -100,7 +100,7 @@ static name g_main("main");
proof_state to_proof_state(ro_environment const & env, context ctx, expr t) {
list<std::pair<name, expr>> extra_binders;
while (is_pi(t)) {
name vname = arg_to_hypothesis_name(env, ctx, abst_name(t), abst_domain(t));
name vname = arg_to_hypothesis_name(abst_name(t), abst_domain(t), env, ctx);
extra_binders.emplace_front(vname, abst_domain(t));
ctx = extend(ctx, vname, abst_domain(t));
t = abst_body(t);

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

@ -124,7 +124,11 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state & s)
\brief Return a name based on \c n that is suitable to be used as a hypothesis name
It basically renames \c n to 'H' if \c d is a proposition and \c n is the default arrow binder name.
*/
name arg_to_hypothesis_name(ro_environment const & env, context const & ctx, name const & n, expr const & d);
name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx,
optional<metavar_env> const & menv = none_menv());
inline name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx, metavar_env const & menv) {
return arg_to_hypothesis_name(n, d, env, ctx, some_menv(menv));
}
UDATA_DEFS_CORE(goals)
UDATA_DEFS(proof_state)