Require Export Omega.
Require Export Peano_dec.

Section U_SETS.

Variable U : Set.

Definition U_set := U → Prop.

Axiom U_set_eq : ∀ E F : U_set, (∀ x : U, E x ↔ F x) → E = F.

Lemma U_eq_set : ∀ E F : U_set, E = F → ∀ x : U, E x → F x.
Proof.
        intros; rewrite <- H; trivial.
Qed.

Lemma U_set_eq_commut : ∀ E F : U_set, E = F → F = E.
Proof.
        auto.
Qed.

Lemma U_set_diff_commut : ∀ E F : U_set, E ≠ F → F ≠ E.
Proof.
        intros; red in |- *; intros.
        elim H; apply U_set_eq_commut; trivial.
Qed.

Inductive Empty : U_set :=.

Inductive Full : U_set :=
    In_full : ∀ x : U, Full x.

Inductive Single (x : U) : U_set :=
    In_single : Single x x.

Lemma Single_equal : ∀ x y : U, Single x y → x = y.
Proof.
        intros; inversion H; trivial.
Qed.

Lemma Single_equal_single : ∀ x y : U, Single x = Single y → x = y.
Proof.
        intros; generalize (U_eq_set _ _ H x).
        intros; elim H0.
        trivial.

        apply In_single.
Qed.

Lemma Empty_nothing : ∀ x : U, ¬ Empty x.
Proof.
        tauto.
Qed.

Lemma U_set_diff : ∀ E F : U_set, (∃ x : U, E x ∧ ¬ F x) → E ≠ F.
Proof.
        intros; red in |- *; intros.
        elim H; intros.
        elim H1; intros.
        elim H3; rewrite <- H0; auto.
Qed.

        Section INCLUSION.

Definition Included (E F : U_set) : Prop := ∀ x : U, E x → F x.

Lemma Included_single :
 ∀ (E : U_set) (x : U), E x → Included (Single x) E.
Proof.
        unfold Included in |- *; intros.
        inversion H0; rewrite <- H1; trivial.
Qed.

        End INCLUSION.

        Section UNION.

Inductive Union (E F : U_set) : U_set :=
  | In_left : ∀ x : U, E x → Union E F x
  | In_right : ∀ x : U, F x → Union E F x.

Lemma Union_eq :
 ∀ E F E' F' : U_set, E = E' → F = F' → Union E F = Union E' F'.
Proof.
        intros; elim H.
        elim H0; trivial.
Qed.

Lemma Union_neutral : ∀ e : U_set, Union Empty e = e.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H.
        inversion H0.

        trivial.

        apply In_right; trivial.
Qed.

Lemma Union_commut : ∀ e1 e2 : U_set, Union e1 e2 = Union e2 e1.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H; [ apply In_right | apply In_left ]; trivial.

        inversion H; [ apply In_right | apply In_left ]; trivial.
Qed.

Lemma Union_assoc :
 ∀ e1 e2 e3 : U_set, Union (Union e1 e2) e3 = Union e1 (Union e2 e3).
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H.
        inversion H0.
        apply In_left; trivial.

        apply In_right; apply In_left; trivial.

        apply In_right; apply In_right; trivial.

        inversion H.
        apply In_left; apply In_left; trivial.

        inversion H0.
        apply In_left; apply In_right; trivial.

        apply In_right; trivial.
Qed.

Lemma Not_union :
 ∀ (E1 E2 : U_set) (x : U), ¬ E1 x → ¬ E2 x → ¬ Union E1 E2 x.
Proof.
        intros; red in |- *; intros.
        inversion H1.
        elim H; trivial.

        elim H0; trivial.
Qed.

Lemma Union_dec :
 ∀ (e1 e2 : U_set) (x : U),
 {e1 x} + {¬ e1 x} → {e2 x} + {¬ e2 x} → Union e1 e2 x → {e1 x} + {e2 x}.
Proof.
        intros; case H.
        left; trivial.

        intros; case H0; intros.
        right; trivial.

        absurd (Union e1 e2 x).
        apply Not_union; trivial.

        trivial.
Qed.

Lemma Included_union : ∀ E F : U_set, Included E (Union E F).
Proof.
        unfold Included in |- *; intros.
        apply In_left; trivial.
Qed.

Lemma Union_absorb : ∀ E F : U_set, Included E F → Union E F = F.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H0; auto.

        apply In_right; trivial.
Qed.

        End UNION.

        Section INTERSECTION.

Inductive Inter (E F : U_set) : U_set :=
    In_inter : ∀ x : U, E x → F x → Inter E F x.

Lemma Inter_eq :
 ∀ E F E' F' : U_set, E = E' → F = F' → Inter E F = Inter E' F'.
Proof.
        intros; elim H.
        elim H0; trivial.
Qed.

Lemma Inter_neutral : ∀ e : U_set, Inter Full e = e.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H; trivial.

        apply In_inter.
        apply In_full; trivial.

        trivial.
Qed.

Lemma Inter_empty : ∀ e : U_set, Inter e Empty = Empty.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H; trivial.

        inversion H.
Qed.

Lemma Inter_commut : ∀ e1 e2 : U_set, Inter e1 e2 = Inter e2 e1.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H; apply In_inter; trivial.

        inversion H; apply In_inter; trivial.
