list.v 111 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

(** 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. *)
59
60
Instance list_delete {A} : Delete nat (list A) :=
  fix go (i : nat) (l : list A) {struct l} : list A :=
61
62
  match l with
  | [] => []
63
  | x :: l => match i with 0 => l | S i => x :: @delete _ _ go i l end
64
  end.
65
66
67

(** 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. *)
68
Instance list_insert {A} : Insert nat A (list A) := λ i x, alter (λ _, x) i.
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
85
86
87
88
  end.

(** 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 :=
89
  match n with 0 => [] | S n => x :: replicate n x end.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
92
93

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

94
Fixpoint last' {A} (x : A) (l : list A) : A :=
95
  match l with [] => x | x :: l => last' x l end.
96
Definition last {A} (l : list A) : option A :=
97
  match l with [] => None | x :: l => Some (last' x l) end.
98

Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
102
103
104
(** 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
105
  | x :: l => match n with 0 => [] | S n => x :: resize n y l end
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
  end.
Arguments resize {_} !_ _ !_.

109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
(** 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) :=
124
  match l with [] => [] | x :: l => f x :: @fmap _ _ _ f go l end.
125
126
Instance list_bind {A B} (f : A  list B) : MBindD list f :=
  fix go (l : list A) :=
127
  match l with [] => [] | x :: l => f x ++ @mbind _ _ _ f go l end.
128
129
Instance list_join: MJoin list :=
  fix go A (ls : list (list A)) : list A :=
130
  match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
131
132
133
134
135

(** 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) :=
136
  match l with [] => [] | x :: l => f n x :: go (S n) l end.
137
138
Definition imap {A B} (f : nat  A  B) : list A  list B := imap_go f 0.

139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
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 {_ _} _ _ _ _ _.
154
155
156
157

(** Zipping lists. *)
Definition zip_with {A B C} (f : A  B  C) : list A  list B  list C :=
  fix go l1 l2 :=
158
  match l1, l2 with x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2 | _ , _ => [] end.
159
160
161
162
163
164
165
166
167
168
169
170
171
172
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.

173
174
(** 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. *)
175
176
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.
177
178
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
179

180
181
182
183
184
185
186
187
188
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 =>
189
190
191
      if decide_rel (=) x1 x2
      then snd_map (x1 ::) (go l1 l2)
      else (x1 :: l1, x2 :: l2, [])
192
193
194
195
196
197
198
199
200
    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
201

202
203
204
205
(** A list [l1] is a sub list of [l2] if [l2] is obtained by removing elements
from [l1] without changing the order. *)
Inductive sublist {A} : relation (list A) :=
  | sublist_nil : sublist [] []
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
  | sublist_skip x l1 l2 : sublist l1 l2  sublist (x :: l1) (x :: l2)
  | sublist_insert x l1 l2 : sublist l1 l2  sublist l1 (x :: l2).
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)
  | contains_insert x l1 l2 : contains l1 l2  contains l1 (x :: l2)
  | 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.
234

235
236
237
238
(** 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 [] []
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
  | 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.
289
290

(** * Basic tactics on lists *)
291
292
293
(** 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. *)
294
295
Tactic Notation "discriminate_list_equality" hyp(H) :=
  apply (f_equal length) in H;
296
  repeat (simpl in H || rewrite app_length in H); exfalso; lia.
297
Tactic Notation "discriminate_list_equality" :=
298
299
300
  match goal with
  | H : @eq (list _) _ _ |- _ => discriminate_list_equality H
  end.
301

302
303
304
(** The tactic [simplify_list_equality] simplifies hypotheses involving
equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
lookups in singleton lists. *)
305
306
307
Ltac simplify_list_equality :=
  repeat match goal with
  | _ => progress simplify_equality
308
  | H : _ ++ _ = _ ++ _ |- _ => first
309
310
    [ 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
311
  | H : [?x] !! ?i = Some ?y |- _ =>
312
313
314
    destruct i; [change (Some x = Some y) in H | discriminate]
  end;
  try discriminate_list_equality.
315

316
317
(** * General theorems *)
Section general_properties.
Robbert Krebbers's avatar
Robbert Krebbers committed
318
Context {A : Type}.
319
320
Implicit Types x y z : A.
Implicit Types l k : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
321

322
323
324
Global Instance: Injective2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed.
Global Instance:  x, Injective (=) (=) (x ::).
Robbert Krebbers's avatar
Robbert Krebbers committed
325
Proof. by injection 1. Qed.
326
Global Instance:  l, Injective (=) (=) (:: l).
Robbert Krebbers's avatar
Robbert Krebbers committed
327
Proof. by injection 1. Qed.
328
Global Instance:  k, Injective (=) (=) (k ++).
329
Proof. intros ???. apply app_inv_head. Qed.
330
Global Instance:  k, Injective (=) (=) (++ k).
331
Proof. intros ???. apply app_inv_tail. Qed.
332
333
334
335
336
337
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.
338

339
340
341
342
343
344
345
346
347
348
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
349
350
Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed.

351
Lemma list_eq l1 l2 : ( i, l1 !! i = l2 !! i)  l1 = l2.
352
353
Proof.
  revert l2. induction l1; intros [|??] H.
354
  * done.
355
356
  * discriminate (H 0).
  * discriminate (H 0).
357
  * f_equal; [by injection (H 0) |]. apply IHl1. intro. apply (H (S _)).
358
Qed.
359
Lemma list_eq_nil l : ( i, l !! i = None)  l = nil.
360
Proof. intros. by apply list_eq. Qed.
361

362
Global Instance list_eq_dec {dec :  x y, Decision (x = y)} :  l k,
363
  Decision (l = k) := list_eq_dec dec.
364
365
Definition list_singleton_dec l : { x | l = [x] } + { length l  1 }.
Proof. by refine match l with [x] => inleft (x_) | _ => inright _ end. Defined.
366

367
Lemma nil_or_length_pos l : l = []  length l  0.
368
Proof. destruct l; simpl; auto with lia. Qed.
369
Lemma nil_length l : length l = 0  l = [].
370
371
Proof. by destruct l. Qed.
Lemma lookup_nil i : @nil A !! i = None.
372
Proof. by destruct i. Qed.
373
Lemma lookup_tail l i : tail l !! i = l !! S i.
374
Proof. by destruct l. Qed.
375

376
Lemma lookup_lt_length l i : is_Some (l !! i)  i < length l.
377
Proof.
378
379
380
381
382
  revert i. induction l.
  * split; by inversion 1.
  * intros [|?]; simpl.
    + split; eauto with arith.
    + by rewrite <-NPeano.Nat.succ_lt_mono.
383
Qed.
384
Lemma lookup_lt_length_1 l i : is_Some (l !! i)  i < length l.
385
Proof. apply lookup_lt_length. Qed.
386
Lemma lookup_lt_length_alt l i x : l !! i = Some x  i < length l.
387
Proof. intros Hl. by rewrite <-lookup_lt_length, Hl. Qed.
388
Lemma lookup_lt_length_2 l i : i < length l  is_Some (l !! i).
389
390
Proof. apply lookup_lt_length. Qed.

391
Lemma lookup_ge_length l i : l !! i = None  length l  i.
392
Proof. rewrite eq_None_not_Some, lookup_lt_length. lia. Qed.
393
Lemma lookup_ge_length_1 l i : l !! i = None  length l  i.
394
Proof. by rewrite lookup_ge_length. Qed.
395
Lemma lookup_ge_length_2 l i : length l  i  l !! i = None.
396
397
Proof. by rewrite lookup_ge_length. Qed.

398
Lemma list_eq_length_eq l1 l2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
399
  length l2 = length l1 
400
  ( i x y, l1 !! i = Some x  l2 !! i = Some y  x = y)  l1 = l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
401
402
403
Proof.
  intros Hlength Hlookup. apply list_eq. intros i.
  destruct (l2 !! i) as [x|] eqn:E.
404
405
  * feed inversion (lookup_lt_length_2 l1 i) as [y]; [|eauto with f_equal].
    pose proof (lookup_lt_length_alt l2 i x E). lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
406
407
408
  * rewrite lookup_ge_length in E |- *. lia.
Qed.

409
410
Lemma lookup_app_l l1 l2 i :
  i < length l1  (l1 ++ l2) !! i = l1 !! i.
411
Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
412
413
Lemma lookup_app_l_Some l1 l2 i x :
  l1 !! i = Some x  (l1 ++ l2) !! i = Some x.
414
Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_length_alt. Qed.
415
Lemma lookup_app_r l1 l2 i : (l1 ++ l2) !! (length l1 + i) = l2 !! i.
416
Proof.
417
  revert i. induction l1; intros [|i]; simpl in *; simplify_equality; auto.
418
Qed.
419
420
Lemma lookup_app_r_alt l1 l2 i :
  length l1  i  (l1 ++ l2) !! i = l2 !! (i - length l1).
421
422
423
424
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply lookup_app_r.
Qed.
425
426
Lemma lookup_app_r_Some l1 l2 i x :
  l2 !! i = Some x  (l1 ++ l2) !! (length l1 + i) = Some x.
427
Proof. by rewrite lookup_app_r. Qed.
428
429
Lemma lookup_app_r_Some_alt l1 l2 i x :
  length l1  i  l2 !! (i - length l1) = Some x  (l1 ++ l2) !! i = Some x.
430
Proof. intro. by rewrite lookup_app_r_alt. Qed.
431
432
Lemma lookup_app_inv l1 l2 i x :
  (l1 ++ l2) !! i = Some x  l1 !! i = Some x  l2 !! (i - length l1) = Some x.
433
Proof.
434
  revert i. induction l1; intros [|i] ?; simpl in *; simplify_equality; auto.
435
Qed.
436
Lemma list_lookup_middle l1 l2 x : (l1 ++ x :: l2) !! length l1 = Some x.
437
Proof. by induction l1; simpl. Qed.
438

439
Lemma alter_length f l i : length (alter f i l) = length l.
440
Proof. revert i. induction l; intros [|?]; simpl; auto with lia. Qed.
441
Lemma insert_length l i x : length (<[i:=x]>l) = length l.
442
443
Proof. apply alter_length. Qed.

444
Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
445
Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
446
Lemma list_lookup_alter_ne f l i j : i  j  alter f i l !! j = l !! j.
447
448
449
450
Proof.
  revert i j. induction l; [done|].
  intros [|i] [|j] ?; try done. apply (IHl i). congruence.
Qed.
451
Lemma list_lookup_insert l i x : i < length l  <[i:=x]>l !! i = Some x.
452
Proof.
453
  intros Hi. unfold insert, list_insert. rewrite list_lookup_alter.
454
455
  by feed inversion (lookup_lt_length_2 l i).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
456
Lemma list_lookup_insert_ne l i j x : i  j  <[i:=x]>l !! j = l !! j.
457
458
Proof. apply list_lookup_alter_ne. Qed.

459
460
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
461
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
462
  intros. destruct i, l as [|x0 [|x1 l]]; simpl in *; simplify_equality.
Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
465
466
  * by exists 1 x1.
  * by exists 0 x0.
Qed.

467
468
Lemma alter_app_l f l1 l2 i :
  i < length l1  alter f i (l1 ++ l2) = alter f i l1 ++ l2.
469
Proof.
470
  revert i. induction l1; intros [|?] ?; simpl in *; f_equal; auto with lia.
471
Qed.
472
Lemma alter_app_r f l1 l2 i :
473
  alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2.
474
475
476
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.
477
478
479
480
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply alter_app_r.
Qed.
481

482
483
Lemma insert_app_l l1 l2 i x :
  i < length l1  <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
484
Proof. apply alter_app_l. Qed.
485
Lemma insert_app_r l1 l2 i x : <[length l1+i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2.
486
Proof. apply alter_app_r. Qed.
487
488
Lemma insert_app_r_alt l1 l2 i x :
  length l1  i  <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
489
490
Proof. apply alter_app_r_alt. Qed.

491
Lemma insert_consecutive_length l i k :
492
493
  length (insert_consecutive i k l) = length l.
Proof. revert i. by induction k; intros; simpl; rewrite ?insert_length. Qed.
494

495
Lemma delete_middle l1 l2 x : delete (length l1) (l1 ++ x :: l2) = l1 ++ l2.
496
497
Proof. induction l1; simpl; f_equal; auto. Qed.

498
(** ** Properties of the [elem_of] predicate *)
499
Lemma not_elem_of_nil x : x  [].
500
Proof. by inversion 1. Qed.
501
Lemma elem_of_nil x : x  []  False.
502
Proof. intuition. by destruct (not_elem_of_nil x). Qed.
503
Lemma elem_of_nil_inv l : ( x, x  l)  l = [].
504
Proof. destruct l. done. by edestruct 1; constructor. Qed.
505
Lemma elem_of_cons l x y : x  y :: l  x = y  x  l.
506
507
Proof.
  split.
508
509
  * inversion 1; subst. by left. by right.
  * intros [?|?]; subst. by left. by right.
510
Qed.
511
Lemma not_elem_of_cons l x y : x  y :: l  x  y  x  l.
Robbert Krebbers's avatar
Robbert Krebbers committed
512
Proof. rewrite elem_of_cons. tauto. Qed.
513
Lemma elem_of_app l1 l2 x : x  l1 ++ l2  x  l1  x  l2.
514
Proof.
515
  induction l1.
516
  * split; [by right|]. intros [Hx|]; [|done]. by destruct (elem_of_nil x).
517
  * simpl. rewrite !elem_of_cons, IHl1. tauto.
518
Qed.
519
Lemma not_elem_of_app l1 l2 x : x  l1 ++ l2  x  l1  x  l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
520
Proof. rewrite elem_of_app. tauto. Qed.
521
Lemma elem_of_list_singleton x y : x  [y]  x = y.
522
Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.
523

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

527
Lemma elem_of_list_split l x : x  l   l1 l2, l = l1 ++ x :: l2.
528
529
530
531
532
Proof.
  induction 1 as [x l|x y l ? [l1 [l2 ?]]].
  * by eexists [], l.
  * subst. by exists (y :: l1) l2.
Qed.
533

534
Lemma elem_of_list_lookup_1 l x : x  l   i, l !! i = Some x.
535
Proof.
536
537
  induction 1 as [|???? IH]; [by exists 0 |].
  destruct IH as [i ?]; auto. by exists (S i).
538
Qed.
539
Lemma elem_of_list_lookup_2 l i x : l !! i = Some x  x  l.
540
541
542
543
Proof.
  revert i. induction l; intros [|i] ?;
    simpl; simplify_equality; constructor; eauto.
Qed.
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
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
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
603

604
(** ** Properties of the [NoDup] predicate *)
605
606
Lemma NoDup_nil : NoDup (@nil A)  True.
Proof. split; constructor. Qed.
607
Lemma NoDup_cons x l : NoDup (x :: l)  x  l  NoDup l.
608
Proof. split. by inversion 1. intros [??]. by constructor. Qed.
609
Lemma NoDup_cons_11 x l : NoDup (x :: l)  x  l.
610
Proof. rewrite NoDup_cons. by intros [??]. Qed.
611
Lemma NoDup_cons_12 x l : NoDup (x :: l)  NoDup l.
612
Proof. rewrite NoDup_cons. by intros [??]. Qed.
613
Lemma NoDup_singleton x : NoDup [x].
614
615
Proof. constructor. apply not_elem_of_nil. constructor. Qed.

616
Lemma NoDup_app l k : NoDup (l ++ k)  NoDup l  ( x, x  l  x  k)  NoDup k.
Robbert Krebbers's avatar
Robbert Krebbers committed
617
Proof.
618
  induction l; simpl.
619
  * rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver.
620
  * rewrite !NoDup_cons.
Robbert Krebbers's avatar
Robbert Krebbers committed
621
    setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
622
623
Qed.

624
Global Instance NoDup_proper: Proper (() ==> iff) (@NoDup A).
625
626
627
628
629
630
631
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
632

633
Lemma NoDup_Permutation l k : NoDup l  NoDup k  ( x, x  l  x  k)  l  k.
634
635
Proof.
  intros Hl. revert k. induction Hl as [|x l Hin ? IH].
636
  * intros k _ Hk. rewrite (elem_of_nil_inv k); [done |].
637
    intros x. rewrite <-Hk, elem_of_nil. intros [].
638
  * intros k Hk Hlk. destruct (elem_of_list_split k x) as [l1 [l2 ?]]; subst.
639
640
    { rewrite <-Hlk. by constructor. }
    rewrite <-Permutation_middle, NoDup_cons in Hk.
641
    destruct Hk as [??]. apply Permutation_cons_app, IH; [done |].
642
    intros y. specialize (Hlk y).
643
    rewrite <-Permutation_middle, !elem_of_cons in Hlk. naive_solver.
644
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
645

646
647
Section no_dup_dec.
  Context `{! x y, Decision (x = y)}.
648

649
650
651
652
  Global Instance NoDup_dec:  l, Decision (NoDup l) :=
    fix NoDup_dec l :=
    match l return Decision (NoDup l) with
    | [] => left NoDup_nil_2
653
    | x :: l =>
654
655
656
657
658
659
660
661
      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
662
    end.
663

664
  Lemma elem_of_remove_dups l x : x  remove_dups l  x  l.
665
666
667
668
669
670
671
672
673
  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.
674
End no_dup_dec.
675

676
(** ** Properties of the [filter] function *)
677
678
679
680
681
682
683
684
685
686
687
688
689
690
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
691

692
(** ** Properties of the [reverse] function *)
693
694
Lemma reverse_nil : reverse [] = @nil A.
Proof. done. Qed.
695
Lemma reverse_singleton x : reverse [x] = [x].
696
Proof. done. Qed.
697
Lemma reverse_cons l x : reverse (x :: l) = reverse l ++ [x].
698
Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
699
Lemma reverse_snoc l x : reverse (l ++ [x]) = x :: reverse l.
700
Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
701
Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
702
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
703
Lemma reverse_length l : length (reverse l) = length l.
704
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
705
Lemma reverse_involutive l : reverse (reverse l) = l.
706
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
707

708
(** ** Properties of the [take] function *)
709
710
711
Definition take_drop := @firstn_skipn A.

Lemma take_nil n : take n (@nil A) = [].
Robbert Krebbers's avatar
Robbert Krebbers committed
712
Proof. by destruct n. Qed.
713
Lemma take_app l k : take (length l) (l ++ k) = l.
Robbert Krebbers's avatar
Robbert Krebbers committed
714
Proof. induction l; simpl; f_equal; auto. Qed.
715
Lemma take_app_alt l k n : n = length l  take n (l ++ k) = l.
Robbert Krebbers's avatar
Robbert Krebbers committed
716
Proof. intros Hn. by rewrite Hn, take_app. Qed.
717
Lemma take_app_le l k n : n  length l  take n (l ++ k) = take n l.
Robbert Krebbers's avatar
Robbert Krebbers committed
718
Proof.
719
  revert n. induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
720
Qed.
721
722
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
723
Proof.
724
  revert n. induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
725
Qed.
726
Lemma take_ge l n : length l  n  take n l = l.
Robbert Krebbers's avatar
Robbert Krebbers committed
727
Proof.
728
  revert n. induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
729
730
Qed.

731
Lemma take_take l n m : take n (take m l) = take (min n m) l.
Robbert Krebbers's avatar
Robbert Krebbers committed
732
Proof. revert n m. induction l; intros [|?] [|?]; simpl; f_equal; auto. Qed.
733
Lemma take_idempotent l n : take n (take n l) = take n l.
Robbert Krebbers's avatar
Robbert Krebbers committed
734
735
Proof. by rewrite take_take, Min.min_idempotent. Qed.

736
Lemma take_length l n : length (take n l) = min n (length l).
Robbert Krebbers's avatar
Robbert Krebbers committed
737
Proof. revert n. induction l; intros [|?]; simpl; f_equal; done. Qed.
738
Lemma take_length_alt l n : n  length l  length (take n l) = n.
Robbert Krebbers's avatar
Robbert Krebbers committed
739
740
Proof. rewrite take_length. apply Min.min_l. Qed.

741
Lemma lookup_take l n i : i < n  take n l !! i = l !! i.
Robbert Krebbers's avatar
Robbert Krebbers committed
742
743
744
745
746
Proof.
  revert n i. induction l; intros [|n] i ?; trivial.
  * auto with lia.
  * destruct i; simpl; auto with arith.
Qed.
747
Lemma lookup_take_ge l n i : n  i  take n l !! i = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
748
Proof. revert n i. induction l; intros [|?] [|?] ?; simpl; auto with lia. Qed.
749
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
750
751
752
753
754
Proof.
  intros. apply list_eq. intros j. destruct (le_lt_dec n j).
  * by rewrite !lookup_take_ge.
  * by rewrite !lookup_take, !list_lookup_alter_ne by lia.
Qed.
755
756
Lemma take_insert l n i x : n  i  take n (<[i:=x]>l) = take n l.
Proof. apply take_alter. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
757

758
(** ** Properties of the [drop] function *)
759
Lemma drop_nil n : drop n (@nil A) = [].
Robbert Krebbers's avatar
Robbert Krebbers committed
760
Proof. by destruct n. Qed.
761
Lemma drop_app l k : drop (length l) (l ++ k) = k.
Robbert Krebbers's avatar
Robbert Krebbers committed
762
Proof. induction l; simpl; f_equal; auto. Qed.
763
Lemma drop_app_alt l k n : n = length l  drop n (l ++ k) = k.
Robbert Krebbers's avatar
Robbert Krebbers committed
764
Proof. intros Hn. by rewrite Hn, drop_app. Qed.
765
766
767
Lemma drop_length l n : length (drop n l) = length l - n.
Proof. revert n. by induction l; intros [|i]; simpl; f_equal. Qed.
Lemma drop_all l : drop (length l) l = [].
Robbert Krebbers's avatar
Robbert Krebbers committed
768
Proof. induction l; simpl; auto. Qed.
769
Lemma drop_all_alt l n : n = length l  drop n l = [].
Robbert Krebbers's avatar
Robbert Krebbers committed
770
771
Proof. intros. subst. by rewrite drop_all. Qed.

772
Lemma lookup_drop l n i : drop n l !! i = l !! (n + i).
Robbert Krebbers's avatar