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 n j).
  * by rewrite !lookup_take_ge.
  * by rewrite !lookup_take, !list_lookup_alter_ne by lia.
Qed.
836 837
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
838

839
(** ** Properties of the [drop] function *)
840
Lemma drop_nil n : drop n (@nil A) = [].
Robbert Krebbers's avatar
Robbert Krebbers committed
841
Proof. by destruct n. Qed.
842
Lemma drop_app l k : drop (length l) (l ++ k) = k.
Robbert Krebbers's avatar
Robbert Krebbers committed
843
Proof. induction l; simpl; f_equal; auto. Qed.
844
Lemma drop_app_alt l k n : n = length l  drop n (l ++ k) = k.
Robbert Krebbers's avatar
Robbert Krebbers committed
845
Proof. intros Hn. by rewrite Hn, drop_app. Qed.
846 847
Lemma drop_length l n : length (drop n l) = length l - n.
Proof. revert n. by induction l; intros [|i]; simpl; f_equal. Qed.
848 849
Lemma drop_ge l n : length l  n  drop n l = [].
Proof. revert n. induction l; intros [|??]; simpl in *; auto with lia. Qed.
850
Lemma drop_all l : drop (length l) l = [].
851
Proof. by apply drop_ge. Qed.
852 853
Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l.
Proof. revert n2. induction l; intros [|?]; simpl; rewrite ?drop_nil; auto. Qed.
854
Lemma lookup_drop l n i : drop n l !! i = l !! (n + i).