library_search regression

Stream: mathlib4

[Patrick Massot]

@Scott Morrison In Lean 3, if I type

import topology.instances.real
import topology.algebra.order.compact

example (f : ℝ → ℝ) {K : set ℝ} (hK: is_compact K) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y :=
begin
  suggest,
  sorry
end

then among many stupid suggestions, I get the very relevant

Try this: refine hK.exists_forall_le _ _

(and by the way suggest using hK returns nothing, but I guess we don't want to fix this at this point). In Lean 4 if I type

import Mathlib.Topology.Instances.Real
import Mathlib.Topology.Algebra.Order.Compact
import Mathlib.Tactic.LibrarySearch

example (f : ℝ → ℝ) {K : Set ℝ} (hK: IsCompact K) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y := by
  library_search

the best it comes up with is

refine IsCompact.exists_forall_le ?_ ?_ ?_

which fails to use assumption hK. Is this a known regression? Note that writing library_search using hK doesn't change anything.

[Patrick Massot]

By the way, trying to continue the same proof (skipping the hopeless side condition), we get to

import Mathlib.Topology.Instances.Real
import Mathlib.Topology.Algebra.Order.Compact
import Mathlib.Tactic.LibrarySearch

example (f : ℝ → ℝ) {K : Set ℝ} (hK: IsCompact K) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y := by
  refine hK.exists_forall_le ?_ ?_
  sorry
  library_search

which very weirdly suggests refine Continuous.continuousOn (False.elim ?_) instead of refine Continuous.continuousOn ?_.

[Scott Morrison]

Ah yes, this is a known issue. The suggest mode of library_search in
mathlib4 has never received much love. The key difference is that in
mathlib3 if we tried a lemma, it applied, but we could not close all
subgoals using solve_by_elim, we would try again with solve_by_elim
closing whatever subset of the subgoals could be closed "safely" (ie
subsingletons). In mathlib4 we have never implemented this second step.
This is what would replace one of the ?_s with hK.

I agree we should fix this!

We could even reorder the results automatically so that partial results
which used more of the local hypotheses (or have fewer unsolved subgoals,
or some combination), score higher.

[Patrick Massot]

It would be nice to fix this especially for propaganda talks purposes. My standard talk example in Lean 3 is a proof where suggest is especially useful.

[Heather Macbeth]

Another library_search failure, posting in the same thread as Patrick's because it seems similar:

import Mathlib.Data.Quot
import Mathlib.Tactic.LibrarySearch

variable {r : α → α → Prop}

example : Function.Surjective (Quot.mk r) := by library_search -- fails

example : Function.Surjective (Quot.mk r) := surjective_quot_mk r -- should find this

[Heather Macbeth]

It works in Lean 3:

import data.quot
import tactic.suggest

variables {α : Type} {r : α → α → Prop}

example : function.surjective (quot.mk r) := by library_search
-- finds `exact surjective_quot_mk r`

[Scott Morrison]

@Heather Macbeth, !4#3724.

[Scott Morrison]

(The bug was using forallMetaTelescopeReducing, rather than just forallMetaTelescope, when indexing lemmas for the discrimination tree. This meant we were blasting through the Function.Surjective and seeing an Exists conclusion, and hence mis-indexing the lemma. This probably affected a great many results!)

[Scott Morrison]

@Patrick Massot, after !4#3743, on your example:

import Mathlib.Topology.Instances.Real
import Mathlib.Topology.Algebra.Order.Compact
import Mathlib.Tactic.LibrarySearch

example (f : ℝ → ℝ) {K : Set ℝ} (hK: IsCompact K) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y := by
  library_search

we have:

• refine IsCompact.exists_forall_le hK ?_ ?_ as one of the suggested solutions
• in fact, as the first solution (on the basis that it uses more local hypotheses than alternatives)
• none of the spurious results which use False.elim ?_
• and better display of the result, with hints:

refine IsCompact.exists_forall_le hK ?_ ?_
-- Remaining subgoals:
-- ⊢ Set.Nonempty K
-- ⊢ ContinuousOn (fun x ↦ f x) K

[Patrick Massot]

Amazing, thanks!