list.v 217 KB
Newer Older
1
2
(** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *)
3
From Coq Require Export Permutation.
4
From stdpp Require Export numbers base option.
Ralf Jung's avatar
Ralf Jung committed
5
6
From stdpp Require Import options.

7
(** FIXME: Workaround for https://github.com/coq/coq/issues/14571 *)
8
9
10
11
12
13
(** Remove the instances [Permutation_cons] and [Permutation_app'] since their
priorities are 10, which is above the priority 5 of [proper_relation], and add
them back with the right priority (default = 0, since these instances have no
premises). *)
Global Remove Hints Permutation_cons Permutation_app' : typeclass_instances.
Global Existing Instances Permutation_cons Permutation_app'.
14

15
16
17
Global Arguments length {_} _ : assert.
Global Arguments cons {_} _ _ : assert.
Global Arguments app {_} _ _ : assert.
18

19
20
21
Global Instance: Params (@length) 1 := {}.
Global Instance: Params (@cons) 1 := {}.
Global Instance: Params (@app) 1 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
22

23
24
25
(** [head] and [tail] are defined as [parsing only] for [hd_error] and [tl] in
the Coq standard library. We redefine these notations to make sure they also
pretty print properly. *)
26
Notation head := hd_error.
27
Notation tail := tl.
28

29
30
Notation take := firstn.
Notation drop := skipn.
31

32
33
Global Arguments head {_} _ : assert.
Global Arguments tail {_} _ : assert.
34

35
36
Global Arguments take {_} !_ !_ / : assert.
Global Arguments drop {_} !_ !_ / : assert.
37

38
39
40
41
Global Instance: Params (@head) 1 := {}.
Global Instance: Params (@tail) 1 := {}.
Global Instance: Params (@take) 1 := {}.
Global Instance: Params (@drop) 1 := {}.
42

43
44
Global Arguments Permutation {_} _ _ : assert.
Global Arguments Forall_cons {_} _ _ _ _ _ : assert.
45

46
Notation "(::)" := cons (only parsing) : list_scope.
47
48
Notation "( x ::.)" := (cons x) (only parsing) : list_scope.
Notation "(.:: l )" := (λ x, cons x l) (only parsing) : list_scope.
49
Notation "(++)" := app (only parsing) : list_scope.
50
51
Notation "( l ++.)" := (app l) (only parsing) : list_scope.
Notation "(.++ k )" := (λ l, app l k) (only parsing) : list_scope.
52
53
54

Infix "≡ₚ" := Permutation (at level 70, no associativity) : stdpp_scope.
Notation "(≡ₚ)" := Permutation (only parsing) : stdpp_scope.
55
56
Notation "( x ≡ₚ.)" := (Permutation x) (only parsing) : stdpp_scope.
Notation "(.≡ₚ x )" := (λ y, y  x) (only parsing) : stdpp_scope.
57
58
Notation "(≢ₚ)" := (λ x y, ¬x  y) (only parsing) : stdpp_scope.
Notation "x ≢ₚ y":= (¬x  y) (at level 70, no associativity) : stdpp_scope.
59
60
Notation "( x ≢ₚ.)" := (λ y, x ≢ₚ y) (only parsing) : stdpp_scope.
Notation "(.≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : stdpp_scope.
61

Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
65
Infix "≡ₚ@{ A }" :=
  (@Permutation A) (at level 70, no associativity, only parsing) : stdpp_scope.
Notation "(≡ₚ@{ A } )" := (@Permutation A) (only parsing) : stdpp_scope.

66
Global Instance maybe_cons {A} : Maybe2 (@cons A) := λ l,
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
  match l with x :: l => Some (x,l) | _ => None end.

69
(** * Definitions *)
70
71
72
73
(** Setoid equality lifted to lists *)
Inductive list_equiv `{Equiv A} : Equiv (list A) :=
  | nil_equiv : []  []
  | cons_equiv x y l k : x  y  l  k  x :: l  y :: k.
74
Global Existing Instance list_equiv.
75

76
77
(** The operation [l !! i] gives the [i]th element of the list [l], or [None]
in case [i] is out of bounds. *)
78
Global Instance list_lookup {A} : Lookup nat A (list A) :=
79
  fix go i l {struct l} : option A := let _ : Lookup _ _ _ := @go in
80
  match l with
81
  | [] => None | x :: l => match i with 0 => Some x | S i => l !! i end
82
  end.
83

Dan Frumin's avatar
Dan Frumin committed
84
85
(** The operation [l !!! i] is a total version of the lookup operation
[l !! i]. *)
86
Global Instance list_lookup_total `{!Inhabited A} : LookupTotal nat A (list A) :=
Dan Frumin's avatar
Dan Frumin committed
87
88
89
90
91
92
  fix go i l {struct l} : A := let _ : LookupTotal _ _ _ := @go in
  match l with
  | [] => inhabitant
  | x :: l => match i with 0 => x | S i => l !!! i end
  end.

93
94
(** 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. *)
95
Global Instance list_alter {A} : Alter nat A (list A) := λ f,
96
  fix go i l {struct l} :=
97
98
  match l with
  | [] => []
99
  | x :: l => match i with 0 => f x :: l | S i => x :: go i l end
100
  end.
101

102
103
(** 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. *)
104
Global Instance list_insert {A} : Insert nat A (list A) :=
105
  fix go i y l {struct l} := let _ : Insert _ _ _ := @go in
106
107
108
109
  match l with
  | [] => []
  | x :: l => match i with 0 => y :: l | S i => x :: <[i:=y]>l end
  end.
110
111
112
113
114
Fixpoint list_inserts {A} (i : nat) (k l : list A) : list A :=
  match k with
  | [] => l
  | y :: k => <[i:=y]>(list_inserts (S i) k l)
  end.
115
Global Instance: Params (@list_inserts) 1 := {}.
116

117
118
119
(** 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. *)
120
Global Instance list_delete {A} : Delete nat (list A) :=
121
  fix go (i : nat) (l : list A) {struct l} : list A :=
122
123
  match l with
  | [] => []
124
  | x :: l => match i with 0 => l | S i => x :: @delete _ _ go i l end
125
  end.
126
127
128

(** 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
129
Definition option_list {A} : option A  list A := option_rect _ (λ x, [x]) [].
130
Global Instance: Params (@option_list) 1 := {}.
131
Global Instance maybe_list_singleton {A} : Maybe (λ x : A, [x]) := λ l,
132
  match l with [x] => Some x | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
135

(** The function [filter P l] returns the list of elements of [l] that
satisfies [P]. The order remains unchanged. *)
136
Global Instance list_filter {A} : Filter A (list A) :=
137
  fix go P _ l := let _ : Filter _ _ := @go in
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
  match l with
  | [] => []
140
  | x :: l => if decide (P x) then x :: filter P l else filter P l
141
142
143
144
  end.

(** The function [list_find P l] returns the first index [i] whose element
satisfies the predicate [P]. *)
145
Definition list_find {A} P `{ x, Decision (P x)} : list A  option (nat * A) :=
146
147
  fix go l :=
  match l with
148
149
  | [] => None
  | x :: l => if decide (P x) then Some (0,x) else prod_map S id <$> go l
150
  end.
151
Global Instance: Params (@list_find) 3 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
153
154
155

(** 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 :=
156
  match n with 0 => [] | S n => x :: replicate n x end.
157
Global Instance: Params (@replicate) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
158

159
160
161
162
(** The function [rotate n l] rotates the list [l] by [n], e.g., [rotate 1
[x0; x1; ...; xm]] becomes [x1; ...; xm; x0]. Rotating by a multiple of
[length l] is the identity function. **)
Definition rotate {A} (n : nat) (l : list A) : list A :=
163
  drop (n `mod` length l) l ++ take (n `mod` length l) l.
164
Global Instance: Params (@rotate) 2 := {}.
165
166
167
168
169
170

(** The function [rotate_take s e l] returns the range between the
indices [s] (inclusive) and [e] (exclusive) of [l]. If [e ≤ s], all
elements after [s] and before [e] are returned. *)
Definition rotate_take {A} (s e : nat) (l : list A) : list A :=
  take (rotate_nat_sub s e (length l)) (rotate s l).
171
Global Instance: Params (@rotate_take) 3 := {}.
172

Robbert Krebbers's avatar
Robbert Krebbers committed
173
174
(** The function [reverse l] returns the elements of [l] in reverse order. *)
Definition reverse {A} (l : list A) : list A := rev_append l [].
175
Global Instance: Params (@reverse) 1 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
176

177
178
179
180
(** The function [last l] returns the last element of the list [l], or [None]
if the list [l] is empty. *)
Fixpoint last {A} (l : list A) : option A :=
  match l with [] => None | [x] => Some x | _ :: l => last l end.
181
Global Instance: Params (@last) 1 := {}.
182
Global Arguments last : simpl nomatch.
183

Robbert Krebbers's avatar
Robbert Krebbers committed
184
185
186
187
188
189
(** 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
190
  | x :: l => match n with 0 => [] | S n => x :: resize n y l end
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  end.
192
Global Arguments resize {_} !_ _ !_ : assert.
193
Global Instance: Params (@resize) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
194

195
196
197
(** 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 be
padded with empty lists. In case [l] is too long, it will be truncated. *)
198
199
Fixpoint reshape {A} (szs : list nat) (l : list A) : list (list A) :=
  match szs with
200
  | [] => [] | sz :: szs => take sz l :: reshape szs (drop sz l)
201
  end.
202
Global Instance: Params (@reshape) 2 := {}.
203

204
Definition sublist_lookup {A} (i n : nat) (l : list A) : option (list A) :=
205
206
207
208
  guard (i + n  length l); Some (take n (drop i l)).
Definition sublist_alter {A} (f : list A  list A)
    (i n : nat) (l : list A) : list A :=
  take i l ++ f (take n (drop i l)) ++ drop (i + n) l.
209

210
211
212
213
(** 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 :=
214
  fix go a l := match l with [] => a | x :: l => go (f a x) l end.
215
216

(** The monadic operations. *)
217
218
Global Instance list_ret: MRet list := λ A x, x :: @nil A.
Global Instance list_fmap : FMap list := λ A B f,
219
  fix go (l : list A) := match l with [] => [] | x :: l => f x :: go l end.
220
Global Instance list_omap : OMap list := λ A B f,
221
222
223
224
225
  fix go (l : list A) :=
  match l with
  | [] => []
  | x :: l => match f x with Some y => y :: go l | None => go l end
  end.
226
Global Instance list_bind : MBind list := λ A B f,
227
  fix go (l : list A) := match l with [] => [] | x :: l => f x ++ go l end.
228
Global Instance list_join: MJoin list :=
229
  fix go A (ls : list (list A)) : list A :=
230
  match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
231
Definition mapM `{MBind M, MRet M} {A B} (f : A  M B) : list A  M (list B) :=
232
  fix go l :=
233
  match l with [] => mret [] | x :: l => y  f x; k  go l; mret (y :: k) end.
234

Robbert Krebbers's avatar
Robbert Krebbers committed
235
(** We define stronger variants of the map function that allow the mapped
236
function to use the index of the elements. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
239
240
241
Fixpoint imap {A B} (f : nat  A  B) (l : list A) : list B :=
  match l with
  | [] => []
  | x :: l => f 0 x :: imap (f  S) l
  end.
242

243
Definition zipped_map {A B} (f : list A  list A  A  B) :
Robbert Krebbers's avatar
Robbert Krebbers committed
244
245
246
247
248
    list A  list A  list B := fix go l k :=
  match k with
  | [] => []
  | x :: k => f l k x :: go (x :: l) k
  end.
249

Robbert Krebbers's avatar
Robbert Krebbers committed
250
Fixpoint imap2 {A B C} (f : nat  A  B  C) (l : list A) (k : list B) : list C :=
Robbert Krebbers's avatar
Robbert Krebbers committed
251
  match l, k with
Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
  | [], _ | _, [] => []
  | x :: l, y :: k => f 0 x y :: imap2 (f  S) l k
Robbert Krebbers's avatar
Robbert Krebbers committed
254
255
  end.

256
257
258
259
260
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).
261
262
Global Arguments zipped_Forall_nil {_ _} _ : assert.
Global Arguments zipped_Forall_cons {_ _} _ _ _ _ _ : assert.
263

264
265
266
267
268
269
270
(** The function [mask f βs l] applies the function [f] to elements in [l] at
positions that are [true] in [βs]. *)
Fixpoint mask {A} (f : A  A) (βs : list bool) (l : list A) : list A :=
  match βs, l with
  | β :: βs, x :: l => (if β then f x else x) :: mask f βs l
  | _, _ => l
  end.
271
272
273
274

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

Robbert Krebbers's avatar
Robbert Krebbers committed
280
281
282
283
(** The predicate [suffix] holds if the first list is a suffix of the second.
The predicate [prefix] holds if the first list is a prefix of the second. *)
Definition suffix {A} : relation (list A) := λ l1 l2,  k, l2 = k ++ l1.
Definition prefix {A} : relation (list A) := λ l1 l2,  k, l2 = l1 ++ k.
284
285
Infix "`suffix_of`" := suffix (at level 70) : stdpp_scope.
Infix "`prefix_of`" := prefix (at level 70) : stdpp_scope.
286
287
Global Hint Extern 0 (_ `prefix_of` _) => reflexivity : core.
Global Hint Extern 0 (_ `suffix_of` _) => reflexivity : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
288

289
Section prefix_suffix_ops.
290
291
  Context `{EqDecision A}.

Robbert Krebbers's avatar
Robbert Krebbers committed
292
  Definition max_prefix : list A  list A  list A * list A * list A :=
293
294
295
296
297
    fix go l1 l2 :=
    match l1, l2 with
    | [], l2 => ([], l2, [])
    | l1, [] => (l1, [], [])
    | x1 :: l1, x2 :: l2 =>
298
      if decide_rel (=) x1 x2
299
      then prod_map id (x1 ::.) (go l1 l2) else (x1 :: l1, x2 :: l2, [])
300
    end.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
302
  Definition max_suffix (l1 l2 : list A) : list A * list A * list A :=
    match max_prefix (reverse l1) (reverse l2) with
303
304
    | (k1, k2, k3) => (reverse k1, reverse k2, reverse k3)
    end.
Robbert Krebbers's avatar
Robbert Krebbers committed
305
306
  Definition strip_prefix (l1 l2 : list A) := (max_prefix l1 l2).1.2.
  Definition strip_suffix (l1 l2 : list A) := (max_suffix l1 l2).1.2.
307
End prefix_suffix_ops.
Robbert Krebbers's avatar
Robbert Krebbers committed
308

309
(** A list [l1] is a sublist of [l2] if [l2] is obtained by removing elements
310
311
312
from [l1] without changing the order. *)
Inductive sublist {A} : relation (list A) :=
  | sublist_nil : sublist [] []
313
  | sublist_skip x l1 l2 : sublist l1 l2  sublist (x :: l1) (x :: l2)
314
  | sublist_cons x l1 l2 : sublist l1 l2  sublist l1 (x :: l2).
315
Infix "`sublist_of`" := sublist (at level 70) : stdpp_scope.
316
Global Hint Extern 0 (_ `sublist_of` _) => reflexivity : core.
317

Robbert Krebbers's avatar
Robbert Krebbers committed
318
(** A list [l2] submseteq a list [l1] if [l2] is obtained by removing elements
319
from [l1] while possiblity changing the order. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
320
321
322
323
324
325
Inductive submseteq {A} : relation (list A) :=
  | submseteq_nil : submseteq [] []
  | submseteq_skip x l1 l2 : submseteq l1 l2  submseteq (x :: l1) (x :: l2)
  | submseteq_swap x y l : submseteq (y :: x :: l) (x :: y :: l)
  | submseteq_cons x l1 l2 : submseteq l1 l2  submseteq l1 (x :: l2)
  | submseteq_trans l1 l2 l3 : submseteq l1 l2  submseteq l2 l3  submseteq l1 l3.
326
Infix "⊆+" := submseteq (at level 70) : stdpp_scope.
327
Global Hint Extern 0 (_ + _) => reflexivity : core.
328

329
330
331
332
333
(** Removes [x] from the list [l]. The function returns a [Some] when the
+removal succeeds and [None] when [x] is not in [l]. *)
Fixpoint list_remove `{EqDecision A} (x : A) (l : list A) : option (list A) :=
  match l with
  | [] => None
334
  | y :: l => if decide (x = y) then Some l else (y ::.) <$> list_remove x l
335
336
337
338
339
340
341
342
  end.

(** Removes all elements in the list [k] from the list [l]. The function returns
a [Some] when the removal succeeds and [None] some element of [k] is not in [l]. *)
Fixpoint list_remove_list `{EqDecision A} (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.
343

344
345
346
347
348
Inductive Forall3 {A B C} (P : A  B  C  Prop) :
     list A  list B  list C  Prop :=
  | Forall3_nil : Forall3 P [] [] []
  | Forall3_cons x y z l k k' :
     P x y z  Forall3 P l k k'  Forall3 P (x :: l) (y :: k) (z :: k').
349

350
(** Set operations on lists *)
351
Global Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2,  x, x  l1  x  l2.
352

353
Section list_set.
354
  Context `{dec : EqDecision A}.
Robbert Krebbers's avatar
Robbert Krebbers committed
355
  Global Instance elem_of_list_dec : RelDecision (@{list A}).
Michael Sammler's avatar
Michael Sammler committed
356
  Proof using Type*.
357
   refine (
358
    fix go x l :=
359
360
    match l return Decision (x  l) with
    | [] => right _
361
    | y :: l => cast_if_or (decide (x = y)) (go x l)
362
363
364
365
366
367
368
369
370
371
372
373
374
    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
375
      then list_difference l k else x :: list_difference l k
376
    end.
377
  Definition list_union (l k : list A) : list A := list_difference l k ++ k.
378
379
380
381
382
  Fixpoint list_intersection (l k : list A) : list A :=
    match l with
    | [] => []
    | x :: l =>
      if decide_rel () x k
383
      then x :: list_intersection l k else list_intersection l k
384
385
386
387
388
389
    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,
390
        match f x y with None => id | Some z => (z ::.) end) (go l k) k
391
392
    end.
End list_set.
393

394
395
396
397
(** These next functions allow to efficiently encode lists of positives (bit
strings) into a single positive and go in the other direction as well. This is
for example used for the countable instance of lists and in namespaces.
 The main functions are [positives_flatten] and [positives_unflatten]. *)
398
399
400
401
402
403
Fixpoint positives_flatten_go (xs : list positive) (acc : positive) : positive :=
  match xs with
  | [] => acc
  | x :: xs => positives_flatten_go xs (acc~1~0 ++ Preverse (Pdup x))
  end.

404
405
406
407
408
409
410
(** Flatten a list of positives into a single positive by duplicating the bits
of each element, so that:

- [0 -> 00]
- [1 -> 11]

and then separating each element with [10]. *)
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
Definition positives_flatten (xs : list positive) : positive :=
  positives_flatten_go xs 1.

Fixpoint positives_unflatten_go
        (p : positive)
        (acc_xs : list positive)
        (acc_elm : positive)
  : option (list positive) :=
  match p with
  | 1 => Some acc_xs
  | p'~0~0 => positives_unflatten_go p' acc_xs (acc_elm~0)
  | p'~1~1 => positives_unflatten_go p' acc_xs (acc_elm~1)
  | p'~1~0 => positives_unflatten_go p' (acc_elm :: acc_xs) 1
  | _ => None
  end%positive.

(** Unflatten a positive into a list of positives, assuming the encoding
428
used by [positives_flatten]. *)
429
430
431
Definition positives_unflatten (p : positive) : option (list positive) :=
  positives_unflatten_go p [] 1.

432
(** * Basic tactics on lists *)
Robbert Krebbers's avatar
Robbert Krebbers committed
433
(** The tactic [discriminate_list] discharges a goal if it submseteq
434
435
a list equality involving [(::)] and [(++)] of two lists that have a different
length as one of its hypotheses. *)
436
Tactic Notation "discriminate_list" hyp(H) :=
437
  apply (f_equal length) in H;
438
  repeat (csimpl in H || rewrite app_length in H); exfalso; lia.
439
Tactic Notation "discriminate_list" :=
440
  match goal with H : _ =@{list _} _ |- _ => discriminate_list H end.
441

442
(** The tactic [simplify_list_eq] simplifies hypotheses involving
443
444
equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
lookups in singleton lists. *)
445
Lemma app_inj_1 {A} (l1 k1 l2 k2 : list A) :
446
447
  length l1 = length k1  l1 ++ l2 = k1 ++ k2  l1 = k1  l2 = k2.
Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed.
448
Lemma app_inj_2 {A} (l1 k1 l2 k2 : list A) :
449
450
  length l2 = length k2  l1 ++ l2 = k1 ++ k2  l1 = k1  l2 = k2.
Proof.
451
  intros ? Hl. apply app_inj_1; auto.
452
453
  apply (f_equal length) in Hl. rewrite !app_length in Hl. lia.
Qed.
454
Ltac simplify_list_eq :=
455
  repeat match goal with
456
  | _ => progress simplify_eq/=
457
  | H : _ ++ _ = _ ++ _ |- _ => first
458
    [ apply app_inv_head in H | apply app_inv_tail in H
459
460
    | apply app_inj_1 in H; [destruct H|done]
    | apply app_inj_2 in H; [destruct H|done] ]
Robbert Krebbers's avatar
Robbert Krebbers committed
461
  | H : [?x] !! ?i = Some ?y |- _ =>
462
    destruct i; [change (Some x = Some y) in H | discriminate]
463
  end.
464

465
466
(** * General theorems *)
Section general_properties.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
Context {A : Type}.
468
469
Implicit Types x y z : A.
Implicit Types l k : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
470

471
Global Instance: Inj2 (=) (=) (=) (@cons A).
472
Proof. by injection 1. Qed.
473
Global Instance:  k, Inj (=) (=) (k ++.).
474
Proof. intros ???. apply app_inv_head. Qed.
475
Global Instance:  k, Inj (=) (=) (.++ k).
476
Proof. intros ???. apply app_inv_tail. Qed.
477
Global Instance: Assoc (=) (@app A).
478
479
480
481
482
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.
483

484
Lemma app_nil l1 l2 : l1 ++ l2 = []  l1 = []  l2 = [].
485
Proof. split; [apply app_eq_nil|]. by intros [-> ->]. Qed.
486
487
Lemma app_singleton l1 l2 x :
  l1 ++ l2 = [x]  l1 = []  l2 = [x]  l1 = [x]  l2 = [].
488
Proof. split; [apply app_eq_unit|]. by intros [[-> ->]|[-> ->]]. Qed.
489
490
491
Lemma cons_middle x l1 l2 : l1 ++ x :: l2 = l1 ++ [x] ++ l2.
Proof. done. Qed.
Lemma list_eq l1 l2 : ( i, l1 !! i = l2 !! i)  l1 = l2.
492
Proof.
493
  revert l2. induction l1 as [|x l1 IH]; intros [|y l2] H.
494
495
496
  - done.
  - discriminate (H 0).
  - discriminate (H 0).
497
  - f_equal; [by injection (H 0)|]. apply (IH _ $ λ i, H (S i)).
498
Qed.
499
500
Global Instance list_eq_dec {dec : EqDecision A} : EqDecision (list A) :=
  list_eq_dec dec.
501
502
503
Global Instance list_eq_nil_dec l : Decision (l = []).
Proof. by refine match l with [] => left _ | _ => right _ end. Defined.
Lemma list_singleton_reflect l :
504
  option_reflect (λ x, l = [x]) (length l  1) (maybe (λ x, [x]) l).
505
506
507
508
Proof. by destruct l as [|? []]; constructor. Defined.

Definition nil_length : length (@nil A) = 0 := eq_refl.
Definition cons_length x l : length (x :: l) = S (length l) := eq_refl.
509
Lemma nil_or_length_pos l : l = []  length l  0.
510
Proof. destruct l; simpl; auto with lia. Qed.
511
Lemma nil_length_inv l : length l = 0  l = [].
512
Proof. by destruct l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
513
514
Lemma lookup_cons_ne_0 l x i : i  0  (x :: l) !! i = l !! pred i.
Proof. by destruct i. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
515
516
517
Lemma lookup_total_cons_ne_0 `{!Inhabited A} l x i :
  i  0  (x :: l) !!! i = l !!! pred i.
Proof. by destruct i. Qed.
518
Lemma lookup_nil i : @nil A !! i = None.
519
Proof. by destruct i. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
520
521
Lemma lookup_total_nil `{!Inhabited A} i : @nil A !!! i = inhabitant.
Proof. by destruct i. Qed.
522
Lemma lookup_tail l i : tail l !! i = l !! S i.
523
Proof. by destruct l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
524
525
Lemma lookup_total_tail `{!Inhabited A} l i : tail l !!! i = l !!! S i.
Proof. by destruct l. Qed.
526
Lemma lookup_lt_Some l i x : l !! i = Some x  i < length l.
527
Proof. revert i. induction l; intros [|?] ?; naive_solver auto with arith. Qed.
528
529
530
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).
531
Proof. revert i. induction l; intros [|?] ?; naive_solver eauto with lia. Qed.
532
533
534
535
536
537
538
539
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
540

541
542
543
Lemma list_eq_same_length l1 l2 n :
  length l2 = n  length l1 = n 
  ( i x y, i < n  l1 !! i = Some x  l2 !! i = Some y  x = y)  l1 = l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
544
Proof.
545
  intros <- Hlen Hl; apply list_eq; intros i. destruct (l2 !! i) as [x|] eqn:Hx.
546
  - destruct (lookup_lt_is_Some_2 l1 i) as [y Hy].
547
548
    { rewrite Hlen; eauto using lookup_lt_Some. }
    rewrite Hy; f_equal; apply (Hl i); eauto using lookup_lt_Some.
549
  - by rewrite lookup_ge_None, Hlen, <-lookup_ge_None.
Robbert Krebbers's avatar
Robbert Krebbers committed
550
Qed.
551

552
Lemma nth_lookup l i d : nth i l d = default d (l !! i).
553
554
555
556
Proof. revert i. induction l as [|x l IH]; intros [|i]; simpl; auto. Qed.
Lemma nth_lookup_Some l i d x : l !! i = Some x  nth i l d = x.
Proof. rewrite nth_lookup. by intros ->. Qed.
Lemma nth_lookup_or_length l i d : {l !! i = Some (nth i l d)} + {length l  i}.
Ralf Jung's avatar
Ralf Jung committed
557
Proof.
558
  rewrite nth_lookup. destruct (l !! i) eqn:?; eauto using lookup_ge_None_1.
Ralf Jung's avatar
Ralf Jung committed
559
560
Qed.

Dan Frumin's avatar
Dan Frumin committed
561
562
563
564
565
566
567
568
569
570
571
572
Lemma list_lookup_total_alt `{!Inhabited A} l i :
  l !!! i = default inhabitant (l !! i).
Proof. revert i. induction l; intros []; naive_solver. Qed.
Lemma list_lookup_total_correct `{!Inhabited A} l i x :
  l !! i = Some x  l !!! i = x.
Proof. rewrite list_lookup_total_alt. by intros ->. Qed.
Lemma list_lookup_lookup_total `{!Inhabited A} l i :
  is_Some (l !! i)  l !! i = Some (l !!! i).
Proof. rewrite list_lookup_total_alt; by intros [x ->]. Qed.
Lemma list_lookup_lookup_total_lt `{!Inhabited A} l i :
  i < length l  l !! i = Some (l !!! i).
Proof. intros ?. by apply list_lookup_lookup_total, lookup_lt_is_Some_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
573
574
575
576
577
578
579
Lemma list_lookup_alt `{!Inhabited A} l i x :
  l !! i = Some x  i < length l  l !!! i = x.
Proof.
  naive_solver eauto using list_lookup_lookup_total_lt,
    list_lookup_total_correct, lookup_lt_Some.
Qed.

580
581
582
583
Lemma lookup_app l1 l2 i :
  (l1 ++ l2) !! i =
    match l1 !! i with Some x => Some x | None => l2 !! (i - length l1) end.
Proof. revert i. induction l1 as [|x l1 IH]; intros [|i]; naive_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
584
Lemma lookup_app_l l1 l2 i : i < length l1  (l1 ++ l2) !! i = l1 !! i.
585
Proof. rewrite lookup_app. by intros [? ->]%lookup_lt_is_Some. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
586
587
588
589
Lemma lookup_total_app_l `{!Inhabited A} l1 l2 i :
  i < length l1  (l1 ++ l2) !!! i = l1 !!! i.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_app_l. Qed.
Lemma lookup_app_l_Some l1 l2 i x : l1 !! i = Some x  (l1 ++ l2) !! i = Some x.
590
Proof. rewrite lookup_app. by intros ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
591
592
Lemma lookup_app_r l1 l2 i :
  length l1  i  (l1 ++ l2) !! i = l2 !! (i - length l1).
593
Proof. rewrite lookup_app. by intros ->%lookup_ge_None. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
594
595
596
597
598
599
600
Lemma lookup_total_app_r `{!Inhabited A} l1 l2 i :
  length l1  i  (l1 ++ l2) !!! i = l2 !!! (i - length l1).
Proof. intros. by rewrite !list_lookup_total_alt, lookup_app_r. Qed.
Lemma lookup_app_Some l1 l2 i x :
  (l1 ++ l2) !! i = Some x 
    l1 !! i = Some x  length l1  i  l2 !! (i - length l1) = Some x.
Proof.
601
602
603
  rewrite lookup_app. destruct (l1 !! i) eqn:Hi.
  - apply lookup_lt_Some in Hi. naive_solver lia.
  - apply lookup_ge_None in Hi. naive_solver lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
604
Qed.
605

606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
Lemma lookup_cons x l i :
  (x :: l) !! i =
    match i with 0 => Some x | S i => l !! i end.
Proof. reflexivity. Qed.
Lemma lookup_cons_Some x l i y :
  (x :: l) !! i = Some y 
    (i = 0  x = y)  (1  i  l !! (i - 1) = Some y).
Proof.
  rewrite lookup_cons. destruct i as [|i].
  - naive_solver lia.
  - replace (S i - 1) with i by lia. naive_solver lia.
Qed.

Lemma list_lookup_singleton x i :
  [x] !! i =
    match i with 0 => Some x | S _ => None end.
Proof. reflexivity. Qed.
Lemma list_lookup_singleton_Some x i y :
  [x] !! i = Some y  i = 0  x = y.
Proof. rewrite lookup_cons_Some. naive_solver. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
627
628
629
630
631
632
Lemma list_lookup_middle l1 l2 x n :
  n = length l1  (l1 ++ x :: l2) !! n = Some x.
Proof. intros ->. by induction l1. Qed.
Lemma list_lookup_total_middle `{!Inhabited A} l1 l2 x n :
  n = length l1  (l1 ++ x :: l2) !!! n = x.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_middle. Qed.
Dan Frumin's avatar
Dan Frumin committed
633

634
Lemma list_insert_alter l i x : <[i:=x]>l = alter (λ _, x) i l.
635
Proof. by revert i; induction l; intros []; intros; f_equal/=. Qed.
636
Lemma alter_length f l i : length (alter f i l) = length l.
637
Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
638
Lemma insert_length l i x : length (<[i:=x]>l) = length l.
639
Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
640
Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
641
642
643
644
645
Proof.
  revert i.
  induction l as [|?? IHl]; [done|].
  intros [|i]; [done|]. apply (IHl i).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
646
647
648
649
650
651
Lemma list_lookup_total_alter `{!Inhabited A} f l i :
  i < length l  alter f i l !!! i = f (l !!! i).
Proof.
  intros [x Hx]%lookup_lt_is_Some_2.
  by rewrite !list_lookup_total_alt, list_lookup_alter, Hx.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
652
Lemma list_lookup_alter_ne f l i j : i  j  alter f i l !! j = l !! j.
653
Proof. revert i j. induction l; [done|]. intros [] []; naive_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
654
655
656
657
Lemma list_lookup_total_alter_ne `{!Inhabited A} f l i j :
  i  j  alter f i l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_alter_ne. Qed.

658
Lemma list_lookup_insert l i x : i < length l  <[i:=x]>l !! i = Some x.
659
Proof. revert i. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
660
661
662
Lemma list_lookup_total_insert `{!Inhabited A} l i x :
  i < length l  <[i:=x]>l !!! i = x.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_insert. Qed.
663
Lemma list_lookup_insert_ne l i j x : i  j  <[i:=x]>l !! j = l !! j.
664
Proof. revert i j. induction l; [done|]. intros [] []; naive_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
665
666
667
Lemma list_lookup_total_insert_ne `{!Inhabited A} l i j x :
  i  j  <[i:=x]>l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_insert_ne. Qed.
668
669
670
671
672
673
Lemma list_lookup_insert_Some l i x j y :
  <[i:=x]>l !! j = Some y 
    i = j  x = y  j < length l  i  j  l !! j = Some y.
Proof.
  destruct (decide (i = j)) as [->|];
    [split|rewrite list_lookup_insert_ne by done; tauto].
674
  - intros Hy. assert (j < length l).
675
676
    { rewrite <-(insert_length l j x); eauto using lookup_lt_Some. }
    rewrite list_lookup_insert in Hy by done; naive_solver.
677
  - intros [(?&?&?)|[??]]; rewrite ?list_lookup_insert; naive_solver.
678
679
680
Qed.
Lemma list_insert_commute l i j x y :
  i  j  <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
681
Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed.
Michael Sammler's avatar
Michael Sammler committed
682
683
Lemma list_insert_id' l i x : (i < length l  l !! i = Some x)  <[i:=x]>l = l.
Proof. revert i. induction l; intros [|i] ?; f_equal/=; naive_solver lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
684
Lemma list_insert_id l i x : l !! i = Some x  <[i:=x]>l = l.
Michael Sammler's avatar
Michael Sammler committed
685
Proof. intros ?. by apply list_insert_id'. Qed.
686
687
Lemma list_insert_ge l i x : length l  i  <[i:=x]>l = l.
Proof. revert i. induction l; intros [|i] ?; f_equal/=; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
688
Lemma list_insert_insert l i x y : <[i:=x]> (<[i:=y]> l) = <[i:=x]> l.
Michael Sammler's avatar
Michael Sammler committed
689
Proof. revert i. induction l; intros [|i]; f_equal/=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
690

691
692
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
693
Proof.
694
  intros. destruct i, l as [|x0 [|x1 l]]; simplify_eq/=.
695
696
  - by exists 1, x1.
  - by exists 0, x0.
Robbert Krebbers's avatar
Robbert Krebbers committed
697
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
698

699
700
Lemma alter_app_l f l1 l2 i :
  i < length l1  alter f i (l1 ++ l2) </