Library EnsembleFacts

Section EnsembleFacts.

Require Import Coq.Sets.Ensembles.
Require Import Coq.Sets.Finite_sets.
Require Import Classical.
Require Import Coq.Logic.ClassicalChoice.
Require Import Coq.Sets.Finite_sets_facts.

Require Import Setoid.
Require Import Coq.omega.Omega.

Definition Operation (U:Type):Type := U->U->U.

Definition Associativity (U:Type) (f:Operation U):=
forall (a b c:U), f (f a b) c= f a (f b c).

Definition Commutativity (U:Type) (f:Operation U):=
forall (a b:U), f a b= f b a.
Implicit Arguments Associativity [U].
Implicit Arguments Commutativity [U].

Theorem existsfunctions : forall (U1 U2:Type) (P:U1->U2->Prop),
(forall (a:U1), exists b:U2, P a b)->
(exists f:U1->U2, forall a:U1, P a (f a)).

Lemma selfincluded : forall (U:Type) (A:Ensemble U),
Included U A A.

Theorem Extensionality_Ensembles_rec:
forall (U:Type) (A B:Ensemble U), A=B -> Same_set U A B.

Lemma SameCouple: forall (U:Type) (a:U),
Couple U a a=Singleton U a.

Lemma EqualCouples:
forall (U:Type) (e a b:U),
Couple U e a=Couple U e b -> a=b.

Lemma CoupleComm: forall (U:Type) (a b:U),
Couple U a b=Couple U b a.

Definition Bijective (U1 U2:Type) (f:U1->U2):Prop:=
(forall a b:U1, a<>b -> f a<>f b) /\
(forall b:U2, exists a:U1, f a=b).

Theorem Bijective_rev : forall (U1 U2:Type) (f:U1->U2) (a b:U1),
 (Bijective U1 U2 f) -> f a=f b -> a=b.

Inductive apply_func (U1 U2:Type) (f:U1->U2) (S:Ensemble U1)
:Ensemble U2 :=
|In_apply_func: forall a:U1, In U1 S a->
  In U2 (apply_func U1 U2 f S) (f a).

Lemma apply_func_rec : forall (U1 U2:Type) (f:U1->U2)
(S:Ensemble U1) (a:U2),
In U2 (apply_func U1 U2 f S) a ->
exists ia:U1, In U1 S ia /\ f ia=a.

Theorem apply_func_empty : forall (U1 U2:Type) (f:U1->U2)
(S:Ensemble U1),
 (apply_func U1 U2 f (Empty_set U1)) = Empty_set U2.

Theorem apply_func_singleton : forall (U1 U2:Type) (f:U1->U2)
(x:U1),
 (apply_func U1 U2 f (Singleton U1 x))
  = Singleton U2 (f x).

Theorem apply_func_add : forall (U1 U2:Type) (f:U1->U2)
(S:Ensemble U1) (x:U1),
 (apply_func U1 U2 f (Add U1 S x))
  = Add U2 (apply_func U1 U2 f S) (f x).

Theorem apply_func_intersection : forall (U1 U2:Type)
(f:U1->U2) (A B:Ensemble U1), (Bijective U1 U2 f) ->
 (apply_func U1 U2 f (Intersection U1 A B))
  = Intersection U2
     (apply_func U1 U2 f A) (apply_func U1 U2 f B).

Theorem apply_func_couple : forall (U1 U2:Type)
(f:U1->U2) (a b:U1), (Bijective U1 U2 f) ->
 (apply_func U1 U2 f (Couple U1 a b))
  = Couple U2 (f a) (f b).

Theorem apply_func_equation : forall (U1 U2:Type) (f:U1->U2)
(A B:Ensemble U1), A=B ->
apply_func U1 U2 f A = apply_func U1 U2 f B.

Theorem bijective_eqcardinal : forall (U1 U2:Type) (f:U1->U2)
 (S:Ensemble U1), (Bijective U1 U2 f) ->
 (forall (n:nat),
   (cardinal U1 S n) ->(cardinal U2 (apply_func U1 U2 f S) n) ).

Definition InverseFunction (U1 U2:Type) (f:U1->U2) (g:U2->U1)
:= forall (a:U1) (b:U2), f a =b -> g b =a.

Lemma UndoInverse :
forall (U1 U2:Type) (f:U1->U2) (g:U2->U1) (a:U1),
InverseFunction U1 U2 f g -> g (f a)=a.

Theorem InverseOfBijectiveIsBijective :
forall (U1 U2:Type) (f:U1->U2) (g:U2->U1),
Bijective U1 U2 f -> InverseFunction U1 U2 f g
-> Bijective U2 U1 g.

Lemma UndoInverseBijective :
forall (U1 U2:Type) (f:U1->U2) (g:U2->U1),
Bijective U1 U2 f->
(InverseFunction U1 U2 f g) -> (InverseFunction U2 U1 g f).

Lemma UndoInverseSym :
forall (U1 U2:Type) (f:U1->U2) (g:U2->U1) (b:U2),
Bijective U1 U2 f ->
InverseFunction U1 U2 f g -> f (g b)=b.

Theorem ExistsInverseOfBijective:
forall (U1 U2:Type) (f:U1->U2), Bijective U1 U2 f ->
exists g:U2->U1, InverseFunction U1 U2 f g.

Lemma BijectionSimplify:
forall (U1 U2:Type) (f:U1->U2) (a b:U1),
Bijective U1 U2 f -> f a = f b -> a=b.

