Axioms that relate (multi)set cardinality with (multi)set difference.

Removed three redundant multiset axioms.

4 files changed, 96 insertions, 30 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 349da0fd..db08a280 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -65,8 +65,8 @@ axiom (forall<T> a, b: Set T :: { Set#Union(a, b) }
     Set#Difference(Set#Union(a, b), b) == a);

 // Follows from the general union axiom, but might be still worth including, because disjoint union is a common case:

 // axiom (forall<T> a, b: Set T :: { Set#Card(Set#Union(a, b)) }

-  // Set#Disjoint(a, b) ==>

-    // Set#Card(Set#Union(a, b)) == Set#Card(a) + Set#Card(b));    

+//   Set#Disjoint(a, b) ==>

+//     Set#Card(Set#Union(a, b)) == Set#Card(a) + Set#Card(b));

 

 function Set#Intersection<T>(Set T, Set T): Set T;

 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }

@@ -81,20 +81,26 @@ axiom (forall<T> a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) }
 axiom (forall<T> a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) }

   Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));

 axiom (forall<T> a, b: Set T :: { Set#Card(Set#Union(a, b)) }{ Set#Card(Set#Intersection(a, b)) }

-  Set#Card(Set#Union(a, b)) + Set#Card(Set#Intersection(a, b)) == Set#Card(a) + Set#Card(b));  

+  Set#Card(Set#Union(a, b)) + Set#Card(Set#Intersection(a, b)) == Set#Card(a) + Set#Card(b));

 

 function Set#Difference<T>(Set T, Set T): Set T;

 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }

   Set#Difference(a,b)[o] <==> a[o] && !b[o]);

 axiom (forall<T> a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }

   b[y] ==> !Set#Difference(a, b)[y] );

+axiom (forall<T> a, b: Set T ::

+  { Set#Card(Set#Difference(a, b)) }

+  Set#Card(Set#Difference(a, b)) + Set#Card(Set#Difference(b, a)) 

+  + Set#Card(Set#Intersection(a, b))

+    == Set#Card(Set#Union(a, b)) &&

+  Set#Card(Set#Difference(a, b)) == Set#Card(a) - Set#Card(Set#Intersection(a, b)));

 

 function Set#Subset<T>(Set T, Set T): bool;

 axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }

   Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o]));

-//axiom(forall<T> a: Set T, b: Set T ::

-// { Set#Subset(a,b), Set#Card(a), Set#Card(b) }  // very restrictive trigger

-//  Set#Subset(a,b) ==> Set#Card(a) <= Set#Card(b));

+// axiom(forall<T> a: Set T, b: Set T ::

+//   { Set#Subset(a,b), Set#Card(a), Set#Card(b) }  // very restrictive trigger

+//   Set#Subset(a,b) ==> Set#Card(a) <= Set#Card(b));

   

 

 function Set#Equal<T>(Set T, Set T): bool;

@@ -167,17 +173,6 @@ axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a,b)[o]
 axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Card(MultiSet#Union(a,b)) }

   MultiSet#Card(MultiSet#Union(a,b)) == MultiSet#Card(a) + MultiSet#Card(b));

   

-// two containment axioms

-axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] }

-  0 < a[y] ==> 0 < MultiSet#Union(a, b)[y]);

-axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), b[y] }

-  0 < b[y] ==> 0 < MultiSet#Union(a, b)[y]);

-

-// symmetry axiom

-axiom (forall<T> a, b: MultiSet T :: { MultiSet#Union(a, b) }

-  MultiSet#Difference(MultiSet#Union(a, b), a) == b &&

-  MultiSet#Difference(MultiSet#Union(a, b), b) == a);

-

 function MultiSet#Intersection<T>(MultiSet T, MultiSet T): MultiSet T;

 axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Intersection(a,b)[o] }

   MultiSet#Intersection(a,b)[o] == Math#min(a[o],  b[o]));

@@ -194,6 +189,12 @@ axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Difference(a,b
   MultiSet#Difference(a,b)[o] == Math#clip(a[o] - b[o]));

 axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Difference(a, b), b[y], a[y] }

   a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0 );

