dafnyformal-verification

In Dafny, show that a sequence of unique elements has the same size as the set of the same elements


I've created a verified SortedMap in Dafny. It is a sequence of (key, value) pairs. The keys are sorted, distinct integers. I can't figure how to show that the length of the "KeySet" must be equal to the length of the sequence.

-- Carl

Error:

this is the postcondition that could not be proved
  |
7 |   ensures |KeySet(sorted_seq)| == |sorted_seq|

Simplifed code:

predicate SortedSeq(sequence: seq<(int, int)>) {
  forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}

function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  set i | i in sorted_seq :: i.0
}


method Main()
{
  var s: seq<(int,int)> := [(1, 2), (30, 40), (50, 50)];
  print KeySet(s);

}

Solution

  • This property requires a proof by induction. Since the way you defined the function is not recursive, this is not easy to do in Dafny. You can either (1) prove the property in a separate inductive lemma, or (2) change the definition to be recursive.

    (1)

    function KeySet(sorted_seq: seq<(int, int)>): set<int>
    {
      set i | i in sorted_seq :: i.0
    }
    
    lemma KeySetSize(sorted_seq: seq<(int, int)>)
      requires SortedSeq(sorted_seq)
      ensures |KeySet(sorted_seq)| == |sorted_seq|
    {
      if sorted_seq == [] {
      } else {
        assert KeySet(sorted_seq) == {sorted_seq[0].0} + KeySet(sorted_seq[1..]);
        KeySetSize(sorted_seq[1..]);
      }
    }
    
    // You can optionally then recombined the bare function and lemma 
    // into a function with the right specification.
    function KeySetWithPost(sorted_seq: seq<(int, int)>): set<int>
      requires SortedSeq(sorted_seq)
      ensures |KeySetWithPost(sorted_seq)| == |sorted_seq|
    {
      KeySetSize(sorted_seq);
      KeySet(sorted_seq)
    }
    

    (2)

    function KeySet(sorted_seq: seq<(int, int)>): set<int>
      requires SortedSeq(sorted_seq)
      ensures |KeySet(sorted_seq)| == |sorted_seq|
      ensures KeySet(sorted_seq) == set i | i in sorted_seq :: i.0
    {
      if sorted_seq == [] then
        {}
      else
        {sorted_seq[0].0} + KeySet(sorted_seq[1..])
    }
    
    // Notice the extra postcondition above, which is required for the proof
    // to go through. Once the proof is done, you can wrap it in a function
    // with no extra postcondition.
    function KeySetWithoutExtraPost(sorted_seq: seq<(int, int)>): set<int>
      requires SortedSeq(sorted_seq)
      ensures |KeySet(sorted_seq)| == |sorted_seq|
    {
      KeySet(sorted_seq)
    }