如何在Dafny循环中证明序列拆分后的多重集相等？

直接利用内置序列性质 #

Dafny原生支持序列分割拼接的基本等式：对于任意满足0 <= i <= |seqa|的索引i，seqa[..i] + seqa[i..] == seqa必然成立。而multiset构造是保等式的——只要两个序列相等，它们的multiset就一定相等。

你可以在目标断言前添加一步辅助断言，让验证器自动完成推导：

assert seqa[..i] + seqa[i..] == seqa;
assert multiset(seqa) == multiset(seqa[..i] + seqa[i..]);

用归纳法手动引导验证（如果需要） #

既然你已经验证了i=0的基础情况，可通过补充归纳步骤完成证明：

1. 归纳假设：假设当i=k时，multiset(seqa) == multiset(seqa[..k] + seqa[k..])成立
2. 推导i=k+1的情况：

   // 拆分k+1位置的序列切片
   assert seqa[..k+1] == seqa[..k] + [seqa[k]];
   assert seqa[k..] == [seqa[k]] + seqa[k+1..];
   // 利用序列拼接的结合律替换
   assert seqa[..k+1] + seqa[k+1..] == seqa[..k] + seqa[k..];
   // 结合归纳假设得出结论
   assert multiset(seqa) == multiset(seqa[..k+1] + seqa[k+1..]);
   

补充循环不变量 #

直接将multiset(seqa) == multiset(seqa[..i] + seqa[i..])加入你的循环不变量集合中。结合已有的0 <= i <= |seqa|不变量，Dafny验证器会自动检查该性质在循环初始化（i=0）和每次迭代后的保持性。如果验证器无法自动完成，再插入上述辅助断言引导推导。

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