feat(tactic/rcases): rcases_hint, rintro_hint

docs/tactics.md

@@ -34,6 +34,20 @@ a description of supported patterns. For example, `rintros (a | ⟨b, c⟩) ⟨d
 will introduce two variables, and then do case splits on both of them producing
 two subgoals, one with variables `a d e` and the other with `b c d e`.
 
+### rcases_hint
+
+`rcases_hint e` will perform case splits on `e` in the same way as `rcases e`,
+but rather than accepting a pattern, it does a maximal cases and prints the
+pattern that would produce this case splitting. The default maximum depth is 5,
+but this can be modified with `rcases_hint e {depth := n}`.
+
+### rintro_hint
+
+`rintro_hint` will introduce and case split on variables in the same way as
+`rintro`, but will also print the `rintro` invocation that would have the same
+result. Like `rcases_hint`, `rintro_hint {depth := n}` allows for modifying the
+depth of splitting; the default is 5.
+
 ### simpa
 
 This is a "finishing" tactic modification of `simp`. The tactic `simpa

tactic/basic.lean

@@ -51,6 +51,12 @@ expr.local_const n n binder_info.default (expr.const n [])
 
 meta def exact_dec_trivial : tactic unit := `[exact dec_trivial]
 
+/-- Runs a tactic for a result, reverting the state after completion -/
+meta def retrieve {α} (tac : tactic α) : tactic α :=
+λ s, result.cases_on (tac s)
+ (λ a s', result.success a s)
+ result.exception
+
 meta def replace_at (tac : expr → tactic (expr × expr)) (hs : list expr) (tgt : bool) : tactic bool :=
 do to_remove ← hs.mfilter $ λ h, do {
          h_type ← infer_type h,

tactic/interactive.lean

@@ -21,18 +21,10 @@ open interactive interactive.types expr
 local notation `listΣ` := list_Sigma
 local notation `listΠ` := list_Pi
 
-/--
-This parser uses the "inverted" meaning for the `many` constructor:
-rather than representing a sum of products, here it represents a
-product of sums. We fix this by applying `invert`, defined below, to
-the result.
--/
-@[reducible] def rcases_patt_inverted := rcases_patt
-
 meta def rcases_parse1 (rcases_parse : parser (listΣ rcases_patt_inverted)) :
   parser rcases_patt_inverted | x :=
-((rcases_patt.one <$> ident_) <|>
-(rcases_patt.many <$> brackets "⟨" "⟩" (sep_by (tk ",") rcases_parse))) x
+((rcases_patt_inverted.one <$> ident_) <|>
+(rcases_patt_inverted.many <$> brackets "⟨" "⟩" (sep_by (tk ",") rcases_parse))) x
 
 meta def rcases_parse : parser (listΣ rcases_patt_inverted) :=
 with_desc "patt" $
@@ -41,16 +33,6 @@ list.cons <$> rcases_parse1 rcases_parse <*> (tk "|" *> rcases_parse1 rcases_par
 meta def rcases_parse_single : parser rcases_patt_inverted :=
 with_desc "patt_list" $ rcases_parse1 rcases_parse
 
-meta mutual def rcases_parse.invert, rcases_parse.invert'
-with rcases_parse.invert : listΣ rcases_patt_inverted → listΣ (listΠ rcases_patt)
-| l := l.map $ λ p, match p with
-| rcases_patt.one n := [rcases_patt.one n]
-| rcases_patt.many l := rcases_parse.invert' <$> l
-end
-with rcases_parse.invert' : listΣ rcases_patt_inverted → rcases_patt
-| [rcases_patt.one n] := rcases_patt.one n
-| l := rcases_patt.many (rcases_parse.invert l)
-
 /--
 The `rcases` tactic is the same as `cases`, but with more flexibility in the
 `with` pattern syntax to allow for recursive case splitting. The pattern syntax
@@ -72,10 +54,10 @@ If there are too many arguments, such as `⟨a, b, c⟩` for splitting on
 parameter as necessary.
 -/
 meta def rcases (p : parse texpr) (ids : parse (tk "with" *> rcases_parse)?) : tactic unit :=
-tactic.rcases p $ rcases_parse.invert $ ids.get_or_else [default _]
+tactic.rcases p $ rcases_patt_inverted.invert_list $ ids.get_or_else [default _]
 
 meta def rintro_parse : parser rcases_patt :=
-rcases_parse.invert' <$> (brackets "(" ")" rcases_parse <|>
+rcases_patt_inverted.invert <$> (brackets "(" ")" rcases_parse <|>
   (λ x, [x]) <$> rcases_parse_single)
 
 /--
@@ -92,6 +74,30 @@ meta def rintro : parse rintro_parse* → tactic unit
 /-- Alias for `rintro`. -/
 meta def rintros := rintro
 
+structure rcases_config := (depth := 5)
+
+/--
+`rcases_hint e` will perform case splits on `e` in the same way as `rcases e`,
+but rather than accepting a pattern, it does a maximal cases and prints the
+pattern that would produce this case splitting. The default maximum depth is 5,
+but this can be modified with `rcases_hint e {depth := n}`.
+-/
+meta def rcases_hint (p : parse texpr) (d : rcases_config := {}) : tactic unit :=
+do patt ← tactic.rcases_hint p d.depth,
+  pe ← pp p,
+  trace $ ↑"snippet: rcases " ++ pe ++ " with " ++ to_fmt patt
+
+/--
+`rintro_hint` will introduce and case split on variables in the same way as
+`rintro`, but will also print the `rintro` invocation that would have the same
+result. Like `rcases_hint`, `rintro_hint {depth := n}` allows for modifying the
+depth of splitting; the default is 5.
+-/
+meta def rintro_hint (d : rcases_config := {}) : tactic unit :=
+do ps ← tactic.rintro_hint d.depth,
+  trace $ ↑"snippet: rintro" ++ format.join (ps.map $ λ p,
+    format.space ++ format.group (p.format tt))
+
 /--
 This is a "finishing" tactic modification of `simp`. The tactic `simpa [rules, ...] using e`
 will simplify the hypothesis `e` using `rules`, then simplify the goal using `rules`, and

tactic/rcases.lean

@@ -32,14 +32,14 @@ local notation `listΠ` := list_Pi
 
 @[reducible] meta def goals := list expr
 
-inductive rcases_patt : Type
+meta inductive rcases_patt : Type
 | one : name → rcases_patt
 | many : listΣ (listΠ rcases_patt) → rcases_patt
 
-instance rcases_patt.inhabited : inhabited rcases_patt :=
+meta instance rcases_patt.inhabited : inhabited rcases_patt :=
 ⟨rcases_patt.one `_⟩
 
