Zulip Chat Archive

I have a question regarding the library_search function. In particular on how we can use it to proof small modifications to known lemmas. For example, I would like to know why library_search does not understand the following example

example (p q : Prop) : (p ∧ (p → q)) → (p → q) :=
begin
assume hyp,
by library_search
end

Whereas a simple

by exact hyp.right

does the trick, and that seems like " applying a single lemma" to me.

Hope the question is clear and anyone can give me a clue on how to understand this type of behaviour!

Arthur Paulino (Mar 30 2022 at 11:38):

I think this is a current blind spot of library_search, not being able to explore right or left attributes of certain terms

Alex J. Best (Mar 30 2022 at 12:02):

Actually I think this is the apply vs apply' bug. At least library search tries and.right but fails to unify.
Just trying apply and.right also fails, but apply' and.right works.
I think this was discussed previously https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/library_search.20failures/near/254188601 but I'll try and see what the concequences of changing library_search to use apply' instead are

Reid Barton (Mar 30 2022 at 12:11):

Maybe the smallest possible example of the apply bug? Usually it occurs with typeclasses involved!

Kevin Buzzard (Mar 30 2022 at 13:06):

Should this then be added to the issue?

Alex J. Best (Mar 30 2022 at 13:07):

Which issue?

Kevin Buzzard (Mar 30 2022 at 13:08):

I'm assuming there is an apply bug issue?

Reid Barton (Mar 30 2022 at 14:14):

I thought there was one but I can't find it

Julian Berman (Mar 30 2022 at 14:54):

https://github.com/leanprover-community/mathlib/issues/2394 and the issue it links seem related but doesn't seem to mention apply specifically

Alex J. Best (Mar 30 2022 at 16:50):

https://github.com/leanprover-community/mathlib/runs/5755739008?check_suite_focus=true now fails a test as

import order.filter.basic

open filter

/- Turn off trace messages so they don't pollute the test build: -/
-- set_option trace.silence_library_search true
set_option trace.suggest true

example {α β γ : Type*} {A : filter α} {B : filter β} {C : filter γ} {f : α → β} {g : β → γ}
  (hf : tendsto f A B) (hg : tendsto g B C) : tendsto (g ∘ f) A C :=
calc
map (g ∘ f) A = map g (map f A) : by library_search
          ... ≤ map g B         : by {apply' supr_le_iff.mp, }
          ... ≤ C               : by library_search!

leaves metavariables in the goal, unfortunately

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib