Module list

This file collects general purpose definitions and theorems on lists that are not in the Coq standard library.
Require Import Permutation.
Require Export base decidable option numbers.

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

Notation Forall_nil_2 := Forall_nil.
Notation Forall_cons_2 := Forall_cons.

Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.
Notation take_drop := firstn_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.

General definitions

Looking up, updating, and deleting elements of a list.
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.
Instance list_alter {A} (f : AA) : 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.
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.
Instance list_insert {A} : Insert nat A (list A) := λ i x,
  alter_, x) i.

The function option_list converts an element of the option type into a list.
Definition option_list {A} : option Alist 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.

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

The function resize n y l takes the first n elements of l in case length ln, 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 predicate prefix_of holds if the first list is a prefix of the second. The predicate suffix_of holds if the first list is a suffix of the second.
Definition prefix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = l1 ++ k.
Definition suffix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = k ++ l1.

Tactics on lists

Lemma cons_inv {A} (l1 l2 : list A) x1 x2 :
  x1 :: l1 = x2 :: l2x1 = x2l1 = l2.
Proof. by injection 1. Qed.

The tactic discriminate_list_equality discharges goals containing invalid list equalities as an assumption.
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" :=
  repeat_on_hyps (fun H => discriminate_list_equality H).

The tactic simplify_list_equality simplifies assumptions involving equalities on lists.
Ltac simplify_list_equality := repeat
  match goal with
  | H : _ :: _ = _ :: _ |- _ =>
     apply cons_inv in H; destruct H
  | 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]
  | _ => progress simplify_equality
  | H : _ |- _ => discriminate_list_equality H
  end.

General theorems

Section general_properties.
Context {A : Type}.

Global Instance: ∀ x : A, Injective (=) (=) (x ::).
Proof. by injection 1. Qed.
Global Instance: ∀ l : list A, Injective (=) (=) (:: l).
Proof. by injection 1. Qed.
Global Instance: ∀ k : list A, Injective (=) (=) (k ++).
Proof. intros ???. apply app_inv_head. Qed.
Global Instance: ∀ k : list A, Injective (=) (=) (++ k).
Proof. intros ???. apply app_inv_tail. Qed.

Lemma app_inj (l1 k1 l2 k2 : list A) :
  length l1 = length k1
  l1 ++ l2 = k1 ++ k2l1 = k1l2 = k2.
Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed.

Lemma list_eq (l1 l2 : list A) : (∀ 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 : list A) : (∀ i, l !! i = None) → l = nil.
Proof. intros. by apply list_eq. Qed.

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


Lemma nil_or_length_pos (l : list A) : l = [] ∨ length l ≠ 0.
Proof. destruct l; simpl; auto with lia. Qed.
Lemma nil_length (l : list A) : 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 : list A) i : tail l !! i = l !! S i.
Proof. by destruct l. Qed.

Lemma lookup_lt_length (l : list A) i :
  is_Some (l !! i) ↔ i < length l.
Proof.
  revert i. induction l.
  * split; by inversion 1.
  * intros [|?]; simpl.
    + split; eauto with arith.
    + by rewrite <-NPeano.Nat.succ_lt_mono.
Qed.

Lemma lookup_lt_length_1 (l : list A) i :
  is_Some (l !! i) → i < length l.
Proof. apply lookup_lt_length. Qed.
Lemma lookup_lt_length_alt (l : list A) i x :
  l !! i = Some xi < length l.
Proof. intros Hl. by rewrite <-lookup_lt_length, Hl. Qed.
Lemma lookup_lt_length_2 (l : list A) i :
  i < length lis_Some (l !! i).
Proof. apply lookup_lt_length. Qed.

Lemma lookup_ge_length (l : list A) i :
  l !! i = Nonelength li.
Proof. rewrite eq_None_not_Some, lookup_lt_length. lia. Qed.
Lemma lookup_ge_length_1 (l : list A) i :
  l !! i = Nonelength li.
Proof. by rewrite lookup_ge_length. Qed.
Lemma lookup_ge_length_2 (l : list A) i :
  length lil !! i = None.
Proof. by rewrite lookup_ge_length. Qed.

Lemma list_eq_length_eq (l1 l2 : list A) :
  length l2 = length l1
  (∀ i x y, l1 !! i = Some xl2 !! i = Some yx = y) →
  l1 = l2.
Proof.
  intros Hlength Hlookup. apply list_eq. intros i.
  destruct (l2 !! i) as [x|] eqn:E.
  * feed inversion (lookup_lt_length_2 l1 i) as [y].
    { pose proof (lookup_lt_length_alt l2 i x E). lia. }
    f_equal. eauto.
  * rewrite lookup_ge_length in E |- *. lia.
Qed.


Lemma lookup_app_l (l1 l2 : list A) 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 : list A) i x :
  l1 !! i = Some x
  (l1 ++ l2) !! i = Some x.
Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_length_alt. Qed.

Lemma lookup_app_r (l1 l2 : list A) i :
  (l1 ++ l2) !! (length l1 + i) = l2 !! i.
Proof.
  revert i.
  induction l1; intros [|i]; simpl in *; simplify_equality; auto.
Qed.

Lemma lookup_app_r_alt (l1 l2 : list A) i :
  length l1i
  (l1 ++ l2) !! i = l2 !! (i - length l1).
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply lookup_app_r.
Qed.

Lemma lookup_app_r_Some (l1 l2 : list A) i x :
  l2 !! i = Some x
  (l1 ++ l2) !! (length l1 + i) = Some x.
Proof. by rewrite lookup_app_r. Qed.
Lemma lookup_app_r_Some_alt (l1 l2 : list A) i x :
  length l1i
  l2 !! (i - length l1) = Some x
  (l1 ++ l2) !! i = Some x.
Proof. intro. by rewrite lookup_app_r_alt. Qed.

Lemma lookup_app_inv (l1 l2 : list A) i x :
  (l1 ++ l2) !! i = Some x
  l1 !! i = Some xl2 !! (i - length l1) = Some x.
Proof.
  revert i.
  induction l1; intros [|i] ?; simpl in *; simplify_equality; auto.
Qed.


Lemma list_lookup_middle (l1 l2 : list A) (x : A) :
  (l1 ++ x :: l2) !! length l1 = Some x.
Proof. by induction l1; simpl. Qed.

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

Lemma list_lookup_alter (f : AA) 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 : AA) l i j :
  ijalter 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 : list A) i x :
  i < length l
  <[i:=x]>l !! i = Some x.
Proof.
  intros Hi. unfold insert, list_insert.
  rewrite list_lookup_alter.
  by feed inversion (lookup_lt_length_2 l i).
Qed.

Lemma list_lookup_insert_ne (l : list A) i j x :
  ij → <[i:=x]>l !! j = l !! j.
Proof. apply list_lookup_alter_ne. Qed.

Lemma list_lookup_other (l : list A) i x :
  length l ≠ 1 →
  l !! i = Some x
  ∃ j y, jil !! j = Some y.
Proof.
  intros Hl Hi.
  destruct i; destruct l as [|x0 [|x1 l]]; simpl in *; simplify_equality.
  * by exists 1 x1.
  * by exists 0 x0.
Qed.


Lemma alter_app_l (f : AA) (l1 l2 : list A) 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 : AA) (l1 l2 : list A) 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 : AA) (l1 l2 : list A) i :
  length l1i
  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 insert_app_l (l1 l2 : list A) 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 : list A) 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 : list A) i x :
  length l1i
  <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
Proof. apply alter_app_r_alt. Qed.

Lemma insert_consecutive_length (l : list A) i k :
  length (insert_consecutive i k l) = length l.
Proof. revert i. by induction k; intros; simpl; rewrite ?insert_length. Qed.

Lemma not_elem_of_nil (x : A) : x ∉ [].
Proof. by inversion 1. Qed.
Lemma elem_of_nil (x : A) : x ∈ [] ↔ False.
Proof. intuition. by destruct (not_elem_of_nil x). Qed.
Lemma elem_of_nil_inv (l : list A) : (∀ x, xl) → l = [].
Proof. destruct l. done. by edestruct 1; constructor. Qed.
Lemma elem_of_cons (l : list A) x y :
  xy :: lx = yxl.
Proof.
  split.
  * inversion 1; subst. by left. by right.
  * intros [?|?]; subst. by left. by right.
Qed.

Lemma not_elem_of_cons (l : list A) x y :
  xy :: lxyxl.
Proof. rewrite elem_of_cons. tauto. Qed.
Lemma elem_of_app (l1 l2 : list A) x :
  xl1 ++ l2xl1xl2.
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 : list A) x :
  xl1 ++ l2xl1xl2.
Proof. rewrite elem_of_app. tauto. Qed.

Lemma elem_of_list_singleton (x y : A) : x ∈ [y] ↔ x = y.
Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.

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

Lemma elem_of_list_split (l : list A) x :
  xl → ∃ 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.


Global Instance elem_of_list_dec {dec : ∀ x y : A, Decision (x = y)} :
  ∀ (x : A) l, Decision (xl).
Proof.
 intros x. refine (
  fix go l :=
  match l return Decision (xl) with
  | [] => right (not_elem_of_nil _)
  | y :: l => cast_if_or (decide_rel (=) x y) (go l)
  end); clear go dec; subst; try (by constructor); by inversion 1.
Defined.


Lemma elem_of_list_lookup_1 (l : list A) x :
  xl → ∃ 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 : list A) i x :
  l !! i = Some xxl.
Proof.
  revert i. induction l; intros [|i] ?;
    simpl; simplify_equality; constructor; eauto.
Qed.

Lemma elem_of_list_lookup (l : list A) x :
  xl ↔ ∃ i, l !! i = Some x.
Proof.
  firstorder eauto using
    elem_of_list_lookup_1, elem_of_list_lookup_2.
Qed.


Lemma NoDup_nil : NoDup (@nil A) ↔ True.
Proof. split; constructor. Qed.
Lemma NoDup_cons (x : A) l : NoDup (x :: l) ↔ xlNoDup l.
Proof. split. by inversion 1. intros [??]. by constructor. Qed.
Lemma NoDup_cons_11 (x : A) l : NoDup (x :: l) → xl.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_cons_12 (x : A) l : NoDup (x :: l) → NoDup l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_singleton (x : A) : NoDup [x].
Proof. constructor. apply not_elem_of_nil. constructor. Qed.

Lemma NoDup_app (l k : list A) :
  NoDup (l ++ k) ↔ NoDup l ∧ (∀ x, xlxk) ∧ 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 (Permutation ==> 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_Permutation (l k : list A) :
  NoDup lNoDup k → (∀ x, xlxk) → Permutation l k.
Proof.
  intros Hl. revert k. induction Hl as [|x l Hin ? IH].
  * intros k _ Hk.
    rewrite (elem_of_nil_inv k); [done |].
    intros x. rewrite <-Hk, elem_of_nil. intros [].
  * intros k Hk Hlk.
    destruct (elem_of_list_split k x) as [l1 [l2 ?]]; subst.
    { rewrite <-Hlk. by constructor. }
    rewrite <-Permutation_middle, NoDup_cons in Hk.
    destruct Hk as [??].
    apply Permutation_cons_app, IH; [done |].
    intros y. specialize (Hlk y).
    rewrite <-Permutation_middle, !elem_of_cons in Hlk.
    naive_solver.
Qed.


Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} :
    ∀ (l : list A), 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 => rightH, NoDup_cons_11 _ _ H Hin)
    | right Hin =>
      match NoDup_dec l with
      | left H => left (NoDup_cons_2 _ _ Hin H)
      | right H => right (HNoDup_cons_12 _ _)
      end
    end
  end.

Section remove_dups.
  Context `{!∀ x y : A, Decision (x = y)}.

  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.

  Lemma elem_of_remove_dups l x :
    xremove_dups lxl.
  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 remove_dups.

Lemma elem_of_list_filter `{∀ x : A, Decision (P x)} l x :
  xfilter P lP xxl.
Proof.
  unfold filter. induction l; simpl; repeat case_decide;
     rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
Qed.

Lemma filter_nodup P `{∀ x : A, Decision (P x)} l :
  NoDup lNoDup (filter P l).
Proof.
  unfold filter. induction 1; simpl; repeat case_decide;
    rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
Qed.


Lemma reverse_nil : reverse [] = @nil A.
Proof. done. Qed.
Lemma reverse_cons (l : list A) x : reverse (x :: l) = reverse l ++ [x].
Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
Lemma reverse_snoc (l : list A) x : reverse (l ++ [x]) = x :: reverse l.
Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
Lemma reverse_app (l1 l2 : list A) :
  reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
Lemma reverse_length (l : list A) : length (reverse l) = length l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
Lemma reverse_involutive (l : list A) : reverse (reverse l) = l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.

Lemma take_nil n :
  take n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma take_app (l k : list A) :
  take (length l) (l ++ k) = l.
Proof. induction l; simpl; f_equal; auto. Qed.
Lemma take_app_alt (l k : list A) n :
  n = length l
  take n (l ++ k) = l.
Proof. intros Hn. by rewrite Hn, take_app. Qed.
Lemma take_app_le (l k : list A) n :
  nlength 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 : list A) n :
  length ln
  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 : list A) n :
  length ln
  take n l = l.
Proof.
  revert n.
  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.


Lemma take_take (l : list A) 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 : list A) n :
  take n (take n l) = take n l.
Proof. by rewrite take_take, Min.min_idempotent. Qed.

Lemma take_length (l : list A) n :
  length (take n l) = min n (length l).
Proof. revert n. induction l; intros [|?]; simpl; f_equal; done. Qed.
Lemma take_length_alt (l : list A) n :
  nlength l
  length (take n l) = n.
Proof. rewrite take_length. apply Min.min_l. Qed.

Lemma lookup_take (l : list A) n i :
  i < ntake 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 : list A) n i :
  nitake n l !! i = None.
Proof.
  revert n i.
  induction l; intros [|?] [|?] ?; simpl; auto with lia.
Qed.

Lemma take_alter (f : AA) l n i :
  nitake 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 : list A) n i x :
  nitake n (<[i:=x]>l) = take n l.
Proof take_alter _ _ _ _.

Lemma drop_nil n :
  drop n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma drop_app (l k : list A) :
  drop (length l) (l ++ k) = k.
Proof. induction l; simpl; f_equal; auto. Qed.
Lemma drop_app_alt (l k : list A) n :
  n = length l
  drop n (l ++ k) = k.
Proof. intros Hn. by rewrite Hn, drop_app. Qed.
Lemma drop_length (l : list A) n :
  length (drop n l) = length l - n.
Proof.
  revert n. by induction l; intros [|i]; simpl; f_equal.
Qed.

Lemma drop_all (l : list A) :
  drop (length l) l = [].
Proof. induction l; simpl; auto. Qed.
Lemma drop_all_alt (l : list A) n :
  n = length l
  drop n l = [].
Proof. intros. subst. by rewrite drop_all. Qed.

Lemma lookup_drop (l : list A) n i :
  drop n l !! i = l !! (n + i).
Proof. revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
Lemma drop_alter (f : AA) l n i :
  i < ndrop 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 : list A) n i x :
  i < ndrop n (<[i:=x]>l) = drop n l.
Proof drop_alter _ _ _ _.

Lemma replicate_length n (x : A) : length (replicate n x) = n.
Proof. induction n; simpl; auto. Qed.
Lemma lookup_replicate n (x : A) 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 : A) i :
  replicate n x !! i = Some yy = xi < n.
Proof.
  revert i.
  induction n; intros [|?]; naive_solver auto with lia.
Qed.

Lemma replicate_plus n m (x : A) :
  replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; simpl; f_equal; auto. Qed.

Lemma take_replicate n m (x : A) :
  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 : A) :
  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 : A) :
  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 : A) :
  drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.

Lemma resize_spec (l : list A) 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 : list A) x :
  resize 0 x l = [].
Proof. by destruct l. Qed.
Lemma resize_nil n (x : A) :
  resize n x [] = replicate n x.
Proof. rewrite resize_spec. rewrite take_nil. simpl. f_equal. lia. Qed.
Lemma resize_ge (l : list A) n x :
  length ln
  resize n x l = l ++ replicate (n - length l) x.
Proof. intros. by rewrite resize_spec, take_ge. Qed.
Lemma resize_le (l : list A) n x :
  nlength l
  resize n x l = take n l.
Proof.
  intros. rewrite resize_spec, (proj2 (NPeano.Nat.sub_0_le _ _)) by done.
  simpl. by rewrite app_nil_r.
Qed.


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

Lemma resize_plus (l : list A) 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 plus_0_r, app_nil_r.
  * by rewrite replicate_plus.
Qed.

Lemma resize_plus_eq (l : list A) 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 : list A) n x :
  nlength 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 : list A) n x :
  length l1n
  resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2.
Proof.
  intros.
  rewrite !resize_spec, take_app_ge, app_assoc by done.
  do 2 f_equal. rewrite app_length. lia.
Qed.


Lemma resize_length (l : list A) n x : length (resize n x l) = n.
Proof.
  rewrite resize_spec, app_length, replicate_length, take_length. lia.
Qed.

Lemma resize_replicate (x : A) n m :
  resize n x (replicate m x) = replicate n x.
Proof. revert m. induction n; intros [|?]; simpl; f_equal; auto. Qed.

Lemma resize_resize (l : list A) n m x :
  nm
  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 : list A) n x :
  resize n x (resize n x l) = resize n x l.
Proof. by rewrite resize_resize. Qed.

Lemma resize_take_le (l : list A) n m x :
  nm
  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 : list A) n x :
  resize n x (take n l) = resize n x l.
Proof. by rewrite resize_take_le. Qed.

Lemma take_resize (l : list A) n m x :
  take n (resize m x l) = resize (min n m) x l.
Proof.
  revert n m.
  induction l; intros [|?] [|?]; simpl; f_equal; auto using take_replicate.
Qed.

Lemma take_resize_le (l : list A) n m x :
  nm
  take n (resize m x l) = resize n x l.
Proof. intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_resize_eq (l : list A) n x :
  take n (resize n x l) = resize n x l.
Proof. intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_length_resize (l : list A) n x :
  length ln
  take (length l) (resize n x l) = l.
Proof. intros. by rewrite take_resize_le, resize_all. Qed.
Lemma take_length_resize_alt (l : list A) n m x :
  m = length l
  mn
  take m (resize n x l) = l.
Proof. intros. subst. by apply take_length_resize. Qed.
Lemma take_resize_plus (l : list A) n m x :
  take n (resize (n + m) x l) = resize n x l.
Proof. by rewrite take_resize, min_l by lia. Qed.

Lemma drop_resize_le (l : list A) n m x :
  nm
  drop n (resize m x l) = resize (m - n) x (drop n l).
Proof.
  revert n m. induction l; simpl.
  * intros. by rewrite drop_nil, !resize_nil, drop_replicate.
  * intros [|?] [|?] ?; simpl; try case_match; auto with lia.
Qed.

Lemma drop_resize_plus (l : list A) n m x :
  drop n (resize (n + m) x l) = resize m x (drop n l).
Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.

Section Forall_Exists.
  Context (P : AProp).

  Lemma Forall_forall l :
    Forall P l ↔ ∀ x, xlP x.
  Proof.
    split.
    * induction 1; inversion 1; subst; auto.
    * intros Hin. induction l; constructor.
      + apply Hin. constructor.
      + apply IHl. intros ??. apply Hin. by constructor.
  Qed.


  Lemma Forall_nil : Forall P [] ↔ True.
  Proof. done. Qed.
  Lemma Forall_cons_1 x l : Forall P (x :: l) → P xForall P l.
  Proof. by inversion 1. Qed.
  Lemma Forall_cons x l : Forall P (x :: l) ↔ P xForall P l.
  Proof. split. by inversion 1. intros [??]. by constructor. Qed.
  Lemma Forall_singleton x : Forall P [x] ↔ P x.
  Proof. rewrite Forall_cons, Forall_nil; tauto. Qed.
  Lemma Forall_app l1 l2 : Forall P (l1 ++ l2) ↔ Forall P l1Forall P l2.
  Proof.
    split.
    * induction l1; inversion 1; intuition.
    * intros [H ?]. induction H; simpl; intuition.
  Qed.

  Lemma Forall_true l : (∀ x, P x) → Forall P l.
  Proof. induction l; auto. Qed.
  Lemma Forall_impl l (Q : AProp) :
    Forall P l → (∀ x, P xQ x) → Forall Q l.
  Proof. intros H ?. induction H; auto. Defined.

  Lemma Forall_delete l i : Forall P lForall P (delete i l).
  Proof.
    intros H. revert i.
    by induction H; intros [|i]; try constructor.
  Qed.

  Lemma Forall_lookup l :
    Forall P l ↔ ∀ i x, l !! i = Some xP x.
  Proof.
    rewrite Forall_forall.
    setoid_rewrite elem_of_list_lookup.
    naive_solver.
  Qed.

  Lemma Forall_lookup_1 l i x :
    Forall P ll !! i = Some xP x.
  Proof. rewrite Forall_lookup. eauto. Qed.
  Lemma Forall_alter f l i :
    Forall P l
    (∀ x, l !! i = Some xP xP (f x)) →
    Forall P (alter f i l).
  Proof.
    intros Hl. revert i.
    induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.


  Lemma Forall_replicate n x :
    P xForall P (replicate n x).
  Proof. induction n; simpl; constructor; auto. Qed.
  Lemma Forall_replicate_eq n (x : A) :
    Forall (=x) (replicate n x).
  Proof. induction n; simpl; constructor; auto. Qed.

  Lemma Exists_exists l :
    Exists P l ↔ ∃ x, xlP x.
  Proof.
    split.
    * induction 1 as [x|y ?? IH].
      + exists x. split. constructor. done.
      + destruct IH as [x [??]]. exists x. split. by constructor. done.
    * intros [x [Hin ?]]. induction l.
      + by destruct (not_elem_of_nil x).
      + inversion Hin; subst. by left. right; auto.
  Qed.

  Lemma Exists_inv x l : Exists P (x :: l) → P xExists P l.
  Proof. inversion 1; intuition trivial. Qed.
  Lemma Exists_app l1 l2 : Exists P (l1 ++ l2) ↔ Exists P l1Exists P l2.
  Proof.
    split.
    * induction l1; inversion 1; intuition.
    * intros [H|H].
      + induction H; simpl; intuition.
      + induction l1; simpl; intuition.
  Qed.


  Lemma Exists_not_Forall l : Exists (notP) l → ¬Forall P l.
  Proof. induction 1; inversion_clear 1; contradiction. Qed.
  Lemma Forall_not_Exists l : Forall (notP) l → ¬Exists P l.
  Proof. induction 1; inversion_clear 1; contradiction. Qed.

  Context {dec : ∀ x, Decision (P x)}.

  Fixpoint Forall_Exists_dec l : {Forall P l} + {Exists (notP) l}.
  Proof.
   refine (
    match l with
    | [] => left _
    | x :: l => cast_if_and (dec x) (Forall_Exists_dec l)
    end); clear Forall_Exists_dec; abstract intuition.
  Defined.


  Lemma not_Forall_Exists l : ¬Forall P lExists (notP) l.
  Proof. intro. destruct (Forall_Exists_dec l); intuition. Qed.

  Global Instance Forall_dec l : Decision (Forall P l) :=
    match Forall_Exists_dec l with
    | left H => left H
    | right H => right (Exists_not_Forall _ H)
    end.

  Fixpoint Exists_Forall_dec l : {Exists P l} + {Forall (notP) l}.
  Proof.
   refine (
    match l with
    | [] => right _
    | x :: l => cast_if_or (dec x) (Exists_Forall_dec l)
    end); clear Exists_Forall_dec; abstract intuition.
  Defined.


  Lemma not_Exists_Forall l : ¬Exists P lForall (notP) l.
  Proof. intro. destruct (Exists_Forall_dec l); intuition. Qed.

  Global Instance Exists_dec l : Decision (Exists P l) :=
    match Exists_Forall_dec l with
    | left H => left H
    | right H => right (Forall_not_Exists _ H)
    end.
End Forall_Exists.
End general_properties.

Section Forall2.
  Context {A B} (P : ABProp).

  Lemma Forall2_nil_inv_l k :
    Forall2 P [] kk = [].
  Proof. by inversion 1. Qed.
  Lemma Forall2_nil_inv_r k :
    Forall2 P k [] → k = [].
  Proof. by inversion 1. Qed.

  Lemma Forall2_cons_inv l1 l2 x1 x2 :
    Forall2 P (x1 :: l1) (x2 :: l2) → P x1 x2Forall2 P l1 l2.
  Proof. by inversion 1. Qed.
  Lemma Forall2_cons_inv_l l1 k x1 :
    Forall2 P (x1 :: l1) k → ∃ x2 l2,
      P x1 x2Forall2 P l1 l2k = x2 :: l2.
  Proof. inversion 1; subst; eauto. Qed.
  Lemma Forall2_cons_inv_r k l2 x2 :
    Forall2 P k (x2 :: l2) → ∃ x1 l1,
      P x1 x2Forall2 P l1 l2k = x1 :: l1.
  Proof. inversion 1; subst; eauto. Qed.
  Lemma Forall2_cons_nil_inv l1 x1 :
    Forall2 P (x1 :: l1) [] → False.
  Proof. by inversion 1. Qed.
  Lemma Forall2_nil_cons_inv l2 x2 :
    Forall2 P [] (x2 :: l2) → False.
  Proof. by inversion 1. Qed.

  Lemma Forall2_flip l1 l2 :
    Forall2 P l1 l2Forall2 (flip P) l2 l1.
  Proof. split; induction 1; constructor; auto. Qed.

  Lemma Forall2_length l1 l2 :
    Forall2 P l1 l2length l1 = length l2.
  Proof. induction 1; simpl; auto. Qed.

  Lemma Forall2_impl (Q : ABProp) l1 l2 :
    Forall2 P l1 l2 → (∀ x y, P x yQ x y) → Forall2 Q l1 l2.
  Proof. intros H ?. induction H; auto. Defined.

  Lemma Forall2_unique l k1 k2 :
    Forall2 P l k1
    Forall2 P l k2
    (∀ x y1 y2, P x y1P x y2y1 = y2) →
    k1 = k2.
  Proof.
    intros H. revert k2.
    induction H; inversion_clear 1; intros; f_equal; eauto.
  Qed.


  Lemma Forall2_Forall_l (Q : AProp) l k :
    Forall2 P l k
    Forally, ∀ x, P x yQ x) k
    Forall Q l.
  Proof. induction 1; inversion_clear 1; eauto. Qed.
  Lemma Forall2_Forall_r (Q : BProp) l k :
    Forall2 P l k
    Forallx, ∀ y, P x yQ y) l
    Forall Q k.
  Proof. induction 1; inversion_clear 1; eauto. Qed.

  Lemma Forall2_lookup l1 l2 i x y :
    Forall2 P l1 l2
      l1 !! i = Some xl2 !! i = Some yP x y.
  Proof.
    intros H. revert i. induction H.
    * discriminate.
    * intros [|?] ??; simpl in *; simplify_equality; eauto.
  Qed.

  Lemma Forall2_lookup_l l1 l2 i x :
    Forall2 P l1 l2l1 !! i = Some x → ∃ y,
      l2 !! i = Some yP x y.
  Proof.
    intros H. revert i. induction H.
    * discriminate.
    * intros [|?] ?; simpl in *; simplify_equality; eauto.
  Qed.

  Lemma Forall2_lookup_r l1 l2 i y :
    Forall2 P l1 l2l2 !! i = Some y → ∃ x,
      l1 !! i = Some xP x y.
  Proof.
    intros H. revert i. induction H.
    * discriminate.
    * intros [|?] ?; simpl in *; simplify_equality; eauto.
  Qed.


  Lemma Forall2_alter_l f l1 l2 i :
    Forall2 P l1 l2
    (∀ x1 x2,
      l1 !! i = Some x1l2 !! i = Some x2P x1 x2P (f x1) x2) →
    Forall2 P (alter f i l1) l2.
  Proof.
    intros Hl. revert i.
    induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.

  Lemma Forall2_alter_r f l1 l2 i :
    Forall2 P l1 l2
    (∀ x1 x2,
      l1 !! i = Some x1l2 !! i = Some x2P x1 x2P x1 (f x2)) →
    Forall2 P l1 (alter f i l2).
  Proof.
    intros Hl. revert i.
    induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.

  Lemma Forall2_alter f g l1 l2 i :
    Forall2 P l1 l2
    (∀ x1 x2,
      l1 !! i = Some x1l2 !! i = Some x2P x1 x2P (f x1) (g x2)) →
    Forall2 P (alter f i l1) (alter g i l2).
  Proof.
    intros Hl. revert i.
    induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.


  Lemma Forall2_replicate_l l n x :
    Forall (P x) l
    length l = n
    Forall2 P (replicate n x) l.
  Proof.
    intros Hl. revert n.
    induction Hl; intros [|?] ?; simplify_equality; constructor; auto.
  Qed.

  Lemma Forall2_replicate_r l n x :
    Forall (flip P x) l
    length l = n
    Forall2 P l (replicate n x).
  Proof.
    intros Hl. revert n.
    induction Hl; intros [|?] ?; simplify_equality; constructor; auto.
  Qed.

  Lemma Forall2_replicate n x1 x2 :
    P x1 x2
    Forall2 P (replicate n x1) (replicate n x2).
  Proof. induction n; simpl; constructor; auto. Qed.

  Lemma Forall2_take l1 l2 n :
    Forall2 P l1 l2
    Forall2 P (take n l1) (take n l2).
  Proof.
    intros Hl1l2. revert n.
    induction Hl1l2; intros [|?]; simpl; auto.
  Qed.

  Lemma Forall2_drop l1 l2 n :
    Forall2 P l1 l2
    Forall2 P (drop n l1) (drop n l2).
  Proof.
    intros Hl1l2. revert n.
    induction Hl1l2; intros [|?]; simpl; auto.
  Qed.

  Lemma Forall2_resize l1 l2 x1 x2 n :
    P x1 x2
    Forall2 P l1 l2
    Forall2 P (resize n x1 l1) (resize n x2 l2).
  Proof.
    intros. rewrite !resize_spec, (Forall2_length l1 l2) by done.
    auto using Forall2_app, Forall2_take, Forall2_replicate.
  Qed.


  Lemma Forall2_resize_ge_l l1 l2 x1 x2 n m :
    (∀ x, P x x2) →
    nm
    Forall2 P (resize n x1 l1) l2
    Forall2 P (resize m x1 l1) (resize m x2 l2).
  Proof.
    intros. assert (n = length l2).
    { by rewrite <-(Forall2_length (resize n x1 l1) l2), resize_length. }
    rewrite (le_plus_minus n m) by done. subst.
    rewrite !resize_plus, resize_all, drop_all, resize_nil.
    apply Forall2_app; [done |].
    apply Forall2_replicate_r; [| by rewrite resize_length].
    by apply Forall_true.
  Qed.

  Lemma Forall2_resize_ge_r l1 l2 x1 x2 n m :
    (∀ x3, P x1 x3) →
    nm
    Forall2 P l1 (resize n x2 l2) →
    Forall2 P (resize m x1 l1) (resize m x2 l2).
  Proof.
    intros. assert (n = length l1).
    { by rewrite (Forall2_length l1 (resize n x2 l2)), resize_length. }
    rewrite (le_plus_minus n m) by done. subst.
    rewrite !resize_plus, resize_all, drop_all, resize_nil.
    apply Forall2_app; [done |].
    apply Forall2_replicate_l; [| by rewrite resize_length].
    by apply Forall_true.
  Qed.


  Lemma Forall2_trans {C} (Q : BCProp) (R : ACProp) l1 l2 l3 :
    (∀ x1 x2 x3, P x1 x2Q x2 x3R x1 x3) →
    Forall2 P l1 l2
    Forall2 Q l2 l3
    Forall2 R l1 l3.
  Proof.
    intros ? Hl1l2. revert l3.
    induction Hl1l2; inversion_clear 1; eauto.
  Qed.


  Lemma Forall2_Forall (Q : AAProp) l :
    Forallx, Q x x) lForall2 Q l l.
  Proof. induction 1; constructor; auto. Qed.

  Global Instance Forall2_dec `{∀ x1 x2, Decision (P x1 x2)} :
    ∀ l1 l2, Decision (Forall2 P l1 l2).
  Proof.
   refine (
    fix go l1 l2 : Decision (Forall2 P l1 l2) :=
    match l1, l2 with
    | [], [] => left _
    | x1 :: l1, x2 :: l2 => cast_if_and (decide (P x1 x2)) (go l1 l2)
    | _, _ => right _
    end); clear go; abstract first [by constructor | by inversion 1].
  Defined.

