list.why 10.1 KB
 Jean-Christophe Filliâtre committed Mar 23, 2010 1 `````` `````` MARCHE Claude committed Apr 20, 2012 2 3 4 5 ``````(** {1 Polymorphic Lists} *) (** {2 Basic theory of polymorphic lists} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 6 7 ``````theory List `````` Andrei Paskevich committed Jun 24, 2010 8 `````` type list 'a = Nil | Cons 'a (list 'a) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 9 10 11 `````` end `````` MARCHE Claude committed Apr 20, 2012 12 13 ``````(** {2 Length of a list} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 14 ``````theory Length `````` 15 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 16 17 18 `````` use import int.Int use import List `````` Andrei Paskevich committed Jun 29, 2011 19 `````` function length (l: list 'a) : int = `````` Jean-Christophe Filliâtre committed Mar 23, 2010 20 `````` match l with `````` Andrei Paskevich committed Jun 17, 2010 21 `````` | Nil -> 0 `````` Jean-Christophe Filliâtre committed Nov 29, 2010 22 `````` | Cons _ r -> 1 + length r `````` Jean-Christophe Filliâtre committed Mar 23, 2010 23 24 `````` end `````` Jean-Christophe Filliâtre committed Aug 03, 2011 25 `````` lemma Length_nonnegative: forall l: list 'a. length l >= 0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 26 `````` `````` Jean-Christophe Filliâtre committed Jun 22, 2011 27 `````` lemma Length_nil: forall l: list 'a. length l = 0 <-> l = Nil `````` Jean-Christophe Filliâtre committed Nov 10, 2010 28 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 29 30 ``````end `````` MARCHE Claude committed Apr 20, 2012 31 32 ``````(** {2 Membership in a list} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 33 34 ``````theory Mem use export List `````` MARCHE Claude committed Dec 15, 2010 35 `````` `````` Andrei Paskevich committed Jun 29, 2011 36 `````` predicate mem (x: 'a) (l: list 'a) = match l with `````` Andrei Paskevich committed Jun 17, 2010 37 `````` | Nil -> false `````` Andrei Paskevich committed Jun 29, 2011 38 `````` | Cons y r -> x = y \/ mem x r `````` Jean-Christophe Filliâtre committed Mar 23, 2010 39 40 41 42 `````` end end `````` MARCHE Claude committed Aug 24, 2012 43 44 45 46 47 48 49 50 51 52 53 54 ``````theory Elements use import List use Mem use set.Fset as FSet function elements (list 'a) : FSet.set 'a axiom elements_mem: forall l:list 'a, x:'a. Mem.mem x l <-> FSet.mem x (elements l) `````` MARCHE Claude committed Aug 24, 2012 55 56 57 `````` lemma elements_Nil: elements (Nil : list 'a) = FSet.empty `````` MARCHE Claude committed Aug 24, 2012 58 59 ``````end `````` MARCHE Claude committed Apr 20, 2012 60 61 ``````(** {2 Nth element of a list} *) `````` 62 ``````theory Nth `````` 63 `````` `````` 64 `````` use export List `````` Jean-Christophe Filliâtre committed Nov 10, 2010 65 `````` use export option.Option `````` 66 `````` use import int.Int `````` MARCHE Claude committed Dec 15, 2010 67 `````` `````` Andrei Paskevich committed Jun 29, 2011 68 `````` function nth (n: int) (l: list 'a) : option 'a = match l with `````` Jean-Christophe Filliâtre committed Jun 22, 2011 69 `````` | Nil -> None `````` Jean-Christophe Filliâtre committed Nov 10, 2010 70 `````` | Cons x r -> if n = 0 then Some x else nth (n - 1) r `````` 71 72 73 74 `````` end end `````` MARCHE Claude committed Jul 08, 2013 75 76 77 78 79 ``````theory NthNoOpt use export List use import int.Int `````` MARCHE Claude committed Dec 10, 2013 80 `````` function nth (n: int) (l: list 'a) : 'a `````` MARCHE Claude committed Jul 08, 2013 81 82 83 84 85 86 87 `````` axiom nth_cons_0: forall x:'a, r:list 'a. nth 0 (Cons x r) = x axiom nth_cons_n: forall x:'a, r:list 'a, n:int. n > 0 -> nth n (Cons x r) = nth (n-1) r end `````` Jean-Christophe Filliâtre committed Jul 21, 2012 88 89 90 91 92 93 94 ``````theory NthLength use export Nth use export Length use import int.Int lemma nth_none_1: `````` Jean-Christophe Filliâtre committed Dec 21, 2012 95 `````` forall l: list 'a, i: int. i < 0 -> nth i l = None `````` Jean-Christophe Filliâtre committed Jul 21, 2012 96 97 `````` lemma nth_none_2: `````` Jean-Christophe Filliâtre committed Dec 21, 2012 98 `````` forall l: list 'a, i: int. i >= length l -> nth i l = None `````` Jean-Christophe Filliâtre committed Jul 21, 2012 99 100 101 102 103 104 `````` lemma nth_none_3: forall l: list 'a, i: int. nth i l = None -> i < 0 \/ i >= length l end `````` MARCHE Claude committed Apr 20, 2012 105 106 ``````(** {2 Head and tail} *) `````` 107 ``````theory HdTl `````` Jean-Christophe Filliâtre committed Nov 15, 2010 108 109 110 111 `````` use export List use export option.Option `````` Andrei Paskevich committed Jun 29, 2011 112 `````` function hd (l: list 'a) : option 'a = match l with `````` Jean-Christophe Filliâtre committed Jun 22, 2011 113 `````` | Nil -> None `````` Jean-Christophe Filliâtre committed Nov 15, 2010 114 115 116 `````` | Cons h _ -> Some h end `````` Andrei Paskevich committed Jun 29, 2011 117 `````` function tl (l: list 'a) : option (list 'a) = match l with `````` Jean-Christophe Filliâtre committed Jun 22, 2011 118 `````` | Nil -> None `````` Jean-Christophe Filliâtre committed Nov 15, 2010 119 120 121 `````` | Cons _ t -> Some t end `````` Jean-Christophe Filliâtre committed Feb 17, 2011 122 123 ``````end `````` MARCHE Claude committed Dec 10, 2013 124 125 126 127 128 129 130 131 132 133 134 135 136 137 ``````theory HdTlNoOpt use export List function hd (l: list 'a) : 'a axiom hd_cons: forall x:'a, r:list 'a. hd (Cons x r) = x function tl (l: list 'a) : list 'a axiom tl_cons: forall x:'a, r:list 'a. tl (Cons x r) = r end `````` 138 ``````(** {2 Relation between head, tail, and nth} *) `````` MARCHE Claude committed Apr 20, 2012 139 `````` `````` Jean-Christophe Filliâtre committed Feb 17, 2011 140 141 ``````theory NthHdTl `````` Jean-Christophe Filliâtre committed Nov 15, 2010 142 `````` use import int.Int `````` Jean-Christophe Filliâtre committed Feb 17, 2011 143 144 `````` use import Nth use import HdTl `````` Jean-Christophe Filliâtre committed Nov 15, 2010 145 `````` `````` Jean-Christophe Filliâtre committed Jun 22, 2011 146 147 `````` lemma Nth_tl: forall l1 l2: list 'a. tl l1 = Some l2 -> `````` 148 `````` forall i: int. i <> -1 -> nth i l2 = nth (i+1) l1 `````` Jean-Christophe Filliâtre committed Nov 15, 2010 149 150 `````` lemma Nth0_head: `````` Jean-Christophe Filliâtre committed Jun 22, 2011 151 `````` forall l: list 'a. nth 0 l = hd l `````` Jean-Christophe Filliâtre committed Nov 15, 2010 152 153 154 `````` end `````` MARCHE Claude committed Apr 20, 2012 155 ``````(** {2 Appending two lists} *) `````` Jean-Christophe Filliâtre committed Nov 15, 2010 156 `````` `````` Jean-Christophe Filliâtre committed Nov 10, 2010 157 158 159 ``````theory Append use export List `````` Andrei Paskevich committed Jun 29, 2011 160 `````` function (++) (l1 l2: list 'a) : list 'a = match l1 with `````` Jean-Christophe Filliâtre committed Nov 10, 2010 161 `````` | Nil -> l2 `````` Jean-Christophe Filliâtre committed Feb 18, 2011 162 `````` | Cons x1 r1 -> Cons x1 (r1 ++ l2) `````` Jean-Christophe Filliâtre committed Nov 10, 2010 163 164 `````` end `````` Jean-Christophe Filliâtre committed Jun 22, 2011 165 166 `````` lemma Append_assoc: forall l1 l2 l3: list 'a. `````` Jean-Christophe Filliâtre committed Feb 18, 2011 167 `````` l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3 `````` Jean-Christophe Filliâtre committed Nov 10, 2010 168 `````` `````` Jean-Christophe Filliâtre committed Jun 22, 2011 169 170 `````` lemma Append_l_nil: forall l: list 'a. l ++ Nil = l `````` Jean-Christophe Filliâtre committed Nov 10, 2010 171 172 173 174 `````` use import Length use import int.Int `````` Jean-Christophe Filliâtre committed Jun 22, 2011 175 176 `````` lemma Append_length: forall l1 l2: list 'a. length (l1 ++ l2) = length l1 + length l2 `````` Jean-Christophe Filliâtre committed Nov 10, 2010 177 `````` `````` 178 179 `````` use import Mem `````` Jean-Christophe Filliâtre committed Jun 22, 2011 180 181 `````` lemma mem_append: forall x: 'a, l1 l2: list 'a. `````` Andrei Paskevich committed Jun 29, 2011 182 `````` mem x (l1 ++ l2) <-> mem x l1 \/ mem x l2 `````` 183 `````` `````` Jean-Christophe Filliâtre committed Aug 02, 2011 184 185 186 187 `````` lemma mem_decomp: forall x: 'a, l: list 'a. mem x l -> exists l1 l2: list 'a. l = l1 ++ Cons x l2 `````` Jean-Christophe Filliâtre committed Nov 10, 2010 188 189 ``````end `````` Jean-Christophe Filliâtre committed Jul 21, 2012 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 ``````theory NthLengthAppend use export NthLength use export Append use import int.Int lemma nth_append_1: forall l1 l2: list 'a, i: int. i < length l1 -> nth i (l1 ++ l2) = nth i l1 lemma nth_append_2: forall l1 l2: list 'a, i: int. length l1 <= i -> nth i (l1 ++ l2) = nth (i - length l1) l2 end `````` Jean-Christophe Filliâtre committed Apr 11, 2013 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 ``````(** {2 Reversing a list} *) theory Reverse use export List use import Append function reverse (l: list 'a) : list 'a = match l with | Nil -> Nil | Cons x r -> reverse r ++ Cons x Nil end lemma reverse_append: forall l1 l2: list 'a, x: 'a. (reverse (Cons x l1)) ++ l2 = (reverse l1) ++ (Cons x l2) lemma reverse_reverse: forall l: list 'a. reverse (reverse l) = l use import Length lemma Reverse_length: forall l: list 'a. length (reverse l) = length l end `````` Jean-Christophe Filliâtre committed Apr 11, 2013 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 ``````(** {2 Reverse append} *) theory RevAppend use import List function rev_append (s t: list 'a) : list 'a = match s with | Cons x r -> rev_append r (Cons x t) | Nil -> t end use import Append lemma rev_append_append_l: forall r s t: list 'a. rev_append (r ++ s) t = rev_append s (rev_append r t) lemma rev_append_append_r: forall r s t: list 'a. rev_append r (s ++ t) = rev_append (rev_append s r) t use import int.Int use import Length lemma rev_append_length: forall s t: list 'a. length (rev_append s t) = length s + length t end `````` Jean-Christophe Filliâtre committed Jun 12, 2013 263 264 265 266 267 268 269 270 271 272 273 274 275 276 ``````(** {2 Zip} *) theory Combine use export List function combine (x: list 'a) (y: list 'b) : list ('a, 'b) = match x, y with | Cons x0 x, Cons y0 y -> Cons (x0, y0) (combine x y) | _ -> Nil end end `````` MARCHE Claude committed Apr 20, 2012 277 278 ``````(** {2 Sorted lists for some order as parameter} *) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 279 280 281 ``````theory Sorted use export List `````` MARCHE Claude committed Dec 15, 2010 282 `````` `````` Jean-Christophe Filliâtre committed Sep 15, 2011 283 284 285 286 `````` type t predicate le t t inductive sorted (l: list t) = `````` Jean-Christophe Filliâtre committed Jun 22, 2011 287 `````` | Sorted_Nil: `````` Jean-Christophe Filliâtre committed Jul 07, 2010 288 `````` sorted Nil `````` Jean-Christophe Filliâtre committed Jun 22, 2011 289 `````` | Sorted_One: `````` Jean-Christophe Filliâtre committed Sep 15, 2011 290 `````` forall x: t. sorted (Cons x Nil) `````` Jean-Christophe Filliâtre committed Jun 22, 2011 291 `````` | Sorted_Two: `````` Jean-Christophe Filliâtre committed Sep 15, 2011 292 293 `````` forall x y: t, l: list t. le x y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) `````` MARCHE Claude committed Dec 15, 2010 294 `````` `````` Jean-Christophe Filliâtre committed Jul 07, 2010 295 296 `````` use import Mem `````` Jean-Christophe Filliâtre committed Sep 15, 2011 297 298 299 300 301 302 `````` lemma sorted_mem: forall x: t, l: list t. (forall y: t. mem y l -> le x y) /\ sorted l <-> sorted (Cons x l) end `````` MARCHE Claude committed Apr 20, 2012 303 304 ``````(** {2 Sorted lists of integers} *) `````` Jean-Christophe Filliâtre committed Sep 15, 2011 305 306 307 308 ``````theory SortedInt use import int.Int clone export Sorted with type t = int, predicate le = (<=) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 309 310 311 `````` end `````` Jean-Christophe Filliâtre committed Apr 11, 2013 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 ``````theory RevSorted type t predicate le t t predicate ge (x y: t) = le y x use import List clone Sorted as Incr with type t = t, predicate le = le clone Sorted as Decr with type t = t, predicate le = ge predicate compat (s t: list t) = match s, t with | Cons x _, Cons y _ -> le x y | _, _ -> true end use import RevAppend lemma rev_append_sorted_incr: forall s t: list t. Incr.sorted (rev_append s t) <-> Decr.sorted s /\ Incr.sorted t /\ compat s t lemma rev_append_sorted_decr: forall s t: list t. Decr.sorted (rev_append s t) <-> Incr.sorted s /\ Decr.sorted t /\ compat t s (* use import Reverse lemma rev_sorted_incr: forall s: list t. Incr.sorted (reverse s) <-> Decr.sorted s lemma rev_sorted_decr: forall s: list t. Decr.sorted (reverse s) <-> Incr.sorted s *) end `````` MARCHE Claude committed Apr 20, 2012 352 353 ``````(** {2 Number of occurrences in a list} *) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 354 ``````theory NumOcc `````` MARCHE Claude committed Dec 15, 2010 355 `````` `````` Jean-Christophe Filliâtre committed Jul 07, 2010 356 357 358 `````` use import int.Int use import List `````` MARCHE Claude committed Oct 04, 2013 359 `````` (** number of occurrences of [x] in [l] *) `````` Andrei Paskevich committed Jun 29, 2011 360 `````` function num_occ (x: 'a) (l: list 'a) : int = `````` Jean-Christophe Filliâtre committed Jul 07, 2010 361 `````` match l with `````` Jean-Christophe Filliâtre committed Jun 22, 2011 362 `````` | Nil -> 0 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 363 364 365 366 367 `````` | Cons y r -> (if x = y then 1 else 0) + num_occ x r end use import Mem `````` MARCHE Claude committed Dec 15, 2010 368 `````` lemma Mem_Num_Occ : `````` Jean-Christophe Filliâtre committed Jun 22, 2011 369 `````` forall x: 'a, l: list 'a. mem x l <-> num_occ x l > 0 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 370 `````` `````` Jean-Christophe Filliâtre committed Jan 20, 2012 371 372 373 374 375 376 `````` use import Append lemma Append_Num_Occ : forall x: 'a, l1 l2: list 'a. num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 377 378 ``````end `````` MARCHE Claude committed Apr 20, 2012 379 380 ``````(** {2 Permutation of lists} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 381 ``````theory Permut `````` Jean-Christophe Filliâtre committed Jul 07, 2010 382 383 384 385 `````` use import NumOcc use import List `````` Andrei Paskevich committed Jun 29, 2011 386 `````` predicate permut (l1: list 'a) (l2: list 'a) = `````` Jean-Christophe Filliâtre committed Jun 22, 2011 387 `````` forall x: 'a. num_occ x l1 = num_occ x l2 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 388 `````` `````` Jean-Christophe Filliâtre committed Jun 22, 2011 389 `````` lemma Permut_refl: forall l: list 'a. permut l l `````` Jean-Christophe Filliâtre committed Jul 07, 2010 390 `````` `````` Jean-Christophe Filliâtre committed Jun 22, 2011 391 `````` lemma Permut_sym: forall l1 l2: list 'a. permut l1 l2 -> permut l2 l1 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 392 `````` `````` Jean-Christophe Filliâtre committed Jun 22, 2011 393 394 `````` lemma Permut_trans: forall l1 l2 l3: list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 395 `````` `````` Jean-Christophe Filliâtre committed Jun 22, 2011 396 397 `````` lemma Permut_cons: forall x: 'a, l1 l2: list 'a. `````` Jean-Christophe Filliâtre committed Jul 07, 2010 398 399 `````` permut l1 l2 -> permut (Cons x l1) (Cons x l2) `````` Jean-Christophe Filliâtre committed Jun 22, 2011 400 401 `````` lemma Permut_swap: forall x y: 'a, l: list 'a. permut (Cons x (Cons y l)) (Cons y (Cons x l)) `````` MARCHE Claude committed Dec 15, 2010 402 `````` `````` Jean-Christophe Filliâtre committed Jan 20, 2012 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 `````` use import Append lemma Permut_cons_append: forall x : 'a, l1 l2 : list 'a. permut (Cons x l1 ++ l2) (l1 ++ Cons x l2) lemma Permut_assoc: forall l1 l2 l3: list 'a. permut ((l1 ++ l2) ++ l3) (l1 ++ (l2 ++ l3)) lemma Permut_append: forall l1 l2 k1 k2 : list 'a. permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2) lemma Permut_append_swap: forall l1 l2 : list 'a. permut (l1 ++ l2) (l2 ++ l1) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 421 422 `````` use import Mem `````` Jean-Christophe Filliâtre committed Jun 22, 2011 423 424 `````` lemma Permut_mem: forall x: 'a, l1 l2: list 'a. permut l1 l2 -> mem x l1 -> mem x l2 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 425 426 427 `````` use import Length `````` Jean-Christophe Filliâtre committed Jun 22, 2011 428 429 `````` lemma Permut_length: forall l1 l2: list 'a. permut l1 l2 -> length l1 = length l2 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 430 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 431 432 ``````end `````` MARCHE Claude committed Apr 20, 2012 433 434 ``````(** {2 List with pairwise distinct elements} *) `````` Jean-Christophe committed Mar 16, 2011 435 436 437 438 439 ``````theory Distinct use import List use import Mem `````` Jean-Christophe Filliâtre committed Jun 22, 2011 440 441 442 443 444 `````` inductive distinct (l: list 'a) = | distinct_zero: distinct (Nil: list 'a) | distinct_one : forall x:'a. distinct (Cons x Nil) | distinct_many: forall x:'a, l: list 'a. `````` Jean-Christophe committed Mar 16, 2011 445 446 447 448 `````` not (mem x l) -> distinct l -> distinct (Cons x l) use import Append `````` Jean-Christophe Filliâtre committed Jun 22, 2011 449 450 `````` lemma distinct_append: forall l1 l2: list 'a. `````` Jean-Christophe committed Mar 16, 2011 451 452 453 454 455 `````` distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) -> distinct (l1 ++ l2) end `````` Jean-Christophe Filliâtre committed Jan 09, 2013 456 457 458 459 460 461 462 463 464 465 466 467 468 469 ``````theory Prefix use export List use import int.Int function prefix (n: int) (l: list 'a) : list 'a = if n <= 0 then Nil else match l with | Nil -> Nil | Cons x r -> Cons x (prefix (n-1) r) end end `````` MARCHE Claude committed Apr 20, 2012 470 471 ``````(** {2 Induction on lists} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 472 ``````theory Induction `````` 473 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 474 475 `````` use import List `````` Jean-Christophe Filliâtre committed Jul 07, 2010 476 477 `````` type elt `````` Andrei Paskevich committed Jun 29, 2011 478 `````` predicate p (list elt) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 479 `````` `````` Jean-Christophe Filliâtre committed Jun 22, 2011 480 481 `````` axiom Induction: p (Nil: list elt) -> `````` Jean-Christophe Filliâtre committed Jul 07, 2010 482 483 `````` (forall x:elt. forall l:list elt. p l -> p (Cons x l)) -> forall l:list elt. p l `````` Jean-Christophe Filliâtre committed Mar 23, 2010 484 485 486 `````` end `````` MARCHE Claude committed Aug 24, 2012 487 `````` `````` MARCHE Claude committed Apr 20, 2012 488 489 ``````(** {2 Maps as lists of pairs} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 490 ``````theory Map `````` 491 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 492 `````` use import List `````` MARCHE Claude committed Dec 15, 2010 493 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 494 `````` type a `````` MARCHE Claude committed Dec 15, 2010 495 `````` type b `````` Andrei Paskevich committed Jun 29, 2011 496 `````` function f a : b `````` Jean-Christophe Filliâtre committed Mar 23, 2010 497 `````` `````` Jean-Christophe Filliâtre committed Aug 03, 2011 498 `````` function map (l: list a) : list b = `````` Jean-Christophe Filliâtre committed Mar 23, 2010 499 `````` match l with `````` Andrei Paskevich committed Jun 17, 2010 500 `````` | Nil -> Nil `````` Andrei Paskevich committed Jun 21, 2010 501 `````` | Cons x r -> Cons (f x) (map r) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 502 `````` end `````` Jean-Christophe Filliâtre committed Aug 03, 2011 503 504 ``````end `````` MARCHE Claude committed Apr 20, 2012 505 506 ``````(** {2 Generic recursors on lists} *) `````` Jean-Christophe Filliâtre committed Aug 03, 2011 507 ``````theory FoldLeft `````` 508 `````` `````` Jean-Christophe Filliâtre committed Aug 03, 2011 509 510 511 512 513 `````` use import List type a type b function f b a : b `````` Jean-Christophe Filliâtre committed Mar 23, 2010 514 `````` `````` Jean-Christophe Filliâtre committed Aug 03, 2011 515 516 517 518 519 `````` function fold_left (acc: b) (l: list a) : b = match l with | Nil -> acc | Cons x r -> fold_left (f acc x) r end `````` 520 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 521 522 ``````end `````` Jean-Christophe Filliâtre committed Aug 03, 2011 523 ``````theory FoldRight `````` 524 `````` `````` Jean-Christophe Filliâtre committed Aug 03, 2011 525 526 527 528 529 530 531 532 533 534 535 `````` use import List type a type b function f a b : b function fold_right (l: list a) (acc: b) : b = match l with | Nil -> acc | Cons x r -> f x (fold_right r acc) end `````` 536 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 537 ``````end `````` Jean-Christophe Filliâtre committed Feb 17, 2011 538 `````` `````` MARCHE Claude committed Apr 20, 2012 539 540 ``````(** {2 Importation of all list theories in one} *) `````` Jean-Christophe Filliâtre committed Feb 17, 2011 541 ``````theory ListRich `````` 542 `````` `````` Jean-Christophe Filliâtre committed Feb 17, 2011 543 544 545 546 547 548 549 550 551 552 553 `````` use export List use export Length use export Mem use export Nth use export HdTl use export NthHdTl use export Append use export Reverse use export Sorted use export NumOcc use export Permut `````` 554 `````` `````` Jean-Christophe Filliâtre committed Feb 17, 2011 555 ``end``