Maps: add MapKeys, MapValues, and related helpers

examples/Collections/Maps/Maps.dfy

@@ -0,0 +1,24 @@
+// RUN: %verify "%s"
+
+/*******************************************************************************
+ * Copyright by the contributors to the Dafny Project
+ * SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+include "../../../src/Functions.dfy"
+include "../../../src/Collections/Maps/Maps.dfy"
+
+module {:options "--function-syntax:4"} MapsExamples {
+  import Functions
+  import Maps
+
+  function ByteKeyMapToIntKeys<Y>(m: map<bv8, Y>): (m': map<int, Y>)
+  {
+    Maps.MapKeys(m, b => b as int)
+  }
+
+  function ByteValueMapToIntValues<X>(m: map<X, bv8>): (m': map<X, int>)
+  {
+    Maps.MapValues(m, b => b as int)
+  }
+}

src/Collections/Maps/Maps.dfy

@@ -1,18 +1,22 @@
 // RUN: %verify "%s"
 
 /*******************************************************************************
- *  Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, 
- *  ETH Zurich, and University of Washington
- *  SPDX-License-Identifier: BSD-2-Clause 
- * 
- *  Modifications and Extensions: Copyright by the contributors to the Dafny Project
- *  SPDX-License-Identifier: MIT 
- *******************************************************************************/
+ * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University,
+ * ETH Zurich, and University of Washington
+ * SPDX-License-Identifier: BSD-2-Clause
+ *
+ * Modifications and Extensions: Copyright by the contributors to the Dafny Project
+ * SPDX-License-Identifier: MIT
+ ******************************************************************************/
 
 include "../../Wrappers.dfy"
+include "../../Functions.dfy"
+include "../Sets/Sets.dfy"
 
 module {:options "-functionSyntax:4"} Maps {
   import opened Wrappers
+  import Functions
+  import Sets
 
   function Get<X, Y>(m: map<X, Y>, x: X): Option<Y>
   {
@@ -93,6 +97,39 @@ module {:options "-functionSyntax:4"} Maps {
     forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x']
   }
 
+  ghost predicate {:opaque} Contains<X, Y>(big: map<X, Y>, small: map<X, Y>)
+  {
+    && small.Keys <= big.Keys
+    && forall x <- small :: small[x] == big[x]
+  }
+
+  lemma LemmaContainsPreservesInjectivity<X, Y>(big: map<X, Y>, small: map<X, Y>)
+    requires Contains(big, small)
+    requires Injective(big)
+    ensures Injective(small)
+  {
+    reveal Contains();
+    reveal Injective();
+  }
+
+  lemma LemmaInjectiveImpliesUniqueValues<X(!new), Y>(m: map<X, Y>)
+    requires Injective(m)
+    ensures |m.Keys| == |m.Values|
+  {
+    if |m| > 0 {
+      var x: X :| x in m;
+      var y := m[x];
+      var m' := Remove(m, x);
+      reveal Contains();
+      assert Contains(m, m');
+
+      reveal Injective();
+      assert m'.Values == m.Values - {y};
+      LemmaContainsPreservesInjectivity(m, m');
+      LemmaInjectiveImpliesUniqueValues(m');
+    }
+  }
+
   /* Swaps map keys and values. Values are not required to be unique; no
   promises on which key is chosen on the intersection. */
   ghost function {:opaque} Invert<X, Y>(m: map<X, Y>): map<Y, X>
@@ -127,4 +164,33 @@ module {:options "-functionSyntax:4"} Maps {
     forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x']
   }
 
+  /* Maps an injective function over the keys of a map, retaining the values. */
+  function {:opaque} MapKeys<X(!new), Y, X'>(m: map<X, Y>, f: X --> X'): (m': map<X', Y>)
+    reads f.reads
+    requires forall x {:trigger f.requires(x)} :: f.requires(x)
+    requires Functions.Injective(f)
+    ensures |m'| == |m|
+    ensures m'.Values == m.Values
+    ensures forall x | x in m :: f(x) in m' && (m'[f(x)] == m[x])
+  {
+    var m' := map k <- m :: f(k) := m[k];
+    Sets.LemmaMapSize(m.Keys, m'.Keys, f);
+    m'
+  }
+
+  /* Maps a function over the values of a map, retaining the keys. */
+  function {:opaque} MapValues<X, Y(!new), Y'>(m: map<X, Y>, f: Y --> Y'): (m': map<X, Y'>)
+    reads f.reads
+    requires forall y {:trigger f.requires(y)} :: f.requires(y)
+    ensures |m'| == |m|
+    ensures m'.Keys == m.Keys
+    ensures forall x | x in m :: m'[x] == f(m[x])
+  {
+    var m' := map x <- m :: x := f(m[x]);
+    assert |m'| == |m| by {
+      assert m'.Keys == m.Keys;
+      assert |m'.Keys| == |m.Keys|;
+    }
+    m'
+  }
 }