library_search getting tired

Stream: mathlib4

[Patrick Massot]

I've been using mathlib4 a bit recently ("using" being opposed to "porting") and I noticed that library_search gets tired after a couple of invocation. When it's tired it immediately gives up instead of searching. Reloading the file (say by using "Refresh file dependency") reboots library_search which then works normally for a while.

[Patrick Massot]

This is in projects depending on mathlib4, not mathlib4 itself, in case this matters.

[Scott Morrison]

Hmm... library_search now does play some clever tricks to try to stop if maxHeartbeats is approaching, and this is surely where the suspicion should lie. If you have a file where this somewhat reliably happens I could try disabling the maxHeartbeats check.

[Patrick Massot]

Of course now that I posted this message I can't get this bug to appear.

[Patrick Massot]

I still have something weird to show. In

import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Topology.UniformSpace.Compact

import Mathlib.Tactic.LibrarySearch

notation "d" => dist
attribute [aesop (rule_sets [Continuous]) apply unsafe] Continuous.continuousOn

macro "ls" : tactic => `(tactic| library_search)

theorem Heine_Cantor [MetricSpace X] [MetricSpace Y] [CompactSpace X]
    {f : X → Y} (hf : Continuous f) : UniformContinuous f := by
  rw [Metric.uniformContinuous_iff]
  intros ε ε_pos
  set K := { p : X × X | ε ≤ d (f p.1) (f p.2) }
  have K_closed : IsClosed K := by
    apply isClosed_le
    continuity
    continuity
  have K_cpct : IsCompact K := by exact IsClosed.isCompact K_closed
  cases' K.eq_empty_or_nonempty with h h
  · use 1, zero_lt_one
    intros x y _
    have : (x, y) ∉ K
    · simp [h]
    simpa using this
  obtain ⟨p, p_in, H⟩ : ∃ p ∈ K, ∀ q : X × X, q ∈ K → d p.1 p.2 ≤ d q.1 q.2
  · apply K_cpct.exists_forall_le h
    continuity
  use d p.1 p.2
  constructor
  · simp
    intro eq
    apply lt_irrefl ε
    calc
      ε ≤ 0 := by simpa [eq] using p_in
      _ < ε := ε_pos
  · intros x x'
    contrapose!
    aesop

replacing line 28, the one saying apply K_cpct.exists_forall_le h by library_search and accepting the suggestion leads to a weird error.

[Patrick Massot]

This is on current mathlib4 master c39117e4de1eff79d24b7512e26aff0f0b5ade4b

[Dan Velleman]

I have experienced this problem as well.

[Patrick Massot]

It seems that library_search takes the initiative to name the hole to be filled and this name clashes with an existing name and confuses Lean.

[Patrick Massot]

Fun fact in passing: accepting this suggestion also raises a deprecation warning which does not show up in the hand-written version because dot notation seems to turn off deprecation warnings.

[Mario Carneiro]

Patrick Massot said:

It seems that library_search takes the initiative to name the hole to be filled and this name clashes with an existing name and confuses Lean.

This is actually a bug in apply IIRC

[Kevin Buzzard]

I was missing the apply bug :-)

[Patrick Massot]

In this case it's also a refine bug.

[Mario Carneiro]

What is the exact suggestion?

[Patrick Massot]

refine IsCompact.exists_forall_le K_cpct h ?hf

[Patrick Massot]

And hf is already the name of a local assumption.

[Mario Carneiro]

That's by design, although it is a somewhat dubious design

[Mario Carneiro]

The issue is that named metavariables are not really scoped in any meaningful sense, so you can end up picking up completely unrelated mvars which happen to have the same name

[Mario Carneiro]

sometimes even mvars you never wrote but were generated internally - this is what apply does

[Mario Carneiro]

have you identified who created the ?hf mvar?

[Mario Carneiro]

if you write let := ?hf you might recognize the proof term

[Patrick Massot]

This named is made up by library_search

[Mario Carneiro]

no, I mean the first ?hf in the proof

[Mario Carneiro]

if you try writing let := ?hf you might be surprised to see the result

[Patrick Massot]

The first hf is an assumption from the statement of the theorem.

[Mario Carneiro]

not hf, ?hf

[Mario Carneiro]

mvars have a separate namespace, they are unrelated to local variables with the same name

[Mario Carneiro]

although apply and other tactics have a penchant for naming mvars after the local variables they will substitute for

[Patrick Massot]

No idea. It don't see it anywhere.

[Mario Carneiro]

and what does let := ?hf do to the tactic state?

[Patrick Massot]

I'll be back later, I need to be in Cambridge for a while.

[Mario Carneiro]

just got to a lean to test this out myself. let := ?hf is a syntax error but let foo := ?hf puts

foo: Continuous fun b ↦ ε := continuous_const

in the context

[Mario Carneiro]

by moving the line around it appears that this ?hf variable appears due to the first continuity in

  have K_closed : IsClosed K := by
    apply isClosed_le
    continuity
    continuity

[Mario Carneiro]

and indeed, you will notice that the case tag on this continuity goal is hf

[Mario Carneiro]

created by the apply on the previous line

[Mario Carneiro]

Oh, this is fun:

def foo (x y : Nat) : Nat := x + y

def bla : Nat := by
  apply foo
  exact ?x

crashes the server

[Mario Carneiro]

another brainteaser: Why does

def foo (x y : Nat) : Nat := x + y

#eval show Nat from
  (let a : Nat := by
      apply foo
      exact 0
      exact 10
    by exact ?x) +
  (let b : Nat := by
      apply foo
      exact 2
      exact 30
    by exact ?x)

print 4?

[Kevin Buzzard]

Because it's 2+2, with the 2 being the exact 2, which was the value of ?x when it was assigned in both cases I guess (although I don't understand elaboration order at all)

[Mario Carneiro]

Yet

#eval show Nat from
  (by
    let a : Nat := by
      apply foo
      exact 0
      exact 1
    exact ?x) +
  (let b : Nat := by
      apply foo
      exact 2
      exact 3
    by exact ?x)

is 0, and

#eval show Nat × Nat from
  (
    let a : Nat := by
      apply foo
      exact 0
      exact 1
    by exact ?x
  ,
    let b : Nat := by
      apply foo
      exact 2
      exact 3
    by exact ?x
  )

is (0, 2)

[Patrick Massot]

Very interesting...