Injective implies Onto

Apr 13, 2014 at 1:04 AM
I need to have that
If an array of size N is injective into 0,1...N-1 then it is onto.
for a program I'm finishing off (inverting a permutation within an array). As a first step, I have this:
    ghost method isOnto(A:array<int>)
        requires A!=null;
        requires forall a:: 0<=a<A.Length ==> 0<=A[a]<A.Length; 
        requires forall a,a':: 0<=a<A.Length && 0<=a'<A.Length && a!=a' ==> A[a]!=A[a'];
        ensures forall b:: 0<=b<A.Length ==> exists a:: 0<=a<A.Length && A[a]==b;
    {   if (A.Length==0) { assume true; }
        else if (A.Length==1) { assert A[0]==0; }
        else { assume false; }
But I don't know where to go from here (or even whether I should be here ;-)

Any suggestions?
Apr 15, 2014 at 9:58 PM
Hi Nunibad,

Here is a solution to the problem: (There may be simpler solutions.) For the reverse problem--proving that the range property (the second precondition in your example) and onto implies injectivity--see Test/VSComp2010/Problem2-Invert.dfy in the Dafny test suite.

As for your question about should you even be here :), my suggestion would be to use multisets, if your application allows for it. That is, if you're trying to show that something is a permutation of something else, then say that its multiset of elements stays the same. There are some examples of this in Test/dafny4, and also see Test/dafny3/GenericSort.dfy.

My solution does a number of things, which may be helpful in other situations as well. Let me highlight a few of them.

One difficulty with the example is the existential quantifier in the postcondition. Actually, the problem is not so much the existential as it is the fact that the existential sits inside a universal quantifier whose bound variable (b) does not have any good trigger. Therefore, even a proof attempt like this:
assume forall b:: 0<=b<A.Length ==> exists a:: 0<=a<A.Length && A[a]==b;
assert forall b:: 0<=b<A.Length ==> exists a:: 0<=a<A.Length && A[a]==b;
does not go through. To solve this, one needs to trick Dafny into seeing the connection between the two universal quantifiers--that is, that one is used to prove the other. As described in other posts (like your Using pointless Id to help instantiation), you could introduce some dummy function and let the automatically inferred triggers take care of it. In this example, however, you can do essentially that, but at the same time making the text more readable. I suggest:
assume forall b :: 0 <= b < A.Length ==> InRange(A, b);
assert forall b :: 0 <= b < A.Length ==> InRange(A, b);
It is nice to write set comprehensions in the program text. But these are also tricky for the verifier, especially the most general form, set x | R(x) :: T(x), which says to form the set consisting of terms like T(x) where x ranges over values satisfying R(x). Even the simpler and more common form, set x | P(x), which says to form the set consisting of those values x that satisfy P(x), can be difficult. The reason for this is that, behind the scenes, such set comprehensions are turned into named functions that return the desired set. The names of these functions are generated to be different for each textual occurrence of a set comprehension in the program. Therefore--especially if these happen to sit inside quantifiers--it can happen that different textual occurrences of the seemingly same set comprehension are not necessarily recognized as being the same.

In my program above, I solved this problem by introducing a function for a common form of set comprehension, namely a set consisting of consecutive integers:
function IntSet(lo: int, hi: int): set<int>
  set i | lo <= i < hi
This made several of the proof obligations go through, and at the same time--I think--improved the readability of the program text.

If you're writing a property involving the equality of two sets, where one set is a set comprehension, it can sometimes be advantageous to write, say,
forall b :: b in R && b in m ==> false
instead of
R * (set b | b in m) == {}
However, in my solution to the problem, either of these worked fine.

Here are several other things to note about my program:
  • I wrote lemma instead of ghost method, but these are essentially synonyms.
  • The lemma uses a loop to compute the inverse-of-A map m. There's nothing wrong with a loop inside a lemma. :)
  • The forall statement at the end uses an unbounded range for b. That's fine (since we're inside a ghost context anyway).
  • When the body of a forall statement (without an explicit ensures clause) is a calc, then the "exported" conclusion of the calculation automatically gets placed in an ensures clause for the forall. If you're using the Dafny IDE in Visual Studio, you can hover the mouse over the forall keyword to see the auto-generated ensures clause.
  • The expression b in m, where m is a map says that b is in the domain of m. This seemed convenient at the time maps were introduced in Dafny, but I think I will change this in the future to instead provide names for the domain and range of maps. Perhaps one will then write something like b in m.Domain instead.
  • During the development of this proof, I had introduced many more proof lines than in this final version. The experience I've had with this before (and that others seem to have, too) is that with all that extra proof stuff lying around, verification times are longer. But once I got the whole proof into place, I discovered, by trial and error, that Dafny didn't need nearly as many hints as I had supplied. Extra proof lines can be nice for the human reader, and if they are, it may be nice to keep them in the final version. However, in this case, I thought the extra proof lines I had introduced were mostly noise, so I deleted (most of) them.