feat(library/init/meta/*): port rename tactic from mathlib
#205
Conversation
We reimplement the interactive `rename` tactic. The new tactic has the following features: - Multiple hypotheses can be renamed at once. - The order of hypotheses doesn't change. - If there are multiple hypotheses with the same name in the context, they are all renamed. This tactic was previously implemented in mathlib. To facilitate the implementation, we also port `list.after` from mathlib.
|
Sorry, just found a bug in nu-rename. Don't review/merge yet. |
`tactic.rename_many` can select the hypotheses to be renamed by unique names. When using this mode, it would erroneously change the display name of any hypothesis that was not renamed to its unique name.
|
Okay, now it's at least less obviously buggy. |
| meta def revertible_local_context : tactic (list expr) := | ||
| do ctx ← local_context, | ||
| frozen ← frozen_local_instances, | ||
| pure $ |
There was a problem hiding this comment.
Is this different from ctx.drop (frozen_local_instance.get_or_else []).length?
There was a problem hiding this comment.
I think so, yes. Your version drops as many hyps from the context as there are frozen instances. However, we can have other hyps in between the frozen instances, so the part of the context that we can't touch can be longer.
There was a problem hiding this comment.
That's my question: is this possible?
There was a problem hiding this comment.
Yes, here's a full test case where the implementations diverge.
namespace list
def after {α} (p : α → Prop) [decidable_pred p] : list α → list α
| [] := []
| (x :: xs) := if p x then xs else after xs
end list
namespace tactic
meta def revertible_local_context₁ : tactic (list expr) :=
do ctx ← local_context,
frozen ← frozen_local_instances,
pure $
match frozen with
| none := ctx
| some [] := ctx
| some (h :: _) := ctx.after (eq h)
end
meta def revertible_local_context₂ : tactic (list expr) :=
do ctx ← local_context,
frozen ← frozen_local_instances,
pure $ ctx.drop $ (frozen.get_or_else []).length
meta def interactive.test : tactic unit :=
do revertible_local_context₁ >>= trace,
revertible_local_context₂ >>= trace
end tactic
lemma test {α : Prop} [decidable α] {β : Prop} [decidable β] : unit :=
begin
test,
exact ()
endThere was a problem hiding this comment.
Ah, so frozen_local_instances only returns the instances.
| @@ -665,7 +684,9 @@ private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indi | |||
| end else none | |||
|
|
|||
| private meta def rename_lams : expr → list name → tactic unit | |||
There was a problem hiding this comment.
I feel like rename_lams should be reimplemented using rename_many and rename_unstable should be removed.
There was a problem hiding this comment.
Yes! That'll be the case tag PR which I'm working on, and which this PR is leading up to.
|
Thanks for the review! |
|
How do you use this tactic to rename multiple variables with the same name? example (x x : ℕ) : ... :=
begin
rename ???
end |
|
Hopefully that just names the second one. If you have this situation, you can call |
|
No, |
| rename' x y -- rename x to y | ||
| rename' x → y -- ditto | ||
| rename' [x y, a b] -- rename x to y and a to b | ||
| rename' [x → y, a → b] -- ditto |
There was a problem hiding this comment.
These should be rename.
There was a problem hiding this comment.
Yeah, I just noticed that as well. :( I'll write a doc PR.
This PR ports the
renameinteractive tactic from mathlib (with some additional improvements). Features over current corerename:Breakage in
mathlib:renameandlist.after(now in core).renamewhen there are multiple hypotheses with the same name.