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

feat(library/tactic/intro_tactic): allow '_' in interactive mode as the anonymous name for intros, cases, induction

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-09 15:42:36 -08:00
parent b6f6126075
commit 3e757d890a
2 changed files with 12 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/init/meta/interactive.lean
View file

@ -29,8 +29,10 @@ meta def list_of (p : parser α) := tk "[" *> sep_by "," p <* tk "]"
'<|>' (rbp 2), ';' (rbp 1), and ',' (rbp 0). It should be used for any (potentially)
trailing expression parameters. -/
meta def texpr := qexpr 2
/-- Parse an identifier or a '_' -/
meta def ident_ : parser name := ident <|> tk "_" >> return `_
meta def using_ident := (tk "using" *> ident)?
meta def with_ident_list := (tk "with" *> ident*) <|> return []
meta def with_ident_list := (tk "with" *> ident_*) <|> return []
meta def without_ident_list := (tk "without" *> ident*) <|> return []
meta def location := (tk "at" *> ident*) <|> return []
meta def qexpr_list := list_of (qexpr 0)
@ -82,7 +84,7 @@ If the goal is an arrow `T → U`, then it puts in the local context either `h:T
If the goal is neither a Pi/forall nor starting with a let definition,
the tactic `intro` applies the tactic `whnf` until the tactic `intro` can be applied or the goal is not `head-reducible`.
-/
meta def intro : parse ident? → tactic unit
meta def intro : parse ident_? → tactic unit
| none := intro1 >> skip
| (some h) := tactic.intro h >> skip
@ -90,7 +92,7 @@ meta def intro : parse ident? → tactic unit
Similar to `intro` tactic. The tactic `intros` will keep introducing new hypotheses until the goal target is not a Pi/forall or let binder.
The variant `intros h_1 ... h_n` introduces `n` new hypotheses using the given identifiers to name them.
-/
meta def intros : parse ident* → tactic unit
meta def intros : parse ident_* → tactic unit
| [] := tactic.intros >> skip
| hs := intro_lst hs >> skip
@ -496,7 +498,7 @@ meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
(cfg : simp_config := {}) : tactic unit :=
simp_using_hs hs attr_names ids cfg
meta def simp_intros (ids : parse ident*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
meta def simp_intros (ids : parse ident_*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
(wo_ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit :=
do s ← mk_simp_set attr_names hs wo_ids,
match ids with
@ -505,7 +507,7 @@ do s ← mk_simp_set attr_names hs wo_ids,
end,
try triv >> try (reflexivity reducible)
meta def simph_intros (ids : parse ident*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
meta def simph_intros (ids : parse ident_*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
(wo_ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit :=
do s ← mk_simp_set attr_names hs wo_ids,
match ids with

10
src/library/tactic/intro_tactic.cpp
View file

@ -14,11 +14,11 @@ Author: Leonardo de Moura
#include "library/tactic/tactic_state.h"
namespace lean {
static name mk_aux_name(list<name> & given_names, name const & default_name) {
static name mk_aux_name(local_context const & lctx, list<name> & given_names, name const & default_name) {
if (given_names) {
name r = head(given_names);
given_names = tail(given_names);
return r;
return r == "_" ? lctx.get_unused_name(default_name) : r;
} else {
return default_name;
}
@ -29,7 +29,7 @@ optional<expr> intron(environment const & env, options const & opts, metavar_con
lean_assert(is_metavar(mvar));
optional<metavar_decl> g = mctx.find_metavar_decl(mvar);
if (!g) return none_expr();
type_context ctx = mk_type_context_for(env, opts, mctx, g->get_context());
type_context ctx = mk_type_context_for(env, opts, mctx, g->get_context());
expr type = g->get_type();
type_context::tmp_locals new_locals(ctx);
buffer<expr> new_Hs;
@ -41,7 +41,7 @@ optional<expr> intron(environment const & env, options const & opts, metavar_con
}
lean_assert(is_pi(type) || is_let(type));
if (is_pi(type)) {
expr H = new_locals.push_local(mk_aux_name(given_names, binding_name(type)), annotated_head_beta_reduce(binding_domain(type)),
expr H = new_locals.push_local(mk_aux_name(ctx.lctx(), given_names, binding_name(type)), annotated_head_beta_reduce(binding_domain(type)),
binding_info(type));
type = instantiate(binding_body(type), H);
new_Hs.push_back(H);
@ -49,7 +49,7 @@ optional<expr> intron(environment const & env, options const & opts, metavar_con
} else {
lean_assert(is_let(type));
expr H = new_locals.push_let(mk_aux_name(given_names, let_name(type)), annotated_head_beta_reduce(let_type(type)), let_value(type));
expr H = new_locals.push_let(mk_aux_name(ctx.lctx(), given_names, let_name(type)), annotated_head_beta_reduce(let_type(type)), let_value(type));
type = instantiate(let_body(type), H);
new_Hs.push_back(H);
new_Hns.push_back(mlocal_name(H));