From 9719245aa1a9953a9f5704edc318c5c5303cf36a Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 15 Mar 2013 18:15:10 -0700 Subject: Added several co-induction examples from a 1996 paper by Larry Paulson. --- Test/dafny3/Answer | 4 ++ Test/dafny3/Paulson.dfy | 180 ++++++++++++++++++++++++++++++++++++++++++++++++ Test/dafny3/runtest.bat | 1 + 3 files changed, 185 insertions(+) create mode 100644 Test/dafny3/Paulson.dfy (limited to 'Test/dafny3') 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 = Nil | Cons(head: T, tail: LList); + +// Simulate function as arguments +datatype FunctionHandle = FH(T); +function Apply(f: FunctionHandle, argument: T): T + +// Function composition +function After(f: FunctionHandle, g: FunctionHandle): FunctionHandle +ghost method Definition_After(f: FunctionHandle, g: FunctionHandle, 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(f: FunctionHandle>, M: LList): LList> +{ + Cons(M, Iterates(f, Apply(f, M))) +} + +comethod Eq24(f: FunctionHandle>, M: LList) + 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(f: FunctionHandle>, M: LList) + 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(f: FunctionHandle>, M: LList): LList> +// ... that satisfies the property in CorollaryEq24: +ghost method Definition_h(f: FunctionHandle>, M: LList) + ensures h(f, M) == Cons(M, Lmap(f, h(f, M))); + +// Functions to support the proof: + +function Iter(n: nat, f: FunctionHandle, 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(n: nat, f: FunctionHandle, b: A, M: LList) + ensures LmapIter(n, f, Cons(b, M)) == Cons(Iter(n, f, b), LmapIter(n, f, M)); +{ + // proof is by (automatic) induction +} + +ghost method Lemma26(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(n: nat, f: FunctionHandle>, u: LList) + 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(f: FunctionHandle>) + // 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(f: FunctionHandle, M: LList, N: LList) + 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 -------------------- -- cgit v1.2.3