From c9b72df34b53d902e609452e6fceafcac18e2ab4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Feb 2014 11:36:26 -0800 Subject: [PATCH] fix(frontends/lean/parser): bug when applying tactics to synthesize remaining meta-variables Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser_tactic.cpp | 6 +++++- tests/lean/apply_tac_bug.lean | 10 ++++++++++ tests/lean/apply_tac_bug.lean.expected.out | 6 ++++++ 3 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 tests/lean/apply_tac_bug.lean create mode 100644 tests/lean/apply_tac_bug.lean.expected.out diff --git a/src/frontends/lean/parser_tactic.cpp b/src/frontends/lean/parser_tactic.cpp index 19a794b23..765100631 100644 --- a/src/frontends/lean/parser_tactic.cpp +++ b/src/frontends/lean/parser_tactic.cpp @@ -254,7 +254,11 @@ expr parser_imp::apply_tactics(expr const & val, metavar_env & menv) { buffer mvars; for_each(val, [&](expr const & e, unsigned) { if (is_metavar(e)) { - mvars.push_back(e); + expr m = e; + if (has_local_context(m)) + m = mk_metavar(metavar_name(m)); + if (std::find(mvars.begin(), mvars.end(), m) == mvars.end()) + mvars.push_back(m); } return true; }); diff --git a/tests/lean/apply_tac_bug.lean b/tests/lean/apply_tac_bug.lean new file mode 100644 index 000000000..32787ea26 --- /dev/null +++ b/tests/lean/apply_tac_bug.lean @@ -0,0 +1,10 @@ +import heq +import macros +import tactic + +theorem my_proof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2 +:= let H1b : b := cast (by simp) H1, + H1_eq_H1b : H1 == H1b := hsymm (cast_heq (by simp) H1), + H1b_eq_H2 : H1b == H2 := to_heq (proof_irrel H1b H2) + in htrans H1_eq_H1b H1b_eq_H2 + diff --git a/tests/lean/apply_tac_bug.lean.expected.out b/tests/lean/apply_tac_bug.lean.expected.out new file mode 100644 index 000000000..2832fadc1 --- /dev/null +++ b/tests/lean/apply_tac_bug.lean.expected.out @@ -0,0 +1,6 @@ + Set: pp::colors + Set: pp::unicode + Imported 'heq' + Imported 'macros' + Imported 'tactic' + Proved: my_proof_irrel