library_search timeout

Stream: new members

[Alex Zhang]

What does it mean when I use library_search or library_search! I get the error message timeout? (not really sure if I have ever got a timeout when using the first)
In particular, what is the difference between timeout and failed when doing such search?

[Kevin Buzzard]

Can you post a reproducible MWE?

[Alex Zhang]

I don't have one for "failed" and one for "timeout" at hand. I will post here if I get them.

[Kevin Buzzard]

Failed I've seen a lot, I think this means "I can't find it". But timeout sounds like it might be a bug, not sure

[Alex Zhang]

example (k x y: α) [ring α] : (k • x) * y = k • (x * y) :=
begin
  library_search
end

This example gives a timeout.

[Huỳnh Trần Khanh]

Not reproducible. It doesn't timeout for me :stuck_out_tongue: Screenshot-from-2021-06-28-17.19.21.png

[Kevin Buzzard]

What are the imports? #mwe

[Kevin Buzzard]

import tactic

variable (α : Type)

example (k x y: α) [ring α] : (k • x) * y = k • (x * y) :=
begin
  library_search -- Try this: exact smul_mul_assoc k x y
end

[Alex Zhang]

Thanks! It is a little weird. It does not time out for me now either (maybe because I changed something in the file before this).

[Eric Rodriguez]

I mean, anecdotally I've also had it time out, but I just take that to mean library_search won't find it

[Alex Zhang]

If I change the code to

import tactic

variable (α : Type)
variable [has_mul α]

example (k x y: α) [ring α] : (k • x) * y = k • (x * y) :=
begin
  library_search
end

the search will fail.
Why could this happen?

[Alex Zhang]

exact smul_mul_assoc k x y, will also fail.

[Kevin Buzzard]

That code above gives alpha two multiplcations and no proof that they're the same, so probably the example isn't even true.

[Kevin Buzzard]

Playing around with the infoview in this state:

α : Type
_inst_1 : has_mul α
k x y: α
_inst_2 : ring α
⊢ k • x * y = k • (x * y)

seems to indicate that both the smul and the mul are coming from _inst_1 rather than _inst_2 so the reason you can't close the goal is that the _inst_1 mul isn't known to be associative.

[Alex Zhang]

I thought [ring \a] just extends [has_mul \a].

[Kevin Buzzard]

And the fact that it extends it means exactly that you shouldn't put it in again.

[Yakov Pechersky]

Ring uses old_structure_cmd iirc so it provides all the fields separately, including the data, so Kevin's point stands.

[Alex Zhang]

Yes.
If I declared [has_mul a] or [ring a] before. But later I want a to be a ring or a field. Is there a way that does extend a previous declaration?

[Alex J. Best]

Not really, just put the earlier stuff in a section

section ring_stuff
variables {a : Type*} [ring a]
lemma a_lemma_about_rings := ...
end ring_stuff
section field_stuff
variables {a : Type*} [field a]
lemma a_lemma_about_fields := ...
end field_stuff

[Alex Zhang]

I am proving

example :(A ⊗ B)⁻¹ = A⁻¹ ⊗ B⁻¹ :=
begin
  suffices : (A⁻¹ ⊗ B⁻¹) ⬝ (A ⊗ B) = 1,
  library_search!,
  --apply inv_eq_left_inv this,
end

The quoted-out line will close the next goal, but if I use library search, it will time out.
I am wondering why library_search fails to work.

[Eric Wieser]

Can you give a #mwe with imports and variables?

[Eric Wieser]

The time taken by library_search greatly depends on how many things you've imported

[Eric Wieser]

Since it only searches imported files

[Alex Zhang]

inv_eq_left_inv is a lemma defined in my current file.

[Alex Zhang]

I will try to extract a #mwe

[Alex Zhang]

OK..Well...lib search even doesn't work for example (h : A ⬝ B = 1) : B = A⁻¹ :=, but it works for example (h : A ⬝ B = 1) : A⁻¹ = B :=

[Eric Wieser]

Again, without the precise types of A and B there's very little chance anyone will be able to help you

[Kevin Buzzard]

Learn how to ask good questions Alex.

[Kevin Buzzard]

It might be a bore but you'll develop some techniques which will eventually enable you to answer some of your own questions by yourself, when writing the mwe reveals the issue (this happens)

[Alex Zhang]

Why does library search fail for the first example?

import tactic
example (a: ℤ) : a * int.one = a := by library_search
example (a: ℤ) : a * int.one = a := mul_one a

[Kevin Buzzard]

because library_search works up to syntactic equality and mul_one a doesn't say syntactically what the example says (it just says it definitionally, which is why the proof works)

[Alex J. Best]

Does by library_search! work?

[Alex Zhang]

@Alex J. Best Yes, that does work!

[Alex Zhang]

Is library_search! always at least powerful as (i.e. more powerful than) library_search?

[Alex J. Best]

Kindof, it searches including definitionally equal things, which means it takes longer. In practice I've found that it can sometimes time out when the normal library search doesn't so I normally run the regular library search then if that fails try adding the !.