Recovering dependent pattern matching for non-constructor

Stream: new members

[pandaman]

Hi! I'm trying to replace a List-based stack with an Array in the hope of improving the performance. However, I got stuck when repairing proofs that use inductive predicates like the following because Lean was unable to see that the two cases match distinct patterns. Is there any way to recover the dependent pattern eliminations in this case? I tried putting the equality as a hypothesis of .nil and .cons, but managing additional equalities cluttered the proof a lot. Thanks!

inductive P : Array Nat → Prop where
  | nil : P #[]
  | cons (h : P xs) : P (xs.push x)

example {xs : Array Nat} (p : P (xs.push x)) : True := by
  cases p with
  | nil => sorry -- dependent elimination failure
  | cons rest => sorry

-- List just works
inductive P' : List Nat → Prop where
  | nil : P' []
  | cons (h : P' xs) : P' (x :: xs)

example {xs : List Nat} (p : P' (x :: xs)) : True := by
  cases p with
  | cons rest => sorry

[Kyle Miller]

Maybe do the theory using the List version, then use Array for definitions that you will actually run, and then write a bit of "glue" to use the List version to prove things about the Array version?

[Kyle Miller]

Dependent elimination isn't extensible, and there's no way yet to relax it (e.g. it would be nice if you could be given the equalities it is trying to eliminate and apply your own tactics)

[pandaman]

Kyle Miller said:

Maybe do the theory using the List version, then use Array for definitions that you will actually run, and then write a bit of "glue" to use the List version to prove things about the Array version?

I would imagine this ends up declaring a version of the algorithm that uses lists as the stack, and writing the lemmas to transport the results itself feels too large.

[Robin Arnez]

Try generalizing beforehand (generalize ha : xs.push x = a at p)