零长度的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

考虑到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

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