+axiom (forall<T> a, b: MultiSet T ::

+  { MultiSet#Card(MultiSet#Difference(a, b)) }

+  MultiSet#Card(MultiSet#Difference(a, b)) + MultiSet#Card(MultiSet#Difference(b, a)) 

+  + 2 * MultiSet#Card(MultiSet#Intersection(a, b))

+    == MultiSet#Card(MultiSet#Union(a, b)) &&

+  MultiSet#Card(MultiSet#Difference(a, b)) == MultiSet#Card(a) - MultiSet#Card(MultiSet#Intersection(a, b)));

 

 // multiset subset means a must have at most as many of each element as b

 function MultiSet#Subset<T>(MultiSet T, MultiSet T): bool;

@@ -464,7 +465,7 @@ axiom (forall<U, V> m: Map U V, m': Map U V::
     Map#Equal(m, m') <==> (forall u : U :: Map#Domain(m)[u] == Map#Domain(m')[u]) &&

                           (forall u : U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u]));

 // extensionality

-axiom  (forall<U, V> m: Map U V, m': Map U V::

+axiom (forall<U, V> m: Map U V, m': Map U V::

   { Map#Equal(m, m') }

     Map#Equal(m, m') ==> m == m');

 

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0db833a4..60599a14 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -738,7 +738,7 @@ Basics.dfy(235,10): Error: when left-hand sides 0 and 1 refer to the same locati
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 51 verified, 11 errors

+Dafny program verifier finished with 57 verified, 11 errors

 

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Purple

@@ -1483,8 +1483,15 @@ Execution trace:
     (0,0): anon0

     (0,0): anon4_Then

     (0,0): anon3

+MultiSets.dfy(267,24): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

+    (0,0): anon3

+    (0,0): anon12_Then

+    (0,0): anon14_Else

 

-Dafny program verifier finished with 53 verified, 3 errors

+Dafny program verifier finished with 54 verified, 4 errors

 

 -------------------- PredExpr.dfy --------------------

 PredExpr.dfy(4,12): Error: condition in assert expression might not hold

@@ -1724,36 +1731,36 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 3 errors

 

 -------------------- Superposition.dfy --------------------

-
+

 Verifying CheckWellformed$$_0_M0.C.M ...

   [0 proof obligations]  verified

-
+

 Verifying Impl$$_0_M0.C.M ...

   [4 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_0_M0.C.P ...

   [4 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_0_M0.C.Q ...

   [3 proof obligations]  error

 Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-
+

 Verifying CheckWellformed$$_0_M0.C.R ...

   [3 proof obligations]  error

 Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-
+

 Verifying CheckWellformed$$_1_M1.C.M ...

   [0 proof obligations]  verified

-
+

 Verifying Impl$$_1_M1.C.M ...

   [1 proof obligation]  verified

-
+

 Verifying CheckWellformed$$_1_M1.C.P ...

   [1 proof obligation]  error

 Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.

@@ -1762,10 +1769,10 @@ Execution trace:
     (0,0): anon7_Else

     (0,0): anon9_Then

     (0,0): anon6

-
+

 Verifying CheckWellformed$$_1_M1.C.Q ...

   [0 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_1_M1.C.R ...

   [0 proof obligations]  verified

 

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|;

+  }

 }

diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy
index ff03bb7a..b9817ac9 100644
--- a/Test/dafny0/MultiSets.dfy
+++ b/Test/dafny0/MultiSets.dfy
@@ -248,3 +248,22 @@ method LetSuchThatExpression(s: multiset<int>)
   ensures |s| != 0 ==> var x :| x in s; true;

 {

 }

+

+// ----------- things that at one point were axioms -------------

+

+method MultiSetProperty0(s: multiset<object>, t: multiset<object>, p: object)

+{

+  if 0 < s[p] {

+    assert 0 < (s + t)[p];

+  }

+  if 0 < t[p] {

+    assert 0 < (s + t)[p];

+  }

+  if * {

+    assert s + t - s == t;

+  } else if * {

+    assert s + t - t == s;

+  } else {

+    assert s + (t - s) == t;  // error

+  }

+}