list.v

    - intros [k Hk]. revert l2 k Hk.
      induction l1 as [|x l1 IH]; simpl; intros l2 k.
      { intros. apply contains_nil_l. }
      destruct (list_remove x l2) as [k'|] eqn:?; intros; simplify_eq.
      rewrite contains_cons_l. eauto using list_remove_Some.
  Qed.
  Global Instance contains_dec l1 l2 : Decision (l1 `contains` l2).
  Proof.
   refine (cast_if (decide (is_Some (list_remove_list l1 l2))));
    abstract (rewrite list_remove_list_contains; tauto).
  Defined.
  Global Instance Permutation_dec l1 l2 : Decision (l1 ≡ₚ l2).
  Proof.
   refine (cast_if_and
    (decide (length l1 = length l2)) (decide (l1 `contains` l2)));
    abstract (rewrite Permutation_alt; tauto).
  Defined.
End contains_dec.

(** ** Properties of [included] *)
Global Instance included_preorder : PreOrder (@included A).
Proof. split; firstorder. Qed.
Lemma included_nil l : [] `included` l.
Proof. intros x. by rewrite elem_of_nil. Qed.

(** ** Properties of the [Forall] and [Exists] predicate *)
Lemma Forall_Exists_dec {P Q : A → Prop} (dec : ∀ x, {P x} + {Q x}) :
  ∀ l, {Forall P l} + {Exists Q l}.
Proof.
 refine (
  fix go l :=
  match l return {Forall P l} + {Exists Q l} with
  | [] => left _
  | x :: l => cast_if_and (dec x) (go l)
  end); clear go; intuition.
Defined.

Section Forall_Exists.
  Context (P : A → Prop).

  Definition Forall_nil_2 := @Forall_nil A.
  Definition Forall_cons_2 := @Forall_cons A.
  Lemma Forall_forall l : Forall P l ↔ ∀ x, x ∈ l → P x.
  Proof.
    split; [induction 1; inversion 1; subst; auto|].
    intros Hin; induction l as [|x l IH]; constructor; [apply Hin; constructor|].
    apply IH. 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 x ∧ Forall P l.
  Proof. by inversion 1. Qed.
  Lemma Forall_cons x l : Forall P (x :: l) ↔ P x ∧ Forall 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_2 l1 l2 : Forall P l1 → Forall P l2 → Forall P (l1 ++ l2).
  Proof. induction 1; simpl; auto. Qed.
  Lemma Forall_app l1 l2 : Forall P (l1 ++ l2) ↔ Forall P l1 ∧ Forall P l2.
  Proof.
    split; [induction l1; inversion 1; intuition|].
    intros [??]; auto using Forall_app_2.
  Qed.
  Lemma Forall_true l : (∀ x, P x) → Forall P l.
  Proof. induction l; auto. Qed.
  Lemma Forall_impl (Q : A → Prop) l :
    Forall P l → (∀ x, P x → Q x) → Forall Q l.
  Proof. intros H ?. induction H; auto. Defined.
  Global Instance Forall_proper:
    Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Forall A).
  Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
  Lemma Forall_iff l (Q : A → Prop) :
    (∀ x, P x ↔ Q x) → Forall P l ↔ Forall Q l.
  Proof. intros H. apply Forall_proper. red; apply H. done. Qed.
  Lemma Forall_not l : length l ≠ 0 → Forall (not ∘ P) l → ¬Forall P l.
  Proof. by destruct 2; inversion 1. Qed.
  Lemma Forall_and {Q} l : Forall (λ x, P x ∧ Q x) l ↔ Forall P l ∧ Forall Q l.
  Proof.
    split; [induction 1; constructor; naive_solver|].
    intros [Hl Hl']; revert Hl'; induction Hl; inversion_clear 1; auto.
  Qed.
  Lemma Forall_and_l {Q} l : Forall (λ x, P x ∧ Q x) l → Forall P l.
  Proof. rewrite Forall_and; tauto. Qed.
  Lemma Forall_and_r {Q} l : Forall (λ x, P x ∧ Q x) l → Forall Q l.
  Proof. rewrite Forall_and; tauto. Qed.
  Lemma Forall_delete l i : Forall P l → Forall 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 x → P x.
  Proof.
    rewrite Forall_forall. setoid_rewrite elem_of_list_lookup. naive_solver.
  Qed.
  Lemma Forall_lookup_1 l i x : Forall P l → l !! i = Some x → P x.
  Proof. rewrite Forall_lookup. eauto. Qed.
  Lemma Forall_lookup_2 l : (∀ i x, l !! i = Some x → P x) → Forall P l.
  Proof. by rewrite Forall_lookup. Qed.
  Lemma Forall_tail l : Forall P l → Forall P (tail l).
  Proof. destruct 1; simpl; auto. Qed.
  Lemma Forall_alter f l i :
    Forall P l → (∀ x, l!!i = Some x → P x → P (f x)) → Forall P (alter f i l).
  Proof.
    intros Hl. revert i. induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.
  Lemma Forall_alter_inv f l i :
    Forall P (alter f i l) → (∀ x, l!!i = Some x → P (f x) → P x) → Forall P l.
  Proof.
    revert i. induction l; intros [|?]; simpl;
      inversion_clear 1; constructor; eauto.
  Qed.
  Lemma Forall_insert l i x : Forall P l → P x → Forall P (<[i:=x]>l).
  Proof. rewrite list_insert_alter; auto using Forall_alter. Qed.
  Lemma Forall_inserts l i k :
    Forall P l → Forall P k → Forall P (list_inserts i k l).
  Proof.
    intros Hl Hk; revert i.
    induction Hk; simpl; auto using Forall_insert.
  Qed.
  Lemma Forall_replicate n x : P x → Forall 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 Forall_take n l : Forall P l → Forall P (take n l).
  Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
  Lemma Forall_drop n l : Forall P l → Forall P (drop n l).
  Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
  Lemma Forall_resize n x l : P x → Forall P l → Forall P (resize n x l).
  Proof.
    intros ? Hl. revert n.
    induction Hl; intros [|?]; simpl; auto using Forall_replicate.
  Qed.
  Lemma Forall_resize_inv n x l :
    length l ≤ n → Forall P (resize n x l) → Forall P l.
  Proof. intros ?. rewrite resize_ge, Forall_app by done. by intros []. Qed.
  Lemma Forall_sublist_lookup l i n k :
    sublist_lookup i n l = Some k → Forall P l → Forall P k.
  Proof.
    unfold sublist_lookup. intros; simplify_option_eq.
    auto using Forall_take, Forall_drop.
  Qed.
  Lemma Forall_sublist_alter f l i n k :
    Forall P l → sublist_lookup i n l = Some k → Forall P (f k) →
    Forall P (sublist_alter f i n l).
  Proof.
    unfold sublist_alter, sublist_lookup. intros; simplify_option_eq.
    auto using Forall_app_2, Forall_drop, Forall_take.
  Qed.
  Lemma Forall_sublist_alter_inv f l i n k :
    sublist_lookup i n l = Some k →
    Forall P (sublist_alter f i n l) → Forall P (f k).
  Proof.
    unfold sublist_alter, sublist_lookup. intros ?; simplify_option_eq.
    rewrite !Forall_app; tauto.
  Qed.
  Lemma Forall_reshape l szs : Forall P l → Forall (Forall P) (reshape szs l).
  Proof.
    revert l. induction szs; simpl; auto using Forall_take, Forall_drop.
  Qed.
  Lemma Forall_rev_ind (Q : list A → Prop) :
    Q [] → (∀ x l, P x → Forall P l → Q l → Q (l ++ [x])) →
    ∀ l, Forall P l → Q l.
  Proof.
    intros ?? l. induction l using rev_ind; auto.
    rewrite Forall_app, Forall_singleton; intros [??]; auto.
  Qed.
  Lemma Exists_exists l : Exists P l ↔ ∃ x, x ∈ l ∧ P x.
  Proof.
    split.
    - induction 1 as [x|y ?? [x [??]]]; exists x; by repeat constructor.
    - 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 x ∨ Exists P l.
  Proof. inversion 1; intuition trivial. Qed.
  Lemma Exists_app l1 l2 : Exists P (l1 ++ l2) ↔ Exists P l1 ∨ Exists P l2.
  Proof.
    split.
    - induction l1; inversion 1; intuition.
    - intros [H|H]; [induction H | induction l1]; simpl; intuition.
  Qed.
  Lemma Exists_impl (Q : A → Prop) l :
    Exists P l → (∀ x, P x → Q x) → Exists Q l.
  Proof. intros H ?. induction H; auto. Defined.
  Global Instance Exists_proper:
    Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Exists A).
  Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
  Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l.
  Proof. induction 1; inversion_clear 1; contradiction. Qed.
  Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
  Proof. induction 1; inversion_clear 1; contradiction. Qed.

  Lemma Forall_list_difference `{∀ x y : A, Decision (x = y)} l k :
    Forall P l → Forall P (list_difference l k).
  Proof.
    rewrite !Forall_forall.
    intros ? x; rewrite elem_of_list_difference; naive_solver.
  Qed.
  Lemma Forall_list_union `{∀ x y : A, Decision (x = y)} l k :
    Forall P l → Forall P k → Forall P (list_union l k).
  Proof. intros. apply Forall_app; auto using Forall_list_difference. Qed.
  Lemma Forall_list_intersection `{∀ x y : A, Decision (x = y)} l k :
    Forall P l → Forall P (list_intersection l k).
  Proof.
    rewrite !Forall_forall.
    intros ? x; rewrite elem_of_list_intersection; naive_solver.
  Qed.

  Context {dec : ∀ x, Decision (P x)}.
  Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l.
  Proof. intro. destruct (Forall_Exists_dec dec l); intuition. Qed.
  Lemma not_Exists_Forall l : ¬Exists P l → Forall (not ∘ P) l.
  Proof. by destruct (Forall_Exists_dec (λ x, swap_if (decide (P x))) l). Qed.
  Global Instance Forall_dec l : Decision (Forall P l) :=
    match Forall_Exists_dec dec l with
    | left H => left H
    | right H => right (Exists_not_Forall _ H)
    end.
  Global Instance Exists_dec l : Decision (Exists P l) :=
    match Forall_Exists_dec (λ x, swap_if (decide (P x))) l with
    | left H => right (Forall_not_Exists _ H)
    | right H => left H
    end.
End Forall_Exists.

Lemma replicate_as_Forall (x : A) n l :
  replicate n x = l ↔ length l = n ∧ Forall (x =) l.
Proof. rewrite replicate_as_elem_of, Forall_forall. naive_solver. Qed.
Lemma replicate_as_Forall_2 (x : A) n l :
  length l = n → Forall (x =) l → replicate n x = l.
Proof. by rewrite replicate_as_Forall. Qed.
End more_general_properties.

Lemma Forall_swap {A B} (Q : A → B → Prop) l1 l2 :
  Forall (λ y, Forall (Q y) l1) l2 ↔ Forall (λ x, Forall (flip Q x) l2) l1.
Proof. repeat setoid_rewrite Forall_forall. simpl. split; eauto. Qed.
Lemma Forall_seq (P : nat → Prop) i n :
  Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
Proof.
  rewrite Forall_lookup. split.
  - intros H j [??]. apply (H (j - i)).
    rewrite lookup_seq; auto with f_equal lia.
  - intros H j x Hj. apply lookup_seq_inv in Hj.
    destruct Hj; subst. auto with lia.
Qed.

(** ** Properties of the [Forall2] predicate *)
Section Forall2.
  Context {A B} (P : A → B → Prop).
  Implicit Types x : A.
  Implicit Types y : B.
  Implicit Types l : list A.
  Implicit Types k : list B.

  Lemma Forall2_same_length l k :
    Forall2 (λ _ _, True) l k ↔ length l = length k.
  Proof.
    split; [by induction 1; f_equal/=|].
    revert k. induction l; intros [|??] ?; simplify_eq/=; auto.
  Qed.
  Lemma Forall2_length l k : Forall2 P l k → length l = length k.
  Proof. by induction 1; f_equal/=. Qed.
  Lemma Forall2_length_l l k n : Forall2 P l k → length l = n → length k = n.
  Proof. intros ? <-; symmetry. by apply Forall2_length. Qed.
  Lemma Forall2_length_r l k n : Forall2 P l k → length k = n → length l = n.
  Proof. intros ? <-. by apply Forall2_length. Qed.

  Lemma Forall2_true l k : (∀ x y, P x y) → length l = length k → Forall2 P l k.
  Proof. rewrite <-Forall2_same_length. induction 2; naive_solver. Qed.
  Lemma Forall2_flip l k : Forall2 (flip P) k l ↔ Forall2 P l k.
  Proof. split; induction 1; constructor; auto. Qed.
  Lemma Forall2_transitive {C} (Q : B → C → Prop) (R : A → C → Prop) l k lC :
    (∀ x y z, P x y → Q y z → R x z) →
    Forall2 P l k → Forall2 Q k lC → Forall2 R l lC.
  Proof. intros ? Hl. revert lC. induction Hl; inversion_clear 1; eauto. Qed.
  Lemma Forall2_impl (Q : A → B → Prop) l k :
    Forall2 P l k → (∀ x y, P x y → Q x y) → Forall2 Q l k.
  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 y1 → P x y2 → y1 = y2) → k1 = k2.
  Proof.
    intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
  Qed.
  Lemma Forall2_forall `{Inhabited C} (Q : C → A → B → Prop) l k :
    Forall2 (λ x y, ∀ z, Q z x y) l k ↔ ∀ z, Forall2 (Q z) l k.
  Proof.
    split; [induction 1; constructor; auto|].
    intros Hlk. induction (Hlk inhabitant) as [|x y l k _ _ IH]; constructor.
    - intros z. by feed inversion (Hlk z).
    - apply IH. intros z. by feed inversion (Hlk z).
  Qed.

  Lemma Forall_Forall2 (Q : A → A → Prop) l :
    Forall (λ x, Q x x) l → Forall2 Q l l.
  Proof. induction 1; constructor; auto. Qed.
  Lemma Forall2_Forall_l (Q : A → Prop) l k :
    Forall2 P l k → Forall (λ y, ∀ x, P x y → Q x) k → Forall Q l.
  Proof. induction 1; inversion_clear 1; eauto. Qed.
  Lemma Forall2_Forall_r (Q : B → Prop) l k :
    Forall2 P l k → Forall (λ x, ∀ y, P x y → Q y) l → Forall Q k.
  Proof. induction 1; inversion_clear 1; eauto. Qed.

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

  Lemma Forall2_cons_inv x l y k :
    Forall2 P (x :: l) (y :: k) → P x y ∧ Forall2 P l k.
  Proof. by inversion 1. Qed.
  Lemma Forall2_cons_inv_l x l k :
    Forall2 P (x :: l) k → ∃ y k', P x y ∧ Forall2 P l k' ∧ k = y :: k'.
  Proof. inversion 1; subst; eauto. Qed.
  Lemma Forall2_cons_inv_r l k y :
    Forall2 P l (y :: k) → ∃ x l', P x y ∧ Forall2 P l' k ∧ l = x :: l'.
  Proof. inversion 1; subst; eauto. Qed.
  Lemma Forall2_cons_nil_inv x l : Forall2 P (x :: l) [] → False.
  Proof. by inversion 1. Qed.
  Lemma Forall2_nil_cons_inv y k : Forall2 P [] (y :: k) → False.
  Proof. by inversion 1. Qed.

  Lemma Forall2_app_l l1 l2 k :
    Forall2 P l1 (take (length l1) k) → Forall2 P l2 (drop (length l1) k) →
    Forall2 P (l1 ++ l2) k.
  Proof. intros. rewrite <-(take_drop (length l1) k). by apply Forall2_app. Qed.
  Lemma Forall2_app_r l k1 k2 :
    Forall2 P (take (length k1) l) k1 → Forall2 P (drop (length k1) l) k2 →
    Forall2 P l (k1 ++ k2).
  Proof. intros. rewrite <-(take_drop (length k1) l). by apply Forall2_app. Qed.
  Lemma Forall2_app_inv l1 l2 k1 k2 :
    length l1 = length k1 →
    Forall2 P (l1 ++ l2) (k1 ++ k2) → Forall2 P l1 k1 ∧ Forall2 P l2 k2.
  Proof.
    rewrite <-Forall2_same_length. induction 1; inversion 1; naive_solver.
  Qed.
  Lemma Forall2_app_inv_l l1 l2 k :
    Forall2 P (l1 ++ l2) k ↔
      ∃ k1 k2, Forall2 P l1 k1 ∧ Forall2 P l2 k2 ∧ k = k1 ++ k2.
  Proof.
    split; [|intros (?&?&?&?&->); by apply Forall2_app].
    revert k. induction l1; inversion 1; naive_solver.
  Qed.
  Lemma Forall2_app_inv_r l k1 k2 :
    Forall2 P l (k1 ++ k2) ↔
      ∃ l1 l2, Forall2 P l1 k1 ∧ Forall2 P l2 k2 ∧ l = l1 ++ l2.
  Proof.
    split; [|intros (?&?&?&?&->); by apply Forall2_app].
    revert l. induction k1; inversion 1; naive_solver.
  Qed.

  Lemma Forall2_tail l k : Forall2 P l k → Forall2 P (tail l) (tail k).
  Proof. destruct 1; simpl; auto. Qed.
  Lemma Forall2_take l k n : Forall2 P l k → Forall2 P (take n l) (take n k).
  Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
  Lemma Forall2_drop l k n : Forall2 P l k → Forall2 P (drop n l) (drop n k).
  Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.

  Lemma Forall2_lookup l k :
    Forall2 P l k ↔ ∀ i, option_Forall2 P (l !! i) (k !! i).
  Proof.
    split; [induction 1; intros [|?]; simpl; try constructor; eauto|].
    revert k. induction l as [|x l IH]; intros [| y k] H.
    - done.
    - feed inversion (H 0).
    - feed inversion (H 0).
    - constructor; [by feed inversion (H 0)|]. apply (IH _ $ λ i, H (S i)).
  Qed.
  Lemma Forall2_lookup_lr l k i x y :
    Forall2 P l k → l !! i = Some x → k !! i = Some y → P x y.
  Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
  Lemma Forall2_lookup_l l k i x :
    Forall2 P l k → l !! i = Some x → ∃ y, k !! i = Some y ∧ P x y.
  Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
  Lemma Forall2_lookup_r l k i y :
    Forall2 P l k → k !! i = Some y → ∃ x, l !! i = Some x ∧ P x y.
  Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
  Lemma Forall2_same_length_lookup_2 l k :
    length l = length k →
    (∀ i x y, l !! i = Some x → k !! i = Some y → P x y) → Forall2 P l k.
  Proof.
    rewrite <-Forall2_same_length. intros Hl Hlookup.
    induction Hl as [|?????? IH]; constructor; [by apply (Hlookup 0)|].
    apply IH. apply (λ i, Hlookup (S i)).
  Qed.
  Lemma Forall2_same_length_lookup l k :
    Forall2 P l k ↔
      length l = length k ∧
      (∀ i x y, l !! i = Some x → k !! i = Some y → P x y).
  Proof.
    naive_solver eauto using Forall2_length,
      Forall2_lookup_lr, Forall2_same_length_lookup_2.
  Qed.

  Lemma Forall2_alter_l f l k i :
    Forall2 P l k →
    (∀ x y, l !! i = Some x → k !! i = Some y → P x y → P (f x) y) →
    Forall2 P (alter f i l) k.
  Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
  Lemma Forall2_alter_r f l k i :
    Forall2 P l k →
    (∀ x y, l !! i = Some x → k !! i = Some y → P x y → P x (f y)) →
    Forall2 P l (alter f i k).
  Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
  Lemma Forall2_alter f g l k i :
    Forall2 P l k →
    (∀ x y, l !! i = Some x → k !! i = Some y → P x y → P (f x) (g y)) →
    Forall2 P (alter f i l) (alter g i k).
  Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.

  Lemma Forall2_insert l k x y i :
    Forall2 P l k → P x y → Forall2 P (<[i:=x]> l) (<[i:=y]> k).
  Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
  Lemma Forall2_inserts l k l' k' i :
    Forall2 P l k → Forall2 P l' k' →
    Forall2 P (list_inserts i l' l) (list_inserts i k' k).
  Proof. intros ? H. revert i. induction H; eauto using Forall2_insert. Qed.

  Lemma Forall2_delete l k i :
    Forall2 P l k → Forall2 P (delete i l) (delete i k).
  Proof. intros Hl. revert i. induction Hl; intros [|]; simpl; intuition. Qed.
  Lemma Forall2_option_list mx my :
    option_Forall2 P mx my → Forall2 P (option_list mx) (option_list my).
  Proof. destruct 1; by constructor. Qed.

  Lemma Forall2_filter Q1 Q2 `{∀ x, Decision (Q1 x), ∀ y, Decision (Q2 y)} l k:
    (∀ x y, P x y → Q1 x ↔ Q2 y) →
    Forall2 P l k → Forall2 P (filter Q1 l) (filter Q2 k).
  Proof.
    intros HP; induction 1 as [|x y l k]; unfold filter; simpl; auto.
    simplify_option_eq by (by rewrite <-(HP x y)); repeat constructor; auto.
  Qed.

  Lemma Forall2_replicate_l k n x :
    length k = n → Forall (P x) k → Forall2 P (replicate n x) k.
  Proof. intros <-. induction 1; simpl; auto. Qed.
  Lemma Forall2_replicate_r l n y :
    length l = n → Forall (flip P y) l → Forall2 P l (replicate n y).
  Proof. intros <-. induction 1; simpl; auto. Qed.
  Lemma Forall2_replicate n x y :
    P x y → Forall2 P (replicate n x) (replicate n y).
  Proof. induction n; simpl; constructor; auto. Qed.

  Lemma Forall2_reverse l k : Forall2 P l k → Forall2 P (reverse l) (reverse k).
  Proof.
    induction 1; rewrite ?reverse_nil, ?reverse_cons; eauto using Forall2_app.
  Qed.
  Lemma Forall2_last l k : Forall2 P l k → option_Forall2 P (last l) (last k).
  Proof. induction 1 as [|????? []]; simpl; repeat constructor; auto. Qed.

  Lemma Forall2_resize l k x y n :
    P x y → Forall2 P l k → Forall2 P (resize n x l) (resize n y k).
  Proof.
    intros. rewrite !resize_spec, (Forall2_length l k) by done.
    auto using Forall2_app, Forall2_take, Forall2_replicate.
  Qed.
  Lemma Forall2_resize_l l k x y n m :
    P x y → Forall (flip P y) l →
    Forall2 P (resize n x l) k → Forall2 P (resize m x l) (resize m y k).
  Proof.
    intros. destruct (decide (m ≤ n)).
    { rewrite <-(resize_resize l m n) by done. by apply Forall2_resize. }
    intros. assert (n = length k); subst.
    { by rewrite <-(Forall2_length (resize n x l) k), resize_length. }
    rewrite (le_plus_minus (length k) m), !resize_plus,
      resize_all, drop_all, resize_nil by lia.
    auto using Forall2_app, Forall2_replicate_r,
      Forall_resize, Forall_drop, resize_length.
  Qed.
  Lemma Forall2_resize_r l k x y n m :
    P x y → Forall (P x) k →
    Forall2 P l (resize n y k) → Forall2 P (resize m x l) (resize m y k).
  Proof.
    intros. destruct (decide (m ≤ n)).
    { rewrite <-(resize_resize k m n) by done. by apply Forall2_resize. }
    assert (n = length l); subst.
    { by rewrite (Forall2_length l (resize n y k)), resize_length. }
    rewrite (le_plus_minus (length l) m), !resize_plus,
      resize_all, drop_all, resize_nil by lia.
    auto using Forall2_app, Forall2_replicate_l,
      Forall_resize, Forall_drop, resize_length.
  Qed.
  Lemma Forall2_resize_r_flip l k x y n m :
    P x y → Forall (P x) k →
    length k = m → Forall2 P l (resize n y k) → Forall2 P (resize m x l) k.
  Proof.
    intros ?? <- ?. rewrite <-(resize_all k y) at 2.
    apply Forall2_resize_r with n; auto using Forall_true.
  Qed.

  Lemma Forall2_sublist_lookup_l l k n i l' :
    Forall2 P l k → sublist_lookup n i l = Some l' →
    ∃ k', sublist_lookup n i k = Some k' ∧ Forall2 P l' k'.
  Proof.
    unfold sublist_lookup. intros Hlk Hl.
    exists (take i (drop n k)); simplify_option_eq.
    - auto using Forall2_take, Forall2_drop.
    - apply Forall2_length in Hlk; lia.
  Qed.
  Lemma Forall2_sublist_lookup_r l k n i k' :
    Forall2 P l k → sublist_lookup n i k = Some k' →
    ∃ l', sublist_lookup n i l = Some l' ∧ Forall2 P l' k'.
  Proof.
    intro. unfold sublist_lookup.
    erewrite Forall2_length by eauto; intros; simplify_option_eq.
    eauto using Forall2_take, Forall2_drop.
  Qed.
  Lemma Forall2_sublist_alter f g l k i n l' k' :
    Forall2 P l k → sublist_lookup i n l = Some l' →
    sublist_lookup i n k = Some k' → Forall2 P (f l') (g k') →
    Forall2 P (sublist_alter f i n l) (sublist_alter g i n k).
  Proof.
    intro. unfold sublist_alter, sublist_lookup.
    erewrite Forall2_length by eauto; intros; simplify_option_eq.
    auto using Forall2_app, Forall2_drop, Forall2_take.
  Qed.
  Lemma Forall2_sublist_alter_l f l k i n l' k' :
    Forall2 P l k → sublist_lookup i n l = Some l' →
    sublist_lookup i n k = Some k' → Forall2 P (f l') k' →
    Forall2 P (sublist_alter f i n l) k.
  Proof.
    intro. unfold sublist_lookup, sublist_alter.
    erewrite <-Forall2_length by eauto; intros; simplify_option_eq.
    apply Forall2_app_l;
      rewrite ?take_length_le by lia; auto using Forall2_take.
    apply Forall2_app_l; erewrite Forall2_length, take_length,
      drop_length, <-Forall2_length, Min.min_l by eauto with lia; [done|].
    rewrite drop_drop; auto using Forall2_drop.
  Qed.

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

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

  Global Instance: Reflexive R → Reflexive (Forall2 R).
  Proof. intros ? l. induction l; by constructor. Qed.
  Global Instance: Symmetric R → Symmetric (Forall2 R).
  Proof. intros. induction 1; constructor; auto. Qed.
  Global Instance: Transitive R → Transitive (Forall2 R).
  Proof. intros ????. apply Forall2_transitive. by apply @transitivity. Qed.
  Global Instance: Equivalence R → Equivalence (Forall2 R).
  Proof. split; apply _. Qed.
  Global Instance: PreOrder R → PreOrder (Forall2 R).
  Proof. split; apply _. Qed.
  Global Instance: AntiSymm (=) R → AntiSymm (=) (Forall2 R).
  Proof. induction 2; inversion_clear 1; f_equal; auto. Qed.

  Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (::).
  Proof. by constructor. Qed.
  Global Instance: Proper (Forall2 R ==> Forall2 R ==> Forall2 R) (++).
  Proof. repeat intro. by apply Forall2_app. Qed.
  Global Instance: Proper (Forall2 R ==> (=)) length.
  Proof. repeat intro. eauto using Forall2_length. Qed.
  Global Instance: Proper (Forall2 R ==> Forall2 R) tail.
  Proof. repeat intro. eauto using Forall2_tail. Qed.
  Global Instance: Proper (Forall2 R ==> Forall2 R) (take n).
  Proof. repeat intro. eauto using Forall2_take. Qed.
  Global Instance: Proper (Forall2 R ==> Forall2 R) (drop n).
  Proof. repeat intro. eauto using Forall2_drop. Qed.

  Global Instance: Proper (Forall2 R ==> option_Forall2 R) (lookup i).
  Proof. repeat intro. by apply Forall2_lookup. Qed.
  Global Instance:
    Proper (R ==> R) f → Proper (Forall2 R ==> Forall2 R) (alter f i).
  Proof. repeat intro. eauto using Forall2_alter. Qed.
  Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (insert i).
  Proof. repeat intro. eauto using Forall2_insert. Qed.
  Global Instance:
    Proper (Forall2 R ==> Forall2 R ==> Forall2 R) (list_inserts i).
  Proof. repeat intro. eauto using Forall2_inserts. Qed.
  Global Instance: Proper (Forall2 R ==> Forall2 R) (delete i).
  Proof. repeat intro. eauto using Forall2_delete. Qed.

  Global Instance: Proper (option_Forall2 R ==> Forall2 R) option_list.
  Proof. repeat intro. eauto using Forall2_option_list. Qed.
  Global Instance: ∀ P `{∀ x, Decision (P x)},
    Proper (R ==> iff) P → Proper (Forall2 R ==> Forall2 R) (filter P).
  Proof. repeat intro; eauto using Forall2_filter. Qed.

  Global Instance: Proper (R ==> Forall2 R) (replicate n).
  Proof. repeat intro. eauto using Forall2_replicate. Qed.
  Global Instance: Proper (Forall2 R ==> Forall2 R) reverse.
  Proof. repeat intro. eauto using Forall2_reverse. Qed.
  Global Instance: Proper (Forall2 R ==> option_Forall2 R) last.
  Proof. repeat intro. eauto using Forall2_last. Qed.
  Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (resize n).
  Proof. repeat intro. eauto using Forall2_resize. Qed.
