# Dafny: Permutations, sequences and multisets

Dafny has support for multisets, which are really useful for reasoning about programs that permute, or otherwise deal with permutations, of sequences or arrays.

```predicate Subpermutation(xs:seq, ys:seq) ensures Subpermutation(xs,ys) ==> forall x :: x in xs ==> x in ys; { assert forall x :: x in xs ==> x in multiset(xs); multiset(xs) <= multiset(ys) }   // THEOREM lemma SubpermutationIsSmaller(xs:seq, ys:seq) requires Subpermutation(xs,ys); ensures |xs| <= |ys|; { assert |multiset(xs)| == |xs|; assert |multiset(ys)| == |ys|;   var xs',ys' := xs,ys;   var XS',YS' := multiset(xs),multiset(ys); var XS'',YS'' := multiset{},multiset{}; while(|XS'|>0) invariant Subpermutation(xs',ys'); invariant XS' == multiset(xs'); invariant YS' == multiset(ys'); invariant XS' + XS'' == multiset(xs); invariant YS' + YS'' == multiset(ys); invariant XS'' == YS''; invariant XS' <= YS'; { assert RemoveFromSequenceReducesMultiSet(xs,multiset(xs),multiset(xs[1..])); var x := xs'; xs' := Remove(x,xs');   ys' := Remove(x,ys');   XS' := XS'[x := XS'[x] - 1]; XS'' := XS''[x := XS''[x] + 1]; YS' := YS'[x := YS'[x] - 1]; YS'' := YS''[x := YS''[x] + 1]; } }   // SUPPORTING DEFINITIONS   // following is a function lemma predicate RemoveFromSequenceReducesMultiSet(xs:seq<T>, XS:multiset<T>, XS':multiset<T>) requires xs != []; requires XS' == multiset(xs[1..]); ensures XS' == multiset(xs)[xs := multiset(xs)[xs] - 1]; ensures RemoveFromSequenceReducesMultiSet(xs,XS,XS'); { assert [xs]+xs[1..] == xs; assert multiset([xs]+xs[1..]) == multiset(xs); true }   function Remove(x:T, xs:seq<T>) :seq<T> requires x in xs; ensures multiset(Remove(x,xs)) == multiset(xs)[x := multiset(xs)[x] - 1]; ensures |Remove(x,xs)|+1 == |xs|; { assert RemoveFromSequenceReducesMultiSet(xs,multiset(xs),multiset(xs[1..])); if xs==x then xs[1..] else [xs] + Remove(x,xs[1..]) }```

# Dafny Triggers

It is possible to write tiggers for particular quantifiers in Dafny programs.

```predicate P(x:int) { true }   lemma ThereIsMoreThanOneInteger(x:int) ensures exists z:int :: z!=x; { // can't prove }   lemma NoReallyThereIsMoreThanOneInteger(x:int) ensures exists z:int {:trigger P(z)} :: z!=x; { assert P(x+1); // can prove }```