Lvc.Constr.CSetDisjoint

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

Set Implicit Arguments.

Definition disj {X} `{OrderedType X} (s t: set X)
  := ∀ x, x ∈ s → x ∈ t → False.

Instance disj_sym {X} `{OrderedType X} : Symmetric disj.
Proof.
  unfold Symmetric, disj; intros.
  cset_tac; intuition; eauto.
Qed.

Lemma disj_sym' X `{OrderedType X} s t
  : disj s t → disj t s.
Proof.
  symmetry; eauto.
Qed.

Hint Immediate disj_sym' : cset.

Instance disj_eq_eq_iff {X} `{OrderedType X}
: Proper (Equal ==> Equal ==> iff) disj.
Proof.
  unfold Proper, respectful, disj; intros.
  cset_tac; firstorder.
Qed.

Instance disj_subset_subset_flip_impl {X} `{OrderedType X}
: Proper (Subset ==> Subset ==> flip impl) disj.
Proof.
  unfold Proper, respectful, disj, flip, impl; intros.
  firstorder.
Qed.

Lemma disj_app {X} `{OrderedType X} (s t u: set X)
: disj s (t ∪ u) ↔ disj s t ∧ disj s u.
Proof.
  split; unfold disj; intros; cset_tac; intuition; eauto.
Qed.

Lemma disj_add {X} `{OrderedType X} (x:X) (s t: set X)
: disj s {x; t} ↔ x ∉ s ∧ disj s t.
Proof.
  split; unfold disj; intros; cset_tac; intuition; eauto.
Qed.

Lemma disj_empty {X} `{OrderedType X} (s: set X)
: disj s {}.
Proof.
  unfold disj; intros; cset_tac; intuition; eauto.
Qed.

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}.
Proof.
  intros. unfold disj. cset_tac; intuition.
Qed.

Lemma disj_1_incl X `{OrderedType X} D D' D''
: disj D D'
   → D'' ⊆ D
   → disj D'' D'.
Proof.
  intros. rewrite H1; eauto.
Qed.

Lemma disj_2_incl X `{OrderedType X} D D' D''
: disj D' D
   → D'' ⊆ D
   → disj D' D''.
Proof.
  intros. rewrite H1; eauto.
Qed.

Lemma disj_incl X `{OrderedType X} (D1 D1' D2 D2':set X)
  : disj D1' D2'
    → D1 ⊆ D1'
    → D2 ⊆ D2'
    → disj D1 D2.
Proof.
  intros.
  eapply disj_1_incl. eapply disj_2_incl; eauto.
  eauto.
Qed.

Hint Resolve disj_incl disj_1_incl disj_2_incl : cset.

Lemma in_disj_absurd X `{OrderedType X} (s t: set X) x
: x ∈ s → x ∈ t → disj s t → False.
Proof.
  unfold disj; cset_tac; intuition; eauto.
Qed.

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.

Lemma disj_minus_eq X `{OrderedType X} (s t:set X)
: disj s t
  → s \ t [=] s.
Proof.
  unfold disj; cset_tac; intuition; eauto.
Qed.

Lemma disj_not_in X `{OrderedType X} x s
: disj {x} s
  → x ∉ s.
Proof.
  unfold disj; cset_tac.
Qed.

Lemma disj_eq_minus X `{OrderedType X} (s t u: set X)
: s [=] t
  → disj t u
  → s [=] t \ u.
Proof.
  unfold disj.
  cset_tac.
Qed.

Lemma disj_struct_1 X `{OrderedType X} s t u
: s [=] t
  → disj s u → disj t u.
Proof.
  intros. rewrite <- H0; eauto.
Qed.

Lemma disj_struct_1_r X `{OrderedType X} s t u
: s [=] t
  → disj t u → disj s u.
Proof.
  intros. rewrite H0; eauto.
Qed.

Lemma disj_struct_2 X `{OrderedType X} s t u
: s [=] t
  → disj u s → disj u t.
Proof.
  intros. rewrite <- H0; eauto.
Qed.

Lemma disj_struct_2_r X `{OrderedType X} s t u
: s [=] t
  → disj u t → disj u s.
Proof.
  intros. rewrite H0; eauto.
Qed.

Lemma disj_intersection X `{OrderedType X} s t
  : disj s t ↔ s ∩ t [=] ∅.
Proof.
  cset_tac.
Qed.

Lemma not_incl_minus X `{OrderedType X} (s t u: set X)
: s ⊆ t
  → disj s u
  → s ⊆ t \ u.
Proof.
  cset_tac; intuition.
Qed.

Lemma disj_minus X `{OrderedType X} s t u
  : (s ∩ t) ⊆ u
    → disj s (t \ u).
Proof.
  intros. hnf; intros. specialize (H0 x).
  cset_tac.
Qed.

Lemma disj_union_left X `{OrderedType X} s t u
  : disj s t → disj s u → disj (t ∪ u) s.
Proof.
  intros. symmetry. eapply disj_app; eauto.
Qed.

Lemma disj_union_right X `{OrderedType X} s t u
  : disj s t → disj s u → disj s (t ∪ u).
Proof.
  intros. eapply disj_app; eauto.
Qed.

Hint Resolve disj_union_left disj_union_right : cset.

Lemma disj_add_swap X `{OrderedType X} x D Ds :
  x ∉ D
  → disj {x; D} Ds
  → disj D {x; Ds}.
Proof.
  unfold disj. cset_tac.
Qed.

Hint Resolve disj_add_swap : cset.

Lemma minus_incl_disj_eq X `{OrderedType X} s t u
  : s [=] t ∪ u
    → disj t u
    → s \ t ⊆ u.
Proof.
  intros A B. rewrite A; cset_tac.
Qed.

Hint Resolve minus_incl_disj_eq : cset.

Hint Resolve disj_not_in disj_struct_1
     disj_struct_1_r disj_struct_2 disj_struct_2_r : cset.

Hint Extern 0 ⇒
match goal with
| [ H : disj ?s ?t |- disj ?s' ?t ] ⇒ eapply disj_1_incl
| [ H : disj ?s ?t |- disj ?s' (?t \ _) ] ⇒ eapply (disj_2_incl H); eapply incl_minus
| [ H : disj ({ _ ; ?s} ∪ _) _ |- disj ?s ?t ] ⇒
  is_evar t; eapply (disj_1_incl H); eapply incl_union_left, incl_add_right, reflexivity
| [ H : disj ?s ?t |- disj ?s (_ ∪ ?t ∪ _) ] ⇒
  eapply (disj_2_incl H); eapply incl_union_left; eapply incl_right
end : cset.

Smpl Add 40 match goal with
         | [ H : disj _ _ |- _ ] ⇒ hnf in H
         | [ |- disj _ _ ] ⇒ hnf
         end : cset.