diff options
| author |  Rustan Leino <unknown> | 2013-07-16 19:11:31 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-07-16 19:11:31 -0700 |
| commit | 8b69f963879696d40da0a1b845988e17fe9d29d2 (patch) | |
| tree | 0638858c44528d9e14ff0b4d4d9db34c0fbbdb72 /Test/dafny0/Basics.dfy | |
| parent | b0bb7bf96406d8695d5ec2377d9ce2b2acba44f0 (diff) | |
Axioms that relate (multi)set cardinality with (multi)set difference.
Removed three redundant multiset axioms.
Diffstat (limited to 'Test/dafny0/Basics.dfy')
| -rw-r--r-- | Test/dafny0/Basics.dfy | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 3d2e35bd..f6e2d895 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -336,4 +336,43 @@ module SetCardinality { ensures |s| != 0 ==> var x :| x in s; true;
{
}
+
+ method G<T>(s: set<T>, t: set<T>)
+ requires s <= t;
+ ensures |s| <= |t|; // it doesn't get this immediately, but the method body offers different proofs
+ {
+ if {
+ case true => assert |t - s| + |t * s| == |t|;
+ case true => calc {
+ |s| <= |t|;
+ <==
+ |s - s| <= |t - s|;
+ }
+ case true => assert 0 <= |t - s|;
+ }
+ }
+
+ method H(s: multiset<int>, t: multiset<int>)
+ requires s <= t;
+ ensures |s| <= |t|; // it doesn't get this immediately, but the method body offers different proofs
+ {
+ if {
+ case true => assert |t - s| + |t * s| == |t|;
+ case true => calc {
+ |s| <= |t|;
+ <==
+ |s - s| <= |t - s|;
+ }
+ case true => assert 0 <= |t - s|;
+ }
+ }
+
+ method K<T>(s: multiset<T>, t: multiset<T>)
+ {
+ assert |s * t| + |t * s|
+ +
+ |s - t| + |t - s|
+ ==
+ |s + t|;
+ }
}
|