phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_relations.v *)
Lemma NoDup_lookup l i j x :
  NoDup l → l !! i = Some x → l !! j = Some x → i = j.
Proof.
  intros Hl. revert i j. induction Hl as [|x' l Hx Hl IH].
  { intros; simplify_eq. }
  intros [|i] [|j] ??; simplify_eq/=; eauto with f_equal;
    exfalso; eauto using list_elem_of_lookup_2.
Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_alt l :
  NoDup l ↔ ∀ i j x, l !! i = Some x → l !! j = Some x → i = j.
Proof.
  split; eauto using NoDup_lookup.
  induction l as [|x l IH]; intros Hl; constructor.
  - rewrite list_elem_of_lookup. intros [i ?].
    opose proof* (Hl (S i) 0); by auto.
  - apply IH. intros i j x' ??. by apply (inj S), (Hl (S i) (S j) x').
Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_filter (P : A → Prop) `{∀ x, Decision (P x)} l :
  NoDup l → NoDup (filter P l).
Proof.
  induction 1; rewrite ?filter_cons; repeat case_decide;
    rewrite ?NoDup_nil, ?NoDup_cons, ?list_elem_of_filter; tauto.
Qed.
(* stdpp/list_relations.v *)
Instance NoDup_dec: ∀ l, Decision (NoDup l)
:=
    fix NoDup_dec l :=
    match l return Decision (NoDup l) with
    | [] => left NoDup_nil_2
    | x :: l =>
      match decide_rel (∈) x l with
      | left Hin => right (λ H, NoDup_cons_1_1 _ _ H Hin)
      | right Hin =>
        match NoDup_dec l with
        | left H => left (NoDup_cons_2 _ _ Hin H)
        | right H => right (H ∘ NoDup_cons_1_2 _ _)
        end
      end
    end.
(* stdpp/list_relations.v *)
Lemma elem_of_remove_dups l x : x ∈ remove_dups l ↔ x ∈ l.
Proof.
    split; induction l; simpl; repeat case_decide;
      rewrite ?elem_of_cons; intuition (simplify_eq; auto).
  Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_remove_dups l : NoDup (remove_dups l).
Proof.
    induction l; simpl; repeat case_decide; try constructor; auto.
    by rewrite elem_of_remove_dups.
  Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_list_difference l k : NoDup l → NoDup (list_difference l k).
Proof.
    induction 1; simpl; try case_decide.
    - constructor.
    - done.
    - constructor; [|done]. rewrite list_elem_of_difference; intuition.
  Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_list_union l k : NoDup l → NoDup k → NoDup (list_union l k).
Proof.
    intros. apply NoDup_app. repeat split.
    - by apply NoDup_list_difference.
    - intro. rewrite list_elem_of_difference. intuition.
    - done.
  Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_list_intersection l k : NoDup l → NoDup (list_intersection l k).
Proof.
    induction 1; simpl; try case_decide.
    - constructor.
    - constructor; [|done]. rewrite list_elem_of_intersection; intuition.
    - done.
  Qed.
(* stdpp/list_relations.v *)
(* ** Properties of the [Permutation] predicate *)
Lemma Permutation_nil_r l : l ≡ₚ [] ↔ l = [].
Proof. split; [by intro; apply Permutation_nil | by intros ->]. Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_singleton_r l x : l ≡ₚ [x] ↔ l = [x].
Proof. split; [by intro; apply Permutation_length_1_inv | by intros ->]. Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_nil_l l : [] ≡ₚ l ↔ [] = l.
Proof. by rewrite (symmetry_iff (≡ₚ)), Permutation_nil_r. Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_singleton_l l x : [x] ≡ₚ l ↔ [x] = l.
Proof. by rewrite (symmetry_iff (≡ₚ)), Permutation_singleton_r. Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_skip x l l' : l ≡ₚ l' → x :: l ≡ₚ x :: l'.
Proof. apply perm_skip. Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_swap x y l : y :: x :: l ≡ₚ x :: y :: l.
Proof. apply perm_swap. Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_singleton_inj x y : [x] ≡ₚ [y] → x = y.
Proof. apply Permutation_length_1. Qed.
(* stdpp/list_relations.v *)
Instance length_Permutation_proper : Proper ((≡ₚ) ==> (=)) (@length A).
Proof. induction 1; simpl; auto with lia. Qed.
(* stdpp/list_relations.v *)
Instance elem_of_Permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈.).
Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
(* stdpp/list_relations.v *)
Instance NoDup_Permutation_proper: Proper ((≡ₚ) ==> iff) (@NoDup A).
Proof.
  induction 1 as [|x l k Hlk IH | |].
  - by rewrite !NoDup_nil.
  - by rewrite !NoDup_cons, IH, Hlk.
  - rewrite !NoDup_cons, !elem_of_cons. intuition.
  - intuition.
Qed.
(* stdpp/list_relations.v *)
Instance app_Permutation_comm : Comm (≡ₚ) (@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.
(* stdpp/list_relations.v *)
Instance cons_Permutation_inj_r x : Inj (≡ₚ) (≡ₚ) (x ::.).
Proof. red. eauto using Permutation_cons_inv. Qed.
(* stdpp/list_relations.v *)
Instance app_Permutation_inj_r k : Inj (≡ₚ) (≡ₚ) (k ++.).
Proof.
  induction k as [|x k IH]; intros l1 l2; simpl; auto.
  intros. by apply IH, (inj (x ::.)).
Qed.
(* stdpp/list_relations.v *)
Instance cons_Permutation_inj_l k : Inj (=) (≡ₚ) (.:: k).
Proof.
  intros x1 x2 Hperm. apply Permutation_singleton_inj.
  apply (inj (k ++.)). by rewrite !(comm (++) k).
Qed.
(* stdpp/list_relations.v *)
Instance app_Permutation_inj_l k : Inj (≡ₚ) (≡ₚ) (.++ k).
Proof. intros l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++.)). Qed.
(* stdpp/list_relations.v *)
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, length_replicate.
  - intros y. rewrite <-Hl. by apply elem_of_replicate_inv.
Qed.
(* stdpp/list_relations.v *)
Lemma reverse_Permutation l : reverse l ≡ₚ l.
Proof.
  induction l as [|x l IH]; [done|].
  by rewrite reverse_cons, (comm (++)), IH.
Qed.
(* stdpp/list_relations.v *)
Lemma delete_Permutation l i x : l !! i = Some x → l ≡ₚ x :: delete i l.
Proof.
  revert i; induction l as [|y l IH]; intros [|i] ?; simplify_eq/=; auto.
  by rewrite Permutation_swap, <-(IH i).
Qed.
(* stdpp/list_relations.v *)
Lemma elem_of_Permutation l x : x ∈ l ↔ ∃ k, l ≡ₚ x :: k.
Proof.
  split.
  - intros [i ?]%list_elem_of_lookup. eexists. by apply delete_Permutation.
  - intros [k ->]. by left.
Qed.
(* stdpp/list_relations.v *)
(* Swapping the values at positions [i1] and [i2] produces a permutation
of the original list [l]. *)
Lemma Permutation_insert_swap l i1 i2 x1 x2 :
  l !! i1 = Some x1 →
  l !! i2 = Some x2 →
  <[i2:=x1]> (<[i1:=x2]> l) ≡ₚ l.
Proof.
  intros Hi1 Hi2. destruct (decide (i1 = i2)); simplify_eq.
  { by rewrite list_insert_insert_eq, list_insert_id. }
  apply list_elem_of_split_length in Hi1 as (l1 & l2 & -> & ->).
  rewrite insert_app_r_alt, Nat.sub_diag by lia; simpl.
  apply lookup_app_Some in Hi2 as [Hi2|[? Hi2]].
  - rewrite insert_app_l by eauto using lookup_lt_Some.
    apply list_elem_of_split_length in Hi2 as (l1' & l2' & -> & ->).
    rewrite insert_app_r_alt, Nat.sub_diag by lia; simpl.
    rewrite <-!Permutation_middle; simpl. by rewrite Permutation_swap.
  - rewrite insert_app_r_alt by lia. f_equiv.
    destruct i2 as [|i2]; simplify_eq/=; [done|].
    rewrite Nat.sub_succ_l in Hi2 |- * by lia; simpl in *.
    apply list_elem_of_split_length in Hi2 as (l1' & l2' & -> & ->).
    rewrite insert_app_r_alt, Nat.sub_diag by lia; simpl.
    rewrite <-!Permutation_middle; simpl. by rewrite Permutation_swap.
Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_cons_inv_r l k x :
  k ≡ₚ x :: l → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
Proof.
  intros Hk. assert (∃ i, k !! i = Some x) as [i Hi].
  { apply list_elem_of_lookup. rewrite Hk, elem_of_cons; auto. }
  exists (take i k), (drop (S i) k). split.
  - by rewrite take_drop_middle.
  - rewrite <-delete_take_drop. apply (inj (x ::.)).
    by rewrite <-Hk, <-(delete_Permutation k) by done.
Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_cons_inv_l l k x :
  x :: l ≡ₚ k → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
Proof. by intros ?%(symmetry_iff (≡ₚ))%Permutation_cons_inv_r. Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_cross_split (la lb lc ld : list A) :
  la ++ lb ≡ₚ lc ++ ld →
  ∃ lac lad lbc lbd,
    lac ++ lad ≡ₚ la ∧ lbc ++ lbd ≡ₚ lb ∧ lac ++ lbc ≡ₚ lc ∧ lad ++ lbd ≡ₚ ld.
Proof.
  revert lc ld.
  induction la as [|x la IH]; simpl; intros lc ld Hperm.
  { exists [], [], lc, ld. by rewrite !(right_id_L [] (++)). }
  assert (x ∈ lc ++ ld)
    as [[lc' Hlc]%elem_of_Permutation|[ld' Hld]%elem_of_Permutation]%elem_of_app.
  { rewrite <-Hperm, elem_of_cons. auto. }
  - rewrite Hlc in Hperm. simpl in Hperm. apply (inj (x ::.)) in Hperm.
    apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
    exists (x :: lac), lad, lbc, lbd; simpl. by rewrite Ha, Hb, Hc, Hd.
  - rewrite Hld, <-Permutation_middle in Hperm. apply (inj (x ::.)) in Hperm.
    apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
    exists lac, (x :: lad), lbc, lbd; simpl.
    by rewrite <-Permutation_middle, Ha, Hb, Hc, Hd.
Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_inj l1 l2 :
  Permutation l1 l2 ↔
    length l1 = length l2 ∧
    ∃ f : nat → nat, Inj (=) (=) f ∧ ∀ i, l1 !! i = l2 !! f i.
Proof.
  split.
  - intros Hl; split; [by apply Permutation_length|].
    induction Hl as [|x l1 l2 _ [f [??]]|x y l|l1 l2 l3 _ [f [? Hf]] _ [g [? Hg]]].
    + exists id; split; [apply _|done].
    + exists (λ i, match i with 0 => 0 | S i => S (f i) end); split.
      * by intros [|i] [|j] ?; simplify_eq/=.
      * intros [|i]; simpl; auto.
    + exists (λ i, match i with 0 => 1 | 1 => 0 | _ => i end); split.
      * intros [|[|i]] [|[|j]]; congruence.
      * by intros [|[|i]].
    + exists (g ∘ f); split; [apply _|]. intros i; simpl. by rewrite <-Hg, <-Hf.
  - intros (Hlen & f & Hf & Hl). revert l2 f Hlen Hf Hl.
    induction l1 as [|x l1 IH]; intros l2 f Hlen Hf Hl; [by destruct l2|].
    rewrite (delete_Permutation l2 (f 0) x) by (by rewrite <-Hl).
    pose (g n := let m := f (S n) in if lt_eq_lt_dec m (f 0) then m else m - 1).
    apply Permutation_skip, (IH _ g).
    + rewrite length_delete by (rewrite <-Hl; eauto); simpl in *; lia.
    + unfold g. intros i j Hg.
      repeat destruct (lt_eq_lt_dec _ _) as [[?|?]|?]; simplify_eq/=; try lia.
      apply (inj S), (inj f); lia.
    + intros i. unfold g. destruct (lt_eq_lt_dec _ _) as [[?|?]|?].
      * by rewrite list_lookup_delete_lt, <-Hl.
      * simplify_eq.
      * rewrite list_lookup_delete_ge, <-Nat.sub_succ_l by lia; simpl.
        by rewrite Nat.sub_0_r, <-Hl.
Qed.
(* stdpp/list_relations.v *)
Instance filter_Permutation (P : A → Prop) `{∀ x, Decision (P x)} :
  Proper ((≡ₚ) ==> (≡ₚ)) (filter P).
