Library zoo.common.gmultiset

From stdpp Require Export
  gmultiset.

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

Section basic.
  Context `{Countable A}.

  Implicit Types x y : A.
  Implicit Types 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 = ∅.
End basic.

Section size.
  Context `{Countable A}.

  Implicit Types x y : A.
  Implicit Types 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 Types x y : A.
  Implicit Types X Y : gmultiset A.
  Implicit Types 𝑋 𝑌 : 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 Types x y : A.
  Implicit Types 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 Types x y : A.
  Implicit Types X Y : gmultiset A.
  Implicit Types 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.