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 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398
Lemma lookup_lt_Some l i x : l !! i = Some x  i < length l.
Proof.
  revert i. induction l; intros [|?] ?;
    simpl in *; simplify_equality; simpl; auto with arith.
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.
  revert i. induction l; intros [|?] ?;
    simpl in *; simplify_equality; simpl; eauto with lia.
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
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
Proof.
402 403 404 405 406
  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
407 408
Qed.

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

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

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

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

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

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

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

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

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

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

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

532
Lemma elem_of_list_lookup_1 l x : x  l   i, l !! i = Some x.
533
Proof.
534 535
  induction 1 as [|???? IH]; [by exists 0 |].
  destruct IH as [i ?]; auto. by exists (S i).
536
Qed.
537
Lemma elem_of_list_lookup_2 l i x : l !! i = Some x  x  l.
538 539 540 541
Proof.
  revert i. induction l; intros [|i] ?;
    simpl; simplify_equality; constructor; eauto.
Qed.
542 543 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
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
601

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

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

622
Global Instance NoDup_proper: Proper (() ==> iff) (@NoDup A).
623 624 625 626 627 628 629
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
630

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

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

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

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

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

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

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

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

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

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

739
Lemma lookup_take l n i : i < n  take n l !! i = l !! i.
Robbert Krebbers's avatar
Robbert Krebbers committed
740 741 742 743 744
Proof.
  revert n i. induction l; intros [|n] i ?; trivial.
  * auto with lia.
  * destruct i; simpl; auto with arith.
Qed.
745
Lemma lookup_take_ge l n i : n  i  take n l !! i = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
746
Proof. revert n i. induction l; intros [|?] [|?] ?; simpl; auto with lia. Qed.
747
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
748 749 750 751 752
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.
753 754
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
755

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

770
Lemma lookup_drop l n i : drop n l !! i = l !! (n + i).
Robbert Krebbers's avatar
Robbert Krebbers committed
771
Proof. revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
772
Lemma drop_alter f l n i : i < n  drop n (alter f i l) = drop n l.
Robbert Krebbers's avatar
Robbert Krebbers committed
773 774 775 776
Proof.
  intros. apply list_eq. intros j.
  by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
Qed.
777 778
Lemma drop_insert l n i x : i < n  drop n (<[i:=x]>l) = drop n l.
Proof. apply drop_alter. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
779

780
Lemma delete_take_drop l i : delete i l = take i l ++ drop (S i) l.
781 782 783
Proof. revert i. induction l; intros [|?]; simpl; auto using f_equal. Qed.

(** ** Properties of the [replicate] function *)
784
Lemma replicate_length n x : length (replicate n x) = n.
785
Proof. induction n; simpl; auto. Qed.
786 787 788
Lemma lookup_replicate n x i : i < n  replicate n x !! i = Some x.
Proof. revert i. induction n; intros [|?]; naive_solver auto with lia. Qed.
Lemma lookup_replicate_inv n x y i :
789
  replicate n x !! i = Some y  y = x  i < n.
790 791
Proof. revert i. induction n; intros [|?]; naive_solver auto with lia. Qed.
Lemma replicate_S n x : replicate (S n) x = x :: replicate  n x.
792
Proof. done. Qed.
793
Lemma replicate_plus n m x :
Robbert Krebbers's avatar
Robbert Krebbers committed
794 795 796
  replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; simpl; f_equal; auto. Qed.

797
Lemma take_replicate n m x : take n (replicate m x) = replicate (min n m) x.
Robbert Krebbers's avatar
Robbert Krebbers committed
798
Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
799
Lemma take_replicate_plus n m x : take n (replicate (n + m) x) = replicate n x.
Robbert Krebbers's avatar
Robbert Krebbers committed
800
Proof. by rewrite take_replicate, min_l by lia. Qed.
801
Lemma drop_replicate n m x : drop n (replicate m x) = replicate (m - n) x.
Robbert Krebbers's avatar
Robbert Krebbers committed
802
Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
803
Lemma drop_replicate_plus n m x : drop n (replicate (n + m) x) = replicate m x.
Robbert Krebbers's avatar
Robbert Krebbers committed
804 805
Proof. rewrite drop_replicate. f_equal. lia. Qed.

806
Lemma reverse_replicate n x : reverse (replicate n x) = replicate n x.
807
Proof.
808 809
  induction n as [|n IH