library_search failures

Stream: general

[Marc Masdeu]

Hi,
I'd like to know why library_search fails in the example below:

import data.real.ereal
import order.complete_lattice
open set

noncomputable theory

example {α : set ereal} {x : ℝ} (h : (x : ereal) ∈ α) :
  (x : ereal) ≤ Sup α :=
begin
  --library_search, -- fails
  exact le_Sup h, -- works like a charm
end

This is related to a small PR that @Eric Wieser is reviewing about adding a bit of api to ereal's. (#9313)

[Eric Wieser]

Yeah, this surprises me too. It fails even without the coercions:

example {s : set ereal} {x : ereal} (h : x ∈ s) : x ≤ Sup s :=
by library_search

yet this works

example {α : Type*} [complete_linear_order α] {s : set α} {x : α} (h : x ∈ s) : x ≤ Sup s :=
by library_search

[Marc Masdeu]

Adding
haveI : complete_linear_order ereal := ereal.complete_linear_order,
doesn't help either. How would one debug this?

[Scott Morrison]

First, check library_seach!. (No luck.)

[Scott Morrison]

Second, try set_option trace.suggest true to see which lemmas it is trying.

[Scott Morrison]

Sure enough, le_Sup is on the list, but it is not successfully using it.

[Scott Morrison]

Look further down the huge trace output, to see what it says when it tries le_Sup, only to be disappointed that it just says:
Trying to apply lemma: le_Sup.{?_mlocal._fresh.23.109287}.

[Scott Morrison]

Simulate by hand the step that library_search should hopefully be trying with this lemma:

(do e ← tactic.to_expr ``(le_Sup), tactic.suggest.apply_and_solve tt {} e),

getting the error message:

invalid apply tactic, failed to unify
  ↑x ≤ Sup α
with
  ?m_2 ∈ ?m_3 → ?m_2 ≤ Sup ?m_3

[Scott Morrison]

(Wonder if a closer approximation to library_searchs inner workings is:
(do e ← tactic.to_expr ``(@le_Sup), tactic.suggest.apply_and_solve tt {} e),...)

[Scott Morrison]

Wonder why that doesn't unify, so turn on set_option pp.all true, and get the more detailed:

invalid apply tactic, failed to unify
  @has_le.le.{0} ereal
    (@preorder.to_has_le.{0} ereal
       (@directed_order.to_preorder.{0} ereal
          (@linear_order.to_directed_order.{0} ereal
             (@conditionally_complete_linear_order.to_linear_order.{0} ereal
                (@conditionally_complete_linear_order_of_complete_linear_order.{0} ereal
                   ereal.complete_linear_order)))))
    (@coe.{1 1} real ereal (@coe_to_lift.{1 1} real ereal (@coe_base.{1 1} real ereal ereal.has_coe)) x)
    (@has_Sup.Sup.{0} ereal ereal.has_Sup α)
with
  ∀ {a : ?m_1},
    @has_mem.mem.{?l_2 ?l_2} ?m_1 (set.{?l_2} ?m_1) (@set.has_mem.{?l_2} ?m_1) a ?m_3 →
    @has_le.le.{?l_2} ?m_1
      (@preorder.to_has_le.{?l_2} ?m_1
         (@partial_order.to_preorder.{?l_2} ?m_1 (@complete_semilattice_Sup.to_partial_order.{?l_2} ?m_1 ?m_4)))
      a
      (@has_Sup.Sup.{?l_2} ?m_1 (@complete_semilattice_Sup.to_has_Sup.{?l_2} ?m_1 ?m_4) ?m_3)

[Scott Morrison]

Not be immediately sure whether to expect that unification to work or not, but realise that first of all we should check what
apply le_Sup does in this problem.

[Scott Morrison]

Discover that this fails! (Even though exact le_Sup h succeeds.)

[Scott Morrison]

At this point we've learnt that this has nothing to do with library_search itself.

[Scott Morrison]

