Hi Rustan ---
Further on time-outs: I have a short program (below) that verifies; but if you un-comment an assumption, it loops. Thus it -is- correct (since an assumption can only make it "correcter"), but I cannot proceed any further with this approach unless
I can experiment with the assumption.
--- So is there any way I can get guidance (from Dafny or Z3) about why it is looping, and how to avoid that?
The background is that the assertion I need has a very particular conjunct in its antecedent, an existential quantifier, and I will eventually need to prove that with a lemma. (It has an inductive assertion, basically that if there is a solution to something
at all, then there is a least one.) But --in the spirit of your remarks about lemmas-- I would like to make sure that the lemma is what I need before I go and prove it. Hence the assumption --- but, because of the loop, I am stuck.
So --- to summarise --- the code below verifies in rise4fun; but if you remove the comment symbols, it times out.
Thanks!
function LastElement(bs: seq<int>): int requires bs!=[]; { bs[|bs|-1] }
function Front(bs: seq<int>): seq<int> requires bs!=[]; { bs[..|bs|-1] }
function LastValue(bs: seq<int>, cs: seq<int>): int requires cs!=[] && selectsUpsequence(bs,cs);
{ bs[LastElement(cs)] }
predicate isStrictlySorted (bs: seq<int>)
{ forall i,j:: 0<=i<j<|bs| ==> bs[i]<bs[j] }
predicate selectsSubsequence (bs: seq<int>, cs: seq<int>)
{ isStrictlySorted(cs) && forall i:: 0<=i<|cs| ==> 0<=cs[i]<|bs| }
predicate selectsUpsequence (bs: seq<int>, cs: seq<int>)
{ selectsSubsequence(bs,cs) && forall i,j:: 0<=i<j<|cs| ==> bs[cs[i]]<bs[cs[j]] }
predicate selectsLowestUpsequence (bs: seq<int>, cs: seq<int>, c: int)
{ selectsUpsequence(bs,cs) &&
(cs!=[] ==> c==bs[LastElement(cs)]
&& forall ds:: selectsUpsequence(bs,ds)
&& |cs|==|ds|
==> c<=bs[LastElement(ds)]) }
method Test() {/*
assume forall bs,cs,ds,d::
selectsUpsequence(bs,cs)
==>
(exists ds,d:: |ds|==|cs| && selectsLowestUpsequence(bs,ds,d))
;*/
assert forall bs,n,cs,c,ds,d:: 0<=n && n+1<|bs| &&
selectsLowestUpsequence(bs[..n],cs,c) &&
selectsLowestUpsequence(bs[..n],ds,d) &&
|ds|==|cs|+1 &&
|cs|>=1 &&
(exists es,e::
selectsLowestUpsequence(bs[..n+1],es,e) &&
|es|==|ds| &&
(c<=LastValue(bs[..n+1],Front(es))<bs[n] ==> c<bs[n]) // Pointless truth supplies a trigger?
) &&
true
==>
if (c<bs[n]<=d) then selectsLowestUpsequence(bs[..n+1],cs+[n],bs[n])
else if bs[n]<=c then selectsLowestUpsequence(bs[..n+1],ds,d)
else if d<bs[n] then selectsLowestUpsequence(bs[..n+1],ds,d)
else false
;
}