cases.lean

inductive foo
| mk1 : nat → nat → foo
| mk2 : nat → bool → foo

example (a : foo) : nat :=
begin
  /- All new hypotheses are named 'a' -/
  cases a
end

/- Remark: Lean will reuse the binder names used in constructors. -/
inductive foo2
| mk1 : Π (x y : nat), foo2
| mk2 : Π (z : nat) (b : bool), foo2

example (a : foo2) : nat :=
begin
  /- The new hypotheses are named 'x', 'y', 'z' and 'b' -/
  cases a
end


namespace tactic
/- We can define our own new tactics. -/
meta def cases_with_fresh_names (h : expr) (p : name) : tactic unit :=
/- Assuming the type of h is of the form (I ...) -/
do I  ← infer_type h >>= whnf,
   /- mk_constructors_arg_names is a helper function defined in the standard library, press M-. to jump to its definition. -/
   ns ← mk_constructors_arg_names I^.get_app_fn^.const_name p,
   cases_using h ns^.join

end tactic

/- We use the namespace tactic.interactive to "auto-quote" the arguments for our tactics. -/
namespace tactic.interactive
open interactive.types tactic

meta def fcases (h : qexpr0) (p : using_ident) : tactic unit :=
do h ← to_expr h,
   match p with
   | some n := cases_with_fresh_names h n
   | none   := cases_with_fresh_names h `h
   end

end tactic.interactive

example (a : foo) : nat :=
begin
  /- creates two goals with hypothesis names: h.1, h.2, h.3, h.4 -/
  fcases a
end

example (a : foo) : nat :=
begin
  /- creates two goals with hypothesis names: H.1, H.2, H.3, H.4 -/
  fcases a using H
end


namespace tactic

def {u} replace_ith {α : Type u} (a : α) : nat → list α → list α
| 0     (h::t) := a :: t
| (n+1) (h::t) := h :: replace_ith n t
| _     l      := l

def replace_name (l : list (list name)) (i : nat) (j : nat) (n : name) : list (list name) :=
match l^.nth i with
| some l_i :=
  let new_l_i := replace_ith n j l_i in
  replace_ith new_l_i i l
| none     := l
end

def replace_names : list (list name) → list (nat × nat × name) → list (list name)
| l []               := l
| l ((i, j, n) :: r) := replace_names (replace_name l i j n) r


/- Similar to cases_with_fresh_names, but we can name hypotheses. -/
meta def cases_with_names (h : expr) (p : name) (r : list (nat × nat × name)) : tactic unit :=
/- Assuming the type of h is of the form (I ...) -/
do I  ← infer_type h >>= whnf,
   /- mk_constructors_arg_names is a helper function defined in the standard library, press M-. to jump to its definition. -/
   ns ← mk_constructors_arg_names I^.get_app_fn^.const_name p,
   ns ← return $ replace_names ns r,
   cases_using h ns^.join

end tactic

/- We use the namespace tactic.interactive to "auto-quote" the arguments for our tactics. -/
namespace tactic.interactive
open interactive.types tactic

/- In the current version we cannot auto-quote names nested in types such as
   list (nat × nat × name).
   This will change in the future. -/
meta def rcases (h : qexpr0) (tk : colon_tk) (r : list (nat × nat × name)) : tactic unit :=
do h ← to_expr h,
   cases_with_names h `h r 

end tactic.interactive

example (a : foo) : nat :=
begin
  /- creates two goals with hypothesis names: x, h.2, h.3, h.4 -/
  rcases a : [(0,0,`x)]
end

example (a : foo) : nat :=
begin
  /- creates two goals with hypothesis names: h.1, x, y, h.4 -/
  rcases a : [(0,1,`x), (1,0,`y)]
end