-def rcases_patt.name : rcases_patt → name
+meta def rcases_patt.name : rcases_patt → name
 | (rcases_patt.one n) := n
 | _ := `_
 
@@ -48,6 +48,80 @@ meta instance rcases_patt.has_reflect : has_reflect rcases_patt
 | (rcases_patt.many l) := `(λ l, rcases_patt.many l).subst $
   by haveI := rcases_patt.has_reflect; exact list.reflect l
 
+/--
+The parser/printer uses an "inverted" meaning for the `many` constructor:
+rather than representing a sum of products, here it represents a
+product of sums. We fix this by applying `invert`, defined below, to
+the result.
+-/
+meta inductive rcases_patt_inverted : Type
+| one : name → rcases_patt_inverted
+| many : listΠ (listΣ rcases_patt_inverted) → rcases_patt_inverted
+
+meta instance rcases_patt_inverted.inhabited : inhabited rcases_patt_inverted :=
+⟨rcases_patt_inverted.one `_⟩
+
+meta instance rcases_patt_inverted.has_reflect : has_reflect rcases_patt_inverted
+| (rcases_patt_inverted.one n) := `(_)
+| (rcases_patt_inverted.many l) := `(λ l, rcases_patt_inverted.many l).subst $
+  by haveI := rcases_patt_inverted.has_reflect; exact list.reflect l
+
+meta mutual def rcases_patt_inverted.invert, rcases_patt_inverted.invert_list
+with rcases_patt_inverted.invert : listΣ rcases_patt_inverted → rcases_patt
+| [rcases_patt_inverted.one n] := rcases_patt.one n
+| l := rcases_patt.many (rcases_patt_inverted.invert_list l)
+
+with rcases_patt_inverted.invert_list : listΣ rcases_patt_inverted → listΣ (listΠ rcases_patt)
+| l := l.map $ λ p,
+  match p with
+  | rcases_patt_inverted.one n := [rcases_patt.one n]
+  | rcases_patt_inverted.many l := rcases_patt_inverted.invert <$> l
+  end
+
+meta mutual def rcases_patt.invert, rcases_patt.invert_many, rcases_patt.invert_list, rcases_patt.invert'
+with rcases_patt.invert : rcases_patt → listΣ rcases_patt_inverted
+| (rcases_patt.one n) := [rcases_patt_inverted.one n]
+| (rcases_patt.many ls) := rcases_patt.invert_many ls
+
+with rcases_patt.invert_many : listΣ (listΠ rcases_patt) → listΣ rcases_patt_inverted
+| [] := []
+| [[rcases_patt.many ls@(_::_::_)]] := rcases_patt.invert_many ls
+| (l::ls) := rcases_patt.invert' l :: rcases_patt.invert_many ls
+
+with rcases_patt.invert_list : listΠ rcases_patt → listΠ (listΣ rcases_patt_inverted)
+| [] := []
+| [rcases_patt.many [l@(_::_::_)]] := rcases_patt.invert_list l
+| (p::l) := rcases_patt.invert p :: rcases_patt.invert_list l
+
+with rcases_patt.invert' : listΠ rcases_patt → rcases_patt_inverted
+| [rcases_patt.one n] := rcases_patt_inverted.one n
+| [] := rcases_patt_inverted.one `_
+| ls := rcases_patt_inverted.many (rcases_patt.invert_list ls)
+
+meta mutual def rcases_patt_inverted.format, rcases_patt_inverted.format_list
+with rcases_patt_inverted.format : rcases_patt_inverted → format
+| (rcases_patt_inverted.one n) := to_fmt n
+| (rcases_patt_inverted.many []) := "⟨⟩"
+| (rcases_patt_inverted.many ls) := "⟨" ++ format.group (format.nest 1 $
+    format.join $ list.intersperse ("," ++ format.line) $
+    ls.map (format.group ∘ rcases_patt_inverted.format_list)) ++ "⟩"
+
+with rcases_patt_inverted.format_list : listΣ rcases_patt_inverted → opt_param bool ff → format
+| [] br := "⟨⟩"
+| [p] br := rcases_patt_inverted.format p
+| (p::l) br :=
+  let fmt := rcases_patt_inverted.format p ++ " |" ++ format.space ++
+    rcases_patt_inverted.format_list l in
+  if br then format.bracket "(" ")" fmt else fmt
+
+meta instance rcases_patt_inverted.has_to_format :
+  has_to_format rcases_patt_inverted := ⟨rcases_patt_inverted.format⟩
+
+meta def rcases_patt.format (p : rcases_patt) (br := ff) : format :=
+rcases_patt_inverted.format_list p.invert br
+
+meta instance rcases_patt.has_to_format : has_to_format rcases_patt := ⟨rcases_patt.format⟩
+
 /--
 Takes the number of fields of a single constructor and patterns to
 match its fields against (not necessarily the same number). The
