feat(tactic): add various tactics about local definitions

src/data/option/defs.lean

@@ -9,6 +9,11 @@ Extra definitions on option.
 namespace option
 variables {α : Type*} {β : Type*}
 
+/-- An elimination principle for `option`. It is a nondependent version of `option.rec_on`. -/
+protected def elim {α β} : option α → β → (α → β) → β
+| (some x) y f := f x
+| none     y f := y
+
 instance has_mem : has_mem α (option α) := ⟨λ a b, b = some a⟩
 
 @[simp] theorem mem_def {a : α} {b : option α} : a ∈ b ↔ b = some a :=

src/tactic/core.lean

@@ -217,15 +217,6 @@ a meaningful expression. -/
 meta def mk_local (n : name) : expr :=
 expr.local_const n n binder_info.default (expr.const n [])
 
-/-- `local_def_value e` returns the value of the expression `e`, assuming that `e` has been defined
-locally using a `let` expression. Otherwise it fails. -/
-meta def local_def_value (e : expr) : tactic expr :=
-do (v,_) ← solve_aux `(true) (do
-         (expr.elet n t v _) ← (revert e >> target)
-           | fail format!"{e} is not a local definition",
-         return v),
-   return v
-
 /-- `pis loc_consts f` is used to create a pi expression whose body is `f`.
 `loc_consts` should be a list of local constants. The function will abstract these local
 constants from `f` and bind them with pi binders.
@@ -353,6 +344,62 @@ do to_remove ← hs.mfilter $ λ h, do {
   to_remove.mmap' (λ h, try (clear h)),
   return (¬ to_remove.empty ∨ goal_simplified)
 
+/-- `revert_after e` reverts all local constants after local constant `e`. -/
+meta def revert_after (e : expr) : tactic ℕ := do
+  l ← local_context,
+  [pos] ← return $ l.indexes_of e | pp e >>= λ s, fail format!"No such local constant {s}",
+  let l := l.drop pos.succ, -- all local hypotheses after `e`
+  revert_lst l
+
+/-- `generalize' e n` is similar as `generalize` but also succeeds when `e` does not occur in the
+  goal, in which case it just calls `assert`. It already introduces the generalized variable. -/
+meta def generalize' (e : expr) (n : name) : tactic expr :=
+(generalize e n >> intro1) <|> note n none e
+
+/- Various tactics related to local definitions (local constants of the form `x : α := t`).
+  We call `t` the body or value of `x`. -/
+
+/-- `local_def_value e` returns the value of the expression `e`, assuming that `e` has been defined
+locally using a `let` expression. Otherwise it fails. -/
+meta def local_def_value (e : expr) : tactic expr :=
+do (v,_) ← solve_aux `(true) (do
+         (expr.elet n t v _) ← (revert e >> target)
+           | fail format!"{e} is not a local definition",
+         return v),
+   return v
+
+/-- `revert_deps e` reverts all the hypotheses that depend on one of the local
+  constants `e`, including the local definitions that have `e` in their definition.
+  This fixes a bug in `revert_kdeps` that does not revert local definitions for which `e` only
+  appears in the definition. -/
+/- We cannot implement it as `revert e >> intro1`, because after that `e` would not be in the
+  local context anymore. -/
+meta def revert_deps (e : expr) : tactic ℕ := do
+  n ← revert_kdeps e,
+  l ← local_context,
+  [pos] ← return $ l.indexes_of e,
+  let l := l.drop pos.succ, -- local hypotheses after `e`
+  ls ← l.mfilter $ λ e', try_core (local_def_value e') >>= λ o, return $ o.elim ff $ λ e'',
+    e''.has_local_constant e,
+  n' ← revert_lst ls,
+  return $ n + n'
+
+/-- `is_local_def e` succeeds when `e` is a local definition (a local constant of the form
+  `e : α := t`) and otherwise fails. -/
+meta def is_local_def (e : expr) : tactic unit :=
+retrieve $ do revert e, expr.elet _ _ _ _ ← target, skip
+
+/-- `clearbody e` clears the body of the local definition `e`, changing it into a regular hypothesis.
+  A hypothesis `e : α := t` is changed to `e : α`. -/
+meta def clearbody (e : expr) : tactic unit := do
+  n ← revert_after e,
+  is_local_def e <|>
+    pp e >>= λ s, fail format!"Cannot clear the body of {s}. It is not a local definition.",
+  let nm := e.local_pp_name,
+  (generalize' e nm >> clear e) <|>
+    fail format!"Cannot clear the body of {nm}. The resulting goal is not type correct.",
+  intron n
+
 /-- A variant of `simplify_bottom_up`. Given a tactic `post` for rewriting subexpressions,
 `simp_bottom_up post e` tries to rewrite `e` starting at the leaf nodes. Returns the resulting
 expression and a proof of equality. -/

src/tactic/interactive.lean

@@ -812,5 +812,44 @@ do (cxt,_) ← solve_aux `(true) $
    trace fmt,
    trace!"begin\n  \nend"
 
