list.why 11.3 KB
Newer Older
1

2 3 4 5
(** {1 Polymorphic Lists} *)

(** {2 Basic theory of polymorphic lists} *)

6 7
theory List

8
  type list 'a = Nil | Cons 'a (list 'a)
9 10 11

end

12 13
(** {2 Length of a list} *)

14
theory Length
15

16 17 18
  use import int.Int
  use import List

Andrei Paskevich's avatar
Andrei Paskevich committed
19
  function length (l: list 'a) : int =
20
    match l with
21
    | Nil      -> 0
22
    | Cons _ r -> 1 + length r
23 24
    end

25
  lemma Length_nonnegative: forall l: list 'a. length l >= 0
26

27
  lemma Length_nil: forall l: list 'a. length l = 0 <-> l = Nil
28

29 30
end

31 32
(** {2 Membership in a list} *)

33
theory Mem
34
  use import List
MARCHE Claude's avatar
MARCHE Claude committed
35

Andrei Paskevich's avatar
Andrei Paskevich committed
36
  predicate mem (x: 'a) (l: list 'a) = match l with
37
    | Nil      -> false
Andrei Paskevich's avatar
Andrei Paskevich committed
38
    | Cons y r -> x = y \/ mem x r
39 40 41 42
    end

end

MARCHE Claude's avatar
MARCHE Claude committed
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)

55 56 57
  lemma elements_Nil:
    elements (Nil : list 'a) = FSet.empty

MARCHE Claude's avatar
MARCHE Claude committed
58 59
end

60 61
(** {2 Nth element of a list} *)

62
theory Nth
63

64 65
  use import List
  use import option.Option
66
  use import int.Int
MARCHE Claude's avatar
MARCHE Claude committed
67

Andrei Paskevich's avatar
Andrei Paskevich committed
68
  function nth (n: int) (l: list 'a) : option 'a = match l with
69
    | Nil      -> None
70
    | Cons x r -> if n = 0 then Some x else nth (n - 1) r
71 72 73 74
  end

end

75 76
theory NthNoOpt

77
  use import List
78 79
  use import int.Int

80
  function nth (n: int) (l: list 'a) : 'a
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

88 89
theory NthLength

90 91 92
  use import int.Int
  use import option.Option
  use import List
93 94 95 96
  use export Nth
  use export Length

  lemma nth_none_1:
97
     forall l: list 'a, i: int. i < 0 -> nth i l = None
98 99

  lemma nth_none_2:
100
     forall l: list 'a, i: int. i >= length l -> nth i l = None
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

107 108
(** {2 Head and tail} *)

109
theory HdTl
110

111 112
  use import List
  use import option.Option
113

Andrei Paskevich's avatar
Andrei Paskevich committed
114
  function hd (l: list 'a) : option 'a = match l with
115
    | Nil      -> None
116 117 118
    | Cons h _ -> Some h
  end

Andrei Paskevich's avatar
Andrei Paskevich committed
119
  function tl (l: list 'a) : option (list 'a) = match l with
120
    | Nil      -> None
121 122 123
    | Cons _ t -> Some t
  end

124 125
end

126 127
theory HdTlNoOpt

128
  use import List
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} *)
141

142 143
theory NthHdTl

144
  use import int.Int
145 146
  use import option.Option
  use import List
147 148
  use import Nth
  use import HdTl
149

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
153 154

  lemma Nth0_head:
155
    forall l: list 'a. nth 0 l = hd l
156 157 158

end

159
(** {2 Appending two lists} *)
160

161
theory Append
162 163

  use import List
164

Andrei Paskevich's avatar
Andrei Paskevich committed
165
  function (++) (l1 l2: list 'a) : list 'a = match l1 with
166
    | Nil -> l2
167
    | Cons x1 r1 -> Cons x1 (r1 ++ l2)
168 169
  end

170
  lemma Append_assoc:
171
    forall l1 "induction" l2 l3: list 'a.
172
    l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
173

174 175
  lemma Append_l_nil:
    forall l: list 'a. l ++ Nil = l
176 177 178 179

  use import Length
  use import int.Int

180
  lemma Append_length:
181
    forall l1 "induction" l2: list 'a. length (l1 ++ l2) = length l1 + length l2
182

183 184
  use import Mem

185
  lemma mem_append:
186
    forall x: 'a, l1 "induction" l2: list 'a.
Andrei Paskevich's avatar
Andrei Paskevich committed
187
    mem x (l1 ++ l2) <-> mem x l1 \/ mem x l2
188

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

193 194
end

195 196
theory NthLengthAppend

197 198
  use import int.Int
  use import List
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:
207
    forall l1 "induction" l2: list 'a, i: int.
208 209 210 211
    length l1 <= i -> nth i (l1 ++ l2) = nth (i - length l1) l2

end

212 213 214 215
(** {2 Reversing a list} *)

theory Reverse

216
  use import List
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)

228 229 230 231
  lemma reverse_cons:
    forall l: list 'a, x: 'a.
    reverse (Cons x l) = reverse l ++ Cons x Nil

232 233 234 235 236

  lemma cons_reverse:
    forall l: list 'a, x: 'a.
    Cons x (reverse l) = reverse (l ++ Cons x Nil)

237 238 239
  lemma reverse_reverse:
    forall l: list 'a. reverse (reverse l) = l

240 241 242 243 244
  use import Mem

  lemma reverse_mem:
    forall l: list 'a, x: 'a. mem x l <-> mem x (reverse l)

245 246 247 248 249 250 251
  use import Length

  lemma Reverse_length:
    forall l: list 'a. length (reverse l) = length l

end

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:
267
    forall r "induction" s t: list 'a.
268 269
      rev_append (r ++ s) t = rev_append s (rev_append r t)

270

271 272 273 274 275

  use import int.Int
  use import Length

  lemma rev_append_length:
276
    forall s "induction" t: list 'a.
277 278
      length (rev_append s t) = length s + length t

279 280 281
  use import Reverse

  lemma rev_append_def:
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
288

289 290
end

291 292 293 294
(** {2 Zip} *)

theory Combine

295
  use import List
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

305 306
(** {2 Sorted lists for some order as parameter} *)

307 308
theory Sorted

309
  use import List
MARCHE Claude's avatar
MARCHE Claude committed
310

311 312
  type t
  predicate le t t
313
  clone relations.Transitive with type t = t, predicate rel = le
314 315

  inductive sorted (l: list t) =
316
    | Sorted_Nil:
317
        sorted Nil
318
    | Sorted_One:
319
        forall x: t. sorted (Cons x Nil)
320
    | Sorted_Two:
321 322
        forall x y: t, l: list t.
        le x y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
MARCHE Claude's avatar
MARCHE Claude committed
323

324 325
  use import Mem

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)

330 331 332
  use import Append

  lemma sorted_append:
333
    forall  l1 "induction" l2: list t.
334 335
    (sorted l1 /\ sorted l2 /\ (forall x y: t. mem x l1 -> mem y l2 -> le x y))
    <->
336 337
    sorted (l1 ++ l2)

338 339
end

340 341
(** {2 Sorted lists of integers} *)

342 343 344
theory SortedInt

  use import int.Int
345
  clone export Sorted with type t = int, predicate le = (<=), goal Transitive.Trans
346 347 348

end

349 350 351 352
theory RevSorted

  type t
  predicate le t t
353
  clone import relations.Transitive with type t = t, predicate rel = le
354 355 356 357
  predicate ge (x y: t) = le y x

  use import List

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
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:
370
    forall s "induction" t: list t.
371 372 373 374
      Incr.sorted (rev_append s t) <->
        Decr.sorted s /\ Incr.sorted t /\ compat s t

  lemma rev_append_sorted_decr:
375
    forall s "induction" t: list t.
376 377 378 379 380
      Decr.sorted (rev_append s t) <->
        Incr.sorted s /\ Decr.sorted t /\ compat t s

end

381 382
(** {2 Number of occurrences in a list} *)

383
theory NumOcc
MARCHE Claude's avatar
MARCHE Claude committed
384

385 386 387
  use import int.Int
  use import List

Andrei Paskevich's avatar
Andrei Paskevich committed
388
  function num_occ (x: 'a) (l: list 'a) : int =
389
    match l with
390
    | Nil      -> 0
391
    | Cons y r -> (if x = y then 1 else 0) + num_occ x r
392 393
    end
  (** number of occurrences of [x] in [l] *)
394

MARCHE Claude's avatar
MARCHE Claude committed
395
  lemma Num_Occ_NonNeg: forall x:'a, l: list 'a. num_occ x l >= 0
396

397 398
  use import Mem

MARCHE Claude's avatar
MARCHE Claude committed
399
  lemma Mem_Num_Occ :
400
    forall x: 'a, l: list 'a. mem x l <-> num_occ x l > 0
401

402 403 404
  use import Append

  lemma Append_Num_Occ :
405
    forall x: 'a, l1 "induction" l2: list 'a.
406 407
    num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2

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)

414 415
end

416 417
(** {2 Permutation of lists} *)

418
theory Permut
419 420 421 422

  use import NumOcc
  use import List

Andrei Paskevich's avatar
Andrei Paskevich committed
423
  predicate permut (l1: list 'a) (l2: list 'a) =
424
    forall x: 'a. num_occ x l1 = num_occ x l2
425

426
  lemma Permut_refl: forall l: list 'a. permut l l
427

428
  lemma Permut_sym: forall l1 l2: list 'a. permut l1 l2 -> permut l2 l1
429

430 431
  lemma Permut_trans:
    forall l1 l2 l3: list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3
432

433 434
  lemma Permut_cons:
    forall x: 'a, l1 l2: list 'a.
435 436
    permut l1 l2 -> permut (Cons x l1) (Cons x l2)

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's avatar
MARCHE Claude committed
439

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)

