vstte12_tree_reconstruction.mlw 9.49 KB
Newer Older
 Jean-Christophe committed Feb 01, 2012 1 `````` `````` Jean-Christophe Filliatre committed Apr 11, 2012 2 ``````(* The 2nd Verified Software Competition (VSTTE 2012) `````` Jean-Christophe committed Feb 01, 2012 3 4 5 6 7 8 9 10 11 `````` https://sites.google.com/site/vstte2012/compet Problem 4: Tree Reconstruction Build a binary tree from a list of leaf depths, if any This is a purely applicative implementation, using immutable lists from Why3's standard library. *) `````` MARCHE Claude committed Feb 26, 2016 12 ``````module Tree `````` Jean-Christophe committed Feb 01, 2012 13 `````` `````` Jean-Christophe Filliatre committed Apr 15, 2012 14 15 16 `````` use export int.Int use export list.List use export list.Append `````` Jean-Christophe committed Feb 01, 2012 17 18 19 20 `````` type tree = Leaf | Node tree tree (* the list of leaf depths for tree t, if root is at depth d *) `````` Andrei Paskevich committed Jun 04, 2017 21 22 `````` let rec function depths (d: int) (t: tree) : list int = match t with `````` Jean-Christophe committed Feb 01, 2012 23 24 `````` | Leaf -> Cons d Nil | Node l r -> depths (d+1) l ++ depths (d+1) r `````` Andrei Paskevich committed Jun 04, 2017 25 `````` end `````` Jean-Christophe committed Feb 01, 2012 26 `````` `````` Jean-Christophe Filliatre committed Apr 24, 2012 27 28 `````` (* lemmas on depths *) `````` Jean-Christophe committed Feb 01, 2012 29 30 31 32 `````` lemma depths_head: forall t: tree, d: int. match depths d t with Cons x _ -> x >= d | Nil -> false end `````` MARCHE Claude committed Feb 26, 2016 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 `````` let rec lemma depths_unique (t1 t2: tree) (d: int) (s1 s2: list int) requires { depths d t1 ++ s1 = depths d t2 ++ s2 } variant { t1 } ensures { t1 = t2 && s1 = s2 } = let d' = d+1 in match t1,t2 with | Leaf,Leaf -> () | Node t11 t12, Node t21 t22 -> depths_unique t11 t21 d' (depths d' t12 ++ s1) (depths d' t22 ++ s2); depths_unique t12 t22 d' s1 s2 | Leaf, (Node t _) | (Node t _), Leaf -> match depths d' t with | Nil -> absurd | Cons x _ -> assert { x >= d' } end end `````` Jean-Christophe committed Feb 01, 2012 49 `````` `````` Jean-Christophe Filliatre committed Apr 24, 2012 50 51 52 53 54 55 56 57 `````` lemma depths_prefix: forall t: tree, d1 d2: int, s1 s2: list int. depths d1 t ++ s1 = depths d2 t ++ s2 -> d1 = d2 lemma depths_prefix_simple: forall t: tree, d1 d2: int. depths d1 t = depths d2 t -> d1 = d2 `````` MARCHE Claude committed Feb 26, 2016 58 59 60 61 62 63 64 65 66 67 `````` let rec lemma depths_subtree (t1 t2: tree) (d1 d2:int) (s1:list int) requires { depths d1 t1 ++ s1 = depths d2 t2 } variant { t1 } ensures { d1 >= d2 } = assert { depths d2 t2 = depths d2 t2 ++ Nil }; match t1 with | Leaf -> () | Node t3 t4 -> depths_subtree t3 t2 (d1+1) d2 (depths (d1+1) t4 ++ s1) end `````` Jean-Christophe Filliatre committed Apr 24, 2012 68 `````` `````` Jean-Christophe Filliatre committed Apr 24, 2012 69 70 71 72 `````` lemma depths_unique2: forall t1 t2: tree, d1 d2: int. depths d1 t1 = depths d2 t2 -> d1 = d2 && t1 = t2 `````` Jean-Christophe Filliatre committed Apr 15, 2012 73 74 75 76 77 ``````end module TreeReconstruction use export Tree `````` Andrei Paskevich committed Jun 15, 2018 78 79 `````` use list.Length use list.HdTlNoOpt `````` Jean-Christophe Filliatre committed May 31, 2018 80 `````` `````` Jean-Christophe committed Feb 01, 2012 81 82 83 `````` exception Failure (* used to signal the algorithm's failure i.e. there is no tree *) `````` Andrei Paskevich committed Jun 07, 2018 84 `````` let rec build_rec (d: int) (s: list int) : (t: tree, s': list int) `````` Jean-Christophe Filliatre committed Jun 05, 2018 85 `````` variant { length s, hd s - d } `````` Andrei Paskevich committed Jun 07, 2018 86 `````` ensures { s = depths d t ++ s' } `````` Andrei Paskevich committed Oct 13, 2012 87 88 `````` raises { Failure -> forall t: tree, s' : list int. depths d t ++ s' <> s } = match s with `````` Jean-Christophe committed Feb 01, 2012 89 90 91 92 93 `````` | Nil -> raise Failure | Cons h t -> if h < d then raise Failure; if h = d then `````` Andrei Paskevich committed Jun 11, 2017 94 `````` Leaf, t `````` Jean-Christophe committed Feb 01, 2012 95 96 97 `````` else let l, s = build_rec (d+1) s in let r, s = build_rec (d+1) s in `````` Andrei Paskevich committed Jun 11, 2017 98 `````` Node l r, s `````` Jean-Christophe committed Feb 01, 2012 99 100 `````` end `````` Andrei Paskevich committed Oct 13, 2012 101 102 103 104 `````` let build (s: list int) : tree ensures { depths 0 result = s } raises { Failure -> forall t: tree. depths 0 t <> s } = let t, s = build_rec 0 s in `````` Jean-Christophe committed Feb 01, 2012 105 106 107 108 109 110 111 112 113 `````` match s with | Nil -> t | _ -> raise Failure end end module Harness `````` Andrei Paskevich committed Jun 15, 2018 114 `````` use TreeReconstruction `````` Jean-Christophe committed Feb 01, 2012 115 `````` `````` Andrei Paskevich committed Oct 13, 2012 116 117 118 119 `````` let harness () ensures { result = Node Leaf (Node (Node Leaf Leaf) Leaf) } raises { Failure -> false } = build (Cons 1 (Cons 3 (Cons 3 (Cons 2 Nil)))) `````` Jean-Christophe committed Feb 01, 2012 120 `````` `````` Andrei Paskevich committed Oct 13, 2012 121 122 123 `````` let harness2 () ensures { false } raises { Failure -> true } = build (Cons 1 (Cons 3 (Cons 2 (Cons 2 Nil)))) `````` Jean-Christophe committed Feb 01, 2012 124 125 126 `````` end `````` Jean-Christophe Filliatre committed Apr 15, 2012 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 ``````(* A variant implementation proposed by Jayadev Misra Given the input list [x1; x2; ...; xn], we first turn it into the list of pairs [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)]. Then, repeatedly, we scan this list from left to right, looking for two consecutive pairs (v1, t1) and (v2, t2) with v1 = v2. Then we replace them with the pair (v1-1, Node t1 t2) and we start again. We stop when there is only one pair left (v,t). Then we must have v=0. The implementation below achieves linear complexity using a zipper data structure to traverse the list of pairs. The left list contains the elements already traversed (thus on the left), in reverse order, and the right list contains the elements yet to be traversed. *) `````` Jean-Christophe Filliatre committed Apr 24, 2012 144 145 146 147 148 ``````(* Proving termination is quite easy and we do it first (though we could, obviously, do it together with proving correctness) *) module ZipperBasedTermination `````` Andrei Paskevich committed Jun 15, 2018 149 150 151 `````` use Tree use list.Length use list.Reverse `````` Jean-Christophe Filliatre committed Apr 24, 2012 152 153 154 155 `````` exception Failure let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree `````` Andrei Paskevich committed Oct 13, 2012 156 `````` variant { length left + length right, length right } `````` Andrei Paskevich committed Mar 23, 2013 157 `````` raises { Failure } `````` Andrei Paskevich committed Oct 13, 2012 158 `````` = match left, right with `````` Jean-Christophe Filliatre committed Apr 24, 2012 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 `````` | _, Nil -> raise Failure | Nil, Cons (v, t) Nil -> if v = 0 then t else raise Failure | Nil, Cons (v, t) right' -> tc (Cons (v, t) Nil) right' | Cons (v1, t1) left', Cons (v2, t2) right' -> if v1 = v2 then tc left' (Cons (v1 - 1, Node t1 t2) right') else tc (Cons (v2, t2) left) right' end end (* Now soundness and completeness *) `````` Jean-Christophe Filliatre committed Apr 15, 2012 174 175 ``````module ZipperBased `````` Andrei Paskevich committed Jun 15, 2018 176 177 178 `````` use Tree use list.Length use list.Reverse `````` Jean-Christophe Filliatre committed Apr 15, 2012 179 `````` `````` Jean-Christophe Filliatre committed Apr 24, 2012 180 181 182 `````` (* the following function generalizes function [depths] to a forest, that is a list of pairs (depth, tree) *) `````` Jean-Christophe Filliatre committed Apr 15, 2012 183 184 185 186 187 `````` function forest_depths (f: list (int, tree)) : list int = match f with | Nil -> Nil | Cons (d, t) r -> depths d t ++ forest_depths r end `````` Jean-Christophe Filliatre committed Apr 24, 2012 188 189 `````` (* an obvious lemma on [forest_depths] *) `````` Jean-Christophe Filliatre committed Apr 15, 2012 190 191 192 193 `````` lemma forest_depths_append: forall f1 f2: list (int, tree). forest_depths (f1 ++ f2) = forest_depths f1 ++ forest_depths f2 `````` Jean-Christophe Filliatre committed Apr 24, 2012 194 195 196 `````` (* to prove completeness, one needs an invariant over the list [left]. The main ingredient is predicate [greedy] below, which states that [d] is distinct from all depths along the left branch of [d1, t1]. *) `````` Jean-Christophe Filliatre committed Apr 24, 2012 197 `````` `````` Jean-Christophe Filliatre committed Apr 24, 2012 198 199 200 201 202 203 `````` predicate greedy (d: int) (d1: int) (t1: tree) = d <> d1 /\ match t1 with Leaf -> true | Node l1 _ -> greedy d (d1+1) l1 end (* then we extend it to a list of pairs [(dn,tn); ...; (d2,t2); (d1,t1)] as follows: [greedy d2 d1 t1], [greedy d3 d2 t2], etc. this is inductive predicate [g] *) `````` Jean-Christophe Filliatre committed Apr 15, 2012 204 `````` `````` Jean-Christophe Filliatre committed Apr 24, 2012 205 206 207 `````` inductive g (l: list (int, tree)) = | Gnil: g Nil | Gone: forall d: int, t: tree. g (Cons (d, t) Nil) `````` Jean-Christophe Filliatre committed Apr 24, 2012 208 209 210 211 212 `````` | Gtwo: forall d1 d2: int, t1 t2: tree, l: list (int, tree). greedy d1 d2 t2 -> g (Cons (d1, t1) l) -> g (Cons (d2, t2) (Cons (d1, t1) l)) (* an easy lemma on [g] *) `````` Jean-Christophe Filliatre committed Apr 24, 2012 213 214 `````` lemma g_append: `````` Martin Clochard committed Apr 05, 2018 215 `````` forall l1 [@induction] l2: list (int, tree). g (l1 ++ l2) -> g l1 `````` Jean-Christophe Filliatre committed Apr 24, 2012 216 `````` `````` Jean-Christophe Filliatre committed Apr 24, 2012 217 218 219 220 221 222 `````` (* key lemma for completeness: whenever we fail because [right] is empty, we have to prove that there is no solution Note: the proof first generalizes the statement as follows: forest_depths ((d1,t1) :: l) <> depths d t + s whenever d < d1 (see the corresponding Coq file) *) `````` Jean-Christophe Filliatre committed Apr 24, 2012 223 `````` `````` Jean-Christophe Filliatre committed May 23, 2018 224 225 226 227 228 229 230 231 `````` lemma depths_length: forall t d. length (depths d t) >= 1 lemma forest_depths_length: forall l. length (forest_depths l) >= 0 lemma g_tail: forall l1 l2: list (int, tree). g (l1 ++ l2) -> g l2 lemma key_lemma : forall t l d d1 t1 s. d < d1 -> 1 <= length l -> g (reverse (Cons (d1, t1) l)) -> not (forest_depths (Cons (d1, t1) l) = (depths d t) ++ s) `````` Jean-Christophe Filliatre committed Apr 24, 2012 232 233 `````` lemma right_nil: forall l: list (int, tree). length l >= 2 -> g l -> `````` Jean-Christophe Filliatre committed Apr 24, 2012 234 235 236 237 238 `````` forall t: tree, d: int. forest_depths (reverse l) <> depths d t (* key lemma for soundness: preservation of the invariant when we move a tree from [right] to [left] *) `````` Jean-Christophe Filliatre committed Apr 24, 2012 239 240 241 `````` lemma main_lemma: forall l: list (int, tree), d1 d2: int, t1 t2: tree. d1 <> d2 -> `````` Jean-Christophe Filliatre committed Apr 24, 2012 242 243 244 245 246 247 248 249 250 251 252 `````` g (Cons (d1, t1) l) -> match t2 with Node l2 _ -> greedy d1 (d2+1) l2 | Leaf -> true end -> g (Cons (d2, t2) (Cons (d1, t1) l)) (* finally, we need a predicate to state that a forest [l] contains only leaves *) predicate only_leaf (l: list (int, tree)) = match l with | Nil -> true | Cons (_, t) r -> t = Leaf /\ only_leaf r end `````` Jean-Christophe Filliatre committed Apr 24, 2012 253 254 `````` exception Failure `````` Jean-Christophe Filliatre committed Apr 15, 2012 255 `````` `````` Andrei Paskevich committed Oct 13, 2012 256 257 `````` let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree requires { (* list [left] satisfies the invariant *) `````` Jean-Christophe Filliatre committed Apr 24, 2012 258 259 `````` g left /\ (* when [left] has one element, it can't be a solution *) `````` Andrei Paskevich committed Jan 19, 2014 260 261 `````` match left with Cons (d1, _) Nil -> d1 <> 0 \/ right <> Nil | _ -> true end /\ `````` Jean-Christophe Filliatre committed Apr 24, 2012 262 263 264 `````` (* apart (possibly) from its head, all elements in [right] are leaves; moreover the left branch of [right]'s head already satisfies invariant [g] when consed to [left] *) `````` Jean-Christophe Filliatre committed Apr 24, 2012 265 266 `````` match right with | Cons (d2, t2) right' -> only_leaf right' /\ `````` Jean-Christophe Filliatre committed Apr 24, 2012 267 `````` match t2 with Node l2 _ -> g (Cons (d2+1, l2) left) `````` Jean-Christophe Filliatre committed Apr 24, 2012 268 `````` | Leaf -> true end `````` Andrei Paskevich committed Oct 13, 2012 269 `````` | Nil -> true end } `````` MARCHE Claude committed Feb 12, 2014 270 `````` variant { length left + 2 * length right } `````` Andrei Paskevich committed Oct 13, 2012 271 272 273 274 `````` ensures { depths 0 result = forest_depths (reverse left ++ right) } raises { Failure -> forall t: tree. depths 0 t <> forest_depths (reverse left ++ right) } = match left, right with `````` Jean-Christophe Filliatre committed Apr 15, 2012 275 276 277 278 `````` | _, Nil -> raise Failure | Nil, Cons (v, t) Nil -> if v = 0 then t else raise Failure `````` Jean-Christophe Filliatre committed Apr 15, 2012 279 280 `````` | Nil, Cons (v, t) right' -> tc (Cons (v, t) Nil) right' `````` Jean-Christophe Filliatre committed Apr 15, 2012 281 282 283 284 285 `````` | Cons (v1, t1) left', Cons (v2, t2) right' -> if v1 = v2 then tc left' (Cons (v1 - 1, Node t1 t2) right') else tc (Cons (v2, t2) left) right' end `````` Jean-Christophe Filliatre committed Apr 24, 2012 286 287 288 289 290 `````` (* Getting function [build] from [tc] is easy: from the list [x1; x2; ...; xn] we simply build the list of pairs [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)]. Function [map_leaf] below does this. *) `````` Guillaume Melquiond committed Mar 17, 2016 291 292 293 294 295 `````` let rec function map_leaf (l: list int) : list (int, tree) = match l with | Nil -> Nil | Cons d r -> Cons (d, Leaf) (map_leaf r) end `````` Jean-Christophe Filliatre committed Apr 15, 2012 296 `````` `````` Jean-Christophe Filliatre committed Apr 24, 2012 297 298 `````` (* two lemmas on [map_leaf] *) `````` Jean-Christophe Filliatre committed Apr 15, 2012 299 300 301 `````` lemma map_leaf_depths: forall l: list int. forest_depths (map_leaf l) = l `````` Jean-Christophe Filliatre committed Apr 24, 2012 302 303 304 `````` lemma map_leaf_only_leaf: forall l: list int. only_leaf (map_leaf l) `````` Andrei Paskevich committed Oct 13, 2012 305 306 307 308 `````` let build (s: list int) ensures { depths 0 result = s } raises { Failure -> forall t: tree. depths 0 t <> s } = tc Nil (map_leaf s) `````` Jean-Christophe Filliatre committed Apr 15, 2012 309 310 `````` end``````