list.v 130 KB
Newer Older
1
(* Copyright (c) 2012-2013, Robbert Krebbers. *)
2
3
4
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *)
5
Require Export Permutation.
6
Require Export numbers base decidable option.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8
Arguments length {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
11
Arguments cons {_} _ _.
Arguments app {_} _ _.
Arguments Permutation {_} _ _.
12
Arguments Forall_cons {_} _ _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
13

14
15
16
Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.
17

18
19
20
Arguments take {_} !_ !_ /.
Arguments drop {_} !_ !_ /.

Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24
25
26
27
Notation "(::)" := cons (only parsing) : C_scope.
Notation "( x ::)" := (cons x) (only parsing) : C_scope.
Notation "(:: l )" := (λ x, cons x l) (only parsing) : C_scope.
Notation "(++)" := app (only parsing) : C_scope.
Notation "( l ++)" := (app l) (only parsing) : C_scope.
Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope.

28
29
30
31
32
33
34
35
36
Infix "≡ₚ" := Permutation (at level 70, no associativity) : C_scope.
Notation "(≡ₚ)" := Permutation (only parsing) : C_scope.
Notation "( x ≡ₚ)" := (Permutation x) (only parsing) : C_scope.
Notation "(≡ₚ x )" := (λ y, y  x) (only parsing) : C_scope.
Notation "(≢ₚ)" := (λ x y, ¬x  y) (only parsing) : C_scope.
Notation "x ≢ₚ y":= (¬x  y) (at level 70, no associativity) : C_scope.
Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : C_scope.
Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : C_scope.

37
38
39
(** * Definitions *)
(** The operation [l !! i] gives the [i]th element of the list [l], or [None]
in case [i] is out of bounds. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
40
Instance list_lookup {A} : Lookup nat A (list A) :=
41
  fix go (i : nat) (l : list A) {struct l} : option A :=
42
43
  match l with
  | [] => None
44
  | x :: l => match i with 0 => Some x | S i => @lookup _ _ _ go i l end
45
  end.
46
47
48

(** The operation [alter f i l] applies the function [f] to the [i]th element
of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
49
Instance list_alter {A} (f : A  A) : AlterD nat A (list A) f :=
50
  fix go (i : nat) (l : list A) {struct l} :=
51
52
  match l with
  | [] => []
53
  | x :: l => match i with 0 => f x :: l | S i => x :: @alter _ _ _ f go i l end
54
  end.
55

56
57
58
59
(** The operation [<[i:=x]> l] overwrites the element at position [i] with the
value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
Instance list_insert {A} : Insert nat A (list A) := λ i x, alter (λ _, x) i.

60
61
62
(** The operation [delete i l] removes the [i]th element of [l] and moves
all consecutive elements one position ahead. In case [i] is out of bounds,
the list is returned unchanged. *)
63
64
Instance list_delete {A} : Delete nat (list A) :=
  fix go (i : nat) (l : list A) {struct l} : list A :=
65
66
  match l with
  | [] => []
67
  | x :: l => match i with 0 => l | S i => x :: @delete _ _ go i l end
68
  end.
69
70
71

(** The function [option_list o] converts an element [Some x] into the
singleton list [[x]], and [None] into the empty list [[]]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
72
73
74
75
76
77
78
79
80
Definition option_list {A} : option A  list A := option_rect _ (λ x, [x]) [].

(** The function [filter P l] returns the list of elements of [l] that
satisfies [P]. The order remains unchanged. *)
Instance list_filter {A} : Filter A (list A) :=
  fix go P _ l :=
  match l with
  | [] => []
  | x :: l =>
81
82
83
    if decide (P x)
    then x :: @filter _ _ (@go) _ _ l
    else @filter _ _ (@go) _ _ l
Robbert Krebbers's avatar
Robbert Krebbers committed
84
  end.
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
Fixpoint filter_Some {A} (l : list (option A)) : list A :=
  match l with
  | [] => []
  | Some x :: l => x :: filter_Some l
  | None :: l => filter_Some l
  end.

(** The function [list_find P l] returns the first index [i] whose element
satisfies the predicate [P]. *)
Definition list_find {A} P `{ x, Decision (P x)} : list A  option nat :=
  fix go l :=
  match l with
  | [] => None
  | x :: l => if decide (P x) then Some 0 else S <$> go l
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
102
103

(** The function [replicate n x] generates a list with length [n] of elements
with value [x]. *)
Fixpoint replicate {A} (n : nat) (x : A) : list A :=
104
  match n with 0 => [] | S n => x :: replicate n x end.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
107
108

(** The function [reverse l] returns the elements of [l] in reverse order. *)
Definition reverse {A} (l : list A) : list A := rev_append l [].

109
Fixpoint last' {A} (x : A) (l : list A) : A :=
110
  match l with [] => x | x :: l => last' x l end.
111
Definition last {A} (l : list A) : option A :=
112
  match l with [] => None | x :: l => Some (last' x l) end.
113

Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
116
117
118
119
(** The function [resize n y l] takes the first [n] elements of [l] in case
[length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
a list of length [n]. *)
Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
  match l with
  | [] => replicate n y
120
  | x :: l => match n with 0 => [] | S n => x :: resize n y l end
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
123
  end.
Arguments resize {_} !_ _ !_.

124
125
126
127
128
129
130
131
132
(* The function [reshape k l] transforms [l] into a list of lists whose sizes are
specified by [k]. In case [l] is too short, the resulting list will end with a
a certain number of empty lists. In case [l] is too long, it will be truncated. *)
Fixpoint reshape {A} (szs : list nat) (l : list A) : list (list A) :=
  match szs with
  | [] => []
  | sz :: szs => take sz l :: reshape szs (drop sz l)
  end.

133
134
135
136
137
Definition sublist_lookup {A} (i n : nat) (l : list A) : option (list A) :=
  guard (i + n  length l); Some $ take n $ drop i l.
Definition sublist_insert {A} (i : nat) (k l : list A) : list A :=
  take i l ++ take (length l - i) k ++ drop (i + length k) l.

138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
(** Functions to fold over a list. We redefine [foldl] with the arguments in
the same order as in Haskell. *)
Notation foldr := fold_right.

Definition foldl {A B} (f : A  B  A) : A  list B  A :=
  fix go a l :=
  match l with
  | [] => a
  | x :: l => go (f a x) l
  end.

(** The monadic operations. *)
Instance list_ret: MRet list := λ A x, x :: @nil A.
Instance list_fmap {A B} (f : A  B) : FMapD list f :=
  fix go (l : list A) :=
153
  match l with [] => [] | x :: l => f x :: @fmap _ _ _ f go l end.
154
155
Instance list_bind {A B} (f : A  list B) : MBindD list f :=
  fix go (l : list A) :=
156
  match l with [] => [] | x :: l => f x ++ @mbind _ _ _ f go l end.
157
158
Instance list_join: MJoin list :=
  fix go A (ls : list (list A)) : list A :=
159
  match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
160
161
162
163
164
165
166
Definition mapM `{!MBind M} `{!MRet M} {A B}
    (f : A  M B) : list A  M (list B) :=
  fix go l :=
  match l with
  | [] => mret []
  | x :: l => y  f x; k  go l; mret (y :: k)
  end.
167
168
169
170
171

(** We define stronger variants of map and fold that allow the mapped
function to use the index of the elements. *)
Definition imap_go {A B} (f : nat  A  B) : nat  list A  list B :=
  fix go (n : nat) (l : list A) :=
172
  match l with [] => [] | x :: l => f n x :: go (S n) l end.
173
174
Definition imap {A B} (f : nat  A  B) : list A  list B := imap_go f 0.

175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
Definition ifoldr {A B} (f : nat  B  A  A) (a : nat  A) :
  nat  list B  A := fix go n l :=
  match l with [] => a n | b :: l => f n b (go (S n) l) end.

Definition zipped_map {A B} (f : list A  list A  A  B) :
  list A  list A  list B := fix go l k :=
  match k with [] => [] | x :: k => f l k x :: go (x :: l) k end.

Inductive zipped_Forall {A} (P : list A  list A  A  Prop) :
    list A  list A  Prop :=
  | zipped_Forall_nil l : zipped_Forall P l []
  | zipped_Forall_cons l k x :
     P l k x  zipped_Forall P (x :: l) k  zipped_Forall P l (x :: k).
Arguments zipped_Forall_nil {_ _} _.
Arguments zipped_Forall_cons {_ _} _ _ _ _ _.
190
191
192
193

(** Zipping lists. *)
Definition zip_with {A B C} (f : A  B  C) : list A  list B  list C :=
  fix go l1 l2 :=
194
  match l1, l2 with x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2 | _ , _ => [] end.
195
196
197
198
199
200
201
202
203
204
205
206
207
208
Notation zip := (zip_with pair).

(** The function [permutations l] yields all permutations of [l]. *)
Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
  match l with
  | [] => [ [x] ]
  | y :: l => (x :: y :: l) :: ((y ::) <$> interleave x l)
  end.
Fixpoint permutations {A} (l : list A) : list (list A) :=
  match l with
  | [] => [ [] ]
  | x :: l => permutations l = interleave x
  end.

209
210
(** The predicate [suffix_of] holds if the first list is a suffix of the second.
The predicate [prefix_of] holds if the first list is a prefix of the second. *)
211
212
Definition suffix_of {A} : relation (list A) := λ l1 l2,  k, l2 = k ++ l1.
Definition prefix_of {A} : relation (list A) := λ l1 l2,  k, l2 = l1 ++ k.
213
214
Infix "`suffix_of`" := suffix_of (at level 70) : C_scope.
Infix "`prefix_of`" := prefix_of (at level 70) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
215

216
217
218
219
220
221
222
223
224
Section prefix_suffix_ops.
  Context `{ x y : A, Decision (x = y)}.

  Definition max_prefix_of : list A  list A  list A * list A * list A :=
    fix go l1 l2 :=
    match l1, l2 with
    | [], l2 => ([], l2, [])
    | l1, [] => (l1, [], [])
    | x1 :: l1, x2 :: l2 =>
225
226
227
      if decide_rel (=) x1 x2
      then snd_map (x1 ::) (go l1 l2)
      else (x1 :: l1, x2 :: l2, [])
228
229
230
231
232
233
234
235
236
    end.
  Definition max_suffix_of (l1 l2 : list A) : list A * list A * list A :=
    match max_prefix_of (reverse l1) (reverse l2) with
    | (k1, k2, k3) => (reverse k1, reverse k2, reverse k3)
    end.

  Definition strip_prefix (l1 l2 : list A) := snd $ fst $ max_prefix_of l1 l2.
  Definition strip_suffix (l1 l2 : list A) := snd $ fst $ max_suffix_of l1 l2.
End prefix_suffix_ops.
Robbert Krebbers's avatar
Robbert Krebbers committed
237

238
(** A list [l1] is a sublist of [l2] if [l2] is obtained by removing elements
239
240
241
from [l1] without changing the order. *)
Inductive sublist {A} : relation (list A) :=
  | sublist_nil : sublist [] []
242
  | sublist_skip x l1 l2 : sublist l1 l2  sublist (x :: l1) (x :: l2)
243
  | sublist_cons x l1 l2 : sublist l1 l2  sublist l1 (x :: l2).
244
245
246
247
248
249
250
251
Infix "`sublist`" := sublist (at level 70) : C_scope.

(** A list [l2] contains a list [l1] if [l2] is obtained by removing elements
from [l1] without changing the order. *)
Inductive contains {A} : relation (list A) :=
  | contains_nil : contains [] []
  | contains_skip x l1 l2 : contains l1 l2  contains (x :: l1) (x :: l2)
  | contains_swap x y l : contains (y :: x :: l) (x :: y :: l)
252
  | contains_cons x l1 l2 : contains l1 l2  contains l1 (x :: l2)
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
  | contains_trans l1 l2 l3 : contains l1 l2  contains l2 l3  contains l1 l3.
Infix "`contains`" := contains (at level 70) : C_scope.

Section contains_dec_help.
  Context {A} {dec :  x y : A, Decision (x = y)}.

  Fixpoint list_remove (x : A) (l : list A) : option (list A) :=
    match l with
    | [] => None
    | y :: l => if decide (x = y) then Some l else (y ::) <$> list_remove x l
    end.
  Fixpoint list_remove_list (k : list A) (l : list A) : option (list A) :=
    match k with
    | [] => Some l
    | x :: k => list_remove x l = list_remove_list k
    end.
End contains_dec_help.
270

271
272
273
274
(** The [same_length] view allows convenient induction over two lists with the
same length. *)
Inductive same_length {A B} : list A  list B  Prop :=
  | same_length_nil : same_length [] []
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
  | same_length_cons x1 x2 l1 l2 :
     same_length l1 l2  same_length (x1 :: l1) (x2 :: l2).
Infix "`same_length`" := same_length (at level 70) : C_scope.

(** Set operations on lists *)
Section list_set.
  Context {A} {dec :  x y : A, Decision (x = y)}.

  Global Instance elem_of_list_dec {dec :  x y : A, Decision (x = y)}
    (x : A) :  l, Decision (x  l).
  Proof.
   refine (
    fix go l :=
    match l return Decision (x  l) with
    | [] => right _
    | y :: l => cast_if_or (decide (x = y)) (go l)
    end); clear go dec; subst; try (by constructor); abstract by inversion 1.
  Defined.

  Fixpoint remove_dups (l : list A) : list A :=
    match l with
    | [] => []
    | x :: l =>
      if decide_rel () x l then remove_dups l else x :: remove_dups l
    end.

  Fixpoint list_difference (l k : list A) : list A :=
    match l with
    | [] => []
    | x :: l =>
      if decide_rel () x k
      then list_difference l k
      else x :: list_difference l k
    end.
  Fixpoint list_intersection (l k : list A) : list A :=
    match l with
    | [] => []
    | x :: l =>
      if decide_rel () x k
      then x :: list_intersection l k
      else list_intersection l k
    end.
  Definition list_intersection_with (f : A  A  option A) :
    list A  list A  list A := fix go l k :=
    match l with
    | [] => []
    | x :: l => foldr (λ y,
        match f x y with None => id | Some z => (z ::) end) (go l k) k
    end.
End list_set.
325
326

(** * Basic tactics on lists *)
327
328
329
(** The tactic [discriminate_list_equality] discharges a goal if it contains
a list equality involving [(::)] and [(++)] of two lists that have a different
length as one of its hypotheses. *)
330
331
Tactic Notation "discriminate_list_equality" hyp(H) :=
  apply (f_equal length) in H;
332
  repeat (simpl in H || rewrite app_length in H); exfalso; lia.
333
Tactic Notation "discriminate_list_equality" :=
334
335
336
  match goal with
  | H : @eq (list _) _ _ |- _ => discriminate_list_equality H
  end.
337

338
339
340
(** The tactic [simplify_list_equality] simplifies hypotheses involving
equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
lookups in singleton lists. *)
341
342
343
Ltac simplify_list_equality :=
  repeat match goal with
  | _ => progress simplify_equality
344
  | H : _ ++ _ = _ ++ _ |- _ => first
345
346
    [ apply app_inj_tail in H; destruct H
    | apply app_inv_head in H | apply app_inv_tail in H ]
Robbert Krebbers's avatar
Robbert Krebbers committed
347
  | H : [?x] !! ?i = Some ?y |- _ =>
348
349
350
    destruct i; [change (Some x = Some y) in H | discriminate]
  end;
  try discriminate_list_equality.
351
352
Ltac simplify_list_equality' :=
  repeat (progress simpl in * || simplify_list_equality).
353

354
355
(** * General theorems *)
Section general_properties.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
Context {A : Type}.
357
358
Implicit Types x y z : A.
Implicit Types l k : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
359

360
361
362
Global Instance: Injective2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed.
Global Instance:  k, Injective (=) (=) (k ++).
363
Proof. intros ???. apply app_inv_head. Qed.
364
Global Instance:  k, Injective (=) (=) (++ k).
365
Proof. intros ???. apply app_inv_tail. Qed.
366
367
368
369
370
371
Global Instance: Associative (=) (@app A).
Proof. intros ???. apply app_assoc. Qed.
Global Instance: LeftId (=) [] (@app A).
Proof. done. Qed.
Global Instance: RightId (=) [] (@app A).
Proof. intro. apply app_nil_r. Qed.
372

373
374
375
376
377
378
379
380
381
382
Lemma app_nil l1 l2 : l1 ++ l2 = []  l1 = []  l2 = [].
Proof. split. apply app_eq_nil. by intros [??]; subst. Qed.
Lemma app_singleton l1 l2 x :
  l1 ++ l2 = [x]  l1 = []  l2 = [x]  l1 = [x]  l2 = [].
Proof. split. apply app_eq_unit. by intros [[??]|[??]]; subst. Qed.

Lemma cons_middle x l1 l2 : l1 ++ x :: l2 = l1 ++ [x] ++ l2.
Proof. done. Qed.
Lemma app_inj l1 k1 l2 k2 :
  length l1 = length k1  l1 ++ l2 = k1 ++ k2  l1 = k1  l2 = k2.
Robbert Krebbers's avatar
Robbert Krebbers committed
383
384
Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed.

385
Lemma list_eq l1 l2 : ( i, l1 !! i = l2 !! i)  l1 = l2.
386
387
Proof.
  revert l2. induction l1; intros [|??] H.
388
  * done.
389
390
  * discriminate (H 0).
  * discriminate (H 0).
391
  * f_equal; [by injection (H 0) |]. apply IHl1. intro. apply (H (S _)).
392
Qed.
393
Lemma list_eq_nil l : ( i, l !! i = None)  l = nil.
394
Proof. intros. by apply list_eq. Qed.
395

396
Global Instance list_eq_dec {dec :  x y, Decision (x = y)} :  l k,
397
  Decision (l = k) := list_eq_dec dec.
398
399
Definition list_singleton_dec l : { x | l = [x] } + { length l  1 }.
Proof. by refine match l with [x] => inleft (x_) | _ => inright _ end. Defined.
400

401
Lemma nil_or_length_pos l : l = []  length l  0.
402
Proof. destruct l; simpl; auto with lia. Qed.
403
Lemma nil_length l : length l = 0  l = [].
404
405
Proof. by destruct l. Qed.
Lemma lookup_nil i : @nil A !! i = None.
406
Proof. by destruct i. Qed.
407
Lemma lookup_tail l i : tail l !! i = l !! S i.
408
Proof. by destruct l. Qed.
409

410
411
Lemma lookup_lt_Some l i x : l !! i = Some x  i < length l.
Proof.
412
  revert i. induction l; intros [|?] ?; simplify_equality'; auto with arith.
413
414
415
416
417
Qed.
Lemma lookup_lt_is_Some_1 l i : is_Some (l !! i)  i < length l.
Proof. intros [??]; eauto using lookup_lt_Some. Qed.
Lemma lookup_lt_is_Some_2 l i : i < length l  is_Some (l !! i).
Proof.
418
  revert i. induction l; intros [|?] ?; simplify_equality'; eauto with lia.
419
420
421
422
423
424
425
426
427
428
429
430
Qed.
Lemma lookup_lt_is_Some l i : is_Some (l !! i)  i < length l.
Proof. split; auto using lookup_lt_is_Some_1, lookup_lt_is_Some_2. Qed.

Lemma lookup_ge_None l i : l !! i = None  length l  i.
Proof. rewrite eq_None_not_Some, lookup_lt_is_Some. lia. Qed.
Lemma lookup_ge_None_1 l i : l !! i = None  length l  i.
Proof. by rewrite lookup_ge_None. Qed.
Lemma lookup_ge_None_2 l i : length l  i  l !! i = None.
Proof. by rewrite lookup_ge_None. Qed.

Lemma list_eq_length l1 l2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
431
  length l2 = length l1 
432
  ( i x y, l1 !! i = Some x  l2 !! i = Some y  x = y)  l1 = l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
433
Proof.
434
435
436
437
438
  intros Hl ?. apply list_eq. intros i. destruct (l2 !! i) as [x|] eqn:Hx.
  * destruct (lookup_lt_is_Some_2 l1 i) as [y ?]; subst.
    + rewrite <-Hl. eauto using lookup_lt_Some.
    + naive_solver.
  * by rewrite lookup_ge_None, <-Hl, <-lookup_ge_None.
Robbert Krebbers's avatar
Robbert Krebbers committed
439
440
Qed.

441
Lemma lookup_app_l l1 l2 i : i < length l1  (l1 ++ l2) !! i = l1 !! i.
442
Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
443
444
Lemma lookup_app_l_Some l1 l2 i x : l1 !! i = Some x  (l1 ++ l2) !! i = Some x.
Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
445

446
Lemma lookup_app_r l1 l2 i : (l1 ++ l2) !! (length l1 + i) = l2 !! i.
447
448
449
450
Proof. revert i. induction l1; intros [|i]; simplify_equality'; auto. Qed.
Lemma lookup_app_r_alt l1 l2 i j :
  j = length l1  (l1 ++ l2) !! (j + i) = l2 !! i.
Proof. intros ->. by apply lookup_app_r. Qed.
451
452
Lemma lookup_app_r_Some l1 l2 i x :
  l2 !! i = Some x  (l1 ++ l2) !! (length l1 + i) = Some x.
453
Proof. by rewrite lookup_app_r. Qed.
454
455
456
457
Lemma lookup_app_minus_r l1 l2 i :
  length l1  i  (l1 ++ l2) !! i = l2 !! (i - length l1).
Proof. intros. rewrite <-(lookup_app_r l1 l2). f_equal. lia. Qed.

458
459
Lemma lookup_app_inv l1 l2 i x :
  (l1 ++ l2) !! i = Some x  l1 !! i = Some x  l2 !! (i - length l1) = Some x.
460
Proof. revert i. induction l1; intros [|i] ?; simplify_equality'; auto. Qed.
461
Lemma list_lookup_middle l1 l2 x : (l1 ++ x :: l2) !! length l1 = Some x.
462
Proof. by induction l1; simpl. Qed.
463

464
Lemma alter_length f l i : length (alter f i l) = length l.
465
Proof. revert i. induction l; intros [|?]; simpl; auto with lia. Qed.
466
Lemma insert_length l i x : length (<[i:=x]>l) = length l.
467
468
Proof. apply alter_length. Qed.

469
Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
470
Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
471
Lemma list_lookup_alter_ne f l i j : i  j  alter f i l !! j = l !! j.
472
473
474
475
Proof.
  revert i j. induction l; [done|].
  intros [|i] [|j] ?; try done. apply (IHl i). congruence.
Qed.
476
Lemma list_lookup_insert l i x : i < length l  <[i:=x]>l !! i = Some x.
477
Proof.
478
  intros Hi. unfold insert, list_insert. rewrite list_lookup_alter.
479
  by destruct (lookup_lt_is_Some_2 l i); simplify_option_equality.
480
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
481
Lemma list_lookup_insert_ne l i j x : i  j  <[i:=x]>l !! j = l !! j.
482
483
Proof. apply list_lookup_alter_ne. Qed.

484
485
Lemma list_lookup_other l i x :
  length l  1  l !! i = Some x   j y, j  i  l !! j = Some y.
Robbert Krebbers's avatar
Robbert Krebbers committed
486
Proof.
487
  intros. destruct i, l as [|x0 [|x1 l]]; simplify_equality'.
Robbert Krebbers's avatar
Robbert Krebbers committed
488
489
490
491
  * by exists 1 x1.
  * by exists 0 x0.
Qed.

492
493
Lemma alter_app_l f l1 l2 i :
  i < length l1  alter f i (l1 ++ l2) = alter f i l1 ++ l2.
494
Proof.
495
  revert i. induction l1; intros [|?] ?; simpl in *; f_equal; auto with lia.
496
Qed.
497
Lemma alter_app_r f l1 l2 i :
498
  alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2.
499
500
501
Proof. revert i. induction l1; intros [|?]; simpl in *; f_equal; auto. Qed.
Lemma alter_app_r_alt f l1 l2 i :
  length l1  i  alter f i (l1 ++ l2) = l1 ++ alter f (i - length l1) l2.
502
503
504
505
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply alter_app_r.
Qed.
506
507
508
509
510
511
512
513
514
515
516
517
Lemma list_alter_ext f g l i :
  ( x, l !! i = Some x  f x = g x)  alter f i l = alter g i l.
Proof. revert i. induction l; intros [|?] ?; simpl; f_equal; auto. Qed.
Lemma list_alter_compose f g l i :
  alter (f  g) i l = alter f i (alter g i l).
Proof. revert i. induction l; intros [|?]; simpl; f_equal; auto. Qed.
Lemma list_alter_commute f g l i j :
  i  j  alter f i (alter g j l) = alter g j (alter f i l).
Proof.
  revert i j.
  induction l; intros [|?] [|?]; simpl; auto with f_equal congruence.
Qed.
518

519
520
Lemma insert_app_l l1 l2 i x :
  i < length l1  <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
521
Proof. apply alter_app_l. Qed.
522
Lemma insert_app_r l1 l2 i x : <[length l1+i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2.
523
Proof. apply alter_app_r. Qed.
524
525
Lemma insert_app_r_alt l1 l2 i x :
  length l1  i  <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
526
527
Proof. apply alter_app_r_alt. Qed.

528
Lemma delete_middle l1 l2 x : delete (length l1) (l1 ++ x :: l2) = l1 ++ l2.
529
530
Proof. induction l1; simpl; f_equal; auto. Qed.

531
(** ** Properties of the [elem_of] predicate *)
532
Lemma not_elem_of_nil x : x  [].
533
Proof. by inversion 1. Qed.
534
Lemma elem_of_nil x : x  []  False.
535
Proof. intuition. by destruct (not_elem_of_nil x). Qed.
536
Lemma elem_of_nil_inv l : ( x, x  l)  l = [].
537
Proof. destruct l. done. by edestruct 1; constructor. Qed.
538
Lemma elem_of_cons l x y : x  y :: l  x = y  x  l.
539
540
Proof.
  split.
541
542
  * inversion 1; subst. by left. by right.
  * intros [?|?]; subst. by left. by right.
543
Qed.
544
Lemma not_elem_of_cons l x y : x  y :: l  x  y  x  l.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
Proof. rewrite elem_of_cons. tauto. Qed.
546
Lemma elem_of_app l1 l2 x : x  l1 ++ l2  x  l1  x  l2.
547
Proof.
548
  induction l1.
549
  * split; [by right|]. intros [Hx|]; [|done]. by destruct (elem_of_nil x).
550
  * simpl. rewrite !elem_of_cons, IHl1. tauto.
551
Qed.
552
Lemma not_elem_of_app l1 l2 x : x  l1 ++ l2  x  l1  x  l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
553
Proof. rewrite elem_of_app. tauto. Qed.
554
Lemma elem_of_list_singleton x y : x  [y]  x = y.
555
Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.
556

Robbert Krebbers's avatar
Robbert Krebbers committed
557
Global Instance elem_of_list_permutation_proper x : Proper (() ==> iff) (x ).
558
Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
559

560
Lemma elem_of_list_split l x : x  l   l1 l2, l = l1 ++ x :: l2.
561
562
563
564
565
Proof.
  induction 1 as [x l|x y l ? [l1 [l2 ?]]].
  * by eexists [], l.
  * subst. by exists (y :: l1) l2.
Qed.
566

567
Lemma elem_of_list_lookup_1 l x : x  l   i, l !! i = Some x.
568
Proof.
569
570
  induction 1 as [|???? IH]; [by exists 0 |].
  destruct IH as [i ?]; auto. by exists (S i).
571
Qed.
572
Lemma elem_of_list_lookup_2 l i x : l !! i = Some x  x  l.
573
Proof.
574
  revert i. induction l; intros [|i] ?; simplify_equality'; constructor; eauto.
575
Qed.
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
Lemma elem_of_list_lookup l x : x  l   i, l !! i = Some x.
Proof. firstorder eauto using elem_of_list_lookup_1, elem_of_list_lookup_2. Qed.

(** ** Set operations on lists *)
Section list_set.
  Context {dec :  x y, Decision (x = y)}.

  Lemma elem_of_list_difference l k x :
    x  list_difference l k  x  l  x  k.
  Proof.
    split; induction l; simpl; try case_decide;
      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
  Qed.
  Lemma list_difference_nodup l k : NoDup l  NoDup (list_difference l k).
  Proof.
    induction 1; simpl; try case_decide.
    * constructor.
    * done.
    * constructor. rewrite elem_of_list_difference; intuition. done.
  Qed.

  Lemma elem_of_list_intersection l k x :
    x  list_intersection l k  x  l  x  k.
  Proof.
    split; induction l; simpl; repeat case_decide;
      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
  Qed.
  Lemma list_intersection_nodup l k : NoDup l  NoDup (list_intersection l k).
  Proof.
    induction 1; simpl; try case_decide.
    * constructor.
    * constructor. rewrite elem_of_list_intersection; intuition. done.
    * done.
  Qed.

  Lemma elem_of_list_intersection_with f l k x :
    x  list_intersection_with f l k   x1 x2,
      x1  l  x2  k  f x1 x2 = Some x.
  Proof.
    split.
    * induction l as [|x1 l IH]; simpl.
      + by rewrite elem_of_nil.
      + intros Hx. setoid_rewrite elem_of_cons.
        cut (( x2, x2  k  f x1 x2 = Some x)
           x  list_intersection_with f l k); [naive_solver|].
        clear IH. revert Hx. generalize (list_intersection_with f l k).
        induction k; simpl; [by auto|].
        case_match; setoid_rewrite elem_of_cons; naive_solver.
    * intros (x1 & x2 & Hx1 & Hx2 & Hx).
      induction Hx1 as [x1 | x1 ? l ? IH]; simpl.
      + generalize (list_intersection_with f l k).
        induction Hx2; simpl; [by rewrite Hx; left |].
        case_match; simpl; try setoid_rewrite elem_of_cons; auto.
      + generalize (IH Hx). clear Hx IH Hx2.
        generalize (list_intersection_with f l k).
        induction k; simpl; intros; [done |].
        case_match; simpl; rewrite ?elem_of_cons; auto.
  Qed.
End list_set.
Robbert Krebbers's avatar
Robbert Krebbers committed
635

636
(** ** Properties of the [NoDup] predicate *)
637
638
Lemma NoDup_nil : NoDup (@nil A)  True.
Proof. split; constructor. Qed.
639
Lemma NoDup_cons x l : NoDup (x :: l)  x  l  NoDup l.
640
Proof. split. by inversion 1. intros [??]. by constructor. Qed.
641
Lemma NoDup_cons_11 x l : NoDup (x :: l)  x  l.
642
Proof. rewrite NoDup_cons. by intros [??]. Qed.
643
Lemma NoDup_cons_12 x l : NoDup (x :: l)  NoDup l.
644
Proof. rewrite NoDup_cons. by intros [??]. Qed.
645
Lemma NoDup_singleton x : NoDup [x].
646
647
Proof. constructor. apply not_elem_of_nil. constructor. Qed.

648
Lemma NoDup_app l k : NoDup (l ++ k)  NoDup l  ( x, x  l  x  k)  NoDup k.
Robbert Krebbers's avatar
Robbert Krebbers committed
649
Proof.
650
  induction l; simpl.
651
  * rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver.
652
  * rewrite !NoDup_cons.
Robbert Krebbers's avatar
Robbert Krebbers committed
653
    setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
654
Qed.
655
Global Instance NoDup_proper: Proper (() ==> iff) (@NoDup A).
656
657
658
659
660
661
662
Proof.
  induction 1 as [|x l k Hlk IH | |].
  * by rewrite !NoDup_nil.
  * by rewrite !NoDup_cons, IH, Hlk.
  * rewrite !NoDup_cons, !elem_of_cons. intuition.
  * intuition.
Qed.
663
664
Lemma NoDup_lookup l i j x :
  NoDup l  l !! i = Some x  l !! j = Some x  i = j.
665
666
667
668
669
670
Proof.
  intros Hl. revert i j. induction Hl as [|x' l Hx Hl IH].
  { intros; simplify_equality. }
  intros [|i] [|j] ??; simplify_equality'; eauto with f_equal;
    exfalso; eauto using elem_of_list_lookup_2.
Qed.
671
672
Lemma NoDup_alt l :
  NoDup l   i j x, l !! i = Some x  l !! j = Some x  i = j.
673
Proof.
674
675
676
677
678
  split; eauto using NoDup_lookup.
  induction l as [|x l IH]; intros Hl; constructor.
  * rewrite elem_of_list_lookup. intros [i ?].
    by feed pose proof (Hl (S i) 0 x); auto.
  * apply IH. intros i j x' ??. by apply (injective S), (Hl (S i) (S j) x').
679
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
680

681
682
Section no_dup_dec.
  Context `{! x y, Decision (x = y)}.
683

684
685
686
687
  Global Instance NoDup_dec:  l, Decision (NoDup l) :=
    fix NoDup_dec l :=
    match l return Decision (NoDup l) with
    | [] => left NoDup_nil_2
688
    | x :: l =>
689
690
691
692
693
694
695
696
      match decide_rel () x l with
      | left Hin => right (λ H, NoDup_cons_11 _ _ H Hin)
      | right Hin =>
        match NoDup_dec l with
        | left H => left (NoDup_cons_2 _ _ Hin H)
        | right H => right (H  NoDup_cons_12 _ _)
        end
      end
697
    end.
698

699
  Lemma elem_of_remove_dups l x : x  remove_dups l  x  l.
700
701
702
703
704
705
706
707
708
  Proof.
    split; induction l; simpl; repeat case_decide;
      rewrite ?elem_of_cons; intuition (simplify_equality; auto).
  Qed.
  Lemma remove_dups_nodup l : NoDup (remove_dups l).
  Proof.
    induction l; simpl; repeat case_decide; try constructor; auto.
    by rewrite elem_of_remove_dups.
  Qed.
709
End no_dup_dec.
710

711
(** ** Properties of the [filter] function *)
712
713
714
715
716
717
718
719
720
721
722
723
724
725
Section filter.
  Context (P : A  Prop) `{ x, Decision (P x)}.

  Lemma elem_of_list_filter l x : x  filter P l  P x  x  l.
  Proof.
    unfold filter. induction l; simpl; repeat case_decide;
       rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
  Qed.
  Lemma filter_nodup l : NoDup l  NoDup (filter P l).
  Proof.
    unfold filter. induction 1; simpl; repeat case_decide;
      rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
  Qed.
End filter.
Robbert Krebbers's avatar
Robbert Krebbers committed
726

727
728
729
730
(** ** Properties of the [find] function *)
Section find.
  Context (P : A  Prop) `{ x, Decision (P x)}.

731
732
  Lemma list_find_Some l i :
    list_find P l = Some i   x, l !! i = Some x  P x.
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
  Proof.
    revert i. induction l; simpl; repeat case_decide;
      eauto with simplify_option_equality.
  Qed.
  Lemma list_find_elem_of l x : x  l  P x   i, list_find P l = Some i.
  Proof.
    induction 1; simpl; repeat case_decide;
      naive_solver (by eauto with simplify_option_equality).
  Qed.
End find.

Section find_eq.
  Context `{ x y, Decision (x = y)}.

  Lemma list_find_eq_Some l i x : list_find (x =) l = Some i  l !! i = Some x.
  Proof.
749
750
    intros.
    destruct (list_find_Some (x =) l i) as (?&?&?); auto with congruence.
751
752
753
754
755
  Qed.
  Lemma list_find_eq_elem_of l x : x  l   i, list_find (x=) l = Some i.
  Proof. eauto using list_find_elem_of. Qed.
End find_eq.

756
(** ** Properties of the [reverse] function *)
757
758
Lemma reverse_nil : reverse [] = @nil A.
Proof. done. Qed.
759
Lemma reverse_singleton x : reverse [x] = [x].
760
Proof. done. Qed.
761
Lemma reverse_cons l x : reverse (x :: l) = reverse l ++ [x].
762
Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
763
Lemma reverse_snoc l x : reverse (l ++ [x]) = x :: reverse l.
764
Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
765
Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
766
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
767
Lemma reverse_length l : length (reverse l) = length l.
768
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
769
Lemma reverse_involutive l : reverse (reverse l) = l.
770
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
Lemma elem_of_reverse_2 x l : x  l  x  reverse l.
Proof.
  induction 1; rewrite reverse_cons, elem_of_app,
    ?elem_of_list_singleton; intuition.
Qed.
Lemma elem_of_reverse x l : x  reverse l  x  l.
Proof.
  split; auto using elem_of_reverse_2.
  intros. rewrite <-(reverse_involutive l). by apply elem_of_reverse_2.
Qed.
Global Instance: Injective (=) (=) (@reverse A).
Proof.
  intros l1 l2 Hl.
  by rewrite <-(reverse_involutive l1), <-(reverse_involutive l2), Hl.
Qed.
786

787
(** ** Properties of the [take] function *)
788
789
790
Definition take_drop := @firstn_skipn A.

Lemma take_nil n : take n (@nil A) = [].
Robbert Krebbers's avatar
Robbert Krebbers committed
791
Proof. by destruct n. Qed.
792
Lemma take_app l k : take (length l) (l ++ k) = l.
Robbert Krebbers's avatar
Robbert Krebbers committed
793
Proof. induction l; simpl; f_equal; auto. Qed.
794
Lemma take_app_alt l k n : n = length l  take n (l ++ k) = l.
Robbert Krebbers's avatar
Robbert Krebbers committed
795
Proof. intros Hn. by rewrite Hn, take_app. Qed.
796
Lemma take_app_le l k n : n  length l  take n (l ++ k) = take n l.
Robbert Krebbers's avatar
Robbert Krebbers committed
797
Proof.
798
  revert n. induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
799
Qed.
800
801
Lemma take_app_ge l k n :
  length l  n  take n (l ++ k) = l ++ take (n - length l) k.
Robbert Krebbers's avatar
Robbert Krebbers committed
802
Proof.
803
  revert n. induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
804
Qed.
805
Lemma take_ge l n : length l  n  take n l = l.
Robbert Krebbers's avatar
Robbert Krebbers committed
806
Proof.
807
  revert n. induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
808
809
Qed.

810
Lemma take_take l n m : take n (take m l) = take (min n m) l.
Robbert Krebbers's avatar
Robbert Krebbers committed
811
Proof. revert n m. induction l; intros [|?] [|?]; simpl; f_equal; auto. Qed.
812
Lemma take_idempotent l n : take n (take n l) = take n l.
Robbert Krebbers's avatar
Robbert Krebbers committed
813
814
Proof. by rewrite take_take, Min.min_idempotent. Qed.

815
Lemma take_length l n : length (take n l) = min n (length l).
Robbert Krebbers's avatar
Robbert Krebbers committed
816
Proof. revert n. induction l; intros [|?]; simpl; f_equal; done. Qed.
817
Lemma take_length_le l n : n  length l  length (take n l) = n.
Robbert Krebbers's avatar
Robbert Krebbers committed
818
Proof. rewrite take_length. apply Min.min_l. Qed.
819
820
Lemma take_length_ge l n : length l  n  length (take n l) = length l.
Proof. rewrite take_length. apply Min.min_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
821

822
Lemma lookup_take l n i : i < n  take n l !! i = l !! i.
Robbert Krebbers's avatar
Robbert Krebbers committed
823
824
825
826
827
Proof.
  revert n i. induction l; intros [|n] i ?; trivial.
  * auto with lia.
  * destruct i; simpl; auto with arith.
Qed.
828
Lemma lookup_take_ge l n i : n  i  take n l !! i = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
829
Proof. revert n i. induction l; intros [|?] [|?] ?; simpl; auto with lia. Qed.
830
Lemma take_alter f l n i : n  i  take n (alter f i l) = take n l.
Robbert Krebbers's avatar
Robbert Krebbers committed
831
832
833
834
835
Proof.
  intros. apply list_eq. intros j. destruct (le_lt_dec