Test cases for co-inductive proofs, and an axiom that makes some of them possible

3 files changed, 263 insertions, 1 deletions

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 3c339054..ae65e2d9 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -2,3 +2,7 @@
 -------------------- Iter.dfy --------------------

 

 Dafny program verifier finished with 15 verified, 0 errors

+

+-------------------- Streams.dfy --------------------

+

+Dafny program verifier finished with 38 verified, 0 errors

diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
new file mode 100644
index 00000000..1369e584
--- /dev/null
+++ b/Test/dafny3/Streams.dfy
@@ -0,0 +1,258 @@
+// ----- Stream

+

+codatatype Stream<T> = Nil | Cons(head: T, tail: Stream);

+

+function append(M: Stream, N: Stream): Stream

+{

+  match M

+  case Nil => N

+  case Cons(t, M') => Cons(t, append(M', N))

+}

+

+// ----- f, g, and maps

+

+type X;

+

+function f(x: X): X

+function g(x: X): X

+

+function map_f(M: Stream<X>): Stream<X>

+{

+  match M

+  case Nil => Nil

+  case Cons(x, N) => Cons(f(x), map_f(N))

+}

+

+function map_g(M: Stream<X>): Stream<X>

+{

+  match M

+  case Nil => Nil

+  case Cons(x, N) => Cons(g(x), map_g(N))

+}

+

+function map_fg(M: Stream<X>): Stream<X>

+{

+  match M

+  case Nil => Nil

+  case Cons(x, N) => Cons(f(g(x)), map_fg(N))

+}

+

+// ----- Theorems

+

+// map (f * g) M = map f (map g M)

+comethod Theorem0(M: Stream<X>)

+  ensures map_fg(M) == map_f(map_g(M));

+{

+  match (M) {

+    case Nil =>

+    case Cons(x, N) =>

+      Theorem0(N);

+  }

+}

+comethod Theorem0_alt(M: Stream<X>)

+  ensures map_fg(M) == map_f(map_g(M));

+{

+  if (M.Cons?) {

+    Theorem0(M.tail);

+  }

+}

+

+// map f (append M N) = append (map f M) (map f N)

+comethod Theorem1(M: Stream<X>, N: Stream<X>)

+  ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

