From 2bc13f6bfd36ff4010e1344fb2f5aeb6c7cc6708 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Apr 2015 13:23:38 -0700 Subject: [PATCH] feat(library/tactic/exact): enforce goal type during elaboration when executing 'exact' tactic Remark: this was the behavior of the 'sexact' tactic. This commit also adds the 'rexact' (relaxed exact) tactic which does not enforce the goal type. closes #495 --- hott/algebra/precategory/functor.hlean | 3 ++- hott/algebra/precategory/nat_trans.hlean | 4 +-- hott/init/tactic.hlean | 5 ++-- library/init/tactic.lean | 5 ++-- src/emacs/lean-syntax.el | 5 ++-- src/frontends/lean/builtin_exprs.cpp | 12 ++++----- src/library/constants.cpp | 20 +++++++++------ src/library/constants.h | 5 ++-- src/library/constants.txt | 5 ++-- src/library/tactic/exact_tactic.cpp | 31 ++++++++++++++---------- src/library/tactic/exact_tactic.h | 2 +- 11 files changed, 56 insertions(+), 41 deletions(-) diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean index 6dc90b47c9..9022101508 100644 --- a/hott/algebra/precategory/functor.hlean +++ b/hott/algebra/precategory/functor.hlean @@ -134,7 +134,8 @@ namespace functor fapply equiv.MK, {intro S, fapply functor.mk, exact (S.1), exact (S.2.1), - exact (pr₁ S.2.2), exact (pr₂ S.2.2)}, + -- TODO(Leo): investigate why we need to use relaxed-exact (rexact) tactic here + exact (pr₁ S.2.2), rexact (pr₂ S.2.2)}, {intro F, cases F with [d1, d2, d3, d4], exact ⟨d1, d2, (d3, @d4)⟩}, diff --git a/hott/algebra/precategory/nat_trans.hlean b/hott/algebra/precategory/nat_trans.hlean index 09237859ca..5f7bed90d2 100644 --- a/hott/algebra/precategory/nat_trans.hlean +++ b/hott/algebra/precategory/nat_trans.hlean @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: algebra.precategory.nat_trans Author: Floris van Doorn, Jakob von Raumer -/ - import .functor .iso open eq category functor is_trunc equiv sigma.ops sigma is_equiv function pi funext iso @@ -63,7 +62,8 @@ namespace nat_trans (Σ (η : Π (a : C), hom (F a) (G a)), Π (a b : C) (f : hom a b), G f ∘ η a = η b ∘ F f) ≃ (F ⟹ G) := begin fapply equiv.mk, - intro S, apply nat_trans.mk, exact (S.2), + -- TODO(Leo): investigate why we need to use rexact in the following line + {intro S, apply nat_trans.mk, rexact (S.2)}, fapply adjointify, intro H, fapply sigma.mk, diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 054e0e33bc..e51348efa4 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -61,9 +61,10 @@ opaque definition generalize (e : expr) : tactic := builtin opaque definition clear (e : expr) : tactic := builtin opaque definition revert (e : expr) : tactic := builtin opaque definition unfold (e : expr) : tactic := builtin +opaque definition refine (e : expr) : tactic := builtin opaque definition exact (e : expr) : tactic := builtin --- rexact is similar to exact, but the goal type is enforced during elaboration -opaque definition sexact (e : expr) : tactic := builtin +-- Relaxed version of exact that does not enforce goal type +opaque definition rexact (e : expr) : tactic := builtin opaque definition trace (s : string) : tactic := builtin inductive expr_list : Type := diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 6262d15b14..2c9fa79f26 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -61,9 +61,10 @@ opaque definition generalize (e : expr) : tactic := builtin opaque definition clear (e : expr) : tactic := builtin opaque definition revert (e : expr) : tactic := builtin opaque definition unfold (e : expr) : tactic := builtin +opaque definition refine (e : expr) : tactic := builtin opaque definition exact (e : expr) : tactic := builtin --- rexact is similar to exact, but the goal type is enforced during elaboration -opaque definition sexact (e : expr) : tactic := builtin +-- Relaxed version of exact that does not enforce goal type +opaque definition rexact (e : expr) : tactic := builtin opaque definition trace (s : string) : tactic := builtin inductive expr_list : Type := diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 9c995213a8..bc4a64ec8d 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -131,8 +131,9 @@ (group (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "fapply" "rename" "intro" "intros" "all_goals" "fold" - "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat" - "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" "unfold" "change")) + "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact" + "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" + "unfold" "change")) word-end) (1 'font-lock-constant-face)) ;; Types diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index f0e3e6a2c8..b346459fa8 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -187,7 +187,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & if (p.curr_is_token(get_bar_tk())) { expr local = p.save_pos(mk_local(id, A), id_pos); expr t = parse_local_equations(p, local); - t = p.mk_app(get_exact_tac_fn(), t, pos); + t = p.mk_app(get_rexact_tac_fn(), t, pos); t = p.save_pos(mk_begin_end_element_annotation(t), pos); t = p.save_pos(mk_begin_end_annotation(t), pos); add_tac(t, pos); @@ -198,7 +198,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & p.next(); auto pos = p.pos(); expr t = p.parse_expr(); - t = p.mk_app(get_exact_tac_fn(), t, pos); + t = p.mk_app(get_rexact_tac_fn(), t, pos); t = p.save_pos(mk_begin_end_element_annotation(t), pos); t = p.save_pos(mk_begin_end_annotation(t), pos); add_tac(t, pos); @@ -207,7 +207,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & p.next(); expr t = p.parse_expr(); p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected"); - t = p.mk_app(get_exact_tac_fn(), t, pos); + t = p.mk_app(get_rexact_tac_fn(), t, pos); t = p.save_pos(mk_begin_end_element_annotation(t), pos); t = p.save_pos(mk_begin_end_annotation(t), pos); add_tac(t, pos); @@ -227,13 +227,13 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & } else if (p.curr_is_token(get_show_tk())) { auto pos = p.pos(); expr t = p.parse_expr(); - t = p.mk_app(get_exact_tac_fn(), t, pos); + 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())) { auto pos = p.pos(); expr t = p.parse_expr(); - t = p.mk_app(get_sexact_tac_fn(), t, pos); + t = p.mk_app(get_exact_tac_fn(), t, pos); add_tac(t, pos); } else { auto pos = p.pos(); @@ -278,7 +278,7 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & static expr parse_proof_qed_core(parser & p, pos_info const & pos) { expr r = p.parse_expr(); p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected"); - r = p.mk_by(p.mk_app(get_exact_tac_fn(), r, pos), pos); + r = p.mk_by(p.mk_app(get_rexact_tac_fn(), r, pos), pos); return r; } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index b216270d27..8ba45f88a1 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -96,14 +96,15 @@ name const * g_tactic_now = nullptr; name const * g_tactic_opt_expr_list = nullptr; name const * g_tactic_or_else = nullptr; name const * g_tactic_par = nullptr; -name const * g_tactic_sexact = nullptr; -name const * g_tactic_state = nullptr; +name const * g_tactic_refine = nullptr; name const * g_tactic_rename = nullptr; name const * g_tactic_repeat = nullptr; name const * g_tactic_revert = nullptr; name const * g_tactic_reverts = nullptr; +name const * g_tactic_rexact = nullptr; name const * g_tactic_rotate_left = nullptr; name const * g_tactic_rotate_right = nullptr; +name const * g_tactic_state = nullptr; name const * g_tactic_trace = nullptr; name const * g_tactic_try_for = nullptr; name const * g_tactic_unfold = nullptr; @@ -211,14 +212,15 @@ void initialize_constants() { g_tactic_opt_expr_list = new name{"tactic", "opt_expr_list"}; g_tactic_or_else = new name{"tactic", "or_else"}; g_tactic_par = new name{"tactic", "par"}; - g_tactic_sexact = new name{"tactic", "sexact"}; - g_tactic_state = new name{"tactic", "state"}; + g_tactic_refine = new name{"tactic", "refine"}; g_tactic_rename = new name{"tactic", "rename"}; g_tactic_repeat = new name{"tactic", "repeat"}; g_tactic_revert = new name{"tactic", "revert"}; g_tactic_reverts = new name{"tactic", "reverts"}; + g_tactic_rexact = new name{"tactic", "rexact"}; g_tactic_rotate_left = new name{"tactic", "rotate_left"}; g_tactic_rotate_right = new name{"tactic", "rotate_right"}; + g_tactic_state = new name{"tactic", "state"}; g_tactic_trace = new name{"tactic", "trace"}; g_tactic_try_for = new name{"tactic", "try_for"}; g_tactic_unfold = new name{"tactic", "unfold"}; @@ -327,14 +329,15 @@ void finalize_constants() { delete g_tactic_opt_expr_list; delete g_tactic_or_else; delete g_tactic_par; - delete g_tactic_sexact; - delete g_tactic_state; + delete g_tactic_refine; delete g_tactic_rename; delete g_tactic_repeat; delete g_tactic_revert; delete g_tactic_reverts; + delete g_tactic_rexact; delete g_tactic_rotate_left; delete g_tactic_rotate_right; + delete g_tactic_state; delete g_tactic_trace; delete g_tactic_try_for; delete g_tactic_unfold; @@ -442,14 +445,15 @@ name const & get_tactic_now_name() { return *g_tactic_now; } name const & get_tactic_opt_expr_list_name() { return *g_tactic_opt_expr_list; } name const & get_tactic_or_else_name() { return *g_tactic_or_else; } name const & get_tactic_par_name() { return *g_tactic_par; } -name const & get_tactic_sexact_name() { return *g_tactic_sexact; } -name const & get_tactic_state_name() { return *g_tactic_state; } +name const & get_tactic_refine_name() { return *g_tactic_refine; } name const & get_tactic_rename_name() { return *g_tactic_rename; } name const & get_tactic_repeat_name() { return *g_tactic_repeat; } name const & get_tactic_revert_name() { return *g_tactic_revert; } name const & get_tactic_reverts_name() { return *g_tactic_reverts; } +name const & get_tactic_rexact_name() { return *g_tactic_rexact; } name const & get_tactic_rotate_left_name() { return *g_tactic_rotate_left; } name const & get_tactic_rotate_right_name() { return *g_tactic_rotate_right; } +name const & get_tactic_state_name() { return *g_tactic_state; } name const & get_tactic_trace_name() { return *g_tactic_trace; } name const & get_tactic_try_for_name() { return *g_tactic_try_for; } name const & get_tactic_unfold_name() { return *g_tactic_unfold; } diff --git a/src/library/constants.h b/src/library/constants.h index 8c4b50f3c7..a5547d31b8 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -98,14 +98,15 @@ name const & get_tactic_now_name(); name const & get_tactic_opt_expr_list_name(); name const & get_tactic_or_else_name(); name const & get_tactic_par_name(); -name const & get_tactic_sexact_name(); -name const & get_tactic_state_name(); +name const & get_tactic_refine_name(); name const & get_tactic_rename_name(); name const & get_tactic_repeat_name(); name const & get_tactic_revert_name(); name const & get_tactic_reverts_name(); +name const & get_tactic_rexact_name(); name const & get_tactic_rotate_left_name(); name const & get_tactic_rotate_right_name(); +name const & get_tactic_state_name(); name const & get_tactic_trace_name(); name const & get_tactic_try_for_name(); name const & get_tactic_unfold_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 67b32a2b47..858c18076c 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -91,14 +91,15 @@ tactic.now tactic.opt_expr_list tactic.or_else tactic.par -tactic.sexact -tactic.state +tactic.refine tactic.rename tactic.repeat tactic.revert tactic.reverts +tactic.rexact tactic.rotate_left tactic.rotate_right +tactic.state tactic.trace tactic.try_for tactic.unfold diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index 14fd785238..a9fb56d5ca 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -37,28 +37,33 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type }); } -static expr * g_exact_tac_fn = nullptr; -static expr * g_sexact_tac_fn = nullptr; +static expr * g_exact_tac_fn = nullptr; +static expr * g_rexact_tac_fn = nullptr; +static expr * g_refine_tac_fn = nullptr; expr const & get_exact_tac_fn() { return *g_exact_tac_fn; } -expr const & get_sexact_tac_fn() { return *g_sexact_tac_fn; } +expr const & get_rexact_tac_fn() { return *g_rexact_tac_fn; } +expr const & get_refine_tac_fn() { return *g_refine_tac_fn; } void initialize_exact_tactic() { - name const & exact_tac_name = get_tactic_exact_name(); - name const & sexact_tac_name = get_tactic_sexact_name(); - g_exact_tac_fn = new expr(Const(exact_tac_name)); - g_sexact_tac_fn = new expr(Const(sexact_tac_name)); + name const & exact_tac_name = get_tactic_exact_name(); + name const & rexact_tac_name = get_tactic_rexact_name(); + name const & refine_tac_name = get_tactic_refine_name(); + g_exact_tac_fn = new expr(Const(exact_tac_name)); + g_rexact_tac_fn = new expr(Const(rexact_tac_name)); + g_refine_tac_fn = new expr(Const(refine_tac_name)); register_tac(exact_tac_name, - [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument"); - return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), false); - }); - register_tac(sexact_tac_name, [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument"); return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true); }); + register_tac(rexact_tac_name, + [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { + check_tactic_expr(app_arg(e), "invalid 'rexact' tactic, invalid argument"); + return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), false); + }); } void finalize_exact_tactic() { delete g_exact_tac_fn; - delete g_sexact_tac_fn; + delete g_rexact_tac_fn; + delete g_refine_tac_fn; } } diff --git a/src/library/tactic/exact_tactic.h b/src/library/tactic/exact_tactic.h index 6c87c4e8b2..6c42649637 100644 --- a/src/library/tactic/exact_tactic.h +++ b/src/library/tactic/exact_tactic.h @@ -9,7 +9,7 @@ Author: Leonardo de Moura namespace lean { expr const & get_exact_tac_fn(); -expr const & get_sexact_tac_fn(); +expr const & get_rexact_tac_fn(); /** \brief Solve first goal iff it is definitionally equal to type of \c e */ void initialize_exact_tactic(); void finalize_exact_tactic();