phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_misc.v *)
Lemma sublist_lookup_Some' l i n l' :
  sublist_lookup i n l = Some l' ↔ l' = take n (drop i l) ∧ i + n ≤ length l.
Proof. unfold sublist_lookup. case_guard; naive_solver lia. Qed.
(* stdpp/list_misc.v *)
Lemma sublist_lookup_None l i n :
  length l < i + n → sublist_lookup i n l = None.
Proof. by unfold sublist_lookup; intros; simplify_option_eq by lia. Qed.
(* stdpp/list_misc.v *)
Lemma sublist_eq l k n :
  (n | length l) → (n | length k) →
  (∀ i, sublist_lookup (i * n) n l = sublist_lookup (i * n) n k) → l = k.
Proof.
  revert l k. assert (∀ l i,
    n ≠ 0 → (n | length l) → ¬n * i `div` n + n ≤ length l → length l ≤ i).
  { intros l i ? [j ->] Hjn. apply Nat.nlt_ge; contradict Hjn.
    rewrite <-Nat.mul_succ_r, (Nat.mul_comm n).
    apply Nat.mul_le_mono_r, Nat.le_succ_l, Nat.Div0.div_lt_upper_bound; lia. }
  intros l k Hl Hk Hlookup. destruct (decide (n = 0)) as [->|].
  { by rewrite (nil_length_inv l),
      (nil_length_inv k) by eauto using Nat.divide_0_l. }
  apply list_eq; intros i. specialize (Hlookup (i `div` n)).
  rewrite (Nat.mul_comm _ n) in Hlookup.
  unfold sublist_lookup in *; simplify_option_eq;
    [|by rewrite !lookup_ge_None_2 by auto].
  apply (f_equal (.!! i `mod` n)) in Hlookup.
  by rewrite !lookup_take_lt, !lookup_drop, <-!Nat.div_mod in Hlookup
    by (auto using Nat.mod_upper_bound with lia).
Qed.
(* stdpp/list_misc.v *)
Lemma sublist_eq_same_length l k j n :
  length l = j * n → length k = j * n →
  (∀ i,i < j → sublist_lookup (i * n) n l = sublist_lookup (i * n) n k) → l = k.
Proof.
  intros Hl Hk ?. destruct (decide (n = 0)) as [->|].
  { by rewrite (nil_length_inv l), (nil_length_inv k) by lia. }
  apply sublist_eq with n; [by exists j|by exists j|].
  intros i. destruct (decide (i < j)); [by auto|].
  assert (∀ m, m = j * n → m < i * n + n).
  { intros ? ->. replace (i * n + n) with (S i * n) by lia.
    apply Nat.mul_lt_mono_pos_r; lia. }
  by rewrite !sublist_lookup_None by auto.
Qed.
(* stdpp/list_misc.v *)
Lemma sublist_lookup_reshape l i n m :
  0 < n → length l = m * n →
  reshape (replicate m n) l !! i = sublist_lookup (i * n) n l.
Proof.
  intros Hn Hl. unfold sublist_lookup.  apply option_eq; intros x; split.
  - intros Hx. case_guard as Hi; simplify_eq/=.
    { f_equal. clear Hi. revert i l Hl Hx.
      induction m as [|m IH]; intros [|i] l ??; simplify_eq/=; auto.
      rewrite <-drop_drop. apply IH; rewrite ?length_drop; auto with lia. }
    destruct Hi. rewrite Hl, <-Nat.mul_succ_l.
    apply Nat.mul_le_mono_r, Nat.le_succ_l. apply lookup_lt_Some in Hx.
    by rewrite length_reshape, length_replicate in Hx.
  - intros Hx. case_guard as Hi; simplify_eq/=.
    revert i l Hl Hi. induction m as [|m IH]; [auto with lia|].
    intros [|i] l ??; simpl; [done|]. rewrite <-drop_drop.
    rewrite IH; rewrite ?length_drop; auto with lia.
