Lvc.Constr.CSetDisjoint

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

Set Implicit Arguments.

Definition disj {X} `{OrderedType X} (s t: set X)
  := s ∩ t [=] ∅.

Instance disj_sym {X} `{OrderedType X} : Symmetric disj.

Instance disj_eq_eq_iff {X} `{OrderedType X}
: Proper (Equal ==> Equal ==> iff) disj.

Instance disj_subset_subset_flip_impl {X} `{OrderedType X}
: Proper (Subset ==> Subset ==> flip impl) disj.

Lemma disj_app {X} `{OrderedType X} (s t u: set X)
: disj s (t ++ u) ↔ disj s t ∧ disj s u.

Lemma disj_add {X} `{OrderedType X} (x:X) (s t: set X)
: disj s {x; t} ↔ x ∉ s ∧ disj s t.

Lemma disj_empty {X} `{OrderedType X} (s: set X)
: disj s {}.

Hint Extern 20 (disj ?a ∅) ⇒ eapply disj_empty.

Hint Extern 20 (disj ∅ ?a) ⇒ eapply disj_sym; eapply disj_empty.

Lemma disj_singleton X `{OrderedType X} x D
: x ∉ D
   → disj D {x}.

Lemma disj_1_incl X `{OrderedType X} D D´ D´´
: disj D D´
   → D´´ ⊆ D
   → disj D´´ D´.

Lemma disj_2_incl X `{OrderedType X} D D´ D´´
: disj D´ D
   → D´´ ⊆ D
   → disj D´ D´´.

Lemma in_disj_absurd X `{OrderedType X} (s t: set X) x
: x ∈ s → x ∈ t → disj s t → False.

Hint Extern 10 ⇒
match goal with
  | [ H : disj ?s ?t, H´ : ?x ∈ ?s, H´´ : ?x ∈ ?t |- _ ] ⇒
    exfalso; eapply (in_disj_absurd H´ H´´ H)
end.