@@ -78,15 +152,14 @@ meta def rcases.process_constructors (params : nat) :
   tactic (dlist name × listΣ (name × listΠ rcases_patt))
 | []      ids := pure (dlist.empty, [])
 | (c::cs) ids := do
-  fn ← mk_const c,
-  n  ← get_arity fn,
-  let (h, t) := by from match cs, ids.tail with
+  n ← mk_const c >>= get_arity,
+  let (h, t) := (match cs, ids.tail with
   -- We matched the last constructor against multiple patterns,
   -- so split off the remaining constructors. This handles matching
   -- `α ⊕ β ⊕ γ` against `a|b|c`.
   | [], _::_ := ([rcases_patt.many ids], [])
   | _, _ := (ids.head, ids.tail)
-  end,
+  end : _),
   let (ns, ps) := rcases.process_constructor (n - params) h,
   (l, r) ← rcases.process_constructors cs t,
   pure (dlist.of_list ns ++ l, (c, ps) :: r)
@@ -137,7 +210,7 @@ with rcases.continue : listΠ (rcases_patt × expr) → tactic goals
 -- top-level `cases` tactic, so there is no more work to do for it.
 | (_ :: l) := rcases.continue l
 
-meta def rcases (p : pexpr) (ids : list (list rcases_patt)) : tactic unit :=
+meta def rcases (p : pexpr) (ids : listΣ (listΠ rcases_patt)) : tactic unit :=
 do e ← i_to_expr p,
   if e.is_local_constant then
     focus1 (rcases_core ids e >>= set_goals)
@@ -153,10 +226,91 @@ do e ← i_to_expr p,
     h ← tactic.intro1,
     focus1 (rcases_core ids h >>= set_goals)
 
