Can I use destruct here given the constraint I have for index range of a list?

Question

I’m trying to prove that for a list of bytes a, all bytes are x01 from index 2 to (n-m-2), where n is the length of a:

(forall (i : nat), ((i >= 2) /\ (i < ((n - m) - 1))) -> ((nth_error a i) = (Some x01)))

and I do have this in the context:

H : nth_error a ?j =
      nth_error ([x00; x00] ++ repeat x01 (n - m - 2) ++ repeat x00 m)%list  ?j

So, after intros i i_range. I have:

i : nat
i_range : is_true (1 < i) /\ is_true (i < n - m - 1)
H : nth_error a ?j =
      nth_error ([x00; x00] ++ repeat x01 (n - m - 2) ++ repeat x00 m)%list  ?j
______________________________________(1/1)
nth_error a i = Some x01

Is this a right approach to destruct the RHS of H to eliminate the first two bytes and the last m bytes? If so, how can I do that with respect to i_range? Let me know if my proof strategy is flawed.

Thanks in advance for any suggestion.

Edit:

The last goal's typo is fixed. It was nth_error buff i = Some x01 first and I changed to nth_error a i = Some x01.

Answer 1

If you can ensure H starts with “forall j,”, the goal should be provable. I am not sure I understand the strategy you suggests, but I’d rewrite ntherror (prefix ++ foo ++ bar) i to ntherror foo (i - 2) (using suitable lemmas, either existing or provable), then since foo is defined using repeat, rewrite ntherror (repeat baz x01) to x01. All these lemmas have arithmetic side conditions that should hold.