feat(tactic/trunc_cases): a tactic for case analysis on trunc hypothe…

…ses (#2368)

```
/--
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.
-/
```

src/tactic/core.lean

@@ -925,10 +925,16 @@ do l ← local_context,
    r ← successes (l.reverse.map (λ h, cases h >> skip)),
    when (r.empty) failed
 
-/-- Given a proof `pr : t`, adds `h : t` to the current context, where the name `h` is fresh. -/
-meta def note_anon (e : expr) : tactic expr :=
-do n ← get_unused_name "lh",
-   note n none e
+/--
+`note_anon t v`, given a proof `v : t`,
+adds `h : t` to the current context, where the name `h` is fresh.
+
+`note_anon none v` will infer the type `t` from `v`.
+-/
+-- While `note` provides a default value for `t`, it doesn't seem this could ever be used.
+meta def note_anon (t : option expr) (v : expr) : tactic expr :=
+do h ← get_unused_name `h none,
+   note h t v
 
 /-- `find_local t` returns a local constant with type t, or fails if none exists. -/
 meta def find_local (t : pexpr) : tactic expr :=

src/tactic/equiv_rw.lean

@@ -192,7 +192,7 @@ do
   e ← equiv_rw_type e x_ty cfg,
   eq ← to_expr ``(%%x' = equiv.symm %%e (equiv.to_fun %%e %%x')),
   prf ← to_expr ``((equiv.symm_apply_apply %%e %%x').symm),
-  h ← assertv_fresh eq prf,
+  h ← note_anon eq prf,
   -- Revert the new hypothesis, so it is also part of the goal.
   revert h,
   ex ← to_expr ``(equiv.to_fun %%e %%x'),

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
@@ -261,7 +251,7 @@ meta def do_substs : tactic unit := do_subst >> repeat do_subst
  and returns `tt` if anything nontrivial has been added. -/
 meta def add_conjuncts : expr → expr → tactic bool :=
 λ pr t,
-let assert_consequences := λ e t, mcond (add_conjuncts e t) skip (assertv_fresh t e >> skip) in
+let assert_consequences := λ e t, mcond (add_conjuncts e t) skip (note_anon t e >> skip) in
 do t' ← whnf_reducible t,
    match t' with
    | `(%%a ∧ %%b) :=

src/tactic/interval_cases.lean

@@ -192,7 +192,7 @@ Here `hl` should be an expression of the form `a ≤ n`, for some explicit `a`,
 `hu` should be of the form `n < b`, for some explicit `b`.
 -/
 meta def interval_cases_using (hl hu : expr) : tactic unit :=
-to_expr ``(mem_set_elems (Ico _ _) ⟨%%hl, %%hu⟩) >>= note_anon >>= fin_cases_at none
+to_expr ``(mem_set_elems (Ico _ _) ⟨%%hl, %%hu⟩) >>= note_anon none >>= fin_cases_at none
 
 setup_tactic_parser
 

src/tactic/trunc_cases.lean

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import tactic.chain
+import tactic.doc_commands
+import data.quot
+
+namespace tactic
+
+/-- Auxiliary tactic for `trunc_cases`. -/
+private meta def trunc_cases_subsingleton (e : expr) (ids : list name) : tactic expr :=
+do
+  -- When the target is a subsingleton,
+  -- we can just use induction along `trunc.rec_on_subsingleton`,
+  -- generating just a single goal.
+  [(_, [e], _)] ← tactic.induction e ids `trunc.rec_on_subsingleton,
+  return e
+
+/-- Auxiliary tactic for `trunc_cases`. -/
+private meta def trunc_cases_nondependent (e : expr) (ids : list name) : tactic expr :=
+do
+  -- We may as well just use `trunc.lift_on`.
+  -- (It would be nice if we could use the `induction` tactic with non-dependent recursors, too?)
+  -- (In fact, the general strategy works just as well here,
+  -- except that it leaves a beta redex in the invariance goal.)
+  to_expr ``(trunc.lift_on %%e) >>= tactic.fapply,
+  -- Replace the hypothesis `e` with the unboxed version.
+  tactic.clear e,
+  e ← tactic.intro e.local_pp_name,
+  -- In the invariance goal, introduce the two arguments using the specified identifiers
+  tactic.swap,
+  match ids.nth 1 with
+  | some n := tactic.intro n
+  | none := tactic.intro1
+  end,
+  match ids.nth 2 with
+  | some n := tactic.intro n
+  | none := tactic.intro1
+  end,
+  tactic.swap,
+  return e
+
+/-- Auxiliary tactic for `trunc_cases`. -/
+private meta def trunc_cases_dependent (e : expr) (ids : list name) : tactic expr :=
+do
+  -- If all else fails, just use the general induction principle.
+  [(_, [e], _), (_, [e_a, e_b, e_p], _)] ← tactic.induction e ids,
+  -- However even now we can do something useful:
+  -- the invariance goal has a useless `e_p : true` hypothesis,
+  -- and after casing on that we may be able to simplify away
+  -- the `eq.rec`.
+  swap, (tactic.cases e_p >> `[try { simp only [eq_rec_constant] }]), swap,
+  return e
+
+namespace interactive
+
+open interactive
+open interactive.types
+open tactic
+
+/--
+`trunc_cases e` performs case analysis on a `trunc` expression `e`,
+attempting the following strategies:
+1. when the goal is a subsingleton, calling `induction e using trunc.rec_on_subsingleton`,
+2. when the goal does not depend on `e`, calling `fapply trunc.lift_on e`,
+   and using `intro` and `clear` afterwards to make the goals look like we used `induction`,
+3. otherwise, falling through to `trunc.rec_on`, and in the new invariance goal
+   calling `cases h_p` on the useless `h_p : true` hypothesis,
+   and then attempting to simplify the `eq.rec`.
+
+`trunc_cases e with h` names the new hypothesis `h`.
+If `e` is a local hypothesis already,
+`trunc_cases` defaults to reusing the same name.
+
+`trunc_cases e with h h_a h_b` will use the names `h_a` and `h_b` for the new hypothesis
+in the invariance goal if `trunc_cases` uses `trunc.lift_on` or `trunc.rec_on`.
+
+Finally, if the new hypothesis from inside the `trunc` is a type class,
+`trunc_cases` resets the instance cache so that it is immediately available.
+-/
+meta def trunc_cases (e : parse texpr) (ids : parse with_ident_list) : tactic unit :=
+do
+  e ← to_expr e,
+  -- If `ids = []` and `e` is a local constant, we'll want to give
+  -- the new unboxed hypothesis the same name.
+  let ids := if ids = [] ∧ e.is_local_constant then [e.local_pp_name] else ids,
+  -- Make a note of the expr `e`, or reuse `e` if it is already a local constant.
+  e ← if e.is_local_constant then
+        return e
+      else
+        (do n ← match ids.nth 0 with | some n := pure n | none := mk_fresh_name end, note n none e),
+  -- Now check if the target is a subsingleton.
+  tgt ← target,
+  ss ← succeeds (mk_app `subsingleton [tgt] >>= mk_instance),
+  -- In each branch here, we're going to capture the name of the new unboxed hypothesis
+  -- so that we can later check if it's a typeclass and if so unfreeze local instances.
+  e ← if ss then trunc_cases_subsingleton e ids
+      else if e.occurs tgt then trunc_cases_dependent e ids
+      else trunc_cases_nondependent 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,71 @@
+import tactic.trunc_cases
+import tactic.interactive
+import data.quot
+
+example (t : trunc ℕ) : punit :=
+begin
+  trunc_cases t,
+  exact (),
+  -- no more goals, because `trunc_cases` used the correct `trunc.rec_on_subsingleton` recursor
+end
+
+example (t : trunc ℕ) : ℕ :=
+begin
+  trunc_cases t,
+  guard_hyp t := ℕ, -- verify that the new hypothesis is still called `t`.
+  exact 0,
+  -- verify that we don't even need to use `simp`,
+  -- because `trunc_cases` has already removed the `eq.rec`.
+  refl,
+end
+
+example {α : Type} [subsingleton α] (I : trunc (has_zero α)) : α :=
+begin
+  trunc_cases I,
+  exact 0,
+end
+
+/-- A mock typeclass, set up so that it's possible to extract data from `trunc (has_unit α)`. -/
+class has_unit (α : Type) [has_one α] :=
+(unit : α)
+(unit_eq_one : unit = 1)
+
+def u {α : Type} [has_one α] [has_unit α] : α := has_unit.unit α
+attribute [simp] has_unit.unit_eq_one
+
+example {α : Type} [has_one α] (I : trunc (has_unit α)) : α :=
+begin
+  trunc_cases I,
+  exact u, -- Verify that the typeclass is immediately available
+  -- Verify that there's no `eq.rec` in the goal.
+  (do tgt ← tactic.target, eq_rec ← tactic.mk_const `eq.rec, guard $ ¬ eq_rec.occurs tgt),
+  simp [u],
+end
+
+universes v w z
+
+/-- Transport through a product is given by individually transporting each component. -/
+-- It's a pity that this is no good as a `simp` lemma.
+-- (It seems the unification problem with `λ a, W a × Z a` is too hard.)
+-- (One could write a tactic to syntactically analyse `eq.rec` expressions
+-- and simplify more of them!)
+lemma eq_rec_prod {α : Sort v} (W : α → Type w) (Z : α → Type z) {a b : α} (p : W a × Z a) (h : a = b) :
+  @eq.rec α a (λ a, W a × Z a) p b h = (@eq.rec α a W p.1 b h, @eq.rec α a Z p.2 b h) :=
+begin
+  cases h,
+  simp only [prod.mk.eta],
+end
+
+-- This time, we make a goal that (quite artificially) depends on the `trunc`.
+example {α : Type} [has_one α] (I : trunc (has_unit α)) : α × plift (I = I) :=
+begin
+  -- This time `trunc_cases` has no choice but to use `trunc.rec_on`.
+  trunc_cases I,
+  { exact ⟨u, plift.up rfl⟩, },
+  { -- And so we get an `eq.rec` in the invariance goal.
+    -- Since `simp` can't handle it because of the unification problem,
+    -- for now we have to handle it by hand.
+    convert eq_rec_prod (λ I, α) (λ I, plift (I = I)) _ _,
+    { simp [u], },
+    { ext, } }
+end