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

feat(library/tactic/exact): enforce goal type during elaboration when executing 'exact' tactic

Browse source 
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
This commit is contained in:
Leonardo de Moura 2015-04-06 13:23:38 -07:00
parent 754276a660
commit 2bc13f6bfd
11 changed files with 56 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
hott/algebra/precategory/functor.hlean
View file

@ -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)⟩},

4
hott/algebra/precategory/nat_trans.hlean
View file

@ -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,

5
hott/init/tactic.hlean
View file

@ -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 :=

5
library/init/tactic.lean
View file

@ -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 :=

5
src/emacs/lean-syntax.el
View file

@ -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

12
src/frontends/lean/builtin_exprs.cpp
View file

@ -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;
}

20
src/library/constants.cpp
View file

@ -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; }

5
src/library/constants.h
View file

@ -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();

5
src/library/constants.txt
View file

@ -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

31
src/library/tactic/exact_tactic.cpp
View file

@ -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;
}
}

2
src/library/tactic/exact_tactic.h
View file

@ -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();