Trying to prove a set to be the union of its singleton sets in Dafny

Question

I have the following code:

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}

But cannot manage to give a suitable body to

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

In particular when trying induction I seem to need using the function pick again and this might give a result different from the one obtained when invoking U.

Answer 1

You are correct, that is something you should be concerned with. Check out the essay "Functions over Set Elements" here for an example of how to deal with that situation. https://leino.science/dafny-power-user/

predicate AllIn<T>(S: set<set<T>>, SU: set<T>) {
  forall xx :: xx in S ==> forall y :: y in xx ==> y in SU
}

predicate AllSingletonSets<T>(S: set<set<T>>) {
  forall ss :: ss in S ==> |ss| == 1
}

ghost function U<T> (S : set<set<T>>) : set<T>
  //requires AllSingletonSets(S); //This is optional it works either way
  ensures AllIn(S, U(S))
{
  if S == {} then 
    // assert AllIn(S, {});
    {}
  else
    var s := pick (S);
    var result := U (S - {s}) + s;
    // assert AllIn(S-{s}, U(S-{s}));
    // var x :| x in s;
    // assert x in s;
    // assert x in  result;

    //This is needed to show extensionality to Dafny
    assert S - {s} + {s} == S;
    // assert AllIn(S, result);
    result
} 

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