list.v

(* Copyright (c) 2012-2013, Robbert Krebbers. *)
(* 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. *)
Require Export Permutation.
Require Export numbers base decidable option.

Arguments length {_} _.
Arguments cons {_} _ _.
Arguments app {_} _ _.
Arguments Permutation {_} _ _.
Arguments Forall_cons {_} _ _ _ _ _.

Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.

Arguments take {_} !_ !_ /.
Arguments drop {_} !_ !_ /.

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.

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.

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

(** 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. *)
Instance list_alter {A} (f : A → A) : AlterD nat A (list A) f :=
  fix go (i : nat) (l : list A) {struct l} :=
  match l with
  | [] => []
  | x :: l => match i with 0 => f x :: l | S i => x :: @alter _ _ _ f go i l end
  end.

(** 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.

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

(** The function [option_list o] converts an element [Some x] into the
singleton list [[x]], and [None] into the empty list [[]]. *)
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 =>
    if decide (P x)
    then x :: @filter _ _ (@go) _ _ l
    else @filter _ _ (@go) _ _ l
  end.
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.

(** 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 :=
  match n with 0 => [] | S n => x :: replicate n x end.

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

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

(** 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
  | x :: l => match n with 0 => [] | S n => x :: resize n y l end
  end.
Arguments resize {_} !_ _ !_.

(* 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.

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.

(** 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) :=
  match l with [] => [] | x :: l => f x :: @fmap _ _ _ f go l end.
Instance list_bind {A B} (f : A → list B) : MBindD list f :=
  fix go (l : list A) :=
  match l with [] => [] | x :: l => f x ++ @mbind _ _ _ f go l end.
Instance list_join: MJoin list :=
  fix go A (ls : list (list A)) : list A :=
  match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
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.

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

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 {_ _} _ _ _ _ _.

(** Zipping lists. *)
Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
  fix go l1 l2 :=
  match l1, l2 with x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2 | _ , _ => [] end.
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.

(** 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. *)
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.
Infix "`suffix_of`" := suffix_of (at level 70) : C_scope.
Infix "`prefix_of`" := prefix_of (at level 70) : C_scope.

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 =>
      if decide_rel (=) x1 x2
      then snd_map (x1 ::) (go l1 l2)
      else (x1 :: l1, x2 :: l2, [])
    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.

(** A list [l1] is a sublist of [l2] if [l2] is obtained by removing elements
from [l1] without changing the order. *)
Inductive sublist {A} : relation (list A) :=
  | sublist_nil : sublist [] []
  | sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
  | sublist_cons 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_cons 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.

(** 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 [] []
  | 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.

(** * Basic tactics on lists *)
(** 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. *)
Tactic Notation "discriminate_list_equality" hyp(H) :=
  apply (f_equal length) in H;
  repeat (simpl in H || rewrite app_length in H); exfalso; lia.
Tactic Notation "discriminate_list_equality" :=
  match goal with
  | H : @eq (list _) _ _ |- _ => discriminate_list_equality H
  end.

(** The tactic [simplify_list_equality] simplifies hypotheses involving
equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
lookups in singleton lists. *)
Ltac simplify_list_equality :=
  repeat match goal with
  | _ => progress simplify_equality
  | H : _ ++ _ = _ ++ _ |- _ => first
    [ apply app_inj_tail in H; destruct H
    | apply app_inv_head in H | apply app_inv_tail in H ]
  | H : [?x] !! ?i = Some ?y |- _ =>
    destruct i; [change (Some x = Some y) in H | discriminate]
  end;
  try discriminate_list_equality.
Ltac simplify_list_equality' :=
  repeat (progress simpl in * || simplify_list_equality).

(** * General theorems *)
Section general_properties.
Context {A : Type}.
Implicit Types x y z : A.
Implicit Types l k : list A.

Global Instance: Injective2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed.
Global Instance: ∀ k, Injective (=) (=) (k ++).
Proof. intros ???. apply app_inv_head. Qed.
Global Instance: ∀ k, Injective (=) (=) (++ k).
Proof. intros ???. apply app_inv_tail. Qed.
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.

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.
Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed.

Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
Proof.
  revert l2. induction l1; intros [|??] H.
  * done.
  * discriminate (H 0).
  * discriminate (H 0).
  * f_equal; [by injection (H 0) |]. apply IHl1. intro. apply (H (S _)).
Qed.
Lemma list_eq_nil l : (∀ i, l !! i = None) → l = nil.
Proof. intros. by apply list_eq. Qed.

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

Lemma nil_or_length_pos l : l = [] ∨ length l ≠ 0.
Proof. destruct l; simpl; auto with lia. Qed.
Lemma nil_length l : length l = 0 → l = [].
Proof. by destruct l. Qed.
Lemma lookup_nil i : @nil A !! i = None.
Proof. by destruct i. Qed.
Lemma lookup_tail l i : tail l !! i = l !! S i.
Proof. by destruct l. Qed.

Lemma lookup_lt_Some l i x : l !! i = Some x → i < length l.
Proof.
  revert i. induction l; intros [|?] ?; simplify_equality'; 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 [|?] ?; simplify_equality'; 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 :
  length l2 = length l1 →
  (∀ i x y, l1 !! i = Some x → l2 !! i = Some y → x = y) → l1 = l2.
Proof.
  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.
Qed.

Lemma lookup_app_l l1 l2 i : i < length l1 → (l1 ++ l2) !! i = l1 !! i.
Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
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.

Lemma lookup_app_r l1 l2 i : (l1 ++ l2) !! (length l1 + i) = l2 !! i.
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.
Lemma lookup_app_r_Some l1 l2 i x :
  l2 !! i = Some x → (l1 ++ l2) !! (length l1 + i) = Some x.
Proof. by rewrite lookup_app_r. Qed.
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.

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

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

Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
Lemma list_lookup_alter_ne f l i j : i ≠ j → alter f i l !! j = l !! j.
Proof.
  revert i j. induction l; [done|].
  intros [|i] [|j] ?; try done. apply (IHl i). congruence.
Qed.
Lemma list_lookup_insert l i x : i < length l → <[i:=x]>l !! i = Some x.
Proof.
  intros Hi. unfold insert, list_insert. rewrite list_lookup_alter.
  by destruct (lookup_lt_is_Some_2 l i); simplify_option_equality.
Qed.
Lemma list_lookup_insert_ne l i j x : i ≠ j → <[i:=x]>l !! j = l !! j.
Proof. apply list_lookup_alter_ne. Qed.

Lemma list_lookup_other l i x :
  length l ≠ 1 → l !! i = Some x → ∃ j y, j ≠ i ∧ l !! j = Some y.
Proof.
  intros. destruct i, l as [|x0 [|x1 l]]; simplify_equality'.
  * by exists 1 x1.
  * by exists 0 x0.
Qed.

Lemma alter_app_l f l1 l2 i :
  i < length l1 → alter f i (l1 ++ l2) = alter f i l1 ++ l2.
Proof.
  revert i. induction l1; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma alter_app_r f l1 l2 i :
  alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2.
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.
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply alter_app_r.
Qed.
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.

Lemma insert_app_l l1 l2 i x :
  i < length l1 → <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
Proof. apply alter_app_l. Qed.
Lemma insert_app_r l1 l2 i x : <[length l1+i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2.
Proof. apply alter_app_r. Qed.
Lemma insert_app_r_alt l1 l2 i x :
  length l1 ≤ i → <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
Proof. apply alter_app_r_alt. Qed.

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

(** ** Properties of the [elem_of] predicate *)
Lemma not_elem_of_nil x : x ∉ [].
Proof. by inversion 1. Qed.
Lemma elem_of_nil x : x ∈ [] ↔ False.
Proof. intuition. by destruct (not_elem_of_nil x). Qed.
Lemma elem_of_nil_inv l : (∀ x, x ∉ l) → l = [].
Proof. destruct l. done. by edestruct 1; constructor. Qed.
Lemma elem_of_cons l x y : x ∈ y :: l ↔ x = y ∨ x ∈ l.
Proof.
  split.
  * inversion 1; subst. by left. by right.
  * intros [?|?]; subst. by left. by right.
Qed.
Lemma not_elem_of_cons l x y : x ∉ y :: l ↔ x ≠ y ∧ x ∉ l.
Proof. rewrite elem_of_cons. tauto. Qed.
Lemma elem_of_app l1 l2 x : x ∈ l1 ++ l2 ↔ x ∈ l1 ∨ x ∈ l2.
Proof.
  induction l1.
  * split; [by right|]. intros [Hx|]; [|done]. by destruct (elem_of_nil x).
  * simpl. rewrite !elem_of_cons, IHl1. tauto.
Qed.
Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
Proof. rewrite elem_of_app. tauto. Qed.
Lemma elem_of_list_singleton x y : x ∈ [y] ↔ x = y.
Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.

Global Instance elem_of_list_permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈).
Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.

Lemma elem_of_list_split l x : x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2.
Proof.
  induction 1 as [x l|x y l ? [l1 [l2 ?]]].
  * by eexists [], l.
  * subst. by exists (y :: l1) l2.
Qed.

Lemma elem_of_list_lookup_1 l x : x ∈ l → ∃ i, l !! i = Some x.
Proof.
  induction 1 as [|???? IH]; [by exists 0 |].
  destruct IH as [i ?]; auto. by exists (S i).
Qed.
Lemma elem_of_list_lookup_2 l i x : l !! i = Some x → x ∈ l.
Proof.
  revert i. induction l; intros [|i] ?; simplify_equality'; constructor; eauto.
Qed.
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.

(** ** Properties of the [NoDup] predicate *)
Lemma NoDup_nil : NoDup (@nil A) ↔ True.
Proof. split; constructor. Qed.
Lemma NoDup_cons x l : NoDup (x :: l) ↔ x ∉ l ∧ NoDup l.
Proof. split. by inversion 1. intros [??]. by constructor. Qed.
Lemma NoDup_cons_11 x l : NoDup (x :: l) → x ∉ l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_cons_12 x l : NoDup (x :: l) → NoDup l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_singleton x : NoDup [x].
Proof. constructor. apply not_elem_of_nil. constructor. Qed.

Lemma NoDup_app l k : NoDup (l ++ k) ↔ NoDup l ∧ (∀ x, x ∈ l → x ∉ k) ∧ NoDup k.
Proof.
  induction l; simpl.
  * rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver.
  * rewrite !NoDup_cons.
    setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver.
Qed.
Global Instance NoDup_proper: Proper ((≡ₚ) ==> iff) (@NoDup A).
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.
Lemma NoDup_lookup l i j x :
  NoDup l → l !! i = Some x → l !! j = Some x → i = j.
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.
Lemma NoDup_alt l :
  NoDup l ↔ ∀ i j x, l !! i = Some x → l !! j = Some x → i = j.
Proof.
  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').
Qed.

Section no_dup_dec.
  Context `{!∀ x y, Decision (x = y)}.

  Global Instance NoDup_dec: ∀ l, Decision (NoDup l) :=
    fix NoDup_dec l :=
    match l return Decision (NoDup l) with
    | [] => left NoDup_nil_2
    | x :: l =>
      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
    end.

  Lemma elem_of_remove_dups l x : x ∈ remove_dups l ↔ x ∈ l.
  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.
End no_dup_dec.

(** ** Properties of the [filter] function *)
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.

(** ** Properties of the [find] function *)
Section find.
  Context (P : A → Prop) `{∀ x, Decision (P x)}.

  Lemma list_find_Some l i :
    list_find P l = Some i → ∃ x, l !! i = Some x ∧ P x.
  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.
    intros.
    destruct (list_find_Some (x =) l i) as (?&?&?); auto with congruence.
  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.

(** ** Properties of the [reverse] function *)
Lemma reverse_nil : reverse [] = @nil A.
Proof. done. Qed.
Lemma reverse_singleton x : reverse [x] = [x].
Proof. done. Qed.
Lemma reverse_cons l x : reverse (x :: l) = reverse l ++ [x].
Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
Lemma reverse_snoc l x : reverse (l ++ [x]) = x :: reverse l.
Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
Lemma reverse_length l : length (reverse l) = length l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
Lemma reverse_involutive l : reverse (reverse l) = l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
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.

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

Lemma take_nil n : take n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma take_app l k : take (length l) (l ++ k) = l.
Proof. induction l; simpl; f_equal; auto. Qed.
Lemma take_app_alt l k n : n = length l → take n (l ++ k) = l.
Proof. intros Hn. by rewrite Hn, take_app. Qed.
Lemma take_app_le l k n : n ≤ length l → take n (l ++ k) = take n l.
Proof.
  revert n. induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_app_ge l k n :
  length l ≤ n → take n (l ++ k) = l ++ take (n - length l) k.
Proof.
  revert n. induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_ge l n : length l ≤ n → take n l = l.
Proof.
  revert n. induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.

Lemma take_take l n m : take n (take m l) = take (min n m) l.
Proof. revert n m. induction l; intros [|?] [|?]; simpl; f_equal; auto. Qed.
Lemma take_idempotent l n : take n (take n l) = take n l.
Proof. by rewrite take_take, Min.min_idempotent. Qed.

Lemma take_length l n : length (take n l) = min n (length l).
Proof. revert n. induction l; intros [|?]; simpl; f_equal; done. Qed.
Lemma take_length_le l n : n ≤ length l → length (take n l) = n.
Proof. rewrite take_length. apply Min.min_l. Qed.
Lemma take_length_ge l n : length l ≤ n → length (take n l) = length l.
Proof. rewrite take_length. apply Min.min_r. Qed.

Lemma lookup_take l n i : i < n → take n l !! i = l !! i.
Proof.
  revert n i. induction l; intros [|n] i ?; trivial.
  * auto with lia.
  * destruct i; simpl; auto with arith.
Qed.
Lemma lookup_take_ge l n i : n ≤ i → take n l !! i = None.
Proof. revert n i. induction l; intros [|?] [|?] ?; simpl; auto with lia. Qed.
Lemma take_alter f l n i : n ≤ i → take n (alter f i l) = take n l.
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.
Lemma take_insert l n i x : n ≤ i → take n (<[i:=x]>l) = take n l.
Proof. apply take_alter. Qed.

(** ** Properties of the [drop] function *)
Lemma drop_nil n : drop n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma drop_app l k : drop (length l) (l ++ k) = k.
Proof. induction l; simpl; f_equal; auto. Qed.
Lemma drop_app_alt l k n : n = length l → drop n (l ++ k) = k.
Proof. intros Hn. by rewrite Hn, drop_app. Qed.
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_ge l n : length l ≤ n → drop n l = [].
Proof. revert n. induction l; intros [|??]; simpl in *; auto with lia. Qed.
Lemma drop_all l : drop (length l) l = [].
Proof. by apply drop_ge. Qed.
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.
Lemma lookup_drop l n i : drop n l !! i = l !! (n + i).
Proof. revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
Lemma drop_alter f l n i : i < n → drop n (alter f i l) = drop n l.
Proof.
  intros. apply list_eq. intros j.
  by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
Qed.
Lemma drop_insert l n i x : i < n → drop n (<[i:=x]>l) = drop n l.
Proof. apply drop_alter. Qed.

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

(** ** Properties of the [replicate] function *)
Lemma replicate_length n x : length (replicate n x) = n.
Proof. induction n; simpl; auto. Qed.
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 :
  replicate n x !! i = Some y → y = x ∧ i < n.
Proof. revert i. induction n; intros [|?]; naive_solver auto with lia. Qed.
Lemma lookup_replicate_None n x i : n ≤ i ↔ replicate n x !! i = None.
Proof.
  rewrite eq_None_not_Some, Nat.le_ngt. split.
  * intros Hin [x' Hx']; destruct Hin.
    by destruct (lookup_replicate_inv n x x' i).
  * intros Hx ?. destruct Hx. exists x; auto using lookup_replicate.
Qed.

Lemma elem_of_replicate_inv x n y : x ∈ replicate n y → x = y.
Proof. induction n; simpl; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma replicate_S n x : replicate (S n) x = x :: replicate  n x.
Proof. done. Qed.
Lemma replicate_plus n m x :
  replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; simpl; f_equal; auto. Qed.

Lemma take_replicate n m x : take n (replicate m x) = replicate (min n m) x.
Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma take_replicate_plus n m x : take n (replicate (n + m) x) = replicate n x.
Proof. by rewrite take_replicate, min_l by lia. Qed.
Lemma drop_replicate n m x : drop n (replicate m x) = replicate (m - n) x.
Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma drop_replicate_plus n m x : drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.

Lemma replicate_as_elem_of x n l :
  l = replicate n x ↔ length l = n ∧ ∀ y, y ∈ l → y = x.
Proof.
  split.
  * intros; subst. eauto using elem_of_replicate_inv, replicate_length.
  * intros [? Hl]; subst. induction l as [|y l IH]; simpl; f_equal.
    + apply Hl. by left.
    + apply IH. intros ??. apply Hl. by right.
Qed.
Lemma reverse_replicate n x : reverse (replicate n x) = replicate n x.
Proof.
  apply replicate_as_elem_of. rewrite reverse_length, replicate_length.
  split; auto.
  intros y. rewrite elem_of_reverse. by apply elem_of_replicate_inv.
Qed.

(** ** Properties of the [resize] function *)
Lemma resize_spec l n x : resize n x l = take n l ++ replicate (n - length l) x.
Proof. revert n. induction l; intros [|?]; simpl; f_equal; auto. Qed.
Lemma resize_0 l x : resize 0 x l = [].
Proof. by destruct l. Qed.
Lemma resize_nil n x : resize n x [] = replicate n x.
Proof. rewrite resize_spec. rewrite take_nil. simpl. f_equal. lia. Qed.
Lemma resize_ge l n x :
  length l ≤ n → resize n x l = l ++ replicate (n - length l) x.
Proof. intros. by rewrite resize_spec, take_ge. Qed.
Lemma resize_le l n x : n ≤ length l → resize n x l = take n l.
Proof.
  intros. rewrite resize_spec, (proj2 (Nat.sub_0_le _ _)) by done.
  simpl. by rewrite (right_id_L [] (++)).
Qed.

Lemma resize_all l x : resize (length l) x l = l.
Proof. intros. by rewrite resize_le, take_ge. Qed.
Lemma resize_all_alt l n x : n = length l → resize n x l = l.
Proof. intros. subst. by rewrite resize_all. Qed.

Lemma resize_plus l n m x :
  resize (n + m) x l = resize n x l ++ resize m x (drop n l).
Proof.
  revert n m. induction l; intros [|?] [|?]; simpl; f_equal; auto.
  * by rewrite Nat.add_0_r, (right_id_L [] (++)).
  * by rewrite replicate_plus.
Qed.
Lemma resize_plus_eq l n m x :
  length l = n → resize (n + m) x l = l ++ replicate m x.
Proof.
  intros. subst. by rewrite resize_plus, resize_all, drop_all, resize_nil.
Qed.

Lemma resize_app_le l1 l2 n x :
  n ≤ length l1 → resize n x (l1 ++ l2) = resize n x l1.
Proof.
  intros. by rewrite !resize_le, take_app_le by (rewrite ?app_length; lia).
Qed.
Lemma resize_app_ge l1 l2 n x :
  length l1 ≤ n → resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2.
Proof.
  intros. rewrite !resize_spec, take_app_ge, (associative_L (++)) by done.
  do 2 f_equal. rewrite app_length. lia.
Qed.

Lemma resize_length l n x : length (resize n x l) = n.
Proof. rewrite resize_spec, app_length, replicate_length, take_length. lia. Qed.
Lemma resize_replicate x n m : resize n x (replicate m x) = replicate n x.
Proof. revert m. induction n; intros [|?]; simpl; f_equal; auto. Qed.

Lemma lookup_resize l n x i : i < n → i < length l → resize n x l !! i = l !! i.
Proof.
  intros ??. destruct (decide (n < length l)).
  * by rewrite resize_le, lookup_take by lia.
  * by rewrite resize_ge, lookup_app_l by lia.
Qed.
Lemma lookup_resize_new l n x i :
  length l ≤ i → i < n → resize n x l !! i = Some x.
Proof.
  intros ??. rewrite resize_ge by lia.
  replace i with (length l + (i - length l)) by lia.
  by rewrite lookup_app_r, lookup_replicate by lia.
Qed.
Lemma lookup_resize_old l n x i : n ≤ i → resize n x l !! i = None.
Proof. intros ?. apply lookup_ge_None_2. by rewrite resize_length. Qed.

Lemma resize_resize l n m x : n ≤ m → resize n x (resize m x l) = resize n x l.
Proof.
  revert n m. induction l; simpl.
  * intros. by rewrite !resize_nil, resize_replicate.
  * intros [|?] [|?] ?; simpl; f_equal; auto with lia.
Qed.
Lemma resize_idempotent l n x : resize n x (resize n x l) = resize n x l.
Proof. by rewrite resize_resize. Qed.

Lemma resize_take_le l n m x : n ≤ m → resize n x (take m l) = resize n x l.
Proof.
  revert n m. induction l; intros [|?] [|?] ?; simpl; f_equal; auto with lia.
Qed.
Lemma resize_take_eq l n x : resize n x (take n l) = resize n x l.
Proof. by rewrite resize_take_le. Qed.

Lemma take_resize l n m x : take n (resize m x l) = resize (min n m) x l.
Proof.