Longest UpSequence --- and quantifiers

Feb 7, 2013 at 10:25 PM

I'm using the longest-upsequence problem as a "getting to know Dafny" example (and it has generated the previous questions). Mainly I'm not treating quantifiers in the style that Dafny/Z3 expects. Can anyone help with a (high-level) way of thinking about how Z3 works, one with which you can figure out "how to quantify" in a way that will help Dafny? See (***) below for a more precise formulation of that.

Meanwhile, here is the latest example.

To say that sequence (of indices) us identifies a subsequence (of values) in ss that are ascending, I wrote

predicate UpSequence (ss: seq<int>, us: seq<int>)
{ |us|<=|ss| && forall i,j:: 0<=i<j<|us| ==> 0<=us[i]<us[j]<|ss| && ss[us[i]]<ss[us[j]] }

(At first I did not include the superfluous |us|<=|ss|. But, without it, Dafny would not accept

UpSequence (ss[..0],[]) ,

which is the example that when stripped down seemed to lead to my earlier questions at [discussion:432113] about existential quantification.)

The current issue is that I would like to be able to conclude



UpSequence(ss,us) ,

that is that if us finds an upsequence in ss then that is an upsequence of its extension ss+[x].

Dafny won't do that for me at the moment. Stripping it down to essentials yields this example:

predicate Test1 (s: int, us: seq<int>)
{ forall i,j:: 0<=i<|us| && 0<=j<|us| ==> true }

predicate Test2 (s: int, us: seq<int>)
{ forall i,j:: 0<=i<|us| && 0<=j<|us| ==> 0<=us[i] }

predicate Test3 (s: int, us: seq<int>)
{ forall i,j:: 0<=i<|us| && 0<=j<|us| ==> 0<=us[i] && 0<=us[j] }

method Tests() {
var yy: seq<int>;
var x: int;

assume Test1 (x,yy);
assert Test1 (x+1,yy);
assume Test2 (x,yy);
assert Test2 (x+1,yy); // Only this one fails.
assume Test3 (x,yy);
assert Test3 (x+1,yy);

which yields

Dafny program verifier version, Copyright (c) 2003-2013, Microsoft.
Test8.dfy(20,10): Error: assertion violation
Test8.dfy(8,3): Related location: Related location
Execution trace:
(0,0): anon0
Dafny program verifier finished with 5 verified, 1 error

(***) I can see that there's an issue of how thing are said --- what I would like is to know how to figure out for myself how to say things. For example, referring to the third post in [discussion:432113], the sort of high-level reasoning I'd like to employ would be something like

assume exists m: int :: m>0;

creates a Skolem constant x, say, and an assertion x>0 about it; then when evaluating

assert exists m: int :: m>0;

the m is instantiated to that x, and the assertion passes.

But actually it does not pass, so this informal reasoning (about how to "drive" Dafny) is not correct. But it's an example of the sort of thing I'm looking for.