Lvc.Constr.SetOperations

Require Export Setoid Coq.Classes.Morphisms.
Require Export Sets SetInterface SetConstructs SetProperties.
Require Import EqDec Get CSet Map AllInRel.

Lemma fold_union_incl X `{OrderedType.OrderedType X} s u (x:X) y
  : x ∈ y
    → y ∈ s
    → x ∈ fold union s u.

Lemma transpose_union X `{OrderedType X}
      : transpose Equal union.

Lemma transpose_union_subset X `{OrderedType X}
      : transpose Subset union.

Lemma fold_union_incl_start X `{OrderedType.OrderedType X} s u (x:X)
  : x ∈ u
    → x ∈ fold union s u.

Lemma map_app X `{OrderedType X} Y `{OrderedType Y} (f:X→Y)
      `{Proper _ (_eq ==> _eq) f} s t
: map f (s ∪ t) [=] map f s ∪ map f t.

Lemma map_add X `{OrderedType X} Y `{OrderedType Y} (f:X→Y)
      `{Proper _ (_eq ==> _eq) f} x t
: map f ({x; t}) [=] {f x; map f t}.

Lemma map_empty X `{OrderedType X} Y `{OrderedType Y} (f:X→Y)
      `{Proper _ (_eq ==> _eq) f}
: map f ∅ [=] ∅.

Instance map_Proper X `{OrderedType X} Y `{OrderedType Y}
  : Proper (@fpeq X Y _eq _ _ ==> _eq ==> _eq) map.

Instance fold_union_Proper X `{OrderedType X}
  : Proper (_eq ==> _eq ==> _eq) (fold union).

Lemma list_union_start_swap X `{OrderedType X} (L : list (set X)) s
: fold_left union L s[=]s ++ list_union L.

Lemma list_union_app X `{OrderedType X} (L L´ : list (set X)) s
: fold_left union (L ++ L´) s [=] fold_left union L s ∪ list_union L´.

Lemma fold_union_app X `{OrderedType X} Gamma Γ´
: fold union (Gamma ∪ Γ´) {}[=]
  fold union Gamma {} ∪ fold union Γ´ {}.

Lemma map_single {X} `{OrderedType X} Y `{OrderedType Y} (f:X→Y)
      `{Proper _ (_eq ==> _eq) f} x
      : map f {{x}} [=] {{f x}}.

Lemma fold_single {X} `{OrderedType X} Y `{Equivalence Y} (f:X→Y→Y)
      `{Proper _ (_eq ==> R ==> R) f} (x:X) (s:Y)
      : transpose R f
        → R (fold f {{x}} s) (f x s).

Lemma incl_fold_union X `{OrderedType X} s t x
  : x \In fold union s t
     → (∃ s´, s´ ∈ s ∧ x ∈ s´) ∨ x ∈ t.

Instance fold_union_morphism X `{OrderedType X}
: Proper (Subset ==> Subset ==> Subset) (fold union).

Lemma list_union_minus_dist X `{OrderedType X} D´´ s s´ L
  :
    s \ D´´ [=] s´
 → fold_left union L s \ D´´
[=] fold_left union (List.map (fun s ⇒ s \ D´´) L) s´.

Instance fold_left_union_morphism X `{OrderedType X}:
  Proper (PIR2 Equal ==> Equal ==> Equal) (fold_left union).

Instance fold_left_subset_morphism X `{OrderedType X}:
  Proper (PIR2 Subset ==> Subset ==> Subset) (fold_left union).

Lemma lookup_set_list_union
      X `{OrderedType X } Y `{OrderedType Y} (ϱ:X→Y) `{Proper _ (_eq ==> _eq) ϱ} l s s´
: lookup_set ϱ s[=]s´ →
  lookup_set ϱ (fold_left union l s)
             [=] fold_left union (List.map (lookup_set ϱ) l) s´.

Lemma list_union_disjunct {X} `{OrderedType X} Y D
: (∀ (n : nat) (e : set X), get Y n e → e ∩ D[=]{})
   ↔ disj (list_union Y) D.

Lemma list_union_cons X `{OrderedType X} s sl
: list_union sl ⊆ list_union (s :: sl).

Hint Resolve list_union_cons : cset.