End Forall2.

Section Forall2_order.
  Context {A} (R : relation A).

  Global Instance: PreOrder RPreOrder (Forall2 R).
  Proof.
    split.
    * intros l. induction l; by constructor.
    * intros ???. apply Forall2_trans. apply transitivity.
  Qed.

  Global Instance: AntiSymmetric RAntiSymmetric (Forall2 R).
  Proof. induction 2; inversion_clear 1; f_equal; auto. Qed.
End Forall2_order.

Ltac decompose_elem_of_list := repeat
  match goal with
  | H : ?x ∈ [] |- _ => by destruct (not_elem_of_nil x)
  | H : __ :: _ |- _ => apply elem_of_cons in H; destruct H
  | H : __ ++ _ |- _ => apply elem_of_app in H; destruct H
  end.
Ltac decompose_Forall := repeat
  match goal with
  | H : Forall _ [] |- _ => clear H
  | H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
  | H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
  | H : Forall2 _ [] [] |- _ => clear H
  | H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
  | H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
  | H : Forall2 _ [] ?l |- _ => apply Forall2_nil_inv_l in H; subst l
  | H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H; subst l
  | H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
     apply Forall2_cons_inv in H; destruct H
  | H : Forall2 _ (_ :: _) ?l |- _ =>
     apply Forall2_cons_inv_l in H; destruct H as (? & ? & ? & ? & ?); subst l
  | H : Forall2 _ ?l (_ :: _) |- _ =>
     apply Forall2_cons_inv_r in H; destruct H as (? & ? & ? & ? & ?); subst l
  end.

Theorems on the prefix and suffix predicates

