[Merged by Bors] - feat(tactic/trunc_cases): a tactic for case analysis on trunc hypotheses

src/tactic/core.lean

@@ -535,6 +535,16 @@ arguments or in the target. Also returns the argument position of each returned
 meta def get_pi_binders_dep : expr → tactic (list (ℕ × binder) × expr) :=
 get_pi_binders_dep_aux 0
 
+/-- call `assert n t` with a fresh name `n`. -/
+meta def assert_fresh (t : expr) : tactic expr :=
+do n ← get_unused_name `h none,
+   assert n t
+
+/-- call `assertv n t v` with a fresh name `n`. -/
+meta def assertv_fresh (t : expr) (v : expr) : tactic expr :=
+do h ← get_unused_name `h none,
+   assertv h t v
+
 /-- A variation on `assert` where a (possibly incomplete)
 proof of the assertion is provided as a parameter.
 

src/tactic/finish.lean

@@ -46,16 +46,6 @@ declare_trace auto.finish
 
 namespace tactic
 
-/-- call `(assert n t)` with a fresh name `n`. -/
-meta def assert_fresh (t : expr) : tactic expr :=
-do n ← get_unused_name `h none,
-   assert n t
-
-/-- call `(assertv n t v)` with a fresh name `n`. -/
-meta def assertv_fresh (t : expr) (v : expr) : tactic expr :=
-do h ← get_unused_name `h none,
-   assertv h t v
-
 namespace interactive
 
 meta def revert_all := tactic.revert_all

src/tactic/trunc_cases.lean

@@ -0,0 +1,41 @@
+import tactic.core
+import tactic.doc_commands
+
+namespace tactic
+namespace interactive
+
+open interactive
+open interactive.types
+open tactic
+
+/--
+Perform case analysis on a `trunc` expression,
+preferentially using the recursor `trunc.rec_on_subsingleton`
+when the goal is a subsingleton,
+and using `trunc.rec` otherwise.
+
+Additionally, if the new hypothesis is a type class,
+reset the instance cache.
+-/
+meta def trunc_cases (e : parse texpr) (ids : parse with_ident_list) : tactic unit :=
+do
+  e ← to_expr e,
+  let ids := if ids = [] ∧ e.is_local_constant then [e.local_pp_name] else ids,
+  e ← if e.is_local_constant then return e else (do t ← infer_type e, assertv_fresh t e),
+  tgt ← target,
+  ss ← succeeds (mk_app `subsingleton [tgt] >>= mk_instance),
+  (_, [e], _) :: _ ← if ss then
+    tactic.induction e ids `trunc.rec_on_subsingleton
+  else
+    tactic.induction e ids,
+  c ← infer_type e >>= is_class,
+  when c unfreeze_local_instances
+
+end interactive
+end tactic
+
+add_tactic_doc
+{ name                     := "trunc_cases",
+  category                 := doc_category.tactic,
+  decl_names               := [`tactic.interactive.trunc_cases],
+  tags                     := ["case bashing"] }

test/trunc_cases.lean

@@ -0,0 +1,30 @@
+import tactic.trunc_cases
+import data.quot
+
+example (t : trunc ℕ) : punit :=
+begin
+  trunc_cases t,
+  exact (),
+  -- no more goals, because `trunc_cases` used the correct recursor
+end
+
+example (t : trunc ℕ) : ℕ :=
+begin
+  trunc_cases t,
+  guard_hyp t := ℕ, -- verify that the new hypothesis is still called `t`.
+  exact 0,
+  simp,
+end
+
+example {α : Type} (I : trunc (has_zero α)) (f : false) : α :=
+begin
+  trunc_cases I,
+  exact 0, -- verify that the typeclass is immediately available
+  exfalso, exact f,
+end
+
+example {α : Type} [subsingleton α] (I : trunc (has_zero α)) (f : false) : α :=
+begin
+  trunc_cases I,
+  exact 0,
+end