Problem with Nested Quantifiers

[DavePearce]

The following assertion from whiley.lang.Array fails to verify:

function indexOf(int[] items, int item, int start) -> (int index)

define indexOf_ensures_1(int[] items, int item, int index) is:
    forall(int i):
        if:
            (0 <= i) && (i < index)
        then:
            items[i] != item

define indexOf_ensures_1(int[] items, int item, int start, int index) is:
    forall(int index$1):
        if:
            index$1 == index
        then:
            forall(int i):
                if:
                    (start <= i) && (i < index)
                then:
                    items[i] != item

assert "postcondition not satisfied":
    forall(int item, int[] items):
        if:
            indexOf_ensures_1(items, item, 0, indexOf(items, item, 0))
        then:
            indexOf_ensures_1(items, item, indexOf(items, item, 0))

Observe that removing the quantifier forall(int index$1) (which is not actually needed) and it will verify. The failing proof looks like this:

 195. exists(int item, int[] items).(((indexOf_ensures_1(items, item, 0, ind () 
 197. exists(int item, int[] items).(indexOf_ensures_1(items, item,  (Simp 195) 
 196. indexOf_ensures_1(items, item, 0, indexOf(items, item, 0)) (Exists-E 197) 
 188. indexOf_ensures_1(items, item, 0, indexOf(items, item, 0))    (And-E 196) 
 190. !indexOf_ensures_1(items, item, 0, indexOf(items, item, 0))   (And-E 196) 
 224. forall(int index$1).((((index$1 != indexOf(items, item, 0)) (Macro-I 188) 
 250. exists(int index$1).((((index$1 == indexOf(items, item, 0)) (Macro-I 190) 
 258. forall(int index$1).((index$1 != indexOf(items, item, 0)) || f (Simp 224) 
 266. exists(int index$1).((index$1 == indexOf(items, item, 0)) && e (Simp 250) 
 265. (index$1 == indexOf(items, item, 0)) && exists(int i).((i  (Exists-E 266) 
 228. index$1 == indexOf(items, item, 0)                            (And-E 265) 
 264. exists(int i).((i >= 0) && (indexOf(items, item, 0) >= (1 + i (And-E 265) 
 272. forall(int index$1).((index$1 != index$1) || forall(int i) (Eq-S 258,228) 
 275. exists(int i).((i >= 0) && (index$1 >= (1 + i)) && (item = (Eq-S 264,228) 
 274. (i >= 0) && (index$1 >= (1 + i)) && (item == items[i])     (Exists-E 275) 
 259. i >= 0                                                        (And-E 274) 
 273. index$1 >= (1 + i)                                            (And-E 274) 
 262. item == items[i]                                              (And-E 274) 
 276. index$1 >= 1                                              (Ieq-I 273,259) 
 279. index$1 == indexOf(items, items[i], 0)                     (Eq-S 228,262) 
 284. forall(int index$1).((index$1 != index$1) || forall(int i) (Eq-S 272,262) 
 290. forall(int index$1).((index$1 != indexOf(items, items[i],  (Eq-S 272,279) 
 291. indexOf(items, items[i], 0) >= (1 + i)                     (Eq-S 273,279) 
 292. indexOf(items, items[i], 0) >= 1                           (Eq-S 276,279) 
 296. forall(int index$1).((index$1 != indexOf(items, items[ (Eq-S 284,279,279) 
./Array.wyal:21: postcondition not satisfied
assert "postcondition not satisfied":
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

NOTE: the inclusion of the unnecessary enclosing quantifier has arisen presumably for valid reasons. Specifically, to handle flow typing which is used in the Whiley code.

[DavePearce]

Here is a simplified version:

define greater(int[] xs, int x) is:
    forall(int i):
        if:
           (i >= 0) && (i < |xs|)
        then:
           xs[i] != x

define greater_2(int[] xs, int x) is:
    forall(int m):
        forall(int i):
           if:
              (i >= 0) && (i < |xs|)
           then:
              xs[i] != x

assert:
    forall(int[] items, int item):
        if:
            greater_2(items,item)
        then:
            greater(items,item)

The failing proof is thus:

 132. exists(int[] items, int item).(((greater_2(items, item)) && (!greater(items, item))))                          () 
 134. exists(int[] items, int item).(greater_2(items, item) && !greater(items, item))                        (Simp 132) 
 133. greater_2(items, item) && !greater(items, item)                                                    (Exists-E 134) 
 125. greater_2(items, item)                                                                                (And-E 133) 
 127. !greater(items, item)                                                                                 (And-E 133) 
 157. forall(int m).(forall(int i).(((((0 >= (i + 1)) || ((i + 1) >= (|items| + 1)))) || ((items[i] != it (Macro-I 125) 
 174. exists(int i).((((((i + 1) >= (0 + 1)) && ((|items| + 1) >= ((i + 1) + 1)))) && ((items[i] == item) (Macro-I 127) 
 181. forall(int m).forall(int i).((0 >= (1 + i)) || (i >= |items|) || (item != items[i]))                   (Simp 157) 
 187. exists(int i).((i >= 0) && (|items| >= (1 + i)) && (item == items[i]))                                 (Simp 174) 
 186. (i >= 0) && (|items| >= (1 + i)) && (item == items[i])                                             (Exists-E 187) 
 182. i >= 0                                                                                                (And-E 186) 
 184. |items| >= (1 + i)                                                                                    (And-E 186) 
 185. item == items[i]                                                                                      (And-E 186) 
 188. |items| >= 1                                                                                      (Ieq-I 184,182) 
 192. forall(int m).forall(int i).((0 >= (1 + i)) || (i >= |items|) || (items[i] != items[i]))           (Eq-S 181,185) 
./test.wyal:16: null
assert:
^^^^^^^^^

Clearly, one option is to add a rule for merging forall(int m).(forall(int i).E) into forall(int m, int i).E). That will verify, though it doesn't feel like a general solution.