考虑到我对列表索引范围的约束，我可以在这里使用 destruct 吗？答案

【问题标题】：Can I use destruct here given the constraint I have for index range of a list?考虑到我对列表索引范围的约束，我可以在这里使用 destruct 吗？
【发布时间】：2020-10-03 15:26:39
【问题描述】：

我试图证明对于字节列表a，从索引2 到(n-m-2) 的所有字节都是x01，其中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。

【问题讨论】：

结论中的buff 变量是否与任何其他术语相关？如果不是，则无法证明目标，因为buff 没有任何限制（例如，它可能为空）。
对不起，为了简单起见，我重命名了一些东西。 Buff 实际上是 a。我会纠正这个问题。谢谢！
在上下文中有一个存在变量 ?j 似乎是一个潜在的问题。特别是，您需要将 ?j 设为 i，这似乎范围不广，因此您可能有错误的目标。
致@Blaisorblade：这个存在变量?j 来自应用我已经证明的另一个定理，即Theorem list_eq_correctness: forall (l1 l2: list byte), list_eq l1 l2 = true -> (forall (j : nat), nth_error l1 j = nth_error l2 j). 如果我需要?j 是i，我可以instantiate ( 1 := i ) in H.
基于问题，实例化应该失败，因为在 i 范围内之前引入了 evar；如果它有效，那就更好了。（如果需要，解决方法是稍后应用引理。）引理没有任何问题，但不幸的是您没有得到 forall 语句。

标签： coq proof coq-tactic formal-verification

【解决方案1】：

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

【讨论】：

（抱歉有错别字，希望还是清楚的；我在手机上）。
别担心！这真的是一个很大的帮助。正如你所说，我使用了两个现有的引理，如rewrite nth_error_app2 in H. simpl in H. rewrite nth_error_app1 in H. 以摆脱 prefix 和 bar。然后，我通过添加assert (nth_error_repeat_elim: forall (i j : nat) (b : byte), j < i -> nth_error (repeat b i) j = Some b). admit. rewrite nth_error_repeat_elim in H. 删除了foo，并通过apply H. 证明了我的目标最后，我使用i_range 来证明那些重写添加为下一个子目标的算术附带条件。非常感谢，@Blaisorblade！