Multiset proof verification in dafny

user_17349751 0
Viewed 95

I'm trying to prove a little lemma for a larger proof, the lemma definition is below:

lemma LoopLemma(a: seq<int>, b: seq<int>, c: seq<int>, k:int, i:int, j:int)
    requires 0 <= i < |a| && 0<= j < |b| && 0 <= k < |c| && i +j ==k && |a| + |b| == |c|
    requires Sorted(c[..k]) && Sorted(b) && Sorted(a) 
    requires multiset(c[..k]) == multiset(a[..i]+b[..j])
    ensures Sorted(c[..k]+[b[j]]) && Sorted(c[..k]+[a[i]])
    
{
    assert multiset(c[..k]) == multiset(a[..i]+b[..j]);
    var q:=a[..i]+b[..j];
    var c1 := c[..k];
    assert Sorted(c1);
    assert multiset(c1) == multiset(q);
    assert |q| == i + j;
    assert |c1| == k == i + j;
    calc {
        multiset(c1) == multiset(q);
        == 
        forall l :: l in multiset(c1) ==> l in multiset(q);
        == {assert forall l :: l in multiset(q) ==> exists r :: 0 <= r <|q| && l == q[r]; assert forall l :: l in multiset(c1) ==> exists r :: 0 <= r <|c1| && l == c1[r];}
        forall l :: 0<=l <|c1| ==> exists r :: 0 <= r < |q| && q[r] == c1[l];

        
    }
}

I get "the calculation step between the previous line and this line might not hold" for the last step, and I don't understand why. All I'm saying there is that if the multisets of two sequences are equal, for any entry in the first sequence exists an entry in the second sequence with the same value. I tried some simpler examples (where I define the sequences explicitly) and it worked. Maybe I don't understand something about multisets?

Any suggestions will help.

dafny
1 Answers

Additional hint that needed here is every element in sequence is in multiset i.e forall i :: 0 <= i < |c[..k]| ==> c[..k][i] in multiset(c[..k]) (hint in forward direction of reasoning). Following snippet verifies.

predicate Sorted(a: seq<int>)
{
   if |a| <= 1 then true else (a[0] <= a[1]) && Sorted(a[1..])
}

lemma LoopLemma(a: seq<int>, b: seq<int>, c: seq<int>, k: int, i: int, j: int)
   requires 0 <= i < |a| && 0 <= j < |b| && 0 <= k < |c| && i + j == k   && |a| + |b| == |c|
   requires Sorted(c[..k]) && Sorted(a) && Sorted(b)
   requires multiset(c[..k]) == multiset(a[..i] + b[..j])
{
   var s := a[..i] + b[..j];
   calc {
      multiset(c[..k]) == multiset(s);
      forall e :: e in multiset(c[..k]) ==> e in multiset(s);
      {
         assert forall e :: e in multiset(c[..k]) ==> 
                exists r :: 0 <= r < |s| && s[r] == e;
         // assert forall e :: e in multiset(c[..k]) ==> 
         //        exists r :: 0 <= r < |c[..k]| && c[..k][r] == e;
         assert forall i :: 0 <= i < |c[..k]| ==> c[..k][i] in multiset(c[..k]);
      }
      forall i :: 0 <= i < |c[..k]| ==> exists r :: 0 <= r < |s| && s[r] == c[..k][i];
   }
}
user_144130690
Related