Proof.
  induction 1; rewrite ?filter_cons;
    repeat (simpl; repeat case_decide); by econstructor.
Qed.
(* stdpp/list_relations.v *)
Lemma filter_app_complement l : filter P l ++ filter (λ x, ¬P x) l ≡ₚ l.
Proof.
    induction l as [|x l IH]; simpl; [done|]. case_decide.
    - rewrite decide_False by naive_solver. simpl. by rewrite IH.
    - rewrite decide_True by done. by rewrite <-Permutation_middle, IH.
  Qed.
(* stdpp/list_relations.v *)
(* ** Properties of the [prefix] and [suffix] predicates *)
Instance : PartialOrder (@prefix A).
Proof.
  split; [split|].
  - intros ?. eexists []. by rewrite (right_id_L [] (++)).
  - intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (assoc_L (++)).
  - intros l1 l2 [k1 ?] [[|x2 k2] ->]; [|discriminate_list].
    by rewrite (right_id_L _ _).
Qed.
(* stdpp/list_relations.v *)
Lemma prefix_nil l : [] `prefix_of` l.
Proof. by exists l. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_nil_inv l : l `prefix_of` [] → l = [].
Proof. intros [k ?]. by destruct l. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_nil_not x l : ¬x :: l `prefix_of` [].
Proof. by intros [k ?]. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_cons x l1 l2 : l1 `prefix_of` l2 → x :: l1 `prefix_of` x :: l2.
Proof. intros [k ->]. by exists k. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_cons_alt x y l1 l2 :
  x = y → l1 `prefix_of` l2 → x :: l1 `prefix_of` y :: l2.
