feat(library/init/meta/interactive): add goal tagging support for by_cases

This commit also incorporates changes suggested at commit 84a1911949dec94.

doc/changes.md

@@ -138,6 +138,8 @@ master branch (aka work in progress branch)
 
 * `apply` now also returns the new metavariables (and the parameter name associated with them). Even the assigned metavariables are returned.
 
+* `by_cases p with h` ==> `by_cases h : p`
+
 *API name changes*
 
 v3.3.0 (14 September 2017)

library/init/algebra/functions.lean

@@ -24,7 +24,7 @@ solve1 $ intros
 >> try `[apply le_of_not_le, assumption]
 
 meta def tactic.interactive.min_tac (a b : interactive.parse lean.parser.pexpr) : tactic unit :=
-`[by_cases (%%a ≤ %%b), iterate {min_tac_step}]
+interactive.by_cases (none, ``(%%a ≤ %%b)); min_tac_step
 
 lemma min_le_left (a b : α) : min a b ≤ a :=
 by min_tac a b

library/init/data/array/basic.lean

@@ -84,7 +84,7 @@ lemma of_beq_aux_eq_tt [∀ i, decidable_eq (α i)] {a b : d_array n α} : ∀ (
     have h₂' : read a ⟨i, h₁⟩ = read b ⟨i, h₁⟩ ∧ d_array.beq_aux a b i _ = tt, {simp [d_array.beq_aux] at h₂, assumption},
     have h₁' : i ≤ n, from le_of_lt h₁,
     have ih  : ∀ (j : nat) (h' : j < i), a.read ⟨j, lt_of_lt_of_le h' h₁'⟩ = b.read ⟨j, lt_of_lt_of_le h' h₁'⟩, from of_beq_aux_eq_tt i h₁' h₂'.2,
-    by_cases j = i with hji,
+    by_cases hji : j = i,
     { subst hji, exact h₂'.1 },
     { have j_lt_i : j < i, from lt_of_le_of_ne (nat.le_of_lt_succ h₃) hji,
       exact ih j j_lt_i }

library/init/data/bool/lemmas.lean

@@ -141,7 +141,7 @@ by cases a; cases b; exact dec_trivial
 by cases a; cases b; exact dec_trivial
 
 @[simp] theorem ite_eq_tt_distrib (c : Prop) [decidable c] (a b : bool) : ((if c then a else b) = tt) = (if c then a = tt else b = tt) :=
-by by_cases c with h; simp [h]
+by by_cases c; simp [*]
 
 @[simp] theorem ite_eq_ff_distrib (c : Prop) [decidable c] (a b : bool) : ((if c then a else b) = ff) = (if c then a = ff else b = ff) :=
-by by_cases c with h; simp [h]
+by by_cases c; simp [*]

library/init/data/list/lemmas.lean

@@ -192,7 +192,7 @@ theorem length_remove_nth : ∀ (l : list α) (i : ℕ), i < length l → length
 
 @[simp] lemma partition_eq_filter_filter (p : α → Prop) [decidable_pred p] : ∀ (l : list α), partition p l = (filter p l, filter (not ∘ p) l)
 | []     := rfl
-| (a::l) := by { by_cases p a with pa; simp [partition, filter, pa, partition_eq_filter_filter l],
+| (a::l) := by { by_cases pa : p a; simp [partition, filter, pa, partition_eq_filter_filter l],
                  rw [if_neg (not_not_intro pa)], rw [if_pos pa] }
 
 /- sublists -/
@@ -223,7 +223,7 @@ lemma length_le_of_sublist : ∀ {l₁ l₂ : list α}, l₁ <+ l₂ → length
 @[simp] theorem filter_append {p : α → Prop} [h : decidable_pred p] :
   ∀ (l₁ l₂ : list α), filter p (l₁++l₂) = filter p l₁ ++ filter p l₂
 | []      l₂ := rfl
-| (a::l₁) l₂ := by by_cases p a with pa; simp [pa, filter_append]
+| (a::l₁) l₂ := by by_cases pa : p a; simp [pa, filter_append]
 
 @[simp] theorem filter_sublist {p : α → Prop} [h : decidable_pred p] : Π (l : list α), filter p l <+ l
 | []     := sublist.slnil

library/init/data/nat/bitwise.lean

@@ -210,21 +210,23 @@ lemma binary_rec_eq {C : nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit
   binary_rec z f (bit b n) = f b n (binary_rec z f n) :=
 begin
   rw [binary_rec],
-  by_cases (bit b n = 0) with h',
-  {simp [dif_pos h'],
-   generalize : binary_rec._main._pack._proof_1 (bit b n) h' = e,
-   revert e,
-   have bf := bodd_bit b n,
-   have n0 := div2_bit b n,
-   rw h' at bf n0,
-   simp at bf n0,
-   rw [← bf, ← n0, binary_rec_zero],
-   intros, exact h.symm },
-  {simp [dif_neg h'],
-   generalize : binary_rec._main._pack._proof_2 (bit b n) = e,
-   revert e,
-   rw [bodd_bit, div2_bit],
-   intros, refl}
+  with_cases { by_cases bit b n = 0 },
+  case pos : h' {
+    simp [dif_pos h'],
+    generalize : binary_rec._main._pack._proof_1 (bit b n) h' = e,
+    revert e,
+    have bf := bodd_bit b n,
+    have n0 := div2_bit b n,
+    rw h' at bf n0,
+    simp at bf n0,
+    rw [← bf, ← n0, binary_rec_zero],
+    intros, exact h.symm },
+  case neg : h' {
+    simp [dif_neg h'],
+    generalize : binary_rec._main._pack._proof_2 (bit b n) = e,
+    revert e,
+    rw [bodd_bit, div2_bit],
+    intros, refl}
 end
 
 lemma bitwise_bit_aux {f : bool → bool → bool} (h : f ff ff = ff) :

library/init/data/ordering/lemmas.lean

@@ -30,13 +30,13 @@ by contradiction
 by contradiction
 
 @[simp] theorem ite_eq_lt_distrib (c : Prop) [decidable c] (a b : ordering) : ((if c then a else b) = ordering.lt) = (if c then a = ordering.lt else b = ordering.lt) :=
-by by_cases c with h; simp [h]
+by by_cases c; simp [*]
 
 @[simp] theorem ite_eq_eq_distrib (c : Prop) [decidable c] (a b : ordering) : ((if c then a else b) = ordering.eq) = (if c then a = ordering.eq else b = ordering.eq) :=
-by by_cases c with h; simp [h]
+by by_cases c; simp [*]
 
 @[simp] theorem ite_eq_gt_distrib (c : Prop) [decidable c] (a b : ordering) : ((if c then a else b) = ordering.gt) = (if c then a = ordering.gt else b = ordering.gt) :=
-by by_cases c with h; simp [h]
+by by_cases c; simp [*]
 
 /- ------------------------------------------------------------------ -/
 end ordering

library/init/meta/interactive.lean

@@ -1439,13 +1439,16 @@ meta def match_target (t : parse texpr) (m := reducible) : tactic unit :=
 tactic.match_target t m >> skip
 
 /--
-`by_cases p with h` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
+`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
 
 This tactic requires that `p` is decidable. To ensure that all propositions are decidable via classical reasoning, use  `local attribute classical.prop_decidable [instance]`.
 -/
-meta def by_cases (q : parse texpr) (n : parse (tk "with" *> ident)?): tactic unit :=
-do p ← tactic.to_expr_strict q,
-   tactic.by_cases p (n.get_or_else `h)
+meta def by_cases : parse cases_arg_p → tactic unit
+| (n, q) := concat_tags $ do
+  p ← tactic.to_expr_strict q,
+  tactic.by_cases p (n.get_or_else `h),
+  pos_g :: neg_g :: rest ← get_goals,
+  return [(`pos, pos_g), (`neg, neg_g)]
 
 /--
 Apply function extensionality and introduce new hypotheses.
@@ -1471,7 +1474,7 @@ tactic.by_contradiction n >> return ()
 An abbreviation for `by_contradiction`.
 -/
 meta def by_contra (n : parse ident?) : tactic unit :=
-tactic.by_contradiction n >> return ()
+by_contradiction n
 
 /--
 Type check the given expression, and trace its type.