458 459
  use import Mem

460 461
  lemma Permut_mem:
    forall x: 'a, l1 l2: list 'a. permut l1 l2 -> mem x l1 -> mem x l2
462 463 464

  use import Length

465 466
  lemma Permut_length:
    forall l1 l2: list 'a. permut l1 l2 -> length l1 = length l2
467

468 469
end

470 471
(** {2 List with pairwise distinct elements} *)

Jean-Christophe's avatar
Jean-Christophe committed
472 473 474 475 476
theory Distinct

  use import List
  use import Mem

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's avatar
Jean-Christophe committed
482 483 484 485
        not (mem x l) -> distinct l -> distinct (Cons x l)

  use import Append

486
  lemma distinct_append:
487
    forall l1 "induction" l2: list 'a.
Jean-Christophe's avatar
Jean-Christophe committed
488 489 490 491 492
    distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) ->
    distinct (l1 ++ l2)

end

493 494
theory Prefix

495
  use import List
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

507 508
theory Sum

509
  use import List
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

519 520
(** {2 Induction on lists} *)

521
theory Induction
522

523 524
  use import List

525 526
  type elt

Andrei Paskevich's avatar
Andrei Paskevich committed
527
  predicate p (list elt)
528

529 530
  axiom Induction:
    p (Nil: list elt) ->
531 532
    (forall x:elt. forall l:list elt. p l -> p (Cons x l)) ->
    forall l:list elt. p l
533 534 535

end

MARCHE Claude's avatar
MARCHE Claude committed
536

537 538
(** {2 Maps as lists of pairs} *)

539
theory Map
540

541
  use import List
MARCHE Claude's avatar
MARCHE Claude committed
542

543
  type a
MARCHE Claude's avatar
MARCHE Claude committed
544
  type b
Andrei Paskevich's avatar
Andrei Paskevich committed
545
  function f a : b
546

547
  function map (l: list a) : list b =
548
    match l with
549
    | Nil      -> Nil
550
    | Cons x r -> Cons (f x) (map r)
551
    end
552 553
end

554 555
(** {2 Generic recursors on lists} *)

556
theory FoldLeft
557

558 559 560 561 562
  use import List

  type a
  type b
  function f b a : b
563

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

570 571
end

572
theory FoldRight
573

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

586
end
587

588 589
(** {2 Importation of all list theories in one} *)

590
theory ListRich
591

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
600
  use export RevAppend
601 602
  use export NumOcc
  use export Permut
603

604
end