feat(tactic): add various tactics about local definitions (leanprover…

…-community#1953)

* feat(tactic): add various tactics about local definitions

* remove {α β}

* rename generalize' in monotonicity.

* updates after reviews

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

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

@@ -218,15 +218,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.
@@ -354,6 +345,70 @@ 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` generalizes the target with respect to `e`. It creates a new local constant
+  with name `n` of the same type as `e` and replaces all occurrences of `e` by `n`.
+
+  `generalize'` is similar to `generalize` but also succeeds when `e` does not occur in the
+  goal, in which case it just calls `assert`.
+  In contrast to `generalize` 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 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 :=
+pp e >>= λ s, -- running `pp` here, because we cannot access it in the `type_context` monad.
+tactic.unsafe.type_context.run $ do
+  lctx <- tactic.unsafe.type_context.get_local_context,
+  some ldecl <- return $ lctx.get_local_decl e.local_uniq_name |
+    tactic.unsafe.type_context.fail format!"No such hypothesis {s}.",
+  some let_val <- return ldecl.value |
+    tactic.unsafe.type_context.fail format!"Variable {e} is not a local definition.",
+  return let_val
+
+/-- `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 that would change the local constant in
+  the context. -/
+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
+
+/-- `clear_value e` clears the body of the local definition `e`, changing it into a regular hypothesis.
+  A hypothesis `e : α := t` is changed to `e : α`.
+  This tactic is called `clearbody` in Coq. -/
+meta def clear_value (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

@@ -826,5 +826,44 @@ do ty ← i_to_expr t,
          fail "could not infer nonempty instance",
        resetI)
 
+/-- `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
+
+/-- `clear_value 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 clear_value (ns : parse ident*) : tactic unit :=
+propagate_tags $ ns.reverse.mmap' $ λ n, get_local n >>= tactic.clear_value
+
+/--
+`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' : e = x` 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

src/tactic/monotonicity/interactive.lean

@@ -405,7 +405,7 @@ open monad
 
 /-- tactic-facing function, similar to `interactive.tactic.generalize` with the
 exception that meta variables -/
-meta def generalize' (h : name) (v : expr) (x : name) : tactic (expr × expr) :=
+private meta def monotonicity.generalize' (h : name) (v : expr) (x : name) : tactic (expr × expr) :=
 do tgt ← target,
    t ← infer_type v,
    tgt' ← do {
@@ -427,7 +427,7 @@ do tgt ← target >>= instantiate_mvars,
    vs' ← mmap (λ v,
              do h ← get_unused_name `h,
                 x ← get_unused_name `x,
-                prod.snd <$> generalize' h v x) vs,
+                prod.snd <$> monotonicity.generalize' h v x) vs,
      tac ctx;
      vs'.mmap' (try ∘ tactic.subst)
 

test/tactics.lean

@@ -530,3 +530,56 @@ begin
 end
 
 end rename'
+
+section local_definitions
+/- Some tactics about local definitions.
+  Testing revert_deps, revert_after, generalize', clear_value. -/
+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,
+  do { e ← get_local `k, e1 ← tactic.local_def_value e, e2 ← to_expr ```(n + 3), guard $ e1 = e2 },
+  do { e ← get_local `n, success_if_fail_with_msg (tactic.local_def_value e)
+    "Variable n is not a local definition." },
+  do { success_if_fail_with_msg (tactic.local_def_value `(1 + 2))
+    "No such hypothesis 1 + 2." },
+  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 {clear_value n}
+    "Cannot clear the body of n. It is not a local definition.",
+  success_if_fail_with_msg {clear_value k}
+    "Cannot clear the body of k. The resulting goal is not type correct.",
+  clear_value 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,
+  clear_value k f,
+  exact unit.star
+end
+
+end local_definitions