From 533ddc02796ce092ebfc203cb1442be8208d6dad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Dec 2017 16:16:57 -0800
Subject: [PATCH] fix(library/init/meta/interactive): remove buggy
 `generalizing` param from `with_cases`

---
 doc/changes.md                     |  2 -
 library/data/rbtree/insert.lean    | 66 +++++++++++++++---------------
 library/init/meta/interactive.lean | 20 ++++-----
 tests/lean/run/with_cases1.lean    | 41 +++++++++++++++++++
 4 files changed, 83 insertions(+), 46 deletions(-)
 create mode 100644 tests/lean/run/with_cases1.lean

diff --git a/doc/changes.md b/doc/changes.md
index 8cd3dffcd6..03d640e2ca 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -48,8 +48,6 @@ master branch (aka work in progress branch)
   and reverts any new hypothesis in the resulting subgoals. `with_cases` also enable "goal tagging".
   Remark: `induction` and `cases` tag goals using constructor names. `apply` and `constructor` tag goals
   using parameter names. The `case` tactic can select goals using tags.
-  `with_cases generalizing id_1 ... id_n { t }` reverts hypotheses `id_1` ... `id_n` before executing `t`.
-  The hypotheses are automatically re-introduced by `case`. The user can optionally rename them at each `case`.
 
 * 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]`.
diff --git a/library/data/rbtree/insert.lean b/library/data/rbtree/insert.lean
index 5ca453d0d5..0ed72a5aa9 100644
--- a/library/data/rbtree/insert.lean
+++ b/library/data/rbtree/insert.lean
@@ -408,12 +408,12 @@ variable [is_strict_weak_order α lt]
 
 lemma find_balance1_lt {l r t v x y lo hi}
                        (h : lt x y)
-                       : ∀ (hl : is_searchable lt l lo (some v))
-                           (hr : is_searchable lt r (some v) (some y))
-                           (ht : is_searchable lt t (some y) hi),
-                           find lt (balance1 l v r y t) x = find lt (red_node l v r) x :=
+                       (hl : is_searchable lt l lo (some v))
+                       (hr : is_searchable lt r (some v) (some y))
+                       (ht : is_searchable lt t (some y) hi)
+                       : find lt (balance1 l v r y t) x = find lt (red_node l v r) x :=
 begin
-  with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
+  with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
   case red_left : _ _ _ z r { apply weak_trichotomous lt z x; intros; simp [*] },
   case red_right : l_left l_val l_right z r {
     with_cases { apply weak_trichotomous lt z x; intro h' },
@@ -437,12 +437,12 @@ end
 
 lemma find_balance1_gt {l r t v x y lo hi}
                        (h : lt y x)
-                       : ∀ (hl : is_searchable lt l lo (some v))
-                           (hr : is_searchable lt r (some v) (some y))
-                           (ht : is_searchable lt t (some y) hi),
-                           find lt (balance1 l v r y t) x = find lt t x :=
+                       (hl : is_searchable lt l lo (some v))
+                       (hr : is_searchable lt r (some v) (some y))
+                       (ht : is_searchable lt t (some y) hi)
+                       : find lt (balance1 l v r y t) x = find lt t x :=
 begin
-  with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
+  with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
   case red_left : _ _ _ z {
     have := trans_of lt (lo_lt_hi hr) h, simp [*] },
   case red_right : _ _ _ z {
@@ -460,13 +460,13 @@ begin
 end
 
 lemma find_balance1_eqv {l r t v x y lo hi}
-                        (h : ¬ lt x y ∧ ¬ lt y x) :
-                        ∀ (hl : is_searchable lt l lo (some v))
-                          (hr : is_searchable lt r (some v) (some y))
-                          (ht : is_searchable lt t (some y) hi),
-                          find lt (balance1 l v r y t) x = some y :=
+                        (h : ¬ lt x y ∧ ¬ lt y x)
+                        (hl : is_searchable lt l lo (some v))
+                        (hr : is_searchable lt r (some v) (some y))
+                        (ht : is_searchable lt t (some y) hi)
+                        : find lt (balance1 l v r y t) x = some y :=
 begin
-  with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
+  with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
   case red_left : _ _ _ z {
     have : lt z x := lt_of_lt_of_incomp (lo_lt_hi hr) h.swap,
     simp [*] },
@@ -489,12 +489,12 @@ end
 
 lemma find_balance2_lt {l v r t x y lo hi}
                        (h :  lt x y)
-                       : ∀ (hl : is_searchable lt l (some y) (some v))
-                           (hr : is_searchable lt r (some v) hi)
-                           (ht : is_searchable lt t lo (some y)),
-                           find lt (balance2 l v r y t) x = find lt t x :=
+                       (hl : is_searchable lt l (some y) (some v))
+                       (hr : is_searchable lt r (some v) hi)
+                       (ht : is_searchable lt t lo (some y))
+                       : find lt (balance2 l v r y t) x = find lt t x :=
 begin
-  with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
+  with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
   case red_left { have := trans h (lo_lt_hi hl_hs₁), simp [*] },
   case red_right { have := trans h (lo_lt_hi hl), simp [*] }
 end
@@ -511,13 +511,13 @@ begin
 end
 
 lemma find_balance2_gt {l v r t x y lo hi}
-                       (h :  lt y x) :
-                       ∀ (hl : is_searchable lt l (some y) (some v))
-                         (hr : is_searchable lt r (some v) hi)
-                         (ht : is_searchable lt t lo (some y)),
-                         find lt (balance2 l v r y t) x = find lt (red_node l v r) x :=
+                       (h :  lt y x)
+                       (hl : is_searchable lt l (some y) (some v))
+                       (hr : is_searchable lt r (some v) hi)
+                       (ht : is_searchable lt t lo (some y))
+                       : find lt (balance2 l v r y t) x = find lt (red_node l v r) x :=
 begin
-  with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
+  with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
   case red_left : _ val _ z {
     with_cases { apply weak_trichotomous lt val x; intro h'; simp [*] },
     case is_lt { apply weak_trichotomous lt z x; intros; simp [*] },
@@ -540,13 +540,13 @@ begin
 end
 
 lemma find_balance2_eqv {l v r t x y lo hi}
-                        (h : ¬ lt x y ∧ ¬ lt y x) :
-                        ∀ (hl : is_searchable lt l (some y) (some v))
-                          (hr : is_searchable lt r (some v) hi)
-                          (ht : is_searchable lt t lo (some y)),
-                          find lt (balance2 l v r y t) x = some y :=
+                        (h : ¬ lt x y ∧ ¬ lt y x)
+                        (hl : is_searchable lt l (some y) (some v))
+                        (hr : is_searchable lt r (some v) hi)
+                        (ht : is_searchable lt t lo (some y))
+                        : find lt (balance2 l v r y t) x = some y :=
 begin
-  with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
+  with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
   case red_left { have := lt_of_incomp_of_lt h (lo_lt_hi hl_hs₁), simp [*] },
   case red_right { have := lt_of_incomp_of_lt h (lo_lt_hi hl), simp [*] }
 end
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 4e09f60cad..4ec4c0fb2b 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -401,16 +401,16 @@ private meta def collect_hyps_uids : tactic name_set :=
 do ctx ← local_context,
    return $ ctx.foldl (λ r h, r.insert h.local_uniq_name) mk_name_set
 
-private meta def revert_new_hyps (num_reverted : nat) (input_hyp_uids : name_set) : tactic unit :=
+private meta def revert_new_hyps (input_hyp_uids : name_set) : tactic unit :=
 do ctx ← local_context,
    let to_revert := ctx.foldr (λ h r, if input_hyp_uids.contains h.local_uniq_name then r else h::r) [],
    tag ← get_main_tag,
    m   ← revert_lst to_revert,
-   set_main_tag (mk_num_name `_case (m + num_reverted) :: tag)
+   set_main_tag (mk_num_name `_case m :: tag)
 
 /--
 Apply `t` to main goal, and revert any new hypothesis in the generated goals,
-and tag generated goals when using supported tactics such as: `induction`, `apply`, ...
+and tag generated goals when using supported tactics such as: `induction`, `apply`, `cases`, `constructor`, ...
 
 This tactic is useful for writing robust proof scripts that are not sensitive
 to the name generation strategy used by `t`.
@@ -426,13 +426,11 @@ end
 
 TODO(Leo): improve docstring
 -/
-meta def with_cases (revert : parse $ (tk "generalizing" *> ident*)?) (t : itactic) : tactic unit :=
-do -- revert `generalizing` params
-   n ← mmap tactic.get_local (revert.get_or_else []) >>= revert_lst,
-   with_enable_tags $ focus1 $ do
-     input_hyp_uids ← collect_hyps_uids,
-     t,
-     all_goals (revert_new_hyps n input_hyp_uids)
+meta def with_cases (t : itactic) : tactic unit :=
+with_enable_tags $ focus1 $ do
+  input_hyp_uids ← collect_hyps_uids,
+  t,
+  all_goals (revert_new_hyps input_hyp_uids)
 
 private meta def get_type_name (e : expr) : tactic name :=
 do e_type ← infer_type e >>= whnf,
@@ -679,10 +677,10 @@ do g   ← find_tagged_goal pre,
    let ids := ids.get_or_else [],
    match is_case_tag tag with
    | some n := do
+      let m := ids.length,
       gs ← get_goals,
       set_goals $ g :: gs.filter (≠ g),
       intro_lst ids,
-      let m := ids.length,
       when (m < n) $ intron (n - m),
       solve1 tac
    | none   :=
diff --git a/tests/lean/run/with_cases1.lean b/tests/lean/run/with_cases1.lean
new file mode 100644
index 0000000000..88da611668
--- /dev/null
+++ b/tests/lean/run/with_cases1.lean
@@ -0,0 +1,41 @@
+example (n : nat) (m : nat) : n > m → m < n :=
+begin
+  with_cases { revert m, induction n },
+  case nat.zero : m' { show 0 > m' → m' < 0, admit },
+  case nat.succ : n' ih m' { show nat.succ n' > m' → m' < nat.succ n', admit }
+end
+
+example (n : nat) (m : nat) : n > m → m < n :=
+begin
+  with_cases { revert m, induction n },
+  case nat.zero { show ∀ m, 0 > m → m < 0, admit },
+  case nat.succ { show ∀ m, nat.succ n_n > m → m < nat.succ n_n, admit }
+end
+
+example (n : nat) (m : nat) : n > m → m < n :=
+begin
+  with_cases { induction n generalizing m },
+  case nat.zero { show 0 > m → m < 0, admit },
+  case nat.succ { show nat.succ n_n > m → m < nat.succ n_n, admit }
+end
+
+example (n : nat) (m : nat) : n > m → m < n :=
+begin
+  with_cases { induction n generalizing m },
+  case nat.zero : m' { show 0 > m' → m' < 0, admit },
+  case nat.succ : n' ih m' { show nat.succ n' > m' → m' < nat.succ n', admit }
+end
+
+example (n : nat) (m : nat) : n > m → m < n :=
+begin
+  with_cases { induction n generalizing m },
+  case nat.zero : m' { show 0 > m' → m' < 0, admit },
+  case nat.succ : n' ih { show nat.succ n' > m → m < nat.succ n', admit }
+end
+
+example (n : nat) (m : nat) : n > m → m < n :=
+begin
+  with_cases { induction n generalizing m },
+  case nat.zero { show 0 > m → m < 0, admit },
+  case nat.succ : n' ih { show nat.succ n' > m → m < nat.succ n', admit }
+end