时间戳

首页 > 解决方案 > 考虑到我对列表索引范围的约束，我可以在这里使用 destruct 吗？

coq - 考虑到我对列表索引范围的约束，我可以在这里使用 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

这是破坏 RHSH以消除前两个字节和最后一个m字节的正确方法吗？如果是这样，我该怎么做i_range？如果我的证明策略有缺陷，请告诉我。

提前感谢您的任何建议。

编辑：

最后一个目标的错字是固定的。这是nth_error buff i = Some x01第一个，我改为nth_error a i = Some x01.

标签： coqproofcoq-tacticformal-verification

解决方案

如果您可以确保 H 以“forall j”开头，那么目标应该是可证明的。我不确定我是否理解您建议的策略，但我会将 ntherror (prefix ++ foo ++ bar) i 重写为 ntherror foo (i - 2) （使用合适的引理，现有的或可证明的），然后因为 foo 是使用重复定义，将 ntherror (repeat baz x01) 重写为 x01。所有这些引理都有应该成立的算术附带条件。

推荐阅读