Library zoo.common.gmultiset

Require Export stdpp.gmultiset.

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.options.

Section basic.
  Context `{Countable A}.

  Implicit Type x y : A.
  Implicit Type X Y : gmultiset A.

  Lemma gmultiset ｰ empty ｰ elem_of X :
    X = ∅ ↔
      ∀ x,
      x ∉ X.

  Lemma gmultiset ｰ disj_union ｰ empty X1 X2 :
    X1 ⊎ X2 = ∅ ↔
      X1 = ∅ ∧
      X2 = ∅.
  Lemma gmultiset ｰ disj_union ｰ empty ｰ inv X1 X2 :
    X1 ⊎ X2 = ∅ →
      X1 = ∅ ∧
      X2 = ∅.

  Lemma elem_of ｰ gmultiset ｰ disj_union ｰ l x X1 X2 :
    x ∈ X1 →
    x ∈ X1 ⊎ X2.
  Lemma elem_of ｰ gmultiset ｰ disj_union ｰ r x X1 X2 :
    x ∈ X2 →
    x ∈ X1 ⊎ X2.
End basic.

Section size.
  Context `{Countable A}.

  Implicit Type x y : A.
  Implicit Type X Y : gmultiset A.

  Lemma gmultiset ｰ size ｰ singleton ｰ inv X x y :
    size X = 1 →
    x ∈ X →
    y ∈ X →
    x = y.
  Lemma gmultiset ｰ size ｰ1ｰ elem_of X :
    size X = 1 →
      ∃ x,
      X = {[+x +]}.

  Lemma gmultiset ｰ elem_of ｰ size ｰ non_empty x X :
    x ∈ X →
    size X ≠ 0.
End size.

Section map.
  Context `{Countable A}.
  Context `{Countable B}.
  Context (f : A → B).

  Implicit Type x y : A.
  Implicit Type X Y : gmultiset A.
  Implicit Type 𝑋 𝑌 : gmultiset B.

  Lemma gmultiset ｰ size ｰ map X :
    size (gmultiset_map f X) = size X.

  Lemma gmultiset_map ｰ empty ｰ inv X :
    gmultiset_map f X = ∅ →
    X = ∅.

  Lemma gmultiset_map ｰ singleton ｰ inv X 𝑥 :
    gmultiset_map f X = {[+𝑥 +]} →
      ∃ x,
      X = {[+x +]} ∧
      𝑥 = f x.

  Lemma gmultiset_map ｰ disj_union ｰ inv X 𝑋1 𝑋2 :
    gmultiset_map f X = 𝑋1 ⊎ 𝑋2 →
      ∃ X1 X2,
      X = X1 ⊎ X2 ∧
      𝑋1 = gmultiset_map f X1 ∧
      𝑋2 = gmultiset_map f X2.
  Lemma gmultiset_map ｰ disj_union ｰ singleton ｰ l ｰ inv X 𝑥 𝑋 :
    gmultiset_map f X = {[+𝑥 +]} ⊎ 𝑋 →
      ∃ x X',
      X = {[+x +]} ⊎ X' ∧
      𝑥 = f x ∧
      𝑋 = gmultiset_map f X'.
  Lemma gmultiset_map ｰ disj_union ｰ singleton ｰ r ｰ inv X 𝑥 𝑋 :
    gmultiset_map f X = 𝑋 ⊎ {[+𝑥 +]} →
      ∃ X' x,
      X = X' ⊎ {[+x +]} ∧
      𝑋 = gmultiset_map f X' ∧
      𝑥 = f x.
End map.

Section list_to_set_disj.
  Context `{Countable A}.

  Implicit Type x y : A.
  Implicit Type l : list A.

  Lemma list_to_set_disj ｰ empty l :
    list_to_set_disj l =@{gmultiset _} ∅ ↔
    l = [].

  Lemma list_to_set_disj ｰ snoc l x :
    list_to_set_disj (l ++ [x]) =@{gmultiset _} {[+x +]} ⊎ list_to_set_disj l.
End list_to_set_disj.

Section disj_union_list.
  Context `{Countable A}.

  Implicit Type x y : A.
  Implicit Type X Y : gmultiset A.
  Implicit Type Xs Ys : list $ gmultiset A.

  Lemma gmultiset ｰ disj_union_list ｰ empty Xs :
    ⋃+ Xs = ∅ ↔
      ∀ X,
      X ∈ Xs →
      X = ∅.
  Lemma gmultiset ｰ disj_union_list ｰ replicate ｰ empty n :
    ⋃+ replicate n ∅ =@{gmultiset A } ∅.

  Lemma gmultiset ｰ disj_union_list ｰ delete Xs i X :
    Xs !! i = Some X →
    ⋃+ (delete i Xs ) = ⋃+ Xs ∖ X.
  Lemma gmultiset ｰ disj_union_list ｰ delete' Xs i X :
    Xs !! i = Some X →
    ⋃+ Xs = X ⊎ ⋃+ (delete i Xs ).

  Lemma gmultiset ｰ disj_union_list ｰ insert Xs i X :
    is_Some (Xs !! i) →
    ⋃+ <[i := X ]> Xs = X ⊎ ⋃+ (delete i Xs ).
  Lemma gmultiset ｰ disj_union_list ｰ insert ｰ id Xs i X :
    Xs !! i = Some X →
    ⋃+ <[i := X ]> Xs = ⋃+ Xs.
  Lemma gmultiset ｰ disj_union_list ｰ insert ｰ disj_union ｰ l Xs i X1 X2 :
    Xs !! i = Some X2 →
    ⋃+ <[i := X1 ⊎ X2 ]> Xs = X1 ⊎ ⋃+ Xs.
  Lemma gmultiset ｰ disj_union_list ｰ insert ｰ disj_union ｰ r Xs i X1 X2 :
    Xs !! i = Some X1 →
    ⋃+ <[i := X1 ⊎ X2 ]> Xs = X2 ⊎ ⋃+ Xs.
End disj_union_list.