(Or rather, we're asking too much of it if we expect it to work when apply fails.)

[Scott Morrison]

But I'm not immediately sure of the diagnosis from this point. To summarise, the real mystery is:

import data.real.ereal
import order.complete_lattice
open set

noncomputable theory

example {α : set ereal} {x : ℝ} (h : (x : ereal) ∈ α) :
  (x : ereal) ≤ Sup α :=
begin
  apply le_Sup,   -- fails
  exact le_Sup h, -- works like a charm
end

[Eric Rodriguez]

I remember someone had this on the discord with one of the extended number lines (I think it was nnreal and le_Refl. Something is definitely off about this all

[Yaël Dillies]

I personally had lots of pain with docs#bsupr_le and docs#le_binfi. You will be desolated to know they don't behave the same, because unification doesn't start with the same arguments (it goes from left to right and the supr is to the left of ≤ while infi is to its right).

[Yaël Dillies]

The problem is that Lean has a very hard time knowing which function should f i hi match.

[Marc Masdeu]

Wow @Scott Morrison , this is a great analysis (even if unsuccessful so far...). I'm more used to seeing apply work when exact doesn't, this is really weird. (But note that apply le_Sup h does indeed work!)

[Reid Barton]

This is the classic "apply bug". It occurs because a ≤ b is a Pi-type for ereal (src#with_top.preorder) but not in general, and then apply gets confused about how many _s to insert.

[Sebastien Gouezel]

Would it be reasonable to mark the order as irreducible on with_top?

[Eric Wieser]

I would guess that you don't want to mark the instance itself irreducible, and instead want

@[irreducible]
protected def with_top.le (o₁ o₂ : with_top α) : Prop := ∀ a ∈ o₂, ∃ b ∈ o₁, b ≤ a

and then use with_top.le to define the order instance.

[Eric Wieser]

By that argument presumably we need to do the same thing to docs#pi.preorder?

[Eric Wieser]

And docs#set.preorder, docs#finset.preorder, ...

[Eric Wieser]

Suggesting that maybe it's better to just stop apply getting confused in the first place

[Sebastien Gouezel]

It's not just apply: I really think that marking more things as irreducible can only help Lean, and that we should probably be doing this much more often. And yes, I meant doing it like you say, with an irreducible definition for with_top.le.

[Reid Barton]

It can also be turned into a structure as with docs#continuous (as @Sebastien Gouezel will no doubt recall...)

[Reid Barton]

Maybe it would be good to have a generic "identity" structure for Props for cases where the overhead of making a new one seems excessive

[Eric Wieser]

Reid Barton said:

Maybe it would be good to have a generic "identity" structure for Props for cases where the overhead of making a new one seems excessive

I suspect we'll want to tailor the name of the projection in each case; set.le will probably want the field to be called of_mem, pi.le perhaps wants .eval or similar, ...

[Reid Barton]

I guess I'm thinking more about examples like with_top.preorder where the specific definition is irrelevant (once you set up the basic lemmas), so it doesn't really matter if it is just called .out or whatever

[Reid Barton]

I mean, the ordering on with_top could just as well have been defined by cases. There's no reason that anyone would guess that it is a Pi type.

[Reid Barton]

set.le and pi.le should probably remain semireducible. At least for set.le, this is used all over the place.

[Reid Barton]

well I guess set.subset is the one whose definition is used all over the place, set.le isn't so common

[Eric Wieser]

If we don't change the reducibility of pi.le then we presumably still have the library_search failure on pi types

[Marc Masdeu]

I don't think I understand what the discussion was about at the end, but is anyone working on this? What kind of work would it entail? Could I contribute?

[Bolton Bailey]

Reusing this thread to complain about my own problem with library_search, mwe below. The thing causing library_search to fail here is apparently the fact that a higher-level file is being imported. It's not clear to me why library_search should time out anyway, since it's only used while coding, and shouldn't be pushed. It seems to me that this kind of problem will only get worse as more is added to mathlib, making timeouts more common and library_search harder to use.

import data.nat.totient -- library_search succeeds without this import
-- import data.finset.locally_finite -- the file with the lemma

open finset

lemma split_Ico {S : Type} [linear_order S] [locally_finite_order S] {a b c : S}
  (a_le_b : a ≤ b) (b_le_c : b ≤ c) :
  Ico a c = Ico a b ∪ Ico b c :=
begin
  library_search, -- (deterministic) timeout
  -- rw finset.Ico_union_Ico_eq_Ico a_le_b b_le_c,
end

[Kevin Buzzard]

This doesn't time out for me -- I might have some timeout figure set higher than you?

[Bolton Bailey]

I haven't done anything in particular to customize my timeout parameters.

[Kevin Buzzard]

yeah but I might have...

[Bolton Bailey]

I would propose the solution of simply finding whatever parameter is causing the timeout here and raising it, but I suspect it would raise the timeout parameter for all of mathlib, which I wouldn't want.

[Kevin Buzzard]

It's just some VS Code setting.

[Kevin Buzzard]

I ran the script to make all.lean and then if I import that, I get the excessive memory consumption error.

[Bolton Bailey]

Still, I don't want to change my VSCode settings, since then I might push some code and be surprised when CI tells me there's a timeout error.

[Kevin Buzzard]

In VS Code settings I have Lean: Time Limit set to 300000 on this machine

[Bolton Bailey]

Let me try that

[Bolton Bailey]

Yes, it works for me with the limit set to 300000. I guess I would suggest based on my experience that the default be changed, I think this is the second time where a higher timeout limit would have been helpful.

[Bolton Bailey]

Perhaps it wouldn't be too big of an issue to let CI operate have one value and the default VSCode parameter have another.

[Bryan Gin-ge Chen]

In fact, we changed the CI to match VSCode so that people wouldn't get confused as to why their code was failing in CI and not in VS Code (or vice versa).

[Bolton Bailey]

Ah, well, maybe it's not currently worth the hassle.

[Bolton Bailey]

Could not the mathlib repository itself override that setting though?

[Bolton Bailey]

What was the limit on the CI before it was changed?

[Bryan Gin-ge Chen]

I can't remember anymore, but it looks like we didn't have a limit at all: #2276

[Scott Morrison]

library_search is much faster in Lean 4, so I don't think this is worth worrying about.

[Gabriel Ebner]

library_search is much faster in Lean 4, so I don't think this is worth worrying about.

I think it should definitely possible to make it much faster than in Lean 3 (we have term indices and caches that persist between tactic invocations), but there's still some performance issues to iron out. Last time I tried it on the synported mathlib, it even timed out when indexing the lemmas. :-/

[Bolton Bailey]

Why is library_search failing here?

import data.rat.basic

example (q : ℚ) (hq : q ≠ 0) : q.num ≠ 0 := by library_search -- fails

example (q : ℚ) (hq : q ≠ 0) : q.num ≠ 0 :=
begin
  exact rat.num_ne_zero_of_ne_zero hq, -- goals accomplished
end

[Kyle Miller]

I don't know, but somehow this works:

example (q : ℚ) (hq : q ≠ 0) : ¬ q.num = 0 := by library_search -- succeeds

[Arthur Paulino]

I think I know how to solve this. @Bolton Bailey do you have other similar cases of failure? I can take a look when I get home.

[Bolton Bailey]

I literally just found it, did a double take, and posted it

[Arthur Paulino]

Done: #12616
This PR only changes two lines of code in the src/tactic/suggest.lean file. Other 7 lines are for tests.