library_search fails to find theorem

Stream: mathlib4

[Dan Velleman]

Here's a simple proof:

example (a b c : Nat) (h : a + b = a + c) : b = c := Nat.add_left_cancel h

Now suppose we ask library_search to help with this example:

example (a b c : Nat) (h : a + b = a + c) : b = c := by library_search

library_search doesn't come up with the theorem Nat.add_left_cancel. Shouldn't it find it?

[Dan Velleman]

By the way: I'm using leanprover/lean4:nightly-2023-04-20.

[Alex J. Best]

import Std.Data.Nat.Basic
import Std.Data.Nat.Lemmas
import Mathlib.Tactic.LibrarySearch

example (a b c : Nat) (h : a + b = a + c) : b = c := by library_search

works ok on the Lean 4 web editor https://lean.math.hhu.de, maybe you just need to update to a newer mathlib? (library search has seen some improvements recently)

[Oliver Nash]

I'm mostly loving our new fast exact? library search but occasionally I'm surprised by failures. For example, shouldn't this work:

import Mathlib

example {n : ℕ} : n = 0 ∨ 0 < n := by exact? -- Fails to find `eq_zero_or_pos`

[David Renshaw]

That's a consequence of this line in isInternal': https://github.com/leanprover-community/mathlib4/blob/a1451be4b1cafd4d5e780a690b9e26c8891d3220/Mathlib/Lean/Expr/Basic.lean#L97

[Eric Wieser]

Is there an issue open about that?

[Oliver Nash]

I just added a comment here: https://github.com/leanprover-community/mathlib4/issues/3426#issuecomment-1644226610

[Eric Wieser]

Oh, I meant an issue against lean4, since that seems like a pretty odd thing to declare internal

[Oliver Nash]

I don't really know what the concept of being "internal" means so I'm not sure what the issue should be. Should it be "Add API to detect if something is internal"?

[David Renshaw]

This pull request is related: https://github.com/leanprover/lean4/pull/2112

[David Renshaw]

and the one it links to: https://github.com/leanprover-community/mathlib4/pull/2349

[Alex J. Best]

Eric Wieser said:

Oh, I meant an issue against lean4, since that seems like a pretty odd thing to declare internal

isInternal' is in mathlib though

[Alex J. Best]

I'm actually not sure what that part of isInternal' is guarding against, I can see declarations with names like _eq_n in mathlib, but none without the leading underscore, perhaps it can just be deleted. Thoughts @Floris van Doorn ?

[Alex J. Best]

I just looked into it a bit more, looks like core lean switched from eq_n to _eq_n in https://github.com/leanprover/lean4/commit/4d1343d67005749367a08d2964a1dfb0bf09d3dd so I think we are safe to remove the eq_n check from isInternal' as it is now covered by isInternal. I made #6036 to change this