Added an alternative statement of the prime theorem

1 files changed, 20 insertions, 35 deletions

diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy
index c85f1607..1cb5d968 100644
--- a/Test/dafny4/Primes.dfy
+++ b/Test/dafny4/Primes.dfy
@@ -18,6 +18,13 @@ lemma AlwaysMorePrimes(k: int)
   }

 }

 

+// Here is an alternative formulation of the theorem

+lemma NoFiniteSetContainsAllPrimes(s: set<int>)

+  ensures exists p :: IsPrime(p) && p !in s;

+{

+  AlwaysMorePrimes(if s == {} then 0 else PickLargest(s) + 1);

+}

+

 // ------------------------- lemmas and auxiliary definitions

 

 predicate AllPrimes(s: set<int>, bound: int)

@@ -49,7 +56,7 @@ lemma GetLargerPrime(s: set<int>, bound: int) returns (p: int)
 function product(s: set<int>): int

 {

   if s == {} then 1 else

-  var a := PickSmallest(s); a * product(s - {a})

+  var a := PickLargest(s); a * product(s - {a})

 }

 

 lemma product_property(s: set<int>)

@@ -84,13 +91,13 @@ lemma ProductPlusOneIsPrime(s: set<int>, q: int)
 

 // The following lemma is essentially just associativity and commutativity of multiplication.

 // To get this proof through, it is necessary to know that if x!=y and y==Pick...(s), then

-// also y==Pick...(s - {x}).  It is for this reason that we use PickSmallest, instead of

+// also y==Pick...(s - {x}).  It is for this reason that we use PickLargest, instead of

 // picking an arbitrary element from s.

 lemma RemoveFactor(x: int, s: set<int>)

   requires x in s;

   ensures product(s) == x * product(s - {x});

 {

-  var y := PickSmallest(s);

+  var y := PickLargest(s);

   if x != y {

     calc {

       product(s);

@@ -100,7 +107,7 @@ lemma RemoveFactor(x: int, s: set<int>)
       x * y * product(s - {y} - {x});

       { assert s - {y} - {x} == s - {x} - {y}; }

       x * y * product(s - {x} - {y});

-      { assert y == PickSmallest(s - {x}); }

+      { assert y == PickLargest(s - {x}); }

       x * product(s - {x});

     }

   }

@@ -162,59 +169,37 @@ lemma Composite(c: int) returns (a: int, b: int)
   }

 }

 

-function PickSmallest(s: set<int>): int

+function PickLargest(s: set<int>): int

   requires s != {};

 {

-  SmallestElementExists(s);

-  var x :| x in s && forall y :: y in s ==> x <= y;

+  LargestElementExists(s);

+  var x :| x in s && forall y :: y in s ==> y <= x;

   x

 }

 

-lemma SmallestElementExists(s: set<int>)

+lemma LargestElementExists(s: set<int>)

   requires s != {};

-  ensures exists x :: x in s && forall y :: y in s ==> x <= y;

+  ensures exists x :: x in s && forall y :: y in s ==> y <= x;

 {

   var s' := s;

   while true

     invariant s' != {} && s' <= s;

-    invariant forall x,y :: x in s' && y in s - s' ==> x <= y;

+    invariant forall x,y :: x in s' && y in s - s' ==> y <= x;

     decreases s';

   {

     var x :| x in s';  // pick something

-    if forall y :: y in s' ==> x <= y {

+    if forall y :: y in s' ==> y <= x {

       // good pick

       return;

     } else {

       // constrain the pick further

-      var y :| y in s' && y < x;

-      s' := set z | z in s && z < x;

+      var y :| y in s' && x < y;

+      s' := set z | z in s && x < z;

       assert y in s';

     }

   }

 }

 

-/*******  This might be an alternative way to implement PickSmallest, if one can prove the desired postcondition of this function  *******

-function PS(s: set<int>): int

-  requires s != {};

-{

-  NonEmptySet(s);  // TODO: why is this needed?

-  var x :| x in s;

-  if forall y :: y in s ==> x <= y then

-    x

-  else

-    var y :| y in s && y < x;  // since not all numbers in s are smaller than x, here is one that isn't

-    var s' := set m | m in s && m < x;  // this is the subset of s containing all numbers smaller than x

-    assert y in s';  // y is in that subset, which implies s' is nonempty

-    PS(s')

-}

-

-lemma NonEmptySet(s: set<int>)

-  requires s != {};

-  ensures exists y :: y in s;

-{

-}

-*******/

-

 // This axiom about % is needed.  Unfortunately, Z3 seems incapable of proving it.

 lemma MulDivMod(a: nat, b: nat, c: nat, j: nat)

   requires a * b == c && j < a;