The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
The following example leads to a lot of quantifier instantiation (though it will pass with the right depth). The problem is that the larger version pushes the depth a lot.
type nat is (int x)
where:
x >= 0
define invariant(nat[] xs) is:
forall(int k):
if:
(0 <= k) && (k < |xs|)
then:
xs[k] >= 0
assert:
forall(int i, nat[] ys, nat[] xs):
if:
invariant(xs)
(i >= 0) && (i < |xs|)
ys == xs[i:=xs[i]]
then:
invariant(ys)
The following example leads to a lot of quantifier instantiation (though it will pass with the right depth). The problem is that the larger version pushes the depth a lot.
type nat is (int x) where: x >= 0 define invariant(nat[] xs) is: forall(int k): if: (0 <= k) && (k < |xs|) then: xs[k] >= 0 assert: forall(int i, nat[] ys, nat[] xs): if: invariant(xs) (i >= 0) && (i < |xs|) ys == xs[i:=xs[i]] then: invariant(ys)