feat(tactic/fin_cases): a tactic to case bash on fin n (#352)

* feat(tactic/fin_cases): a tactic to case bash on `fin n`

* using core is_numeral

* removing guard

just rely on eval_expr to decide if we have an explicit nat

* add parsing, tests, documentation

* don't fail if the rewrite fails

* fixes

data/fin.lean

@@ -27,6 +27,8 @@ lemma eq_iff_veq (a b : fin n) : a = b ↔ a.1 = b.1 :=
 
 instance fin_to_nat (n : ℕ) : has_coe (fin n) nat := ⟨fin.val⟩
 
+@[simp] def mk_val {m n : ℕ} (h : m < n) : (⟨m, h⟩ : fin n).val = m := rfl
+
 instance {n : ℕ} : decidable_linear_order (fin n) :=
 { le_refl := λ a, @le_refl ℕ _ _,
   le_trans := λ a b c, @le_trans ℕ _ _ _ _,

docs/tactics.md

@@ -551,3 +551,14 @@ Known limitation(s):
     `squeeze_simp` will produce as many suggestions as the number of goals it is applied to.
     It is likely that none of the suggestion is a good replacement but they can all be
     combined by concatenating their list of lemmas.
+
+## fin_cases
+Performs cases analysis on a `fin n` hypothesis. As an example, in
+```
+example (f : ℕ → Prop) (p : fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val :=
+begin
+  fin_cases p,
+  all_goals { assumption }
+end
+```
+after `fin_cases p`, there are three goals, `f 0`, `f 1`, and `f 2`.

tactic/fin_cases.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2018 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Scott Morrison
+
+Case bashing on `fin n`, for explicit numerals `n`.
+-/
+import data.fin
+
+namespace tactic
+open lean.parser
+open interactive interactive.types expr
+
+meta def fin_cases_at (e : expr) : tactic unit :=
+do `(fin %%n) ← infer_type e,
+   n ← eval_expr ℕ n,
+   [(_, [val, bd], _)] ← cases_core e [`val, `bd],
+   -- We now call `cases val` n times, rotating the generated goals out of the way.
+   iterate_at_most n (do val ← get_local `val, cases val, rotate 1),
+   -- We've got an absurd hypothesis `bd`, but it is messy: it looks like
+   -- `nat.succ (... (nat.succ val)) < n`
+   -- So we rewrite it as `bd : val + 1 + ... + 1 < n`, and use `dec_trivial` to kill it.
+   ss ← mk_const `nat.succ_eq_add_one,
+   bd ← get_local `bd,
+   (list.range n).mfoldl (λ bd _, do rewrite_hyp ss bd) bd,
+   to_expr ``(absurd %%bd dec_trivial) >>= exact,
+   -- We put the goals back in order, and clear the `bd` hypotheses.
+   iterate_exactly n (do rotate_right 1,
+                         try `[rw [fin.mk_val]],
+                         try (get_local `bd >>= clear))
+
+namespace interactive
+private meta def hyp := tk "*" *> return none <|> some <$> ident
+
+/--
+`fin_cases h` performs case analysis on a hypothesis `h : fin n`, where `n` is an explicit natural
+number. `fin_cases *` performs case analysis on all suitable hypotheses.
+
+As an example, in
+```
+example (f : ℕ → Prop) (p : fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val :=
+begin
+  fin_cases p,
+  all_goals { assumption }
+end
+```
+after `fin_cases p`, there are three goals, `f 0`, `f 1`, and `f 2`.
+-/
+meta def fin_cases : parse hyp → tactic unit
+| none := do ctx ← local_context,
+             ctx.mfirst fin_cases_at <|> fail "No explicit `fin n` hypotheses."
+| (some n) := do h ← get_local n, fin_cases_at h
+end interactive
+
+end tactic

tests/fin_cases.lean

@@ -0,0 +1,17 @@
+import tactic.fin_cases
+
+
+example (f : ℕ → Prop) (p : fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val :=
+begin
+  fin_cases *,
+  all_goals { assumption }
+end
+
+example (x2 : fin 2) (x3 : fin 3) (n : nat) (y : fin n) : x2.val * x3.val = x3.val * x2.val :=
+begin
+  fin_cases x2;
+  fin_cases x3,
+  success_if_fail { fin_cases * },
+  success_if_fail { fin_cases y },
+  all_goals { simp },
+end