Lemma to prove the opposite implication from Seq.LemmaCardinalityOfSetNoDuplicates

src/Collections/Multisets/Multiset.dfy

@@ -0,0 +1,46 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT 
+*******************************************************************************/
+
+module Multiset {
+
+  /* converts a multiset to a set */
+  function method {:opaque} ToSet<T>(s: multiset<T>): set<T> 
+  {
+    set x: T | x in s
+  }
+
+  /* proves that the cardinality of a multiset is always more than or equal to that
+  of the conversion to a set */
+  lemma LemmaCardinalityOfSetBound<T>(m: multiset<T>)
+    ensures |ToSet(m)| <= |m| 
+  {
+    reveal ToSet();
+    if |m| == 0 {
+    } else {
+      var x :| x in m;
+      var xs := multiset{}[x := m[x]];
+      assert ToSet(xs) == {x};
+      var rest := m - xs;
+      LemmaCardinalityOfSetBound(rest);
+      assert ToSet(m) == ToSet(xs) + ToSet(rest);
+    }
+  }
+
+  lemma LemmaCardinalityOfSetWithDuplicates<T>(m: multiset<T>, x: T)
+    requires m[x] > 1
+    ensures |ToSet(m)| < |m| 
+  {
+    reveal ToSet();
+    var xs := multiset{}[x := m[x]];
+    assert ToSet(xs) == {x};
+    var rest := m - xs;
+    LemmaCardinalityOfSetBound(rest);
+    assert ToSet(m) == ToSet(xs) + ToSet(rest);
+    assert |xs| > 1;
+  }
+}

src/Collections/Multisets/Multiset.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors

src/Collections/Sequences/Seq.dfy

@@ -14,13 +14,15 @@
 *  SPDX-License-Identifier: MIT 
 *******************************************************************************/
 
+include "../Multisets/Multiset.dfy"
 include "../../Wrappers.dfy"
 include "../../Math.dfy"
 
 module Seq {
 
   import opened Wrappers
   import Math
+  import Multiset
 
   /**********************************************************
   *
@@ -200,6 +202,26 @@ module Seq {
     }
   }
 
+  /* A sequence that converts to a set of the same cardinality has no duplicates  */
+  lemma LemmaNoDuplicatesCardinalityOfSet<T>(s: seq<T>)
+    requires |ToSet(s)| == |s|
+    ensures HasNoDuplicates(s)
+  {
+    reveal HasNoDuplicates();
+    reveal ToSet();
+    reveal Multiset.ToSet();
+    // Proof by contrapositive: if there is a duplicate, then the cardinality of the
+    // set would be strictly less than that of the sequence, which contradicts the precondition.
+    if i,j :| 0 <= i < j < |s| && s[i] == s[j] {
+      var x := s[i];
+      assert s == s[..j] + s[j..];
+      assert multiset(s)[x] >= 2;
+      Multiset.LemmaCardinalityOfSetWithDuplicates(multiset(s), x);
+      assert ToSet(s) == Multiset.ToSet(multiset(s));
+      assert |ToSet(s)| < |s|;
+     }
+  }
+
   /* proves that there are no duplicate values in the multiset version of the sequence */
   lemma LemmaMultisetHasNoDuplicates<T>(s: seq<T>)
     requires HasNoDuplicates(s)

src/Collections/Sequences/Seq.dfy.expect

@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 69 verified, 0 errors
+Dafny program verifier finished with 70 verified, 0 errors