End Forall2_proper.

Section Forall3.
  Context {A B C} (P : A → B → C → Prop).
  Hint Extern 0 (Forall3 _ _ _ _) => constructor.

  Lemma Forall3_app l1 l2 k1 k2 k1' k2' :
    Forall3 P l1 k1 k1' → Forall3 P l2 k2 k2' →
    Forall3 P (l1 ++ l2) (k1 ++ k2) (k1' ++ k2').
  Proof. induction 1; simpl; auto. Qed.
  Lemma Forall3_cons_inv_l x l k k' :
    Forall3 P (x :: l) k k' → ∃ y k2 z k2',
      k = y :: k2 ∧ k' = z :: k2' ∧ P x y z ∧ Forall3 P l k2 k2'.
  Proof. inversion_clear 1; naive_solver. Qed.
  Lemma Forall3_app_inv_l l1 l2 k k' :
    Forall3 P (l1 ++ l2) k k' → ∃ k1 k2 k1' k2',
     k = k1 ++ k2 ∧ k' = k1' ++ k2' ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
  Proof.
    revert k k'. induction l1 as [|x l1 IH]; simpl; inversion_clear 1.
    - by repeat eexists; eauto.
    - by repeat eexists; eauto.
    - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
  Qed.
  Lemma Forall3_cons_inv_m l y k k' :
    Forall3 P l (y :: k) k' → ∃ x l2 z k2',
      l = x :: l2 ∧ k' = z :: k2' ∧ P x y z ∧ Forall3 P l2 k k2'.
  Proof. inversion_clear 1; naive_solver. Qed.
  Lemma Forall3_app_inv_m l k1 k2 k' :
    Forall3 P l (k1 ++ k2) k' → ∃ l1 l2 k1' k2',
     l = l1 ++ l2 ∧ k' = k1' ++ k2' ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
  Proof.
    revert l k'. induction k1 as [|x k1 IH]; simpl; inversion_clear 1.
    - by repeat eexists; eauto.
    - by repeat eexists; eauto.
    - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
  Qed.
  Lemma Forall3_cons_inv_r l k z k' :
    Forall3 P l k (z :: k') → ∃ x l2 y k2,
      l = x :: l2 ∧ k = y :: k2 ∧ P x y z ∧ Forall3 P l2 k2 k'.
  Proof. inversion_clear 1; naive_solver. Qed.
  Lemma Forall3_app_inv_r l k k1' k2' :
    Forall3 P l k (k1' ++ k2') → ∃ l1 l2 k1 k2,
      l = l1 ++ l2 ∧ k = k1 ++ k2 ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
  Proof.
    revert l k. induction k1' as [|x k1' IH]; simpl; inversion_clear 1.
    - by repeat eexists; eauto.
    - by repeat eexists; eauto.
    - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
  Qed.
  Lemma Forall3_impl (Q : A → B → C → Prop) l k k' :
    Forall3 P l k k' → (∀ x y z, P x y z → Q x y z) → Forall3 Q l k k'.
  Proof. intros Hl ?; induction Hl; auto. Defined.
  Lemma Forall3_length_lm l k k' : Forall3 P l k k' → length l = length k.
  Proof. by induction 1; f_equal/=. Qed.
  Lemma Forall3_length_lr l k k' : Forall3 P l k k' → length l = length k'.
  Proof. by induction 1; f_equal/=. Qed.
  Lemma Forall3_lookup_lmr l k k' i x y z :
    Forall3 P l k k' →
    l !! i = Some x → k !! i = Some y → k' !! i = Some z → P x y z.
  Proof.
    intros H. revert i. induction H; intros [|?] ???; simplify_eq/=; eauto.
  Qed.
  Lemma Forall3_lookup_l l k k' i x :
    Forall3 P l k k' → l !! i = Some x →
    ∃ y z, k !! i = Some y ∧ k' !! i = Some z ∧ P x y z.
  Proof.
    intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
  Qed.
  Lemma Forall3_lookup_m l k k' i y :
    Forall3 P l k k' → k !! i = Some y →
    ∃ x z, l !! i = Some x ∧ k' !! i = Some z ∧ P x y z.
  Proof.
    intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
  Qed.
  Lemma Forall3_lookup_r l k k' i z :
    Forall3 P l k k' → k' !! i = Some z →
    ∃ x y, l !! i = Some x ∧ k !! i = Some y ∧ P x y z.
  Proof.
    intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
  Qed.
  Lemma Forall3_alter_lm f g l k k' i :
    Forall3 P l k k' →
    (∀ x y z, l !! i = Some x → k !! i = Some y → k' !! i = Some z →
      P x y z → P (f x) (g y) z) →
    Forall3 P (alter f i l) (alter g i k) k'.
  Proof. intros Hl. revert i. induction Hl; intros [|]; auto. Qed.
