dependent match elimination failed

Stream: lean4

[Bhavik Mehta]

I often run into the error "dependent match elimination failed, inaccessible pattern found", and I find this pretty confusing and hard to fix. Here's an example:

inductive MyOrder : Nat × Nat × Nat → Nat × Nat × Nat → Prop
  | twice {x y n u v m : Nat} : m + 2 ≤ n → MyOrder (x, y, n) (u, v, m)
  | within {x y u v m : Nat} : x ≤ u → y ≤ v → MyOrder (x, y, m) (u, v, m)
  | next_min {x y u v m : Nat} : min x y + 1 ≤ min u v → MyOrder (x, y, m + 1) (u, v, m)

theorem antisymmetric : ∀ {x y : Nat × Nat × Nat}, MyOrder x y → MyOrder y x → x = y
  | _, _, .twice _, .twice _ => _
  | _, _, .twice _, .within _ _ => _
  | _, _, .twice _, .next_min _ => _
  | _, _, .within _ _, .twice _ => _
  | _, _, .within _ _, .within _ _ => _
  | _, _, .next_min _, .twice _ => _

the error given here is

dependent match elimination failed, inaccessible pattern found
  .(n✝)
constructor expected

The solution I found is to change the sixth underscore to three more underscores (_, _, _) instead, but this was essentially by trial and error. What does this error mean, why do I keep getting it with inductive types, and can we make this whole situation clearer?

[Kyle Miller]

I tried understanding this better, and my guess is that match is making a mistake for which arguments in the pattern are inaccessible (or at least there's something in this example that misleads it).

If you use an explicit pattern in that spot, it works:

theorem antisymmetric : ∀ {x y : Nat × Nat × Nat}, MyOrder x y → MyOrder y x → x = y
  | _, _, .twice _, .twice _ => _
  | _, p, .twice _, .within _ _ => _
  | _, _, .twice _, .next_min _ => _
  | _, _, .within _ _, .twice _ => _
  | _, _, .within _ _, .within _ _ => _
  | _, _, .next_min _, .twice _ => _

There's a step in "dependent match elimination" that can handle explicit patterns and do constructor splitting.

I'm not sure about the details, but I think the deal is that _ can stand for .(_) when necessary, for convenience. Inaccessible patterns .(...) indicate a term that's supposed to be determined by the other patterns, and there should be no matching done on it. It's not clear to me why p above shouldn't be inaccessible.

[Bhavik Mehta]

Huh, I'm surprised that putting p there or putting (_, _, _) there fixes it. My guess was that expanding out would help, but p seems to me like it's blocking any expansion, so I'm surprised that that works..

[Kyle Miller]

It's probably worth making creating issue for this. Maybe it's all somehow logical in the end, but it would be nice if it could work without needing to guess how to work around it.

[Bhavik Mehta]

lean4#6416