From ad6b00ea28f55dbfc6c6d6cb95ca31f9985c2e79 Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Fri, 5 Nov 2021 20:09:54 -0700
Subject: [PATCH 1/3] feat: Multiset lemmas

A few lemmas with multisets that are useful.
---
 src/Collections/Multiset/Multiset.dfy        | 46 ++++++++++++++++++++
 src/Collections/Multiset/Multiset.dfy.expect |  2 +
 src/Collections/Sequences/Seq.dfy            | 39 +++++++++++++++++
 src/Collections/Sequences/Seq.dfy.expect     |  2 +-
 4 files changed, 88 insertions(+), 1 deletion(-)
 create mode 100644 src/Collections/Multiset/Multiset.dfy
 create mode 100644 src/Collections/Multiset/Multiset.dfy.expect

diff --git a/src/Collections/Multiset/Multiset.dfy b/src/Collections/Multiset/Multiset.dfy
new file mode 100644
index 00000000..e3d35bd7
--- /dev/null
+++ b/src/Collections/Multiset/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;
+  }
+}
diff --git a/src/Collections/Multiset/Multiset.dfy.expect b/src/Collections/Multiset/Multiset.dfy.expect
new file mode 100644
index 00000000..ebe2328e
--- /dev/null
+++ b/src/Collections/Multiset/Multiset.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy
index 060168dd..6f8ab4dd 100644
--- a/src/Collections/Sequences/Seq.dfy
+++ b/src/Collections/Sequences/Seq.dfy
@@ -766,4 +766,43 @@ module Seq {
     }
   }
 
+  /* If the multiset of a is a subset of the multiset of b,
+   * then every item in a is in b.
+   */
+  lemma LemmaMultisetSubsetImpliesSeqMemebership<T>(a: seq<T>, b: seq<T>)
+    requires multiset(a) <= multiset(b)
+    ensures forall i | i in a :: i in b
+  {
+    if |a| == 0 {
+    } else {
+      assert multiset{First(a)} <= multiset(b);
+      assert First(a) in b;
+      assert a == [First(a)] + a[1..];
+      LemmaMultisetSubsetImpliesSeqMemebership(a[1..], b);
+    }
+  }
+
+  /* Every item in the parts to be flattend
+   * is in the flattened seq.
+   */
+  lemma LemmaFlattenMembership<T>(parts: seq<seq<T>>, flat: seq<T>)
+    requires Flatten(parts) == flat
+    ensures forall index
+    | 0 <= index < |parts|
+    :: multiset(parts[index]) <= multiset(flat)
+    ensures multiset(Flatten(parts)) == multiset(flat)
+    ensures forall part | part in parts
+    :: (forall i | i in part :: i in flat)
+    ensures forall i | i in flat
+    :: (exists part | part in parts :: i in part)
+  {
+    if |parts| == 0 {
+    } else {
+      assert multiset(First(parts)) <= multiset(flat);
+      assert parts == [First(parts)] + parts[1..];
+      assert flat ==  First(parts) + Flatten(parts[1..]);
+      LemmaFlattenMembership(parts[1..], Flatten(parts[1..]));
+    }
+  }
+
 }
diff --git a/src/Collections/Sequences/Seq.dfy.expect b/src/Collections/Sequences/Seq.dfy.expect
index 808136c6..c01e9601 100644
--- a/src/Collections/Sequences/Seq.dfy.expect
+++ b/src/Collections/Sequences/Seq.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 71 verified, 0 errors
+Dafny program verifier finished with 73 verified, 0 errors

From 2dc963cb97a2799f94af0c665f4c92e6cc599240 Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Tue, 9 Nov 2021 16:56:03 -0800
Subject: [PATCH 2/3] Update src/Collections/Sequences/Seq.dfy.expect

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
---
 src/Collections/Sequences/Seq.dfy.expect | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Collections/Sequences/Seq.dfy.expect b/src/Collections/Sequences/Seq.dfy.expect
index c01e9601..ef71487d 100644
--- a/src/Collections/Sequences/Seq.dfy.expect
+++ b/src/Collections/Sequences/Seq.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 73 verified, 0 errors
+Dafny program verifier finished with 74 verified, 0 errors

From c9d51d4b54a56e7daba8813ce777da7a2da3e8ae Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Tue, 9 Nov 2021 16:56:30 -0800
Subject: [PATCH 3/3] Update src/Collections/Multiset/Multiset.dfy

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
---
 src/Collections/Multiset/Multiset.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Collections/Multiset/Multiset.dfy b/src/Collections/Multiset/Multiset.dfy
index e3d35bd7..88edf33a 100644
--- a/src/Collections/Multiset/Multiset.dfy
+++ b/src/Collections/Multiset/Multiset.dfy
@@ -16,7 +16,7 @@ module Multiset {
 
   /* 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>)
+  lemma LemmaCardinalityOfToSetBound<T>(m: multiset<T>)
     ensures |ToSet(m)| <= |m| 
   {
     reveal ToSet();