From stdpp Require Import prelude ssreflect gmultiset.
From stdpp Require Import options.

Lemma prefix_of_fmap {A B} (f : A → B) (xs xs' : list A) :
  xs `prefix_of` xs' →
  f <$> xs `prefix_of` f <$> xs'.
Proof. intros [ys ->]. exists (f <$> ys). apply fmap_app. Qed.

Lemma prefix_sublist {A} (l1 l2 : list A) : l1 `prefix_of` l2 → l1 `sublist_of` l2.
Proof. intros [k ->]. by apply sublist_inserts_r. Qed.

Lemma prefix_submseteq {A} (l1 l2 : list A) : l1 `prefix_of` l2 → l1 ⊆+ l2.
Proof. intros [k ->]. by apply submseteq_inserts_r. Qed.

Lemma take_less_prefix {A} n m (xs : list A) : n ≤ m → take n xs `prefix_of` take m xs.
Proof.
  intros Hnm.
  replace n with (n `min` m); last lia.
  rewrite -take_take.
  apply prefix_take.
Qed.

Lemma take_app_prefix {A} n (xs ys : list A) : take n xs `prefix_of` take n (xs ++ ys).
Proof. unfold prefix. exists (take (n - length xs) ys). apply firstn_app. Qed.

Lemma Forall_prefix {A} (xs xs' : list A) Φ : xs `prefix_of` xs' → Forall Φ xs' → Forall Φ xs.
Proof. by intros [? ->] [? _]%Forall_app. Qed.

Lemma drop_cons_inv {A} n x (xs xs' : list A) :
  drop n xs = x :: xs' → xs !! n = Some x ∧ drop (S n) xs = xs'.
Proof.
  intros Hxs. split.
  - by rewrite -[n]Nat.add_0_r -lookup_drop Hxs.
  - by rewrite -Nat.add_1_r -drop_drop Hxs.
Qed.

Lemma list_to_set_disj_size `{Countable A} (l : list A) :
  size (list_to_set_disj l : gmultiset A) = length l.
Proof.
  induction l; first done.
  by rewrite /= gmultiset_size_disj_union IHl gmultiset_size_singleton.
Qed.

Lemma gmultiset_subseteq_size_eq `{Countable A, LeibnizEquiv A} (X Y : gmultiset A) :
  X ⊆ Y → size Y ≤ size X → X = Y.
Proof.
  revert Y. induction X using gmultiset_ind; intros Y HY Hsize.
  - rewrite gmultiset_size_empty in Hsize.
    apply symmetry, gmultiset_size_empty_inv. lia.
  - rewrite gmultiset_size_disj_union gmultiset_size_singleton in Hsize.
    assert (X ⊆ Y ∖ {[+ x +]}) as HXY%IHX; [multiset_solver..|].
    rewrite gmultiset_size_difference; last multiset_solver.
    rewrite gmultiset_size_singleton. lia.
Qed.

Lemma elements_list_to_set_disj_perm `{Countable A} (l : list A) : l ≡ₚ elements (list_to_set_disj l : gmultiset A).
Proof.
  induction l; first done.
  by rewrite list_to_set_disj_cons gmultiset_elements_disj_union gmultiset_elements_singleton -IHl.
Qed.