'import all' sometimes still requires @[expose] when using grind

[cmlsharp]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Sometimes @[expose] is required even when using import all to import a module. Even more strangely, this behavior can be affected by function declaration order and whether you also public import that same module.

Consider the following example

Test/Foo.lean

module

public def increment? (i : Nat) (sz: Nat) : Option Nat :=
  if _ : i < sz - 1 then some (i + 1) else none

--@[expose]
public def iterate (a : Array Nat) (i : Nat) : Array Nat :=
  match _ : increment? i a.size with
  | none => a
  | some j =>
    have h: i < a.size := by simp_all[increment?]; omega
    iterate (a.set i a[i]) j
termination_by a.size - i
decreasing_by
  simp_all [increment?]
  omega

Test/Bar.lean

module
import all Test.Foo
public import Test.Foo

theorem iterate_does_nothing (a :Array Nat) (i : Nat) :
    iterate a i = a := by
  induction a, i using iterate.induct with grind [iterate]

With the @[expose] annotation, this will compile. Without it, I get the following error message:

▼ 7:44-7:58: error:
invalid pattern(s) for `iterate.match_1.congr_eq_2`
  [iterate.match_1✝ #5 #4 #3 #2]
the following theorem parameters cannot be instantiated:
  j : Nat
  heq_1 : x✝ = some j

▼ 7:44-7:58: error:
invalid pattern(s) for `iterate.match_1.congr_eq_2`
  [iterate.match_1✝ #5 #4 #3 #2]
the following theorem parameters cannot be instantiated:
  j : Nat
  heq_1 : x✝ = some j

This is already unexpected behavior, but things get even a little stranger.

Consider the following example where we have two copies of iterate, one tagged with @[expose] one not tagged.

Test/Foo.lean

module

public def increment? (i : Nat) (sz: Nat) : Option Nat :=
  if _ : i < sz - 1 then some (i + 1) else none

public def iterate (a : Array Nat) (i : Nat) : Array Nat :=
  match _ : increment? i a.size with
  | none => a
  | some j =>
    have h: i < a.size := by simp_all[increment?]; omega
    iterate (a.set i a[i]) j
termination_by a.size - i
decreasing_by
  simp_all [increment?]
  omega

@[expose]
public def iterate_expose (a : Array Nat) (i : Nat) : Array Nat :=
  match _ : increment? i a.size with
  | none => a
  | some j =>
    have h: i < a.size := by simp_all[increment?]; omega
    iterate_expose (a.set i a[i]) j
termination_by a.size - i
decreasing_by
  simp_all [increment?]
  omega

And the corresponding theorems:

Test/Bar.lean

module
import all Test.Foo
public import Test.Foo

theorem iterate_does_nothing (a :Array Nat) (i : Nat) :
    iterate a i = a := by
  induction a, i using iterate.induct with grind [iterate]

theorem iterate_expose_does_nothing (a :Array Nat) (i : Nat) :
    iterate_expose a i = a := by
  induction a, i using iterate_expose.induct with grind [iterate_expose]

As written, iterate_does_nothing will fail with the aforementioned error message, while iterate_expose_does_nothing will succeed.

However:

• If public import Test.Foo is removed, both versions will fail. The error message on the exposed version is a more standard grind failure message. Attempting to unfold iterate_expose yields ⊢ iterate_expose._unary ⟨a, i⟩ = a.
• Even more bizarrely, if you keep public import Test.Foo and swap the declaration order of iterate and iterate_expose in Test/Foo.lean, both theorems succeed.
• Swapping the definitions and removing public import Test.Foo causes iterate_does_nothing to succeed while iterate_expose_does_nothing does not.

Context

This came up in my PR to add verification to the BinaryHeap implementation in Batteries. leanprover-community/batteries#1602.

Steps to Reproduce

See above.

Expected behavior: import all should not require @[expose] annotations to work, removing public import should not alter whether definitions can be unfolded, declaration order of independent functions should not matter.

Actual behavior: @[expose] annotations are required to make grind prove a theorem even when using import all. Removing public import while having an @[expose] annotation, makes the proof break. Swapping the declaration order of two independent functions makes everything work for some reason.

Versions

Lean 4.28.0-nightly-2026-01-08
Target: x86_64-unknown-linux-gnu

[nomeata]

The two declarations will share a matcher, maybe the congr eq generation for that matcher depends on which one came first.