apply? not giving obvious short outputs

Stream: mathlib4

[Bolton Bailey]

In the file below, I want to use apply to find the name of the lemma IsClosed.union/see if it exists. In fact this lemma does exist, and works perfectly, and intuitively it feels like the first thing I should try in this situation.

import Mathlib

example (a b : Set ℝ) : IsClosed (a ∪ b) := by
  apply?
  -- apply IsClosed.union

How should I think about the way apply? chooses to order its outputs?

(Edited to be more minimal, the lemma shows up now, but not as the first option)

[Martin Dvořák]

Afaik ordering of the outputs of apply? is a very hard problem that we haven't tackled yet.

[Kim Morrison]

Well, rather I would say we have tackled it, and despite a lot of thought going into it (by both me and Joe Hendrix when preparing std_exact?) the results still leave a lot to be desired. It's not for lack of trying. :-)

[Vasily Ilin]

@Kim Morrison , After 5 minutes of searching I was unable to locate the source code for apply?. Would you mind pointing to it? I want to see what is the current ordering. From personal experience, apply? often favors low-level statements as opposed to high-level API, which is counter-intuitive to me. For example, when working with Reals, it usually suggests things about Cauchy sequences.

I also wonder if either of the following two orderings has been tried?

1. Order lemmas by frequency of use in mathlib, the more frequent the higher. This requires ~10Mb memory to store a table of frequencies.
2. Order by the number of dependencies to surface high-level API first. More dependencies = higher level. Also ~10Mb of memory to store.

[Damiano Testa]

I tried to Ctrl-Click on apply? and it took me to docs#Lean.Elab.LibrarySearch.evalApply. The implementation appears to be the one of exact?, with a flag set to false.

[Kevin Buzzard]

And then you ctrl-click on exact? and repeat until you're happy.

[Vasily Ilin]

Kevin Buzzard said:

And then you ctrl-click on exact? and repeat until you're happy.

I don't understand what you mean. How to find the implementation of apply??

[Kevin Buzzard]

example : False := by
  apply? -- wait for orange bars to go away and then ctrl-click on `apply?`
         -- or command-click on a mac

In general, whenever you have compiling code, you can ctrl-click on anything and jump to its definition.

[Vasily Ilin]

It takes me to https://github.com/leanprover/lean4/blob/744f98064b056ee27fc8c97f524797c8cc96f436/src/Lean/Elab/Tactic/LibrarySearch.lean#L20-L55
This is the implementation of exact?, not apply?.

[Chris Henson]

As has been explained above, this single function is used for both apply? and exact?. Look at the rest of the file, immediately below.

[Kevin Buzzard]

It takes me to this code

@[builtin_tactic Lean.Parser.Tactic.apply?]
def evalApply : Tactic := fun stx => do
  let `(tactic| apply? $[using $[$required],*]?) := stx
        | throwUnsupportedSyntax
  exact? (← getRef) required false

which is exactly the definition of apply?, you can see let `(tactic| apply? ... in the definition, and it's defined to be exact? ... required false. Now looking at the definition of exact? you can see it takes an input (requireClose : Bool) and so apply? is "exact? but don't require to close the goal".

[Vasily Ilin]

Okay, I see now, thank you