Qed.
(* stdpp/list_misc.v *)
Lemma sublist_lookup_compose l1 l2 l3 i n j m :
  sublist_lookup i n l1 = Some l2 → sublist_lookup j m l2 = Some l3 →
  sublist_lookup (i + j) m l1 = Some l3.
Proof.
  unfold sublist_lookup; intros; simplify_option_eq;
    repeat match goal with
    | H : _ ≤ length _ |- _ => rewrite length_take, length_drop in H
    end; rewrite ?take_drop_commute, ?drop_drop, ?take_take,
      ?Nat.min_l, Nat.add_assoc by lia; auto with lia.
Qed.
(* stdpp/list_misc.v *)
Lemma length_sublist_alter f l i n k :
  sublist_lookup i n l = Some k → length (f k) = n →
  length (sublist_alter f i n l) = length l.
Proof.
  unfold sublist_alter, sublist_lookup. intros Hk ?; simplify_option_eq.
  rewrite !length_app, Hk, !length_take, !length_drop; lia.
Qed.
(* stdpp/list_misc.v *)
Lemma sublist_lookup_alter f l i n k :
  sublist_lookup i n l = Some k → length (f k) = n →
  sublist_lookup i n (sublist_alter f i n l) = f <$> sublist_lookup i n l.
Proof.
  unfold sublist_lookup. intros Hk ?. erewrite length_sublist_alter by eauto.
  unfold sublist_alter; simplify_option_eq.
  by rewrite Hk, drop_app_length', take_app_length' by (rewrite ?length_take; lia).
Qed.
(* stdpp/list_misc.v *)
Lemma sublist_lookup_alter_ne f l i j n k :
  sublist_lookup j n l = Some k → length (f k) = n → i + n ≤ j ∨ j + n ≤ i →
  sublist_lookup i n (sublist_alter f j n l) = sublist_lookup i n l.
Proof.
  unfold sublist_lookup. intros Hk Hi ?. erewrite length_sublist_alter by eauto.
  unfold sublist_alter; simplify_option_eq; f_equal; rewrite Hk.
  apply list_eq; intros ii.
  destruct (decide (ii < length (f k))); [|by rewrite !lookup_take_ge by lia].
  rewrite !lookup_take_lt, !lookup_drop by done. destruct (decide (i + ii < j)).
  { by rewrite lookup_app_l, lookup_take_lt by (rewrite ?length_take; lia). }
  rewrite lookup_app_r by (rewrite length_take; lia).
  rewrite length_take_le, lookup_app_r, lookup_drop by lia. f_equal; lia.
Qed.
(* stdpp/list_misc.v *)
Lemma sublist_alter_all f l n : length l = n → sublist_alter f 0 n l = f l.
Proof.
  intros <-. unfold sublist_alter; simpl.
  by rewrite drop_all, (right_id_L [] (++)), take_ge.
Qed.
(* stdpp/list_misc.v *)
Lemma sublist_alter_compose f g l i n k :
  sublist_lookup i n l = Some k → length (f k) = n → length (g k) = n →
  sublist_alter (f ∘ g) i n l = sublist_alter f i n (sublist_alter g i n l).
Proof.
  unfold sublist_alter, sublist_lookup. intros Hk ??; simplify_option_eq.
  by rewrite !take_app_length', drop_app_length', !(assoc_L (++)), drop_app_length',
    take_app_length' by (rewrite ?length_app, ?length_take, ?Hk; lia).
