list.why 7.96 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
34
theory Mem
  use export 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
  use export List
65
  use export 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
77
78
79
80
81
theory NthLength

  use export Nth
  use export Length
  use import int.Int

  lemma nth_none_1:
82
     forall l: list 'a, i: int. i < 0 -> nth i l = None
83
84

  lemma nth_none_2:
85
     forall l: list 'a, i: int. i >= length l -> nth i l = None
86
87
88
89
90
91

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

end

92
93
(** {2 Head and tail} *)

94
theory HdTl
95
96
97
98

  use export List
  use export option.Option

Andrei Paskevich's avatar
Andrei Paskevich committed
99
  function hd (l: list 'a) : option 'a = match l with
100
    | Nil      -> None
101
102
103
    | Cons h _ -> Some h
  end

Andrei Paskevich's avatar
Andrei Paskevich committed
104
  function tl (l: list 'a) : option (list 'a) = match l with
105
    | Nil      -> None
106
107
108
    | Cons _ t -> Some t
  end

109
110
end

111
(** {2 Relation between head, tail, and nth} *)
112

113
114
theory NthHdTl

115
  use import int.Int
116
117
  use import Nth
  use import HdTl
118

119
120
121
  lemma Nth_tl:
    forall l1 l2: list 'a. tl l1 = Some l2 ->
    forall i: int. nth i l2 = nth (i+1) l1
122
123

  lemma Nth0_head:
124
    forall l: list 'a. nth 0 l = hd l
125
126
127

end

128
(** {2 Appending two lists} *)
129

130
131
132
theory Append
  use export List

Andrei Paskevich's avatar
Andrei Paskevich committed
133
  function (++) (l1 l2: list 'a) : list 'a = match l1 with
134
    | Nil -> l2
135
    | Cons x1 r1 -> Cons x1 (r1 ++ l2)
136
137
  end

138
139
  lemma Append_assoc:
    forall l1 l2 l3: list 'a.
140
    l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
141

142
143
  lemma Append_l_nil:
    forall l: list 'a. l ++ Nil = l
144
145
146
147

  use import Length
  use import int.Int

148
149
  lemma Append_length:
    forall l1 l2: list 'a. length (l1 ++ l2) = length l1 + length l2
150

151
152
  use import Mem

153
154
  lemma mem_append:
    forall x: 'a, l1 l2: list 'a.
Andrei Paskevich's avatar
Andrei Paskevich committed
155
    mem x (l1 ++ l2) <-> mem x l1 \/ mem x l2
156

157
158
159
160
  lemma mem_decomp:
    forall x: 'a, l: list 'a.
    mem x l -> exists l1 l2: list 'a. l = l1 ++ Cons x l2

161
162
end

163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
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

179
(** {2 Reversing a list} *)
180

181
182
183
184
185
theory Reverse

  use export List
  use import Append

Andrei Paskevich's avatar
Andrei Paskevich committed
186
  function reverse (l: list 'a) : list 'a = match l with
187
    | Nil      -> Nil
188
    | Cons x r -> reverse r ++ Cons x Nil
189
190
  end

191
192
193
194
195
196
  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
197

198
  use import Length
MARCHE Claude's avatar
MARCHE Claude committed
199

200
201
  lemma Reverse_length:
    forall l: list 'a. length (reverse l) = length l
202
203
204

end

205
206
(** {2 Sorted lists for some order as parameter} *)

207
208
209
theory Sorted

  use export List
MARCHE Claude's avatar
MARCHE Claude committed
210

211
212
213
214
  type t
  predicate le t t

  inductive sorted (l: list t) =
215
    | Sorted_Nil:
216
        sorted Nil
217
    | Sorted_One:
218
        forall x: t. sorted (Cons x Nil)
219
    | Sorted_Two:
220
221
        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
222

223
224
  use import Mem

225
226
227
228
229
230
  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

231
232
(** {2 Sorted lists of integers} *)

233
234
235
236
theory SortedInt

  use import int.Int
  clone export Sorted with type t = int, predicate le = (<=)
237
238
239

end

240
241
(** {2 Number of occurrences in a list} *)

242
theory NumOcc
MARCHE Claude's avatar
MARCHE Claude committed
243

244
245
246
  use import int.Int
  use import List

247
  (* number of occurrence of x in l *)
Andrei Paskevich's avatar
Andrei Paskevich committed
248
  function num_occ (x: 'a) (l: list 'a) : int =
249
    match l with
250
    | Nil      -> 0
251
252
253
254
255
    | Cons y r -> (if x = y then 1 else 0) + num_occ x r
   end

  use import Mem

MARCHE Claude's avatar
MARCHE Claude committed
256
  lemma Mem_Num_Occ :
257
    forall x: 'a, l: list 'a. mem x l <-> num_occ x l > 0
258

259
260
261
262
263
264
  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

265
266
end

267
268
(** {2 Permutation of lists} *)

269
theory Permut
270
271
272
273

  use import NumOcc
  use import List

Andrei Paskevich's avatar
Andrei Paskevich committed
274
  predicate permut (l1: list 'a) (l2: list 'a) =
275
    forall x: 'a. num_occ x l1 = num_occ x l2
276

277
  lemma Permut_refl: forall l: list 'a. permut l l
278

279
  lemma Permut_sym: forall l1 l2: list 'a. permut l1 l2 -> permut l2 l1
280

281
282
  lemma Permut_trans:
    forall l1 l2 l3: list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3
283

284
285
  lemma Permut_cons:
    forall x: 'a, l1 l2: list 'a.
286
287
    permut l1 l2 -> permut (Cons x l1) (Cons x l2)

288
289
  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
290

291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
  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)

309
310
  use import Mem

311
312
  lemma Permut_mem:
    forall x: 'a, l1 l2: list 'a. permut l1 l2 -> mem x l1 -> mem x l2
313
314
315

  use import Length

316
317
  lemma Permut_length:
    forall l1 l2: list 'a. permut l1 l2 -> length l1 = length l2
318

319
320
end

321
322
(** {2 List with pairwise distinct elements} *)

Jean-Christophe's avatar
Jean-Christophe committed
323
324
325
326
327
theory Distinct

  use import List
  use import Mem

328
329
330
331
332
  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
333
334
335
336
        not (mem x l) -> distinct l -> distinct (Cons x l)

  use import Append

337
338
  lemma distinct_append:
    forall l1 l2: list 'a.
Jean-Christophe's avatar
Jean-Christophe committed
339
340
341
342
343
    distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) ->
    distinct (l1 ++ l2)

end

344
345
346
347
348
349
350
351
352
353
354
355
356
357
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

358
359
(** {2 Induction on lists} *)

360
theory Induction
361

362
363
  use import List

364
365
  type elt

Andrei Paskevich's avatar
Andrei Paskevich committed
366
  predicate p (list elt)
367

368
369
  axiom Induction:
    p (Nil: list elt) ->
370
371
    (forall x:elt. forall l:list elt. p l -> p (Cons x l)) ->
    forall l:list elt. p l
372
373
374

end

MARCHE Claude's avatar
MARCHE Claude committed
375

376
377
(** {2 Maps as lists of pairs} *)

378
theory Map
379

380
  use import List
MARCHE Claude's avatar
MARCHE Claude committed
381

382
  type a
MARCHE Claude's avatar
MARCHE Claude committed
383
  type b
Andrei Paskevich's avatar
Andrei Paskevich committed
384
  function f a : b
385

386
  function map (l: list a) : list b =
387
    match l with
388
    | Nil      -> Nil
389
    | Cons x r -> Cons (f x) (map r)
390
    end
391
392
end

393
394
(** {2 Generic recursors on lists} *)

395
theory FoldLeft
396

397
398
399
400
401
  use import List

  type a
  type b
  function f b a : b
402

403
404
405
406
407
  function fold_left (acc: b) (l: list a) : b =
    match l with
    | Nil      -> acc
    | Cons x r -> fold_left (f acc x) r
    end
408

409
410
end

411
theory FoldRight
412

413
414
415
416
417
418
419
420
421
422
423
  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
424

425
end
426

427
428
(** {2 Importation of all list theories in one} *)

429
theory ListRich
430

431
432
433
434
435
436
437
438
439
440
441
  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
442

443
end