From c133d2650537172cbbbc9592878f3d401a99e77b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 May 2015 16:21:15 -0700 Subject: [PATCH] feat(frontends/lean/builtin_exprs): change how 'show' is processed in tactics Unresolved placeholders were not being reported --- hott/types/sigma.hlean | 7 +++---- src/frontends/lean/builtin_exprs.cpp | 7 +------ tests/lean/show_tac.lean | 7 +++++++ tests/lean/show_tac.lean.expected.out | 18 ++++++++++++++++++ 4 files changed, 29 insertions(+), 10 deletions(-) create mode 100644 tests/lean/show_tac.lean create mode 100644 tests/lean/show_tac.lean.expected.out diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 47704b091..481cceab0 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -205,17 +205,16 @@ namespace sigma intro u, cases u with a b, apply (sigma_eq (left_inv f a)), - show transport B (left_inv f a) ((g (f⁻¹ (f a)))⁻¹ (transport B' (right_inv f (f a))⁻¹ (g a b))) = b, - from calc + calc transport B (left_inv f a) ((g (f⁻¹ (f a)))⁻¹ (transport B' (right_inv f (f a))⁻¹ (g a b))) = (g a)⁻¹ (transport (B' ∘ f) (left_inv f a) (transport B' (right_inv f (f a))⁻¹ (g a b))) - : by rewrite (fn_tr_eq_tr_fn (left_inv f a) (λ a, (g a)⁻¹)) + : by esimp; rewrite (fn_tr_eq_tr_fn (left_inv f a) (λ a, (g a)⁻¹)) ... = (g a)⁻¹ (transport B' (ap f (left_inv f a)) (transport B' (right_inv f (f a))⁻¹ (g a b))) : ap (g a)⁻¹ !transport_compose ... = (g a)⁻¹ (transport B' (ap f (left_inv f a)) (transport B' (ap f (left_inv f a))⁻¹ (g a b))) : ap (λ x, (g a)⁻¹ (transport B' (ap f (left_inv f a)) (transport B' x⁻¹ (g a b)))) (adj f a) ... = (g a)⁻¹ (g a b) : {!tr_inv_tr} - ... = b : by rewrite (left_inv (g a) b) + ... = b : by esimp; rewrite (left_inv (g a) b) end definition sigma_equiv_sigma_of_is_equiv [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)] diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 0e8f58890..eac15967b 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -228,14 +228,9 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & throw parser_error("invalid 'have' tactic, 'by', 'begin', 'proof', or 'from' expected", p.pos()); } } - } else if (p.curr_is_token(get_show_tk())) { - auto pos = p.pos(); - expr t = p.parse_tactic_expr_arg(); - t = p.mk_app(get_rexact_tac_fn(), t, pos); - add_tac(t, pos); } else if (p.curr_is_token(get_match_tk()) || p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) || p.curr_is_token(get_fun_tk()) || - p.curr_is_token(get_calc_tk())) { + p.curr_is_token(get_calc_tk()) || p.curr_is_token(get_show_tk())) { auto pos = p.pos(); expr t = p.parse_tactic_expr_arg(); t = p.mk_app(get_exact_tac_fn(), t, pos); diff --git a/tests/lean/show_tac.lean b/tests/lean/show_tac.lean new file mode 100644 index 000000000..291e8aa2e --- /dev/null +++ b/tests/lean/show_tac.lean @@ -0,0 +1,7 @@ +example (a b : Prop) : a ∧ b → b ∧ a := +begin + intro Hab, + have Ha : a, from and.elim_left Hab, + have Hb : b, from and.elim_right Hab, + show b ∧ a, from and.intro _ Ha +end diff --git a/tests/lean/show_tac.lean.expected.out b/tests/lean/show_tac.lean.expected.out new file mode 100644 index 000000000..e823be637 --- /dev/null +++ b/tests/lean/show_tac.lean.expected.out @@ -0,0 +1,18 @@ +show_tac.lean:6:29: error: don't know how to synthesize placeholder +a b : Prop, +Hab : a ∧ b, +Ha : a, +Hb : b +⊢ b +show_tac.lean:6:2: error:invalid 'exact' tactic, term still contains metavariables after elaboration + show b ∧ a, from and.intro ?M_1 Ha +proof state: +a b : Prop, +Hab : a ∧ b, +Ha : a, +Hb : b +⊢ b ∧ a +show_tac.lean:7:0: error: failed to add declaration '14.0' to environment, value has metavariables +remark: set 'formatter.hide_full_terms' to false to see the complete term + λ (a b : Prop) (Hab : …), + ?M_1