Definition Compose (U1 U2 U3:Type) (f:U2->U3) (g:U1->U2):=
fun (a:U1) => f (g a).

Theorem BijectionComposition :
forall (U1 U2 U3:Type) (f:U2->U3) (g:U1->U2),
Bijective U2 U3 f -> Bijective U1 U2 g ->
Bijective U1 U3 (Compose U1 U2 U3 f g).

Lemma DifferentAdd_Empty : forall (U:Type) (x:U) (A:Ensemble U),
Add U A x <> Empty_set U.

Lemma DisjointAddElim:
forall (U:Type) (A:Ensemble U) (a x:U),
In U (Add U A a) x -> ~ In U A a -> x<>a -> In U A x.

Lemma DisjointAddEquation:
forall (U:Type) (A B:Ensemble U) (a b:U),
Add U A a=Add U B b-> ~ In U A a -> ~ In U B b ->
(a=b /\ A=B) \/ (a<>b /\ In U A b /\ In U B a).

Lemma EnsembleAddInto:
forall (U:Type) (A B:Ensemble U) (a x:U),
In U A x -> Add U B a = A -> a <> x -> In U B x.

Lemma EnsembleAddComm:
forall (U:Type) (A:Ensemble U) (a b:U),
Add U (Add U A a) b= Add U (Add U A b) a.

Lemma DisjointAddEquationElim:
forall (U:Type) (A B:Ensemble U) (x:U),
~ In U A x -> ~ In U B x -> Add U A x=Add U B x -> A=B.

Lemma NonEmptyAsAdd:
forall (U:Type) (A:Ensemble U),
Finite U A-> forall a:U,
In U A a ->
exists B:Ensemble U, A=Add U B a /\ ~ In U B a.

Lemma EnsembleAddIncludes :
forall (U:Type) (A:Ensemble U) (a:U),
Included U A (Add U A a).

Lemma EnsembleSubFinite :
forall (U:Type) (A:Ensemble U) (a:U),
Finite U (Add U A a) -> Finite U A.

Lemma DisjointAddEquationCommon:
forall (U:Type) (A B:Ensemble U) (a b:U),
Finite U A-> Add U A a=Add U B b->
~ In U A a -> ~ In U B b -> a<>b ->
exists C:Ensemble U, A =Add U C b /\ B=Add U C a /\
~In U C a /\ ~In U C b /\ In U A b /\ In U B a.

Lemma EnsembleAddEmptyIsSingleton:
forall (U:Type) (A:Ensemble U) (a:U),
Add U (Empty_set U) a = Singleton U a.

Lemma EnsemblesSingletonEqAdd:
forall (U:Type) (A:Ensemble U) (a b:U),
Singleton U b = Add U A a -> a=b.

Lemma EnsemblesSingletonEqDisjAdd:
forall (U:Type) (A:Ensemble U) (a b:U),
~ In U A a -> Singleton U b = Add U A a ->
(a=b /\ A=Empty_set U) .

Lemma EnsembleAddToSub :
forall (U:Type) (A B:Ensemble U) (a:U),
~In U A a -> Add U A a=B -> A=Subtract U B a.

Lemma EnsembleSubCardinal :
forall (U:Type) (A:Ensemble U) (a:U) (n:nat),
~In U A a -> cardinal U (Add U A a) (S n) -> cardinal U A n.

Theorem apply_func_finite :
forall (U1 U2:Type) (f:U1->U2) (A:Ensemble U1),
Finite U1 A -> Finite U2 (apply_func U1 U2 f A).

Inductive EnsembleReduction (U:Type) (f:Operation U)
(S:Ensemble U) (zero:U): U -> Prop :=
|EnsembleReduction_empty: S=Empty_set U ->
  EnsembleReduction U f S zero zero
|EnsembleReduction_add: forall (A:Ensemble U) (x rA:U),
  (EnsembleReduction U f A zero rA) -> ~ In U A x ->
  S=Add U A x -> EnsembleReduction U f S zero (f rA x).

Lemma EnsembleReductionExistence :
forall (U:Type) (f:Operation U) (S:Ensemble U) (zero:U),
Finite U S -> exists red:U,
 EnsembleReduction U f S zero red.

Theorem EnsembleReduction_unique :
forall (U:Type) (f:Operation U) (S:Ensemble U) (zero a b:U),
Associativity f -> Commutativity f-> Finite U S ->
EnsembleReduction U f S zero a ->
EnsembleReduction U f S zero b ->
a=b.

Inductive EnsembleApplyReduction (U1 U2:Type)
(f:U1->U2) (g:Operation U2)
(S:Ensemble U1) (zero:U2): U2 -> Prop :=
|EnsembleApplyReduction_empty: S=Empty_set U1 ->
  EnsembleApplyReduction U1 U2 f g S zero zero
|EnsembleApplyReduction_add:
  forall (A:Ensemble U1) (x:U1) (rA:U2),
  (EnsembleApplyReduction U1 U2 f g A zero rA) ->
  ~ In U1 A x -> S=Add U1 A x ->
  EnsembleApplyReduction U1 U2 f g S zero (g rA (f x)).

Lemma EnsembleApplyReductionExistence :
forall (U1 U2:Type) (f:U1->U2) (g:Operation U2)
(S:Ensemble U1) (zero:U2),
Finite U1 S -> exists red:U2,
 EnsembleApplyReduction U1 U2 f g S zero red.


End EnsembleFacts.