Section prefix_postfix.
  Context {A : Type}.

  Global Instance: PreOrder (@prefix_of A).
  Proof.
    split.
    * intros ?. eexists []. by rewrite app_nil_r.
    * intros ??? [k1 ?] [k2 ?].
      exists (k1 ++ k2). subst. by rewrite app_assoc.
  Qed.


  Lemma prefix_of_nil (l : list A) : prefix_of [] l.
  Proof. by exists l. Qed.
  Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
  Proof. by intros [k E]. Qed.
  Lemma prefix_of_cons x y (l1 l2 : list A) :
    x = yprefix_of l1 l2prefix_of (x :: l1) (y :: l2).
  Proof. intros ? [k E]. exists k. by subst. Qed.
  Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
    prefix_of (x :: l1) (y :: l2) → x = y.
  Proof. intros [k E]. by injection E. Qed.
  Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
    prefix_of (x :: l1) (y :: l2) → prefix_of l1 l2.
  Proof. intros [k E]. exists k. by injection E. Qed.

  Lemma prefix_of_app_l (l1 l2 l3 : list A) :
    prefix_of (l1 ++ l3) l2prefix_of l1 l2.
  Proof. intros [k ?]. red. exists (l3 ++ k). subst. by rewrite <-app_assoc. Qed.
  Lemma prefix_of_app_r (l1 l2 l3 : list A) :
    prefix_of l1 l2prefix_of l1 (l2 ++ l3).
  Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite app_assoc. Qed.

  Global Instance: PreOrder (@suffix_of A).
  Proof.
    split.
    * intros ?. by eexists [].
    * intros ??? [k1 ?] [k2 ?].
      exists (k2 ++ k1). subst. by rewrite app_assoc.
  Qed.


  Lemma prefix_suffix_reverse (l1 l2 : list A) :
    prefix_of l1 l2suffix_of (reverse l1) (reverse l2).
  Proof.
    split; intros [k E]; exists (reverse k).
    * by rewrite E, reverse_app.
    * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
  Qed.

  Lemma suffix_prefix_reverse (l1 l2 : list A) :
    suffix_of l1 l2prefix_of (reverse l1) (reverse l2).
  Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.

  Lemma suffix_of_nil (l : list A) : suffix_of [] l.
  Proof. exists l. by rewrite app_nil_r. Qed.
  Lemma suffix_of_nil_inv (l : list A) : suffix_of l [] → l = [].
  Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
  Lemma suffix_of_cons_nil_inv x (l : list A) : ¬suffix_of (x :: l) [].
  Proof. by intros [[] ?]. Qed.

  Lemma suffix_of_app (l1 l2 k : list A) :
    suffix_of l1 l2suffix_of (l1 ++ k) (l2 ++ k).
  Proof. intros [k' E]. exists k'. subst. by rewrite app_assoc. Qed.

  Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
    suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y.
  Proof.
    rewrite suffix_prefix_reverse, !reverse_snoc.
    by apply prefix_of_cons_inv_1.
  Qed.

  Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) :
    suffix_of (l1 ++ [x]) (l2 ++ [y]) → suffix_of l1 l2.
  Proof.
    rewrite !suffix_prefix_reverse, !reverse_snoc.
    by apply prefix_of_cons_inv_2.
  Qed.


  Lemma suffix_of_cons_l (l1 l2 : list A) x :
    suffix_of (x :: l1) l2suffix_of l1 l2.
  Proof. intros [k ?]. exists (k ++ [x]). subst. by rewrite <-app_assoc. Qed.
  Lemma suffix_of_app_l (l1 l2 l3 : list A) :

  suffix_of (l3 ++ l1) l2suffix_of l1 l2.
  Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite <-app_assoc. Qed.
  Lemma suffix_of_cons_r (l1 l2 : list A) x :
    suffix_of l1 l2suffix_of l1 (x :: l2).
  Proof. intros [k ?]. exists (x :: k). by subst. Qed.
  Lemma suffix_of_app_r (l1 l2 l3 : list A) :
    suffix_of l1 l2suffix_of l1 (l3 ++ l2).
  Proof. intros [k ?]. exists (l3 ++ k). subst. by rewrite app_assoc. Qed.

  Lemma suffix_of_cons_inv (l1 l2 : list A) x y :
    suffix_of (x :: l1) (y :: l2) →
      x :: l1 = y :: l2suffix_of (x :: l1) l2.
  Proof.
    intros [[|? k] E].
    * by left.
    * right. simplify_equality. by apply suffix_of_app_r.
  Qed.


  Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
  Proof. intros [??]. discriminate_list_equality. Qed.

  Context `{∀ x y : A, Decision (x = y)}.

  Fixpoint strip_prefix (l1 l2 : list A) : list A * (list A * list A) :=
    match l1, l2 with
    | [], l2 => ([], ([], l2))
    | l1, [] => ([], (l1, []))
    | x :: l1, y :: l2 =>
      if decide_rel (=) x y
      then fst_map (x ::) (strip_prefix l1 l2)
      else ([], (x :: l1, y :: l2))
    end.

  Global Instance prefix_of_dec: ∀ l1 l2 : list A,
      Decision (prefix_of l1 l2) :=
    fix go l1 l2 :=
    match l1, l2 return { prefix_of l1 l2 } + { ¬prefix_of l1 l2 } with
    | [], _ => left (prefix_of_nil _)
    | _, [] => right (prefix_of_nil_not _ _)
    | x :: l1, y :: l2 =>
      match decide_rel (=) x y with
      | left Exy =>
        match go l1 l2 with
        | left Hl1l2 => left (prefix_of_cons _ _ _ _ Exy Hl1l2)
        | right Hl1l2 => right (Hl1l2prefix_of_cons_inv_2 _ _ _ _)
        end
      | right Exy => right (Exyprefix_of_cons_inv_1 _ _ _ _)
      end
    end.

  Global Instance suffix_of_dec (l1 l2 : list A) :
    Decision (suffix_of l1 l2).
  Proof.
    refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
     abstract (by rewrite suffix_prefix_reverse).
  Defined.

End prefix_postfix.

The simplify_suffix_of tactic removes suffix_of hypotheses that are tautologies, and simplifies suffix_of hypotheses involving (::) and (++).
Ltac simplify_suffix_of := repeat
  match goal with
  | H : suffix_of (_ :: _) _ |- _ =>
    destruct (suffix_of_cons_not _ _ H)
  | H : suffix_of (_ :: _) [] |- _ =>
    apply suffix_of_nil_inv in H
  | H : suffix_of (_ :: _) (_ :: _) |- _ =>
    destruct (suffix_of_cons_inv _ _ _ _ H); clear H
  | H : suffix_of ?x ?x |- _ => clear H
  | H : suffix_of ?x (_ :: ?x) |- _ => clear H
  | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
  | _ => progress simplify_equality
  end.

The solve_suffix_of tactic tries to solve goals involving suffix_of. It uses simplify_suffix_of to simplify hypotheses and tries to solve suffix_of conclusions. This tactic either fails or proves the goal.
Ltac solve_suffix_of := solve [intuition (repeat
  match goal with
  | _ => done
  | _ => progress simplify_suffix_of
  | |- suffix_of [] _ => apply suffix_of_nil
  | |- suffix_of _ _ => reflexivity
  | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r
  | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r
  | H : suffix_of _ _False |- _ => destruct H
  end)].
Hint Extern 0 (PropHolds (suffix_of _ _)) =>
  unfold PropHolds; solve_suffix_of : typeclass_instances.

Folding lists

Notation foldr := fold_right.
Notation foldr_app := fold_right_app.

Lemma foldr_permutation {A B} (R : relation B)
   `{!Equivalence R}
   (f : ABB) (b : B)
   `{!Proper ((=) ==> R ==> R) f}
   (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
  Proper (Permutation ==> R) (foldr f b).
Proof.
  induction 1; simpl.
  * done.
  * by f_equiv.
  * apply Hf.
  * etransitivity; eauto.
Qed.


We redefine foldl with the arguments in the same order as in Haskell.
Definition foldl {A B} (f : ABA) : Alist BA :=
  fix go a l :=
  match l with
  | [] => a
  | x :: l => go (f a x) l
  end.

Lemma foldl_app {A B} (f : ABA) (l k : list B) (a : A) :
  foldl f a (l ++ k) = foldl f (foldl f a l) k.
Proof. revert a. induction l; simpl; auto. Qed.

Monadic operations

Instance list_ret: MRet list := λ A x, x :: @nil A.
Instance list_fmap {A B} (f : AB) : 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 : Alist 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 : AM B) : list AM (list B) :=
  fix go l :=
  match l with
  | [] => mret []
  | x :: l => yf x; kgo l; mret (y :: k)
  end.

Section list_fmap.
  Context {A B : Type} (f : AB).

  Lemma list_fmap_compose {C} (g : BC) l :
    gf <$> l = g <$> f <$> l.
  Proof. induction l; simpl; f_equal; auto. Qed.

  Lemma list_fmap_ext (g : AB) (l : list A) :
    (∀ x, f x = g x) → fmap f l = fmap g l.
  Proof. intro. induction l; simpl; f_equal; auto. Qed.
  Lemma list_fmap_ext_alt (g : AB) (l : list A) :
    Forallx, f x = g x) lfmap f l = fmap g l.
  Proof.
    split.
    * induction 1; simpl; f_equal; auto.
    * induction l; simpl; constructor; simplify_equality; auto.
  Qed.


  Global Instance: Injective (=) (=) fInjective (=) (=) (fmap f).
  Proof.
    intros ? l1. induction l1 as [|x l1 IH].
    * by intros [|??].
    * intros [|??]; simpl; intros; f_equal; simplify_equality; auto.
  Qed.

  Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
  Proof. induction l1; simpl; by f_equal. Qed.
  Lemma fmap_cons_inv y l k :
    f <$> l = y :: k → ∃ x l', y = f xl = x :: l'.
  Proof. intros. destruct l; simpl; simplify_equality; eauto. Qed.
  Lemma fmap_app_inv l k1 k2 :
    f <$> l = k1 ++ k2 → ∃ l1 l2,
      k1 = f <$> l1k2 = f <$> l2l = l1 ++ l2.
  Proof.
    revert l. induction k1 as [|y k1 IH]; simpl.
    * intros l ?. by eexists [], l.
    * intros [|x l] ?; simpl; simplify_equality.
      destruct (IH l) as [l1 [l2 [? [??]]]]; subst; [done |].
      by exists (x :: l1) l2.
  Qed.


  Lemma fmap_length l : length (f <$> l) = length l.
  Proof. induction l; simpl; by f_equal. Qed.
  Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
  Proof.
    induction l; simpl; [done |].
    by rewrite !reverse_cons, fmap_app, IHl.
  Qed.

  Lemma fmap_replicate n x :
    f <$> replicate n x = replicate n (f x).
  Proof. induction n; simpl; f_equal; auto. Qed.

  Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
  Proof. revert i. induction l; by intros [|]. Qed.
  Lemma list_lookup_fmap_inv l i x :
    (f <$> l) !! i = Some x → ∃ y, x = f yl !! i = Some y.
  Proof.
    intros Hi. rewrite list_lookup_fmap in Hi.
    destruct (l !! i) eqn:?; simplify_equality; eauto.
  Qed.

   
  Lemma list_alter_fmap (g : AA) (h : BB) l i :
    Forallx, f (g x) = h (f x)) l
    f <$> alter g i l = alter h i (f <$> l).
  Proof.
    intros Hl. revert i.
    induction Hl; intros [|i]; simpl; f_equal; auto.
  Qed.

  Lemma elem_of_list_fmap_1 l x : xlf xf <$> l.
  Proof. induction 1; simpl; rewrite elem_of_cons; intuition. Qed.
  Lemma elem_of_list_fmap_1_alt l x y : xly = f xyf <$> l.
  Proof. intros. subst. by apply elem_of_list_fmap_1. Qed.
  Lemma elem_of_list_fmap_2 l x : xf <$> l → ∃ y, x = f yyl.
  Proof.
    induction l as [|y l IH]; simpl; intros; decompose_elem_of_list.
    + exists y. split; [done | by left].
    + destruct IH as [z [??]]. done. exists z. split; [done | by right].
  Qed.

  Lemma elem_of_list_fmap l x : xf <$> l ↔ ∃ y, x = f yyl.
  Proof.
    firstorder eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
  Qed.


  Lemma NoDup_fmap_1 (l : list A) :
    NoDup (f <$> l) → NoDup l.
  Proof.
    induction l; simpl; inversion_clear 1; constructor; auto.
    rewrite elem_of_list_fmap in *. naive_solver.
  Qed.

  Lemma NoDup_fmap_2 `{!Injective (=) (=) f} (l : list A) :
    NoDup lNoDup (f <$> l).
  Proof.
    induction 1; simpl; constructor; trivial.
    rewrite elem_of_list_fmap. intros [y [Hxy ?]].
    apply (injective f) in Hxy. by subst.
  Qed.

  Lemma NoDup_fmap `{!Injective (=) (=) f} (l : list A) :
    NoDup (f <$> l) ↔ NoDup l.
  Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.

  Global Instance fmap_Permutation_proper:
    Proper (Permutation ==> Permutation) (fmap f).
  Proof. induction 1; simpl; econstructor; eauto. Qed.

  Lemma Forall_fmap (l : list A) (P : BProp) :
    Forall P (f <$> l) ↔ Forall (Pf) l.
  Proof.
    split; induction l; inversion_clear 1; constructor; auto.
  Qed.


  Lemma Forall2_fmap_l {C} (P : BCProp) l1 l2 :
    Forall2 P (f <$> l1) l2Forall2 (Pf) l1 l2.
  Proof.
    split; revert l2; induction l1; inversion_clear 1; constructor; auto.
  Qed.

  Lemma Forall2_fmap_r {C} (P : CBProp) l1 l2 :
    Forall2 P l1 (f <$> l2) ↔ Forall2x, P xf) l1 l2.
  Proof.
    split; revert l1; induction l2; inversion_clear 1; constructor; auto.
  Qed.

  Lemma Forall2_fmap_1 {C D} (g : CD) (P : BDProp) l1 l2 :
    Forall2 P (f <$> l1) (g <$> l2) →
    Forall2x1 x2, P (f x1) (g x2)) l1 l2.
  Proof. revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed.
  Lemma Forall2_fmap_2 {C D} (g : CD) (P : BDProp) l1 l2 :
    Forall2x1 x2, P (f x1) (g x2)) l1 l2
    Forall2 P (f <$> l1) (g <$> l2).
  Proof. induction 1; simpl; auto. Qed.
  Lemma Forall2_fmap {C D} (g : CD) (P : BDProp) l1 l2 :
    Forall2 P (f <$> l1) (g <$> l2) ↔
    Forall2x1 x2, P (f x1) (g x2)) l1 l2.
  Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.

  Lemma mapM_fmap_Some (g : Boption A) (l : list A) :
    (∀ x, g (f x) = Some x) →
    mapM g (f <$> l) = Some l.
  Proof. intros. by induction l; simpl; simplify_option_equality. Qed.
  Lemma mapM_fmap_Some_inv (g : Boption A) (l : list A) (k : list B) :
    (∀ x y, g y = Some xy = f x) →
    mapM g k = Some l
    k = f <$> l.
  Proof.
    intros Hgf. revert l; induction k as [|y k]; intros [|x l] ?;
      simplify_option_equality; f_equiv; eauto.
  Qed.


  Lemma mapM_Some (g : Boption A) l k :
    Forall2x y, g x = Some y) l k
    mapM g l = Some k.
  Proof. by induction 1; simplify_option_equality. Qed.

  Lemma Forall2_impl_mapM (P : BAProp) (g : Boption A) l k :
    Forallx, ∀ y, g x = Some yP x y) l
    mapM g l = Some k
    Forall2 P l k.
  Proof.
    intros Hl. revert k. induction Hl; intros [|??] ?;
      simplify_option_equality; eauto.
  Qed.

End list_fmap.

Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
  (∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ ly1 = y2) →
  NoDup l
  NoDup (fst <$> l).
Proof.
  intros Hunique.
  induction 1 as [|[x1 y1] l Hin Hnodup IH]; simpl; constructor.
  * rewrite elem_of_list_fmap.
    intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
    rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
  * apply IH. intros.
    eapply Hunique; rewrite ?elem_of_cons; eauto.
Qed.


Section list_bind.
  Context {A B : Type} (f : Alist B).

  Lemma bind_app (l1 l2 : list A) :
    (l1 ++ l2) ≫= f = (l1 ≫= f) ++ (l2 ≫= f).
  Proof.
    induction l1; simpl; [done|].
    by rewrite <-app_assoc, IHl1.
  Qed.

  Lemma elem_of_list_bind (x : B) (l : list A) :
    xl ≫= f ↔ ∃ y, xf yyl.
  Proof.
    split.
    * induction l as [|y l IH]; simpl; intros; decompose_elem_of_list.
      + exists y. split; [done | by left].
      + destruct IH as [z [??]]. done.
        exists z. split; [done | by right].
    * intros [y [Hx Hy]].
      induction Hy; simpl; rewrite elem_of_app; intuition.
  Qed.


  Lemma Forall2_bind {C D} (g : Clist D) (P : BDProp) l1 l2 :
    Forall2x1 x2, Forall2 P (f x1) (g x2)) l1 l2
    Forall2 P (l1 ≫= f) (l2 ≫= g).
  Proof. induction 1; simpl; auto using Forall2_app. Qed.
End list_bind.

Section list_ret_join.
  Context {A : Type}.

  Lemma list_join_bind (ls : list (list A)) :
    mjoin ls = ls ≫= id.
  Proof. induction ls; simpl; f_equal; auto. Qed.

  Lemma elem_of_list_ret (x y : A) :
    x ∈ @mret list _ A yx = y.
  Proof. apply elem_of_list_singleton. Qed.
  Lemma elem_of_list_join (x : A) (ls : list (list A)) :
    xmjoin ls ↔ ∃ l, xllls.
  Proof. by rewrite list_join_bind, elem_of_list_bind. Qed.

  Lemma join_nil (ls : list (list A)) :
    mjoin ls = [] ↔ Forall (= []) ls.
  Proof.
    split.
    * by induction ls as [|[|??] ?]; constructor; auto.
    * by induction 1 as [|[|??] ?].
  Qed.

  Lemma join_nil_1 (ls : list (list A)) :
    mjoin ls = [] → Forall (= []) ls.
  Proof. by rewrite join_nil. Qed.
  Lemma join_nil_2 (ls : list (list A)) :
    Forall (= []) lsmjoin ls = [].
  Proof. by rewrite join_nil. Qed.

  Lemma join_length (ls : list (list A)) :
    length (mjoin ls) = foldr (pluslength) 0 ls.
  Proof. by induction ls; simpl; rewrite ?app_length; f_equal. Qed.
  Lemma join_length_same (ls : list (list A)) n :
    Foralll, length l = n) ls
    length (mjoin ls) = length ls * n.
  Proof. rewrite join_length. by induction 1; simpl; f_equal. Qed.

  Lemma lookup_join_same_length (ls : list (list A)) n i :
    n ≠ 0 →
    Foralll, length l = n) ls
    mjoin ls !! i = ls !! (i `div` n) ≫= (!! (i `mod` n)).
  Proof.
    intros Hn Hls. revert i.
    induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
    destruct (decide (i < n)) as [Hin|Hin].
    * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
      rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
      simpl. rewrite lookup_app_l; auto with lia.
    * replace i with ((i - n) + 1 * n) by lia.
      rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
      replace (i - n + 1 * n) with i by lia.
      rewrite (plus_comm _ 1), lookup_app_r_alt, IH by lia.
      by subst.
  Qed.


  Lemma alter_join_same_length f (ls : list (list A)) n i :
    n ≠ 0 →
    Foralll, length l = n) ls
    alter f i (mjoin ls) = mjoin (alter (alter f (i `mod` n)) (i `div` n) ls).
  Proof.
    intros Hn Hls. revert i.
    induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
    destruct (decide (i < n)) as [Hin|Hin].
    * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
      rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
      simpl. rewrite alter_app_l; auto with lia.
    * replace i with ((i - n) + 1 * n) by lia.
      rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
      replace (i - n + 1 * n) with i by lia.
      rewrite (plus_comm _ 1), alter_app_r_alt, IH by lia.
      by subst.
  Qed.

  Lemma insert_join_same_length (ls : list (list A)) n i x :
    n ≠ 0 →
    Foralll, length l = n) ls
    <[i:=x]>(mjoin ls) = mjoin (alter <[i `mod` n:=x]> (i `div` n) ls).
  Proof. apply alter_join_same_length. Qed.

  Lemma Forall2_join {B} (P : ABProp) ls1 ls2 :
    Forall2 (Forall2 P) ls1 ls2
    Forall2 P (mjoin ls1) (mjoin ls2).
  Proof. induction 1; simpl; auto using Forall2_app. Qed.
End list_ret_join.

Ltac simplify_list_fmap_equality := repeat
  match goal with
  | _ => progress simplify_equality
  | H : _ <$> _ = _ :: _ |- _ =>
    apply fmap_cons_inv in H; destruct H as [? [? [??]]]
  | H : _ :: _ = _ <$> _ |- _ => symmetry in H
  | H : _ <$> _ = _ ++ _ |- _ =>
    apply fmap_app_inv in H; destruct H as [? [? [? [??]]]]
  | H : _ ++ _ = _ <$> _ |- _ => symmetry in H
  end.

Indexed folds and maps

We define stronger variants of map and fold that also take the index of the element into account.
Definition imap_go {A B} (f : natAB) : natlist Alist 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 : natAB) : list Alist B := imap_go f 0.

Definition ifoldr {A B} (f : natBAA)
    (a : natA) : natlist BA :=
  fix go (n : nat) (l : list B) : A :=
  match l with
  | nil => a n
  | b :: l => f n b (go (S n) l)
  end.

Lemma ifoldr_app {A B} (f : natBAA) (a : natA)
    (l1 l2 : list B) n :
  ifoldr f a n (l1 ++ l2) = ifoldr fn, ifoldr f a n l2) n l1.
Proof.
  revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto.
Qed.


Lists of the same length

The same_length view allows convenient induction over two lists with the same length.
Section same_length.
  Context {A B : Type}.

  Inductive same_length : list Alist BProp :=
    | same_length_nil : same_length [] []
    | same_length_cons x y l k :
      same_length l ksame_length (x :: l) (y :: k).

  Lemma same_length_length_1 l k :
    same_length l klength l = length k.
  Proof. induction 1; simpl; auto. Qed.
  Lemma same_length_length_2 l k :
    length l = length ksame_length l k.
  Proof.
    revert k. induction l; intros [|??]; try discriminate;
      constructor; auto with arith.
  Qed.

  Lemma same_length_length l k :
    same_length l klength l = length k.
  Proof. split; auto using same_length_length_1, same_length_length_2. Qed.

  Lemma same_length_lookup l k i :
    same_length l kis_Some (l !! i) → is_Some (k !! i).
  Proof.
    rewrite same_length_length.
    setoid_rewrite lookup_lt_length.
    intros E. by rewrite E.
  Qed.


  Lemma Forall2_same_length (P : ABProp) l1 l2 :
    Forall2 P l1 l2
    same_length l1 l2.
  Proof. intro. eapply same_length_length, Forall2_length; eauto. Qed.
  Lemma Forall2_app_inv (P : ABProp) l1 l2 k1 k2 :
    same_length l1 k1
    Forall2 P (l1 ++ l2) (k1 ++ k2) → Forall2 P l2 k2.
  Proof. induction 1. done. inversion 1; subst; auto. Qed.

  Lemma same_length_Forall2 l1 l2 :
    same_length l1 l2Forall2_ _, True) l1 l2.
  Proof. split; induction 1; constructor; auto. Qed.

  Lemma same_length_take l1 l2 n :
    same_length l1 l2
    same_length (take n l1) (take n l2).
  Proof. rewrite !same_length_Forall2. apply Forall2_take. Qed.
  Lemma same_length_drop l1 l2 n :
    same_length l1 l2
    same_length (drop n l1) (drop n l2).
  Proof. rewrite !same_length_Forall2. apply Forall2_drop. Qed.
  Lemma same_length_resize l1 l2 x1 x2 n :
    same_length (resize n x1 l1) (resize n x2 l2).
  Proof. apply same_length_length. by rewrite !resize_length. Qed.
End same_length.

Instance: ∀ A, Reflexive (@same_length A A).
Proof. intros A l. induction l; constructor; auto. Qed.

Zipping lists

Definition zip_with {A B C} (f : ABC) : list Alist Blist C :=
  fix go l1 l2 :=
  match l1, l2 with
  | x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2
  | _ , _ => []
  end.

Section zip_with.
  Context {A B C : Type} (f : ABC).

  Lemma zip_with_length l1 l2 :
    length l1length l2
    length (zip_with f l1 l2) = length l1.
  Proof.
    revert l2.
    induction l1; intros [|??]; simpl; auto with lia.
  Qed.


  Lemma zip_with_fmap_fst_le (g : CA) l1 l2 :
    (∀ x y, g (f x y) = x) →
    length l1length l2
    g <$> zip_with f l1 l2 = l1.
  Proof.
    revert l2.
    induction l1; intros [|??] ??; simpl in *; f_equal; auto with lia.
  Qed.

  Lemma zip_with_fmap_snd_le (g : CB) l1 l2 :
    (∀ x y, g (f x y) = y) →
    length l2length l1
    g <$> zip_with f l1 l2 = l2.
  Proof.
    revert l1.
    induction l2; intros [|??] ??; simpl in *; f_equal; auto with lia.
  Qed.

  Lemma zip_with_fmap_fst (g : CA) l1 l2 :
    (∀ x y, g (f x y) = x) →
    same_length l1 l2
    g <$> zip_with f l1 l2 = l1.
  Proof. induction 2; simpl; f_equal; auto. Qed.
  Lemma zip_with_fmap_snd (g : CB) l1 l2 :
    (∀ x y, g (f x y) = y) →
    same_length l1 l2
    g <$> zip_with f l1 l2 = l2.
  Proof. induction 2; simpl; f_equal; auto. Qed.

  Lemma Forall_zip_with_fst (P : AProp) (Q : CProp) l1 l2 :
    Forall P l1
    Forally, ∀ x, P xQ (f x y)) l2
    Forall Q (zip_with f l1 l2).
  Proof.
    intros Hl1. revert l2.
    induction Hl1; destruct 1; simpl in *; auto.
  Qed.

  Lemma Forall_zip_with_snd (P : BProp) (Q : CProp) l1 l2 :
    Forallx, ∀ y, P yQ (f x y)) l1
    Forall P l2
    Forall Q (zip_with f l1 l2).
  Proof.
    intros Hl1. revert l2.
    induction Hl1; destruct 1; simpl in *; auto.
  Qed.

End zip_with.

Notation zip := (zip_with pair).

Section zip.
  Context {A B : Type}.

  Lemma zip_length (l1 : list A) (l2 : list B) :
    length l1length l2
    length (zip l1 l2) = length l1.
  Proof. by apply zip_with_length. Qed.

  Lemma zip_fmap_fst_le (l1 : list A) (l2 : list B) :
    length l1length l2
    fst <$> zip l1 l2 = l1.
  Proof. by apply zip_with_fmap_fst_le. Qed.
  Lemma zip_fmap_snd (l1 : list A) (l2 : list B) :
    length l2length l1
    snd <$> zip l1 l2 = l2.
  Proof. by apply zip_with_fmap_snd_le. Qed.

  Lemma zip_fst (l1 : list A) (l2 : list B) :
    same_length l1 l2
    fst <$> zip l1 l2 = l1.
  Proof. by apply zip_with_fmap_fst. Qed.
  Lemma zip_snd (l1 : list A) (l2 : list B) :
    same_length l1 l2snd <$> zip l1 l2 = l2.
  Proof. by apply zip_with_fmap_snd. Qed.
End zip.

Definition zipped_map {A B} (f : list Alist AAB) :
    list Alist Alist B :=
  fix go l k :=
  match k with
  | [] => []
  | x :: k => f l k x :: go (x :: l) k
  end.

Lemma elem_of_zipped_map {A B} (f : list Alist AAB) l k x :
  xzipped_map f l k
    ∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
Proof.
  split.
  * revert l. induction k as [|z k IH]; simpl;
      intros l ?; decompose_elem_of_list.
    + by eexists [], k, z.
    + destruct (IH (z :: l)) as [k' [k'' [y [??]]]]; [done |]; subst.
      eexists (z :: k'), k'', y. split; [done |].
      by rewrite reverse_cons, <-app_assoc.
  * intros [k' [k'' [y [??]]]]; subst.
    revert l. induction k' as [|z k' IH]; intros l.
    + by left.
    + right. by rewrite reverse_cons, <-!app_assoc.
Qed.


Section zipped_list_ind.
  Context {A} (P : list Alist AProp).
  Context (Pnil : ∀ l, P l []).
  Context (Pcons : ∀ l k x, P (x :: l) kP l (x :: k)).

  Fixpoint zipped_list_ind l k : P l k :=
    match k with
    | [] => Pnil _
    | x :: k => Pcons _ _ _ (zipped_list_ind (x :: l) k)
    end.
End zipped_list_ind.

Inductive zipped_Forall {A} (P : list Alist AAProp) :
    list Alist AProp :=
  | 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 {_ _} _ _ _ _ _.

Lemma zipped_Forall_app {A} (P : list Alist AAProp) l k k' :
  zipped_Forall P l (k ++ k') → zipped_Forall P (reverse k ++ l) k'.
Proof.
  revert l. induction k as [|x k IH]; simpl; [done |].
  inversion_clear 1. rewrite reverse_cons, <-app_assoc.
  by apply IH.
Qed.


Permutations

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.

Section permutations.
  Context {A : Type}.

  Lemma interleave_cons (x : A) (l : list A) :
    x :: linterleave x l.
  Proof. destruct l; simpl; rewrite elem_of_cons; auto. Qed.
  Lemma interleave_Permutation (x : A) (l l' : list A) :
    l' ∈ interleave x lPermutation l' (x :: l).
  Proof.
    revert l'. induction l as [|y l IH]; intros l'; simpl.
    * rewrite elem_of_list_singleton. intros. by subst.
    * rewrite elem_of_cons, elem_of_list_fmap.
      intros [?|[? [? H]]]; subst.
      + by constructor.
      + rewrite (IH _ H). constructor.
  Qed.


  Lemma permutations_refl (l : list A) :
    lpermutations l.
  Proof.
    induction l; simpl.
    * by apply elem_of_list_singleton.
    * apply elem_of_list_bind. eauto using interleave_cons.
  Qed.

  Lemma permutations_skip (x : A) (l l' : list A) :
    lpermutations l' →
    x :: lpermutations (x :: l').
  Proof.
    intros Hl. simpl. apply elem_of_list_bind.
    eauto using interleave_cons.
  Qed.

  Lemma permutations_swap (x y : A) (l : list A) :
    y :: x :: lpermutations (x :: y :: l).
  Proof.
    simpl. apply elem_of_list_bind.
    exists (y :: l). split; simpl.
    * destruct l; simpl; rewrite !elem_of_cons; auto.
    * apply elem_of_list_bind. simpl.
      eauto using interleave_cons, permutations_refl.
  Qed.

  Lemma permutations_nil (l : list A) :
    lpermutations [] ↔ l = [].
  Proof. simpl. by rewrite elem_of_list_singleton. Qed.

  Lemma interleave_interleave_toggle (x1 x2 : A) (l1 l2 l3 : list A) :
    l1interleave x1 l2
    l2interleave x2 l3 → ∃ l4,
      l1interleave x2 l4l4interleave x1 l3.
  Proof.
    revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
    { intros Hl1 Hl2.
      rewrite elem_of_list_singleton in Hl2. subst. simpl in Hl1.
      rewrite elem_of_cons, elem_of_list_singleton in Hl1.
      exists [x1]. simpl.
      rewrite elem_of_cons, !elem_of_list_singleton. tauto. }
    rewrite elem_of_cons, elem_of_list_fmap.
    intros Hl1 [? | [l2' [??]]]; subst; simpl in *.
    * rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
      destruct Hl1 as [? | [? | [l4 [??]]]]; subst.
      + exists (x1 :: y :: l3). simpl. rewrite !elem_of_cons. tauto.
      + exists (x1 :: y :: l3). simpl. rewrite !elem_of_cons. tauto.
      + exists l4. simpl. rewrite elem_of_cons. auto using interleave_cons.
    * rewrite elem_of_cons, elem_of_list_fmap in Hl1.
      destruct Hl1 as [? | [l1' [??]]]; subst.
      + exists (x1 :: y :: l3). simpl.
        rewrite !elem_of_cons, !elem_of_list_fmap.
        split; [| by auto]. right. right. exists (y :: l2').
        rewrite elem_of_list_fmap. naive_solver.
      + destruct (IH l1' l2') as [l4 [??]]; auto.
        exists (y :: l4). simpl.
        rewrite !elem_of_cons, !elem_of_list_fmap. naive_solver.
  Qed.

  Lemma permutations_interleave_toggle (x : A) (l1 l2 l3 : list A) :
    l1permutations l2
    l2interleave x l3 → ∃ l4,
      l1interleave x l4l4permutations l3.
  Proof.
    revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
    { intros Hl1 Hl2. eexists []. simpl.
      split; [| by rewrite elem_of_list_singleton].
      rewrite elem_of_list_singleton in Hl2.
      by rewrite Hl2 in Hl1. }
    rewrite elem_of_cons, elem_of_list_fmap.
    intros Hl1 [? | [l2' [? Hl2']]]; subst; simpl in *.
    * rewrite elem_of_list_bind in Hl1.
      destruct Hl1 as [l1' [??]]. by exists l1'.
    * rewrite elem_of_list_bind in Hl1.
      setoid_rewrite elem_of_list_bind.
      destruct Hl1 as [l1' [??]].
      destruct (IH l1' l2') as [l1'' [??]]; auto.
      destruct (interleave_interleave_toggle y x l1 l1' l1'') as [? [??]]; eauto.
  Qed.

  Lemma permutations_trans (l1 l2 l3 : list A) :
    l1permutations l2
    l2permutations l3
    l1permutations l3.
  Proof.
    revert l1 l2. induction l3 as [|x l3 IH]; intros l1 l2; simpl.
    * intros Hl1 Hl2. rewrite elem_of_list_singleton in Hl2.
      by rewrite Hl2 in Hl1.
    * rewrite !elem_of_list_bind. intros Hl1 [l2' [Hl2 Hl2']].
      destruct (permutations_interleave_toggle x l1 l2 l2') as [? [??]]; eauto.
  Qed.


  Lemma permutations_Permutation (l l' : list A) :
    l' ∈ permutations lPermutation l l'.
  Proof.
    split.
    * revert l'. induction l; simpl; intros l''.
      + rewrite elem_of_list_singleton.
        intros. subst. constructor.
      + rewrite elem_of_list_bind. intros [l' [Hl'' ?]].
        rewrite (interleave_Permutation _ _ _ Hl'').
        constructor; auto.
    * induction 1; eauto using permutations_refl,
        permutations_skip, permutations_swap, permutations_trans.
  Qed.


  Global Instance Permutation_dec `{∀ x y : A, Decision (x = y)}
    (l1 l2 : list A) : Decision (Permutation l1 l2).
  Proof.
    refine (cast_if (decide (l2permutations l1)));
      by rewrite <-permutations_Permutation.
  Defined.

End permutations.

Set operations on lists

Section list_set_operations.
  Context {A} {dec : ∀ x y : A, Decision (x = y)}.

  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.
  Lemma elem_of_list_difference l k x :
    xlist_difference l kxlxk.
  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 lNoDup (list_difference l k).
  Proof.
    induction 1; simpl; try case_decide.
    * constructor.
    * done.
    * constructor. rewrite elem_of_list_difference; intuition. done.
  Qed.


  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.
  Lemma elem_of_list_intersection l k x :
    xlist_intersection l kxlxk.
  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 lNoDup (list_intersection l k).
  Proof.
    induction 1; simpl; try case_decide.
    * constructor.
    * constructor. rewrite elem_of_list_intersection; intuition. done.
    * done.
  Qed.


  Definition list_intersection_with (f : AAoption A) :
      list Alist Alist A :=
    fix go l k :=
    match l with
    | [] => []
    | x :: l => foldry,
       match f x y with None => id | Some z => (z ::) end) (go l k) k
    end.
  Lemma elem_of_list_intersection_with f l k x :
    xlist_intersection_with f l k ↔ ∃ x1 x2,
      x1lx2kf 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, x2kf x1 x2 = Some x)
          ∨ xlist_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_operations.