phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_monad.v *)
Lemma fmap_take n l : f <$> take n l = take n (f <$> l).
Proof. revert n. by induction l; intros [|?]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma fmap_drop n l : f <$> drop n l = drop n (f <$> l).
Proof. revert n. by induction l; intros [|?]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma const_fmap (l : list A) (y : B) :
    (∀ i x, l !! i = Some x → f x = y) →
    f <$> l = replicate (length l) y.
Proof. rewrite <-Forall_lookup. induction 1; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
Proof. revert i. induction l; intros [|n]; by try revert n. Qed.
(* stdpp/list_monad.v *)
Lemma list_lookup_total_fmap `{!Inhabited A, !Inhabited B} l i :
    i < length l → (f <$> l) !!! i = f (l !!! i).
Proof.
    intros [x Hx]%lookup_lt_is_Some_2.
    by rewrite !list_lookup_total_alt, list_lookup_fmap, Hx.
  Qed.
(* stdpp/list_monad.v *)
Lemma list_lookup_fmap_Some l i y :
    (f <$> l) !! i = Some y ↔ ∃ x, y = f x ∧ l !! i = Some x.
Proof. rewrite list_lookup_fmap, fmap_Some. naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma list_lookup_fmap_Some_1 l i y :
    (f <$> l) !! i = Some y → ∃ x, y = f x ∧ l !! i = Some x.
Proof. by rewrite list_lookup_fmap_Some. Qed.
(* stdpp/list_monad.v *)
Lemma list_lookup_fmap_Some_2 l i x :
    l !! i = Some x → (f <$> l) !! i = Some (f x).
Proof. rewrite list_lookup_fmap_Some. naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma list_fmap_insert l i x: f <$> <[i:=x]>l = <[i:=f x]>(f <$> l).
Proof. revert i. by induction l; intros [|i]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma list_fmap_alter (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.
(* stdpp/list_monad.v *)
Lemma list_fmap_delete l i : f <$> (delete i l) = delete i (f <$> l).
Proof.
    revert i. induction l; intros i; destruct i; csimpl; eauto.
    naive_solver congruence.
  Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_fmap l y : y ∈ f <$> l ↔ ∃ x, y = f x ∧ x ∈ l.
Proof.
    setoid_rewrite list_elem_of_lookup. setoid_rewrite list_lookup_fmap_Some.
    naive_solver.
  Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_fmap_1 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
Proof. by rewrite list_elem_of_fmap. Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_fmap_2 l x : x ∈ l → f x ∈ f <$> l.
Proof. rewrite list_elem_of_fmap. naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_fmap_2' l x y : x ∈ l → y = f x → y ∈ f <$> l.
Proof. intros ? ->. by apply list_elem_of_fmap_2. Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_fmap_inj `{!Inj (=) (=) f} l x : f x ∈ f <$> l ↔ x ∈ l.
Proof. rewrite list_elem_of_fmap. naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_fmap_inj_2 `{!Inj (=) (=) f} l x : f x ∈ f <$> l → x ∈ l.
Proof. by rewrite list_elem_of_fmap_inj. Qed.
(* stdpp/list_monad.v *)
Lemma list_fmap_inj R1 R2 :
    Inj R1 R2 f → Inj (Forall2 R1) (Forall2 R2) (fmap f).
Proof.
    intros ? l1. induction l1; intros [|??]; inv 1; constructor; auto.
  Qed.
(* stdpp/list_monad.v *)
Instance list_fmap_eq_inj : Inj (=) (=) f → Inj (=@{list A}) (=) (fmap f).
Proof.
    intros ?%list_fmap_inj ?? ?%list_eq_Forall2%(inj _). by apply list_eq_Forall2.
  Qed.
(* stdpp/list_monad.v *)
Instance list_fmap_equiv_inj `{!Equiv A, !Equiv B} :
    Inj (≡) (≡) f → Inj (≡@{list A}) (≡) (fmap f).
Proof.
    intros ?%list_fmap_inj ?? ?%list_equiv_Forall2%(inj _).
    by apply list_equiv_Forall2.
  Qed.
