Library Coq.Sets.Powerset_facts


Require Export Ensembles.

Require Export Constructive_sets.

Require Export Relations_1.

Require Export Relations_1_facts.

Require Export Partial_Order.

Require Export Cpo.

Require Export Powerset.




Section Sets_as_an_algebra.

  Variable U : Type.




  Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X.

  Proof.

    auto 6 with sets.

  Qed.




  Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.

  Proof.

    unfold Add at 1 in |- *; auto using Empty_set_zero with sets.

  Qed.




  Lemma less_than_empty :

    forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.

  Proof.

    auto with sets.

  Qed.




  Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A.

  Proof.

    auto with sets.

  Qed.




  Theorem Union_associative :

    forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).

  Proof.

    auto 9 with sets.

  Qed.




  Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A.

  Proof.

    auto 7 with sets.

  Qed.




  Lemma Union_absorbs :

    forall A B:Ensemble U, Included U B A -> Union U A B = A.

  Proof.

    auto 7 with sets.

  Qed.




  Theorem Couple_as_union :

    forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.

  Proof.

    intros x y; apply Extensionality_Ensembles; split; red in |- *.

    intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).

    intros x0 H'; elim H'; auto with sets.

  Qed.




  Theorem Triple_as_union :

    forall x y z:U,

      Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =

      Triple U x y z.

  Proof.

    intros x y z; apply Extensionality_Ensembles; split; red in |- *.

    intros x0 H'; elim H'.

    intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).

    intros x1 H'0; elim H'0; auto with sets.

    intros x0 H'; elim H'; auto with sets.

  Qed.




  Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.

  Proof.

    intros x y.

    rewrite <- (Couple_as_union x y).

    rewrite <- (Union_idempotent (Singleton U x)).

    apply Triple_as_union.

  Qed.




  Theorem Triple_as_Couple_Singleton :

    forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).

  Proof.

    intros x y z.

    rewrite <- (Triple_as_union x y z).

    rewrite <- (Couple_as_union x y); auto with sets.

  Qed.




  Theorem Intersection_commutative :

    forall A B:Ensemble U, Intersection U A B = Intersection U B A.

  Proof.

    intros A B.

    apply Extensionality_Ensembles.

    split; red in |- *; intros x H'; elim H'; auto with sets.

  Qed.




  Theorem Distributivity :

    forall A B C:Ensemble U,

      Intersection U A (Union U B C) =

      Union U (Intersection U A B) (Intersection U A C).

  Proof.

    intros A B C.

    apply Extensionality_Ensembles.

    split; red in |- *; intros x H'.

    elim H'.

    intros x0 H'0 H'1; generalize H'0.

    elim H'1; auto with sets.

    elim H'; intros x0 H'0; elim H'0; auto with sets.

  Qed.




  Theorem Distributivity' :

    forall A B C:Ensemble U,

      Union U A (Intersection U B C) =

      Intersection U (Union U A B) (Union U A C).

  Proof.

    intros A B C.

    apply Extensionality_Ensembles.

    split; red in |- *; intros x H'.

    elim H'; auto with sets.

    intros x0 H'0; elim H'0; auto with sets.

    elim H'.

    intros x0 H'0; elim H'0; auto with sets.

    intros x1 H'1 H'2; try exact H'2.

    generalize H'1.

    elim H'2; auto with sets.

  Qed.




  Theorem Union_add :

    forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).

  Proof.

    unfold Add in |- *; auto using Union_associative with sets.

  Qed.




  Theorem Non_disjoint_union :

    forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.

  Proof.

    intros X x H'; unfold Add in |- *.

    apply Extensionality_Ensembles; red in |- *.

    split; red in |- *; auto with sets.

    intros x0 H'0; elim H'0; auto with sets.

    intros t H'1; elim H'1; auto with sets.

  Qed.




  Theorem Non_disjoint_union' :

    forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.

  Proof.

    intros X x H'; unfold Subtract in |- *.

    apply Extensionality_Ensembles.

    split; red in |- *; auto with sets.

    intros x0 H'0; elim H'0; auto with sets.

    intros x0 H'0; apply Setminus_intro; auto with sets.

    red in |- *; intro H'1; elim H'1.

    lapply (Singleton_inv U x x0); auto with sets.

    intro H'4; apply H'; rewrite H'4; auto with sets.

  Qed.




  Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.

  Proof.

    intro x; rewrite (Empty_set_zero' x); auto with sets.

  Qed.




  Lemma incl_add :

    forall (A B:Ensemble U) (x:U),

      Included U A B -> Included U (Add U A x) (Add U B x).

  Proof.

    intros A B x H'; red in |- *; auto with sets.

    intros x0 H'0.

    lapply (Add_inv U A x x0); auto with sets.

    intro H'1; elim H'1;

      [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ];

      auto with sets.

  Qed.




  Lemma incl_add_x :

    forall (A B:Ensemble U) (x:U),

      ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.

  Proof.

    unfold Included in |- *.

    intros A B x H' H'0 x0 H'1.

    lapply (H'0 x0); auto with sets.

    intro H'2; lapply (Add_inv U B x x0); auto with sets.

    intro H'3; elim H'3;

      [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ].

    absurd (In U A x0); auto with sets.

    rewrite <- H'4; auto with sets.

  Qed.




  Lemma Add_commutative :

    forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.

  Proof.

    intros A x y.

    unfold Add in |- *.

    rewrite (Union_associative A (Singleton U x) (Singleton U y)).

    rewrite (Union_commutative (Singleton U x) (Singleton U y)).

    rewrite <- (Union_associative A (Singleton U y) (Singleton U x));

      auto with sets.

  Qed.




  Lemma Add_commutative' :

    forall (A:Ensemble U) (x y z:U),

      Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y.

  Proof.

    intros A x y z.

    rewrite (Add_commutative (Add U A x) y z).

    rewrite (Add_commutative A x z); auto with sets.

  Qed.




  Lemma Add_distributes :

    forall (A B:Ensemble U) (x y:U),

      Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).

  Proof.

    intros A B x y H'; try assumption.

    rewrite <- (Union_add (Add U A x) B y).

    unfold Add at 4 in |- *.

    rewrite (Union_commutative A (Singleton U x)).

    rewrite Union_associative.

    rewrite (Union_absorbs A B H').

    rewrite (Union_commutative (Singleton U x) A).

    auto with sets.

  Qed.




  Lemma setcover_intro :

    forall (U:Type) (A x y:Ensemble U),

      Strict_Included U x y ->

      ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) ->

      covers (Ensemble U) (Power_set_PO U A) y x.

  Proof.

    intros; apply Definition_of_covers; auto with sets.

  Qed.




End Sets_as_an_algebra.




Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add

  singlx incl_add: sets v62.