Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Map created with comprehension shorthand vs full comprehension #336

Closed
utaal opened this issue Aug 2, 2019 · 0 comments · Fixed by #340
Closed

Map created with comprehension shorthand vs full comprehension #336

utaal opened this issue Aug 2, 2019 · 0 comments · Fixed by #340

Comments

@utaal
Copy link

utaal commented Aug 2, 2019 •
edited
Loading

For the following:

    var a := map[2 := (3, 5), 3 := (5, 8)];
    assert (map k | k in a :: k := a[k].0)
        == (map k | k in a :: a[k].0); // <- this is line 8

Note that the second map comprehension implicitly uses k as the key
(k := a[k].0 vs a[k].0)

I get:

examples/map-comprehension.dfy(8,8): Error: assertion violation

@samuelgruetter on Gitter suggests proving it with:

predicate submap<K, V>(m1: map<K, V>, m2: map<K, V>) {
    forall k :: k in m1 ==> k in m2 && m1[k] == m2[k]
}

lemma map_ext<K, V>(m1: map<K, V>, m2: map<K, V>)
    requires submap(m1, m2)
    requires submap(m2, m1)
    ensures m1 == m2
{}

method test() {
    var a := map[2 := (3, 5), 3 := (5, 8)];
    map_ext(map k | k in a :: k := a[k].0, map k | k in a :: a[k].0);
    assert (map k | k in a :: k := a[k].0)
        == (map k | k in a :: a[k].0);
}

But we believe this should be provable without the map_ext hint.
RustanLeino added a commit to RustanLeino/dafny that referenced this issue Aug 3, 2019
@RustanLeino
Try to treat general map comprehension as the common case
da1a096 
If a general map comprehension has the form `map x | R(x) :: x := T(x)`, then
translate it (in the verifier) in the same way as the common `map x | R(x) :: T(x)`.

Fixes dafny-lang#336
@RustanLeino RustanLeino mentioned this issue Aug 6, 2019
Merged
amaurremi pushed a commit to amaurremi/dafny that referenced this issue Aug 7, 2019
@RustanLeino @amaurremi
Try to treat general map comprehension as the common case
f45e49c 
If a general map comprehension has the form `map x | R(x) :: x := T(x)`, then
translate it (in the verifier) in the same way as the common `map x | R(x) :: T(x)`.

Fixes dafny-lang#336
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Try to treat general map comprehension as the common case RustanLeino/dafny
1 participant
@utaal