Lvc.Constr.CSetGet

Require Export Setoid Coq.Classes.Morphisms.
Require Export Sets SetInterface SetConstructs SetProperties.
Require Import EqDec Get CSetNotation CSetTac CSetComputable.

Definition list_union X `{OrderedType X} (L:list (set X)) :=
  fold_left union L ∅.


Lemma list_union_start {X} `{OrderedType X} (s: set X) L t
: s ⊆ t
  → s ⊆ fold_left union L t.

Lemma list_union_incl {X} `{OrderedType X} (L:list (set X)) (s s´:set X)
  : (∀ n t, get L n t → t ⊆ s´)
   → s ⊆ s´
   → fold_left union L s ⊆ s´.

Lemma incl_list_union {X} `{OrderedType X} (s: set X) L n t u
: get L n t
  → s ⊆ t
  → s ⊆ fold_left union L u.

Lemma list_union_get {X} `{OrderedType X} L (x:X) u
: x ∈ fold_left union L u
  → { n : nat & { t : set X | get L n t ∧ x ∈ t} } + { x ∈ u }.

Lemma get_list_union_map X Y `{OrderedType Y} (f:X → set Y) L n x
: get L n x
  → f x [<=] list_union (List.map f L).

Lemma get_in_incl X `{OrderedType X} (L:list X) s
: (∀ n x, get L n x → x ∈ s)
  → of_list L ⊆ s.

Lemma get_in_of_list X `{OrderedType X} L n x
    : get L n x
      → x ∈ of_list L.