use tactic

[robertylewis]

As requested on Zulip, a synonym for refine ⟨x, _⟩.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

For reviewers: code review check list

[digama0]

Is it possible to make the equivalent of <e1, e2, ..., en, _> with pexpr generation? The problem with <e1, <e2, ..., <en, _>>> is that it doesn't work with inductives and structures with more than two args.

[sgouezel]

Copy docstring to docs/tactics.md?

[robertylewis]

No way that's obvious to me. The anonymous constructor is a macro, and I can't build that shape recursively. This could be made to work for arbitrary inductives by looking at the target, identifying the constructor, and applying that, but that's more effort than I meant to spend here -- I don't think existsi works in that generality either, does it?

[johoelzl]

Myabe an adoption of the constructor tactic would help here?

[robertylewis]

You can do tactic.fconstructor >> l.mmap' tactic.refine when you have a single constructor with multiple arguments, but not when you have nested constructors with one argument each (like ∃ a b c : ℤ, a + b + c = 6). The anonymous constructor notation conveniently covers both these cases, but they're not really analogous otherwise.

[digama0]

Another possible generalization is to "figure out" the right bracketing of constructors, but maybe that's too magical? (Although I don't mind small tactics, once we have decided to have a tactic it seems reasonable to generalize it to any adjacent use cases to get something nice.)

[robertylewis]

Yeah, I mean, this is a one liner where the doc string took longer to write than the tactic itself. I can try to generalize it at some point but it won't happen this week.