Removed the old (though automatic) coinduction principle

1 files changed, 0 insertions, 59 deletions

diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy
deleted file mode 100644
index c5651c90..00000000
--- a/Test/dafny0/CoPredicates.dfy
+++ /dev/null
@@ -1,59 +0,0 @@
-codatatype Stream<T> = Cons(head: T, tail: Stream);

-

-function Upward(n: int): Stream<int>

-{

-  Cons(n, Upward(n + 1))

-}

-

-copredicate Pos(s: Stream<int>)

-{

-  0 < s.head && Pos(s.tail)

-}

-

-copredicate X(s: Stream)

-{

-  X(s)

-}

-

-ghost method AlwaysLemma(s: Stream)

-  ensures X(s);

-{

-}

-

-function Doubles(n: int): Stream<int>

-{

-  Cons(2*n, Doubles(n + 1))

-}

-

-copredicate Even(s: Stream<int>)

-{

-  s.head % 2 == 0 && Even(s.tail)

-}

-

-ghost method Lemma0(n: int)

-  ensures Even(Doubles(n));

-{

-}

-

-function UpwardBy2(n: int): Stream<int>

-{

-  Cons(n, UpwardBy2(n + 2))

-}

-

-ghost method Lemma1(n: int)

-  ensures Even(UpwardBy2(2*n));  // error:  this is true, but Dafny can't prove it

-{

-}

-

-function U2(n: int): Stream<int>

-  requires n % 2 == 0;

-{

-  UpwardBy2(n)

-}

-

-// Postponed:

-//ghost method Lemma2(n: int)

-//  ensures Even(UpwardBy2(2*n));  // this is true, and Dafny can prove it

-//{

-//  assert Even(U2(2*n));  // ... thanks to this lemma

-//}