(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(****************************************************************************)
(*                                                                          *)
(*                         Naive Set Theory in Coq                          *)
(*                                                                          *)
(*                     INRIA                        INRIA                   *)
(*              Rocquencourt                        Sophia-Antipolis        *)
(*                                                                          *)
(*                                 Coq V6.1                                 *)
(*									    *)
(*			         Gilles Kahn 				    *)
(*				 Gerard Huet				    *)
(*									    *)
(*									    *)
(*                                                                          *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
(* to the Newton Institute for providing an exceptional work environment    *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
(****************************************************************************)

Require Export Ensembles.
Require Export Constructive_sets.
Require Export Classical.

Section Ensembles_classical.
  Variable U : Type.

  Lemma not_included_empty_Inhabited :
    forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.
U:Type
forall A : Ensemble U,
~ Included U A (Empty_set U) -> Inhabited U A
  Proof.
U:Type
forall A : Ensemble U,
~ Included U A (Empty_set U) -> Inhabited U A
    intros A NI.
U:Type
A:Ensemble U
NI:~ Included U A (Empty_set U)
Inhabited U A
    elim (not_all_ex_not U (fun x:U => ~ In U A x)).
U:Type
A:Ensemble U
NI:~ Included U A (Empty_set U)
forall x : U, ~ ~ In U A x -> Inhabited U A
U:Type
A:Ensemble U
NI:~ Included U A (Empty_set U)
~ (forall n : U, ~ In U A n)
    intros x H; apply Inhabited_intro with x.
U:Type
A:Ensemble U
NI:~ Included U A (Empty_set U)
x:U
H:~ ~ In U A x
In U A x
U:Type
A:Ensemble U
NI:~ Included U A (Empty_set U)
~ (forall n : U, ~ In U A n)
    apply NNPP; auto with sets.
U:Type
A:Ensemble U
NI:~ Included U A (Empty_set U)
~ (forall n : U, ~ In U A n)
    red; intro.
U:Type
A:Ensemble U
NI:~ Included U A (Empty_set U)
H:forall n : U, ~ In U A n
False
    apply NI; red.
U:Type
A:Ensemble U
NI:~ Included U A (Empty_set U)
H:forall n : U, ~ In U A n
forall x : U, In U A x -> In U (Empty_set U) x
    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.
U:Type
forall A : Ensemble U,
A <> Empty_set U -> Inhabited U A
  Proof.
U:Type
forall A : Ensemble U,
A <> Empty_set U -> Inhabited U A
    intros; apply not_included_empty_Inhabited.
U:Type
A:Ensemble U
H:A <> Empty_set U
~ Included U A (Empty_set U)
    red; 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).
U:Type
forall X Y : Ensemble U,
Included U X Y ->
~ Included U Y X -> Inhabited U (Setminus U Y X)
  Proof.
U:Type
forall X Y : Ensemble U,
Included U X Y ->
~ Included U Y X -> Inhabited U (Setminus U Y X)
    intros X Y I NI.
U:Type
X, Y:Ensemble U
I:Included U X Y
NI:~ Included U Y X
Inhabited U (Setminus U Y X)
    elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).
U:Type
X, Y:Ensemble U
I:Included U X Y
NI:~ Included U Y X
forall x : U,
~ (In U Y x -> In U X x) ->
Inhabited U (Setminus U Y X)
    intros x YX.
U:Type
X, Y:Ensemble U
I:Included U X Y
NI:~ Included U Y X
x:U
YX:~ (In U Y x -> In U X x)
Inhabited U (Setminus U Y X)
    apply Inhabited_intro with x.
U:Type
X, Y:Ensemble U
I:Included U X Y
NI:~ Included U Y X
x:U
YX:~ (In U Y x -> In U X x)
In U (Setminus U Y X) x
    apply Setminus_intro.
U:Type
X, Y:Ensemble U
I:Included U X Y
NI:~ Included U Y X
x:U
YX:~ (In U Y x -> In U X x)
In U Y x
U:Type
X, Y:Ensemble U
I:Included U X Y
NI:~ Included U Y X
x:U
YX:~ (In U Y x -> In U X x)
~ In U X x
    apply not_imply_elim with (In U X x); trivial with sets.
U:Type
X, Y:Ensemble U
I:Included U X Y
NI:~ Included U Y X
x:U
YX:~ (In U Y x -> In U X x)
~ In U X x
    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).
