• API
• FAQ
• Tools
• Archive
SHARE
TWEET Untitled a guest May 23rd, 2019 91 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. datatype Tree<T> = Leaf | Node(Tree<T>, Tree<T>, T)
2. datatype List<T> = Nil | Cons(T, List<T>)
3.
4. function flatten<T>(tree: Tree<T>): List<T>
5. {
6.     match(tree)
7.     case Leaf() =>  Nil
8.     case Node(tree1, tree2, x) => Cons(x, append(flatten(tree1), flatten(tree2)))
9. }
10.
11. function append<T>(xs: List<T>, ys: List<T>): List<T>
12.   ensures xs == Nil ==> append(xs, ys) == ys
13.   ensures (ys == Nil) == (append(xs, ys) == xs)
14. {
15.     match(xs)
16.         case Nil => ys
17.         case Cons(x, xs') =>  Cons(x, append(xs', ys))
18. }
19.
20. function listContains<T>(xs: List<T>, element: T): bool
21. {
22.     match(xs)
23.     case Nil => false
24.         case Cons(x, xs') => (x == element) || listContains(xs', element)
25. }
26.
27. function treeContains<T>(tree: Tree<T>, element: T): bool
28. {
29.     match(tree)
30.     case Leaf() => false
31.     case Node(tree1, tree2, x) => (x == element) || treeContains(tree1, element) || treeContains(tree2, element)
32. }
33.
34. lemma littleAppendsAreBigAppend<T>(xs: List<T>, ys: List<T>, element: T)
35.   ensures listContains(xs, element) || listContains(ys, element) <==> listContains(append(xs, ys) ,element)
36. {
37.
38. }
39.
40. lemma sameElements<T>(tree: Tree<T>, element: T)
41.   ensures treeContains(tree, element) <==> listContains(flatten(tree), element)
42. {
43.   match(tree) {
44.      case Leaf() => {
45.        assert treeContains(tree, element)
46.            == treeContains(Leaf(), element)
47.            == false
48.            == listContains<T>(Nil, element)
49.            == listContains(flatten(tree), element);
50.       }
51.       case Node(tree1, tree2, x) => {
52.         assert treeContains(tree, element)
53.           == treeContains(Node(tree1, tree2, x), element)
54.           == (x == element) || treeContains(tree1, element) || treeContains(tree2, element);
55.
56.         sameElements(tree1, element);
57.         sameElements(tree2, element);
58.
59.         assert (x == element) || treeContains(tree1, element) || treeContains(tree2, element)
60.           == (x == element) || listContains(flatten(tree1), element) || listContains(flatten(tree2), element);
61.
62.         littleAppendsAreBigAppend(flatten(tree1), flatten(tree2), element);
63.
64.         assert listContains(flatten(tree), element)
65.           == listContains(flatten(Node(tree1, tree2, x)), element)
66.           == listContains(append(Cons(x, flatten(tree1)), flatten(tree2)), element)
67.           == listContains(Cons(x, append(flatten(tree1), flatten(tree2))), element)
68.           == (x == element) || listContains(append(flatten(tree1), flatten(tree2)), element)
69.           == (x == element) || listContains(flatten(tree1), element) || listContains(flatten(tree2), element);
70.     }
71.   }
72. }
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top