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. OK, I Understand
 
Top