primed tactics from mathlib

[bryangingechen]

Here's a list of "primed" tactics in mathlib which fix bugs or add features to tactics in the core library. I'm not sure which of these should replace their counterparts, if someone else can review this that'd be great. (Feel free to edit this list directly!)

I can try to tackle the ones from tactic.core and tactic.interactive which don't require modifying C++.

Primed tactics in mathlib's tactic.core:

• [ ] ~~of_tactic'~~ / has_coe' replaces ~~of_tactic and~~ has_coe in init.lean.parser. ~~of_tactic is implemented in C++ here.~~ of_tactic' was removed in the 3.7.1c update since it was no longer necessary after the fix in #147.

• [ ] eval_expr' replaces eval_expr in init.meta.tactic; C++ implementation here.

• [ ] has_attribute' returns a bool whereas has_attribute in init.meta.tactic returns a nat; C++ implementation here.

• [ ] simp_bottom_up' "a variant" of simplify_bottom_up.

• [ ] triv': "Unlike triv, it only unfolds reducible definitions, so it sometimes fails faster."

~- [ ] iterate', compare iterate in init.meta.tactic.~

~- [ ] target' is a wrapper around target (C++ implementation here) that instantiates mvars and calls whnf.~

• [ ] resolve_name' wraps resolve_name (C++ implementation here) so that it succeeds on a list of empty goals.

Primed tactics in mathlib's tactic.interactive:

• [ ] congr' behaves like congr but takes an optional argument specifying the depth of recursive applications.

• [ ] guard_hyp' fixes guard_hyp by instantiating meta variables.

~- [ ] guard_expr_eq' uses is_def_eq, whereas guard_expr_eq uses alpha_eqv.~

~- [ ] guard_target' uses guard_expr_eq', whereas guard_target uses guard_expr_eq.~

• [ ] change' "mimics the behavior of change, except in the case of change x with y at l. In this case, it will correctly replace occurences of x with y at all possible hypotheses in l. As long as x and y are defeq, it should never fail."

Other primed tactics in mathlib:

• [x] rename' adds several features to rename. Ported in #205.

• [ ] apply' / symmetry' / reflexivity' / transitivity' / ... fixes the "apply bug" in apply and related tactics (also in init.meta.interactive). See also apply_fun.

• [ ] clear' works like clear (C++ implementation here) except that the hypotheses can be cleared in any order. See also clear_dependent in the same file.

Any others?

[fpvandoorn]

Since a couple of hours: generalize' and its corresponding interactive version (not completely backwards compatible, since it already apply intro1).

[bryangingechen]

@fpvandoorn Ah, cool! Do you mind making a PR to core either replacing generalize with generalize' or just fixing it?

[cipher1024]

I think target' should not replace target. We don't need to instantiate mvars and normalize the goal every time we query it. It is a much slower version of target.

[gebner]

iterate', compare iterate in init.meta.tactic.

They do different things.

guard_target' uses guard_expr_eq', whereas guard_target uses guard_expr_eq.

:-1: This is mainly used for testing, where you explicitly do not want to compare modulo definitional equality.

[bryangingechen]

Thanks, I crossed those out in the post above!

[JLimperg]

revert_deps could also be a candidate. It works like revert_kdependencies, but takes the bodies of local definitions into account. It would have to be generalised a bit to properly replace revert_kdependencies.