# Library LibFsetExt

Set Implicit Arguments.
Require Import LibTactics LibFset LibReflect LibList LibLogic.

Section Basic.
Variables A : Type.
Implicit Types E F: fset A.
Implicit Types x y : A.

Lemma in_and_notin: E x y,
x \in Ey \notin Ex y.
Proof.
introv H1 H2 H3. rewrite H3 in H1. false.
Qed.

Axiom fset_extens_iff : E F,
( x, x \in E = x \in F) E = F.

Lemma fset_neq: E F,
( x, x \in E x \notin E \n F) → E F.
Proof.
introv H. destruct H as (x & Hin & Hni). introv H.
lets K: fset_extens_iff E F. destruct K as (_ & H0). specializes H0 H x.
apply Hni. rewrite in_inter. split¬.
rewrite¬ <- H0.
Qed.

Lemma empty_dec: E,
E = \{} E \{}.
Proof.
intro. lets (l & Hl): (fset_finite E). cases l.
rewrite from_list_nil in Hl. left¬.
rewrite from_list_cons in Hl. right. rewrite Hl.
introv H. rewrite <- fset_extens_iff in H. specializes H a.
rewrite in_empty in H. rewrite <- H.
rewrite in_union. left. rewrite¬ in_singleton.
Qed.

Lemma singleton_absurd: x,
\{x} \{}.
Proof.
introv. apply fset_neq. x. split.
rewrite¬ in_singleton.
unfolds. introv H. rewrite inter_empty_r in H. rewrite¬ in_empty in H.
Qed.

End Basic.

Section Remove.
Variables A : Type.
Implicit Types E F G: fset A.
Implicit Types x: A.

Lemma notin_remove : E F x,
x \notin E \- Fx \notin E x \in F.
Proof.
introv H.
unfolds notin.
rewrite in_remove in H.
rew_logic in H. unfolds notin. rew_logic¬ in H.
Qed.

Lemma remove_while_notin: E x,
x \notin EE \- \{x} = E.
Proof.
introv H; apply fset_extens; unfold subset; introv H1.
rewrite in_remove in H1. destruct¬ H1.
rewrite in_remove. split¬. rewrite notin_singleton. applys× in_and_notin.
Qed.

Lemma remove_in_subsets: E F G,
E \c FE \- G \c F \- G.
Proof.
introv H.
unfolds subset. introv H1. rewrite in_remove. split.
apply H. rewrite in_remove in H1. apply H1.
rewrite in_remove in H1. apply H1.
Qed.

Lemma remove_comm: E F G,
(E \- F) \- G = (E \- G) \- F.
Proof.
introv. apply fset_extens; unfold subset; intro; rewrite_all in_remove; introv H; intuition.
Qed.

Lemma remove_same: E,
(E \- E) = \{}.
Proof.
introv. apply fset_extens; unfold subset; intro; rewrite in_remove; introv H.
false H. apply H.
rewrite in_empty in H. false.
Qed.

Lemma remove_empty: E,
E \- \{} = E.
Proof.
introv. apply fset_extens; unfold subset; intro; rewrite in_remove; introv H.
apply H.
split¬.
apply notin_empty.
Qed.

Lemma remove_from_empty: E,
(\{} \- E) = \{}.
Proof.
introv. apply fset_extens; unfold subset; intro; rewrite in_remove; introv H.
apply H.
split.
apply H.
rewrite in_empty in H. false.
Qed.

Lemma from_rem_to_union: E F x, Comparable A
x \in FE = F \- \{x}\{x} \u E = F.
Proof.
introv Hcmp H1 H2; apply fset_extens; unfold subset; introv H3.
rewrite in_union in H3. destruct H3.
rewrite in_singleton in H. rewrite¬ H.
rewrite H2 in H. rewrite× in_remove in H.
rewrite in_union. eapply fset_extens_iff in H2. erewrite H2.
rewrite in_remove. rewrite in_singleton. rewrite notin_singleton.
destruct Hcmp. specializes comparable x x0. destruct comparable as (b & dec).
destruct b.
apply eq_true_l in dec. rewrite istrue_isTrue in dec. subst. left¬.
apply eq_false_l in dec. rewrite istrue_neg in dec. rewrite istrue_isTrue in dec. right¬.
Qed.