Qed.
(* stdpp/list_misc.v *)
Lemma Forall_sublist_lookup P 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.
(* stdpp/list_misc.v *)
Lemma Forall_sublist_alter P 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.
(* stdpp/list_misc.v *)
Lemma Forall_sublist_alter_inv P 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.
(* stdpp/list_misc.v *)
Lemma zip_with_sublist_alter {A B} (f : A → B → A) g l k i n l' k' :
  length l = length k →
  sublist_lookup i n l = Some l' → sublist_lookup i n k = Some k' →
  length (g l') = length k' → zip_with f (g l') k' = g (zip_with f l' k') →
  zip_with f (sublist_alter g i n l) k = sublist_alter g i n (zip_with f l k).
Proof.
  unfold sublist_lookup, sublist_alter. intros Hlen; rewrite Hlen.
  intros ?? Hl' Hk'. simplify_option_eq.
  by rewrite !zip_with_app_l, !zip_with_drop, Hl', drop_drop, !zip_with_take,
    !length_take_le, Hk' by (rewrite ?length_drop; auto with lia).
Qed.
(* stdpp/list_misc.v *)
Lemma Forall2_resize l (k : list B) x (y : B) 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 P l k) by done.
    auto using Forall2_app, Forall2_take, Forall2_replicate.
  Qed.
(* stdpp/list_misc.v *)
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 P (resize n x l) k), length_resize. }
    rewrite (Nat.le_add_sub (length k) m), !resize_add,
      resize_all, drop_all, resize_nil by lia.
    auto using Forall2_app, Forall2_replicate_r,
      Forall_resize, Forall_drop, length_resize.
  Qed.
(* stdpp/list_misc.v *)
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 P l (resize n y k)), length_resize. }
    rewrite (Nat.le_add_sub (length l) m), !resize_add,
      resize_all, drop_all, resize_nil by lia.
    auto using Forall2_app, Forall2_replicate_l,
      Forall_resize, Forall_drop, length_resize.
  Qed.
(* stdpp/list_misc.v *)
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.
(* stdpp/list_misc.v *)
Lemma Forall2_rotate n l k :
    Forall2 P l k → Forall2 P (rotate n l) (rotate n k).
Proof.
    intros HAll. unfold rotate. rewrite (Forall2_length _ _ _ HAll).
    eauto using Forall2_app, Forall2_take, Forall2_drop.
  Qed.
(* stdpp/list_misc.v *)
Lemma Forall2_rotate_take s e l k :
    Forall2 P l k → Forall2 P (rotate_take s e l) (rotate_take s e k).
Proof.
    intros HAll. unfold rotate_take. rewrite (Forall2_length _ _ _ HAll).
    eauto using Forall2_take, Forall2_rotate.
  Qed.
(* stdpp/list_misc.v *)
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.
(* stdpp/list_misc.v *)
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 P) by eauto; intros; simplify_option_eq.
    eauto using Forall2_take, Forall2_drop.
  Qed.
(* stdpp/list_misc.v *)
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.
(* stdpp/list_misc.v *)
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 P) by eauto; intros; simplify_option_eq.
    apply Forall2_app_l;
      rewrite ?length_take_le by lia; auto using Forall2_take.
    apply Forall2_app_l; erewrite Forall2_length, length_take,
      length_drop, <-Forall2_length, Nat.min_l by eauto with lia; [done|].
    rewrite drop_drop; auto using Forall2_drop.
  Qed.