Qed.

Lemma Inter_assoc :
 ∀ e1 e2 e3 : U_set, Inter (Inter e1 e2) e3 = Inter e1 (Inter e2 e3).
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H; inversion H0.
        apply In_inter; trivial.
        apply In_inter; trivial.

        inversion H; inversion H1.
        apply In_inter; trivial.
        apply In_inter; trivial.
Qed.

Lemma Not_inter : ∀ (E1 E2 : U_set) (x : U), ¬ E1 x → ¬ Inter E1 E2 x.
Proof.
        intros; red in |- *; intros.
        inversion H0.
        elim H; trivial.
Qed.

Lemma Included_inter : ∀ E F : U_set, Included (Inter E F) E.
Proof.
        unfold Included in |- *; intros.
        inversion H; trivial.
Qed.

Lemma Inter_absorb : ∀ E F : U_set, Included E F → Inter E F = E.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H0; auto.

        apply In_inter; auto.
Qed.

        End INTERSECTION.

        Section DIFFERENCE.

Inductive Differ (E F : U_set) : U_set :=
    In_differ : ∀ x : U, E x → ¬ F x → Differ E F x.

Lemma Differ_E_E : ∀ E : U_set, Differ E E = Empty.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H.
        absurd (E x); trivial.

        inversion H.
Qed.

Lemma Differ_empty : ∀ E : U_set, Differ E Empty = E.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H; trivial.

        apply In_differ.
        trivial.

        tauto.
Qed.

Lemma Union_differ_inter :
 ∀ E F : U_set,
 (∀ x : U, {F x} + {¬ F x}) → Union (Differ E F) (Inter E F) = E.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H0.
        inversion H1; trivial.

        inversion H1; trivial.

        case (H x); intros.
        apply In_right; apply In_inter; trivial.

        apply In_left; apply In_differ; trivial.
Qed.

        End DIFFERENCE.

        Section MIXED_PROPERTIES.

Lemma Distributivity_inter_union :
 ∀ E F G : U_set, Inter E (Union F G) = Union (Inter E F) (Inter E G).
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H; inversion H1.
        apply In_left; apply In_inter; auto.

        apply In_right; apply In_inter; auto.

        inversion H; inversion H0.
        apply In_inter.
        trivial.

        apply In_left; trivial.

        apply In_inter.
        trivial.

        apply In_right; trivial.
Qed.

Lemma Distributivity_union_inter :
 ∀ E F G : U_set, Union E (Inter F G) = Inter (Union E F) (Union E G).
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H.
        apply In_inter; apply In_left; trivial.

        inversion H0; apply In_inter; apply In_right; trivial.

        inversion H.
        inversion H0.
        apply In_left; trivial.

        inversion H1.
        apply In_left; trivial.

        apply In_right; apply In_inter; trivial.
Qed.

Lemma Union_inversion :
 ∀ E F G : U_set,
 Inter E F = Empty → Inter E G = Empty → Union E F = Union E G → F = G.
Proof.
        intros; apply U_set_eq; split; intros.
        generalize (In_right E F x H2).
        rewrite H1; intros.
        inversion H3.
        absurd (Inter E F x).
        rewrite H; tauto.

        apply In_inter; auto.

        trivial.

        generalize (In_right E G x H2).
        rewrite <- H1; intros.
        inversion H3.
        absurd (Inter E G x).
        rewrite H0; tauto.

        apply In_inter; auto.

        trivial.
Qed.

Lemma Union_inversion2 :
 ∀ E F G H : U_set,
 Inter E F = Empty →
 Inter E G = Empty →
 Inter G H = Empty → Union E F = Union G H → F = Union G (Inter F H).
Proof.
        intros; apply U_set_eq; split; intros.
        generalize (In_right E F x H4).
        rewrite H3; intros.
        inversion H5.
        apply In_left; trivial.

        apply In_right; apply In_inter; trivial.

        inversion H4.
        generalize (In_left G H x H5).
        rewrite <- H3; intros.
        inversion H7.
        absurd (Inter E G x).
        rewrite H1; tauto.

        apply In_inter; trivial.

        trivial.

        inversion H5; trivial.
Qed.

Lemma Single_disjoint :
 ∀ (x : U) (E : U_set), ¬ E x → Inter (Single x) E = Empty.
Proof.
        intros; apply U_set_eq; split; intros.
        inversion H0.
        inversion H1; absurd (E x).
        trivial.

        rewrite H4; trivial.

        inversion H0.
Qed.

Lemma Single_single_disjoint :
 ∀ x y : U, x ≠ y → Inter (Single x) (Single y) = Empty.
Proof.
        intros; apply Single_disjoint.
        red in |- *; intros H0; elim H; inversion H0; trivial.
Qed.

Lemma Union_single_single :
 ∀ (e : U_set) (x y : U),
 x ≠ y →
 ¬ e y → Union (Single x) (Single y) = Union (Single y) e → e = Single x.
Proof.
        intros; symmetry in |- *; apply (Union_inversion (Single y)).
        apply Single_single_disjoint; auto.

        apply Single_disjoint; trivial.

        rewrite Union_commut; trivial.
Qed.

        End MIXED_PROPERTIES.

End U_SETS.