diff options
Diffstat (limited to 'Test/dafny1/Rippling.dfy')
-rw-r--r-- | Test/dafny1/Rippling.dfy | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 0a4d541d..5fd87a6c 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -234,6 +234,13 @@ function sort(xs: List): List case Cons(y, ys) => insort(y, sort(ys))
}
+function reverse(xs: List): List
+{
+ match xs
+ case Nil => Nil
+ case Cons(t, rest) => concat(reverse(rest), Cons(t, Nil))
+}
+
// Pair list functions
function zip(a: List, b: List): PList
@@ -554,3 +561,28 @@ ghost method P67() assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));
}
}
+
+// ---------
+
+ghost method Lemma_RevConcat(xs: List, ys: List)
+ ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
+{
+ match (xs) {
+ case Nil =>
+ assert forall ws :: concat(ws, Nil) == ws;
+ case Cons(t, rest) =>
+ Lemma_RevConcat(rest, ys);
+ assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);
+ }
+}
+
+ghost method Theorem(xs: List)
+ ensures reverse(reverse(xs)) == xs;
+{
+ match (xs) {
+ case Nil =>
+ case Cons(t, rest) =>
+ Lemma_RevConcat(reverse(rest), Cons(t, Nil));
+ Theorem(rest);
+ }
+}
|