(* stdpp/list_misc.v *)
Instance : ∀ n, Proper (R ==> Forall2 R ==> Forall2 R) (resize n).
Proof. repeat intro. eauto using Forall2_resize. Qed.
(* stdpp/list_misc.v *)
Instance resize_proper `{!Equiv A} n : Proper ((≡) ==> (≡) ==> (≡@{list A})) (resize n).
Proof.
    induction n; destruct 2; simpl; repeat (constructor || f_equiv); auto.
  Qed.
(* stdpp/list_misc.v *)
Instance : ∀ n, Proper (Forall2 R ==> Forall2 R) (rotate n).
Proof. repeat intro. eauto using Forall2_rotate. Qed.
(* stdpp/list_misc.v *)
Instance rotate_proper `{!Equiv A} n : Proper ((≡@{list A}) ==> (≡)) (rotate n).
Proof. intros ??. rewrite !list_equiv_Forall2. by apply Forall2_rotate. Qed.
(* stdpp/list_misc.v *)
Instance : ∀ s e, Proper (Forall2 R ==> Forall2 R) (rotate_take s e).
Proof. repeat intro. eauto using Forall2_rotate_take. Qed.
(* stdpp/list_misc.v *)
Instance rotate_take_proper `{!Equiv A} s e : Proper ((≡@{list A}) ==> (≡)) (rotate_take s e).
Proof. intros ??. rewrite !list_equiv_Forall2. by apply Forall2_rotate_take. Qed.
(* stdpp/list_misc.v *)
(* ** Properties of the [mask] function *)
Lemma mask_nil f βs : mask f βs [] =@{list A} [].
Proof. by destruct βs. Qed.
(* stdpp/list_misc.v *)
Lemma length_mask f βs l : length (mask f βs l) = length l.
Proof. revert βs. induction l; intros [|??]; f_equal/=; auto. Qed.
(* stdpp/list_misc.v *)
Lemma mask_true f l n : length l ≤ n → mask f (replicate n true) l = f <$> l.
Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_misc.v *)
Lemma mask_false f l n : mask f (replicate n false) l = l.
Proof. revert l. induction n; intros [|??]; f_equal/=; auto. Qed.
(* stdpp/list_misc.v *)
Lemma mask_app f βs1 βs2 l :
  mask f (βs1 ++ βs2) l
  = mask f βs1 (take (length βs1) l) ++ mask f βs2 (drop (length βs1) l).
Proof. revert l. induction βs1;intros [|??]; f_equal/=; auto using mask_nil. Qed.
(* stdpp/list_misc.v *)
Lemma mask_app_2 f βs l1 l2 :
  mask f βs (l1 ++ l2)
  = mask f (take (length l1) βs) l1 ++ mask f (drop (length l1) βs) l2.
Proof. revert βs. induction l1; intros [|??]; f_equal/=; auto. Qed.
(* stdpp/list_misc.v *)
Lemma take_mask f βs l n : take n (mask f βs l) = mask f (take n βs) (take n l).
Proof. revert n βs. induction l; intros [|?] [|[] ?]; f_equal/=; auto. Qed.
(* stdpp/list_misc.v *)
Lemma drop_mask f βs l n : drop n (mask f βs l) = mask f (drop n βs) (drop n l).
Proof.
  revert n βs. induction l; intros [|?] [|[] ?]; f_equal/=; auto using mask_nil.
Qed.
(* stdpp/list_misc.v *)
Lemma sublist_lookup_mask f βs l i n :
  sublist_lookup i n (mask f βs l)
  = mask f (take n (drop i βs)) <$> sublist_lookup i n l.
Proof.
  unfold sublist_lookup; rewrite length_mask; simplify_option_eq; auto.
  by rewrite drop_mask, take_mask.
Qed.
(* stdpp/list_misc.v *)
Lemma mask_mask f g βs1 βs2 l :
  (∀ x, f (g x) = f x) → βs1 =.>* βs2 →
  mask f βs2 (mask g βs1 l) = mask f βs2 l.
Proof.
  intros ? Hβs. revert l. by induction Hβs as [|[] []]; intros [|??]; f_equal/=.
Qed.
(* stdpp/list_misc.v *)
Lemma lookup_mask f βs l i :
  βs !! i = Some true → mask f βs l !! i = f <$> l !! i.
Proof.
  revert i βs. induction l; intros [] [] ?; simplify_eq/=; f_equal; auto.
Qed.
(* stdpp/list_misc.v *)
Lemma lookup_mask_notin f βs l i :
  βs !! i ≠ Some true → mask f βs l !! i = l !! i.
Proof.
  revert i βs. induction l; intros [] [|[]] ?; simplify_eq/=; auto.
Qed.
(* stdpp/list_misc.v *)
Lemma positives_flatten_go_app xs acc :
    positives_flatten_go xs acc = acc ++ positives_flatten_go xs 1.
Proof.
    revert acc.
    induction xs as [|x xs IH]; intros acc; simpl.
    - reflexivity.
    - rewrite IH.
      rewrite (IH (6 ++ _)).
      rewrite 2!(assoc_L (++)).
      reflexivity.
  Qed.
(* stdpp/list_misc.v *)
Lemma positives_unflatten_go_app p suffix xs acc :
    positives_unflatten_go (suffix ++ Pos.reverse (Pos.dup p)) xs acc =
    positives_unflatten_go suffix xs (acc ++ p).
Proof.
    revert suffix acc.
    induction p as [p IH|p IH|]; intros acc suffix; simpl.
    - rewrite 2!Pos.reverse_xI.
      rewrite 2!(assoc_L (++)).
      rewrite IH.
      reflexivity.
    - rewrite 2!Pos.reverse_xO.
      rewrite 2!(assoc_L (++)).
      rewrite IH.
      reflexivity.
    - reflexivity.
  Qed.
(* stdpp/list_misc.v *)
Lemma positives_unflatten_flatten_go suffix xs acc :
    positives_unflatten_go (suffix ++ positives_flatten_go xs 1) acc 1 =
    positives_unflatten_go suffix (xs ++ acc) 1.
Proof.
    revert suffix acc.
    induction xs as [|x xs IH]; intros suffix acc; simpl.
    - reflexivity.
    - rewrite positives_flatten_go_app.
      rewrite (assoc_L (++)).
      rewrite IH.
      rewrite (assoc_L (++)).
      rewrite positives_unflatten_go_app.
      simpl.
      rewrite (left_id_L 1 (++)).
      reflexivity.
  Qed.
(* stdpp/list_misc.v *)
Lemma positives_unflatten_flatten xs :
    positives_unflatten (positives_flatten xs) = Some xs.
Proof.
    unfold positives_flatten, positives_unflatten.
    replace (positives_flatten_go xs 1)
      with (1 ++ positives_flatten_go xs 1)
      by apply (left_id_L 1 (++)).
    rewrite positives_unflatten_flatten_go.
    simpl.
    rewrite (right_id_L [] (++)%list).
    reflexivity.
  Qed.
(* stdpp/list_misc.v *)
Lemma positives_flatten_app xs ys :
    positives_flatten (xs ++ ys) = positives_flatten xs ++ positives_flatten ys.
Proof.
    unfold positives_flatten.
    revert ys.
    induction xs as [|x xs IH]; intros ys; simpl.
    - rewrite (left_id_L 1 (++)).
      reflexivity.
    - rewrite positives_flatten_go_app, (positives_flatten_go_app xs).
      rewrite IH.
      rewrite (assoc_L (++)).
      reflexivity.
  Qed.
(* stdpp/list_misc.v *)
Lemma positives_flatten_cons x xs :
    positives_flatten (x :: xs)
    = 1~1~0 ++ Pos.reverse (Pos.dup x) ++ positives_flatten xs.
Proof.
    change (x :: xs) with ([x] ++ xs)%list.
    rewrite positives_flatten_app.
    rewrite (assoc_L (++)).
    reflexivity.
  Qed.
(* stdpp/list_misc.v *)
Lemma positives_flatten_suffix (l k : list positive) :
    l `suffix_of` k → ∃ q, positives_flatten k = q ++ positives_flatten l.
Proof.
    intros [l' ->].
    exists (positives_flatten l').
    apply positives_flatten_app.
  Qed.
(* stdpp/list_misc.v *)
Lemma positives_flatten_suffix_eq p1 p2 (xs ys : list positive) :
    length xs = length ys →
    p1 ++ positives_flatten xs = p2 ++ positives_flatten ys →
    xs = ys.
Proof.
    revert p1 p2 ys; induction xs as [|x xs IH];
      intros p1 p2 [|y ys] ?; simplify_eq/=; auto.
    rewrite !positives_flatten_cons, !(assoc _); intros Hl.
    assert (xs = ys) as <- by eauto; clear IH; f_equal.
    apply (inj (.++ positives_flatten xs)) in Hl.
    rewrite 2!Pos.reverse_dup in Hl.
    apply (Pos.dup_suffix_eq _ _ p1 p2) in Hl.
    by apply (inj Pos.reverse).
  Qed.
(* stdpp/list_monad.v *)
(* The monadic operations. *)
Instance list_ret: MRet list
:= λ A x, x :: @nil A.
(* stdpp/list_monad.v *)
Instance list_fmap : FMap list
:= λ A B f,
  fix go (l : list A) := match l with [] => [] | x :: l => f x :: go l end.
(* stdpp/list_monad.v *)
Instance list_omap : OMap list
:= λ A B f,
  fix go (l : list A) :=
  match l with
  | [] => []
  | x :: l => match f x with Some y => y :: go l | None => go l end
  end.
(* stdpp/list_monad.v *)
Instance list_bind : MBind list
:= λ A B f,
  fix go (l : list A) := match l with [] => [] | x :: l => f x ++ go l end.
(* stdpp/list_monad.v *)
Instance list_join: MJoin list
:=
  fix go A (ls : list (list A)) : list A :=
  match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
(* stdpp/list_monad.v *)
Definition mapM `{MBind M, MRet M} {A B} (f : A → M B) : list A → M (list B)
:=
  fix go l :=
  match l with [] => mret [] | x :: l => y ← f x; k ← go l; mret (y :: k) end.
