feat(tactic/rcases): clear pattern - in rcases (#3868)

This allows you to write:
```lean
example (h : ∃ x : ℕ, true) : true :=
begin
  rcases h with ⟨x, -⟩,
  -- x : ℕ |- true
end
```
to clear unwanted hypotheses. Note that dependents are also cleared,
meaning that you can get into trouble if you try to keep matching when a
variable later in the pattern is deleted. The `_` pattern will match
a hypothesis even if it has been deleted, so this is the recommended way
to match on variables dependent on a deleted hypothesis.
You can use `-` if you prefer, but watch out for unintended variables
getting deleted if there are duplicate names!

src/tactic/rcases.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import data.dlist
 import tactic.core
+import tactic.clear
 
 /-!
 
@@ -22,6 +23,7 @@ the input expression). An `rcases` pattern has the following grammar:
 * A name like `x`, which names the active hypothesis as `x`.
 * A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
   hypothesis).
+* A hyphen `-`, which clears the active hypothesis and any dependents.
 * The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
   hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
 * A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
@@ -84,14 +86,15 @@ annotations in reported types.
 local notation `listΣ` := list_Sigma
 local notation `listΠ` := list_Pi
 
-/-- A list of metavariables representing subgoals. -/
-@[reducible] meta def goals := list expr
+/-- A metavariable representing a subgoal, together with a list of local constants to clear. -/
+@[reducible] meta def uncleared_goal := list expr × expr
 
 /--
 An `rcases` pattern can be one of the following, in a nested combination:
 
 * A name like `foo`
 * The special keyword `rfl` (for pattern matching on equality using `subst`)
+* A hyphen `-`, which clears the active hypothesis and any dependents.
 * A type ascription like `pat : ty` (parentheses are optional)
 * A tuple constructor like `⟨p1, p2, p3⟩`
 * An alternation / variant pattern `p1 | p2 | p3`
@@ -108,6 +111,7 @@ type with 3 constructors,  `p1 | (p2 | p3)` will act like `p1 | (p2 | p3) | _` i
 -/
 meta inductive rcases_patt : Type
 | one : name → rcases_patt
+| clear : rcases_patt
 | typed : rcases_patt → pexpr → rcases_patt
 | tuple : listΠ rcases_patt → rcases_patt
 | alts : listΣ rcases_patt → rcases_patt