+{

+  match (M) {

+    case Nil =>

+    case Cons(x, M') =>

+      Theorem1(M', N);

+  }

+}

+comethod Theorem1_alt(M: Stream<X>, N: Stream<X>)

+  ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

+{

+  if (M.Cons?) {

+    Theorem1(M.tail, N);

+  }

+}

+

+// append NIL M = M

+ghost method Theorem2(M: Stream<X>)

+  ensures append(Nil, M) == M;

+{

+  // trivial

+}

+

+// append M NIL = M

+comethod Theorem3(M: Stream<X>)

+  ensures append(M, Nil) == M;

+{

+  match (M) {

+    case Nil =>

+    case Cons(x, N) =>

+      Theorem3(N);

+  }

+}

+comethod Theorem3_alt(M: Stream<X>)

+  ensures append(M, Nil) == M;

+{

+  if (M.Cons?) {

+    Theorem3(M.tail);

+  }

+}

+

+// append M (append N P) = append (append M N) P

+comethod Theorem4(M: Stream<X>, N: Stream<X>, P: Stream<X>)

+  ensures append(M, append(N, P)) == append(append(M, N), P);

+{

+  match (M) {

+    case Nil =>

+    case Cons(x, M') =>

+      Theorem4(M', N, P);

+  }

+}

+comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)

+  ensures append(M, append(N, P)) == append(append(M, N), P);

+{

+  if (M.Cons?) {

+    Theorem4(M.tail, N, P);

+  }

+}

+

+// ----- Flatten

+

+// Flatten can't be written as just:

+//

+//     function SimpleFlatten<T>(M: Stream<Stream>): Stream

+//     {

+//       match M

+//       case Nil => Nil

+//       case Cons(s, N) => append(s, SimpleFlatten(N))

+//     }

+//

+// because this function fails to be productive given an infinite stream of Nil's.

+// Instead, here are two variations SimpleFlatten.  The first variation (FlattenStartMarker)

+// prepends a "startMarker" to each of the streams in "M".  The other (FlattenNonEmpties)

+// insists that "M" contains no empty streams.  One can prove a theorem that relates these

+// two versions.

+

+// This first variation of Flatten returns a stream of the streams in M, each preceded with

+// "startMarker".

+

+function FlattenStartMarker<T>(M: Stream<Stream>, startMarker: T): Stream

+{

+  FlattenStartMarkerAcc(Nil, M, startMarker)

+}

+

+function FlattenStartMarkerAcc<T>(accumulator: Stream, M: Stream<Stream>, startMarker: T): Stream

+{

+  match accumulator

+  case Cons(hd, tl) =>

+    Cons(hd, FlattenStartMarkerAcc(tl, M, startMarker))

+  case Nil =>

+    match M

+    case Nil => Nil

+    case Cons(s, N) => Cons(startMarker, FlattenStartMarkerAcc(s, N, startMarker))

+}

+

+// The next variation of Flatten requires M to contain no empty streams.

+

+copredicate StreamOfNonEmpties(M: Stream<Stream>)

+{

+  match M

+  case Nil => true

+  case Cons(s, N) => s.Cons? && StreamOfNonEmpties(N)

+}

+

+function FlattenNonEmpties(M: Stream<Stream>): Stream

+  requires StreamOfNonEmpties(M);

+{

+  FlattenNonEmptiesAcc(Nil, M)

+}

+

+function FlattenNonEmptiesAcc(accumulator: Stream, M: Stream<Stream>): Stream

+  requires StreamOfNonEmpties(M);

+{

+  match accumulator

+  case Cons(hd, tl) =>

+    Cons(hd, FlattenNonEmptiesAcc(tl, M))

+  case Nil =>

+    match M

+    case Nil => Nil

+    case Cons(s, N) => Cons(s.head, FlattenNonEmptiesAcc(s.tail, N))

+}

+

+// We can prove a theorem that links the previous two variations of flatten.  To

+// do that, we first define a function that prepends an element to each stream

+// of a given stream of streams.

+// The "assume" statements below are temporary workaround.  They make the proofs

+// unsound, but, as a temporary measure, they express the intent of the proofs.

+

+function Prepend<T>(x: T, M: Stream<Stream>): Stream<Stream>

+  ensures StreamOfNonEmpties(Prepend(x, M));

+{

+  match M

+  case Nil => Nil

+  case Cons(s, N) => Cons(Cons(x, s), Prepend(x, N))

+}

+

+ghost method Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)

+  ensures FlattenStartMarker(M, startMarker) == FlattenNonEmpties(Prepend(startMarker, M));

+{

+  Lemma_Flatten(Nil, M, startMarker);

+}

+

+comethod Lemma_Flatten<T>(accumulator: Stream, M: Stream<Stream>, startMarker: T)

+  ensures FlattenStartMarkerAcc(accumulator, M, startMarker) == FlattenNonEmptiesAcc(accumulator, Prepend(startMarker, M));

+{

+  calc {

+    FlattenStartMarkerAcc(accumulator, M, startMarker);

+    { Lemma_FlattenAppend0(accumulator, M, startMarker); }

+    append(accumulator, FlattenStartMarkerAcc(Nil, M, startMarker));

+    { Lemma_Flatten(Nil, M, startMarker);

+      assume FlattenStartMarkerAcc(Nil, M, startMarker) == FlattenNonEmptiesAcc(Nil, Prepend(startMarker, M));  // postcondition of the co-recursive call

+    }

+    append(accumulator, FlattenNonEmptiesAcc(Nil, Prepend(startMarker, M)));

+    { Lemma_FlattenAppend1(accumulator, Prepend(startMarker, M)); }

+    FlattenNonEmptiesAcc(accumulator, Prepend(startMarker, M));

+  }

+}

+

+comethod Lemma_FlattenAppend0<T>(s: Stream, M: Stream<Stream>, startMarker: T)

+  ensures FlattenStartMarkerAcc(s, M, startMarker) == append(s, FlattenStartMarkerAcc(Nil, M, startMarker));

+{

+  match (s) {

+    case Nil =>

+    case Cons(hd, tl) =>

+      calc {

+        FlattenStartMarkerAcc(Cons(hd, tl), M, startMarker);

+        Cons(hd, FlattenStartMarkerAcc(tl, M, startMarker));

+        { Lemma_FlattenAppend0(tl, M, startMarker);

+          assume FlattenStartMarkerAcc(tl, M, startMarker) == append(tl, FlattenStartMarkerAcc(Nil, M, startMarker));  // this is the postcondition of the co-recursive call

+        }

+        Cons(hd, append(tl, FlattenStartMarkerAcc(Nil, M, startMarker)));

+        // def. append

+        append(Cons(hd, tl), FlattenStartMarkerAcc(Nil, M, startMarker));

+      }

+  }

+}

+

+comethod Lemma_FlattenAppend1<T>(s: Stream, M: Stream<Stream>)

+  requires StreamOfNonEmpties(M);

+  ensures FlattenNonEmptiesAcc(s, M) == append(s, FlattenNonEmptiesAcc(Nil, M));

+{

+  match (s) {

+    case Nil =>

+    case Cons(hd, tl) =>

+      calc {

+        FlattenNonEmptiesAcc(Cons(hd, tl), M);

+        // def. FlattenNonEmptiesAcc

+        Cons(hd, FlattenNonEmptiesAcc(tl, M));

+        { Lemma_FlattenAppend1(tl, M);

+          assume FlattenNonEmptiesAcc(tl, M) == append(tl, FlattenNonEmptiesAcc(Nil, M));  // postcondition of the co-recursive call

+        }

+        Cons(hd, append(tl, FlattenNonEmptiesAcc(Nil, M)));

+        // def. append

+        append(Cons(hd, tl), FlattenNonEmptiesAcc(Nil, M));

+      }

+  }

+}

diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index 35d8cc60..9265dcd0 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -4,7 +4,7 @@ setlocal
 set BINARIES=..\..\Binaries

 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

-for %%f in (Iter.dfy) do (

+for %%f in (Iter.dfy Streams.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f