U:Type
forall X Y : Ensemble U,
Included U X Y ->
X <> Y -> Inhabited U (Setminus U Y X)
  Proof.
U:Type
forall X Y : Ensemble U,
Included U X Y ->
X <> Y -> Inhabited U (Setminus U Y X)
    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.
U:Type
forall (A : Ensemble U) (x y : U),
In U A y -> x <> y -> In U (Subtract U A x) y
  Proof.
U:Type
forall (A : Ensemble U) (x y : U),
In U A y -> x <> y -> In U (Subtract U A x) y
    unfold Subtract at 1; 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.
U:Type
forall (A : Ensemble U) (x y : U),
In U (Subtract U A x) y -> In U A y /\ x <> y
  Proof.
U:Type
forall (A : Ensemble U) (x y : U),
In U (Subtract U A x) y -> In U A y /\ x <> y
    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.
U:Type
forall X Y : Ensemble U,
Included U X Y -> Strict_Included U X Y \/ X = Y
  Proof.
U:Type
forall X Y : Ensemble U,
Included U X Y -> Strict_Included U X Y \/ X = Y
    intros X Y H'; try assumption.
U:Type
X, Y:Ensemble U
H':Included U X Y
Strict_Included U X Y \/ X = Y
    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).
U:Type
forall X Y : Ensemble U,
Strict_Included U X Y ->
Included U X Y /\ Inhabited U (Setminus U Y X)
  Proof.
U:Type
forall X Y : Ensemble U,
Strict_Included U X Y ->
Included U X Y /\ Inhabited U (Setminus U Y X)
    intros X Y H'; red in H'.
U:Type
X, Y:Ensemble U
H':Included U X Y /\ X <> Y
Included U X Y /\ Inhabited U (Setminus U Y X)
    split; [ tauto | idtac ].
U:Type
X, Y:Ensemble U
H':Included U X Y /\ X <> Y
Inhabited U (Setminus U Y X)
    elim H'; intros H'0 H'1; try exact H'1; clear H'.
U:Type
X, Y:Ensemble U
H'0:Included U X Y
H'1:X <> Y
Inhabited U (Setminus U Y X)
    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).
U:Type
forall X : Ensemble U,
~ Strict_Included U X (Empty_set U)
  Proof.
U:Type
forall X : Ensemble U,
~ Strict_Included U X (Empty_set U)
    intro X; red; intro H'; try exact H'.
U:Type
X:Ensemble U
H':Strict_Included U X (Empty_set U)
False
    lapply (Strict_Included_inv X (Empty_set U)); auto with sets.
U:Type
X:Ensemble U
H':Strict_Included U X (Empty_set U)
Included U X (Empty_set U) /\
Inhabited U (Setminus U (Empty_set U) X) -> False
    intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.
U:Type
X:Ensemble U
H':Strict_Included U X (Empty_set U)
H'1:Included U X (Empty_set U)
H'2:Inhabited U (Setminus U (Empty_set U) X)
forall x : U,
In U (Setminus U (Empty_set U) X) x -> False
    intros x H'0; elim H'0.
U:Type
X:Ensemble U
H':Strict_Included U X (Empty_set U)
H'1:Included U X (Empty_set U)
H'2:Inhabited U (Setminus U (Empty_set U) X)
x:U
H'0:In U (Setminus U (Empty_set U) X) x
In U (Empty_set U) x -> ~ In U X x -> False
    intro H'3; elim H'3.
  Qed.

  Lemma Complement_Complement :
    forall A:Ensemble U, Complement U (Complement U A) = A.
U:Type
forall A : Ensemble U,
Complement U (Complement U A) = A
  Proof.
U:Type
forall A : Ensemble U,
Complement U (Complement U A) = A
    unfold Complement; intros; apply Extensionality_Ensembles;
      auto with sets.
U:Type
A:Ensemble U
Same_set U
  (fun x : U => ~ In U (fun x0 : U => ~ In U A x0) x)
  A
    red; split; auto with sets.
U:Type
A:Ensemble U
Included U
  (fun x : U => ~ In U (fun x0 : U => ~ In U A x0) x)
  A
    red; intros; apply NNPP; auto with sets.
  Qed.

End Ensembles_classical.

 Hint Resolve Strict_super_set_contains_new_element Subtract_intro
  not_SIncl_empty: sets.