Strange 'import all' bug

Stream: batteries

[cmlsharp]

Here's an isolated example, this experimentation actually led me to find some _very_ odd behavior (including that the declaration order of independent functions matters)

First, as minimal of an example as I can get:

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]

This will compile only if @[expose] is uncommented. I get the following error:

▼ 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

However, I discovered even more weirdness.

Let's augment Foo and Bar with identical copies of iterate at varying visibilities:

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


def iterate_priv (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_priv (a.set i a[i]) j
termination_by a.size - i
decreasing_by
  simp_all [increment?]
  omega

And lets modify Test/Bar.lean to have the corresponding theorems:

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]

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

At first, it's as before, only iterate_expose_does_nothing compiles.

Two strange facts about this setup:

• Removing the public import Test.Foo (or replacing it with import Test.Foo) causes all three theorems to fail to compile. The reported error for iterate and iterate_priv are the same as before, but the iterate_exposetheorem now fails with a standard grind failure. Investigating further reveals that, 'iterate_expose' cannot be unfolded (or more accurately, unfolding it doesn't give you its body, it gives you stuff that if you keep unfolding you get the recursion in terms of WellFounded.fix etc).
• Even more bizarrely, changing the declaration order of these functions in Test/Foo.lean changes the result. If iterate_expose is declared _before_ iterate and iterate_priv, then all three theorems compile!
• If iterate_expose is declared first _and_ public import Test.Foo is removed, then iterate_does_nothing and iterate_priv_does_nothing will compile while iterate_expose_does_nothing will not.

I did try to simplify this match statement into e.g. a dependent if-then-else, but I was not able to replicate the issue, so the match seems important.

Edit: also as an additional note, the use of iterate.induct doesn't seem important here. Just replacing the whole proof with 'grind [iterate]' shows the same error "invalid patterns" error when iterate is non-exposed and just reports an expected failure to prove when it is.

[Notification Bot]

A message was moved here from #batteries > Verifying BinaryHeap (PR Review) by cmlsharp.

[cmlsharp]

github issue:
https://github.com/leanprover/lean4/issues/11948