给定列表索引范围的约束，我可以在这里使用destruct吗？

问题描述

我试图证明对于字节列表a，所有字节都是x01，从索引2到(n-m-2)，其中n是a的长度：

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

在上下文中确实有此内容

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

因此，在intros i i_range.之后，我有：

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

这是销毁H的RHS以消除前两个字节和后m个字节的正确方法吗？如果是这样，我该如何针对i_range执行此操作？让我知道我的证明策略是否有缺陷。

预先感谢您的任何建议。

编辑：

最后一个目标的错字是固定的。首先是nth_error buff i = Some x01，然后我更改为nth_error a i = Some x01。

解决方法

如果可以确保H以“ forall j”开头，则该目标应是可证明的。我不确定我是否理解您建议的策略，但是我会将ntherror（前缀++ foo ++栏）重写为ntherror foo（i-2）（使用适当的已有或可证明的引理），然后由于foo为使用重复定义，将ntherror（重复baz x01）重写为x01。所有这些引理都有应满足的算术副条件。