如何在Dafny中验证序列与多重集关联的无重复元素引理？

我需要在Dafny中验证以下引理：若序列s1无重复元素，且序列s0的多重集与s1的多重集相等，则s0也无重复元素。但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)
{}

尝试的验证代码 #

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) // 反证法：假设s0有重复
    {
        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);    // 此断言无法通过
}

问题分析与解决方案 #

当前代码的核心问题是：Dafny无法自动将multiset(s1)[e1] > 1与s1存在重复元素这两个属性关联起来。需要补充一个辅助引理，明确“无重复序列的多重集中每个元素的计数必为1”这一逻辑关系，从而完成矛盾推导。

完整验证代码 #

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

// 辅助引理：无重复序列的多重集中，每个元素的计数不超过1
lemma noD_implies_multiset_count_at_most_one(s: seq<nat>)
    requires noD(s)
    ensures forall e :: multiset(s)[e] <= 1
{
    forall e | e in multiset(s)
    {
        if multiset(s)[e] > 1
        {
            // 取出序列中两个不同索引的相同元素
            var i, j :| 0<=i < |s| && 0<=j < |s| && i != j && s[i] == e && s[j] == e;
            // 该结论违反noD的定义，产生矛盾
            assert !noD(s);
        }
    }
}

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)
    {
        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 e := s0[i0];
        // 调用辅助引理，得到s1中所有元素的多重集计数都<=1
        noD_implies_multiset_count_at_most_one(s1);
        assert multiset(s1)[e] <= 1;
        
        // 从s0的重复元素推导出该元素在s0的多重集中计数>1
        assert multiset(s0)[e] > 1;
        // 结合s0与s1的多重集相等，得出矛盾
        assert multiset(s1)[e] > 1;
        // 矛盾说明原假设不成立，s0必无重复
    }
}

代码说明 #

1. 辅助引理noD_implies_multiset_count_at_most_one通过反证法证明：如果序列无重复，那么其多重集中每个元素的计数不会超过1。
2. 在主引理中，调用该辅助引理后，我们可以从s1无重复推导出multiset(s1)[e] <=1，而之前的推导已经得到multiset(s1)[e]>1，两者形成矛盾，从而证明原引理的结论s0无重复成立。

内容的提问来源于stack exchange，提问作者Markel Barrena