strange error with unrelated theorem

Stream: lean4

[Arthur Paulino]

I'm getting a strange error on this theorem when commenting out the theorem above it (State.skipStep). Even simply replacing the proof of State.skipStep by a sorry causes the same error:

failed to generate equality theorems for `match` expression
case lam.mk
motive : Value → Sort u_1
h_1 : (ns : NEList String) → (h : NEList.noDup ns = true) → (p : Program) → motive (Value.lam (Lambda.mk ns h p))
h_2 : (v : Value) → motive v
l✝ : NEList String
a✝¹ : NEList.noDup l✝ = true
a✝ : Program
: ∀ (ns : NEList String) (h : NEList.noDup ns = true) (p : Program),
  Value.lam (Lambda.mk l✝ a✝¹ a✝) = Value.lam (Lambda.mk ns h p) → False
⊢ h_1 l✝ a✝¹ a✝ = h_2 (Value.lam (Lambda.mk l✝ a✝¹ a✝))

[Arthur Paulino]

Forgot to mention: I'm using leanprover/lean4:nightly-2022-04-19

[Leonardo de Moura]

Could you please create a #mwe for this issue?

[Arthur Paulino]

I tried to but I couldn't :(
It seems to rely on the pile of definitions from my repo

[Leonardo de Moura]

The error seems to happen when Lean tries to create the equation theorems for stepN or step. Could you confirm which one triggers the problem by using the command:

attribute [simp] stepN
attribute [simp] step

stepN looks very simple. So, I am betting the problem is on step, but I did not find its definition yet.
The next step would be to keep reducing the complexity of step while the bug is still triggered.
We would be very grateful if you could go over this minimization problem. It would save us a lot of time.

[Arthur Paulino]

Both of the following work:

attribute [simp] stepN
attribute [simp] step

The definition of step is indeed involved. I'll try to minimize the problem but since the problem arises in a theorem when commenting out another (apparently unrelated) theorem, I am not very optimistic about it

[Arthur Paulino]

@Leonardo de Moura here's a gist with a piece of self-contained Lean code:
https://gist.github.com/arthurpaulino/410aeaedba79282402127183d8d6f863

[Arthur Paulino]

The code is shorter because I only took the necessary definitions but I wasn't able to find a smaller instance of the issue

[Sébastien Michelland]

FWIW, I wanted to give it a try so I installed leanprover/lean4:nightly-2022-04-19 but the server keeps crashing on my computer.

[Leonardo de Moura]

Arthur Paulino said:

Leonardo de Moura here's a gist with a piece of self-contained Lean code:
https://gist.github.com/arthurpaulino/410aeaedba79282402127183d8d6f863

Thanks! I managed to reproduce the problem. I am investigating.

[Leonardo de Moura]

@Arthur Paulino Pushed a fix for this https://github.com/leanprover/lean4/commit/73076b855c94eaa1a380e05411b60ca19df191f6

[Arthur Paulino]

Thanks!!