Renaming `library_search`

Stream: mathlib4

[Scott Morrison]

@Patrick Massot wrote to me saying

And also it's really awfully long to type so we told students to start all their files with

macro "ls" : tactic => `(tactic|library_search)

So... shall I rename library_search?

[Scott Morrison]

/poll Possible names for library_search

[Thomas Murrills]

what about apply? (and have? and rewrite?), in the spirit of using *? for try-this-like behavior?

[Jireh Loreaux]

just thinking out loud: ls is confusing unless you know what it's short for, doubly so because in the shell it means "list". I guess that's also true of rw, but I feel like there's less options to expand rw into a meaningful word.

[Jireh Loreaux]

One key thing though: library_search doesn't show appear in finished code, so there is no sacrifice for readability if we make it ultra short like ls. But ls could easily be a variable name. To appease my thoughts above, I've added lib to the list of choices. It is:

• short and quick to type
• indicative of the expanded word
• not so likely to be a variable in context (I guess maybe this doesn't matter from a parsing perspective though.)

[Scott Morrison]

search is proving popular, but I worry that it's just cause y'all are used to using library_search, and haven't got in the habit of using the also useful search tools propose and rewrites. :-)

[Eric Wieser]

Does library_search ever actually produce apply foo?

[Eric Wieser]

Doesn't it produce exact foo, suggesting exact? would be better than apply??

[Alex J. Best]

Well it uses either exact or refine via docs4#Std.Tactic.TryThis.addExactSuggestion

[Scott Morrison]

I agree it is a little strange given the "Try this:" output never says apply. I would prefer apply? over exact?, but only mildly. (And perhaps only because I already know too much about how it works internally -- try applying everything, then clean up the mess if possible.) In favor of apply is that everyone knows that it is the basic "backwards reasoning tactic", not necessarily a finishing tactic. That is, while exact is only for finishing, and refine is not for finishing, apply can be either.

[Floris van Doorn]

One disadvantage with the apply? approach is that we already use ? like this for "execute this command, but show more information what you did" (like simp?/tidy?/@[simps?]/@[to_additive?]/...) and this is a very different use.

[Damiano Testa]

An option for the name could be close?, with the ambiguity of "closing the goal/are we close to the end".

[Ruben Van de Velde]

Could call it "finish"

[Ruben Van de Velde]

Or "omega"

[Mario Carneiro]

those are both tactics already, with significantly different behaviors

[Mario Carneiro]

TBH naming a tactic as essentially "thing that closes the goal" is a terribly vague description

[Thomas Murrills]

Floris van Doorn said:

One disadvantage with the apply? approach is that we already use ? like this for "execute this command, but show more information what you did" (like simp?/tidy?/@[simps?]/@[to_additive?]/...) and this is a very different use.

I think “show me how to do this” and “show me what you’re doing when you do this” are sufficiently close notions (since the latter is essentially still “show me how to do this”, just with the fact that it also gets done) such that these both are what you’d intuitively expect ? to mean given the context.

And, crucially, they’re in complementary settings, so that ? always means the only thing it intuitively could. That is, I don’t think it’s possible for these uses to overlap—you’ll never want to see more information on what happens and see how to replace an incomplete command.

[Thomas Murrills]

I think that either way, we need a standard way to tell lean “show me how to do this”/“try completing this yourself”; I think e.g. rw? and have? are so much better than rewrites and propose because of their closer relationship to existing names and intuitive meaning.

(I don’t think I’d guess that nounifying and pluralizing an imperative verb would get me a search; besides, rewrites looks like a present tense indicative verb, which introduces a little friction.)

Another option could be rw..., I guess? rw? seems the most natural to me, though, and what I would expect given that the user is asking a question of lean.

[Yaël Dillies]

I would advise against rw? specifically because there has been this idea going round of a tactic that finds possible things to rewrite in the goal, and this not yet existing tactic would most naturally be called rw?.

[Thomas Murrills]

Wait, what’s the difference between that and rewrites?

[Thomas Murrills]

(Also if it’s not clear I’m talking about rw? as a renaming of rewrites just as an example; library_search would presumably turn into an analogous modification of apply or exact)

[Yaël Dillies]

Ahah that tactic was already implemented! Can you tell I'm not following? :grinning_face_with_smiling_eyes:

[Jon Eugster]

rw?, have?, and apply? as a combo do look really intuitive!
(as long as they really do stuff one could achieve with the corresponding tactics if one knew the correct lemmas to use)

that being said, for me apply and refine are also really close, I dont think it would be confusing if apply? suggests a refine term

[Eric Wieser]

I think if we make apply? an alias for library_search, we should do the same thing for refine?

[Eric Wieser]

We could keep exact? for "library search but no side goals allowed"

[Eric Wieser]

(which I think was what library_search always meant in lean 3, but I get the feeling it no longer does in Lean 4?)

[Patrick Massot]

Yes, the Lean 3 version was a exact? and the refine? one was called suggest. They got merged in Lean 4.

[Eric Wieser]

note there is now a PR at !4#4885

[Eric Wieser]

Patrick Massot said:

Yes, the Lean 3 version was a exact? and the refine? one was called suggest. They got merged in Lean 4.

Do you have an example in mind where the refine? one works? The web editor seems to just crash for me.

[Eric Wieser]

Should we change the name of the import from Mathlib.Tactic.LibrarySearch now that that's not the preferred name of the tactic?
Weirdly Mathlib.Tactic.Apply?is valid to Lean, but the filename it searches for is illegal on windows.

[Mario Carneiro]

I could have sworn that issue has already been tackled in at least one other tactic... there is SimpTrace.lean which supplies the simp? tactic

[Mario Carneiro]

but maybe ApplyTrace.lean doesn't work in this case because it is using ? very liberally

[Sebastian Ullrich]

Perhaps you were thinking of Tactic.Clear!? (I remember because it broke the Nix setup)

[Mario Carneiro]

I suppose that's an example of not solving the problem, and also probably my recollection

[Mario Carneiro]

I think we should just rename it, it's nice if lean can handle such files but for a project naming convention I would be inclined to stick to a very restricted character set for file names because of the myriad other ways files get processed

[Scott Morrison]

Notice that not only did I leave the file names the same, I left the "plumbing" version of the tactics with their original names as well.