-meta def rintro (ids : list rcases_patt) : tactic unit :=
+meta def rintro (ids : listΠ rcases_patt) : tactic unit :=
 do l ← ids.mmap (λ id, do
     e ← intro id.name,
     return (id, e)),
   focus1 (rcases.continue l >>= set_goals)
 
+def merge_list {α} (m : α → α → α) : list α → list α → list α
+| [] l₂ := l₂
+| l₁ [] := l₁
+| (a :: l₁) (b :: l₂) := m a b :: merge_list l₁ l₂
+
+meta def rcases_patt.merge : rcases_patt → rcases_patt → rcases_patt
+| (rcases_patt.many ids₁) (rcases_patt.many ids₂) :=
+  rcases_patt.many (merge_list (merge_list rcases_patt.merge) ids₁ ids₂)
+| (rcases_patt.one `rfl) (rcases_patt.many ids₂) :=
+  rcases_patt.many (merge_list (merge_list rcases_patt.merge) [[]] ids₂)
+| (rcases_patt.many ids₁) (rcases_patt.one `rfl) :=
+  rcases_patt.many (merge_list (merge_list rcases_patt.merge) ids₁ [[]])
+| (rcases_patt.one `rfl) (rcases_patt.one `rfl) := rcases_patt.one `rfl
+| (rcases_patt.one `_) p := p
+| p (rcases_patt.one `_) := p
+| (rcases_patt.one n) _ := rcases_patt.one n
+| _ (rcases_patt.one n) := rcases_patt.one n
+
+meta mutual def rcases_hint_core, rcases_hint.process_constructors, rcases_hint.continue
+with rcases_hint_core : ℕ → expr → tactic (rcases_patt × goals)
+| depth e := do
+  (t, e) ← get_local_and_type e,
+  t ← whnf t,
+  env ← get_env,
+  some l ← try_core (guard (depth ≠ 0) >> cases_core e) |
+    prod.mk (rcases_patt.one e.local_pp_name) <$> get_goals,
+  let I := t.get_app_fn.const_name,
+  if I = ``eq then
+    prod.mk (rcases_patt.one `rfl) <$> get_goals
+  else do
+    let c := env.constructors_of I,
+    gs ← get_goals,
+    (ps, gs') ← rcases_hint.process_constructors (depth - 1) c (gs.zip l),
+    pure (rcases_patt.many ps, gs')
+
+with rcases_hint.process_constructors : ℕ → listΣ name →
+  list (expr × name × listΠ expr × list (name × expr)) →
+  tactic (listΣ (listΠ rcases_patt) × goals)
+| depth [] _  := pure ([], [])
+| depth cs [] := pure (cs.map (λ _, []), [])
+| depth (c::cs) ((g, c', hs, _) :: l) :=
+  if c ≠ c' then do
+    (ps, gs) ← rcases_hint.process_constructors depth cs l,
+    pure ([] :: ps, gs)
+  else do
+    (p, gs) ← set_goals [g] >> rcases_hint.continue depth hs,
+    (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)
+| depth [] := prod.mk [] <$> get_goals
+| depth (e :: l) := do
+  (p, gs) ← rcases_hint_core depth e,
+  (ps, gs') ← gs.mfoldl (λ (r : listΠ rcases_patt × goals) g,
+    do (ps, gs') ← set_goals [g] >> rcases_hint.continue depth l,
+      pure (merge_list rcases_patt.merge r.1 ps, r.2 ++ gs')) ([], []),
+  pure (p :: ps, gs')
+
+meta def rcases_hint (p : pexpr) (depth : nat) : tactic rcases_patt :=
+do e ← i_to_expr p,
+  if e.is_local_constant then
+    focus1 $ do (p, gs) ← rcases_hint_core depth e, set_goals gs, pure p
+  else do
+    x ← mk_fresh_name,
+    n ← revert_kdependencies e semireducible,
+    (tactic.generalize e x)
+    <|>
+    (do t ← infer_type e,
+        tactic.assertv x t e,
+        get_local x >>= tactic.revert,
+        pure ()),
+    h ← tactic.intro1,
+    focus1 $ do (p, gs) ← rcases_hint_core depth h, set_goals gs, pure p
+
+meta def rintro_hint (depth : nat) : tactic (listΠ rcases_patt) :=
+do l ← intros,
+  focus1 $ do
+    (p, gs) ← rcases_hint.continue depth l,
+    set_goals gs,
+    pure p
+
 end tactic