Items of Map

[dreamqin68]

Hi,

I am experiencing an issue with map.Items. For example,

lemma mapTest()
{
    var map1 := map['a' := 0, 'b':= 6];
    assert ('a', 0) in map1.Items;
    assert ('b', 6) in map1.Items;
    assert |map1.Items| == 2;
    assert map1.Items == {('a', 0), ('b', 6)};
}

the assertion assert map1.Items == {('a', 0), ('b', 6)} fails, although it should be trivially true.

Thanks!

[stefan-aws]

This verifies with Dafny 4.8.1:

lemma mapTest()
{
    var map1: map<char, int> := map['a' := 0, 'b':= 6];
    assert map1.Items == {('a', 0), ('b', 6)} by {
      forall x ensures x in map1.Items <==> x in {('a', 0), ('b', 6)} {
        if x in map1.Items {
          assert exists k :: k in map1.Keys && x.0 == k && x.1 == map1[k];
        }
      }
      SetEquality(map1.Items, {('a', 0), ('b', 6)});   
    }
} 

lemma SetEquality<T>(s: set<T>, t: set<T>)
  requires forall x :: x in s <==> x in t
  ensures s == t
{}

[dreamqin68]

Thank you!