list.v

  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 {A} (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 {A} (x : A) n l :
  length l = n → Forall (x =) l → replicate n x = l.
Proof. by rewrite replicate_as_Forall. Qed.

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_equality'; 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_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_flip l k : Forall2 (flip P) k l ↔ Forall2 P l k.
  Proof. split; induction 1; constructor; auto. 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_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_lookup_lr l k i x y :
    Forall2 P l k → l !! i = Some x → k !! i = Some y → P x y.
  Proof.
    intros H. revert i. induction H; intros [|?] ??; simplify_equality'; eauto.
  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.
    intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
  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.
    intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
  Qed.
  Lemma Forall2_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_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_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_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_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_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_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_ge_l l k x y n m :
    P x y → Forall (flip P y) l → n ≤ m →
    Forall2 P (resize n x l) k → Forall2 P (resize m x l) (resize m y k).
  Proof.
    intros. assert (n = length k) as ->.
    { 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 done; auto using Forall2_app, Forall2_replicate_r,
      Forall_resize, Forall_drop, resize_length.
  Qed.
  Lemma Forall2_resize_ge_r l k x y n m :
    P x y → Forall (P x) k → n ≤ m →
    Forall2 P l (resize n y k) → Forall2 P (resize m x l) (resize m y k).
  Proof.
    intros. assert (n = length l) as ->.
    { 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 done; auto using Forall2_app, Forall2_replicate_l,
      Forall_resize, Forall_drop, resize_length.
  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_equality.
    * 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_equality.
    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_equality.
    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_equality.
    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.
  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_Forall (Q : A → A → Prop) l :
    Forall (λ x, Q x x) l → Forall2 Q l l.
  Proof. induction 1; constructor; auto. 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_order.
  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. 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: AntiSymmetric (=) R → AntiSymmetric (=) (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. eauto using Forall2_app. Qed.
  Global Instance: Proper (Forall2 R ==> Forall2 R) (delete i).
  Proof. repeat intro. eauto using Forall2_delete. Qed.
  Global Instance: Proper (R ==> Forall2 R) (replicate n).
  Proof. repeat intro. eauto using Forall2_replicate. 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 (R ==> Forall2 R ==> Forall2 R) (resize n).
  Proof. repeat intro. eauto using Forall2_resize. Qed.
End Forall2_order.

Section Forall3.
  Context {A B C} (P : A → B → C → Prop).
  Lemma Forall3_impl (Q : A → B → C → Prop) l l' k :
    Forall3 P l l' k → (∀ x y z, P x y z → Q x y z) → Forall3 Q l l' k.
  Proof. intros Hl ?. induction Hl; constructor; auto. Defined.
  Lemma Forall3_length_lm l l' k : Forall3 P l l' k → length l = length l'.
  Proof. by induction 1; f_equal'. Qed.
  Lemma Forall3_lookup_lmr l l' k i x y z :
    Forall3 P l l' k →
    l !! i = Some x → l' !! i = Some y → k !! i = Some z → P x y z.
  Proof.
    intros H. revert i. induction H; intros [|?] ???; simplify_equality'; eauto.
  Qed.
  Lemma Forall3_lookup_l l l' k i x :
    Forall3 P l l' k → l !! i = Some x →
    ∃ y z, l' !! i = Some y ∧ k !! i = Some z ∧ P x y z.
  Proof.
    intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
  Qed.
  Lemma Forall3_lookup_m l l' k i y :
    Forall3 P l l' k → l' !! 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_equality'; eauto.
  Qed.
  Lemma Forall3_lookup_r l l' k i z :
    Forall3 P l l' k → k !! i = Some z →
    ∃ x y, l !! i = Some x ∧ l' !! i = Some y ∧ P x y z.
  Proof.
    intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
  Qed.
  Lemma Forall3_alter_lm f g l l' k i :
    Forall3 P l l' k →
    (∀ x y z, l !! i = Some x → l' !! 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 l') k.
  Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
End Forall3.

(** * 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.
  Global Instance: Injective (=) (=) f → Injective (=) (=) (fmap f).
  Proof.
    intros ? l1. induction l1 as [|x l1 IH]; [by intros [|??]|].
    intros [|??]; intros; f_equal'; simplify_equality; 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_equality'; 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_equality'.
    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_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 replicate_const_fmap (x : A) (l : list A) :
    const x <$> l = replicate (length l) x.
  Proof. by induction l; f_equal'. 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_equality; 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 `{!Injective (=) (=) f} l : NoDup l → NoDup (f <$> l).
  Proof.
    induction 1; simpl; constructor; trivial. rewrite elem_of_list_fmap.
    intros [y [Hxy ?]]. apply (injective f) in Hxy. by subst.
  Qed.
  Lemma NoDup_fmap `{!Injective (=) (=) f} l : 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_equality; 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 (fst <$> l).
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 !(associative_L (++)), (commutative (++) (f _)).
    * by apply contains_inserts_l.
    * etransitivity; eauto.
  Qed.
  Global Instance bind_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (mbind f).
  Proof.
    induction 1; csimpl; auto.
    * by f_equiv.
    * by rewrite !(associative_L (++)), (commutative (++) (f _)).
    * etransitivity; 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 <-?(associative_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.

Section mapM.
  Context {A B : Type} (f : A → option B).

  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; simpl; rewrite ?Hfg, ?IHl. Qed.
  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.
  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.
  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:?; simpl; [|discriminate].
      destruct (mapM f l); intros; simplify_equality. constructor; auto.
  Qed.
  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.
  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.
  Lemma mapM_length l k : mapM f l = Some k → length l = length k.
  Proof. intros. by eapply Forall2_length, mapM_Some_1. Qed.
  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.
  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.
  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.
  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.
  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.
  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.
  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 induction l; simpl; simplify_option_equality. Qed.
  Lemma mapM_fmap_Some_inv (g : B → A) (l : list B) (k : list A) :
    (∀ x y, f y = Some x → y = g x) → mapM f k = Some l → k = g <$> l.
  Proof.
    intros Hgf. revert l; induction k as [|??]; intros [|??] ?;
      simplify_option_equality; f_equiv; eauto.
  Qed.
End mapM.

(** ** Properties of the [permutations] function *)
Section permutations.
  Context {A : Type}.
  Implicit Types x y z : A.
  Implicit Types l : list A.

  Lemma interleave_cons x l : x :: l ∈ interleave x l.
  Proof. destruct l; simpl; rewrite elem_of_cons; auto. Qed.
  Lemma interleave_Permutation x l l' : l' ∈ interleave x l → l' ≡ₚ x :: l.
  Proof.
    revert l'. induction l as [|y l IH]; intros l'; simpl.
    * rewrite elem_of_list_singleton. by intros ->.
    * rewrite elem_of_cons, elem_of_list_fmap. intros [->|[? [-> H]]]; [done|].
      rewrite (IH _ H). constructor.
  Qed.
  Lemma permutations_refl l : l ∈ permutations l.
  Proof.
    induction l; simpl; [by apply elem_of_list_singleton|].
    apply elem_of_list_bind. eauto using interleave_cons.
  Qed.
  Lemma permutations_skip x l l' :
    l ∈ permutations l' → x :: l ∈ permutations (x :: l').
  Proof. intro. apply elem_of_list_bind; eauto using interleave_cons. Qed.
  Lemma permutations_swap x y l : y :: x :: l ∈ permutations (x :: y :: l).
  Proof.
    simpl. apply elem_of_list_bind. exists (y :: l). split; simpl.
    * destruct l; csimpl; rewrite !elem_of_cons; auto.
    * apply elem_of_list_bind. simpl.
      eauto using interleave_cons, permutations_refl.
  Qed.
  Lemma permutations_nil l : l ∈ permutations [] ↔ l = [].
  Proof. simpl. by rewrite elem_of_list_singleton. Qed.
  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 !elem_of_list_singleton. intros ? ->. exists [x1].
      change (interleave x2 [x1]) with ([[x2; x1]] ++ [[x1; x2]]).
      by rewrite (commutative (++)), elem_of_list_singleton. }
    rewrite elem_of_cons, elem_of_list_fmap.
    intros Hl1 [? | [l2' [??]]]; simplify_equality'.
    * rewrite !elem_of_cons, elem_of_list_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, elem_of_list_fmap in Hl1.
      destruct Hl1 as [? | [l1' [??]]]; subst.
      + exists (x1 :: y :: l3). csimpl.
        rewrite !elem_of_cons, !elem_of_list_fmap.
        split; [| by auto]. right. right. exists (y :: l2').
        rewrite elem_of_list_fmap. naive_solver.
      + destruct (IH l1' l2') as [l4 [??]]; auto. exists (y :: l4). simpl.
        rewrite !elem_of_cons, !elem_of_list_fmap. naive_solver.
  Qed.
  Lemma permutations_interleave_toggle x 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 elem_of_list_singleton. intros Hl1 ->. eexists [].
      by rewrite elem_of_list_singleton. }
    rewrite elem_of_cons, elem_of_list_fmap.
    intros Hl1 [? | [l2' [? Hl2']]]; simplify_equality'.
    * rewrite elem_of_list_bind in Hl1.
      destruct Hl1 as [l1' [??]]. by exists l1'.
    * rewrite elem_of_list_bind in Hl1. setoid_rewrite elem_of_list_bind.
      destruct Hl1 as [l1' [??]]. destruct (IH l1' l2') as (l1''&?&?); auto.
      destruct (interleave_interleave_toggle y x l1 l1' l1'') as (?&?&?); eauto.
  Qed.
  Lemma permutations_trans l1 l2 l3 :
    l1 ∈ permutations l2 → l2 ∈ permutations l3 → l1 ∈ permutations l3.
  Proof.
    revert l1 l2. induction l3 as [|x l3 IH]; intros l1 l2; simpl.
    * rewrite !elem_of_list_singleton. intros Hl1 ->; simpl in *.
      by rewrite elem_of_list_singleton in Hl1.
    * rewrite !elem_of_list_bind. intros Hl1 [l2' [Hl2 Hl2']].
      destruct (permutations_interleave_toggle x l1 l2 l2') as [? [??]]; eauto.
  Qed.
  Lemma permutations_Permutation l l' : l' ∈ permutations l ↔ l ≡ₚ l'.
  Proof.
    split.
    * revert l'. induction l; simpl; intros l''.
      + rewrite elem_of_list_singleton. by intros ->.
      + rewrite elem_of_list_bind. intros [l' [Hl'' ?]].
        rewrite (interleave_Permutation _ _ _ Hl''). constructor; auto.
    * induction 1; eauto using permutations_refl,
        permutations_skip, permutations_swap, permutations_trans.
  Qed.
End permutations.

(** ** Properties of the folding functions *)
Definition foldr_app := @fold_right_app.
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.
Lemma foldr_permutation {A B} (R : relation B) `{!Equivalence R}
    (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
    (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
  Proper ((≡ₚ) ==> R) (foldr f b).
Proof. induction 1; simpl; [done|by f_equiv|apply Hf|etransitivity; eauto]. Qed.

(** ** Properties of the [zip_with] and [zip] functions *)
Section zip_with.
  Context {A B C : Type} (f : A → B → C).
  Implicit Types x : A.
  Implicit Types y : B.
  Implicit Types l : list A.
  Implicit Types k : list B.

  Lemma zip_with_nil_r l : zip_with f l [] = [].
  Proof. by destruct l. Qed.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  Lemma zip_with_nil_inv l k : zip_with f l k = [] → l = [] ∨ k = [].
  Proof. destruct l, k; intros; simplify_equality'; auto. Qed.
  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_equality'; repeat eexists. Qed.
  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_equality'.
    destruct (IH l k) as (l1&k1&l2&k2&->&->&->&->&?); [done |].
    exists (x :: l1) (y :: k1) l2 k2; simpl; auto with congruence.
  Qed.
  Lemma zip_with_inj `{!Injective2 (=) (=) (=) 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.
  Lemma zip_with_length l k :
    length (zip_with f l k) = min (length l) (length k).
  Proof. revert k. induction l; intros [|??]; simpl; auto with lia. Qed.
  Lemma zip_with_length_l l k :
    length l ≤ length k → length (zip_with f l k) = length l.
  Proof. rewrite zip_with_length; lia. Qed.
  Lemma zip_with_length_r l k :
    length k ≤ length l → length (zip_with f l k) = length k.
  Proof. rewrite zip_with_length; lia. Qed.
  Lemma zip_with_length_same_l P l k :
    Forall2 P l k → length (zip_with f l k) = length l.
  Proof. induction 1; simpl; auto. Qed.
  Lemma zip_with_length_same_r P l k :
    Forall2 P l k → length (zip_with f l k) = length k.
  Proof. induction 1; simpl; auto. Qed.
  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.
  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.
  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.
  Lemma zip_with_zip l k : zip_with f l k = curry f <$> zip l k.
  Proof. revert k. by induction l; intros [|??]; f_equal'. Qed.
  Lemma zip_with_fst_snd lk :
    zip_with f (fst <$> lk) (snd <$> lk) = curry f <$> lk.
  Proof. by induction lk as [|[]]; f_equal'. Qed.
  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.
  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.
  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.
  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.
  Lemma zip_with_take_l n l k :
    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.
  Lemma zip_with_take_r n l k :
    length l ≤ 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.
  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.
  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.
End zip_with.

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_equality.
  by rewrite !zip_with_app_l, !zip_with_drop, Hl', drop_drop, !zip_with_take,
    !take_length_le, Hk' by (rewrite ?drop_length; auto with lia).
Qed.

Section zip.
  Context {A B : Type}.
  Implicit Types l : list A.
  Implicit Types k : list B.
  Lemma fst_zip l k : length l ≤ length k → fst <$> zip l k = l.
  Proof. by apply fmap_zip_with_l. Qed.
  Lemma snd_zip l k : length k ≤ length l → snd <$> zip l k = k.
  Proof. by apply fmap_zip_with_r. Qed.
  Lemma zip_fst_snd (lk : list (A * B)) : zip (fst <$> lk) (snd <$> lk) = lk.
  Proof. by induction lk as [|[]]; f_equal'. Qed.
  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.
  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.
End zip.

Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x :
  x ∈ zipped_map f l k ↔
    ∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
Proof.
  split.
  * revert l. induction k as [|z k IH]; simpl; intros l; inversion_clear 1.
    { by eexists [], k, z. }
    destruct (IH (z :: l)) as (k'&k''&y&->&->); [done |].
    eexists (z :: k'), k'', y. by rewrite reverse_cons, <-(associative_L (++)).
  * intros (k'&k''&y&->&->). revert l. induction k' as [|z k' IH]; [by left|].
    intros l; right. by rewrite reverse_cons, <-!(associative_L (++)).
Qed.
Section zipped_list_ind.
  Context {A} (P : list A → list A → Prop).
  Context (Pnil : ∀ l, P l []) (Pcons : ∀ l k x, P (x :: l) k → P l (x :: k)).
  Fixpoint zipped_list_ind l k : P l k :=
    match k with
    | [] => Pnil _ | x :: k => Pcons _ _ _ (zipped_list_ind (x :: l) k)
    end.
End zipped_list_ind.
Lemma zipped_Forall_app {A} (P : list A → list A → A → Prop) l k k' :
  zipped_Forall P l (k ++ k') → zipped_Forall P (reverse k ++ l) k'.
Proof.
  revert l. induction k as [|x k IH]; simpl; [done |].
  inversion_clear 1. rewrite reverse_cons, <-(associative_L (++)). by apply IH.
Qed.

(** * Relection over lists *)
(** We define a simple data structure [rlist] to capture a syntactic
representation of lists consisting of constants, applications and the nil list.
Note that we represent [(x ::)] as [rapp (rnode [x])]. For now, we abstract
over the type of constants, but later we use [nat]s and a list representing
a corresponding environment. *)
Inductive rlist (A : Type) :=
  rnil : rlist A | rnode : A → rlist A | rapp : rlist A → rlist A → rlist A.
Arguments rnil {_}.
Arguments rnode {_} _.
Arguments rapp {_} _ _.

Module rlist.
Fixpoint to_list {A} (t : rlist A) : list A :=
  match t with
  | rnil => [] | rnode l => [l] | rapp t1 t2 => to_list t1 ++ to_list t2
  end.
Notation env A := (list (list A)) (only parsing).
Definition eval {A} (E : env A) : rlist nat → list A :=
  fix go t :=
  match t with
  | rnil => []
  | rnode i => from_option [] (E !! i)
  | rapp t1 t2 => go t1 ++ go t2
  end.

(** A simple quoting mechanism using type classes. [QuoteLookup E1 E2 x i]
means: starting in environment [E1], look up the index [i] corresponding to the
constant [x]. In case [x] has a corresponding index [i] in [E1], the original
environment is given back as [E2]. Otherwise, the environment [E2] is extended
with a binding [i] for [x]. *)
Section quote_lookup.
  Context {A : Type}.
  Class QuoteLookup (E1 E2 : list A) (x : A) (i : nat) := {}.
  Global Instance quote_lookup_here E x : QuoteLookup (x :: E) (x :: E) x 0.
  Global Instance quote_lookup_end x : QuoteLookup [] [x] x 0.
  Global Instance quote_lookup_further E1 E2 x i y :
    QuoteLookup E1 E2 x i → QuoteLookup (y :: E1) (y :: E2) x (S i) | 1000.
End quote_lookup.

Section quote.
  Context {A : Type}.
  Class Quote (E1 E2 : env A) (l : list A) (t : rlist nat) := {}.
  Global Instance quote_nil: Quote E1 E1 [] rnil.
  Global Instance quote_node E1 E2 l i:
    QuoteLookup E1 E2 l i → Quote E1 E2 l (rnode i) | 1000.
  Global Instance quote_cons E1 E2 E3 x l i t :
    QuoteLookup E1 E2 [x] i →