@@ -191,6 +195,7 @@ meta def alts₁ : listΣ (listΠ rcases_patt) → rcases_patt
 
 meta instance has_reflect : has_reflect rcases_patt
 | (one n) := `(_)
+| clear := `(_)
 | (typed l e) :=
   (`(typed).subst (has_reflect l)).subst (reflect e)
 | (tuple l) := `(λ l, tuple l).subst $
@@ -203,6 +208,7 @@ printed at high precedence, i.e. it will have parentheses around it if it is not
 or atomic name. -/
 protected meta def format : ∀ bracket : bool, rcases_patt → tactic _root_.format
 | _ (one n) := pure $ to_fmt n
+| _ clear := pure "-"
 | _ (tuple []) := pure "⟨⟩"
 | _ (tuple ls) := do
   fs ← ls.mmap $ format ff,
@@ -290,14 +296,17 @@ private meta def get_local_and_type (e : expr) : tactic (expr × expr) :=
   `⟨a | b, ⟨c, d⟩⟩` performs the `⟨c, d⟩` match twice, once on the `a` branch and once on `b`.
 -/
 meta mutual def rcases_core, rcases.continue
-with rcases_core : rcases_patt → expr → tactic goals
+with rcases_core : rcases_patt → expr → tactic (list uncleared_goal)
 | (rcases_patt.one `rfl) e := do
   (t, e) ← get_local_and_type e,
   subst e,
-  get_goals
+  list.map (prod.mk []) <$> get_goals
 -- If the pattern is any other name, we already bound the name in the
 -- top-level `cases` tactic, so there is no more work to do for it.
-| (rcases_patt.one _) _ := get_goals
+| (rcases_patt.one _) _ := list.map (prod.mk []) <$> get_goals
+| rcases_patt.clear e := do
+  m ← try_core (get_local_and_type e),
+  list.map (prod.mk $ m.elim [] (λ ⟨_, e⟩, [e])) <$> get_goals
 | (rcases_patt.typed p ty) e := do
   (t, e) ← get_local_and_type e,
   ty ← i_to_expr_no_subgoals ``(%%ty : Sort*),
@@ -335,15 +344,29 @@ with rcases_core : rcases_patt → expr → tactic goals
   -- as some constructors may be impossible for type reasons. (See its
   -- documentation.) Match up the new goals with our remaining work
   -- by constructor name.
-  list.join <$> (align (λ (a : name × _) (b : _ × name × _), a.1 = b.2.1) r (gs.zip l)).mmap
-    (λ⟨⟨_, ps⟩, g, _, hs, _⟩,
-      set_goals [g] >> rcases.continue (ps.zip hs))
+  let ls := align (λ (a : name × _) (b : _ × name × _), a.1 = b.2.1) r (gs.zip l),
+  list.join <$> ls.mmap (λ⟨⟨_, ps⟩, g, _, hs, _⟩, set_goals [g] >> rcases.continue (ps.zip hs))
 
-with rcases.continue : listΠ (rcases_patt × expr) → tactic goals
-| [] := get_goals
+with rcases.continue : listΠ (rcases_patt × expr) → tactic (list uncleared_goal)
+| [] := list.map (prod.mk []) <$> get_goals
 | ((pat, e) :: pes) := do
   gs ← rcases_core pat e,
-  list.join <$> gs.mmap (λ g, set_goals [g] >> rcases.continue pes)
+  list.join <$> gs.mmap (λ ⟨cs, g⟩, do
+    set_goals [g],
+    ugs ← rcases.continue pes,
+    pure $ ugs.map $ λ ⟨cs', gs⟩, (cs ++ cs', gs))
+
+/-- Given a list of `uncleared_goal`s, each of which is a goal metavariable and
+a list of variables to clear, actually perform the clear and set the goals with the result. -/
+meta def clear_goals (ugs : list uncleared_goal) : tactic unit := do
+  gs ← ugs.mmap (λ ⟨cs, g⟩, do
+    set_goals [g],
+    cs ← cs.mfoldr (λ c cs,
+      (do (_, c) ← get_local_and_type c, pure (c :: cs)) <|> pure cs) [],
+    clear' tt cs,
+    [g] ← get_goals,
+    pure g),
+  set_goals gs
 
 /-- `rcases h e pat` performs case distinction on `e` using `pat` to
 name the arising new variables and assumptions. If `h` is `some` name,
@@ -362,7 +385,7 @@ meta def rcases (h : option name) (p : pexpr) (pat : rcases_patt) : tactic unit
     | none := i_to_expr p
     end,
   if e.is_local_constant then
-    focus1 (rcases_core pat e >>= set_goals)
+    focus1 (rcases_core pat e >>= clear_goals)
   else do
     x ← pat.name.elim mk_fresh_name pure,
     n ← revert_kdependencies e semireducible,
@@ -372,15 +395,15 @@ meta def rcases (h : option name) (p : pexpr) (pat : rcases_patt) : tactic unit
       get_local x >>= tactic.revert,
       pure ()),
     h ← tactic.intro1,
-    focus1 (rcases_core pat h >>= set_goals)
+    focus1 (rcases_core pat h >>= clear_goals)
 
 /-- `rintro pat₁ pat₂ ... patₙ` introduces `n` arguments, then pattern matches on the `patᵢ` using
 the same syntax as `rcases`. -/
 meta def rintro (ids : listΠ rcases_patt) : tactic unit :=
 do l ← ids.mmap (λ id, do
     e ← intro $ id.name.get_or_else `_,
     pure (id, e)),
-  focus1 (rcases.continue l >>= set_goals)
+  focus1 (rcases.continue l >>= clear_goals)
 
 /-- Like `zip_with`, but if the lists don't match in length, the excess elements will be put at the
 end of the result. -/
@@ -404,6 +427,8 @@ meta def rcases_patt.merge : rcases_patt → rcases_patt → rcases_patt
 | (rcases_patt.one `rfl) (rcases_patt.one `rfl) := rcases_patt.one `rfl
 | (rcases_patt.one `_) p := p
 | p (rcases_patt.one `_) := p
+| rcases_patt.clear p := p
+| p rcases_patt.clear := p
 | (rcases_patt.one n) _ := rcases_patt.one n
 
 /--
@@ -422,7 +447,7 @@ meta def rcases_patt.merge : rcases_patt → rcases_patt → rcases_patt
   `depth` and recording the successful cases. It returns `ps`, and the list of generated subgoals.
 -/
 meta mutual def rcases_hint_core, rcases_hint.process_constructors, rcases_hint.continue
-with rcases_hint_core : ℕ → expr → tactic (rcases_patt × goals)
+with rcases_hint_core : ℕ → expr → tactic (rcases_patt × list expr)
 | depth e := do
   (t, e) ← get_local_and_type e,
   t ← whnf t,
@@ -441,7 +466,7 @@ with rcases_hint_core : ℕ → expr → tactic (rcases_patt × goals)
 
 with rcases_hint.process_constructors : ℕ → listΣ name →
   list (expr × name × listΠ expr × list (name × expr)) →
-  tactic (listΣ (listΠ rcases_patt) × goals)
+  tactic (listΣ (listΠ rcases_patt) × list expr)
 | depth [] _  := pure ([], [])
 | depth cs [] := pure (cs.map (λ _, []), [])
 | depth (c::cs) ((g, c', hs, _) :: l) :=
@@ -453,11 +478,11 @@ with rcases_hint.process_constructors : ℕ → listΣ name →
     (ps, gs') ← rcases_hint.process_constructors depth cs l,
     pure (p :: ps, gs ++ gs')
 
-with rcases_hint.continue : ℕ → listΠ expr → tactic (listΠ rcases_patt × goals)
+with rcases_hint.continue : ℕ → listΠ expr → tactic (listΠ rcases_patt × list expr)
 | depth [] := prod.mk [] <$> get_goals
 | depth (e :: es) := do
   (p, gs) ← rcases_hint_core depth e,
-  (ps, gs') ← gs.mfoldl (λ (r : listΠ rcases_patt × goals) g,
+  (ps, gs') ← gs.mfoldl (λ (r : listΠ rcases_patt × list expr) g,
     do (ps, gs') ← set_goals [g] >> rcases_hint.continue depth es,
       pure (merge_list rcases_patt.merge r.1 ps, r.2 ++ gs')) ([], []),
   pure (p :: ps, gs')
@@ -507,28 +532,34 @@ setup_tactic_parser
 * `rcases_patt_parse_list` will parse an alternation list, `patt_med`, one or more `patt`
   patterns separated by `|`. It does not parse a `:` at the end, so that `a | b : ty` parses as
   `(a | b) : ty` where `a | b` is the `patt_med` part.
+* `rcases_patt_parse_list_rest a` parses an alternation list after the initial pattern, `| b | c`.
 
 ```lean
 patt ::= patt_med (":" expr)?
 patt_med ::= (patt_hi "|")* patt_hi
 patt_hi ::= id | "rfl" | "_" | "⟨" (patt ",")* patt "⟩" | "(" patt ")"
 ```
 -/
-meta mutual def rcases_patt_parse, rcases_patt_parse_list
+meta mutual def rcases_patt_parse, rcases_patt_parse_list, rcases_patt_parse_list_rest
 with rcases_patt_parse : bool → parser rcases_patt
 | tt := with_desc "patt_hi" $
   (brackets "(" ")" (rcases_patt_parse ff)) <|>
   (rcases_patt.tuple <$> brackets "⟨" "⟩" (sep_by (tk ",") (rcases_patt_parse ff))) <|>
+  (tk "-" $> rcases_patt.clear) <|>
   (rcases_patt.one <$> ident_)
 | ff := with_desc "patt" $ do
   pat ← rcases_patt.alts' <$> rcases_patt_parse_list,
   (tk ":" *> pat.typed <$> texpr) <|> pure pat
 
 with rcases_patt_parse_list : parser (listΣ rcases_patt)
-| x := (with_desc "patt_med" $ do
-  pat ← rcases_patt_parse tt,
+| x := (with_desc "patt_med" $ rcases_patt_parse tt >>= rcases_patt_parse_list_rest) x
+
+with rcases_patt_parse_list_rest : rcases_patt → parser (listΣ rcases_patt)
+| pat :=
   (tk "|" *> list.cons pat <$> rcases_patt_parse_list) <|>
-  pure [pat]) x
+  -- hack to support `-|-` patterns, because `|-` is a token
+  (tk "|-" *> list.cons pat <$> rcases_patt_parse_list_rest rcases_patt.clear) <|>
+  pure [pat]
 
 /-- Parse the optional depth argument `(: n)?` of `rcases?` and `rintro?`, with default depth 5. -/
 meta def rcases_parse_depth : parser nat :=
@@ -575,6 +606,7 @@ the input expression). An `rcases` pattern has the following grammar:
 * A name like `x`, which names the active hypothesis as `x`.
 * A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
   hypothesis).
+* A hyphen `-`, which clears the active hypothesis and any dependents.
 * The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
   hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
 * A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it

test/rcases.lean

@@ -20,9 +20,9 @@ end
 
 example (x : α × β × γ) : true :=
 begin
-  rcases x with ⟨a, ⟨b, c⟩⟩,
+  rcases x with ⟨a, ⟨-, c⟩⟩,
   { guard_hyp a := α,
-    guard_hyp b := β,
+    success_if_fail { guard_hyp x_snd_fst := β },
     guard_hyp c := γ,
     trivial }
 end
@@ -62,11 +62,11 @@ end
 
 example : true :=
 begin
-  obtain ⟨n : ℕ, h : n = n, f : true⟩ : ∃ n : ℕ, n = n ∧ true,
+  obtain ⟨n : ℕ, h : n = n, -⟩ : ∃ n : ℕ, n = n ∧ true,
   { existsi 0, simp },
   guard_hyp n := ℕ,
   guard_hyp h := n = n,
-  guard_hyp f := true,
+  success_if_fail {assumption},
   trivial
 end
 
@@ -133,3 +133,26 @@ begin
   obtain one_lt_n | (n_le_one : n + 1 ≤ 1) := nat.lt_or_ge 1 (n + 1),
   trivial, trivial,
 end
+
+example (h : ∃ x : ℕ, x = x ∧ 1 = 1) : true :=
+begin
+  rcases h with ⟨-, _⟩,
+  (do lc ← tactic.local_context, guard lc.empty),
+  trivial
+end
+
+example (h : ∃ x : ℕ, x = x ∧ 1 = 1) : true :=
+begin
+  rcases h with ⟨-, _, h⟩,
+  (do lc ← tactic.local_context, guard (lc.length = 1)),
+  guard_hyp h := 1 = 1,
+  trivial
+end
+
+example (h : true ∨ true ∨ true) : true :=
+begin
+  rcases h with -|-|-,
+  iterate 3 {
+    (do lc ← tactic.local_context, guard lc.empty),
+    trivial },
+end