(* stdpp/list_monad.v *)
Instance : Params (@mapM) 5
:= {}.
(* stdpp/list_monad.v *)
(* We define stronger variants of the map function that allow the mapped
function to use the index of the elements. *)
Fixpoint imap {A B} (f : nat → A → B) (l : list A) : list B
:=
  match l with
  | [] => []
  | x :: l => f 0 x :: imap (f ∘ S) l
  end.
(* stdpp/list_monad.v *)
Instance : Params (@imap) 2
:= {}.
(* stdpp/list_monad.v *)
Definition zipped_map {A B} (f : list A → list A → A → B) :
    list A → list A → list B
:= fix go l k :=
  match k with
  | [] => []
  | x :: k => f l k x :: go (x :: l) k
  end.
(* stdpp/list_monad.v *)
Instance : Params (@zipped_map) 2
:= {}.
(* stdpp/list_monad.v *)
Fixpoint imap2 {A B C} (f : nat → A → B → C) (l : list A) (k : list B) : list C
:=
  match l, k with
  | [], _ | _, [] => []
  | x :: l, y :: k => f 0 x y :: imap2 (f ∘ S) l k
  end.
(* stdpp/list_monad.v *)
Instance : Params (@imap2) 3
:= {}.
(* stdpp/list_monad.v *)
Inductive zipped_Forall {A} (P : list A → list A → A → Prop) :
    list A → list A → Prop
