我有以下引理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
中指定的定义,这似乎也是微不足道的。为什么我的证明者找不到解决方案?