list.why 11.3 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 Filliatre committed Nov 29, 2010 22 `````` | Cons _ r -> 1 + length r `````` Jean-Christophe Filliâtre committed Mar 23, 2010 23 24 `````` end `````` Jean-Christophe Filliatre 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 Filliatre committed Jun 22, 2011 27 `````` lemma Length_nil: forall l: list 'a. length l = 0 <-> l = Nil `````` Jean-Christophe Filliatre 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 ``````theory Mem `````` Guillaume Melquiond committed Aug 21, 2014 34 `````` use import 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 `````` `````` Guillaume Melquiond committed Aug 21, 2014 64 65 `````` use import List use import 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 Filliatre committed Jun 22, 2011 69 `````` | Nil -> None `````` Jean-Christophe Filliatre 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 ``````theory NthNoOpt `````` Guillaume Melquiond committed Aug 21, 2014 77 `````` use import List `````` MARCHE Claude committed Jul 08, 2013 78 79 `````` 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 committed Jul 21, 2012 88 89 ``````theory NthLength `````` Guillaume Melquiond committed Aug 21, 2014 90 91 92 `````` use import int.Int use import option.Option use import List `````` Jean-Christophe committed Jul 21, 2012 93 94 95 96 `````` use export Nth use export Length lemma nth_none_1: `````` Jean-Christophe Filliatre committed Dec 21, 2012 97 `````` forall l: list 'a, i: int. i < 0 -> nth i l = None `````` Jean-Christophe committed Jul 21, 2012 98 99 `````` lemma nth_none_2: `````` Jean-Christophe Filliatre committed Dec 21, 2012 100 `````` forall l: list 'a, i: int. i >= length l -> nth i l = None `````` Jean-Christophe committed Jul 21, 2012 101 102 103 104 105 106 `````` 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 107 108 ``````(** {2 Head and tail} *) `````` 109 ``````theory HdTl `````` Jean-Christophe Filliatre committed Nov 15, 2010 110 `````` `````` Guillaume Melquiond committed Aug 21, 2014 111 112 `````` use import List use import option.Option `````` Jean-Christophe Filliatre committed Nov 15, 2010 113 `````` `````` Andrei Paskevich committed Jun 29, 2011 114 `````` function hd (l: list 'a) : option 'a = match l with `````` Jean-Christophe Filliatre committed Jun 22, 2011 115 `````` | Nil -> None `````` Jean-Christophe Filliatre committed Nov 15, 2010 116 117 118 `````` | Cons h _ -> Some h end `````` Andrei Paskevich committed Jun 29, 2011 119 `````` function tl (l: list 'a) : option (list 'a) = match l with `````` Jean-Christophe Filliatre committed Jun 22, 2011 120 `````` | Nil -> None `````` Jean-Christophe Filliatre committed Nov 15, 2010 121 122 123 `````` | Cons _ t -> Some t end `````` Jean-Christophe Filliatre committed Feb 17, 2011 124 125 ``````end `````` MARCHE Claude committed Dec 10, 2013 126 127 ``````theory HdTlNoOpt `````` Guillaume Melquiond committed Aug 21, 2014 128 `````` use import List `````` MARCHE Claude committed Dec 10, 2013 129 130 131 132 133 134 135 136 137 138 139 `````` 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 `````` 140 ``````(** {2 Relation between head, tail, and nth} *) `````` MARCHE Claude committed Apr 20, 2012 141 `````` `````` Jean-Christophe Filliatre committed Feb 17, 2011 142 143 ``````theory NthHdTl `````` Jean-Christophe Filliatre committed Nov 15, 2010 144 `````` use import int.Int `````` Guillaume Melquiond committed Aug 21, 2014 145 146 `````` use import option.Option use import List `````` Jean-Christophe Filliatre committed Feb 17, 2011 147 148 `````` use import Nth use import HdTl `````` Jean-Christophe Filliatre committed Nov 15, 2010 149 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 150 151 `````` lemma Nth_tl: forall l1 l2: list 'a. tl l1 = Some l2 -> `````` 152 `````` forall i: int. i <> -1 -> nth i l2 = nth (i+1) l1 `````` Jean-Christophe Filliatre committed Nov 15, 2010 153 154 `````` lemma Nth0_head: `````` Jean-Christophe Filliatre committed Jun 22, 2011 155 `````` forall l: list 'a. nth 0 l = hd l `````` Jean-Christophe Filliatre committed Nov 15, 2010 156 157 158 `````` end `````` MARCHE Claude committed Apr 20, 2012 159 ``````(** {2 Appending two lists} *) `````` Jean-Christophe Filliatre committed Nov 15, 2010 160 `````` `````` Jean-Christophe Filliatre committed Nov 10, 2010 161 ``````theory Append `````` Guillaume Melquiond committed Aug 21, 2014 162 163 `````` use import List `````` Jean-Christophe Filliatre committed Nov 10, 2010 164 `````` `````` Andrei Paskevich committed Jun 29, 2011 165 `````` function (++) (l1 l2: list 'a) : list 'a = match l1 with `````` Jean-Christophe Filliatre committed Nov 10, 2010 166 `````` | Nil -> l2 `````` Jean-Christophe Filliatre committed Feb 18, 2011 167 `````` | Cons x1 r1 -> Cons x1 (r1 ++ l2) `````` Jean-Christophe Filliatre committed Nov 10, 2010 168 169 `````` end `````` Jean-Christophe Filliatre committed Jun 22, 2011 170 `````` lemma Append_assoc: `````` Léon Gondelman committed Sep 18, 2014 171 `````` forall l1 "induction" l2 l3: list 'a. `````` Jean-Christophe Filliatre committed Feb 18, 2011 172 `````` l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3 `````` Jean-Christophe Filliatre committed Nov 10, 2010 173 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 174 175 `````` lemma Append_l_nil: forall l: list 'a. l ++ Nil = l `````` Jean-Christophe Filliatre committed Nov 10, 2010 176 177 178 179 `````` use import Length use import int.Int `````` Jean-Christophe Filliatre committed Jun 22, 2011 180 `````` lemma Append_length: `````` Léon Gondelman committed Sep 18, 2014 181 `````` forall l1 "induction" l2: list 'a. length (l1 ++ l2) = length l1 + length l2 `````` Jean-Christophe Filliatre committed Nov 10, 2010 182 `````` `````` 183 184 `````` use import Mem `````` Jean-Christophe Filliatre committed Jun 22, 2011 185 `````` lemma mem_append: `````` Léon Gondelman committed Sep 18, 2014 186 `````` forall x: 'a, l1 "induction" l2: list 'a. `````` Andrei Paskevich committed Jun 29, 2011 187 `````` mem x (l1 ++ l2) <-> mem x l1 \/ mem x l2 `````` 188 `````` `````` Jean-Christophe Filliatre committed Aug 02, 2011 189 190 191 192 `````` lemma mem_decomp: forall x: 'a, l: list 'a. mem x l -> exists l1 l2: list 'a. l = l1 ++ Cons x l2 `````` Jean-Christophe Filliatre committed Nov 10, 2010 193 194 ``````end `````` Jean-Christophe committed Jul 21, 2012 195 196 ``````theory NthLengthAppend `````` Guillaume Melquiond committed Aug 21, 2014 197 198 `````` use import int.Int use import List `````` Jean-Christophe committed Jul 21, 2012 199 200 201 202 203 204 205 206 `````` use export NthLength use export Append 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: `````` Léon Gondelman committed Sep 18, 2014 207 `````` forall l1 "induction" l2: list 'a, i: int. `````` Jean-Christophe committed Jul 21, 2012 208 209 210 211 `````` length l1 <= i -> nth i (l1 ++ l2) = nth (i - length l1) l2 end `````` Jean-Christophe Filliatre committed Apr 11, 2013 212 213 214 215 ``````(** {2 Reversing a list} *) theory Reverse `````` Guillaume Melquiond committed Aug 21, 2014 216 `````` use import List `````` Jean-Christophe Filliatre committed Apr 11, 2013 217 218 219 220 221 222 223 224 225 226 227 `````` 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) `````` Jean-Christophe Filliatre committed Mar 29, 2014 228 229 230 231 `````` lemma reverse_cons: forall l: list 'a, x: 'a. reverse (Cons x l) = reverse l ++ Cons x Nil `````` Léon Gondelman committed Sep 18, 2014 232 233 234 235 236 `````` lemma cons_reverse: forall l: list 'a, x: 'a. Cons x (reverse l) = reverse (l ++ Cons x Nil) `````` Jean-Christophe Filliatre committed Apr 11, 2013 237 238 239 `````` lemma reverse_reverse: forall l: list 'a. reverse (reverse l) = l `````` Jean-Christophe Filliatre committed Mar 29, 2014 240 241 242 243 244 `````` use import Mem lemma reverse_mem: forall l: list 'a, x: 'a. mem x l <-> mem x (reverse l) `````` Jean-Christophe Filliatre committed Apr 11, 2013 245 246 247 248 249 250 251 `````` use import Length lemma Reverse_length: forall l: list 'a. length (reverse l) = length l end `````` Jean-Christophe Filliatre committed Apr 11, 2013 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 ``````(** {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: `````` Léon Gondelman committed Sep 18, 2014 267 `````` forall r "induction" s t: list 'a. `````` Jean-Christophe Filliatre committed Apr 11, 2013 268 269 `````` rev_append (r ++ s) t = rev_append s (rev_append r t) `````` Léon Gondelman committed Sep 18, 2014 270 `````` `````` Jean-Christophe Filliatre committed Apr 11, 2013 271 272 273 274 275 `````` use import int.Int use import Length lemma rev_append_length: `````` Léon Gondelman committed Sep 18, 2014 276 `````` forall s "induction" t: list 'a. `````` Jean-Christophe Filliatre committed Apr 11, 2013 277 278 `````` length (rev_append s t) = length s + length t `````` Jean-Christophe Filliatre committed Mar 29, 2014 279 280 281 `````` use import Reverse lemma rev_append_def: `````` Léon Gondelman committed Sep 18, 2014 282 283 284 285 286 287 `````` forall r "induction" s: list 'a. rev_append r s = reverse r ++ s lemma rev_append_append_r: forall r s t: list 'a. rev_append r (s ++ t) = rev_append (rev_append s r) t `````` Jean-Christophe Filliatre committed Mar 29, 2014 288 `````` `````` Jean-Christophe Filliatre committed Apr 11, 2013 289 290 ``````end `````` Jean-Christophe Filliatre committed Jun 12, 2013 291 292 293 294 ``````(** {2 Zip} *) theory Combine `````` Guillaume Melquiond committed Aug 21, 2014 295 `````` use import List `````` Jean-Christophe Filliatre committed Jun 12, 2013 296 297 298 299 300 301 302 303 304 `````` 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 305 306 ``````(** {2 Sorted lists for some order as parameter} *) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 307 308 ``````theory Sorted `````` Guillaume Melquiond committed Aug 21, 2014 309 `````` use import List `````` MARCHE Claude committed Dec 15, 2010 310 `````` `````` Jean-Christophe Filliatre committed Sep 15, 2011 311 312 `````` type t predicate le t t `````` Léon Gondelman committed Sep 18, 2014 313 `````` clone relations.Transitive with type t = t, predicate rel = le `````` Jean-Christophe Filliatre committed Sep 15, 2011 314 315 `````` inductive sorted (l: list t) = `````` Jean-Christophe Filliatre committed Jun 22, 2011 316 `````` | Sorted_Nil: `````` Jean-Christophe Filliâtre committed Jul 07, 2010 317 `````` sorted Nil `````` Jean-Christophe Filliatre committed Jun 22, 2011 318 `````` | Sorted_One: `````` Jean-Christophe Filliatre committed Sep 15, 2011 319 `````` forall x: t. sorted (Cons x Nil) `````` Jean-Christophe Filliatre committed Jun 22, 2011 320 `````` | Sorted_Two: `````` Jean-Christophe Filliatre committed Sep 15, 2011 321 322 `````` 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 323 `````` `````` Jean-Christophe Filliâtre committed Jul 07, 2010 324 325 `````` use import Mem `````` Jean-Christophe Filliatre committed Sep 15, 2011 326 327 328 329 `````` lemma sorted_mem: forall x: t, l: list t. (forall y: t. mem y l -> le x y) /\ sorted l <-> sorted (Cons x l) `````` Jean-Christophe Filliatre committed Mar 29, 2014 330 331 332 `````` use import Append lemma sorted_append: `````` Léon Gondelman committed Sep 18, 2014 333 `````` forall l1 "induction" l2: list t. `````` Jean-Christophe Filliatre committed Apr 01, 2014 334 335 `````` (sorted l1 /\ sorted l2 /\ (forall x y: t. mem x l1 -> mem y l2 -> le x y)) <-> `````` Jean-Christophe Filliatre committed Mar 29, 2014 336 337 `````` sorted (l1 ++ l2) `````` Jean-Christophe Filliatre committed Sep 15, 2011 338 339 ``````end `````` MARCHE Claude committed Apr 20, 2012 340 341 ``````(** {2 Sorted lists of integers} *) `````` Jean-Christophe Filliatre committed Sep 15, 2011 342 343 344 ``````theory SortedInt use import int.Int `````` Léon Gondelman committed Sep 18, 2014 345 `````` clone export Sorted with type t = int, predicate le = (<=), goal Transitive.Trans `````` Jean-Christophe Filliâtre committed Jul 07, 2010 346 347 348 `````` end `````` Jean-Christophe Filliatre committed Apr 11, 2013 349 350 351 352 ``````theory RevSorted type t predicate le t t `````` Léon Gondelman committed Sep 18, 2014 353 `````` clone import relations.Transitive with type t = t, predicate rel = le `````` Jean-Christophe Filliatre committed Apr 11, 2013 354 355 356 357 `````` predicate ge (x y: t) = le y x use import List `````` Léon Gondelman committed Sep 18, 2014 358 359 `````` clone Sorted as Incr with type t = t, predicate le = le, goal Transitive.Trans clone Sorted as Decr with type t = t, predicate le = ge, goal Transitive.Trans `````` Jean-Christophe Filliatre committed Apr 11, 2013 360 361 362 363 364 365 366 367 368 369 `````` 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: `````` Léon Gondelman committed Sep 18, 2014 370 `````` forall s "induction" t: list t. `````` Jean-Christophe Filliatre committed Apr 11, 2013 371 372 373 374 `````` Incr.sorted (rev_append s t) <-> Decr.sorted s /\ Incr.sorted t /\ compat s t lemma rev_append_sorted_decr: `````` Léon Gondelman committed Sep 18, 2014 375 `````` forall s "induction" t: list t. `````` Jean-Christophe Filliatre committed Apr 11, 2013 376 377 378 379 380 `````` Decr.sorted (rev_append s t) <-> Incr.sorted s /\ Decr.sorted t /\ compat t s end `````` MARCHE Claude committed Apr 20, 2012 381 382 ``````(** {2 Number of occurrences in a list} *) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 383 ``````theory NumOcc `````` MARCHE Claude committed Dec 15, 2010 384 `````` `````` Jean-Christophe Filliâtre committed Jul 07, 2010 385 386 387 `````` use import int.Int use import List `````` Andrei Paskevich committed Jun 29, 2011 388 `````` function num_occ (x: 'a) (l: list 'a) : int = `````` Jean-Christophe Filliâtre committed Jul 07, 2010 389 `````` match l with `````` Jean-Christophe Filliatre committed Jun 22, 2011 390 `````` | Nil -> 0 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 391 `````` | Cons y r -> (if x = y then 1 else 0) + num_occ x r `````` Guillaume Melquiond committed Jan 28, 2014 392 393 `````` end (** number of occurrences of [x] in [l] *) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 394 `````` `````` MARCHE Claude committed Nov 19, 2014 395 `````` lemma Num_Occ_NonNeg: forall x:'a, l: list 'a. num_occ x l >= 0 `````` Léon Gondelman committed Sep 18, 2014 396 `````` `````` Jean-Christophe Filliâtre committed Jul 07, 2010 397 398 `````` use import Mem `````` MARCHE Claude committed Dec 15, 2010 399 `````` lemma Mem_Num_Occ : `````` Jean-Christophe Filliatre committed Jun 22, 2011 400 `````` forall x: 'a, l: list 'a. mem x l <-> num_occ x l > 0 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 401 `````` `````` Jean-Christophe committed Jan 20, 2012 402 403 404 `````` use import Append lemma Append_Num_Occ : `````` Léon Gondelman committed Sep 18, 2014 405 `````` forall x: 'a, l1 "induction" l2: list 'a. `````` Jean-Christophe committed Jan 20, 2012 406 407 `````` num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2 `````` Jean-Christophe Filliatre committed Mar 29, 2014 408 409 410 411 412 413 `````` use import Reverse lemma reverse_num_occ : forall x: 'a, l: list 'a. num_occ x l = num_occ x (reverse l) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 414 415 ``````end `````` MARCHE Claude committed Apr 20, 2012 416 417 ``````(** {2 Permutation of lists} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 418 ``````theory Permut `````` Jean-Christophe Filliâtre committed Jul 07, 2010 419 420 421 422 `````` use import NumOcc use import List `````` Andrei Paskevich committed Jun 29, 2011 423 `````` predicate permut (l1: list 'a) (l2: list 'a) = `````` Jean-Christophe Filliatre committed Jun 22, 2011 424 `````` forall x: 'a. num_occ x l1 = num_occ x l2 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 425 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 426 `````` lemma Permut_refl: forall l: list 'a. permut l l `````` Jean-Christophe Filliâtre committed Jul 07, 2010 427 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 428 `````` lemma Permut_sym: forall l1 l2: list 'a. permut l1 l2 -> permut l2 l1 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 429 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 430 431 `````` 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 432 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 433 434 `````` lemma Permut_cons: forall x: 'a, l1 l2: list 'a. `````` Jean-Christophe Filliâtre committed Jul 07, 2010 435 436 `````` permut l1 l2 -> permut (Cons x l1) (Cons x l2) `````` Jean-Christophe Filliatre committed Jun 22, 2011 437 438 `````` 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 439 `````` `````` Jean-Christophe Filliatre committed Jan 20, 2012 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 `````` 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 458 459 `````` use import Mem `````` Jean-Christophe Filliatre committed Jun 22, 2011 460 461 `````` 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 462 463 464 `````` use import Length `````` Jean-Christophe Filliatre committed Jun 22, 2011 465 466 `````` lemma Permut_length: forall l1 l2: list 'a. permut l1 l2 -> length l1 = length l2 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 467 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 468 469 ``````end `````` MARCHE Claude committed Apr 20, 2012 470 471 ``````(** {2 List with pairwise distinct elements} *) `````` Jean-Christophe committed Mar 16, 2011 472 473 474 475 476 ``````theory Distinct use import List use import Mem `````` Jean-Christophe Filliatre committed Jun 22, 2011 477 478 479 480 481 `````` 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 482 483 484 485 `````` not (mem x l) -> distinct l -> distinct (Cons x l) use import Append `````` Jean-Christophe Filliatre committed Jun 22, 2011 486 `````` lemma distinct_append: `````` Léon Gondelman committed Sep 18, 2014 487 `````` forall l1 "induction" l2: list 'a. `````` Jean-Christophe committed Mar 16, 2011 488 489 490 491 492 `````` distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) -> distinct (l1 ++ l2) end `````` Jean-Christophe Filliatre committed Jan 09, 2013 493 494 ``````theory Prefix `````` Guillaume Melquiond committed Aug 21, 2014 495 `````` use import List `````` Jean-Christophe Filliatre committed Jan 09, 2013 496 497 498 499 500 501 502 503 504 505 506 `````` 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 `````` Jean-Christophe Filliatre committed Jun 08, 2014 507 508 ``````theory Sum `````` Guillaume Melquiond committed Aug 21, 2014 509 `````` use import List `````` Jean-Christophe Filliatre committed Jun 08, 2014 510 511 512 513 514 515 516 517 518 `````` use import int.Int function sum (l: list int) : int = match l with | Nil -> 0 | Cons x r -> x + sum r end end `````` MARCHE Claude committed Apr 20, 2012 519 520 ``````(** {2 Induction on lists} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 521 ``````theory Induction `````` 522 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 523 524 `````` use import List `````` Jean-Christophe Filliâtre committed Jul 07, 2010 525 526 `````` type elt `````` Andrei Paskevich committed Jun 29, 2011 527 `````` predicate p (list elt) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 528 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 529 530 `````` axiom Induction: p (Nil: list elt) -> `````` Jean-Christophe Filliâtre committed Jul 07, 2010 531 532 `````` (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 533 534 535 `````` end `````` MARCHE Claude committed Aug 24, 2012 536 `````` `````` MARCHE Claude committed Apr 20, 2012 537 538 ``````(** {2 Maps as lists of pairs} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 539 ``````theory Map `````` 540 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 541 `````` use import List `````` MARCHE Claude committed Dec 15, 2010 542 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 543 `````` type a `````` MARCHE Claude committed Dec 15, 2010 544 `````` type b `````` Andrei Paskevich committed Jun 29, 2011 545 `````` function f a : b `````` Jean-Christophe Filliâtre committed Mar 23, 2010 546 `````` `````` Jean-Christophe Filliatre committed Aug 03, 2011 547 `````` function map (l: list a) : list b = `````` Jean-Christophe Filliâtre committed Mar 23, 2010 548 `````` match l with `````` Andrei Paskevich committed Jun 17, 2010 549 `````` | Nil -> Nil `````` Andrei Paskevich committed Jun 21, 2010 550 `````` | Cons x r -> Cons (f x) (map r) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 551 `````` end `````` Jean-Christophe Filliatre committed Aug 03, 2011 552 553 ``````end `````` MARCHE Claude committed Apr 20, 2012 554 555 ``````(** {2 Generic recursors on lists} *) `````` Jean-Christophe Filliatre committed Aug 03, 2011 556 ``````theory FoldLeft `````` 557 `````` `````` Jean-Christophe Filliatre committed Aug 03, 2011 558 559 560 561 562 `````` use import List type a type b function f b a : b `````` Jean-Christophe Filliâtre committed Mar 23, 2010 563 `````` `````` Jean-Christophe Filliatre committed Aug 03, 2011 564 565 566 567 568 `````` function fold_left (acc: b) (l: list a) : b = match l with | Nil -> acc | Cons x r -> fold_left (f acc x) r end `````` 569 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 570 571 ``````end `````` Jean-Christophe Filliatre committed Aug 03, 2011 572 ``````theory FoldRight `````` 573 `````` `````` Jean-Christophe Filliatre committed Aug 03, 2011 574 575 576 577 578 579 580 581 582 583 584 `````` 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 `````` 585 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 586 ``````end `````` Jean-Christophe Filliatre committed Feb 17, 2011 587 `````` `````` MARCHE Claude committed Apr 20, 2012 588 589 ``````(** {2 Importation of all list theories in one} *) `````` Jean-Christophe Filliatre committed Feb 17, 2011 590 ``````theory ListRich `````` 591 `````` `````` Jean-Christophe Filliatre committed Feb 17, 2011 592 593 594 595 596 597 598 599 `````` use export List use export Length use export Mem use export Nth use export HdTl use export NthHdTl use export Append use export Reverse `````` Jean-Christophe Filliatre committed Feb 18, 2014 600 `````` use export RevAppend `````` Jean-Christophe Filliatre committed Feb 17, 2011 601 602 `````` use export NumOcc use export Permut `````` 603 `````` `````` Jean-Christophe Filliatre committed Feb 17, 2011 604 ``end``