Lvc.Constr.CSetCases

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

Section theorems.
  Variable X : Type.
  Context `{OrderedType X}.

  Lemma in_add_case s (x y:X)
    : y ∈ {{x}} ∪ s → x===y ∨ (x =/= y ∧ y ∈ s).

  Lemma in_in_neq s (x y:X)
    : x ∈ s → ¬y ∈ s → x =/= y.

  Lemma minus_inane s (x:X)
    : x ∉ s
    → s ≅ (s\{{x}}).

  Lemma incl_set_decomp (s t:set X)
    : s ⊆ t → t ≅ s ∪ (t \ s).

  Lemma incl_union_minus (s t:set X)
    : s ⊆ (t ∪ (s \ t)).

  Lemma union_minus s (x:X)
    : x ∉ s → s ≅ ({{x}} ∪ s) \ {{x}}.

  Lemma set_fact_1 s t (x:X)
    : x ∉ t
    → {{x}} ∪ (s \ ({{x}} ∪ t)) ≅ {{x}} ∪ s \ t.

  Lemma incl_not_in (x:X) s t
    : x ∉ s → s\{{x}} ⊆ t → s ⊆ t.


  Lemma minus_incl_special (c c´ d : set X)
    : c ⊆ c´
    → c ∪ (c´ \ (c \ d)) ≅ c´.

  Lemma minus_incl_meet_special (c c´ d : set X)
    : d ⊆ c
    → c ⊆ c´
    → c ∩ (c´ \ (c \ d)) ≅ d.

  Lemma minus_minus_id (s t: set X)
    : s ⊆ t
    → s ≅ t \ (t \ s).
End theorems.