Dafny: Want to show that a sequence of sets == the set of the sequence (corrected)

I have sequences of (inclusive) integer ranges.e.g.: [(1,3), (40,40)] represents the set 1,2,3,40.

I'd like to show that appending two sequences is the same as taking the union of the sets they represent. It works when I append a range to the front, but not when I append it to the back.

In the code below, InsertBefore verifies, but InsertAfter fails with

This postcondition might not hold: SeqToSet(r) == SeqToSet(sorted_map0) + RangeToSet(pair)

Can/should I define SeqToSet to split the sequence non-deterministically?

-- Carl

code:

// *inclusive* range to set
function RangeToSet(pair: (int,int)): set<int>
  requires ValidPair(pair)
{
  set i | pair.0 <= i <= pair.1 :: i
}
predicate ValidPair(pair: (int,int)) {
  pair.0 <= pair.1
}
predicate ValidSeq(sequence: seq<(int, int)>) {
  forall p | p in sequence :: ValidPair(p)
}
function SeqToSet(sequence: seq<(int,int)>): set<int>
  decreases |sequence|
  requires ValidSeq(sequence)
{
  if |sequence| == 0 then {}
  else RangeToSet(sequence[0]) + SeqToSet(sequence[1..])
}

// Verifies
method InsertBefore(sorted_map0: seq<(int,int)>, pair: (int,int)) returns (r: seq<(int,int)>)
  requires ValidPair(pair)
  requires ValidSeq(sorted_map0)
  ensures ValidSeq(r)
  ensures SeqToSet(r) == SeqToSet(sorted_map0) + RangeToSet(pair)
{
  r := [pair] + sorted_map0;
}
// Fails
method InsertAfter(sorted_map0: seq<(int,int)>, pair: (int,int)) returns (r: seq<(int,int)>)
  requires pair.0 <= pair.1
  requires ValidSeq(sorted_map0)
  ensures ValidSeq(r)
  ensures SeqToSet(r) == SeqToSet(sorted_map0) + RangeToSet(pair)
{
  r := sorted_map0 + [pair];
}

I don't understand your definition of SortedAndDisjointSeq. If I modify definition to following, I am able to verify both assert.

predicate SortedAndDisjointSeq(sequence: seq<(int, int)>) {
  (forall p | p in sequence :: p.0 <= p.1) &&
  (forall i, j | 0 <= i < j < |sequence| :: (sequence[i].1 < sequence[j].0 || sequence[j].1 < sequence[i].0))
}

Further error in your code is function precondition can't be proved. It means s + [p] doesn't satisfy disjoint definition - which points out that your disjoint condition is somewhat wrong.

This is classic case of verification in one direction is easy and in another direction requires induction. For example proving 0 + n is equal to n might be easy compared to proving n + 0 equal to n. As + is defined using structural induction on first argument.

Here too we require induction (compared to InsertBefore which was easy and dafny can do proof automatically). Easiest way to do it to use recursion so that inductive argument is available to use in proof.

method InsertAfter(sorted_map0: seq<(int,int)>, pair: (int,int)) returns (r: seq<(int,int)>)
  requires pair.0 <= pair.1
  requires ValidSeq(sorted_map0)
  ensures ValidSeq(r)
  ensures SeqToSet(r) == SeqToSet(sorted_map0) + RangeToSet(pair)
{
  if sorted_map0 == [] {
     r := sorted_map0 + [pair];
  }
  else {
     var t := InsertAfter(sorted_map0[1..], pair);
     r := [sorted_map0[0]] +  t;
  }
} 

If you care about generated code and insist that direct version is fast. You can use ghost directive and prove same thing in this way where ghost declaration and while loop is stripped away in generated code and used only for proof.

method InsertAfterInline(sorted_map0: seq<(int,int)>, pair: (int,int)) returns (r: seq<(int,int)>)
  requires pair.0 <= pair.1
  requires ValidSeq(sorted_map0)
  ensures ValidSeq(r)
  ensures SeqToSet(r) == SeqToSet(sorted_map0) + RangeToSet(pair)
{
   r := sorted_map0 +  [pair];
   
   ghost var t := |sorted_map0|;
   ghost var mm := sorted_map0[t..];
   ghost var rr := [pair];

   while t > 0
     invariant 0 <= t <= |sorted_map0|
     invariant mm == sorted_map0[t..]
     invariant SeqToSet(mm + rr) == SeqToSet(mm) + RangeToSet(pair)
  {
     assert SeqToSet(mm + rr) == SeqToSet(mm) + RangeToSet(pair);
     t := t - 1;
     mm := sorted_map0[t..];
     calc {
        SeqToSet(mm + rr);
        {
          assert (mm + rr)[0] == mm[0];
          assert (mm + rr)[1..] == mm[1..] + rr;
        }
        RangeToSet(mm[0]) + SeqToSet(mm[1..] + rr);
        RangeToSet(mm[0]) + SeqToSet(mm[1..]) + RangeToSet(pair);
        SeqToSet(mm) + RangeToSet(pair);
     }
  }
}