Lemma rem_union_cancel: E x, Comparable A
x \in EE \- \{x} \u \{x} = E.
Proof.
introv Hcmp H. apply fset_extens; unfold subset; intros y .
rewrite in_union in . destruct .
rewrite in_remove in H0. destruct¬ H0.
rewrite in_singleton in H0. subst¬.
rewrite in_union. destruct Hcmp. specializes comparable x y.
destruct comparable as (b & dec). destruct b.
apply eq_true_l in dec. rewrite istrue_isTrue in dec. subst.
right. rewrite¬ in_singleton.
apply eq_false_l in dec. rewrite istrue_neg in dec. rewrite istrue_isTrue in dec.
left. rewrite in_remove. rewrite notin_singleton. split¬.
Qed.

Lemma remove_union: E F G,
E \- (F \u G) = (E \- F) \- G.
Proof.
introv.
apply fset_extens; unfold subset; intro; rewrite_all in_remove; introv H.
rewrite× notin_union in H.
rewrite× notin_union.
Qed.

Lemma remove_union_distr : E F G,
(E \- G) \u (F \- G) = (E \u F) \- G.
Proof.
introv; apply fset_extens; introv Hin;
rewrite in_union in *; rewrite in_remove in *; inverts Hin; intuition;
try rewrite in_union in *; try rewrite in_remove in *; try inverts H; jauto.
Qed.

Lemma remove_union_comm : E F x,
x \notin F(E \- F) \u \{x} = (E \u \{x}) \- F.
Proof.
introv Hnin; apply fset_extens; introv Hin;
rewrite in_remove in *; rewrite in_union in *; rewrite in_remove in *;
inverts Hin; jauto.
rewrite in_singleton in H; subst; splits¬.
right; rewrites¬ in_singleton.
inverts H; jauto.
Qed.

End Remove.

Section Union.
Variables A : Type.
Implicit Types E F G: fset A.
Implicit Types x y: A.

x \in E\{x} \u E = E.
Proof.
introv H. apply fset_extens; unfold subset; intros y .
rewrite in_union in . destruct¬ .
rewrite in_singleton in H0. subst¬.
rewrite in_union. right¬.
Qed.

Lemma union_empty: E F,
E \u F = \{}E=\{} F = \{}.
Proof.
introv H. split.
rewrite <- H. apply fset_extens; unfolds; introv H0.
rewrite in_union. left¬.
eapply fset_extens_iff in H. rewrite H in H0. false. rewrite¬ in_empty in H0.
rewrite <- H. apply fset_extens; unfolds; introv H0.
rewrite in_union. right¬.
eapply fset_extens_iff in H. rewrite H in H0. false. rewrite¬ in_empty in H0.
Qed.

Lemma from_union_to_rem: E F x,
x \notin E\{x} \u E = FE = F \- \{x}.
Proof.
introv H1 H2; apply fset_extens; unfold subset; introv H3.
rewrite <- H2. rewrite union_comm. rewrite union_remove. rewrite in_union.
left. rewrite¬ remove_while_notin.
rewrite <- H2 in H3. rewrite union_comm in H3. rewrite union_remove in H3.
rewrite in_union in H3. destruct H3. rewrite¬ remove_while_notin in H.
rewrite remove_same in H. rewrite× in_empty in H.
Qed.

Lemma union_subset: E F G,
(E \u F) \c GE \c G.
Proof.
unfold subset; introv H Hin.
apply H. rewrite in_union. left¬.
Qed.

Lemma union_inv: E x y,
\{x} \u E = \{y}x = y.
Proof.
introv H.
lets : fset_extens_iff. specializes A (\{ x} \u E) (\{ y}).
destruct . specializes H1 H x. rewrite in_union in H1.
rewrite_all in_singleton in H1. rewrite <- H1.
left¬.
Qed.

Lemma singleton_union: E F x,
\{x} = E \u Fx \in E x \in F.
Proof.
introv H.
lets : fset_extens_iff. specializes A \{ x} (E \u F).
destruct . specializes H1 H x. rewrite in_singleton in H1.
assert (x \in E \u F). rewrite¬ <- H1. clear H1.
rewrite¬ in_union in H2.
Qed.

