Dafny序列转多重集引理无法自动证明的解决方案咨询

注意：绝对不要随意把可证的性质加为公理，一旦公理和内置理论冲突会导致整个证明体系出现矛盾，后续开发会出现大量不可排查的验证错误。该结论属于Dafny内置理论覆盖的恒真命题，完全可以被验证器正常证明。

• 验证失败核心原因：Dafny对序列转多重集的操作内置了拼接恒等规则：对任意序列s1、s2，永远满足multiset(s1 + s2) == multiset(s1) + multiset(s2)。你的前提中已经给出multiset(nums[1..]) == ms，而长度大于0的序列nums天然等价于单元素序列[nums[0]]和子序列nums[1..]的拼接。原代码没有显式触发这个序列拆分的重写规则，反而手动添加了大量逐元素计数的中间断言，额外增加了验证器的证明目标，最终导致验证卡住。

可直接通过验证的实现 #

原代码中所有手动写的逐元素断言都可以删除，只需要显式声明序列拆分的等式触发内置重写规则即可：

lemma multisetSequence(nums: seq<int>, ms: multiset<int>) 
    requires |nums| > 0
    requires multiset(nums[1..]) == ms;
    ensures multiset(nums) == ms + multiset{nums[0]}
{
    // 触发内置重写：nums等价于首元素拼接后续子序列
    assert nums == [nums[0]] + nums[1..];
}

上述代码不需要额外补充其他证明步骤，Dafny可直接验证通过。

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