feat(library/tactic/inversion_tactic): add 'case ... with ...' variant that allows user to specify names for new hypotheses

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

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<name>                    m_ids;
     name_generator                m_ngen;
     substitution                  m_subst;
     std::unique_ptr<type_checker> 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<name> 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<name> const & ids) {
     auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) -> optional<proof_state> {
-        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<name>());
+                 });
+    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<name> 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() {}

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<name> const & ids = list<name>());
 void initialize_inversion_tactic();
 void finalize_inversion_tactic();
 }

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