failed to generate equality theorems

Stream: lean4

[Sébastien Michelland]

I have encountered one of the strange match equality theorem errors while trying to simplify a definition. Here's a MWE, hopefully annotated with useful leads (the computations make no sense now that it's minimized):

inductive Ty :=
| int: Ty
| other: Ty -- required for error

inductive Tensor :=
| int: Int -> Tensor
| nested: List Tensor -> Tensor

def hasBaseType: Tensor → Ty → Bool
  | .int _, Ty.int      => true
  | .int _, Ty.other    => true -- Merging Ty.int and Ty.other solves error
  | .nested _, _        => true

-- Not passing h solves error
def flatten (e: Tensor) (τ: Ty) (h: hasBaseType e τ): List Int :=
  match e, τ with
  | .int _, Ty.int     => []
  | .int _, _          => [] -- Ty.other rather than wildcard solves error
  | .nested [], _      => []
  | .nested (_::_), _  => [] -- Merging [] and (_::_) solves error

theorem flatten_list (l: List Tensor) τ (h: hasBaseType (.nested l) τ):
    flatten (.nested l) τ h = [] := by
  simp [flatten] -- failed to generate equality theorems for `match` expression `flatten.match_1`

I tested on the latest nightly leanprover/lean4:nightly-2022-04-24.

[Leonardo de Moura]

@Sébastien Michelland Thanks for posting the issue. Could you also post the version that produces errors during match equality theorem generation? I merged the Ty.int and Ty.other cases and it did not trigger the problem.

[Sébastien Michelland]

Interesting. The version I posted should, in fact, cause the error; all the notes are for changes that make it go away.

[Sébastien Michelland]

For the record, the error also occurs in lake build, so a VSCode problem seems unlikely.

[Leonardo de Moura]

@Sébastien Michelland My mistake. I managed to reproduce the problem. Thanks.

[Leonardo de Moura]

Pushed a fix for this one https://github.com/leanprover/lean4/commit/6bc5433b17ee269265aab3adad83dbdbbb80f198

[Sébastien Michelland]

Thank you very much. The rate at which you put out these fixes is impressive, and much appreciated.

[rami3l]

@Leonardo de Moura Hi! I have recently encountered a similar issue as well. Would you mind taking another look?

inductive Ty where
| star: Ty
notation " ✶ " => Ty.star

abbrev Context : Type := List Ty

inductive Lookup : Context → Ty → Type where
| z : Lookup (t :: Γ) t

inductive Term : Context → Ty → Type where
| var : Lookup Γ a → Term Γ a
| lam : Term (✶ :: Γ) ✶ → Term Γ ✶
| ap : Term Γ ✶ → Term Γ ✶ → Term Γ ✶

abbrev plus : Term Γ a → Term Γ a
| .var i => .var i
| .lam n => .lam (plus n)
| .ap (.lam _) m => plus m -- This case takes precedence over the next one.
| .ap l m => (plus l).ap (plus m)

example : plus (.ap l m) = (plus l).ap (plus m) := by
  unfold plus
  ^^ failed to generate equality theorems for `match` expression `plus.match_1`

PS: My lean-toolchain says leanprover/lean4:nightly-2023-05-16.

[Leonardo de Moura]

Please create an issue on GitHub.

[rami3l]

@Leonardo de Moura Thanks! I have created https://github.com/leanprover/lean4/issues/2237 for this.