stdlib/list.mlw

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