Reversing semantics of `library_search`

Stream: general

[Scott Morrison]

Currently library_search only unfolds reducible definitions when trying to apply lemmas (or local facts), while library_search! uses the default behaviour of apply, that is, it will look through normal definitions.

[Scott Morrison]

The reason for this is that often you're looking for a suitable rewriting lemma, and being told rfl isn't very helpful.

[Scott Morrison]

Also, with the default behaviour of apply you're more likely to get "weird" answers...

[Scott Morrison]

However library_search is definitely weaker than library_search!, if all you want is an answer.

[Scott Morrison]

I am tempted to reverse the semantics, and have library_search be the "by all any means necessary" tactic, and library_search! be the more refined option.

[Scott Morrison]

In my experience from last week, beginners want the brute force option, while experts want the subtler one, so we should make the experts work harder to get what they want.

[Johan Commelin]

Makes sense to me..., except that ! seems to a mnemonic for "apply more force". How about '? Or is that too generic a suffix?

[Floris van Doorn]

It seems reasonable to make the current library_search! the default one.
As Johan said, I don't think library_search! is a good name for the current library_search. We could just use a different name, like quick_search? Or if we want the same name, maybe library_search-?

[Johan Commelin]

library_search♭ — the joys of unicode

[Kevin Buzzard]

We could have set_option old_library_search true

[Kevin Buzzard]

That seemed to work well for structures :P

[Mario Carneiro]

I think that matches that abuse defeq should be discouraged to newcomers

[Mario Carneiro]

for the exact reason that they shouldn't need to know the defeqs to make sense of the lemma and why it works

[Mario Carneiro]

so I don't think that we should make library_search! the default. It could possibly be a fallback if the usual search fails

[Scott Morrison]

Yes --- Mario makes a good point too. I'm conflicted.

[Scott Morrison]

Regarding the "matches that abuse defeq should be discouraged to newcomers" --- if the _only_ match requires unfolding something semireducible, is it better to fail, or return that match?

[Scott Morrison]

That's the essential question I'm unsure of.

[Scott Morrison]

If we think it's better to return that match, there are three options:

1. swap the semantics
2. have library_search do two passes, the first time with current library_search behaviour, the second time with current library_search! behaviour
3. just do one pass, looking for lemmas that apply with standard apply settings. If one is found, try again with the same lemma, with apply { md := reducible }. If it matches with reducible, return that solution immediately. If it doesn't, stash this lemma away, and continue through the rest of the library. If the rest of the library fails, return the lemma that we found that works with standard apply settings.

[Scott Morrison]

All three options are bad:

1. we'll be returning many more up-to-defeq solutions, like we did until a month ago
2. it will take twice as long to run anytime it fails
3. it involves a substantial rewrite :-)

[Johan Commelin]

@Scott Olson I'm sure that you realise that the badness of (3) is categorically different from the badness in (1) and (2).
But of course I understand your point completely. :wink:

[Johan Commelin]

So, let's at least not forget about (3), even if we don't choose it immediately. It might be a good limit point that we want to converge to.

[Floris van Doorn]

I think you meant to ping a different Scott?

[Johan Commelin]

@Scott Morrison :up:
Scott Olson: Oops, sorry for the bad ping.