Lemma union_not_empty: E F,
E \u F \{} E \{} F \{}.
Proof.
split. introv H.
destruct (empty_dec F).
left. rewrite <- (union_empty_r E). rewrite <- H0 at 1. assumption.
right¬.
introv H1 H2. apply union_empty in H2. destruct H2 as (H2 & H3).
destruct H1 ; apply¬ H.
Qed.

End Union.

Section Inter.
Variables A : Type.
Implicit Types E F G: fset A.

Lemma inter_union: E F G,
(E \u F) \n G = \{}E \n G = \{} F \n G = \{}.
Proof.
introv H. split; apply fset_extens; rewrite <- fset_extens_iff in H; unfolds subset;
introv H1; specializes H x; rewrite in_inter in ×.
rewrite <- H. rewrite in_union. split×.
rewrite in_empty in H1. false.
rewrite <- H. rewrite in_union. split×.
rewrite in_empty in H1. false.
Qed.

Lemma inter_remove: E F, (E \- F) \n F = \{}.
Proof.
introv. apply fset_extens; unfolds subset; introv H;
rewrite in_inter in *; rewrite in_remove in ×.
false H. apply H.
rewrite in_empty in H. false.
Qed.

Lemma inter_not_empty_exists : E F,
E \n F \{} x, x \in E \n F.
Proof.
introv Hneq.
elim (classic ( x, x \in E \n F)); introv Hnex; jauto.
false; apply Hneq.
apply fset_extens; introv Hin.
rewrite in_empty; rewrite× not_exists in Hnex.
rewrite× in_empty in Hin.
Qed.

Lemma inter_empty_subset : E1 E2 F1 F2,
E1 \n E2 = \{}F1 \c E1F2 \c E2F1 \n F2 = \{}.
Proof.
introv Hie Hs1 Hs2.
rewrite <- fset_extens_iff in Hie.
apply fset_extens; introv Hin.
rewrite in_inter in Hin; inverts Hin; apply Hs1 in H; apply Hs2 in H0.
rewrite <- (Hie x); rewrites× in_inter.
rewrite× in_empty in Hin.
Qed.

End Inter.

Section Subset.
Variables A : Type.
Implicit Types E F: fset A.
Implicit Types x: A.

Lemma fset_eq_sub: E F,
E = FE \c F.
Proof.
introv H.
rewrite H.
apply subset_refl.
Qed.

Lemma subset_of_empty: E,
E \c \{}E = \{}.
Proof.
introv H. apply fset_extens; unfolds subset; introv H1.
specializes¬ H H1.
rewrite in_empty in H1. false.
Qed.

Lemma subset_union_r: E F x,
x \notin EE \c (\{x} \u F) = E \c F.
Proof.
introv H. unfolds subset. rew_logic. split; introv H1 H2.
specializes H1 x0 H2. rewrite in_union in H1. destruct¬ H1.
rewrite in_singleton in H0. subst. false¬ H.
specializes H1 x0 H2. rewrite¬ in_union.
Qed.

End Subset.

Section FromList.
Variables A : Type.
Implicit Types E F : fset A.
Implicit Types l : list A.
Implicit Types x : A.

Lemma from_list_notin : l x,
¬Mem x lx \notin from_list l.
Proof.
induction l; introv Hnm.
rewrite from_list_nil. apply notin_empty.
rewrite from_list_cons. rewrite notin_union. split.
unfold notin. introv H. apply Hnm. rewrite in_singleton in H. rewrite H. apply Mem_here.
apply IHl. introv H. apply Hnm. constructor¬.
Qed.

Lemma from_list_spec : x l,
x \in from_list l = Mem x l.
Proof.
unfold from_list. induction l; rew_list.
rewrite in_empty. rewrite¬ Mem_nil_eq.
rewrite in_union, in_singleton. rewrite¬ Mem_cons_eq. congruence.
Qed.

Lemma from_list_base: l,
from_list l = \{}l = nil.
Proof.
introv H. induction¬ l.
rewrite from_list_cons in H. apply union_empty in H. false.
destruct H. eapply fset_extens_iff in H. rewrite in_singleton in H.
rewrite in_empty in H. rewrite¬ <- H.
Qed.

Lemma from_list_app : l1 l2,
from_list (l1 ++ l2) = from_list l1 \u from_list l2.
Proof.
introv; apply fset_extens; introv Hin; rewrite in_union in *;
repeat rewrite from_list_spec in *; rewrite Mem_app_or_eq in *; auto.
Qed.

End FromList.