function expected: @ι' (φ j)

Stream: general

[Richard Copley]

What's happening to cause this confusing message from exact??

import Mathlib.Logic.Basic
import Mathlib.Data.ZMod.Basic
import Mathlib.Topology.UniformSpace.Pi

-- or: "import Mathlib"

theorem xxx {p : Prop} (h : ¬¬p) : p := by
  exact?
-- function expected
--   @ι' (φ j)

When one has forgotten what of_not_not is called, this is sad, but at least the message makes sense; just one of life's little disappointments:

import Mathlib.Logic.Basic

theorem xxx {p : Prop} (h : ¬¬p) : p := by
  exact?
-- `exact?` could not close the goal. Try `apply?` to see partial suggestions.

[Damiano Testa]

With the online server, both give the error message

-- `exact?` could not close the goal. Try `apply?` to see partial suggestions.

[Damiano Testa]

Note that you can get an actual suggestion with the iff version and no imports!

theorem xxx {p : Prop} : ¬¬p ↔ p := by
  exact?  -- `Try this: exact Classical.not_not`

[Richard Copley]

Damiano Testa said:

With the online server, both give the error message
-- `exact?` could not close the goal. Try `apply?` to see partial suggestions.

So they do, thanks! This was fixed 12 days ago with the merger of #10644, I think.

[Yury G. Kudryashov]

Why did this pr affect exact??

[Joe Hendrix]

This bug was subtle, but was fixed in lean4#3610. It should be fixed by updating to Lean v4.7.0-rc2 (or later).

[Joe Hendrix]

What was happening was library search when converted to lazy discriminator trees had a bug where different free variables were assigned the same name. They didn't appear in the same local context, but I wasn't clearing some caches when swapping out the local context so the cache contained invalid data.

It was pretty tricky to actually trigger the bug though as it required very specific confusion and caching was only shared across a few modules when library search built the initial lazy discrimination tree. I suspect the changes in that PR happened to change code in a way that re-hid the underlying initialization bug.

[Yury G. Kudryashov]

Thank you for the explanation.