End Forall3.

(** Setoids *)
Section setoid.
  Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
  Implicit Types l k : list A.

  Lemma equiv_Forall2 l k : l ≡ k ↔ Forall2 (≡) l k.
  Proof. split; induction 1; constructor; auto. Qed.
  Lemma list_equiv_lookup l k : l ≡ k ↔ ∀ i, l !! i ≡ k !! i.
  Proof.
    rewrite equiv_Forall2, Forall2_lookup.
    by setoid_rewrite equiv_option_Forall2.
  Qed.

  Global Instance list_equivalence : Equivalence ((≡) : relation (list A)).
  Proof.
    split.
    - intros l. by apply equiv_Forall2.
    - intros l k; rewrite !equiv_Forall2; by intros.
    - intros l1 l2 l3; rewrite !equiv_Forall2; intros; by trans l2.
  Qed.
  Global Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A).
  Proof. induction 1; f_equal; fold_leibniz; auto. Qed.

  Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
  Proof. by constructor. Qed.
  Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A).
  Proof. induction 1; intros ???; simpl; try constructor; auto. Qed.
  Global Instance length_proper : Proper ((≡) ==> (=)) (@length A).
  Proof. induction 1; f_equal/=; auto. Qed.
  Global Instance tail_proper : Proper ((≡) ==> (≡)) (@tail A).
  Proof. by destruct 1. Qed.
  Global Instance take_proper n : Proper ((≡) ==> (≡)) (@take A n).
  Proof. induction n; destruct 1; constructor; auto. Qed.
  Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n).
  Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
  Global Instance list_lookup_proper i :
    Proper ((≡) ==> (≡)) (lookup (M:=list A) i).
  Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed.
  Global Instance list_alter_proper f i :
    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
  Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
  Global Instance list_insert_proper i :
    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) i).
  Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
  Global Instance list_inserts_proper i :
    Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i).
  Proof.
    intros k1 k2 Hk; revert i.
    induction Hk; intros ????; simpl; try f_equiv; naive_solver.
  Qed.
  Global Instance list_delete_proper i :
    Proper ((≡) ==> (≡)) (delete (M:=list A) i).
  Proof. induction i; destruct 1; try constructor; eauto. Qed.
  Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A).
  Proof. destruct 1; by constructor. Qed.
  Global Instance list_filter_proper P `{∀ x, Decision (P x)} :
    Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡)) (filter (B:=list A) P).
  Proof. intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
  Global Instance replicate_proper n : Proper ((≡) ==> (≡)) (@replicate A n).
  Proof. induction n; constructor; auto. Qed.
  Global Instance reverse_proper : Proper ((≡) ==> (≡)) (@reverse A).
  Proof. induction 1; rewrite ?reverse_cons; repeat (done || f_equiv). Qed.
  Global Instance last_proper : Proper ((≡) ==> (≡)) (@last A).
  Proof. induction 1 as [|????? []]; simpl; repeat (done || f_equiv). Qed.
  Global Instance resize_proper n : Proper ((≡) ==> (≡) ==> (≡)) (@resize A n).
  Proof. induction n; destruct 2; simpl; repeat (auto || f_equiv). Qed.
End setoid.

(** * Properties of the monadic operations *)
Section fmap.
  Context {A B : Type} (f : A → B).

  Lemma list_fmap_id (l : list A) : id <$> l = l.
  Proof. induction l; f_equal/=; auto. Qed.
  Lemma list_fmap_compose {C} (g : B → C) l : g ∘ f <$> l = g <$> f <$> l.
  Proof. induction l; f_equal/=; auto. Qed.
  Lemma list_fmap_ext (g : A → B) (l1 l2 : list A) :
    (∀ x, f x = g x) → l1 = l2 → fmap f l1 = fmap g l2.
  Proof. intros ? <-. induction l1; f_equal/=; auto. Qed.
  Lemma list_fmap_setoid_ext `{Equiv B} (g : A → B) l :
    (∀ x, f x ≡ g x) → f <$> l ≡ g <$> l.
  Proof. induction l; constructor; auto. Qed.

  Global Instance: Inj (=) (=) f → Inj (=) (=) (fmap f).
  Proof.
    intros ? l1. induction l1 as [|x l1 IH]; [by intros [|??]|].
    intros [|??]; intros; f_equal/=; simplify_eq; auto.
  Qed.

  Definition fmap_nil : f <$> [] = [] := eq_refl.
  Definition fmap_cons x l : f <$> x :: l = f x :: f <$> l := eq_refl.

  Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
  Proof. by induction l1; f_equal/=. Qed.
  Lemma fmap_nil_inv k :  f <$> k = [] → k = [].
  Proof. by destruct k. Qed.
  Lemma fmap_cons_inv y l k :
    f <$> l = y :: k → ∃ x l', y = f x ∧ k = f <$> l' ∧ l = x :: l'.
  Proof. intros. destruct l; simplify_eq/=; eauto. Qed.
  Lemma fmap_app_inv l k1 k2 :
    f <$> l = k1 ++ k2 → ∃ l1 l2, k1 = f <$> l1 ∧ k2 = f <$> l2 ∧ l = l1 ++ l2.
  Proof.
    revert l. induction k1 as [|y k1 IH]; simpl; [intros l ?; by eexists [],l|].
    intros [|x l] ?; simplify_eq/=.
    destruct (IH l) as (l1&l2&->&->&->); [done|]. by exists (x :: l1), l2.
  Qed.

  Lemma fmap_length l : length (f <$> l) = length l.
  Proof. by induction l; f_equal/=. Qed.
  Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
  Proof.
    induction l as [|?? IH]; csimpl; by rewrite ?reverse_cons, ?fmap_app, ?IH.
  Qed.
  Lemma fmap_tail l : f <$> tail l = tail (f <$> l).
  Proof. by destruct l. Qed.
  Lemma fmap_last l : last (f <$> l) = f <$> last l.
  Proof. induction l as [|? []]; simpl; auto. Qed.
  Lemma fmap_replicate n x :  f <$> replicate n x = replicate n (f x).
  Proof. by induction n; f_equal/=. Qed.
  Lemma fmap_take n l : f <$> take n l = take n (f <$> l).
  Proof. revert n. by induction l; intros [|?]; f_equal/=. Qed.
  Lemma fmap_drop n l : f <$> drop n l = drop n (f <$> l).
  Proof. revert n. by induction l; intros [|?]; f_equal/=. Qed.
  Lemma fmap_resize n x l : f <$> resize n x l = resize n (f x) (f <$> l).
  Proof.
    revert n. induction l; intros [|?]; f_equal/=; auto using fmap_replicate.
  Qed.
  Lemma const_fmap (l : list A) (y : B) :
    (∀ x, f x = y) → f <$> l = replicate (length l) y.
  Proof. intros; induction l; 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 y ∧ l !! i = Some y.
  Proof.
    intros Hi. rewrite list_lookup_fmap in Hi.
    destruct (l !! i) eqn:?; simplify_eq/=; eauto.
  Qed.
  Lemma list_alter_fmap (g : A → A) (h : B → B) l i :
    Forall (λ x, f (g x) = h (f x)) l → f <$> alter g i l = alter h i (f <$> l).
  Proof. intros Hl. revert i. by induction Hl; intros [|i]; f_equal/=. Qed.

  Lemma elem_of_list_fmap_1 l x : x ∈ l → f x ∈ f <$> l.
  Proof. induction 1; csimpl; rewrite elem_of_cons; intuition. Qed.
  Lemma elem_of_list_fmap_1_alt l x y : x ∈ l → y = f x → y ∈ f <$> l.
  Proof. intros. subst. by apply elem_of_list_fmap_1. Qed.
  Lemma elem_of_list_fmap_2 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
  Proof.
    induction l as [|y l IH]; simpl; inversion_clear 1.
    - 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 : x ∈ f <$> l ↔ ∃ y, x = f y ∧ y ∈  l.
  Proof.
    naive_solver eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
  Qed.

  Lemma NoDup_fmap_1 l : 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 `{!Inj (=) (=) f} l : NoDup l → NoDup (f <$> l).
  Proof.
    induction 1; simpl; constructor; trivial. rewrite elem_of_list_fmap.
    intros [y [Hxy ?]]. apply (inj f) in Hxy. by subst.
  Qed.
  Lemma NoDup_fmap `{!Inj (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
  Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.

  Global Instance fmap_sublist: Proper (sublist ==> sublist) (fmap f).
  Proof. induction 1; simpl; econstructor; eauto. Qed.
  Global Instance fmap_contains: Proper (contains ==> contains) (fmap f).
  Proof. induction 1; simpl; econstructor; eauto. Qed.
  Global Instance fmap_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (fmap f).
  Proof. induction 1; simpl; econstructor; eauto. Qed.

  Lemma Forall_fmap_ext_1 (g : A → B) (l : list A) :
    Forall (λ x, f x = g x) l → fmap f l = fmap g l.
  Proof. by induction 1; f_equal/=. Qed.
  Lemma Forall_fmap_ext (g : A → B) (l : list A) :
    Forall (λ x, f x = g x) l ↔ fmap f l = fmap g l.
  Proof.
    split; [auto using Forall_fmap_ext_1|].
    induction l; simpl; constructor; simplify_eq; auto.
  Qed.
  Lemma Forall_fmap (P : B → Prop) l : Forall P (f <$> l) ↔ Forall (P ∘ f) l.
  Proof. split; induction l; inversion_clear 1; constructor; auto. Qed.
  Lemma Exists_fmap (P : B → Prop) l : Exists P (f <$> l) ↔ Exists (P ∘ f) l.
  Proof. split; induction l; inversion 1; constructor; by auto. Qed.

  Lemma Forall2_fmap_l {C} (P : B → C → Prop) l1 l2 :
    Forall2 P (f <$> l1) l2 ↔ Forall2 (P ∘ f) l1 l2.
  Proof.
    split; revert l2; induction l1; inversion_clear 1; constructor; auto.
  Qed.
  Lemma Forall2_fmap_r {C} (P : C → B → Prop) l1 l2 :
    Forall2 P l1 (f <$> l2) ↔ Forall2 (λ x, P x ∘ f) l1 l2.
  Proof.
    split; revert l1; induction l2; inversion_clear 1; constructor; auto.
  Qed.
  Lemma Forall2_fmap_1 {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
    Forall2 P (f <$> l1) (g <$> l2) → Forall2 (λ x1 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 : C → D) (P : B → D → Prop) l1 l2 :
    Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2 → Forall2 P (f <$> l1) (g <$> l2).
  Proof. induction 1; csimpl; auto. Qed.
  Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
    Forall2 P (f <$> l1) (g <$> l2) ↔ Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
  Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.

  Lemma list_fmap_bind {C} (g : B → list C) l : (f <$> l) ≫= g = l ≫= g ∘ f.
  Proof. by induction l; f_equal/=. Qed.
End fmap.

Lemma list_alter_fmap_mono {A} (f : A → A) (g : A → A) l i :
  Forall (λ x, f (g x) = g (f x)) l → f <$> alter g i l = alter g i (f <$> l).
Proof. auto using list_alter_fmap. Qed.
Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
  (∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ l → y1 = y2) → NoDup l → NoDup (l.*1).
Proof.
  intros Hunique. induction 1 as [|[x1 y1] l Hin Hnodup IH]; csimpl; 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 bind.
  Context {A B : Type} (f : A → list B).

  Lemma list_bind_ext (g : A → list B) l1 l2 :
    (∀ x, f x = g x) → l1 = l2 → l1 ≫= f = l2 ≫= g.
  Proof. intros ? <-. by induction l1; f_equal/=. Qed.
  Lemma Forall_bind_ext (g : A → list B) (l : list A) :
    Forall (λ x, f x = g x) l → l ≫= f = l ≫= g.
  Proof. by induction 1; f_equal/=. Qed.
  Global Instance bind_sublist: Proper (sublist ==> sublist) (mbind f).
  Proof.
    induction 1; simpl; auto;
      [by apply sublist_app|by apply sublist_inserts_l].
  Qed.
  Global Instance bind_contains: Proper (contains ==> contains) (mbind f).
  Proof.
    induction 1; csimpl; auto.
    - by apply contains_app.
    - by rewrite !(assoc_L (++)), (comm (++) (f _)).
    - by apply contains_inserts_l.
    - etrans; eauto.
  Qed.
  Global Instance bind_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (mbind f).
  Proof.
    induction 1; csimpl; auto.
    - by f_equiv.
    - by rewrite !(assoc_L (++)), (comm (++) (f _)).
    - etrans; eauto.
  Qed.
  Lemma bind_cons x l : (x :: l) ≫= f = f x ++ l ≫= f.
  Proof. done. Qed.
  Lemma bind_singleton x : [x] ≫= f = f x.
  Proof. csimpl. by rewrite (right_id_L _ (++)). Qed.
  Lemma bind_app l1 l2 : (l1 ++ l2) ≫= f = (l1 ≫= f) ++ (l2 ≫= f).
  Proof. by induction l1; csimpl; rewrite <-?(assoc_L (++)); f_equal. Qed.
  Lemma elem_of_list_bind (x : B) (l : list A) :
    x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
  Proof.
    split.
    - induction l as [|y l IH]; csimpl; [inversion 1|].
      rewrite elem_of_app. intros [?|?].
      + exists y. split; [done | by left].
      + destruct IH as [z [??]]. done. exists z. split; [done | by right].
    - intros [y [Hx Hy]]. induction Hy; csimpl; rewrite elem_of_app; intuition.
  Qed.
  Lemma Forall_bind (P : B → Prop) l :
    Forall P (l ≫= f) ↔ Forall (Forall P ∘ f) l.
  Proof.
    split.
    - induction l; csimpl; rewrite ?Forall_app; constructor; csimpl; intuition.
    - induction 1; csimpl; rewrite ?Forall_app; auto.
  Qed.
  Lemma Forall2_bind {C D} (g : C → list D) (P : B → D → Prop) l1 l2 :
    Forall2 (λ x1 x2, Forall2 P (f x1) (g x2)) l1 l2 →
    Forall2 P (l1 ≫= f) (l2 ≫= g).
  Proof. induction 1; csimpl; auto using Forall2_app. Qed.
End bind.

Section ret_join.
  Context {A : Type}.

  Lemma list_join_bind (ls : list (list A)) : mjoin ls = ls ≫= id.
  Proof. by induction ls; f_equal/=. Qed.
  Global Instance mjoin_Permutation:
    Proper (@Permutation (list A) ==> (≡ₚ)) mjoin.
  Proof. intros ?? E. by rewrite !list_join_bind, E. Qed.
  Lemma elem_of_list_ret (x y : A) : x ∈ @mret list _ A y ↔ x = y.
  Proof. apply elem_of_list_singleton. Qed.
  Lemma elem_of_list_join (x : A) (ls : list (list A)) :
    x ∈ mjoin ls ↔ ∃ l, x ∈ l ∧ l ∈ ls.
  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 1 as [|[|??] ?]].
    by induction ls as [|[|??] ?]; constructor; auto.
  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 (= []) ls → mjoin ls = [].
  Proof. by rewrite join_nil. Qed.
  Lemma Forall_join (P : A → Prop) (ls: list (list A)) :
    Forall (Forall P) ls → Forall P (mjoin ls).
  Proof. induction 1; simpl; auto using Forall_app_2. Qed.
  Lemma Forall2_join {B} (P : A → B → Prop) ls1 ls2 :
    Forall2 (Forall2 P) ls1 ls2 → Forall2 P (mjoin ls1) (mjoin ls2).
  Proof. induction 1; simpl; auto using Forall2_app. Qed.
End ret_join.