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

fix(library/init/meta/relation_tactics,library/tactic/subst_tactic): fixes #1772

Browse source
This commit is contained in:
Leonardo de Moura 2017-08-21 14:51:30 -07:00
parent 5cbc1470b9
commit fb2186334a
3 changed files with 14 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/relation_tactics.lean
View file

@ -10,7 +10,7 @@ namespace tactic
open expr
private meta def relation_tactic (md : transparency) (op_for : environment → name → option name) (tac_name : string) : tactic unit :=
do tgt ← target,
do tgt ← target >>= instantiate_mvars,
env ← get_env,
let r := get_app_fn tgt,
match (op_for env (const_name r)) with

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

@ -40,7 +40,7 @@ expr subst(environment const & env, options const & opts, transparency_mode cons
lean_assert(mctx.find_metavar_decl(mvar));
metavar_decl g = mctx.get_metavar_decl(mvar);
type_context ctx = mk_type_context_for(env, opts, mctx, g.get_context(), m);
expr H_type = ctx.infer(H);
expr H_type = ctx.instantiate_mvars(ctx.infer(H));
expr lhs, rhs;
lean_verify(is_eq(H_type, lhs, rhs));
if (symm) std::swap(lhs, rhs);
@ -129,7 +129,7 @@ vm_obj tactic_subst(expr const & l, tactic_state const & s) {
optional<local_decl> d = lctx.find_local_decl(l);
if (!d)
return tactic::mk_exception(sstream() << "subst tactic failed, unknown '" << mlocal_pp_name(l) << "' hypothesis", s);
expr const & type = d->get_type();
expr type = mctx.instantiate_mvars(d->get_type());
expr lhs, rhs;
if (is_eq(type, lhs, rhs)) {
if (is_local(rhs) && !depends_on(lhs, mctx, lctx, rhs)) {
@ -138,7 +138,7 @@ vm_obj tactic_subst(expr const & l, tactic_state const & s) {
return tactic_subst_core(d->get_name(), false, s);
} else {
return tactic::mk_exception(sstream() << "subst tactic failed, hypothesis '"
<< mlocal_pp_name(l) << "' is not of the form (x = t) or (t = x)", s);
<< mlocal_pp_name(l) << "' is not of the form (x = t) or (t = x)", s);
}
} else {
bool found = false;
@ -146,7 +146,8 @@ vm_obj tactic_subst(expr const & l, tactic_state const & s) {
lctx.for_each_after(*d, [&](local_decl const & d2) {
if (found) return;
expr lhs, rhs;
if (is_eq(d2.get_type(), lhs, rhs)) {
expr type = mctx.instantiate_mvars(d2.get_type());
if (is_eq(type, lhs, rhs)) {
if (is_local(lhs) && mlocal_name(lhs) == d->get_name() && !depends_on(rhs, mctx, lctx, lhs)) {
found = true;
r = tactic_subst_core(d2.get_name(), false, s);

8
tests/lean/run/1772.lean Normal file
View file

@ -0,0 +1,8 @@
example (p : Prop) (f : ∀ q : Prop, q → q) : p = p :=
by apply f _ _; refl
example (p : Prop) (f : ∀ q : Prop, q → q) : p = p :=
by apply f _ _; transitivity; refl
example (p r : Prop) (f : ∀ q : Prop, (r = q → q) → q) (h2 : r): p :=
by apply f _ (λ h, _); subst h; assumption