(* stdpp/list_monad.v *)
(* A version of [NoDup_fmap_2] that does not require [f] to be injective for
      *all* inputs. *)
Lemma NoDup_fmap_2_strong l :
    (∀ x y, x ∈ l → y ∈ l → f x = f y → x = y) →
    NoDup l →
    NoDup (f <$> l).
Proof.
    intros Hinj. induction 1 as [|x l ?? IH]; simpl; constructor.
    - intros [y [Hxy ?]]%list_elem_of_fmap.
      apply Hinj in Hxy; [by subst|by constructor..].
    - apply IH. clear- Hinj.
      intros x' y Hx' Hy. apply Hinj; by constructor.
  Qed.
(* stdpp/list_monad.v *)
Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
Proof.
    induction l; simpl; inv 1; constructor; auto.
    rewrite list_elem_of_fmap in *. naive_solver.
  Qed.
(* stdpp/list_monad.v *)
Lemma NoDup_fmap_2 `{!Inj (=) (=) f} l : NoDup l → NoDup (f <$> l).
Proof. apply NoDup_fmap_2_strong. intros ?? _ _. apply (inj f). Qed.
(* stdpp/list_monad.v *)
Lemma NoDup_fmap `{!Inj (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
(* stdpp/list_monad.v *)
Instance fmap_sublist: Proper (sublist ==> sublist) (fmap f).
Proof. induction 1; simpl; econstructor; eauto. Qed.
(* stdpp/list_monad.v *)
Instance fmap_submseteq: Proper (submseteq ==> submseteq) (fmap f).
Proof. induction 1; simpl; econstructor; eauto. Qed.
(* stdpp/list_monad.v *)
Instance fmap_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (fmap f).
Proof. induction 1; simpl; econstructor; eauto. Qed.
(* stdpp/list_monad.v *)
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.
(* stdpp/list_monad.v *)
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.
(* stdpp/list_monad.v *)
Lemma Forall_fmap (P : B → Prop) l : Forall P (f <$> l) ↔ Forall (P ∘ f) l.
Proof. split; induction l; inv 1; constructor; auto. Qed.
(* stdpp/list_monad.v *)
Lemma Exists_fmap (P : B → Prop) l : Exists P (f <$> l) ↔ Exists (P ∘ f) l.
Proof. split; induction l; inv 1; constructor; by auto. Qed.
(* stdpp/list_monad.v *)
Lemma Forall2_fmap_l {C} (P : B → C → Prop) l k :
    Forall2 P (f <$> l) k ↔ Forall2 (P ∘ f) l k.
Proof.
    split; revert k; induction l; inv 1; constructor; auto.
  Qed.
(* stdpp/list_monad.v *)
Lemma Forall2_fmap_r {C} (P : C → B → Prop) k l :
    Forall2 P k (f <$> l) ↔ Forall2 (λ x, P x ∘ f) k l.
Proof.
    split; revert k; induction l; inv 1; constructor; auto.
  Qed.
(* stdpp/list_monad.v *)
Lemma Forall2_fmap_1 {C D} (g : C → D) (P : B → D → Prop) l k :
    Forall2 P (f <$> l) (g <$> k) → Forall2 (λ x1 x2, P (f x1) (g x2)) l k.
Proof. revert k; induction l; intros [|??]; inv 1; auto. Qed.
(* stdpp/list_monad.v *)
Lemma Forall2_fmap_2 {C D} (g : C → D) (P : B → D → Prop) l k :
    Forall2 (λ x1 x2, P (f x1) (g x2)) l k → Forall2 P (f <$> l) (g <$> k).
Proof. induction 1; csimpl; auto. Qed.
(* stdpp/list_monad.v *)
Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l k :
    Forall2 P (f <$> l) (g <$> k) ↔ Forall2 (λ x1 x2, P (f x1) (g x2)) l k.
Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
(* stdpp/list_monad.v *)
Lemma list_fmap_bind {C} (g : B → list C) l : (f <$> l) ≫= g = l ≫= g ∘ f.
Proof. by induction l; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma list_fmap_ext (f g : A → B) l :
    (∀ i x, l !! i = Some x → f x = g x) → f <$> l = g <$> l.
Proof.
    intros Hfg. apply list_eq; intros i. rewrite !list_lookup_fmap.
    destruct (l !! i) eqn:?; f_equal/=; eauto.
  Qed.
(* stdpp/list_monad.v *)
Lemma list_fmap_equiv_ext `{!Equiv B} (f g : A → B) l :
    (∀ i x, l !! i = Some x → f x ≡ g x) → f <$> l ≡ g <$> l.
Proof.
    intros Hl. apply list_equiv_lookup; intros i. rewrite !list_lookup_fmap.
    destruct (l !! i) eqn:?; simpl; constructor; eauto.
  Qed.
(* stdpp/list_monad.v *)
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 list_elem_of_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.
(* stdpp/list_monad.v *)
Instance list_omap_proper `{!Equiv A, !Equiv B} :
  Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) omap.
Proof.
  intros f1 f2 Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
  destruct (Hf _ _ Hx); by repeat f_equiv.
Qed.
(* stdpp/list_monad.v *)
Lemma list_fmap_omap {C} (g : B → C) l :
    g <$> omap f l = omap (λ x, g <$> (f x)) l.
Proof.
    induction l as [|x y IH]; [done|]. csimpl.
    destruct (f x); csimpl; [|done]. by f_equal.
  Qed.
(* stdpp/list_monad.v *)
Lemma list_omap_ext {A'} (g : A' → option B) l1 (l2 : list A') :
    Forall2 (λ a b, f a = g b) l1 l2 →
    omap f l1 = omap g l2.
Proof.
    induction 1 as [|x y l l' Hfg ? IH]; [done|].
    csimpl. rewrite Hfg. destruct (g y); [|done]. by f_equal.
  Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_omap l y : y ∈ omap f l ↔ ∃ x, x ∈ l ∧ f x = Some y.
Proof.
    split.
    - induction l as [|x l]; csimpl; repeat case_match;
        repeat (setoid_rewrite elem_of_nil || setoid_rewrite elem_of_cons);
        naive_solver.
    - intros (x&Hx&?). by induction Hx; csimpl; repeat case_match;
        simplify_eq; try constructor; auto.
  Qed.
(* stdpp/list_monad.v *)
Instance omap_Permutation : Proper ((≡ₚ) ==> (≡ₚ)) (omap f).
Proof. induction 1; simpl; repeat case_match; econstructor; eauto. Qed.
(* stdpp/list_monad.v *)
Lemma omap_app l1 l2 :
    omap f (l1 ++ l2) = omap f l1 ++ omap f l2.
Proof. induction l1; csimpl; repeat case_match; naive_solver congruence. Qed.
(* stdpp/list_monad.v *)
Lemma omap_option_list mx :
    omap f (option_list mx) = option_list (mx ≫= f).
Proof. by destruct mx. Qed.
(* stdpp/list_monad.v *)
Instance list_bind_proper `{!Equiv A, !Equiv B} :
  Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) mbind.
Proof. induction 2; csimpl; constructor || f_equiv; auto. Qed.
(* stdpp/list_monad.v *)
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.
(* stdpp/list_monad.v *)
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.
(* stdpp/list_monad.v *)
Instance bind_sublist: Proper (sublist ==> sublist) (mbind f).
Proof.
    induction 1; simpl; auto;
      [by apply sublist_app|by apply sublist_inserts_l].
  Qed.
(* stdpp/list_monad.v *)
Instance bind_submseteq: Proper (submseteq ==> submseteq) (mbind f).
Proof.
    induction 1; csimpl; auto.
    - by apply submseteq_app.
    - by rewrite !(assoc_L (++)), (comm (++) (f _)).
    - by apply submseteq_inserts_l.
    - etrans; eauto.
  Qed.
(* stdpp/list_monad.v *)
Instance bind_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (mbind f).
Proof.
    induction 1; csimpl; auto.
    - by f_equiv.
    - by rewrite !(assoc_L (++)), (comm (++) (f _)).
    - etrans; eauto.
  Qed.
(* stdpp/list_monad.v *)
Lemma bind_cons x l : (x :: l) ≫= f = f x ++ l ≫= f.
Proof. done. Qed.
(* stdpp/list_monad.v *)
Lemma bind_singleton x : [x] ≫= f = f x.
Proof. csimpl. by rewrite (right_id_L _ (++)). Qed.
(* stdpp/list_monad.v *)
Lemma bind_app l1 l2 : (l1 ++ l2) ≫= f = (l1 ≫= f) ++ (l2 ≫= f).
Proof. by induction l1; csimpl; rewrite <-?(assoc_L (++)); f_equal. Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_bind (x : B) (l : list A) :
    x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
Proof.
    split.
    - induction l as [|y l IH]; csimpl; [inv 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.
(* stdpp/list_monad.v *)
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.
(* stdpp/list_monad.v *)
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.
(* stdpp/list_monad.v *)
Lemma NoDup_bind l :
    (∀ x1 x2 y, x1 ∈ l → x2 ∈ l → y ∈ f x1 → y ∈ f x2 → x1 = x2) →
    (∀ x, x ∈ l → NoDup (f x)) → NoDup l → NoDup (l ≫= f).
Proof.
    intros Hinj Hf. induction 1 as [|x l ?? IH]; csimpl; [constructor|].
    apply NoDup_app. split_and!.
    - eauto 10 using list_elem_of_here.
    - intros y ? (x'&?&?)%list_elem_of_bind.
      destruct (Hinj x x' y); auto using list_elem_of_here, list_elem_of_further.
    - eauto 10 using list_elem_of_further.
  Qed.
(* stdpp/list_monad.v *)
(* ** Properties of [mjoin] on lists *)
Instance list_join_proper `{!Equiv A} :
  Proper ((≡) ==> (≡@{list A})) mjoin.
Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
(* stdpp/list_monad.v *)
Lemma list_join_bind (ls : list (list A)) : mjoin ls = ls ≫= id.
Proof. by induction ls; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Instance join_Permutation : Proper ((≡ₚ@{list A}) ==> (≡ₚ)) mjoin.
Proof. intros ?? E. by rewrite !list_join_bind, E. Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_ret (x y : A) : x ∈ @mret list _ A y ↔ x = y.
Proof. apply list_elem_of_singleton. Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_join (x : A) (ls : list (list A)) :
    x ∈ mjoin ls ↔ ∃ l : list A, x ∈ l ∧ l ∈ ls.
Proof. by rewrite list_join_bind, list_elem_of_bind. Qed.
(* stdpp/list_monad.v *)
Lemma join_nil (ls : list (list A)) : mjoin ls = [] ↔ Forall (.= []) ls.
Proof.
    split; [|by induction 1 as [|[|??] ?]].
    by induction ls as [|[|??] ?]; constructor; auto.
  Qed.
(* stdpp/list_monad.v *)
Lemma join_nil_1 (ls : list (list A)) : mjoin ls = [] → Forall (.= []) ls.
Proof. by rewrite join_nil. Qed.
(* stdpp/list_monad.v *)
Lemma join_nil_2 (ls : list (list A)) : Forall (.= []) ls → mjoin ls = [].
Proof. by rewrite join_nil. Qed.
(* stdpp/list_monad.v *)
Lemma join_cons (l : list A) ls : mjoin (l :: ls) = l ++ mjoin ls.
Proof. done. Qed.
(* stdpp/list_monad.v *)
Lemma join_app (l1 l2 : list (list A)) :
    mjoin (l1 ++ l2) = mjoin l1 ++ mjoin l2.
Proof.
    induction l1 as [|x l1 IH]; simpl; [done|]. by rewrite <-(assoc_L _ _), IH.
  Qed.
(* stdpp/list_monad.v *)
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.
(* stdpp/list_monad.v *)
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.
(* stdpp/list_monad.v *)
Instance mapM_proper `{!Equiv A, !Equiv B} :
  Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{option (list B)})) mapM.
Proof.
  induction 2; csimpl; repeat (f_equiv || constructor || intro || auto).
Qed.
(* stdpp/list_monad.v *)
Lemma mapM_ext (g : A → option B) l : (∀ x, f x = g x) → mapM f l = mapM g l.
Proof. intros Hfg. by induction l as [|?? IHl]; simpl; rewrite ?Hfg, ?IHl. Qed.
(* stdpp/list_monad.v *)
Lemma Forall2_mapM_ext (g : A → option B) l k :
    Forall2 (λ x y, f x = g y) l k → mapM f l = mapM g k.
Proof. induction 1 as [|???? Hfg ? IH]; simpl; [done|]. by rewrite Hfg, IH. Qed.
(* stdpp/list_monad.v *)
Lemma Forall_mapM_ext (g : A → option B) l :
    Forall (λ x, f x = g x) l → mapM f l = mapM g l.
Proof. induction 1 as [|?? Hfg ? IH]; simpl; [done|]. by rewrite Hfg, IH. Qed.
(* stdpp/list_monad.v *)
Lemma mapM_Some_1 l k : mapM f l = Some k → Forall2 (λ x y, f x = Some y) l k.
Proof.
    revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
    - destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
    - destruct (f x) eqn:?; intros; simplify_option_eq; auto.
  Qed.
(* stdpp/list_monad.v *)
Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k → mapM f l = Some k.
Proof.
    induction 1 as [|???? Hf ? IH]; simpl; [done |].
    rewrite Hf. simpl. by rewrite IH.
  Qed.
(* stdpp/list_monad.v *)
Lemma mapM_Some l k : mapM f l = Some k ↔ Forall2 (λ x y, f x = Some y) l k.
Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
(* stdpp/list_monad.v *)
Lemma length_mapM l k : mapM f l = Some k → length l = length k.
Proof. intros. by eapply Forall2_length, mapM_Some_1. Qed.
(* stdpp/list_monad.v *)
Lemma mapM_None_1 l : mapM f l = None → Exists (λ x, f x = None) l.
Proof.
    induction l as [|x l IH]; simpl; [done|].
    destruct (f x) eqn:?; simpl; eauto. by destruct (mapM f l); eauto.
  Qed.
(* stdpp/list_monad.v *)
Lemma mapM_None_2 l : Exists (λ x, f x = None) l → mapM f l = None.
Proof.
    induction 1 as [x l Hx|x l ? IH]; simpl; [by rewrite Hx|].
    by destruct (f x); simpl; rewrite ?IH.
  Qed.
(* stdpp/list_monad.v *)
Lemma mapM_None l : mapM f l = None ↔ Exists (λ x, f x = None) l.
Proof. split; auto using mapM_None_1, mapM_None_2. Qed.
(* stdpp/list_monad.v *)
Lemma mapM_is_Some_1 l : is_Some (mapM f l) → Forall (is_Some ∘ f) l.
Proof.
    unfold compose. setoid_rewrite <-not_eq_None_Some.
    rewrite mapM_None. apply (not_Exists_Forall _).
  Qed.
(* stdpp/list_monad.v *)
Lemma mapM_is_Some_2 l : Forall (is_Some ∘ f) l → is_Some (mapM f l).
Proof.
    unfold compose. setoid_rewrite <-not_eq_None_Some.
    rewrite mapM_None. apply (Forall_not_Exists _).
  Qed.
(* stdpp/list_monad.v *)
Lemma mapM_is_Some l : is_Some (mapM f l) ↔ Forall (is_Some ∘ f) l.
Proof. split; auto using mapM_is_Some_1, mapM_is_Some_2. Qed.
(* stdpp/list_monad.v *)
Lemma mapM_fmap_Forall_Some (g : B → A) (l : list B) :
    Forall (λ x, f (g x) = Some x) l → mapM f (g <$> l) = Some l.
Proof. by induction 1; simpl; simplify_option_eq. Qed.
(* stdpp/list_monad.v *)
Lemma mapM_fmap_Some (g : B → A) (l : list B) :
    (∀ x, f (g x) = Some x) → mapM f (g <$> l) = Some l.
Proof. intros. by apply mapM_fmap_Forall_Some, Forall_true. Qed.
(* stdpp/list_monad.v *)
Lemma mapM_fmap_Forall2_Some_inv (g : B → A) (l : list A) (k : list B) :
    mapM f l = Some k → Forall2 (λ x y, f x = Some y → g y = x) l k → g <$> k = l.
Proof. induction 2; simplify_option_eq; naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma mapM_fmap_Some_inv (g : B → A) (l : list A) (k : list B) :
    mapM f l = Some k → (∀ x y, f x = Some y → g y = x) → g <$> k = l.
Proof. eauto using mapM_fmap_Forall2_Some_inv, Forall2_true, length_mapM. Qed.
(* stdpp/list_monad.v *)
Lemma imap_const {A B} (f : A → B) l : imap (const f) l = f <$> l.
Proof. induction l; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Instance imap_proper `{!Equiv A, !Equiv B} :
  Proper (pointwise_relation _ ((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B}))
         imap.
Proof.
  intros f f' Hf l l' Hl. revert f f' Hf.
  induction Hl as [|x1 x2 l1 l2 ?? IH]; intros f f' Hf; simpl; constructor.
  - by apply Hf.
  - apply IH. intros i y y' ?; simpl. by apply Hf.
Qed.
(* stdpp/list_monad.v *)
Lemma imap_ext g l :
    (∀ i x, l !! i = Some x → f i x = g i x) → imap f l = imap g l.
Proof. revert f g; induction l as [|x l IH]; intros; f_equal/=; eauto. Qed.
(* stdpp/list_monad.v *)
Lemma imap_nil : imap f [] = [].
Proof. done. Qed.
(* stdpp/list_monad.v *)
Lemma imap_app l1 l2 :
    imap f (l1 ++ l2) = imap f l1 ++ imap (λ n, f (length l1 + n)) l2.
Proof.
    revert f. induction l1 as [|x l1 IH]; intros f; f_equal/=.
    by rewrite IH.
  Qed.
(* stdpp/list_monad.v *)
Lemma imap_cons x l : imap f (x :: l) = f 0 x :: imap (f ∘ S) l.
Proof. done. Qed.
(* stdpp/list_monad.v *)
Lemma imap_fmap {C} (g : C → A) l : imap f (g <$> l) = imap (λ n, f n ∘ g) l.
Proof. revert f. induction l; intros; f_equal/=; eauto. Qed.
(* stdpp/list_monad.v *)
Lemma fmap_imap {C} (g : B → C) l : g <$> imap f l = imap (λ n, g ∘ f n) l.
Proof. revert f. induction l; intros; f_equal/=; eauto. Qed.
(* stdpp/list_monad.v *)
Lemma list_lookup_imap l i : imap f l !! i = f i <$> l !! i.
Proof.
    revert f i. induction l as [|x l IH]; intros f [|i]; f_equal/=; auto.
    by rewrite IH.
  Qed.
(* stdpp/list_monad.v *)
Lemma list_lookup_imap_Some l i x :
    imap f l !! i = Some x ↔ ∃ y, l !! i = Some y ∧ x = f i y.
Proof. by rewrite list_lookup_imap, fmap_Some. Qed.
(* stdpp/list_monad.v *)
Lemma list_lookup_total_imap `{!Inhabited A, !Inhabited B} l i :
    i < length l → imap f l !!! i = f i (l !!! i).
Proof.
    intros [x Hx]%lookup_lt_is_Some_2.
    by rewrite !list_lookup_total_alt, list_lookup_imap, Hx.
  Qed.
(* stdpp/list_monad.v *)
Lemma length_imap l : length (imap f l) = length l.
Proof. revert f. induction l; simpl; eauto. Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_lookup_imap_1 l x :
    x ∈ imap f l → ∃ i y, x = f i y ∧ l !! i = Some y.
Proof.
    intros [i Hin]%list_elem_of_lookup. rewrite list_lookup_imap in Hin.
    simplify_option_eq; naive_solver.
  Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_lookup_imap_2 l x i : l !! i = Some x → f i x ∈ imap f l.
Proof.
    intros Hl. rewrite list_elem_of_lookup.
    exists i. by rewrite list_lookup_imap, Hl.
  Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_lookup_imap l x :
    x ∈ imap f l ↔ ∃ i y, x = f i y ∧ l !! i = Some y.
Proof. naive_solver eauto using elem_of_lookup_imap_1, elem_of_lookup_imap_2. Qed.
(* stdpp/list_monad.v *)
Lemma interleave_cons x l : x :: l ∈ interleave x l.
Proof. destruct l; simpl; rewrite elem_of_cons; auto. Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_interleave l1 l2 x :
    l1 ∈ interleave x l2 ↔ ∃ l l', l1 = l ++ x :: l' ∧ l2 = l ++ l'.
Proof.
    split.
    - revert l1. induction l2 as [|y l IH]; intros l1; simpl.
      { intros ->%list_elem_of_singleton. by exists [], []. }
      intros [->|H]%elem_of_cons; [by exists [], (y :: l)|].
      apply list_elem_of_fmap in H as [? [-> H]].
      apply IH in H as (l' & l'' & -> & ->).
      exists (y :: l'), l''. eauto.
    - intros (l & l' & -> & ->).
      induction l as [|y l IH]; simpl; [apply interleave_cons|].
      apply list_elem_of_further. by apply list_elem_of_fmap_2.
  Qed.
(* stdpp/list_monad.v *)
Lemma interleave_Permutation x l l' : l' ∈ interleave x l → l' ≡ₚ x :: l.
Proof.
    intros (l1&l2&->&->)%elem_of_interleave. by rewrite Permutation_middle.
  Qed.
(* stdpp/list_monad.v *)
Lemma permutations_refl l : l ∈ permutations l.
Proof.
    induction l; simpl; [by apply list_elem_of_singleton|].
    apply list_elem_of_bind. eauto using interleave_cons.
  Qed.
(* stdpp/list_monad.v *)
Lemma permutations_skip x l l' :
    l ∈ permutations l' → x :: l ∈ permutations (x :: l').
Proof. intro. apply list_elem_of_bind; eauto using interleave_cons. Qed.
(* stdpp/list_monad.v *)
Lemma permutations_swap x y l : y :: x :: l ∈ permutations (x :: y :: l).
Proof.
    simpl. apply list_elem_of_bind. exists (y :: l). split; simpl.
    - destruct l; csimpl; rewrite !elem_of_cons; auto.
    - apply list_elem_of_bind. simpl.
      eauto using interleave_cons, permutations_refl.
  Qed.
(* stdpp/list_monad.v *)
Lemma permutations_nil l : l ∈ permutations [] ↔ l = [].
Proof. simpl. by rewrite list_elem_of_singleton. Qed.
(* stdpp/list_monad.v *)
Lemma interleave_interleave_toggle x1 x2 l1 l2 l3 :
    l1 ∈ interleave x1 l2 → l2 ∈ interleave x2 l3 → ∃ l4,
      l1 ∈ interleave x2 l4 ∧ l4 ∈ interleave x1 l3.
Proof.
    revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
    { rewrite !list_elem_of_singleton. intros ? ->. exists [x1].
      change (interleave x2 [x1]) with ([[x2; x1]] ++ [[x1; x2]]).
      by rewrite (comm (++)), list_elem_of_singleton. }
    rewrite elem_of_cons, list_elem_of_fmap.
    intros Hl1 [? | [l2' [??]]]; simplify_eq/=.
    - rewrite !elem_of_cons, list_elem_of_fmap in Hl1.
      destruct Hl1 as [? | [? | [l4 [??]]]]; subst.
      + exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
      + exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
      + exists l4. simpl. rewrite elem_of_cons. auto using interleave_cons.
    - rewrite elem_of_cons, list_elem_of_fmap in Hl1.
      destruct Hl1 as [? | [l1' [??]]]; subst.
      + exists (x1 :: y :: l3). csimpl.
        rewrite !elem_of_cons, !list_elem_of_fmap.
        split; [| by auto]. right. right. exists (y :: l2').
        rewrite list_elem_of_fmap. naive_solver.
      + destruct (IH l1' l2') as [l4 [??]]; auto. exists (y :: l4). simpl.
        rewrite !elem_of_cons, !list_elem_of_fmap. naive_solver.
  Qed.