Pattern matching subtypes

Stream: lean4

[Andrés Goens]

I was trying to write a pattern match on a subtype structure and got a strange error. Here's an #MWE:

def drop_false_head? {n : Nat} : Vector Bool (n+1) → Option (Vector Bool n)
  | Vector.cons false z => some z
  | _ => none

I get

invalid patterns, `z` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  { val := false :: .(z.1), property := (_ : Nat.succ (List.length ↑z) = Nat.succ n) }

Is there a way to get the pattern matcher to do this (there's an annotation that allows me to mark Vector.cons here to work as a constructor for pattern matching, right)? Or is this a fundamental limitation with how the pattern matcher gets delaborated on subtypes?

(I'm not looking for a workaround here, for this example I can just pattern match the subtype with something like | ⟨true :: z,hcons⟩ => some ⟨z, by aesop⟩, I'm curious about the pattern matching in general in this context)

[Mario Carneiro]

I guess the issue is that the property := (_ : ...) part is actually hiding a proof, and you can't pattern match proofs

[Mario Carneiro]

note that in your proposed alternative match, you have an additional binding hcons that doesn't exist in the original version

[Alex Keizer]

On the other hand, we can write an alternative recursion principle that breaks a vector down into nil and cons cases, kind of like the computational analogue of Vector.inductionOn. Is there some way to instruct the equation compiler / pattern matcher to work with such an alternative recursion principle (akin to how induction ... using ... can be used to use an alternative induction principle)?