1

I have the following lemma in why3:

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

This seems like it would be the base case behavior, but apparently isn't. Any ideas on why this isn't working?

UPDATE
I was able to reduce the issue to a single missing lemma:

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

This seems trivial as well, given the definition of array_eq_sub as specified in the documentation. Why can't my prover find a solution?

Derek Brown
  • 4,232
  • 4
  • 27
  • 44

1 Answers1

0

After struggling with this issue, I decided to take a look at the why3 source code. I found a definition which was different from what was documented:

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

In short, the lengths of the arrays have to be equal in order for a portion of them to be equal. This was different than what was documented, and I suspect may be causing many theorems to be unsound.

Derek Brown
  • 4,232
  • 4
  • 27
  • 44