Proof. intros ->. apply prefix_cons. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_cons_inv_1 x y l1 l2 : x :: l1 `prefix_of` y :: l2 → x = y.
Proof. by intros [k ?]; simplify_eq/=. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_cons_inv_2 x y l1 l2 :
  x :: l1 `prefix_of` y :: l2 → l1 `prefix_of` l2.
Proof. intros [k ?]; simplify_eq/=. by exists k. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_app k l1 l2 : l1 `prefix_of` l2 → k ++ l1 `prefix_of` k ++ l2.
Proof. intros [k' ->]. exists k'. by rewrite (assoc_L (++)). Qed.
(* stdpp/list_relations.v *)
Lemma prefix_app_alt k1 k2 l1 l2 :
  k1 = k2 → l1 `prefix_of` l2 → k1 ++ l1 `prefix_of` k2 ++ l2.
Proof. intros ->. apply prefix_app. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_app_inv k l1 l2 :
  k ++ l1 `prefix_of` k ++ l2 → l1 `prefix_of` l2.
Proof.
  intros [k' E]. exists k'. rewrite <-(assoc_L (++)) in E. by simplify_list_eq.
Qed.
(* stdpp/list_relations.v *)
Lemma prefix_app_l l1 l2 l3 : l1 ++ l3 `prefix_of` l2 → l1 `prefix_of` l2.
Proof. intros [k ->]. exists (l3 ++ k). by rewrite (assoc_L (++)). Qed.
(* stdpp/list_relations.v *)
Lemma prefix_app_r l1 l2 l3 : l1 `prefix_of` l2 → l1 `prefix_of` l2 ++ l3.
Proof. intros [k ->]. exists (k ++ l3). by rewrite (assoc_L (++)). Qed.
(* stdpp/list_relations.v *)
Lemma prefix_take l n : take n l `prefix_of` l.
Proof. rewrite <-(take_drop n l) at 2. apply prefix_app_r. done. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_lookup_lt l1 l2 i :
  i < length l1 → l1 `prefix_of` l2 → l1 !! i = l2 !! i.
Proof. intros ? [? ->]. by rewrite lookup_app_l. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_lookup_Some l1 l2 i x :
  l1 !! i = Some x → l1 `prefix_of` l2 → l2 !! i = Some x.
Proof. intros ? [k ->]. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite length_app. lia. Qed.
(* stdpp/list_relations.v *)
Lemma prefix_snoc_not l x : ¬l ++ [x] `prefix_of` l.
Proof. intros [??]. discriminate_list. Qed.
(* stdpp/list_relations.v *)
Lemma elem_of_prefix l1 l2 x :
  x ∈ l1 → l1 `prefix_of` l2 → x ∈ l2.
Proof. intros Hin [l' ->]. apply elem_of_app. by left. Qed.
(* stdpp/list_relations.v *)
(* [prefix] is not a total order, but [l1] and [l2] are always comparable if
  they are both prefixes of some [l3]. *)
Lemma prefix_weak_total l1 l2 l3 :
  l1 `prefix_of` l3 → l2 `prefix_of` l3 → l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
Proof.
  intros [k1 H1] [k2 H2]. rewrite H2 in H1.
  apply app_eq_inv in H1 as [(k&?&?)|(k&?&?)]; [left|right]; exists k; eauto.
Qed.
(* stdpp/list_relations.v *)
Instance : PartialOrder (@suffix A).
Proof.
  split; [split|].
  - intros ?. by eexists [].
  - intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
  - intros l1 l2 [k1 ?] [[|x2 k2] ->]; [done|discriminate_list].
Qed.
(* stdpp/list_relations.v *)
Instance prefix_dec `{!EqDecision A} : RelDecision prefix
:=
  fix go l1 l2 :=
  match l1, l2  with
  | [], _ => left (prefix_nil _)
  | _, [] => right (prefix_nil_not _ _)
  | x :: l1, y :: l2 =>
    match decide_rel (=) x y with
    | left Hxy =>
      match go l1 l2 with
      | left Hl1l2 => left (prefix_cons_alt _ _ _ _ Hxy Hl1l2)
      | right Hl1l2 => right (Hl1l2 ∘ prefix_cons_inv_2 _ _ _ _)
      end
    | right Hxy => right (Hxy ∘ prefix_cons_inv_1 _ _ _ _)
    end
  end.
(* stdpp/list_relations.v *)
Lemma prefix_not_elem_of_app_cons_inv x y l1 l2 k1 k2 :
  x ∉ k1 → y ∉ l1 →
  (l1 ++ x :: l2) `prefix_of` (k1 ++ y :: k2) →
  l1 = k1 ∧ x = y ∧ l2 `prefix_of` k2.
Proof.
  intros Hin1 Hin2 [k Hle]. rewrite <-(assoc_L (++)) in Hle.
  apply not_elem_of_app_cons_inv_l in Hle; [|done..]. unfold prefix. naive_solver.
Qed.
(* stdpp/list_relations.v *)
Lemma prefix_length_eq l1 l2 :
  l1 `prefix_of` l2 → length l2 ≤ length l1 → l1 = l2.
Proof.
  intros Hprefix Hlen. assert (length l1 = length l2).
  { apply prefix_length in Hprefix. lia. }
  eapply list_eq_same_length with (length l1); [done..|].
  intros i x y _ ??. assert (l2 !! i = Some x) by eauto using prefix_lookup_Some.
  congruence.
Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_fst l1 l2 :
    l1 = (max_prefix l1 l2).2 ++ (max_prefix l1 l2).1.1.
Proof.
    revert l2. induction l1; intros [|??]; simpl;
      repeat case_decide; f_equal/=; auto.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_fst_alt l1 l2 k1 k2 k3 :
    max_prefix l1 l2 = (k1, k2, k3) → l1 = k3 ++ k1.
Proof.
    intros. pose proof (max_prefix_fst l1 l2).
    by destruct (max_prefix l1 l2) as [[]?]; simplify_eq.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_fst_prefix l1 l2 : (max_prefix l1 l2).2 `prefix_of` l1.
Proof. eexists. apply max_prefix_fst. Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_fst_prefix_alt l1 l2 k1 k2 k3 :
    max_prefix l1 l2 = (k1, k2, k3) → k3 `prefix_of` l1.
Proof. eexists. eauto using max_prefix_fst_alt. Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_snd l1 l2 :
    l2 = (max_prefix l1 l2).2 ++ (max_prefix l1 l2).1.2.
Proof.
    revert l2. induction l1; intros [|??]; simpl;
      repeat case_decide; f_equal/=; auto.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_snd_alt l1 l2 k1 k2 k3 :
    max_prefix l1 l2 = (k1, k2, k3) → l2 = k3 ++ k2.
Proof.
    intro. pose proof (max_prefix_snd l1 l2).
    by destruct (max_prefix l1 l2) as [[]?]; simplify_eq.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_snd_prefix l1 l2 : (max_prefix l1 l2).2 `prefix_of` l2.
Proof. eexists. apply max_prefix_snd. Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_snd_prefix_alt l1 l2 k1 k2 k3 :
    max_prefix l1 l2 = (k1,k2,k3) → k3 `prefix_of` l2.
Proof. eexists. eauto using max_prefix_snd_alt. Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_max l1 l2 k :
    k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` (max_prefix l1 l2).2.
Proof.
    intros [l1' ->] [l2' ->]. by induction k; simpl; repeat case_decide;
      simpl; auto using prefix_nil, prefix_cons.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_max_alt l1 l2 k1 k2 k3 k :
    max_prefix l1 l2 = (k1,k2,k3) →
    k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` k3.
Proof.
    intro. pose proof (max_prefix_max l1 l2 k).
    by destruct (max_prefix l1 l2) as [[]?]; simplify_eq.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_prefix_max_snoc l1 l2 k1 k2 k3 x1 x2 :
    max_prefix l1 l2 = (x1 :: k1, x2 :: k2, k3) → x1 ≠ x2.
Proof.
    intros Hl ->. destruct (prefix_snoc_not k3 x2).
    eapply max_prefix_max_alt; eauto.
    - rewrite (max_prefix_fst_alt _ _ _ _ _ Hl).
      apply prefix_app, prefix_cons, prefix_nil.
    - rewrite (max_prefix_snd_alt _ _ _ _ _ Hl).
      apply prefix_app, prefix_cons, prefix_nil.
  Qed.
(* stdpp/list_relations.v *)
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.
(* stdpp/list_relations.v *)
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.
(* stdpp/list_relations.v *)
Lemma suffix_nil l : [] `suffix_of` l.
Proof. exists l. by rewrite (right_id_L [] (++)). Qed.
(* stdpp/list_relations.v *)
Lemma suffix_nil_inv l : l `suffix_of` [] → l = [].
Proof. by intros [[|?] ?]; simplify_list_eq. Qed.
(* stdpp/list_relations.v *)
Lemma suffix_cons_nil_inv x l : ¬x :: l `suffix_of` [].
Proof. by intros [[] ?]. Qed.
(* stdpp/list_relations.v *)
Lemma suffix_snoc l1 l2 x :
  l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [x].
Proof. intros [k ->]. exists k. by rewrite (assoc_L (++)). Qed.
(* stdpp/list_relations.v *)
Lemma suffix_snoc_alt x y l1 l2 :
  x = y → l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [y].
Proof. intros ->. apply suffix_snoc. Qed.
(* stdpp/list_relations.v *)
Lemma suffix_app l1 l2 k : l1 `suffix_of` l2 → l1 ++ k `suffix_of` l2 ++ k.
Proof. intros [k' ->]. exists k'. by rewrite (assoc_L (++)). Qed.
(* stdpp/list_relations.v *)
Lemma suffix_app_alt l1 l2 k1 k2 :
  k1 = k2 → l1 `suffix_of` l2 → l1 ++ k1 `suffix_of` l2 ++ k2.
Proof. intros ->. apply suffix_app. Qed.
(* stdpp/list_relations.v *)
Lemma suffix_snoc_inv_1 x y l1 l2 :
  l1 ++ [x] `suffix_of` l2 ++ [y] → x = y.
Proof. intros [k' E]. rewrite (assoc_L (++)) in E. by simplify_list_eq. Qed.
(* stdpp/list_relations.v *)
Lemma suffix_snoc_inv_2 x y l1 l2 :
  l1 ++ [x] `suffix_of` l2 ++ [y] → l1 `suffix_of` l2.
Proof.
  intros [k' E]. exists k'. rewrite (assoc_L (++)) in E. by simplify_list_eq.
Qed.
(* stdpp/list_relations.v *)
Lemma suffix_app_inv l1 l2 k :
  l1 ++ k `suffix_of` l2 ++ k → l1 `suffix_of` l2.
Proof.
  intros [k' E]. exists k'. rewrite (assoc_L (++)) in E. by simplify_list_eq.
Qed.
(* stdpp/list_relations.v *)
Lemma suffix_cons_l l1 l2 x : x :: l1 `suffix_of` l2 → l1 `suffix_of` l2.
Proof. intros [k ->]. exists (k ++ [x]). by rewrite <-(assoc_L (++)). Qed.
(* stdpp/list_relations.v *)
Lemma suffix_app_l l1 l2 l3 : l3 ++ l1 `suffix_of` l2 → l1 `suffix_of` l2.
Proof. intros [k ->]. exists (k ++ l3). by rewrite <-(assoc_L (++)). Qed.
(* stdpp/list_relations.v *)
Lemma suffix_cons_r l1 l2 x : l1 `suffix_of` l2 → l1 `suffix_of` x :: l2.
Proof. intros [k ->]. by exists (x :: k). Qed.
(* stdpp/list_relations.v *)
Lemma suffix_app_r l1 l2 l3 : l1 `suffix_of` l2 → l1 `suffix_of` l3 ++ l2.
Proof. intros [k ->]. exists (l3 ++ k). by rewrite (assoc_L (++)). Qed.
(* stdpp/list_relations.v *)
Lemma suffix_drop l n : drop n l `suffix_of` l.
Proof. rewrite <-(take_drop n l) at 2. apply suffix_app_r. done. Qed.
(* stdpp/list_relations.v *)
Lemma suffix_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_eq/=. by apply suffix_app_r.
Qed.
(* stdpp/list_relations.v *)
Lemma suffix_lookup_lt l1 l2 i :
  i < length l1 →
  l1 `suffix_of` l2 →
  l1 !! i = l2 !! (i + (length l2 - length l1)).
Proof.
  intros Hi [k ->]. rewrite length_app, lookup_app_r by lia. f_equal; lia.
Qed.
(* stdpp/list_relations.v *)
Lemma suffix_lookup_Some l1 l2 i x :
  l1 !! i = Some x →
  l1 `suffix_of` l2 →
  l2 !! (i + (length l2 - length l1)) = Some x.
Proof. intros. by rewrite <-suffix_lookup_lt by eauto using lookup_lt_Some. Qed.
(* stdpp/list_relations.v *)
Lemma suffix_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite length_app. lia. Qed.
(* stdpp/list_relations.v *)
Lemma suffix_cons_not x l : ¬x :: l `suffix_of` l.
Proof. intros [??]. discriminate_list. Qed.
(* stdpp/list_relations.v *)
Lemma elem_of_suffix l1 l2 x :
  x ∈ l1 → l1 `suffix_of` l2 → x ∈ l2.
Proof. intros Hin [l' ->]. apply elem_of_app. by right. Qed.
(* stdpp/list_relations.v *)
(* [suffix] is not a total order, but [l1] and [l2] are always comparable if
  they are both suffixes of some [l3]. *)
Lemma suffix_weak_total l1 l2 l3 :
  l1 `suffix_of` l3 → l2 `suffix_of` l3 → l1 `suffix_of` l2 ∨ l2 `suffix_of` l1.
Proof.
  intros [k1 Hl1] [k2 Hl2]. rewrite Hl1 in Hl2.
  apply app_eq_inv in Hl2 as [(k&?&?)|(k&?&?)]; [left|right]; exists k; eauto.
Qed.
(* stdpp/list_relations.v *)
Instance suffix_dec `{!EqDecision A} : RelDecision (@suffix A).
Proof.
  refine (λ l1 l2, cast_if (decide_rel prefix (reverse l1) (reverse l2)));
   abstract (by rewrite suffix_prefix_reverse).
Defined.
(* stdpp/list_relations.v *)
Lemma suffix_not_elem_of_app_cons_inv x y l1 l2 k1 k2 :
  x ∉ k2 → y ∉ l2 →
  (l1 ++ x :: l2) `suffix_of` (k1 ++ y :: k2) →
  l1 `suffix_of` k1 ∧ x = y ∧ l2 = k2.
Proof.
  intros Hin1 Hin2 [k Hle]. rewrite (assoc_L (++)) in Hle.
  apply not_elem_of_app_cons_inv_r in Hle; [|done..]. unfold suffix. naive_solver.
Qed.
(* stdpp/list_relations.v *)
Lemma suffix_length_eq l1 l2 :
  l1 `suffix_of` l2 → length l2 ≤ length l1 → l1 = l2.
Proof.
  intros. apply (inj reverse), prefix_length_eq.
  - by apply suffix_prefix_reverse.
  - by rewrite !length_reverse.
Qed.
(* stdpp/list_relations.v *)
Lemma max_suffix_fst l1 l2 :
    l1 = (max_suffix l1 l2).1.1 ++ (max_suffix l1 l2).2.
Proof.
    rewrite <-(reverse_involutive l1) at 1.
    rewrite (max_prefix_fst (reverse l1) (reverse l2)). unfold max_suffix.
    destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
    by rewrite reverse_app.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_suffix_fst_alt l1 l2 k1 k2 k3 :
    max_suffix l1 l2 = (k1, k2, k3) → l1 = k1 ++ k3.
Proof.
    intro. pose proof (max_suffix_fst l1 l2).
    by destruct (max_suffix l1 l2) as [[]?]; simplify_eq.
  Qed.