library_search timeout

Stream: mathlib4

[Heather Macbeth]

@Scott Morrison Any thoughts on why library_search is timing out here? I tried it on master as well as on !4#3771 and !4#3725.

import Mathlib.Data.Real.ENNReal
import Mathlib.Tactic.LibrarySearch

open ENNReal

-- works
example {a b c d : ℝ≥0∞} (ac : a < c) (bd : b < d) : a * b < c * d := ENNReal.mul_lt_mul ac bd

-- times out
example {a b c d : ℝ≥0∞} (ac : a < c) (bd : b < d) : a * b < c * d := by library_search

[Scott Morrison]

set_option trace.Tactic.librarySearch.lemmas true in reveals two things:

1. There are a long list of lemmas to try here. This is because the way DiscrTree works, there's not really a good way to look up "lemmas that prove _ < _ in ℝ≥0∞". So we just have to try out every lemma that proves a strict inequality. If you add set_option maxHeartbeats 0 it does succeed on this example.
2. The lemma we're after comes last in that list of lemmas! I'm a bit surprised !4#3725 doesn't help here. I wonder if just reversing the list of lemmas would be a good idea, on the principle that later defined lemmas are more likely to be more specific?

[Heather Macbeth]

Interesting ... your idea in (2) does seem plausible.

[Heather Macbeth]

Do you know if the mathlib3 implementation did this, intentionally or not?

[Scott Morrison]

I have a great fix in !4#3725 now. It turns out that the lemmas that come back from DiscrTree.getMatch come in batches, coming from different parts of the discrimination tree. Looking at some typical results, it looks like more specific results tend to come after less specific ones.

That is the opposite of what we want to do in library_search, where the most specific lemmas are the most useful.

Hence in !4#3725 I have just added a .reverse, and at the same time when I put the lemmas into the discrimination tree I sort them by longest first.

This has the net result that we try the most specific lemmas (according to the discrimination tree) first, and amongst those we try the ones with the shortest names first.

In your example, this means that ENNReal.mul_lt_mul is actually the very first lemma tried, and so library_search finishes essentially instantly.

[Scott Morrison]

!4#3771 should probably be merged first. It is a pretty simple change, that improves performance but shouldn't change behaviour, so hopefully someone can merge that soon. :-)

[Scott Morrison]

Patrick merged !4#3771, and I've updated !4#3725 to master, so it is ready for review/merge too.