From e7df2cb8448880e983084af029902169e413e3ec Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 4 Feb 2020 18:33:57 +0100 Subject: [PATCH] feat(tactic): add various tactics about local definitions --- src/data/option/defs.lean | 5 +++ src/tactic/core.lean | 65 ++++++++++++++++++++++++++++++++----- src/tactic/interactive.lean | 39 ++++++++++++++++++++++ test/tactics.lean | 48 +++++++++++++++++++++++++++ 4 files changed, 148 insertions(+), 9 deletions(-) diff --git a/src/data/option/defs.lean b/src/data/option/defs.lean index 36ebc54d059bf..303b2b13218eb 100644 --- a/src/data/option/defs.lean +++ b/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 := diff --git a/src/tactic/core.lean b/src/tactic/core.lean index 09cdcb4eb5615..ebc8f84daccc2 100644 --- a/src/tactic/core.lean +++ b/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. -/ diff --git a/src/tactic/interactive.lean b/src/tactic/interactive.lean index a5dc4fdc9bcfd..20802d1002499 100644 --- a/src/tactic/interactive.lean +++ b/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 diff --git a/test/tactics.lean b/test/tactics.lean index 2911ac468a346..ac8deca8c32aa 100644 --- a/test/tactics.lean +++ b/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