:=
  | zipped_Forall_nil l : zipped_Forall P l []
  | zipped_Forall_cons l k x :
     P l k x → zipped_Forall P (x :: l) k → zipped_Forall P l (x :: k).
(* stdpp/list_monad.v *)
(* The Cartesian product on lists satisfies (lemma [list_elem_of_cprod]):

  x ∈ cprod l k ↔ x.1 ∈ l ∧ x.2 ∈ k

There are little meaningful things to say about the order of the elements in
[cprod] (so there are no lemmas for that). It thus only makes sense to use
[cprod] when treating the lists as a set-like structure (i.e., up to duplicates
and permutations). *)
Instance list_cprod {A B} : CProd (list A) (list B) (list (A * B))
:=
  λ l k, x ← l; (x,.) <$> k.
(* stdpp/list_monad.v *)
(* The function [permutations l] yields all permutations of [l]. *)
Fixpoint interleave {A} (x : A) (l : list A) : list (list A)
:=
  match l with
  | [] => [[x]]| y :: l => (x :: y :: l) :: ((y ::.) <$> interleave x l)
  end.
(* stdpp/list_monad.v *)
Fixpoint permutations {A} (l : list A) : list (list A)
:=
  match l with [] => [[]] | x :: l => permutations l ≫= interleave x end.
