
I thought that Dafny would unroll function definitions on "known" input. But it does not. Here an example:
Take the predicate subsequence for lists  as in the end of this message.
Then,, I was stuck in the following:
var xs:= Cons(1,Cons(2, Nil));
var ys:= Cons(2,Cons(1, Cons(1, Nil)));
assert ! (subsequence(xs, ys)) ; //Dafny does not verify
I could force the above to verify by “calculations”, as follows:
calc {
subsequence(xs,ys);
==>
subsequence(Cons(1,Cons(2, Nil)), Cons(1,Cons(1, Nil)));
==>
subsequence(Cons(2, Nil), Cons(1,Cons(1, Nil)));
==>
subsequence(Cons(2, Nil), Cons(1, Nil));
==>
subsequence(Cons(2, Nil), Nil);
==
false;
}
assert ! (subsequence(xs, ys)) ; // verifies
But I would have thought that Dafny sould have unrolled the definition of “subsequence”, since it know that it terminates on finite inputs.
Cheers,
Sophia
PS And here the definitions
predicate subsequence<T>(xs: list<T>, ys: list<T>)
{
match xs
case Nil => true
case Cons(x, xs') =>
match ys
case Nil => false
case Cons(y, ys') =>
if (x == y)
then subsequence(xs', ys')
else subsequence(xs, ys')
}



Related to previous:
I tried to reason with quantifiers and induction, but several proofs which I expected should go through, did not.
I think it is has to do with the treatment of constant terms, that they are “unrolled” only one level deep.
I defined, for lists the following predicates
 predicate elem<T>(n: T, xs: list<T>) – recursively
 predicate subset<T>(xs: list<T>, ys: list<T>) – through universal quantifiers
I attach the definitions at the end of this posting.
I could easily prove that subset => subsequence, quite easily,
But then, I was stuck in the following:
var xs:= Cons(1,Cons(2, Nil));
var ys:= Cons(2,Cons(1, Cons(1, Nil)));
assert subset(xs,ys); // does not verify
I then tried unrolling the definitions, and after a lot of unrolling, I could verify.
First I added
assert forall x:: ( (elem(x,xs)) ==> (x==1  x==2) ); // does not verify
assert subset(xs,ys); // does not verify
The I added
var us:= Cons(1,Nil);
var xs:= Cons(1,Cons(2, Nil));
var ys:= Cons(2,Cons(1, Cons(1, Nil)));
assert forall x:: ( elem(x,us) ==> (x==1 ) ) ; // verifies
assert forall x:: ( (elem(x,xs)) ==> (x==1  x==2) ); // verifies
assert subset(xs,ys); // still does not verify
I then added some more:
assert forall x:: ( elem(x,us) ==> (x==1 ) ) ;
assert forall x:: ( (elem(x,xs)) ==> (x==1  x==2) );
assert subset(xs,zs);
assert subset(xs,vs);
assert elem(2,ys);
assert elem(1,ys);
assert subset(xs,ys); // verifies
Also, instead I unrolled the definition of xs, and it worked too:
var vs:= Cons(2,Cons(1, Nil));
assert subset(xs,vs);
assert subset(xs,ys);
And here the definitions
predicate elem<T>(n: T, xs: list<T>)
{
match xs
case Nil => false
case Cons(y, ys) => n == y  elem(n, ys)
}
predicate subset<T>(xs: list<T>, ys: list<T>)
{
forall x :: elem(x, xs) ==> elem(x, ys)
}
predicate subsequence<T>(xs: list<T>, ys: list<T>)
{
match xs
case Nil => true
case Cons(x, xs') =>
match ys
case Nil => false
case Cons(y, ys') =>
if (x == y)
then subsequence(xs', ys')
else subsequence(xs, ys')
}


Coordinator
Apr 25, 2013 at 12:12 AM

Hi Sophia,
Re your first post above: Dafny applies the same rule to all uses of functions, regardless of if the arguments are given as literals. That is, they are subject to the same unwind limits. One way to change this (which I'm not currently planning on doing, but
perhaps it should be done) would be to let users manually set the unwinding depth (perhaps in an attribute attached to an assert statement). A solution that would do this automatically would be nicer, but this is trickythe function call is not known to terminate
until the verifier has checked it to terminate (for example, what if the definition of subset was written to recurse forever), so one needs to invoke the verifier before one can determine if it is safe to (without any limits) partially evaluate calls.
Re your second post: You say you can prove subset ==> subsequence. Did you perhaps mean subsequence ==> subset?
In conclusion: Your various manual unrollings, asserts, and calculations arehowever awkwardcurrently the way to prove such properties.
Rustan

