phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_monad.v *)
Lemma permutations_interleave_toggle x l1 l2 l3 :
    l1 ∈ permutations l2 → l2 ∈ interleave x l3 → ∃ l4,
      l1 ∈ interleave x l4 ∧ l4 ∈ permutations l3.
Proof.
    revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
    { rewrite list_elem_of_singleton. intros Hl1 ->. eexists [].
      by rewrite list_elem_of_singleton. }
    rewrite elem_of_cons, list_elem_of_fmap.
    intros Hl1 [? | [l2' [? Hl2']]]; simplify_eq/=.
    - rewrite list_elem_of_bind in Hl1.
      destruct Hl1 as [l1' [??]]. by exists l1'.
    - rewrite list_elem_of_bind in Hl1. setoid_rewrite list_elem_of_bind.
      destruct Hl1 as [l1' [??]]. destruct (IH l1' l2') as (l1''&?&?); auto.
      destruct (interleave_interleave_toggle y x l1 l1' l1'') as (?&?&?); eauto.
  Qed.
(* stdpp/list_monad.v *)
Lemma permutations_trans l1 l2 l3 :
    l1 ∈ permutations l2 → l2 ∈ permutations l3 → l1 ∈ permutations l3.
Proof.
    revert l1 l2. induction l3 as [|x l3 IH]; intros l1 l2; simpl.
    - rewrite !list_elem_of_singleton. intros Hl1 ->; simpl in *.
      by rewrite list_elem_of_singleton in Hl1.
    - rewrite !list_elem_of_bind. intros Hl1 [l2' [Hl2 Hl2']].
      destruct (permutations_interleave_toggle x l1 l2 l2') as [? [??]]; eauto.
  Qed.
(* stdpp/list_monad.v *)
Lemma permutations_Permutation l l' : l' ∈ permutations l ↔ l ≡ₚ l'.
Proof.
    split.
    - revert l'. induction l; simpl; intros l''.
      + rewrite list_elem_of_singleton. by intros ->.
      + rewrite list_elem_of_bind. intros [l' [Hl'' ?]].
        rewrite (interleave_Permutation _ _ _ Hl''). constructor; auto.
    - induction 1; eauto using permutations_refl,
        permutations_skip, permutations_swap, permutations_trans.
  Qed.
(* stdpp/list_monad.v *)
Lemma powermset_submseteq l l' : l ∈ powermset l' ↔ l ⊆+ l'.
Proof.
   split.
   - revert l; induction l' as [|x l' IH]; simpl; intros l.
     { by intros ->%list_elem_of_singleton. }
     intros [(k & Hl & Hk)%list_elem_of_bind|?]%elem_of_app.
     + apply IH in Hk. apply interleave_Permutation in Hl as ->.
       by apply submseteq_skip.
     + by apply submseteq_cons, IH.
   - revert l; induction l' as [|x l' IH]; simpl; intros l.
     { intros ->%submseteq_nil_r. apply list_elem_of_here. }
     rewrite elem_of_app, list_elem_of_bind.
     intros [H|(k & Hperm & Hsub)]%submseteq_cons_r; [by eauto|].
     apply Permutation_cons_inv_r in Hperm as (k1 & k2 & -> & Hperm).
     left. exists (k1 ++ k2). split.
     + apply elem_of_interleave. by exists k1, k2.
     + apply IH. by rewrite <-Hperm.
  Qed.
(* stdpp/list_monad.v *)
Lemma powermset_refl l : l ∈ powermset l.
Proof. by rewrite powermset_submseteq. Qed.
(* stdpp/list_monad.v *)
Lemma powermset_nil l : l ∈ powermset [] ↔ l = [].
Proof. simpl. by rewrite list_elem_of_singleton. Qed.
(* stdpp/list_monad.v *)
Lemma powermset_permutations l l' : l ∈ permutations l' → l ∈ powermset l'.
Proof.
    rewrite powermset_submseteq, permutations_Permutation. by intros ->.
  Qed.
(* stdpp/list_monad.v *)
Lemma powermset_trans l1 l2 l3 :
    l1 ∈ powermset l2 → l2 ∈ powermset l3 → l1 ∈ powermset l3.
Proof. rewrite !powermset_submseteq. apply submseteq_trans. Qed.
(* stdpp/list_monad.v *)
(* Note that [foldr] has much better support, so when in doubt, it should be
preferred over [foldl]. *)
Definition foldr_app
:= @fold_right_app.
(* stdpp/list_monad.v *)
Lemma foldr_cons {A B} (f : B → A → A) (a : A) l x :
  foldr f a (x :: l) = f x (foldr f a l).
Proof. done. Qed.
(* stdpp/list_monad.v *)
Lemma foldr_snoc {A B} (f : B → A → A) (a : A) l x :
  foldr f a (l ++ [x]) = foldr f (f x a) l.
Proof. rewrite foldr_app. done. Qed.
(* stdpp/list_monad.v *)
Lemma foldr_fmap {A B C} (f : B → A → A) x (l : list C) g :
  foldr f x (g <$> l) = foldr (λ b a, f (g b) a) x l.
Proof. induction l; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Lemma foldr_ext {A B} (f1 f2 : B → A → A) x1 x2 l1 l2 :
  (∀ b a, f1 b a = f2 b a) → l1 = l2 → x1 = x2 → foldr f1 x1 l1 = foldr f2 x2 l2.
Proof. intros Hf -> ->. induction l2 as [|x l2 IH]; f_equal/=; by rewrite Hf, IH. Qed.
(* stdpp/list_monad.v *)
Lemma foldr_permutation {A B} (R : relation B) `{!PreOrder R}
    (f : A → B → B) (b : B) `{Hf : !∀ x, Proper (R ==> R) (f x)} (l1 l2 : list A) :
  (∀ j1 a1 j2 a2 b,
    j1 ≠ j2 → l1 !! j1 = Some a1 → l1 !! j2 = Some a2 →
    R (f a1 (f a2 b)) (f a2 (f a1 b))) →
  l1 ≡ₚ l2 → R (foldr f b l1) (foldr f b l2).
Proof.
  intros Hf'. induction 1 as [|x l1 l2 _ IH|x y l|l1 l2 l3 Hl12 IH _ IH']; simpl.
  - done.
  - apply Hf, IH; eauto.
  - apply (Hf' 0 _ 1); eauto.
  - etrans; [eapply IH, Hf'|].
    apply IH'; intros j1 a1 j2 a2 b' ???.
    symmetry in Hl12; apply Permutation_inj in Hl12 as [_ (g&?&Hg)].
    apply (Hf' (g j1) _ (g j2)); [naive_solver|by rewrite <-Hg..].
Qed.
(* stdpp/list_monad.v *)
Lemma foldr_permutation_proper {A B} (R : relation B) `{!PreOrder R}
    (f : A → B → B) (b : B) `{!∀ x, Proper (R ==> R) (f x)}
    (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
  Proper ((≡ₚ) ==> R) (foldr f b).
Proof. intros l1 l2 Hl. apply foldr_permutation; auto. Qed.
(* stdpp/list_monad.v *)
Instance foldr_permutation_proper' {A} (R : relation A) `{!PreOrder R}
    (f : A → A → A) (a : A) `{!∀ a, Proper (R ==> R) (f a), !Assoc R f, !Comm R f} :
  Proper ((≡ₚ) ==> R) (foldr f a).
Proof.
  apply (foldr_permutation_proper R f); [solve_proper|].
  assert (Proper (R ==> R ==> R) f).
  { intros a1 a2 Ha b1 b2 Hb. by rewrite Hb, (comm f a1), Ha, (comm f). }
  intros a1 a2 b.
  by rewrite (assoc f), (comm f _ b), (assoc f), (comm f b), (comm f _ a2).
Qed.
(* stdpp/list_monad.v *)
Lemma foldr_cons_permute_strong {A B} (R : relation B) `{!PreOrder R}
    (f : A → B → B) (b : B) `{!∀ a, Proper (R ==> R) (f a)} x l :
  (∀ j1 a1 j2 a2 b,
    j1 ≠ j2 → (x :: l) !! j1 = Some a1 → (x :: l) !! j2 = Some a2 →
    R (f a1 (f a2 b)) (f a2 (f a1 b))) →
  R (foldr f b (x :: l)) (foldr f (f x b) l).
Proof.
  intros. rewrite <-foldr_snoc.
  apply (foldr_permutation _ f b); [done|]. by rewrite Permutation_app_comm.
Qed.
(* stdpp/list_monad.v *)
Lemma foldr_cons_permute {A} (f : A → A → A) (a : A) x l :
  Assoc (=) f →
  Comm (=) f →
  foldr f a (x :: l) = foldr f (f x a) l.
Proof.
  intros. apply (foldr_cons_permute_strong (=) f a).
  intros j1 a1 j2 a2 b _ _ _. by rewrite !(assoc_L f), (comm_L f a1).
Qed.
(* stdpp/list_monad.v *)
(* The following lemma shows that folding over a list twice (using the result
of the first fold as input for the second fold) is equivalent to folding over
the list once, *if* the function is idempotent for the elements of the list
and does not care about the order in which elements are processed. *)
Lemma foldr_idemp_strong {A B} (R : relation B) `{!PreOrder R}
    (f : A → B → B) (b : B) `{!∀ x, Proper (R ==> R) (f x)} (l : list A) :
  (∀ j a b,
    (** This is morally idempotence for elements of [l] *)
    l !! j = Some a →
    R (f a (f a b)) (f a b)) →
  (∀ j1 a1 j2 a2 b,
    (** This is morally commutativity + associativity for elements of [l] *)
    j1 ≠ j2 → l !! j1 = Some a1 → l !! j2 = Some a2 →
    R (f a1 (f a2 b)) (f a2 (f a1 b))) →
  R (foldr f (foldr f b l) l) (foldr f b l).
Proof.
  intros Hfidem Hfcomm. induction l as [|x l IH]; simpl; [done|].
  trans (f x (f x (foldr f (foldr f b l) l))).
  { f_equiv. rewrite <-foldr_snoc, <-foldr_cons.
    apply (foldr_permutation (flip R) f).
    - solve_proper.
    - intros j1 a1 j2 a2 b' ???. by apply (Hfcomm j2 _ j1).
    - by rewrite <-Permutation_cons_append. }
  rewrite <-foldr_cons.
  trans (f x (f x (foldr f b l))); [|by apply (Hfidem 0)].
  simpl. do 2 f_equiv. apply IH.
  - intros j a b' ?. by apply (Hfidem (S j)).
  - intros j1 a1 j2 a2 b' ???. apply (Hfcomm (S j1) _ (S j2)); auto with lia.
Qed.
(* stdpp/list_monad.v *)
Lemma foldr_idemp {A} (f : A → A → A) (a : A) (l : list A) :
  IdemP (=) f →
  Assoc (=) f →
  Comm (=) f →
  foldr f (foldr f a l) l = foldr f a l.
Proof.
  intros. apply (foldr_idemp_strong (=) f a).
  - intros j a1 a2 _. by rewrite (assoc_L f), (idemp f).
  - intros x1 a1 x2 a2 a3 _ _ _. by rewrite !(assoc_L f), (comm_L f a1).
Qed.
(* stdpp/list_monad.v *)
Lemma foldr_comm_acc_strong {A B} (R : relation B) `{!PreOrder R}
    (f : A → B → B) (g : B → B) b l :
  (∀ x, Proper (R ==> R) (f x)) →
  (∀ x y, x ∈ l → R (f x (g y)) (g (f x y))) →
  R (foldr f (g b) l) (g (foldr f b l)).
Proof.
  intros ? Hcomm. induction l as [|x l IH]; simpl; [done|].
  rewrite <-Hcomm by eauto using list_elem_of_here.
  by rewrite IH by eauto using list_elem_of_further.
Qed.
(* stdpp/list_monad.v *)
Lemma foldr_comm_acc {A B} (f : A → B → B) (g : B → B) (b : B) l :
  (∀ x y, f x (g y) = g (f x y)) →
  foldr f (g b) l = g (foldr f b l).
Proof. intros. apply (foldr_comm_acc_strong _); [solve_proper|done]. Qed.
(* stdpp/list_monad.v *)
Lemma foldr_join {A B} (ls : list (list A)) (f : A → B → B) x :
  foldr f x (mjoin ls) = foldr (λ l y, foldr f y l) x ls.
Proof.
  induction ls as [|l ls IH]; simpl; [done|].
  by rewrite foldr_app, IH.
Qed.
(* stdpp/list_monad.v *)
Lemma foldl_app {A B} (f : A → B → A) (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.
(* stdpp/list_monad.v *)
Lemma foldl_snoc {A B} (f : A → B → A) (a : A) l x :
  foldl f a (l ++ [x]) = f (foldl f a l) x.
Proof. rewrite foldl_app. done. Qed.
(* stdpp/list_monad.v *)
Lemma foldl_fmap {A B C} (f : A → B → A) x (l : list C) g :
  foldl f x (g <$> l) = foldl (λ a b, f a (g b)) x l.
Proof. revert x. induction l; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Lemma foldl_foldr {A B} (f : A → B → A) l a :
  foldl f a l = foldr (flip f) a (reverse l).
Proof.
  revert a. induction l as [|x l IH]; intros a; simpl; [done|].
  by rewrite reverse_cons, foldr_snoc, IH.
Qed.
(* stdpp/list_monad.v *)
Lemma foldr_foldl {A B} (f : A → B → B) l a :
  foldr f a l = foldl (flip f) a (reverse l).
Proof. by rewrite foldl_foldr, reverse_involutive. Qed.
(* stdpp/list_monad.v *)
(* ** Properties of the [zip_with] and [zip] functions *)
Instance zip_with_proper `{!Equiv A, !Equiv B, !Equiv C} :
  Proper (((≡) ==> (≡) ==> (≡)) ==>
          (≡@{list A}) ==> (≡@{list B}) ==> (≡@{list C})) zip_with.
Proof.
  intros f1 f2 Hf. induction 1; destruct 1; simpl; [constructor..|].
  f_equiv; [|by auto]. by apply Hf.
Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_nil_l k : zip_with f [] k = [].
Proof. done. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_nil_r l : zip_with f l [] = [].
Proof. by destruct l. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_app l1 l2 k1 k2 :
    length l1 = length k1 →
    zip_with f (l1 ++ l2) (k1 ++ k2) = zip_with f l1 k1 ++ zip_with f l2 k2.
Proof. rewrite <-Forall2_same_length. induction 1; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_app_l l1 l2 k :
    zip_with f (l1 ++ l2) k
    = zip_with f l1 (take (length l1) k) ++ zip_with f l2 (drop (length l1) k).
Proof.
    revert k. induction l1; intros [|??]; f_equal/=; auto. by destruct l2.
  Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_app_r l k1 k2 :
    zip_with f l (k1 ++ k2)
    = zip_with f (take (length k1) l) k1 ++ zip_with f (drop (length k1) l) k2.
Proof. revert l. induction k1; intros [|??]; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_flip l k : zip_with (flip f) k l = zip_with f l k.
Proof. revert k. induction l; intros [|??]; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_ext (g : A → B → C) l1 l2 k1 k2 :
    (∀ x y, f x y = g x y) → l1 = l2 → k1 = k2 →
    zip_with f l1 k1 = zip_with g l2 k2.
Proof. intros ? <-<-. revert k1. by induction l1; intros [|??]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma Forall_zip_with_ext_l (g : A → B → C) l k1 k2 :
    Forall (λ x, ∀ y, f x y = g x y) l → k1 = k2 →
    zip_with f l k1 = zip_with g l k2.
Proof. intros Hl <-. revert k1. by induction Hl; intros [|??]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma Forall_zip_with_ext_r (g : A → B → C) l1 l2 k :
    l1 = l2 → Forall (λ y, ∀ x, f x y = g x y) k →
    zip_with f l1 k = zip_with g l2 k.
Proof. intros <- Hk. revert l1. by induction Hk; intros [|??]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_fmap_l {D} (g : D → A) lD k :
    zip_with f (g <$> lD) k = zip_with (λ z, f (g z)) lD k.
Proof. revert k. by induction lD; intros [|??]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_fmap_r {D} (g : D → B) l kD :
    zip_with f l (g <$> kD) = zip_with (λ x z, f x (g z)) l kD.
Proof. revert kD. by induction l; intros [|??]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_nil_inv l k : zip_with f l k = [] → l = [] ∨ k = [].
Proof. destruct l, k; intros; simplify_eq/=; auto. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_cons_inv l k z lC :
    zip_with f l k = z :: lC →
    ∃ x y l' k', z = f x y ∧ lC = zip_with f l' k' ∧ l = x :: l' ∧ k = y :: k'.
Proof. intros. destruct l, k; simplify_eq/=; repeat eexists. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_app_inv l k lC1 lC2 :
    zip_with f l k = lC1 ++ lC2 →
    ∃ l1 k1 l2 k2, lC1 = zip_with f l1 k1 ∧ lC2 = zip_with f l2 k2 ∧
      l = l1 ++ l2 ∧ k = k1 ++ k2 ∧ length l1 = length k1.
Proof.
    revert l k. induction lC1 as [|z lC1 IH]; simpl.
    { intros l k ?. by eexists [], [], l, k. }
    intros [|x l] [|y k] ?; simplify_eq/=.
    destruct (IH l k) as (l1&k1&l2&k2&->&->&->&->&?); [done |].
    exists (x :: l1), (y :: k1), l2, k2; simpl; auto with congruence.
  Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_inj `{!Inj2 (=) (=) (=) f} l1 l2 k1 k2 :
    length l1 = length k1 → length l2 = length k2 →
    zip_with f l1 k1 = zip_with f l2 k2 → l1 = l2 ∧ k1 = k2.
Proof.
    rewrite <-!Forall2_same_length. intros Hl. revert l2 k2.
    induction Hl; intros ?? [] ?; f_equal; naive_solver.
  Qed.
(* stdpp/list_monad.v *)
Lemma length_zip_with l k :
    length (zip_with f l k) = min (length l) (length k).
Proof. revert k. induction l; intros [|??]; simpl; auto with lia. Qed.
(* stdpp/list_monad.v *)
Lemma length_zip_with_l l k :
    length l ≤ length k → length (zip_with f l k) = length l.
Proof. rewrite length_zip_with; lia. Qed.
(* stdpp/list_monad.v *)
Lemma length_zip_with_l_eq l k :
    length l = length k → length (zip_with f l k) = length l.
Proof. rewrite length_zip_with; lia. Qed.
(* stdpp/list_monad.v *)
Lemma length_zip_with_r l k :
    length k ≤ length l → length (zip_with f l k) = length k.
Proof. rewrite length_zip_with; lia. Qed.
(* stdpp/list_monad.v *)
Lemma length_zip_with_r_eq l k :
    length k = length l → length (zip_with f l k) = length k.
Proof. rewrite length_zip_with; lia. Qed.
(* stdpp/list_monad.v *)
Lemma length_zip_with_same_l P l k :
    Forall2 P l k → length (zip_with f l k) = length l.
Proof. induction 1; simpl; auto. Qed.
(* stdpp/list_monad.v *)
Lemma length_zip_with_same_r P l k :
    Forall2 P l k → length (zip_with f l k) = length k.
Proof. induction 1; simpl; auto. Qed.
(* stdpp/list_monad.v *)
Lemma lookup_zip_with l k i :
    zip_with f l k !! i = (x ← l !! i; y ← k !! i; Some (f x y)).
Proof.
    revert k i. induction l; intros [|??] [|?]; f_equal/=; auto.
    by destruct (_ !! _).
  Qed.
(* stdpp/list_monad.v *)
Lemma lookup_total_zip_with `{!Inhabited A, !Inhabited B, !Inhabited C} l k i :
    i < length l → i < length k → zip_with f l k !!! i = f (l !!! i) (k !!! i).
Proof.
    intros [x Hx]%lookup_lt_is_Some_2 [y Hy]%lookup_lt_is_Some_2.
    by rewrite !list_lookup_total_alt, lookup_zip_with, Hx, Hy.
  Qed.
(* stdpp/list_monad.v *)
Lemma lookup_zip_with_Some l k i z :
    zip_with f l k !! i = Some z
    ↔ ∃ x y, z = f x y ∧ l !! i = Some x ∧ k !! i = Some y.
Proof. rewrite lookup_zip_with. destruct (l !! i), (k !! i); naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma lookup_zip_with_None l k i  :
    zip_with f l k !! i = None
    ↔ l !! i = None ∨ k !! i = None.
Proof. rewrite lookup_zip_with. destruct (l !! i), (k !! i); naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma insert_zip_with l k i x y :
    <[i:=f x y]>(zip_with f l k) = zip_with f (<[i:=x]>l) (<[i:=y]>k).
Proof. revert i k. induction l; intros [|?] [|??]; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Lemma fmap_zip_with_l (g : C → A) l k :
    (∀ x y, g (f x y) = x) → length l ≤ length k → g <$> zip_with f l k = l.
Proof. revert k. induction l; intros [|??] ??; f_equal/=; auto with lia. Qed.
(* stdpp/list_monad.v *)
Lemma fmap_zip_with_r (g : C → B) l k :
    (∀ x y, g (f x y) = y) → length k ≤ length l → g <$> zip_with f l k = k.
Proof. revert l. induction k; intros [|??] ??; f_equal/=; auto with lia. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_zip l k : zip_with f l k = uncurry f <$> zip l k.
Proof. revert k. by induction l; intros [|??]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_fst_snd lk : zip_with f (lk.*1) (lk.*2) = uncurry f <$> lk.
Proof. by induction lk as [|[]]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_replicate n x y :
    zip_with f (replicate n x) (replicate n y) = replicate n (f x y).
Proof. by induction n; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_replicate_l n x k :
    length k ≤ n → zip_with f (replicate n x) k = f x <$> k.
Proof. revert n. induction k; intros [|?] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_replicate_r n y l :
    length l ≤ n → zip_with f l (replicate n y) = flip f y <$> l.
Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_replicate_r_eq n y l :
    length l = n → zip_with f l (replicate n y) = flip f y <$> l.
Proof. intros; apply zip_with_replicate_r; lia. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_take n l k :
    take n (zip_with f l k) = zip_with f (take n l) (take n k).
Proof. revert n k. by induction l; intros [|?] [|??]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_drop n l k :
    drop n (zip_with f l k) = zip_with f (drop n l) (drop n k).
Proof.
    revert n k. induction l; intros [] []; f_equal/=; auto using zip_with_nil_r.
  Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_take_l' n l k :
    length l `min` length k ≤ n → zip_with f (take n l) k = zip_with f l k.
Proof. revert n k. induction l; intros [] [] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_take_l l k :
    zip_with f (take (length k) l) k = zip_with f l k.
Proof. apply zip_with_take_l'; lia. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_take_r' n l k :
    length l `min` length k ≤ n → zip_with f l (take n k) = zip_with f l k.
Proof. revert n k. induction l; intros [] [] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_take_r l k :
    zip_with f l (take (length l) k) = zip_with f l k.
Proof. apply zip_with_take_r'; lia. Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_take_both' n1 n2 l k :
    length l `min` length k ≤ n1 → length l `min` length k ≤ n2 →
    zip_with f (take n1 l) (take n2 k) = zip_with f l k.
Proof.
    intros.
    rewrite zip_with_take_l'; [apply zip_with_take_r' | rewrite length_take]; lia.
  Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_take_both l k :
    zip_with f (take (length k) l) (take (length l) k) = zip_with f l k.
Proof. apply zip_with_take_both'; lia. Qed.
(* stdpp/list_monad.v *)
Lemma Forall_zip_with_fst (P : A → Prop) (Q : C → Prop) l k :
    Forall P l → Forall (λ y, ∀ x, P x → Q (f x y)) k →
    Forall Q (zip_with f l k).
Proof. intros Hl. revert k. induction Hl; destruct 1; simpl in *; auto. Qed.
(* stdpp/list_monad.v *)
Lemma Forall_zip_with_snd (P : B → Prop) (Q : C → Prop) l k :
    Forall (λ x, ∀ y, P y → Q (f x y)) l → Forall P k →
    Forall Q (zip_with f l k).
Proof. intros Hl. revert k. induction Hl; destruct 1; simpl in *; auto. Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_lookup_zip_with_1 l k (z : C) :
    z ∈ zip_with f l k → ∃ i x y, z = f x y ∧ l !! i = Some x ∧ k !! i = Some y.
Proof.
    intros [i Hin]%list_elem_of_lookup. rewrite lookup_zip_with in Hin.
    simplify_option_eq; naive_solver.
  Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_lookup_zip_with_2 l k x y (z : C) i :
    l !! i = Some x → k !! i = Some y → f x y ∈ zip_with f l k.
Proof.
    intros Hl Hk. rewrite list_elem_of_lookup.
    exists i. by rewrite lookup_zip_with, Hl, Hk.
  Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_lookup_zip_with l k (z : C) :
    z ∈ zip_with f l k ↔ ∃ i x y, z = f x y ∧ l !! i = Some x ∧ k !! i = Some y.
Proof.
    naive_solver eauto using
                 elem_of_lookup_zip_with_1, elem_of_lookup_zip_with_2.
  Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_zip_with l k (z : C) :
    z ∈ zip_with f l k → ∃ x y, z = f x y ∧ x ∈ l ∧ y ∈ k.
Proof.
    intros ?%elem_of_lookup_zip_with.
    naive_solver eauto using list_elem_of_lookup_2.
  Qed.
(* stdpp/list_monad.v *)
Lemma zip_with_diag {A C} (f : A → A → C) l :
  zip_with f l l = (λ x, f x x) <$> l.
Proof. induction l as [|?? IH]; [done|]. simpl. rewrite IH. done. Qed.
(* stdpp/list_monad.v *)
(* The lemmas below are outside the section so the [_r] version can be derived
from the [_l] version. *)
Lemma NoDup_zip_with_l_strong {A B C} (f : A → B → C) l k :
  (∀ i1 i2 x1 x2 y1 y2,
    l !! i1 = Some x1 → k !! i1 = Some y1 →
    l !! i2 = Some x2 → k !! i2 = Some y2 →
    f x1 y1 = f x2 y2 → x1 = x2) →
  NoDup l →
  NoDup (zip_with f l k).
Proof.
  intros Hinj.
  induction 1 as [|x l Hxl Hl IHl] in k, Hinj |- *; [constructor|].
  destruct k as [|y k]; simpl; [by constructor|]. constructor.
  - intros (i & x' & y' & Hf & Hx & Hy)%elem_of_lookup_zip_with_1.
    assert (x = x') as -> by (by eapply (Hinj 0 (S i))).
    by apply list_elem_of_lookup_2 in Hx.
  - apply IHl. intros i1 i2 x1 x2 y1 y2 Hl1 Hk1 Hl2 Hk2 Hf.
    by eapply (Hinj (S i1) (S i2)).
Qed.
(* stdpp/list_monad.v *)
Lemma NoDup_zip_with_r_strong {A B C} (f : A → B → C) l k :
  (∀ i1 i2 x1 x2 y1 y2,
    l !! i1 = Some x1 → k !! i1 = Some y1 →
    l !! i2 = Some x2 → k !! i2 = Some y2 →
    f x1 y1 = f x2 y2 → y1 = y2) →
  NoDup k →
  NoDup (zip_with f l k).
Proof.
  intros Hinj. rewrite <-zip_with_flip.
  apply NoDup_zip_with_l_strong. naive_solver.
Qed.
(* stdpp/list_monad.v *)
Lemma NoDup_zip_with_l {A B C} (f : A → B → C) `{!Inj2 (=) (=) (=) f} l k :
  NoDup l → NoDup (zip_with f l k).
Proof. apply NoDup_zip_with_l_strong. naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma NoDup_zip_with_r {A B C} (f : A → B → C) `{!Inj2 (=) (=) (=) f} l k :
  NoDup k → NoDup (zip_with f l k).
Proof. apply NoDup_zip_with_r_strong. naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma zip_nil_l k : zip [] k =@{list (A * B)} [].
Proof. apply zip_with_nil_l. Qed.
(* stdpp/list_monad.v *)
Lemma zip_nil_r l : zip l [] =@{list (A * B)} [].
Proof. apply zip_with_nil_r. Qed.
(* stdpp/list_monad.v *)
Lemma fst_zip l k : length l ≤ length k → (zip l k).*1 = l.
Proof. by apply fmap_zip_with_l. Qed.
(* stdpp/list_monad.v *)
Lemma snd_zip l k : length k ≤ length l → (zip l k).*2 = k.
Proof. by apply fmap_zip_with_r. Qed.
(* stdpp/list_monad.v *)
Lemma zip_fst_snd (lk : list (A * B)) : zip (lk.*1) (lk.*2) = lk.
Proof. by induction lk as [|[]]; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma Forall2_fst P l1 l2 k1 k2 :
    length l2 = length k2 → Forall2 P l1 k1 →
    Forall2 (λ x y, P (x.1) (y.1)) (zip l1 l2) (zip k1 k2).
Proof.
    rewrite <-Forall2_same_length. intros Hlk2 Hlk1. revert l2 k2 Hlk2.
    induction Hlk1; intros ?? [|??????]; simpl; auto.
  Qed.
(* stdpp/list_monad.v *)
Lemma Forall2_snd P l1 l2 k1 k2 :
    length l1 = length k1 → Forall2 P l2 k2 →
    Forall2 (λ x y, P (x.2) (y.2)) (zip l1 l2) (zip k1 k2).
Proof.
    rewrite <-Forall2_same_length. intros Hlk1 Hlk2. revert l1 k1 Hlk1.
    induction Hlk2; intros ?? [|??????]; simpl; auto.
  Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_zip_l x1 x2 l k :
    (x1, x2) ∈ zip l k → x1 ∈ l.
Proof. intros ?%elem_of_zip_with. naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_zip_r x1 x2 l k :
    (x1, x2) ∈ zip l k → x2 ∈ k.
Proof. intros ?%elem_of_zip_with. naive_solver. Qed.
(* stdpp/list_monad.v *)
Lemma length_zip l k :
    length (zip l k) = min (length l) (length k).
Proof. by rewrite length_zip_with. Qed.
(* stdpp/list_monad.v *)
Lemma zip_nil_inv l k :
    zip l k = [] → l = [] ∨ k = [].
Proof. intros. by eapply zip_with_nil_inv. Qed.
(* stdpp/list_monad.v *)
Lemma lookup_zip_Some l k i x y :
    zip l k !! i = Some (x, y) ↔ l !! i = Some x ∧ k !! i = Some y.
Proof. rewrite lookup_zip_with_Some. naive_solver. Qed.