## Stream: general

### Topic: Reversing semantics of library_search

#### Scott Morrison (Jul 20 2020 at 13:18):

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 (Jul 20 2020 at 13:19):

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 (Jul 20 2020 at 13:19):

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

#### Scott Morrison (Jul 20 2020 at 13:19):

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

#### Scott Morrison (Jul 20 2020 at 13:20):

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 (Jul 20 2020 at 13:21):

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 (Jul 20 2020 at 14:10):

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 (Jul 20 2020 at 16:47):

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 (Jul 20 2020 at 16:49):

library_search♭ — the joys of unicode

#### Kevin Buzzard (Jul 20 2020 at 16:52):

We could have set_option old_library_search true

#### Kevin Buzzard (Jul 20 2020 at 16:52):

That seemed to work well for structures :P

#### Mario Carneiro (Jul 20 2020 at 21:00):

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

#### Mario Carneiro (Jul 20 2020 at 21:01):

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 (Jul 20 2020 at 21:02):

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 (Jul 21 2020 at 00:57):

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

#### Scott Morrison (Jul 21 2020 at 00:58):

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 (Jul 21 2020 at 00:58):

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

#### Scott Morrison (Jul 21 2020 at 01:01):

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 (Jul 21 2020 at 01:02):

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 (Jul 21 2020 at 04:33):

@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 (Jul 21 2020 at 04:33):

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 (Jul 21 2020 at 04:51):

I think you meant to ping a different Scott?

#### Johan Commelin (Jul 21 2020 at 04:59):

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

Last updated: May 12 2021 at 04:19 UTC