array_eq_sub 零长度的行为

Question

我在 why3 中有以下引理：

lemma trivial:
  forall a : array 'a, b : array 'a.
  array_eq_sub a b 0 0

这似乎是基本情况下的行为，但显然不是。关于为什么这不起作用的任何想法？

更新
我能够将问题减少到一个缺失的引理：

lemma array_eq_2:
  forall a : array 'a, b : array 'a.
  map_eq_sub a.elts b.elts 0 0 -> array_eq_sub a b 0 0

考虑到 the documentation 中指定的 array_eq_sub 的定义，这似乎也是微不足道的。为什么我的证明者找不到解决方案？

Answer 1

在纠结这个问题之后，我决定看一下 why3 源代码。我发现了一个与文档中不同的定义：

predicate array_eq_sub (a1 a2: array 'a) (l u: int) =
  a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\
  map_eq_sub a1.elts a2.elts l u

简而言之，数组的长度必须相等才能使其中的一部分相等。这与记录的不同，我怀疑可能导致许多定理不可靠。

array_eq_sub 零长度的行为

array_eq_sub behavior for zero length

why3