+/-- `revert_deps n₁ n₂ ...` reverts all the hypotheses that depend on one of `n₁, n₂, ...`
+  It does not revert `n₁, n₂, ...` themselves (unless they depend on another `nᵢ`). -/
+meta def revert_deps (ns : parse ident*) : tactic unit :=
+propagate_tags $ ns.reverse.mmap' $ λ n, get_local n >>= tactic.revert_deps
+
+/-- `revert_after n` reverts all the hypotheses after `n`. -/
+meta def revert_after (n : parse ident) : tactic unit :=
+propagate_tags $ get_local n >>= tactic.revert_after >> skip
+
+/-- `clearbody n₁ n₂ ...` clears the bodies of the local definitions `n₁, n₂ ...`, changing them
+  into regular hypotheses. A hypothesis `n : α := t` is changed to `n : α`. -/
+meta def clearbody (ns : parse ident*) : tactic unit :=
+propagate_tags $ ns.reverse.mmap' $ λ n, get_local n >>= tactic.clearbody
+
+/--
+`generalize' : e = x` replaces all occurrences of `e` in the target with a new hypothesis `x` of the same type.
+
+`generalize' h : e = x` in addition registers the hypothesis `h : e = x`.
+
+`generalize'` is similar to `generalize`. The difference is that `generalize'` also succeeds when `e`
+  does not occur in the goal. It is similar to `set`, but the resulting hypothesis `x` is not a local definition.
+-/
+meta def generalize' (h : parse ident?) (_ : parse $ tk ":") (p : parse generalize_arg_p) : tactic unit :=
+propagate_tags $
+do let (p, x) := p,
+   e ← i_to_expr p,
+   some h ← pure h | tactic.generalize' e x >> skip,
+   tgt ← target,
+   -- if generalizing fails, fall back to not replacing anything
+   tgt' ← do {
+     ⟨tgt', _⟩ ← solve_aux tgt (tactic.generalize' e x >> target),
+     to_expr ``(Π x, %%e = x → %%(tgt'.binding_body.lift_vars 0 1))
+   } <|> to_expr ``(Π x, %%e = x → %%tgt),
+   t ← assert h tgt',
+   swap,
+   exact ``(%%t %%e rfl),
+   intro x,
+   intro h
+
 end interactive
 end tactic

test/tactics.lean

@@ -500,3 +500,51 @@ section simp_rw
     (∀ s, f '' s ⊆ t) = ∀ s : set α, ∀ x ∈ s, x ∈ f ⁻¹' t :=
   by simp_rw [set.image_subset_iff, set.subset_def]
 end simp_rw
+
+section local_definitions
+/- Some tactics about local definitions.
+  Testing revert_deps, revert_after, generalize', clearbody. -/
+open tactic
+example {A : ℕ → Type} {n : ℕ} : let k := n + 3, l := k + n, f : A k → A k := id in
+  ∀(x : A k) (y : A (n + k)) (z : A n) (h : k = n + n), unit :=
+begin
+  intros, guard_target unit,
+  revert_deps k, tactic.intron 5, guard_target unit,
+  revert_after n, tactic.intron 7, guard_target unit,
+  do { e ← get_local `k, tactic.revert_deps e, l ← local_context, guard $ e ∈ l, intros },
+  exact unit.star
+end
+
+example {A : ℕ → Type} {n : ℕ} : let k := n + 3, l := k + n, f : A k → A (n+3) := id in
+  ∀(x : A k) (y : A (n + k)) (z : A n) (h : k = n + n), unit :=
+begin
+  intros,
+  success_if_fail_with_msg {generalize : n + k = x}
+    "generalize tactic failed, failed to find expression in the target",
+  generalize' : n + k = x,
+  generalize' h : n + k = y,
+  exact unit.star
+end
+
+example {A : ℕ → Type} {n : ℕ} : let k := n + 3, l := k + n, f : A k → A (n+3) := id in
+  ∀(x : A k) (y : A (n + k)) (z : A n) (h : k = n + n), unit :=
+begin
+  intros,
+  tactic.to_expr ```(n + n) >>= λ e, tactic.generalize' e `xxx,
+  success_if_fail_with_msg {clearbody n}
+    "Cannot clear the body of n. It is not a local definition.",
+  success_if_fail_with_msg {clearbody k}
+    "Cannot clear the body of k. The resulting goal is not type correct.",
+  clearbody k f,
+  exact unit.star
+end
+
+example {A : ℕ → Type} {n : ℕ} : let k := n + 3, l := k + n, f : A k → A k := id in
+  ∀(x : A k) (y : A (n + k)) (z : A n) (h : k = n + n), unit :=
+begin
+  intros,
+  clearbody k f,
+  exact unit.star
+end
+
+end local_definitions