feat(library/init/meta/interactive): add cases_matching p tactic

doc/changes.md

@@ -48,6 +48,10 @@ master branch (aka work in progress branch)
 - Add `guard_names { t }`. This tactic applies `t` to the main goal,
   and reverts any new hypothesis in the resulting subgoals.
 
+- Add `cases_matching p` tactic for applying the `cases` tactic to a hypothesis `h : t` s.t.
+  `t` matches the pattern `p`. Alternative versions: `cases_matching * p` and `cases_matching [p_1, ..., p_n]`.
+  Example: `cases_matching * [_ ∨ _, _ ∧ _]` destructs all conjunctions and disjunctions in the main goal.
+
 *Changes*
 
 - `cases h` now also tries to clear `h` when performing dependent elimination.

library/data/rbtree/basic.lean

@@ -6,15 +6,11 @@ Authors: Leonardo de Moura
 universe u
 
 namespace tactic
-/- TODO(Leo): move blast_disjs to another file. -/
 
 namespace interactive
 
 meta def blast_disjs : tactic unit :=
-focus1 $ repeat $ any_hyp $ λ h, do
-  t ← infer_type h,
-  guard (t.is_or ≠ none),
-  tactic.cases h [h.local_pp_name, h.local_pp_name]
+`[cases_matching * _ ∨ _]
 
 end interactive
 end tactic

library/data/rbtree/insert.lean

@@ -256,8 +256,8 @@ begin
   apply ins.induction lt t z; intros; simp [mem, ins, strict_weak_order.equiv, *] at *; blast_disjs,
   any_goals { simp [h] },
   any_goals { have ih := ih h, cases ih; simp [*], done },
-  { have h := of_mem_balance1_node lt h, blast_disjs, have := ih h, blast_disjs, all_goals { simp [*] } },
-  { have h := of_mem_balance2_node lt h, blast_disjs, have := ih h, blast_disjs, all_goals { simp [*] } }
+  { have h' := of_mem_balance1_node lt h, blast_disjs, have := ih h', blast_disjs, all_goals { simp [*] } },
+  { have h' := of_mem_balance2_node lt h, blast_disjs, have := ih h', blast_disjs, all_goals { simp [*] } }
 end
 
 lemma equiv_or_mem_of_mem_insert [is_strict_weak_order α lt] {t : rbnode α} {x z} : ∀ (h : x ∈ t.insert lt z), x ≈[lt] z ∨ x ∈ t :=

library/init/meta/interactive.lean

@@ -599,6 +599,30 @@ meta def cases : parse cases_arg_p → parse with_ident_list → tactic unit
   hx  ← get_local x,
   tactic.cases hx ids
 
+private meta def find_matching_hyp (ps : list pattern) : tactic expr :=
+do ctx ← local_context,
+   ctx.mfirst $ λ h, do
+     type ← infer_type h,
+     ps.mfirst $ λ p, do
+       match_pattern_core reducible p type,
+       return h
+
+/--
+`cases_matching p` applies the `cases` tactic to a hypothesis `h : type` if `type` matches the pattern `p`.
+`cases_matching [p_1, ..., p_n]` applies the `cases` tactic to a hypothesis `h : type` if `type` matches one of the given patterns.
+`cases_matching * p` more efficient and compact version of `focus1 { repeat { cases_matching p } }`. It is more efficient because the pattern is compiled once.
+
+Example: The following tactic destructs all conjunctions and disjunctions in the current goal.
+```
+cases_matching * [_ ∨ _, _ ∧ _]
+```
+-/
+meta def cases_matching (rec : parse $ (tk "*")?) (ps : parse pexpr_list_or_texpr) : tactic unit :=
+do ps ← ps.mmap pexpr_to_pattern,
+   if rec.is_none
+   then find_matching_hyp ps >>= tactic.cases
+   else tactic.focus1 $ tactic.repeat $ find_matching_hyp ps >>= tactic.cases
+
 /--
 Tries to solve the current goal using a canonical proof of `true`, or the `reflexivity` tactic, or the `contradiction` tactic.
 -/