Zulip Chat Archive

Stream: general

Topic: Reversing semantics of `library_search`


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 20 2020 at 13:19):

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

view this post on Zulip Scott Morrison (Jul 20 2020 at 13:19):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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-?

view this post on Zulip Johan Commelin (Jul 20 2020 at 16:49):

library_search♭ — the joys of unicode

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 16:52):

We could have set_option old_library_search true

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 16:52):

That seemed to work well for structures :P

view this post on Zulip Mario Carneiro (Jul 20 2020 at 21:00):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 21 2020 at 00:57):

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

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Jul 21 2020 at 00:58):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 21 2020 at 01:02):

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 :-)

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Jul 21 2020 at 04:51):

I think you meant to ping a different Scott?

view this post on Zulip 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