CODEWITHSUNDEEP
duplicatessetsequencedafnymultiset
Markel Barrena
Markel Barrena

Reputation: 3

Sequence relations with multisets

I am trying to verify the following lemma in dafny:

ghost predicate noD(s: seq<nat>)
{
    forall i :: 0<=i <|s| ==> !(exists j :: 0<=j< |s| && i!=j && s[i]==s[j])
}

lemma sequence_multiset_relation_lemma(s0: seq<nat>, s1: seq<nat>)
    requires noD(s1)
    requires multiset(s0) == multiset(s1)
    ensures noD(s0)
{}

It basically states that if one sequence have no duplicated elements, then other sequences with the same elements won't have duplicated elements.

However, Dafny seems to struggle when linking properties between sequences and their respective multisets.

This is what I've tried so far:

lemma sequence_multiset_relation_lemma(s0: seq<nat>, s1: seq<nat>)
    requires noD(s1)
    requires multiset(s0) == multiset(s1)
    ensures noD(s0)
{
    if !noD(s0) //contradiction
    {
        var i0 :| 0<=i0<|s0| && (exists j :: 0<=j<|s0| && j!=i0 && s0[j]==s0[i0]);
        var j0 :| 0<=j0<|s0| && j0!=i0 && s0[j0]==s0[i0];
        assert s0[i0] == s0[j0] && i0!=j0;
        var e1 := s0[i0];
        var e2 := s0[j0];
        assert e1 == e2;
        assert e1 in multiset(s0) && e2 in multiset(s0);
        assert e1 in multiset(s1) && e2 in multiset(s1);
        duplicates_imply_multiset_count(s0, e1, i0, j0);
        assert multiset(s0)[(e1)]>1;
        assert multiset(s1)[(e1)]>1;
        assert exists i :: 0<=i<|s1| && (exists j :: 0<=j<|s1| && s1[j]==s1[i] && j!=i);    //assertion might not hold
}

Can anybody help me figure out how to verify this? Thanks!

Upvotes: 0

Views: 56

Answers (0)

Related Questions