尝试在 Dafny 中证明一个集合是其单例集合的并集

Question

我有以下代码：

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

却无法给予合适的身体

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

特别是在尝试归纳时，我似乎需要使用该函数 再次选择，这可能会得到与获得的结果不同的结果 当调用 U 时。

Answer 1

你是对的，这是你应该关心的事情。 请查看文章“集合元素上的函数”，了解如何处理这种情况的示例。 https://leino.science/dafny-power-user/