Library Coq.Sets.Classical_sets


Require Export Ensembles.

Require Export Constructive_sets.

Require Export Classical_Type.




Section Ensembles_classical.

  Variable U : Type.




  Lemma not_included_empty_Inhabited :

    forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.

  Proof.

    intros A NI.

    elim (not_all_ex_not U (fun x:U => ~ In U A x)).

    intros x H; apply Inhabited_intro with x.

    apply NNPP; auto with sets.

    red in |- *; intro.

    apply NI; red in |- *.

    intros x H'; elim (H x); trivial with sets.

  Qed.




  Lemma not_empty_Inhabited :

    forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.

  Proof.

    intros; apply not_included_empty_Inhabited.

    red in |- *; auto with sets.

  Qed.




  Lemma Inhabited_Setminus :

    forall X Y:Ensemble U,

      Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).

  Proof.

    intros X Y I NI.

    elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).

    intros x YX.

    apply Inhabited_intro with x.

    apply Setminus_intro.

    apply not_imply_elim with (In U X x); trivial with sets.

    auto with sets.

  Qed.




  Lemma Strict_super_set_contains_new_element :

    forall X Y:Ensemble U,

      Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).

  Proof.

    auto 7 using Inhabited_Setminus with sets.

  Qed.




  Lemma Subtract_intro :

    forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.

  Proof.

    unfold Subtract at 1 in |- *; auto with sets.

  Qed.

  Hint Resolve Subtract_intro : sets.




  Lemma Subtract_inv :

    forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.

  Proof.

    intros A x y H'; elim H'; auto with sets.

  Qed.




  Lemma Included_Strict_Included :

    forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.

  Proof.

    intros X Y H'; try assumption.

    elim (classic (X = Y)); auto with sets.

  Qed.




  Lemma Strict_Included_inv :

    forall X Y:Ensemble U,

      Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).

  Proof.

    intros X Y H'; red in H'.

    split; [ tauto | idtac ].

    elim H'; intros H'0 H'1; try exact H'1; clear H'.

    apply Strict_super_set_contains_new_element; auto with sets.

  Qed.




  Lemma not_SIncl_empty :

    forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).

  Proof.

    intro X; red in |- *; intro H'; try exact H'.

    lapply (Strict_Included_inv X (Empty_set U)); auto with sets.

    intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.

    intros x H'0; elim H'0.

    intro H'3; elim H'3.

  Qed.




  Lemma Complement_Complement :

    forall A:Ensemble U, Complement U (Complement U A) = A.

  Proof.

    unfold Complement in |- *; intros; apply Extensionality_Ensembles;

      auto with sets.

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

    red in |- *; intros; apply NNPP; auto with sets.

  Qed.




End Ensembles_classical.




 Hint Resolve Strict_super_set_contains_new_element Subtract_intro

  not_SIncl_empty: sets v62.