From e0debca7719b1db3103b0a69235d0cb3c7330456 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Nov 2014 22:25:37 -0800 Subject: [PATCH] feat(library/tactic/inversion_tactic): add 'case ... with ...' variant that allows user to specify names for new hypotheses --- library/tools/tactic.lean | 13 ++++++----- src/library/tactic/inversion_tactic.cpp | 29 +++++++++++++++++++------ src/library/tactic/inversion_tactic.h | 2 +- tests/lean/run/vec_inv2.lean | 29 +++++++++++++++++++++++++ 4 files changed, 60 insertions(+), 13 deletions(-) create mode 100644 tests/lean/run/vec_inv2.lean diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index 1ec2c52ea..89d007014 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -57,8 +57,7 @@ opaque definition revert (e : expr) : tactic := builtin opaque definition unfold (e : expr) : tactic := builtin opaque definition exact (e : expr) : tactic := builtin opaque definition trace (s : string) : tactic := builtin -opaque definition inversion (e : expr) : tactic := builtin -definition cases := inversion +opaque definition inversion (id : expr) : tactic := builtin notation a `↦` b := rename a b @@ -66,17 +65,21 @@ inductive expr_list : Type := nil : expr_list, cons : expr → expr_list → expr_list -opaque definition intro_lst (es : expr_list) : tactic := builtin +opaque definition inversion_with (id : expr) (ids : expr_list) : tactic := builtin +notation `cases` a := inversion a +notation `cases` a `with` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := inversion_with a l + +opaque definition intro_lst (ids : expr_list) : tactic := builtin notation `intros` := intro_lst expr_list.nil notation `intros` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := intro_lst l opaque definition generalize_lst (es : expr_list) : tactic := builtin notation `generalizes` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := generalize_lst l -opaque definition clear_lst (es : expr_list) : tactic := builtin +opaque definition clear_lst (ids : expr_list) : tactic := builtin notation `clears` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := clear_lst l -opaque definition revert_lst (es : expr_list) : tactic := builtin +opaque definition revert_lst (ids : expr_list) : tactic := builtin notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l infixl `;`:15 := and_then diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index c34834f14..67d8ff207 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -18,6 +18,7 @@ class inversion_tac { environment const & m_env; io_state const & m_ios; proof_state const & m_ps; + list m_ids; name_generator m_ngen; substitution m_subst; std::unique_ptr m_tc; @@ -192,7 +193,14 @@ class inversion_tac { expr g_type = g.get_type(); for (unsigned i = 0; i < nargs; i++) { expr type = binding_domain(g_type); - expr new_h = mk_local(m_ngen.next(), get_unused_name(binding_name(g_type), new_hyps), type, binder_info()); + name new_h_name; + if (m_ids) { + new_h_name = head(m_ids); + m_ids = tail(m_ids); + } else { + new_h_name = binding_name(g_type); + } + expr new_h = mk_local(m_ngen.next(), get_unused_name(new_h_name, new_hyps), type, binder_info()); new_hyps.push_back(new_h); g_type = instantiate(binding_body(g_type), new_h); } @@ -400,8 +408,8 @@ class inversion_tac { } public: - inversion_tac(environment const & env, io_state const & ios, proof_state const & ps): - m_env(env), m_ios(ios), m_ps(ps), + inversion_tac(environment const & env, io_state const & ios, proof_state const & ps, list const & ids): + m_env(env), m_ios(ios), m_ps(ps), m_ids(ids), m_ngen(m_ps.get_ngen()), m_tc(mk_type_checker(m_env, m_ngen.mk_child(), m_ps.relax_main_opaque())) { } @@ -432,9 +440,9 @@ public: } }; -tactic inversion_tactic(name const & n) { +tactic inversion_tactic(name const & n, list const & ids) { auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) -> optional { - inversion_tac tac(env, ios, ps); + inversion_tac tac(env, ios, ps, ids); return tac.execute(n); }; return tactic01(fn); @@ -443,8 +451,15 @@ tactic inversion_tactic(name const & n) { void initialize_inversion_tactic() { register_tac(name({"tactic", "inversion"}), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - name n = tactic_expr_to_id(app_arg(e), "invalid 'inversion' tactic, argument must be an identifier"); - return inversion_tactic(n); + name n = tactic_expr_to_id(app_arg(e), "invalid 'inversion/cases' tactic, argument must be an identifier"); + return inversion_tactic(n, list()); + }); + register_tac(name({"tactic", "inversion_with"}), + [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + name n = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'cases-with' tactic, argument must be an identifier"); + buffer ids; + get_tactic_id_list_elements(app_arg(e), ids, "invalid 'cases-with' tactic, list of identifiers expected"); + return inversion_tactic(n, to_list(ids.begin(), ids.end())); }); } void finalize_inversion_tactic() {} diff --git a/src/library/tactic/inversion_tactic.h b/src/library/tactic/inversion_tactic.h index 92f7d550e..83864ee31 100644 --- a/src/library/tactic/inversion_tactic.h +++ b/src/library/tactic/inversion_tactic.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" namespace lean { -tactic inversion_tactic(name const & from, name const & to); +tactic inversion_tactic(name const & n, list const & ids = list()); void initialize_inversion_tactic(); void finalize_inversion_tactic(); } diff --git a/tests/lean/run/vec_inv2.lean b/tests/lean/run/vec_inv2.lean new file mode 100644 index 000000000..18c42f35c --- /dev/null +++ b/tests/lean/run/vec_inv2.lean @@ -0,0 +1,29 @@ +import data.nat.basic data.empty data.prod +open nat eq.ops prod + +inductive vector (T : Type) : ℕ → Type := + nil {} : vector T 0, + cons : T → ∀{n}, vector T n → vector T (succ n) + +set_option pp.metavar_args true +set_option pp.implicit true +set_option pp.notation false + +namespace vector + variables {A B C : Type} + variables {n m : nat} + + theorem z_cases_on {C : vector A 0 → Type} (v : vector A 0) (Hnil : C nil) : C v := + begin + cases v, + apply Hnil + end + + protected definition destruct (v : vector A (succ n)) {P : Π {n : nat}, vector A (succ n) → Type} + (H : Π {n : nat} (h : A) (t : vector A n), P (cons h t)) : P v := + begin + cases v with (h', n', t'), + apply (H h' t') + end + +end vector