如何在Dafny中证明集合是其单元素集合的并集

用户定义了以下Dafny函数：

ghost function U<T> (S : set<set<T>>) : set<T>
{
  if S == {} then {}
  else var s := pick(S);
       U(S - {s}) + s
} 

ghost function pick<T> (s : set<T>) : T
requires s != {}
{ var x :| x in s ; x }

需要证明的引理：

lemma singletonsU<T> (s : set<T>)
ensures s == U(set x <- s :: {x})

问题核心 #

问题出在pick函数的非确定性：U的递归实现依赖pick选择集合中的任意元素，但归纳证明时如果再次调用pick，无法保证和U内部的选择一致，导致逻辑链断裂。

解决思路 #

先证明U函数的本质是集合的广义并，即U(S)的结果与pick的选择无关，始终等于S中所有集合的并集。基于这个性质，再证明目标引理就会很简单。

步骤1：证明U的广义并性质

先写一个辅助引理，证明U(S)等于S中所有元素的并集：

lemma UIsUnion<T>(S: set<set<T>>)
ensures U(S) == union { t | t in S }
{
  if S == {} {
    // 基础情况：空集的并是空集
    assert U(S) == {};
    assert union { t | t in S } == {};
  } else {
    // 归纳步骤：取S中的任意元素s
    var s := pick(S);
    // 归纳假设：U(S - {s})是S-{s}的广义并
    UIsUnion(S - {s});
    // 展开U的定义并推导
    calc {
      U(S);
      U(S - {s}) + s;
      union { t | t in S - {s} } + s;
      union { t | t in S };
    }
  }
}

步骤2：证明目标引理singletonsU

利用上面的辅助引理，直接推导：

lemma singletonsU<T> (s : set<T>)
ensures s == U(set x <- s :: {x})
{
  // 调用辅助引理，将U转换为广义并
  UIsUnion(set x <- s :: {x});
  // 推导广义并结果
  calc {
    U(set x <- s :: {x});
    union { t | t in set x <- s :: {x} };
    s;
  }
}

关键说明 #

• 辅助引理UIsUnion通过集合归纳（Dafny会自动处理集合的归纳逻辑），证明了U的结果和pick的选择无关，本质就是广义并。
• 目标引理只需将U替换为广义并，再利用“所有单元素集合{x}的并集等于原集合s”的性质即可得证。

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