为何该Dafny引理无法自动证明？如何手动完成证明？

数据老陈

2026-6-13

Dafny引理证明问题解析

为什么自动证明失败？

Dafny的自动定理 prover 不会自动关联多重集（multiset）与序列成员关系（!in）的底层定义。虽然逻辑上等价多重集的成员存在性必然一致，但Dafny无法直接推断出“序列中不存在某元素”等价于“该元素在序列对应多重集中的计数为0”这层关联，必须手动引导它完成定义展开和逻辑推导。

手动证明方法

可以通过展开核心定义、结合逻辑链式推导来完成证明，以下是两种实现方式：

方式1：分步断言推导

lemma ElementExclusionLemma<T>(seqa: seq<T>, seqb: seq<T>, x: T)
  ensures multiset(seqa) == multiset(seqb) ==> (x !in seqa ==> x !in seqb)
{
  // 假设前提条件成立
  assume multiset(seqa) == multiset(seqb);
  assume x !in seqa;
  
  // 展开序列成员关系的本质：不在序列中 = 多重集计数为0
  assert count(multiset(seqa), x) == 0;
  // 利用多重集等价的前提，迁移计数结果到seqb
  assert count(multiset(seqb), x) == 0;
  // 反向推导回序列成员关系
  assert x !in seqb;
}

方式2：用calc块做链式推导（更简洁）

lemma ElementExclusionLemma<T>(seqa: seq<T>, seqb: seq<T>, x: T)
  ensures multiset(seqa) == multiset(seqb) ==> (x !in seqa ==> x !in seqb)
{
  calc {
    x !in seqa;
    ==> { 序列成员关系的定义 }
    count(multiset(seqa), x) == 0;
    ==> { 利用multiset等价的前提 }
    count(multiset(seqb), x) == 0;
    ==> { 序列成员关系的定义反向推导 }
    x !in seqb;
  }
}