1

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.

Theo Deep
  • 666
  • 4
  • 15
  • 1
    If your program verifies, you can safely ignore this warning. See [this answer](https://stackoverflow.com/questions/49398650/dafny-what-does-no-terms-found-to-trigger-on-mean). – James Wilcox Apr 08 '21 at 15:12
  • Completely, my concern in this case is that I would like to know how to manually select the trigger for this example. – Theo Deep Apr 08 '21 at 15:30

1 Answers1

1

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.

James Wilcox
  • 5,307
  • 16
  • 25
  • Whoa, thanks a lot, that is the idea I was suggesting on my Edit. However, that last `forall` with `ensures` is a mind-blow for me, and have never seen it. Did not know that `::` could be replaced with `|` either. There is always something new to know about Dafny, maybe I should read a complete manual. As always, lots of thanks, mate :) – Theo Deep Apr 08 '21 at 20:08
  • 1
    yeah, there are a ton of features :) the "forall statement" is definitely a good one to know – James Wilcox Apr 08 '21 at 22:43