list.v

Proof.
  revert n m. induction l; simpl.
  * intros. by rewrite drop_nil, !resize_nil, drop_replicate.
  * intros [|?] [|?] ?; simpl; try case_match; auto with lia.
Qed.
Lemma drop_resize_plus l n m x :
  drop n (resize (n + m) x l) = resize m x (drop n l).
Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
Lemma lookup_resize l n x i : i < n → i < length l → resize n x l !! i = l !! i.
Proof.
  intros ??. destruct (decide (n < length l)).
  * by rewrite resize_le, lookup_take by lia.
  * by rewrite resize_ge, lookup_app_l by lia.
Qed.
Lemma lookup_resize_new l n x i :
  length l ≤ i → i < n → resize n x l !! i = Some x.
Proof.
  intros ??. rewrite resize_ge by lia.
  replace i with (length l + (i - length l)) by lia.
  by rewrite lookup_app_r, lookup_replicate_2 by lia.
Qed.
Lemma lookup_resize_old l n x i : n ≤ i → resize n x l !! i = None.
Proof. intros ?. apply lookup_ge_None_2. by rewrite resize_length. Qed.
End general_properties.

Section more_general_properties.
Context {A : Type}.
Implicit Types x y z : A.
Implicit Types l k : list A.

(** ** Properties of the [reshape] function *)
Lemma reshape_length szs l : length (reshape szs l) = length szs.
Proof. revert l. by induction szs; intros; f_equal'. Qed.
Lemma join_reshape szs l :
  sum_list szs = length l → mjoin (reshape szs l) = l.
Proof.
  revert l. induction szs as [|sz szs IH]; simpl; intros l Hl; [by destruct l|].
  by rewrite IH, take_drop by (rewrite drop_length; lia).
Qed.
Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n.
Proof. induction m; simpl; auto. Qed.

(** ** Properties of [sublist_lookup] and [sublist_alter] *)
Lemma sublist_lookup_length l i n k :
  sublist_lookup i n l = Some k → length k = n.
Proof.
  unfold sublist_lookup; intros; simplify_option_equality.
  rewrite take_length, drop_length; lia.
Qed.
Lemma sublist_lookup_all l n : length l = n → sublist_lookup 0 n l = Some l.
Proof.
  intros. unfold sublist_lookup; case_option_guard; [|lia].
  by rewrite take_ge by (rewrite drop_length; lia).
Qed.
Lemma sublist_lookup_Some l i n :
  i + n ≤ length l → sublist_lookup i n l = Some (take n (drop i l)).
Proof. by unfold sublist_lookup; intros; simplify_option_equality. Qed.
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_equality by lia. Qed.
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.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_equality;
    [|by rewrite !lookup_ge_None_2 by auto].
  apply (f_equal (!! i `mod` n)) in Hlookup.
  by rewrite !lookup_take, !lookup_drop, <-!Nat.div_mod in Hlookup
    by (auto using Nat.mod_upper_bound with lia).