(* stdpp/list_monad.v *)
(* The function [powermset l] returns the list of all lists [l'] such that
[l' ⊆+ l] (notation for [submseteq l' l]). In other words, it returns the
"powerset" of [l], where each [l'] is obtained from [l] by removing elements
and possibly changing the order. *)
Fixpoint powermset {A} (l : list A) : list (list A)
:=
  match l with
  | [] => [[]]
  | x :: l => (powermset l ≫= interleave x) ++ powermset l
  end.
(* stdpp/list_monad.v *)
(* Correspondence to [list_prod] from the stdlib, a version that does not use
the [CProd] class for the interface, nor the monad classes for the definition *)
Lemma list_cprod_list_prod {B} l (k : list B) : cprod l k = list_prod l k.
Proof. unfold cprod, list_cprod. induction l; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Lemma list_elem_of_cprod {B} l (k : list B) (x : A * B) :
  x ∈ cprod l k ↔ x.1 ∈ l ∧ x.2 ∈ k.
Proof.
  rewrite list_cprod_list_prod, !list_elem_of_In.
  destruct x. apply in_prod_iff.
Qed.
(* stdpp/list_monad.v *)
(* * Properties of the monadic operations *)
Lemma list_fmap_id {A} (l : list A) : id <$> l = l.
Proof. induction l; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Instance list_fmap_proper `{!Equiv A, !Equiv B} :
  Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) fmap.
Proof. induction 2; csimpl; constructor; auto. Qed.
(* stdpp/list_monad.v *)
Lemma list_fmap_compose {C} (g : B → C) l : g ∘ f <$> l = g <$> (f <$> l).
Proof. induction l; f_equal/=; auto. Qed.
(* stdpp/list_monad.v *)
Lemma list_fmap_inj_1 f' l x :
    f <$> l = f' <$> l → x ∈ l → f x = f' x.
Proof. intros Hf Hin. induction Hin; naive_solver. Qed.
(* stdpp/list_monad.v *)
Definition fmap_nil : f <$> [] = []
:= eq_refl.
(* stdpp/list_monad.v *)
Definition fmap_cons x l : f <$> x :: l = f x :: (f <$> l)
:= eq_refl.
(* stdpp/list_monad.v *)
Lemma list_fmap_singleton x : f <$> [x] = [f x].
Proof. reflexivity. Qed.
(* stdpp/list_monad.v *)
Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
Proof. by induction l1; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma fmap_snoc l x : f <$> l ++ [x] = (f <$> l) ++ [f x].
Proof. rewrite fmap_app, list_fmap_singleton. done. Qed.
(* stdpp/list_monad.v *)
Lemma fmap_nil_inv k :  f <$> k = [] → k = [].
Proof. by destruct k. Qed.
(* stdpp/list_monad.v *)
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.
(* stdpp/list_monad.v *)
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.
(* stdpp/list_monad.v *)
Lemma fmap_option_list mx :
    f <$> (option_list mx) = option_list (f <$> mx).
Proof. by destruct mx. Qed.
(* stdpp/list_monad.v *)
Lemma list_fmap_alt l :
    f <$> l = omap (λ x, Some (f x)) l.
Proof. induction l; simplify_eq/=; done. Qed.
(* stdpp/list_monad.v *)
Lemma length_fmap l : length (f <$> l) = length l.
Proof. by induction l; f_equal/=. Qed.
(* stdpp/list_monad.v *)
Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
Proof.
    induction l as [|?? IH]; csimpl; by rewrite ?reverse_cons, ?fmap_app, ?IH.
  Qed.
(* stdpp/list_monad.v *)
Lemma fmap_tail l : f <$> tail l = tail (f <$> l).
Proof. by destruct l. Qed.
(* stdpp/list_monad.v *)
Lemma fmap_last l : last (f <$> l) = f <$> last l.
Proof. induction l as [|? []]; simpl; auto. Qed.
(* stdpp/list_monad.v *)
Lemma fmap_replicate n x :  f <$> replicate n x = replicate n (f x).
Proof. by induction n; f_equal/=. Qed.