list.mlw 11.9 KB
Newer Older
1

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

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

6
module List
7

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

10 11 12 13 14
  let predicate is_nil (l:list 'a)
    ensures { result <-> l = Nil }
  =
    match l with Nil -> true | Cons _ _ -> false end

15 16
end

17 18
(** {2 Length of a list} *)

19
module Length
20

21 22
  use int.Int
  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 29
    end

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 35
end

36 37 38 39
(** {2 Quantifiers on lists} *)

module Quant

40
  use List
41 42 43 44 45 46 47 48 49

  let rec function for_all (p: 'a -> bool) (l:list 'a) : bool =
    match l with
    | Nil -> true
    | Cons x r -> p x && for_all p r
    end

  let rec function for_some (p: 'a -> bool) (l:list 'a) : bool =
    match l with
50
    | Nil -> false
51 52 53
    | Cons x r -> p x || for_some p r
    end

54 55 56
  let function mem (eq:'a -> 'a -> bool) (x:'a) (l:list 'a) : bool =
    for_some (eq x) l

57 58
end

59 60
(** {2 Membership in a list} *)

61
module Mem
62
  use List
MARCHE Claude's avatar
MARCHE Claude committed
63

64
  predicate mem (x: 'a) (l: list 'a) = match l with
65
    | Nil      -> false
66
    | Cons y r -> x = y \/ mem x r
67 68 69 70
    end

end

71
module Elements
MARCHE Claude's avatar
MARCHE Claude committed
72

73
  use set.Fset
74 75
  use List
  use Mem
MARCHE Claude's avatar
MARCHE Claude committed
76

77
  function elements (l: list 'a) : fset 'a =
78
    match l with
79 80
    | Nil -> empty
    | Cons x r -> add x (elements r)
81
    end
MARCHE Claude's avatar
MARCHE Claude committed
82

83
  lemma elements_mem:
84
    forall x: 'a, l: list 'a. mem x l <-> Fset.mem x (elements l)
85

MARCHE Claude's avatar
MARCHE Claude committed
86 87
end

88 89
(** {2 Nth element of a list} *)

90
module Nth
91

92 93 94
  use List
  use option.Option
  use int.Int
MARCHE Claude's avatar
MARCHE Claude committed
95

96
  let rec function nth (n: int) (l: list 'a) : option 'a =
97
    match l with
98
    | Nil      -> None
99
    | Cons x r -> if n = 0 then Some x else nth (n - 1) r
100
    end
101 102 103

end

104
module NthNoOpt
105

106 107
  use List
  use int.Int
108

109
  function nth (n: int) (l: list 'a) : 'a
110 111 112 113 114 115 116

  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

117
module NthLength
118

119 120 121
  use int.Int
  use option.Option
  use List
122 123 124 125
  use export Nth
  use export Length

  lemma nth_none_1:
126
     forall l: list 'a, i: int. i < 0 -> nth i l = None
127 128

  lemma nth_none_2:
129
     forall l: list 'a, i: int. i >= length l -> nth i l = None
130 131 132 133 134 135

  lemma nth_none_3:
     forall l: list 'a, i: int. nth i l = None -> i < 0 \/ i >= length l

end

136 137
(** {2 Head and tail} *)

138
module HdTl
139

140 141
  use List
  use option.Option
142

143
  let function hd (l: list 'a) : option 'a = match l with
144
    | Nil      -> None
145 146 147
    | Cons h _ -> Some h
  end

148
  let function tl (l: list 'a) : option (list 'a) = match l with
149
    | Nil      -> None
150 151 152
    | Cons _ t -> Some t
  end

153 154
end

155
module HdTlNoOpt
156

157
  use List
158 159 160 161 162 163 164 165 166 167 168

  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

169
(** {2 Relation between head, tail, and nth} *)
170

171
module NthHdTl
172

173 174 175 176 177
  use int.Int
  use option.Option
  use List
  use Nth
  use HdTl
178

179 180
  lemma Nth_tl:
    forall l1 l2: list 'a. tl l1 = Some l2 ->
181
    forall i: int. i <> -1 -> nth i l2 = nth (i+1) l1
182 183

  lemma Nth0_head:
184
    forall l: list 'a. nth 0 l = hd l
185 186 187

end

188
(** {2 Appending two lists} *)
189

190
module Append
191

192
  use List
193

194
  let rec function (++) (l1 l2: list 'a) : list 'a =
195
    match l1 with
196
    | Nil -> l2
197
    | Cons x1 r1 -> Cons x1 (r1 ++ l2)
198
    end
199

200
  lemma Append_assoc:
201
    forall l1 [@induction] l2 l3: list 'a.
202
    l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
203

204 205
  lemma Append_l_nil:
    forall l: list 'a. l ++ Nil = l
206

207 208
  use Length
  use int.Int
209

210
  lemma Append_length:
211
    forall l1 [@induction] l2: list 'a. length (l1 ++ l2) = length l1 + length l2
212

213
  use Mem
214

215
  lemma mem_append:
216
    forall x: 'a, l1 [@induction] l2: list 'a.
217
    mem x (l1 ++ l2) <-> mem x l1 \/ mem x l2
218

219 220 221 222
  lemma mem_decomp:
    forall x: 'a, l: list 'a.
    mem x l -> exists l1 l2: list 'a. l = l1 ++ Cons x l2

223 224
end

225
module NthLengthAppend
226

227 228
  use int.Int
  use List
229 230 231 232 233 234 235 236
  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:
237
    forall l1 [@induction] l2: list 'a, i: int.
238 239 240 241
    length l1 <= i -> nth i (l1 ++ l2) = nth (i - length l1) l2

end

242 243
(** {2 Reversing a list} *)

244
module Reverse
245

246 247
  use List
  use Append
248

249
  let rec function reverse (l: list 'a) : list 'a =
250
    match l with
251 252
    | Nil      -> Nil
    | Cons x r -> reverse r ++ Cons x Nil
253
    end
254 255 256 257 258

  lemma reverse_append:
    forall l1 l2: list 'a, x: 'a.
    (reverse (Cons x l1)) ++ l2 = (reverse l1) ++ (Cons x l2)

259 260 261 262
  lemma reverse_cons:
    forall l: list 'a, x: 'a.
    reverse (Cons x l) = reverse l ++ Cons x Nil

263 264 265 266 267

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

268 269 270
  lemma reverse_reverse:
    forall l: list 'a. reverse (reverse l) = l

271
  use Mem
272 273 274 275

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

276
  use Length
277 278 279 280 281 282

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

end

283 284
(** {2 Reverse append} *)

285
module RevAppend
286

287
  use List
288

289
  let rec function rev_append (s t: list 'a) : list 'a =
290 291 292 293 294
    match s with
    | Cons x r -> rev_append r (Cons x t)
    | Nil -> t
    end

295
  use Append
296 297

  lemma rev_append_append_l:
298
    forall r [@induction] s t: list 'a.
299 300
      rev_append (r ++ s) t = rev_append s (rev_append r t)

301 302
  use int.Int
  use Length
303 304

  lemma rev_append_length:
305
    forall s [@induction] t: list 'a.
306 307
      length (rev_append s t) = length s + length t

308
  use Reverse
309 310

  lemma rev_append_def:
311
    forall r [@induction] s: list 'a. rev_append r s = reverse r ++ s
312 313 314 315

  lemma rev_append_append_r:
    forall r s t: list 'a.
      rev_append r (s ++ t) = rev_append (rev_append s r) t
316

317 318
end

319 320
(** {2 Zip} *)

321
module Combine
322

323
  use List
324

325 326
  let rec function combine (x: list 'a) (y: list 'b) : list ('a, 'b)
  = match x, y with
327 328 329 330 331 332
    | Cons x0 x, Cons y0 y -> Cons (x0, y0) (combine x y)
    | _ -> Nil
    end

end

333 334
(** {2 Sorted lists for some order as parameter} *)

335
module Sorted
336

337
  use List
MARCHE Claude's avatar
MARCHE Claude committed
338

339 340
  type t
  predicate le t t
341
  clone relations.Transitive with
342
    type t = t, predicate rel = le, axiom Trans
343 344

  inductive sorted (l: list t) =
345
    | Sorted_Nil:
346
        sorted Nil
347
    | Sorted_One:
348
        forall x: t. sorted (Cons x Nil)
349
    | Sorted_Two:
350 351
        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
352

353
  use Mem
354

355 356 357 358
  lemma sorted_mem:
    forall x: t, l: list t.
    (forall y: t. mem y l -> le x y) /\ sorted l <-> sorted (Cons x l)

359
  use Append
360 361

  lemma sorted_append:
362
    forall  l1 [@induction] l2: list t.
363 364
    (sorted l1 /\ sorted l2 /\ (forall x y: t. mem x l1 -> mem y l2 -> le x y))
    <->
365 366
    sorted (l1 ++ l2)

367 368
end

369 370
(** {2 Sorted lists of integers} *)

371
module SortedInt
372

373
  use int.Int
374
  clone export Sorted with type t = int, predicate le = (<=), goal Transitive.Trans
375 376 377

end

378
module RevSorted
379 380 381

  type t
  predicate le t t
382
  clone relations.Transitive with
383
    type t = t, predicate rel = le, axiom Trans
384 385
  predicate ge (x y: t) = le y x

386
  use List
387

388 389
  clone Sorted as Incr with type t = t, predicate le = le, goal .
  clone Sorted as Decr with type t = t, predicate le = ge, goal .
390 391 392 393 394 395 396

  predicate compat (s t: list t) =
    match s, t with
    | Cons x _, Cons y _ -> le x y
    | _, _ -> true
    end

397
  use RevAppend
398 399

  lemma rev_append_sorted_incr:
400
    forall s [@induction] t: list t.
401 402 403 404
      Incr.sorted (rev_append s t) <->
        Decr.sorted s /\ Incr.sorted t /\ compat s t

  lemma rev_append_sorted_decr:
405
    forall s [@induction] t: list t.
406 407 408 409 410
      Decr.sorted (rev_append s t) <->
        Incr.sorted s /\ Decr.sorted t /\ compat t s

end

411 412
(** {2 Number of occurrences in a list} *)

413
module NumOcc
MARCHE Claude's avatar
MARCHE Claude committed
414

415 416
  use int.Int
  use List
417

418
  function num_occ (x: 'a) (l: list 'a) : int =
419
    match l with
420
    | Nil      -> 0
421
    | Cons y r -> (if x = y then 1 else 0) + num_occ x r
422
    end
423
  (** number of occurrences of `x` in `l` *)
424

425
  lemma Num_Occ_NonNeg: forall x:'a, l: list 'a. num_occ x l >= 0
426

427
  use Mem
428

MARCHE Claude's avatar
MARCHE Claude committed
429
  lemma Mem_Num_Occ :
430
    forall x: 'a, l: list 'a. mem x l <-> num_occ x l > 0
431

432
  use Append
433 434

  lemma Append_Num_Occ :
435
    forall x: 'a, l1 [@induction] l2: list 'a.
436 437
    num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2

438
  use Reverse
439 440 441 442 443

  lemma reverse_num_occ :
    forall x: 'a, l: list 'a.
    num_occ x l = num_occ x (reverse l)

444 445
end

446 447
(** {2 Permutation of lists} *)

448
module Permut
449

450 451
  use NumOcc
  use List
452

453
  predicate permut (l1: list 'a) (l2: list 'a) =
454
    forall x: 'a. num_occ x l1 = num_occ x l2
455

456
  lemma Permut_refl: forall l: list 'a. permut l l
457

458
  lemma Permut_sym: forall l1 l2: list 'a. permut l1 l2 -> permut l2 l1
459

460 461
  lemma Permut_trans:
    forall l1 l2 l3: list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3
462

463 464
  lemma Permut_cons:
    forall x: 'a, l1 l2: list 'a.
465 466
    permut l1 l2 -> permut (Cons x l1) (Cons x l2)

467 468
  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
469

470
  use Append
471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487

  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)

488
  use Mem
489

490 491
  lemma Permut_mem:
    forall x: 'a, l1 l2: list 'a. permut l1 l2 -> mem x l1 -> mem x l2
492

493
  use Length
494

495
  lemma Permut_length:
496
    forall l1 [@induction] l2: list 'a. permut l1 l2 -> length l1 = length l2
497

498 499
end

500 501
(** {2 List with pairwise distinct elements} *)

502
module Distinct
503

504 505
  use List
  use Mem
506

507 508 509 510 511
  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.
512 513
        not (mem x l) -> distinct l -> distinct (Cons x l)

514
  use Append
515

516
  lemma distinct_append:
517
    forall l1 [@induction] l2: list 'a.
518 519 520 521 522
    distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) ->
    distinct (l1 ++ l2)

end

523
module Prefix
524

525 526
  use List
  use int.Int
527

528
  let rec function prefix (n: int) (l: list 'a) : list 'a =
529 530 531 532 533 534 535 536
    if n <= 0 then Nil else
    match l with
    | Nil -> Nil
    | Cons x r -> Cons x (prefix (n-1) r)
    end

end

537
module Sum
538

539 540
  use List
  use int.Int
541

542
  let rec function sum (l: list int) : int =
543 544 545 546
    match l with
    | Nil -> 0
    | Cons x r -> x + sum r
    end
547 548 549

end

550
(*
551 552
(** {2 Induction on lists} *)

553
module Induction
554

555
  use List
556

557
  (* type elt *)
558

559
  (* predicate p (list elt) *)
560

561
  axiom Induction:
562 563 564 565
    forall p: list 'a -> bool.
    p (Nil: list 'a) ->
    (forall x:'a. forall l:list 'a. p l -> p (Cons x l)) ->
    forall l:list 'a. p l
566 567

end
568
*)
MARCHE Claude's avatar
MARCHE Claude committed
569

570 571
(** {2 Maps as lists of pairs} *)

572
module Map
573

574
  use List
MARCHE Claude's avatar
MARCHE Claude committed
575

576
  function map (f: 'a -> 'b) (l: list 'a) : list 'b =
577
    match l with
578
    | Nil      -> Nil
579
    | Cons x r -> Cons (f x) (map f r)
580
    end
581 582
end

583 584
(** {2 Generic recursors on lists} *)

585
module FoldLeft
586

587
  use List
588

589
  function fold_left (f: 'b -> 'a -> 'b) (acc: 'b) (l: list 'a) : 'b =
590 591
    match l with
    | Nil      -> acc
592
    | Cons x r -> fold_left f (f acc x) r
593
    end
594

595
  use Append
596 597

  lemma fold_left_append:
598
    forall l1 [@induction] l2: list 'a, f: 'b -> 'a -> 'b, acc : 'b.
599 600
    fold_left f acc (l1++l2) = fold_left f (fold_left f acc l1) l2

601 602
end

603
module FoldRight
604

605
  use List
606

607
  function fold_right (f: 'a -> 'b -> 'b) (l: list 'a) (acc: 'b) : 'b =
608 609
    match l with
    | Nil      -> acc
610
    | Cons x r -> f x (fold_right f r acc)
611
    end
612

613
  use Append
614 615

  lemma fold_right_append:
616
    forall l1 [@induction] l2: list 'a, f: 'a -> 'b -> 'b, acc : 'b.
617 618
    fold_right f (l1++l2) acc = fold_right f l1 (fold_right f l2 acc)

619
end
620

621 622
(** {2 Importation of all list theories in one} *)

623
module ListRich
624

625 626 627 628 629 630 631 632
  use export List
  use export Length
  use export Mem
  use export Nth
  use export HdTl
  use export NthHdTl
  use export Append
  use export Reverse
633
  use export RevAppend
634 635
  use export NumOcc
  use export Permut
636

637
end