search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

Need inverse of LemmaCardinalityOfSetNoDuplicates #18

Closed robin-aws closed 2 years ago

robin-aws commented 2 years ago

This lemma proves this implication:

  lemma LemmaCardinalityOfSetNoDuplicates<T>(s: seq<T>)
    requires HasNoDuplicates(s)
    ensures |ToSet(s)| == |s|

But the opposite implication would also be very useful:

  lemma LemmaNoDuplicatesCardinalityOfSet<T>(s: seq<T>)
    requires |ToSet(s)| == |s|
    ensures HasNoDuplicates(s)

Especially because |ToSet(s)| == |s| is much cheaper to evaluate at runtime than HasNoDuplicates(s) would be (if it was a compiled function method)

gancherj commented 2 years ago

Created pull request. Please let me know if any style fixes are needed :)