Search code examples
triggersz3theorem-provingdafnymultiset

Trigger Dafny with multisets


This lemma verifies, but it raises the warning Not triggers found:

lemma multisetPreservesGreater (a:seq<int>, b:seq<int>, c:int, f:int, x:int)
       requires |a|==|b| && 0 <= c <= f + 1 <= |b| 
       requires (forall j :: c <= j <= f ==> a[j] >= x)
       requires multiset(a[c..f+1]) == multiset(b[c..f+1])
       ensures (forall j :: c <= j <= f ==> b[j] >= x)
{

       assert (forall j :: j in multiset(a[c..f+1]) ==> j in multiset(b[c..f+1]));

}

I do not know how to instantiate this trigger (cannot instantiate it as a function, or can I?). Any help?

Edit: Maybe I can instantiate a method f such that takes an array and inserts it in a multiset, and therefore I can trigger f(a), but that does not mention i. I will try.


Solution

  • Here's one way to transform the program so that there are no trigger warnings.

    function SeqRangeToMultiSet(a: seq<int>, c: int, f: int): multiset<int>
      requires 0 <= c <= f + 1 <= |a|
    {
      multiset(a[c..f+1])
    }
    
    lemma multisetPreservesGreater (a:seq<int>, b:seq<int>, c:int, f:int, x:int)
           requires |a|==|b| && 0 <= c <= f + 1 <= |b| 
           requires (forall j :: c <= j <= f ==> a[j] >= x)
           requires multiset(a[c..f+1]) == multiset(b[c..f+1])
           ensures (forall j :: c <= j <= f ==> b[j] >= x)
    {
           assert forall j :: j in SeqRangeToMultiSet(a, c, f) ==> j in SeqRangeToMultiSet(b, c, f);
           forall j | c <= j <= f
            ensures b[j] >= x
           {
            assert b[j] in SeqRangeToMultiSet(b, c, f);
           }
    }
    

    The point is that we introduce the function SeqRangeToMultiSet to stand for a subexpression that is not a valid trigger (because it contains arithmetic). Then SeqRangeToMultiSet itself can be the trigger.

    The downside of this approach is that it decreases automation. You can see that we had to add a forall statement to prove the postcondition. The reason is that we need to mention the trigger, which does not appear in the post condition.