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.

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

feat: Multiset lemmas #28

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 46 additions & 0 deletions src/Collections/Multiset/Multiset.dfy
Original file line number Diff line number Diff line change
@@ -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 LemmaCardinalityOfToSetBound<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;
}
}
2 changes: 2 additions & 0 deletions src/Collections/Multiset/Multiset.dfy.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

Dafny program verifier finished with 2 verified, 0 errors
39 changes: 39 additions & 0 deletions src/Collections/Sequences/Seq.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -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)
robin-aws marked this conversation as resolved.
Show resolved Hide resolved
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..]));
}
}

}
2 changes: 1 addition & 1 deletion src/Collections/Sequences/Seq.dfy.expect
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@

Dafny program verifier finished with 71 verified, 0 errors
Dafny program verifier finished with 74 verified, 0 errors