Qed.
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.
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_option_guard as Hi.
    { f_equal. clear Hi. revert i l Hl Hx.
      induction m as [|m IH]; intros [|i] l ??; simplify_equality'; auto.
      rewrite <-drop_drop. apply IH; rewrite ?drop_length; 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 reshape_length, replicate_length in Hx.
  * intros Hx. case_option_guard as Hi; simplify_equality'.
    revert i l Hl Hi. induction m as [|m IH]; [auto with lia|].
    intros [|i] l ??; simpl; [done|]. rewrite <-drop_drop.
    rewrite IH; rewrite ?drop_length; auto with lia.
Qed.
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_equality;
    repeat match goal with
    | H : _ ≤ length _ |- _ => rewrite take_length, drop_length in H
    end; rewrite ?take_drop_commute, ?drop_drop, ?take_take,
      ?Min.min_l, Nat.add_assoc by lia; auto with lia.
Qed.
Lemma sublist_alter_length 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_equality.
  rewrite !app_length, Hk, !take_length, !drop_length; lia.
Qed.
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 sublist_alter_length by eauto.
  unfold sublist_alter; simplify_option_equality.
  by rewrite Hk, drop_app_alt, take_app_alt by (rewrite ?take_length; lia).
Qed.
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 sublist_alter_length by eauto.
  unfold sublist_alter; simplify_option_equality; 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, !lookup_drop by done. destruct (decide (i + ii < j)).
  { by rewrite lookup_app_l, lookup_take by (rewrite ?take_length; lia). }
  rewrite lookup_app_r by (rewrite take_length; lia).
  rewrite take_length_le, lookup_app_r, lookup_drop by lia. f_equal; lia.
Qed.
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.
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_equality.
  by rewrite !take_app_alt, drop_app_alt, !(associative_L (++)), drop_app_alt,
    take_app_alt by (rewrite ?app_length, ?take_length, ?Hk; lia).
Qed.

(** ** Properties of the [mask] function *)
Lemma mask_nil f βs : mask f βs (@nil A) = [].
Proof. by destruct βs. Qed.
Lemma mask_length f βs l : length (mask f βs l) = length l.
Proof. revert βs. induction l; intros [|??]; f_equal'; auto. Qed.
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.
Lemma mask_false f l n : mask f (replicate n false) l = l.
Proof. revert l. induction n; intros [|??]; f_equal'; auto. Qed.
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.
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.
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.
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.
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 mask_length; simplify_option_equality; auto.
  by rewrite drop_mask, take_mask.
Qed.
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.
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_equality'; f_equal; auto.
Qed.
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_equality'; auto.
Qed.

(** ** Properties of the [seq] function *)
Lemma fmap_seq j n : S <$> seq j n = seq (S j) n.
Proof. revert j. induction n; intros; f_equal'; auto. Qed.
Lemma lookup_seq j n i : i < n → seq j n !! i = Some (j + i).
Proof.
  revert j i. induction n as [|n IH]; intros j [|i] ?; simpl; auto with lia.
  rewrite IH; auto with lia.
Qed.
Lemma lookup_seq_ge j n i : n ≤ i → seq j n !! i = None.
Proof. revert j i. induction n; intros j [|i] ?; simpl; auto with lia. Qed.
Lemma lookup_seq_inv j n i j' : seq j n !! i = Some j' → j' = j + i ∧ i < n.
Proof.
  destruct (le_lt_dec n i); [by rewrite lookup_seq_ge|].
  rewrite lookup_seq by done. intuition congruence.
Qed.

(** ** Properties of the [Permutation] predicate *)
Lemma Permutation_nil l : l ≡ₚ [] ↔ l = [].
Proof. split. by intro; apply Permutation_nil. by intros ->. Qed.
Lemma Permutation_singleton l x : l ≡ₚ [x] ↔ l = [x].
Proof. split. by intro; apply Permutation_length_1_inv. by intros ->. Qed.
Definition Permutation_skip := @perm_skip A.
Definition Permutation_swap := @perm_swap A.
Definition Permutation_singleton_inj := @Permutation_length_1 A.

Global Existing Instance Permutation_app'_Proper.
Global Instance: Proper ((≡ₚ) ==> (=)) (@length A).
Proof. induction 1; simpl; auto with lia. Qed.
Global Instance: Commutative (≡ₚ) (@app A).
Proof.
  intros l1. induction l1 as [|x l1 IH]; intros l2; simpl.
  * by rewrite (right_id_L [] (++)).
  * rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
Qed.
Global Instance: ∀ x : A, Injective (≡ₚ) (≡ₚ) (x ::).
Proof. red. eauto using Permutation_cons_inv. Qed.
Global Instance: ∀ k : list A, Injective (≡ₚ) (≡ₚ) (k ++).
Proof.
  red. induction k as [|x k IH]; intros l1 l2; simpl; auto.
  intros. by apply IH, (injective (x ::)).
Qed.
Global Instance: ∀ k : list A, Injective (≡ₚ) (≡ₚ) (++ k).
Proof.
  intros k l1 l2. rewrite !(commutative (++) _ k). by apply (injective (k ++)).
Qed.
Lemma replicate_Permutation n x l : replicate n x ≡ₚ l → replicate n x = l.
Proof.
  intros Hl. apply replicate_as_elem_of. split.
  * by rewrite <-Hl, replicate_length.
  * intros y. rewrite <-Hl. by apply elem_of_replicate_inv.
Qed.
Lemma reverse_Permutation l : reverse l ≡ₚ l.
Proof.
  induction l as [|x l IH]; [done|].
  by rewrite reverse_cons, (commutative (++)), IH.
Qed.

(** ** Properties of the [prefix_of] and [suffix_of] predicates *)
Global Instance: PreOrder (@prefix_of A).
Proof.
  split.
  * intros ?. eexists []. by rewrite (right_id_L [] (++)).
  * intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (associative_L (++)).
Qed.
Lemma prefix_of_nil l : [] `prefix_of` l.
Proof. by exists l. Qed.
Lemma prefix_of_nil_not x l : ¬x :: l `prefix_of` [].
Proof. by intros [k ?]. Qed.
Lemma prefix_of_cons x l1 l2 : l1 `prefix_of` l2 → x :: l1 `prefix_of` x :: l2.
Proof. intros [k ->]. by exists k. Qed.
Lemma prefix_of_cons_alt x y l1 l2 :
  x = y → l1 `prefix_of` l2 → x :: l1 `prefix_of` y :: l2.
Proof. intros ->. apply prefix_of_cons. Qed.
Lemma prefix_of_cons_inv_1 x y l1 l2 : x :: l1 `prefix_of` y :: l2 → x = y.
Proof. by intros [k ?]; simplify_equality'. Qed.
Lemma prefix_of_cons_inv_2 x y l1 l2 :
  x :: l1 `prefix_of` y :: l2 → l1 `prefix_of` l2.
Proof. intros [k ?]; simplify_equality'. by exists k. Qed.
Lemma prefix_of_app k l1 l2 : l1 `prefix_of` l2 → k ++ l1 `prefix_of` k ++ l2.
Proof. intros [k' ->]. exists k'. by rewrite (associative_L (++)). Qed.
Lemma prefix_of_app_alt k1 k2 l1 l2 :
  k1 = k2 → l1 `prefix_of` l2 → k1 ++ l1 `prefix_of` k2 ++ l2.
Proof. intros ->. apply prefix_of_app. Qed.
Lemma prefix_of_app_l l1 l2 l3 : l1 ++ l3 `prefix_of` l2 → l1 `prefix_of` l2.
Proof. intros [k ->]. exists (l3 ++ k). by rewrite (associative_L (++)). Qed.
Lemma prefix_of_app_r l1 l2 l3 : l1 `prefix_of` l2 → l1 `prefix_of` l2 ++ l3.
Proof. intros [k ->]. exists (k ++ l3). by rewrite (associative_L (++)). Qed.
Lemma prefix_of_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite app_length. lia. Qed.
Lemma prefix_of_snoc_not l x : ¬l ++ [x] `prefix_of` l.
Proof. intros [??]. discriminate_list_equality. Qed.
Global Instance: PreOrder (@suffix_of A).
Proof.
  split.
  * intros ?. by eexists [].
  * intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (associative_L (++)).
Qed.
Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2,
    Decision (l1 `prefix_of` l2) := fix go l1 l2 :=
  match l1, l2 return { l1 `prefix_of` l2 } + { ¬l1 `prefix_of` l2 } with
  | [], _ => left (prefix_of_nil _)
  | _, [] => right (prefix_of_nil_not _ _)
  | x :: l1, y :: l2 =>
    match decide_rel (=) x y with
    | left Hxy =>
      match go l1 l2 with
      | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Hxy Hl1l2)
      | right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
      end
    | right Hxy => right (Hxy ∘ prefix_of_cons_inv_1 _ _ _ _)
    end
  end.

Section prefix_ops.
  Context `{∀ x y, Decision (x = y)}.
  Lemma max_prefix_of_fst l1 l2 :
    l1 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.1.
  Proof.
    revert l2. induction l1; intros [|??]; simpl;
      repeat case_decide; f_equal'; auto.
  Qed.
  Lemma max_prefix_of_fst_alt l1 l2 k1 k2 k3 :
    max_prefix_of l1 l2 = (k1, k2, k3) → l1 = k3 ++ k1.
  Proof.
    intros. pose proof (max_prefix_of_fst l1 l2).
    by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
  Qed.
  Lemma max_prefix_of_fst_prefix l1 l2 : (max_prefix_of l1 l2).2 `prefix_of` l1.
  Proof. eexists. apply max_prefix_of_fst. Qed.
  Lemma max_prefix_of_fst_prefix_alt l1 l2 k1 k2 k3 :
    max_prefix_of l1 l2 = (k1, k2, k3) → k3 `prefix_of` l1.
  Proof. eexists. eauto using max_prefix_of_fst_alt. Qed.
  Lemma max_prefix_of_snd l1 l2 :
    l2 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.2.
  Proof.
    revert l2. induction l1; intros [|??]; simpl;
      repeat case_decide; f_equal'; auto.
  Qed.
  Lemma max_prefix_of_snd_alt l1 l2 k1 k2 k3 :
    max_prefix_of l1 l2 = (k1, k2, k3) → l2 = k3 ++ k2.
  Proof.
    intro. pose proof (max_prefix_of_snd l1 l2).
    by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
  Qed.
  Lemma max_prefix_of_snd_prefix l1 l2 : (max_prefix_of l1 l2).2 `prefix_of` l2.
  Proof. eexists. apply max_prefix_of_snd. Qed.
  Lemma max_prefix_of_snd_prefix_alt l1 l2 k1 k2 k3 :
    max_prefix_of l1 l2 = (k1,k2,k3) → k3 `prefix_of` l2.
  Proof. eexists. eauto using max_prefix_of_snd_alt. Qed.
  Lemma max_prefix_of_max l1 l2 k :
    k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` (max_prefix_of l1 l2).2.
  Proof.
    intros [l1' ->] [l2' ->]. by induction k; simpl; repeat case_decide;
      simpl; auto using prefix_of_nil, prefix_of_cons.
  Qed.
  Lemma max_prefix_of_max_alt l1 l2 k1 k2 k3 k :
    max_prefix_of l1 l2 = (k1,k2,k3) →
    k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` k3.
  Proof.
    intro. pose proof (max_prefix_of_max l1 l2 k).
    by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
  Qed.
  Lemma max_prefix_of_max_snoc l1 l2 k1 k2 k3 x1 x2 :
    max_prefix_of l1 l2 = (x1 :: k1, x2 :: k2, k3) → x1 ≠ x2.
  Proof.
    intros Hl ->. destruct (prefix_of_snoc_not k3 x2).
    eapply max_prefix_of_max_alt; eauto.
    * rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
      apply prefix_of_app, prefix_of_cons, prefix_of_nil.
    * rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
      apply prefix_of_app, prefix_of_cons, prefix_of_nil.
  Qed.
End prefix_ops.

Lemma prefix_suffix_reverse l1 l2 :
  l1 `prefix_of` l2 ↔ reverse l1 `suffix_of` reverse l2.
Proof.
  split; intros [k E]; exists (reverse k).
  * by rewrite E, reverse_app.
  * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
Qed.
Lemma suffix_prefix_reverse l1 l2 :
  l1 `suffix_of` l2 ↔ reverse l1 `prefix_of` reverse l2.
Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
Lemma suffix_of_nil l : [] `suffix_of` l.
Proof. exists l. by rewrite (right_id_L [] (++)). Qed.
Lemma suffix_of_nil_inv l : l `suffix_of` [] → l = [].
Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
Lemma suffix_of_cons_nil_inv x l : ¬x :: l `suffix_of` [].
Proof. by intros [[] ?]. Qed.
Lemma suffix_of_snoc l1 l2 x :
  l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [x].
Proof. intros [k ->]. exists k. by rewrite (associative_L (++)). Qed.
Lemma suffix_of_snoc_alt x y l1 l2 :
  x = y → l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [y].
Proof. intros ->. apply suffix_of_snoc. Qed.
Lemma suffix_of_app l1 l2 k : l1 `suffix_of` l2 → l1 ++ k `suffix_of` l2 ++ k.
Proof. intros [k' ->]. exists k'. by rewrite (associative_L (++)). Qed.
Lemma suffix_of_app_alt l1 l2 k1 k2 :
  k1 = k2 → l1 `suffix_of` l2 → l1 ++ k1 `suffix_of` l2 ++ k2.
Proof. intros ->. apply suffix_of_app. Qed.
Lemma suffix_of_snoc_inv_1 x y l1 l2 :
  l1 ++ [x] `suffix_of` l2 ++ [y] → x = y.
Proof.
  intros [k' E]. rewrite (associative_L (++)) in E.
  by simplify_list_equality.
Qed.
Lemma suffix_of_snoc_inv_2 x y l1 l2 :
  l1 ++ [x] `suffix_of` l2 ++ [y] → l1 `suffix_of` l2.
Proof.
  intros [k' E]. exists k'. rewrite (associative_L (++)) in E.
  by simplify_list_equality.
Qed.
Lemma suffix_of_app_inv l1 l2 k :
  l1 ++ k `suffix_of` l2 ++ k → l1 `suffix_of` l2.
Proof.
  intros [k' E]. exists k'. rewrite (associative_L (++)) in E.
  by simplify_list_equality.
Qed.
Lemma suffix_of_cons_l l1 l2 x : x :: l1 `suffix_of` l2 → l1 `suffix_of` l2.
Proof. intros [k ->]. exists (k ++ [x]). by rewrite <-(associative_L (++)). Qed.
Lemma suffix_of_app_l l1 l2 l3 : l3 ++ l1 `suffix_of` l2 → l1 `suffix_of` l2.
Proof. intros [k ->]. exists (k ++ l3). by rewrite <-(associative_L (++)). Qed.
Lemma suffix_of_cons_r l1 l2 x : l1 `suffix_of` l2 → l1 `suffix_of` x :: l2.
Proof. intros [k ->]. by exists (x :: k). Qed.
Lemma suffix_of_app_r l1 l2 l3 : l1 `suffix_of` l2 → l1 `suffix_of` l3 ++ l2.
Proof. intros [k ->]. exists (l3 ++ k). by rewrite (associative_L (++)). Qed.
Lemma suffix_of_cons_inv l1 l2 x y :
  x :: l1 `suffix_of` y :: l2 → x :: l1 = y :: l2 ∨ x :: l1 `suffix_of` l2.
Proof.
  intros [[|? k] E]; [by left|].
  right. simplify_equality'. by apply suffix_of_app_r.
Qed.
Lemma suffix_of_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite app_length. lia. Qed.
Lemma suffix_of_cons_not x l : ¬x :: l `suffix_of` l.
Proof. intros [??]. discriminate_list_equality. Qed.
Global Instance suffix_of_dec `{∀ x y, Decision (x = y)} l1 l2 :
  Decision (l1 `suffix_of` l2).
Proof.
  refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
   abstract (by rewrite suffix_prefix_reverse).
Defined.

Section max_suffix_of.
  Context `{∀ x y, Decision (x = y)}.

  Lemma max_suffix_of_fst l1 l2 :
    l1 = (max_suffix_of l1 l2).1.1 ++ (max_suffix_of l1 l2).2.
  Proof.
    rewrite <-(reverse_involutive l1) at 1.
    rewrite (max_prefix_of_fst (reverse l1) (reverse l2)). unfold max_suffix_of.
    destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
    by rewrite reverse_app.
  Qed.
  Lemma max_suffix_of_fst_alt l1 l2 k1 k2 k3 :
    max_suffix_of l1 l2 = (k1, k2, k3) → l1 = k1 ++ k3.
  Proof.
    intro. pose proof (max_suffix_of_fst l1 l2).
    by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
  Qed.
  Lemma max_suffix_of_fst_suffix l1 l2 : (max_suffix_of l1 l2).2 `suffix_of` l1.
  Proof. eexists. apply max_suffix_of_fst. Qed.
  Lemma max_suffix_of_fst_suffix_alt l1 l2 k1 k2 k3 :
    max_suffix_of l1 l2 = (k1, k2, k3) → k3 `suffix_of` l1.
  Proof. eexists. eauto using max_suffix_of_fst_alt. Qed.
  Lemma max_suffix_of_snd l1 l2 :
    l2 = (max_suffix_of l1 l2).1.2 ++ (max_suffix_of l1 l2).2.
  Proof.
    rewrite <-(reverse_involutive l2) at 1.
    rewrite (max_prefix_of_snd (reverse l1) (reverse l2)). unfold max_suffix_of.
    destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
    by rewrite reverse_app.
  Qed.
  Lemma max_suffix_of_snd_alt l1 l2 k1 k2 k3 :
    max_suffix_of l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
  Proof.
    intro. pose proof (max_suffix_of_snd l1 l2).
    by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
  Qed.
  Lemma max_suffix_of_snd_suffix l1 l2 : (max_suffix_of l1 l2).2 `suffix_of` l2.
  Proof. eexists. apply max_suffix_of_snd. Qed.
  Lemma max_suffix_of_snd_suffix_alt l1 l2 k1 k2 k3 :
    max_suffix_of l1 l2 = (k1,k2,k3) → k3 `suffix_of` l2.
  Proof. eexists. eauto using max_suffix_of_snd_alt. Qed.
  Lemma max_suffix_of_max l1 l2 k :
    k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` (max_suffix_of l1 l2).2.
  Proof.
    generalize (max_prefix_of_max (reverse l1) (reverse l2)).
    rewrite !suffix_prefix_reverse. unfold max_suffix_of.
    destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
    rewrite reverse_involutive. auto.
  Qed.
  Lemma max_suffix_of_max_alt l1 l2 k1 k2 k3 k :
    max_suffix_of l1 l2 = (k1, k2, k3) →
    k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` k3.
  Proof.
    intro. pose proof (max_suffix_of_max l1 l2 k).
    by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
  Qed.
  Lemma max_suffix_of_max_snoc l1 l2 k1 k2 k3 x1 x2 :
    max_suffix_of l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) → x1 ≠ x2.
  Proof.
    intros Hl ->. destruct (suffix_of_cons_not x2 k3).
    eapply max_suffix_of_max_alt; eauto.
    * rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
      by apply (suffix_of_app [x2]), suffix_of_app_r.
    * rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
      by apply (suffix_of_app [x2]), suffix_of_app_r.
  Qed.
End max_suffix_of.

(** ** Properties of the [sublist] predicate *)
Lemma sublist_length l1 l2 : l1 `sublist` l2 → length l1 ≤ length l2.
Proof. induction 1; simpl; auto with arith. Qed.
Lemma sublist_nil_l l : [] `sublist` l.
Proof. induction l; try constructor; auto. Qed.
Lemma sublist_nil_r l : l `sublist` [] ↔ l = [].
Proof. split. by inversion 1. intros ->. constructor. Qed.
Lemma sublist_app l1 l2 k1 k2 :
  l1 `sublist` l2 → k1 `sublist` k2 → l1 ++ k1 `sublist` l2 ++ k2.
Proof. induction 1; simpl; try constructor; auto. Qed.
Lemma sublist_inserts_l k l1 l2 : l1 `sublist` l2 → l1 `sublist` k ++ l2.
Proof. induction k; try constructor; auto. Qed.
Lemma sublist_inserts_r k l1 l2 : l1 `sublist` l2 → l1 `sublist` l2 ++ k.
Proof. induction 1; simpl; try constructor; auto using sublist_nil_l. Qed.
Lemma sublist_cons_r x l k :
  l `sublist` x :: k ↔ l `sublist` k ∨ ∃ l', l = x :: l' ∧ l' `sublist` k.
Proof. split. inversion 1; eauto. intros [?|(?&->&?)]; constructor; auto. Qed.
Lemma sublist_cons_l x l k :
  x :: l `sublist` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist` k2.
Proof.
  split.
  * intros Hlk. induction k as [|y k IH]; inversion Hlk.
    + eexists [], k. by repeat constructor.
    + destruct IH as (k1&k2&->&?); auto. by exists (y :: k1) k2.
  * intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip.
Qed.
Lemma sublist_app_r l k1 k2 :
  l `sublist` k1 ++ k2 ↔
    ∃ l1 l2, l = l1 ++ l2 ∧ l1 `sublist` k1 ∧ l2 `sublist` k2.
Proof.
  split.
  * revert l k2. induction k1 as [|y k1 IH]; intros l k2; simpl.
    { eexists [], l. by repeat constructor. }
    rewrite sublist_cons_r. intros [?|(l' & ? &?)]; subst.
    + destruct (IH l k2) as (l1&l2&?&?&?); trivial; subst.
      exists l1 l2. auto using sublist_cons.
    + destruct (IH l' k2) as (l1&l2&?&?&?); trivial; subst.
      exists (y :: l1) l2. auto using sublist_skip.
  * intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
Lemma sublist_app_l l1 l2 k :
  l1 ++ l2 `sublist` k ↔
    ∃ k1 k2, k = k1 ++ k2 ∧ l1 `sublist` k1 ∧ l2 `sublist` k2.
Proof.
  split.
  * revert l2 k. induction l1 as [|x l1 IH]; intros l2 k; simpl.
    { eexists [], k. by repeat constructor. }
    rewrite sublist_cons_l. intros (k1 & k2 &?&?); subst.
    destruct (IH l2 k2) as (h1 & h2 &?&?&?); trivial; subst.
    exists (k1 ++ x :: h1) h2. rewrite <-(associative_L (++)).
    auto using sublist_inserts_l, sublist_skip.
  * intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist` k ++ l2 → l1 `sublist` l2.
Proof.
  induction k as [|y k IH]; simpl; [done |].
  rewrite sublist_cons_r. intros [Hl12|(?&?&?)]; [|simplify_equality; eauto].
  rewrite sublist_cons_l in Hl12. destruct Hl12 as (k1&k2&Hk&?).
  apply IH. rewrite Hk. eauto using sublist_inserts_l, sublist_cons.
Qed.
Lemma sublist_app_inv_r k l1 l2 : l1 ++ k `sublist` l2 ++ k → l1 `sublist` l2.
Proof.
  revert l1 l2. induction k as [|y k IH]; intros l1 l2.
  { by rewrite !(right_id_L [] (++)). }
  intros. feed pose proof (IH (l1 ++ [y]) (l2 ++ [y])) as Hl12.
  { by rewrite <-!(associative_L (++)). }
  rewrite sublist_app_l in Hl12. destruct Hl12 as (k1&k2&E&?&Hk2).
  destruct k2 as [|z k2] using rev_ind; [inversion Hk2|].
  rewrite (associative_L (++)) in E; simplify_list_equality.
  eauto using sublist_inserts_r.
Qed.
Global Instance: PartialOrder (@sublist A).
Proof.
  split; [split|].
  * intros l. induction l; constructor; auto.
  * intros l1 l2 l3 Hl12. revert l3. induction Hl12.
    + auto using sublist_nil_l.
    + intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst.
      eauto using sublist_inserts_l, sublist_skip.
    + intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst.
      eauto using sublist_inserts_l, sublist_cons.
  * intros l1 l2 Hl12 Hl21. apply sublist_length in Hl21.
    induction Hl12; f_equal'; auto with arith.
    apply sublist_length in Hl12. lia.
Qed.
Lemma sublist_take l i : take i l `sublist` l.
Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_r. Qed.
Lemma sublist_drop l i : drop i l `sublist` l.
Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_l. Qed.
Lemma sublist_delete l i : delete i l `sublist` l.
Proof. revert i. by induction l; intros [|?]; simpl; constructor. Qed.
Lemma sublist_foldr_delete l is : foldr delete l is `sublist` l.
Proof.
  induction is as [|i is IH]; simpl; [done |].
  transitivity (foldr delete l is); auto using sublist_delete.
Qed.
Lemma sublist_alt l1 l2 : l1 `sublist` l2 ↔ ∃ is, l1 = foldr delete l2 is.
Proof.
  split; [|intros [is ->]; apply sublist_foldr_delete].
  intros Hl12. cut (∀ k, ∃ is, k ++ l1 = foldr delete (k ++ l2) is).
  { intros help. apply (help []). }
  induction Hl12 as [|x l1 l2 _ IH|x l1 l2 _ IH]; intros k.
  * by eexists [].
  * destruct (IH (k ++ [x])) as [is His]. exists is.
    by rewrite <-!(associative_L (++)) in His.
  * destruct (IH k) as [is His]. exists (is ++ [length k]).
    rewrite fold_right_app. simpl. by rewrite delete_middle.
Qed.
Lemma Permutation_sublist l1 l2 l3 :
  l1 ≡ₚ l2 → l2 `sublist` l3 → ∃ l4, l1 `sublist` l4 ∧ l4 ≡ₚ l3.
Proof.
  intros Hl1l2. revert l3.
  induction Hl1l2 as [|x l1 l2 ? IH|x y l1|l1 l1' l2 ? IH1 ? IH2].
  * intros l3. by exists l3.
  * intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst.
    destruct (IH l3'') as (l4&?&Hl4); auto. exists (l3' ++ x :: l4).
    split. by apply sublist_inserts_l, sublist_skip. by rewrite Hl4.
  * intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?& Hl3); subst.
    rewrite sublist_cons_l in Hl3. destruct Hl3 as (l5'&l5''&?& Hl5); subst.
    exists (l3' ++ y :: l5' ++ x :: l5''). split.
    - by do 2 apply sublist_inserts_l, sublist_skip.
    - by rewrite !Permutation_middle, Permutation_swap.
  * intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial.
    destruct (IH1 l3') as (l3'' &?&?); trivial. exists l3''.
    split. done. etransitivity; eauto.
Qed.
Lemma sublist_Permutation l1 l2 l3 :
  l1 `sublist` l2 → l2 ≡ₚ l3 → ∃ l4, l1 ≡ₚ l4 ∧ l4 `sublist` l3.
Proof.
  intros Hl1l2 Hl2l3. revert l1 Hl1l2.
  induction Hl2l3 as [|x l2 l3 ? IH|x y l2|l2 l2' l3 ? IH1 ? IH2].
  * intros l1. by exists l1.
  * intros l1. rewrite sublist_cons_r. intros [?|(l1'&l1''&?)]; subst.
    { destruct (IH l1) as (l4&?&?); trivial.
      exists l4. split. done. by constructor. }
    destruct (IH l1') as (l4&?&Hl4); auto. exists (x :: l4).
    split. by constructor. by constructor.
  * intros l1. rewrite sublist_cons_r. intros [Hl1|(l1'&l1''&Hl1)]; subst.
    { exists l1. split; [done|]. rewrite sublist_cons_r in Hl1.
      destruct Hl1 as [?|(l1'&?&?)]; subst; by repeat constructor. }
    rewrite sublist_cons_r in Hl1. destruct Hl1 as [?|(l1''&?&?)]; subst.
    + exists (y :: l1'). by repeat constructor.
    + exists (x :: y :: l1''). by repeat constructor.
  * intros l1 ?. destruct (IH1 l1) as (l3'&?&?); trivial.
    destruct (IH2 l3') as (l3'' &?&?); trivial. exists l3''.
    split; [|done]. etransitivity; eauto.
Qed.

(** Properties of the [contains] predicate *)
Lemma contains_length l1 l2 : l1 `contains` l2 → length l1 ≤ length l2.
Proof. induction 1; simpl; auto with lia. Qed.
Lemma contains_nil_l l : [] `contains` l.
Proof. induction l; constructor; auto. Qed.
Lemma contains_nil_r l : l `contains` [] ↔ l = [].
Proof.
  split; [|intros ->; constructor].
  intros Hl. apply contains_length in Hl. destruct l; simpl in *; auto with lia.
Qed.
Global Instance: PreOrder (@contains A).
Proof.
  split.
  * intros l. induction l; constructor; auto.
  * red. apply contains_trans.
Qed.
Lemma Permutation_contains l1 l2 : l1 ≡ₚ l2 → l1 `contains` l2.
Proof. induction 1; econstructor; eauto. Qed.
Lemma sublist_contains l1 l2 : l1 `sublist` l2 → l1 `contains` l2.
Proof. induction 1; constructor; auto. Qed.
Lemma contains_Permutation l1 l2 : l1 `contains` l2 → ∃ k, l2 ≡ₚ l1 ++ k.
Proof.
  induction 1 as
    [|x y l ? [k Hk]| |x l1 l2 ? [k Hk]|l1 l2 l3 ? [k Hk] ? [k' Hk']].
  * by eexists [].
  * exists k. by rewrite Hk.
  * eexists []. rewrite (right_id_L [] (++)). by constructor.
  * exists (x :: k). by rewrite Hk, Permutation_middle.
  * exists (k ++ k'). by rewrite Hk', Hk, (associative_L (++)).
Qed.
Lemma contains_Permutation_length_le l1 l2 :
  length l2 ≤ length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
Proof.
  intros Hl21 Hl12. destruct (contains_Permutation l1 l2) as [[|??] Hk]; auto.
  * by rewrite Hk, (right_id_L [] (++)).
  * rewrite Hk, app_length in Hl21; simpl in Hl21; lia.
Qed.
Lemma contains_Permutation_length_eq l1 l2 :
  length l2 = length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
Proof. intro. apply contains_Permutation_length_le. lia. Qed.
Global Instance: Proper ((≡ₚ) ==> (≡ₚ) ==> iff) (@contains A).
Proof.
  intros l1 l2 ? k1 k2 ?. split; intros.
  * transitivity l1. by apply Permutation_contains.
    transitivity k1. done. by apply Permutation_contains.
  * transitivity l2. by apply Permutation_contains.
    transitivity k2. done. by apply Permutation_contains.
Qed.
Global Instance: AntiSymmetric (≡ₚ) (@contains A).
Proof. red. auto using contains_Permutation_length_le, contains_length. Qed.
Lemma contains_take l i : take i l `contains` l.
Proof. auto using sublist_take, sublist_contains. Qed.
Lemma contains_drop l i : drop i l `contains` l.
Proof. auto using sublist_drop, sublist_contains. Qed.
Lemma contains_delete l i : delete i l `contains` l.
Proof. auto using sublist_delete, sublist_contains. Qed.
Lemma contains_foldr_delete l is : foldr delete l is `sublist` l.
Proof. auto using sublist_foldr_delete, sublist_contains. Qed.
Lemma contains_sublist_l l1 l3 :
  l1 `contains` l3 ↔ ∃ l2, l1 `sublist` l2 ∧ l2 ≡ₚ l3.
Proof.
  split.
  { intros Hl13. elim Hl13; clear l1 l3 Hl13.
    * by eexists [].
    * intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
    * intros x y l. exists (y :: x :: l). by repeat constructor.
    * intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
    * intros l1 l3 l5 ? (l2&?&?) ? (l4&?&?).
      destruct (Permutation_sublist l2 l3 l4) as (l3'&?&?); trivial.
      exists l3'. split; etransitivity; eauto. }
  intros (l2&?&?).
  transitivity l2; auto using sublist_contains, Permutation_contains.
Qed.
Lemma contains_sublist_r l1 l3 :
  l1 `contains` l3 ↔ ∃ l2, l1 ≡ₚ l2 ∧ l2 `sublist` l3.
Proof.
  rewrite contains_sublist_l.
  split; intros (l2&?&?); eauto using sublist_Permutation, Permutation_sublist.
Qed.
Lemma contains_inserts_l k l1 l2 : l1 `contains` l2 → l1 `contains` k ++ l2.
Proof. induction k; try constructor; auto. Qed.
Lemma contains_inserts_r k l1 l2 : l1 `contains` l2 → l1 `contains` l2 ++ k.
Proof. rewrite (commutative (++)). apply contains_inserts_l. Qed.
Lemma contains_skips_l k l1 l2 : l1 `contains` l2 → k ++ l1 `contains` k ++ l2.
Proof. induction k; try constructor; auto. Qed.
Lemma contains_skips_r k l1 l2 : l1 `contains` l2 → l1 ++ k `contains` l2 ++ k.
Proof. rewrite !(commutative (++) _ k). apply contains_skips_l. Qed.
Lemma contains_app l1 l2 k1 k2 :
  l1 `contains` l2 → k1 `contains` k2 → l1 ++ k1 `contains` l2 ++ k2.
Proof.
  transitivity (l1 ++ k2); auto using contains_skips_l, contains_skips_r.
Qed.
Lemma contains_cons_r x l k :
  l `contains` x :: k ↔ l `contains` k ∨ ∃ l', l ≡ₚ x :: l' ∧ l' `contains` k.
Proof.
  split.
  * rewrite contains_sublist_r. intros (l'&E&Hl').
    rewrite sublist_cons_r in Hl'. destruct Hl' as [?|(?&?&?)]; subst.
    + left. rewrite E. eauto using sublist_contains.
    + right. eauto using sublist_contains.
  * intros [?|(?&E&?)]; [|rewrite E]; by constructor.
Qed.
Lemma contains_cons_l x l k :
  x :: l `contains` k ↔ ∃ k', k ≡ₚ x :: k' ∧ l `contains` k'.
Proof.
  split.
  * rewrite contains_sublist_l. intros (l'&Hl'&E).
    rewrite sublist_cons_l in Hl'. destruct Hl' as (k1&k2&?&?); subst.
    exists (k1 ++ k2). split; eauto using contains_inserts_l, sublist_contains.
    by rewrite Permutation_middle.
  * intros (?&E&?). rewrite E. by constructor.
Qed.
Lemma contains_app_r l k1 k2 :
  l `contains` k1 ++ k2 ↔ ∃ l1 l2,
    l ≡ₚ l1 ++ l2 ∧ l1 `contains` k1 ∧ l2 `contains` k2.
Proof.
  split.
  * rewrite contains_sublist_r. intros (l'&E&Hl').
    rewrite sublist_app_r in Hl'. destruct Hl' as (l1&l2&?&?&?); subst.
    exists l1 l2. eauto using sublist_contains.
  * intros (?&?&E&?&?). rewrite E. eauto using contains_app.
Qed.
Lemma contains_app_l l1 l2 k :
  l1 ++ l2 `contains` k ↔ ∃ k1 k2,
    k ≡ₚ k1 ++ k2 ∧ l1 `contains` k1 ∧ l2 `contains` k2.
Proof.
  split.
  * rewrite contains_sublist_l. intros (l'&Hl'&E).
    rewrite sublist_app_l in Hl'. destruct Hl' as (k1&k2&?&?&?); subst.
    exists k1 k2. split. done. eauto using sublist_contains.
  * intros (?&?&E&?&?). rewrite E. eauto using contains_app.
Qed.
Lemma contains_app_inv_l l1 l2 k :
  k ++ l1 `contains` k ++ l2 → l1 `contains` l2.
Proof.
  induction k as [|y k IH]; simpl; [done |]. rewrite contains_cons_l.
  intros (?&E&?). apply Permutation_cons_inv in E. apply IH. by rewrite E.
Qed.
Lemma contains_app_inv_r l1 l2 k :
  l1 ++ k `contains` l2 ++ k → l1 `contains` l2.
Proof.
  revert l1 l2. induction k as [|y k IH]; intros l1 l2.
  { by rewrite !(right_id_L [] (++)). }
  intros. feed pose proof (IH (l1 ++ [y]) (l2 ++ [y])) as Hl12.
  { by rewrite <-!(associative_L (++)). }
  rewrite contains_app_l in Hl12. destruct Hl12 as (k1&k2&E1&?&Hk2).
  rewrite contains_cons_l in Hk2. destruct Hk2 as (k2'&E2&?).
  rewrite E2, (Permutation_cons_append k2'), (associative_L (++)) in E1.
  apply Permutation_app_inv_r in E1. rewrite E1. eauto using contains_inserts_r.
Qed.
Lemma contains_cons_middle x l k1 k2 :
  l `contains` k1 ++ k2 → x :: l `contains` k1 ++ x :: k2.
Proof. rewrite <-Permutation_middle. by apply contains_skip. Qed.
Lemma contains_app_middle l1 l2 k1 k2 :
  l2 `contains` k1 ++ k2 → l1 ++ l2 `contains` k1 ++ l1 ++ k2.
Proof.
  rewrite !(associative (++)), (commutative (++) k1 l1), <-(associative_L (++)).
  by apply contains_skips_l.
Qed.
Lemma contains_middle l k1 k2 : l `contains` k1 ++ l ++ k2.
Proof. by apply contains_inserts_l, contains_inserts_r. Qed.

Lemma Permutation_alt l1 l2 :
  l1 ≡ₚ l2 ↔ length l1 = length l2 ∧ l1 `contains` l2.
Proof.
  split.
  * by intros Hl; rewrite Hl.
  * intros [??]; auto using contains_Permutation_length_eq.
Qed.

Lemma NoDup_contains l k : NoDup l → (∀ x, x ∈ l → x ∈ k) → l `contains` k.
Proof.
  intros Hl. revert k. induction Hl as [|x l Hx ? IH].
  { intros k Hk. by apply contains_nil_l. }
  intros k Hlk. destruct (elem_of_list_split k x) as (l1&l2&?); subst.
  { apply Hlk. by constructor. }
  rewrite <-Permutation_middle. apply contains_skip, IH.
  intros y Hy. rewrite elem_of_app.
  specialize (Hlk y). rewrite elem_of_app, !elem_of_cons in Hlk.
  by destruct Hlk as [?|[?|?]]; subst; eauto.
Qed.
Lemma NoDup_Permutation l k : NoDup l → NoDup k → (∀ x, x ∈ l ↔ x ∈ k) → l ≡ₚ k.
Proof.
  intros. apply (anti_symmetric contains); apply NoDup_contains; naive_solver.
Qed.

Section contains_dec.
  Context `{∀ x y, Decision (x = y)}.

  Lemma list_remove_Permutation l1 l2 k1 x :
    l1 ≡ₚ l2 → list_remove x l1 = Some k1 →
    ∃ k2, list_remove x l2 = Some k2 ∧ k1 ≡ₚ k2.
  Proof.
    intros Hl. revert k1. induction Hl
      as [|y l1 l2 ? IH|y1 y2 l|l1 l2 l3 ? IH1 ? IH2]; simpl; intros k1 Hk1.
    * done.
    * case_decide; simplify_equality; eauto.
      destruct (list_remove x l1) as [l|] eqn:?; simplify_equality.
      destruct (IH l) as (?&?&?); simplify_option_equality; eauto.
    * simplify_option_equality; eauto using Permutation_swap.
    * destruct (IH1 k1) as (k2&?&?); trivial.
      destruct (IH2 k2) as (k3&?&?); trivial.
      exists k3. split; eauto. by transitivity k2.
  Qed.
  Lemma list_remove_Some l k x : list_remove x l = Some k → l ≡ₚ x :: k.
  Proof.
    revert k. induction l as [|y l IH]; simpl; intros k ?; [done |].
    simplify_option_equality; auto. by rewrite Permutation_swap, <-IH.
  Qed.
  Lemma list_remove_Some_inv l k x :
    l ≡ₚ x :: k → ∃ k', list_remove x l = Some k' ∧ k ≡ₚ k'.
  Proof.
    intros. destruct (list_remove_Permutation (x :: k) l k x) as (k'&?&?).
    * done.
    * simpl; by case_decide.
    * by exists k'.
  Qed.
  Lemma list_remove_list_contains l1 l2 :
    l1 `contains` l2 ↔ is_Some (list_remove_list l1 l2).
  Proof.
    split.
    * revert l2. induction l1 as [|x l1 IH]; simpl.
      { intros l2 _. by exists l2. }
      intros l2. rewrite contains_cons_l. intros (k&Hk&?).
      destruct (list_remove_Some_inv l2 k x) as (k2&?&Hk2); trivial.
      simplify_option_equality. apply IH. by rewrite <-Hk2.
    * intros [k Hk]. revert l2 k Hk.
      induction l1 as [|x l1 IH]; simpl; intros l2 k.
      { intros. apply contains_nil_l. }
      destruct (list_remove x l2) as [k'|] eqn:?; intros; simplify_equality.
      rewrite contains_cons_l. eauto using list_remove_Some.
  Qed.
  Global Instance contains_dec l1 l2 : Decision (l1 `contains` l2).
  Proof.
   refine (cast_if (decide (is_Some (list_remove_list l1 l2))));
    abstract (rewrite list_remove_list_contains; tauto).
  Defined.
  Global Instance Permutation_dec l1 l2 : Decision (l1 ≡ₚ l2).
  Proof.
   refine (cast_if_and
    (decide (length l1 = length l2)) (decide (l1 `contains` l2)));
    abstract (rewrite Permutation_alt; tauto).
  Defined.
End contains_dec.
End more_general_properties.

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

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

  Definition Forall_nil_2 := @Forall_nil A.
  Definition Forall_cons_2 := @Forall_cons A.
  Lemma Forall_forall l : Forall P l ↔ ∀ x, x ∈ l → P x.
  Proof.
    split; [induction 1; inversion 1; subst; auto|].
    intros Hin; induction l as [|x l IH]; constructor; [apply Hin; constructor|].
    apply IH. intros ??. apply Hin. by constructor.
  Qed.
  Lemma Forall_nil : Forall P [] ↔ True.
  Proof. done. Qed.
  Lemma Forall_cons_1 x l : Forall P (x :: l) → P x ∧ Forall P l.
  Proof. by inversion 1. Qed.
  Lemma Forall_cons x l : Forall P (x :: l) ↔ P x ∧ Forall P l.
  Proof. split. by inversion 1. intros [??]. by constructor. Qed.
  Lemma Forall_singleton x : Forall P [x] ↔ P x.
  Proof. rewrite Forall_cons, Forall_nil; tauto. Qed.
  Lemma Forall_app_2 l1 l2 : Forall P l1 → Forall P l2 → Forall P (l1 ++ l2).
  Proof. induction 1; simpl; auto. Qed.
  Lemma Forall_app l1 l2 : Forall P (l1 ++ l2) ↔ Forall P l1 ∧ Forall P l2.
  Proof.
    split; [induction l1; inversion 1; intuition|].
    intros [??]; auto using Forall_app_2.
  Qed.
  Lemma Forall_true l : (∀ x, P x) → Forall P l.
  Proof. induction l; auto. Qed.
  Lemma Forall_impl (Q : A → Prop) l :
    Forall P l → (∀ x, P x → Q x) → Forall Q l.
  Proof. intros H ?. induction H; auto. Defined.
  Global Instance Forall_proper:
    Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Forall A).
  Proof. split; subst; induction 1; constructor (by firstorder auto). Qed.
  Lemma Forall_iff l (Q : A → Prop) :
    (∀ x, P x ↔ Q x) → Forall P l ↔ Forall Q l.
  Proof. intros H. apply Forall_proper. red; apply H. done. Qed.
  Lemma Forall_not l : length l ≠ 0 → Forall (not ∘ P) l → ¬Forall P l.
  Proof. by destruct 2; inversion 1. Qed.
  Lemma Forall_and {Q} l : Forall (λ x, P x ∧ Q x) l ↔ Forall P l ∧ Forall Q l.
  Proof.
    split; [induction 1; constructor; naive_solver|].
    intros [Hl Hl']; revert Hl'; induction Hl; inversion_clear 1; auto.
  Qed.
  Lemma Forall_and_l {Q} l : Forall (λ x, P x ∧ Q x) l → Forall P l.
  Proof. rewrite Forall_and; tauto. Qed.
  Lemma Forall_and_r {Q} l : Forall (λ x, P x ∧ Q x) l → Forall Q l.
  Proof. rewrite Forall_and; tauto. Qed.
  Lemma Forall_delete l i : Forall P l → Forall P (delete i l).
  Proof. intros H. revert i. by induction H; intros [|i]; try constructor. Qed.
  Lemma Forall_lookup l : Forall P l ↔ ∀ i x, l !! i = Some x → P x.
  Proof.
    rewrite Forall_forall. setoid_rewrite elem_of_list_lookup. naive_solver.
  Qed.
  Lemma Forall_lookup_1 l i x : Forall P l → l !! i = Some x → P x.
  Proof. rewrite Forall_lookup. eauto. Qed.
  Lemma Forall_lookup_2 l : (∀ i x, l !! i = Some x → P x) → Forall P l.
  Proof. by rewrite Forall_lookup. Qed.
  Lemma Forall_alter f l i :
    Forall P l → (∀ x, l!!i = Some x → P x → P (f x)) → Forall P (alter f i l).
  Proof.
    intros Hl. revert i. induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.
  Lemma Forall_alter_inv f l i :
    Forall P (alter f i l) → (∀ x, l!!i = Some x → P (f x) → P x) → Forall P l.
  Proof.
    revert i. induction l; intros [|?]; simpl;
      inversion_clear 1; constructor; eauto.
  Qed.
  Lemma Forall_replicate n x : P x → Forall P (replicate n x).
  Proof. induction n; simpl; constructor; auto. Qed.
  Lemma Forall_replicate_eq n (x : A) : Forall (x =) (replicate n x).
  Proof. induction n; simpl; constructor; auto. Qed.