Problem with Reasoning about Existentials

[DavePearce]

Currently, the following theorem fails to verify:

define invariant([int] items, int item, int n) is:
    exists(int i):
        n < i && items[i] == item

assert:
    forall([int] items, int item, int n):
        if:
            invariant(items,item,n)
            items[n] != item
        then:
            invariant(items,item,n+1)

This doesn't work because the theorem prover does not pull out existentials. Perhaps it could ...

[DavePearce]

Here's another simpler example which fails for reasons unknown:

assert:
    forall ([int] items):
        if:
            |items| > 0
        then:
            exists (int i):
                i == 0
                items[0] == items[i]

UPDATE: the problem is that there's nothing for quantifier instantiation to trigger on.

[DavePearce]

For the above example, the generated condition for unsat checking is:

assert "":
    some([int] r0):
        0 < |r0|
        forall(int r1):
            case:
                r1 != 0
            case:
                r0[0] != r0[r1]

It's not really clear how this could generate unsat, because the inner quantifier will never instantiate. This example arises from this whiley function, specifically establishing the existential on entry:

function max(int[] items) -> (int r)
requires |items| > 0
ensures all { i in 0..|items| | items[i] <= r }
ensures some { i in 0..|items| | items[i] == r }:
    //
    int i = 1
    int max = items[0]
    //
    while i < |items| 
    where i >= 1
    //where all { k in 0..i | items[k] <= max }
    where some { k in 0..i | items[k] == max }:
        if items[i] > max:
            max = items[i]
        i = i + 1
    //
    return max

Here, the universal quantifer commented out as that also is not satisfied on entry (see #545).