diff options
Diffstat (limited to 'Test/dafny3')
| -rw-r--r-- | Test/dafny3/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny3/Paulson.dfy | 180 | ||||
| -rw-r--r-- | Test/dafny3/runtest.bat | 1 |
3 files changed, 185 insertions, 0 deletions
diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer index 284c5233..fe3b762e 100644 --- a/Test/dafny3/Answer +++ b/Test/dafny3/Answer @@ -38,3 +38,7 @@ Dafny program verifier finished with 24 verified, 0 errors -------------------- SetIterations.dfy --------------------
Dafny program verifier finished with 13 verified, 0 errors
+
+-------------------- Paulson.dfy --------------------
+
+Dafny program verifier finished with 28 verified, 0 errors
diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy new file mode 100644 index 00000000..ce9df5fe --- /dev/null +++ b/Test/dafny3/Paulson.dfy @@ -0,0 +1,180 @@ +// The following are Dafny versions from Section 8 of
+// "Mechanizing Coinduction and Corecursion in Higher-order Logic"
+// by Lawrence C. Paulson, 1996.
+
+codatatype LList<T> = Nil | Cons(head: T, tail: LList);
+
+// Simulate function as arguments
+datatype FunctionHandle<T> = FH(T);
+function Apply<T>(f: FunctionHandle<T>, argument: T): T
+
+// Function composition
+function After(f: FunctionHandle, g: FunctionHandle): FunctionHandle
+ghost method Definition_After<T>(f: FunctionHandle<T>, g: FunctionHandle<T>, arg: T)
+ ensures Apply(After(f, g), arg) == Apply(f, Apply(g, arg));
+
+function Lmap(f: FunctionHandle, a: LList): LList
+{
+ match a
+ case Nil => Nil
+ case Cons(x, xs) => Cons(Apply(f, x), Lmap(f, xs))
+}
+
+function Lappend(a: LList, b: LList): LList
+{
+ match a
+ case Nil => b
+ case Cons(x, xs) => Cons(x, Lappend(xs, b))
+}
+
+// ---------- Section 8.3 ----------
+
+comethod Example6(f: FunctionHandle, g: FunctionHandle, M: LList)
+ ensures Lmap(After(f, g), M) == Lmap(f, Lmap(g, M));
+{
+ match M {
+ case Nil =>
+ case Cons(x, xs) =>
+ assert Lmap(After(f, g), M)
+ == Lmap(After(f, g), Cons(x, xs))
+ == // def. Lmap
+ Cons(Apply(After(f, g), x), Lmap(After(f, g), xs));
+ Definition_After(f, g, x);
+ assert Cons(Apply(After(f, g), x), Lmap(After(f, g), xs))
+ == Cons(Apply(f, Apply(g, x)), Lmap(After(f, g), xs));
+
+ // use co-induction hypothesis
+ assert
+ Cons(Apply(f, Apply(g, x)), Lmap(After(f, g), xs))
+ ==#[_k]
+ Cons(Apply(f, Apply(g, x)), Lmap(f, Lmap(g, xs)));
+
+ calc {
+ Cons(Apply(f, Apply(g, x)), Lmap(f, Lmap(g, xs)));
+ // def. Lmap
+ Lmap(f, Cons(Apply(g, x), Lmap(g, xs)));
+ // def. Lmap
+ Lmap(f, Lmap(g, Cons(x, xs)));
+ Lmap(f, Lmap(g, M));
+ }
+ }
+}
+
+// ---------- Section 8.4 ----------
+
+// Iterates(f, M) == [M, f M, f^2 M, ..., f^n M, ...]
+function Iterates<A>(f: FunctionHandle<LList<A>>, M: LList<A>): LList<LList<A>>
+{
+ Cons(M, Iterates(f, Apply(f, M)))
+}
+
+comethod Eq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)
+ ensures Lmap(f, Iterates(f, M)) == Iterates(f, Apply(f, M));
+{
+ calc {
+ Lmap(f, Iterates(f, M));
+ Lmap(f, Cons(M, Iterates(f, Apply(f, M))));
+ Cons(Apply(f, M), Lmap(f, Iterates(f, Apply(f, M))));
+ }
+
+ Eq24(f, Apply(f, M)); // co-induction hypothesis
+ assert Lmap(f, Iterates(f, Apply(f, M)))
+ ==#[_k-1]
+ Iterates(f, Apply(f, Apply(f, M)));
+
+ calc {
+ Cons(Apply(f, M), Iterates(f, Apply(f, Apply(f, M))));
+ // def. Iterates
+ Iterates(f, Apply(f, M));
+ }
+}
+
+ghost method CorollaryEq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)
+ ensures Iterates(f, M) == Cons(M, Lmap(f, Iterates(f, M)));
+{
+ Eq24(f, M);
+}
+
+// Now prove that equation in CorollaryEq24 uniques characterizes Iterates.
+// Paulson says "The bisimulation for this proof is unusually complex".
+
+// Let h be any function
+function h<A>(f: FunctionHandle<LList<A>>, M: LList<A>): LList<LList<A>>
+// ... that satisfies the property in CorollaryEq24:
+ghost method Definition_h<A>(f: FunctionHandle<LList<A>>, M: LList<A>)
+ ensures h(f, M) == Cons(M, Lmap(f, h(f, M)));
+
+// Functions to support the proof:
+
+function Iter<A>(n: nat, f: FunctionHandle<A>, arg: A): A
+{
+ if n == 0 then arg else Apply(f, Iter(n-1, f, arg))
+}
+
+function LmapIter(n: nat, f: FunctionHandle, arg: LList): LList
+{
+ if n == 0 then arg else Lmap(f, LmapIter(n-1, f, arg))
+}
+
+ghost method Lemma25<A>(n: nat, f: FunctionHandle<A>, b: A, M: LList<A>)
+ ensures LmapIter(n, f, Cons(b, M)) == Cons(Iter(n, f, b), LmapIter(n, f, M));
+{
+ // proof is by (automatic) induction
+}
+
+ghost method Lemma26<A>(n: nat, f: FunctionHandle, x: LList) // (26) in the paper, but with f := LMap f
+ ensures LmapIter(n, f, Lmap(f, x)) == LmapIter(n+1, f, x);
+{
+ // proof is by (automatic) induction
+}
+
+comethod BisimulationLemma<A>(n: nat, f: FunctionHandle<LList<A>>, u: LList<A>)
+ ensures LmapIter(n, f, h(f, u)) == LmapIter(n, f, Iterates(f, u));
+{
+ calc {
+ LmapIter(n, f, h(f, u));
+ { Definition_h(f, u); }
+ LmapIter(n, f, Cons(u, Lmap(f, h(f, u))));
+ { Lemma25(n, f, u, Lmap(f, h(f, u))); }
+ Cons(Iter(n, f, u), LmapIter(n, f, Lmap(f, h(f, u))));
+ { Lemma26(n, f, h(f, u)); }
+ Cons(Iter(n, f, u), LmapIter(n+1, f, h(f, u)));
+ }
+
+ assert LmapIter(n+1, f, h(f, u))
+ ==#[_k-1]
+ LmapIter(n+1, f, Iterates(f, u));
+
+ calc {
+ Cons(Iter(n, f, u), LmapIter(n+1, f, Iterates(f, u)));
+ { Lemma26(n, f, Iterates(f, u)); }
+ Cons(Iter(n, f, u), LmapIter(n, f, Lmap(f, Iterates(f, u))));
+ { Lemma25(n, f, u, Lmap(f, Iterates(f, u))); }
+ LmapIter(n, f, Cons(u, Lmap(f, Iterates(f, u))));
+ { CorollaryEq24(f, u); }
+ LmapIter(n, f, Iterates(f, u));
+ }
+}
+
+ghost method Example7<A>(f: FunctionHandle<LList<A>>)
+ // Given the definition of h, prove h(f, _) == Iterates(f, _):
+ ensures forall M :: h(f, M) == Iterates(f, M);
+{
+ forall (M) {
+ BisimulationLemma(0, f, M);
+ }
+}
+
+// ---------- Section 8.5 ----------
+
+comethod Example8<A>(f: FunctionHandle<A>, M: LList<A>, N: LList<A>)
+ ensures Lmap(f, Lappend(M, N)) == Lappend(Lmap(f, M), Lmap(f, N));
+{
+ // A proof doesn't get any simpler than this
+}
+
+comethod Associativity(a: LList, b: LList, c: LList)
+ ensures Lappend(Lappend(a, b), c) == Lappend(a, Lappend(b, c));
+{
+ // Again, Dafny does this proof completely automatically
+}
diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat index 82fd878c..3bcae386 100644 --- a/Test/dafny3/runtest.bat +++ b/Test/dafny3/runtest.bat @@ -8,6 +8,7 @@ for %%f in ( Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy
SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy
InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy
+ Paulson.dfy
) do (
echo.
echo -------------------- %%f --------------------
|