Library EnsembleAsType

Section EnsembleAsType.

Require Import EnsembleFacts.

Require Import Coq.Sets.Ensembles.
Require Import Coq.Relations.Relations.
Require Import Classical.

Require Import types.

Inductive EnsembleAsType (U:Type) (A:Ensemble U) :=
EnsembleAsTypeIntro: forall x:U, In U A x -> EnsembleAsType U A
.

Definition EAT:=EnsembleAsType.

Lemma EAT_anyhypothesis:forall (U:Type) (A:Ensemble U) (x:U)
(H1 H2:In U A x),
EnsembleAsTypeIntro U A x H1=EnsembleAsTypeIntro U A x H2.

Definition EAT_in (U:Type) (A:Ensemble U) (f:U->EAT U A):=
forall (x:U) (H:In U A x), f x=EnsembleAsTypeIntro U A x H.

Definition EAT_out (U:Type) (A:Ensemble U) (f:EAT U A->U):=
forall (x:U) (H:In U A x), f (EnsembleAsTypeIntro U A x H)=x.

Theorem EAT_out_in:forall (U:Type) (A:Ensemble U) (fin:U->EAT U A)
(fout:EAT U A->U) (x:U), EAT_in U A fin -> EAT_out U A fout ->
In U A x -> fout (fin x)=x.

Theorem EAT_in_out:forall (U:Type) (A:Ensemble U) (fin:U->EAT U A)
(fout:EAT U A->U) (x:EAT U A), EAT_in U A fin -> EAT_out U A fout ->
fin (fout x)=x.

Theorem EAT_out_InA: forall (U:Type) (A:Ensemble U)
(fout:EAT U A->U) (x:EAT U A), EAT_out U A fout -> In U A (fout x).


Theorem EAT_in_exists: forall (U:Type) (A:Ensemble U) (x:U),
In U A x -> exists f, EAT_in U A f.

Theorem EAT_existence: forall (U:Type) (A:Ensemble U)
(x:EnsembleAsType U A), exists y:U,
exists InA:In U A y, EnsembleAsTypeIntro U A y InA=x.

Definition EnsembleAsTypeOut (U:Type) (A:Ensemble U)
:EnsembleAsType U A->U.
Defined.

Definition EAT_fout:=EnsembleAsTypeOut.

Theorem EnsembleAsTypeOut_isout: forall (U:Type) (A:Ensemble U),
EAT_out U A (EnsembleAsTypeOut U A).

Theorem EAT_out_intro: forall (U:Type) (A:Ensemble U) (x:U)
(xh:In U A x),
EnsembleAsTypeOut U A (EnsembleAsTypeIntro U A x xh)=x.

Theorem EAT_fout_in:forall (U:Type) (A:Ensemble U) (fin:U->EAT U A)
(x:U), EAT_in U A fin -> In U A x -> EAT_fout U A (fin x)=x.

Theorem EAT_in_fout:forall (U:Type) (A:Ensemble U) (fin:U->EAT U A)
(x:EAT U A), EAT_in U A fin -> fin (EAT_fout U A x)=x.

Theorem EAT_fout_InA: forall (U:Type) (A:Ensemble U)
(x:EAT U A), In U A (EAT_fout U A x).

Theorem EAT_fout_simplify: forall (U:Type) (A:Ensemble U)
(x y:EAT U A), EAT_fout U A x=EAT_fout U A y->x=y.

Definition EAT_ex1set:=Triple nat 2 5 11.

Definition EAT_ex1:=EnsembleAsType nat EAT_ex1set.

Theorem EAT_ex2: forall x:EAT_ex1,
EnsembleAsTypeOut nat EAT_ex1set x=2 \/
EnsembleAsTypeOut nat EAT_ex1set x=5 \/
EnsembleAsTypeOut nat EAT_ex1set x=11.


Inductive BigUnion (U:Type) (S:Ensemble (Ensemble U)):Ensemble U:=
BigUnion_intro:forall X:Ensemble U, In (Ensemble U) S X
-> forall x:U, In U X x-> In U (BigUnion U S) x.

Theorem BigUnion_pair: forall (U:Type) (A B:Ensemble U),
BigUnion U (Couple (Ensemble U) A B)=Union U A B.

Inductive BigIntersection (U:Type) (S:Ensemble (Ensemble U))
:Ensemble U:=
BigIntersection_intro:forall x:U,
(forall X:Ensemble U, In (Ensemble U) S X -> In U X x)
-> In U (BigIntersection U S) x.

Theorem BigIntersection_pair: forall (U:Type) (A B:Ensemble U),
BigIntersection U (Couple (Ensemble U) A B)=Intersection U A B.

Definition Partition (U:Type) (P:Ensemble (Ensemble U)):=
BigUnion U P=Full_set U /\
(forall X Y:Ensemble U, In (Ensemble U) P X -> In (Ensemble U) P Y
 -> X<>Y -> Intersection U X Y=Empty_set U).

Inductive RelatedElements (U:Type) (R:relation U) (x:U):Ensemble U:=
RelatedElements_intro: forall y:U, R x y
 -> In U (RelatedElements U R x) y.

Theorem RelatedByEquivalence: forall (U:Type) (R:relation U) (x y:U),
equiv U R -> R x y -> RelatedElements U R x=RelatedElements U R y.

Definition PartitionFromEquivalence (U:Type) (R:relation U)
:Ensemble (Ensemble U) :=
apply_func U (Ensemble U)
 
 (fun x=>RelatedElements U R x)
 (Full_set U).

Theorem PartitionFromEquivalence_intro:
forall (U:Type) (R:relation U) (x:U),
equiv U R->In (Ensemble U) (PartitionFromEquivalence U R)
(RelatedElements U R x).

Theorem PartitionFromEquivalence_out:
forall (U:Type) (R:relation U) (X:Ensemble U),
equiv U R->In (Ensemble U) (PartitionFromEquivalence U R) X->
exists x:U,X=(RelatedElements U R x).

Theorem EquivalenceFormsPartition: forall (U:Type) (R:relation U),
equiv U R->Partition U (PartitionFromEquivalence U R).

Inductive EquivalenceFromPartition (U:Type) (P:Ensemble (Ensemble U))
:relation U:=
EquivalenceFromPartition_intro:
 forall X:Ensemble U, In (Ensemble U) P X->
 forall a b:U, In U X a -> In U X b ->
 (EquivalenceFromPartition U P) a b.

Theorem ElementPartition: forall (U:Type) (P:Ensemble (Ensemble U))
(x:U),
Partition U P-> exists X:Ensemble U, In (Ensemble U) P X /\ In U X x.

Theorem EquivalenceFromPartition_equiv:
 forall (U:Type) (P:Ensemble (Ensemble U)), Partition U P->
equiv U (EquivalenceFromPartition U P).

Lemma PartitionExlusive: forall (U:Type) (P:Ensemble (Ensemble U))
(A B:Ensemble U) (x:U),
Partition U P -> In (Ensemble U) P A -> In (Ensemble U) P B ->
In U A x -> In U B x -> A=B.

Theorem UniquePartition: forall (U:Type) (R:relation U),
equiv U R->exists! P:Ensemble (Ensemble U),
 Partition U P /\
 (forall S:Ensemble U, In (Ensemble U) P S->S<>Empty_set U) /\
 forall (a b:U), R a b <->
  (forall (X:Ensemble U), In (Ensemble U) P X ->
   In U X a -> In U X b).

End EnsembleAsType.