feat(meta/interactive): Allow case to match multiple cases

library/init/meta/interactive.lean

@@ -659,6 +659,15 @@ do ⟨exact_matches, suffix_matches⟩ ← goals_with_matching_tag ns,
      "Invalid `case`: there is more than one goal tagged with tag {ns}."
    end
 
+meta def case_arg_parser : lean.parser (list name × option (list name)) :=
+prod.mk <$> ident_* <*> (tk ":" *> ident_*)?
+
+meta def case_parser : lean.parser (list (list name × option (list name))) :=
+  (list_of case_arg_parser)
+  <|>
+  (functor.map (λ x, [x]) case_arg_parser)
+
+
 /--
 Focuses on a goal ('case') generated by `induction`, `cases` or `with_cases`.
 
@@ -698,6 +707,11 @@ Note that this renaming functionality only work reliably *directly after* an
 `induction`/`cases`/`with_cases`. If you need to perform additional work after
 an `induction` or `cases` (e.g. introduce hypotheses in all goals), use
 `with_cases`.
+
+Multiple cases can be handled by the same tactic block with
+```
+case [A : N₀ ... Nₙ, B : M₀ ... Mₙ] {...}
+```
 -/
 /-
 TODO `case` could be generalised to work with zero names as well. The form
@@ -709,24 +723,40 @@ hypotheses to `x, y, z`. The renaming functionality would be available only if
 the goal has a case tag.
 -/
 meta def case (ns : parse ident_*) (ids : parse $ (tk ":" *> ident_*)?) (tac : itactic) : tactic unit :=
-do ⟨goal, tag⟩ ← goal_with_matching_tag ns,
-   let ids := ids.get_or_else [],
-   let num_ids := ids.length,
-   goals ← get_goals,
-   set_goals $ goal :: goals.filter (≠ goal),
-   match tag with
-   | (case_tag.pi _ num_args) := do
-     intro_lst ids,
-     when (num_ids < num_args) $ intron (num_args - num_ids)
-   | (case_tag.hyps _ new_hyp_names) := do
-       let num_new_hyps := new_hyp_names.length,
-       when (num_ids > num_new_hyps) $ fail format!
-         "Invalid `case`: You gave {num_ids} names, but the case introduces
-         {num_new_hyps} new hypotheses.",
-       let renamings := rb_map.of_list (new_hyp_names.zip ids),
-       propagate_tags $ tactic.rename_many renamings tt tt
-   end,
-   solve1 tac
+do
+  target_goals ← args.mmap (λ ⟨ns, ids⟩, do
+    ⟨goal, tag⟩ ← goal_with_matching_tag ns,
+    let ids := ids.get_or_else [],
+    let num_ids := ids.length,
+    goals ← get_goals,
+    let other_goals := goals.filter (≠ goal),
+    set_goals [goal],
+    match tag with
+    | (case_tag.pi _ num_args) := do
+      intro_lst ids,
+      when (num_ids < num_args) $ intron (num_args - num_ids)
+    | (case_tag.hyps _ new_hyp_names) := do
+        let num_new_hyps := new_hyp_names.length,
+        when (num_ids > num_new_hyps) $ fail format!
+          "Invalid `case'`: You gave {num_ids} names, but the case introduces
+          {num_new_hyps} new hypotheses.",
+        let renamings := native.rb_map.of_list (new_hyp_names.zip ids),
+        propagate_tags $ tactic.rename_many renamings tt tt
+    end,
+    goals ← get_goals,
+    set_goals other_goals,
+    match goals with
+    | [g] := return g
+    | _ := fail "Unexpected goals introduced by renaming"
+    end),
+  remaining_goals ← get_goals,
+  set_goals target_goals,
+  tac,
+  unsolved_goals ← get_goals,
+  match unsolved_goals with
+  | [] := set_goals remaining_goals
+  | _ := fail "case tactic failed, focused goals have not been solved"
+  end
 
 /--
 Assuming `x` is a variable in the local context with an inductive type, `destruct x` splits the main goal, producing one goal for each constructor of the inductive type, in which `x` is assumed to be a general instance of that constructor. In contrast to `cases`, the local context is unchanged, i.e. no elements are reverted or introduced.

tests/lean/case.lean

@@ -81,3 +81,29 @@ begin
   case nil { exact 0 },
   case cons : x xs { exact 0 }
 end
+
+example (α β : Type*) (i j : α ⊕ β) : ℕ :=
+begin
+  with_cases {cases hi : i; cases hj : j},
+  case [sum.inl sum.inl, sum.inr sum.inr] {
+    exact 1,
+    exact 1,
+  },
+  case [sum.inl sum.inr, sum.inr sum.inl] {
+    exact 2,
+    exact 2,
+  },
+end
+
+example (α β : Type*) (i j : α ⊕ β) : ℕ :=
+begin
+  with_cases {cases hi : i; cases hj : j},
+  case [sum.inl sum.inl : i j, sum.inr sum.inr : i j] {
+    exact 1,
+    exact 1,
+  },
+  case [sum.inl sum.inr : i j, sum.inr sum.inl : i j] {
+    exact 2,
+    exact 2,
+  },
+end

tests/lean/case.lean.expected.out

@@ -1,30 +1,30 @@
-case.lean:4:2: error: solve1 tactic failed, focused goal has not been solved
+case.lean:4:2: error: case tactic failed, focused goals have not been solved
 state:
 case list.cons
 xs_hd : ℕ,
 xs_tl : list ℕ,
 xs_ih : ℕ
 ⊢ ℕ
-case.lean:10:2: error: solve1 tactic failed, focused goal has not been solved
+case.lean:10:2: error: case tactic failed, focused goals have not been solved
 state:
 case list.cons
 xs_hd : ℕ,
 xs_tl : list ℕ
 ⊢ ℕ
-case.lean:18:4: error: solve1 tactic failed, focused goal has not been solved
+case.lean:18:4: error: case tactic failed, focused goals have not been solved
 state:
 case list.cons, list.cons
 x xs_ih x : ℕ,
 xs : list ℕ
 ⊢ ℕ
-case.lean:26:2: error: solve1 tactic failed, focused goal has not been solved
+case.lean:26:2: error: case tactic failed, focused goals have not been solved
 state:
 case list.cons
 xs_hd : ℕ,
 xs_tl : list ℕ,
 xs_ih : ℕ
 ⊢ ℕ
-case.lean:32:2: error: solve1 tactic failed, focused goal has not been solved
+case.lean:32:2: error: case tactic failed, focused goals have not been solved
 state:
 case list.cons
 xs : list ℕ,
@@ -42,7 +42,7 @@ case list.cons
 xs_hd : ℕ,
 xs_tl : list ℕ
 ⊢ ℕ
-case.lean:44:2: error: solve1 tactic failed, focused goal has not been solved
+case.lean:44:2: error: case tactic failed, focused goals have not been solved
 state:
 case list.cons
 xs_hd : ℕ,
@@ -108,7 +108,7 @@ xs_hd : ℕ,
 xs_tl : list ℕ,
 xs_ih : ℕ
 ⊢ ℕ
-case.lean:68:2: error: solve1 tactic failed, focused goal has not been solved
+case.lean:68:2: error: case tactic failed, focused goals have not been solved
 state:
 x : ℕ,
 xs : list ℕ,