# Library Algebra.Parts

Set Implicit Arguments.
Unset Strict Implicit.
Require Export Sets.
Title "Parts of a set"
We define here the set of parts of a set, inclusion, union of a part,
"and we prove that there is no surjection from a set in its part set".
Section Subtype.
In Coq type theory, there is no primitive notion of subtype
Comments "Then we have to define such a notion".
Variable E : Setoid.
Variable F : Type.
Variable i : F E.
We have implicitely defined a subset of E which is the image of i .
Comments "As a setoid, this subset has" F
" as carrier, and we identify two elements of" F
"which have the same image by" i ":".

Definition subtype_image_equal (x y : F) : Prop := Equal (i x) (i y).

Lemma subtype_image_equiv : equivalence subtype_image_equal.
red in |- ×.
split; [ try assumption | idtac ].
red in |- ×.
unfold subtype_image_equal in |- *; unfold app_rel in |- *; simpl in |- *;
auto with algebra.
red in |- ×.
split; [ try assumption | idtac ].
red in |- ×.
unfold subtype_image_equal in |- *; unfold app_rel in |- *; simpl in |- *;
auto with algebra.
intros x y z H' H'0; try assumption.
apply Trans with (i y); auto with algebra.
red in |- ×.
unfold subtype_image_equal in |- *; unfold app_rel in |- *; simpl in |- *;
auto with algebra.
Qed.

Definition subtype_image_set : Setoid := Build_Setoid subtype_image_equiv.
End Subtype.
Section Part_type.
We define now a general structure for this kind of subset:
Parts of E will be nothing more than predicates on E which are compatible with equality:

Definition pred_compatible (P : E Prop) : Prop :=
x y : E, P x Equal y x (P y:Prop).

Record Predicate : Type :=
{Pred_fun : E Prop; Pred_compatible_prf : pred_compatible Pred_fun:Prop}.
Variable P : Predicate.
The type of elements of the subset defined by P is the following:

Record subtype : Type :=
{subtype_elt : E; subtype_prf : Pred_fun P subtype_elt:Prop}.
Then elements of subsets are composed of an element of E and a proof that they verify the predicate given by
Comments "We can now define the subset of" E "defined by the predicate" P ":".

Definition part :=
Build_subtype_image (subtype_image_carrier:=subtype) subtype_elt.
End Part_type.
We can see a subset as a set with these coercions:
Coercion set_of_subtype_image : subtype_image >-> Setoid.
Coercion part : Predicate >-> subtype_image.
We define x A) for elements of E :

Definition in_part (E : Setoid) (x : E) (A : Predicate E) := Pred_fun A x.
Section Part_set.
Variable E : Setoid.
The equality between parts of E :

Definition eq_part (A B : Predicate E) : Prop :=
x : E, (in_part x A in_part x B) (in_part x B in_part x A).

Let eq_part_equiv : equivalence eq_part.
red in |- ×.
split; [ try assumption | idtac ].
red in |- ×.
unfold eq_part, app_rel in |- *; simpl in |- ×.
intuition.
red in |- ×.
split; [ try assumption | idtac ].
red in |- ×.
unfold eq_part, app_rel in |- *; simpl in |- ×.
intros x y z H' H'0 x0; try assumption.
elim (H'0 x0); intros H'2 H'3; try exact H'2.
elim (H' x0); intros H'1 H'4; try exact H'1.
intuition.
red in |- ×.
unfold eq_part, app_rel in |- *; simpl in |- ×.
intros x y H' x0; try assumption.
elim (H' x0); intros H'2 H'3; try exact H'2.
intuition.
Qed.
We define the set E) of all parts of E , with its equality:
The empty part E) :
Hint Unfold pred_compatible: algebra.

Definition empty : part_set.
apply (Build_Predicate (E:=E) (Pred_fun:=fun x : EFalse)).
auto with algebra.
Defined.
And the full part:

Definition full : part_set.
apply (Build_Predicate (E:=E) (Pred_fun:=fun x : ETrue)).
auto with algebra.
Defined.
End Part_set.
Hint Unfold pred_compatible: algebra.
Section Inclusion.
Variable E : Setoid.
The relation of belonging is compatible with equality:

Lemma in_part_comp_l :
(A : part_set E) (x y : E), in_part x A Equal y x in_part y A.
intros A; try assumption.
exact (Pred_compatible_prf (E:=E) (p:=A)).
Qed.

Lemma in_part_comp_r :
(x : E) (A B : part_set E), in_part x A Equal A B in_part x B.
simpl in |- *; unfold eq_part in |- ×.
intros x A B H' H'0; try assumption.
elim (H'0 x).
intuition.
Qed.

Lemma empty_prop : x : E, ¬ in_part x (empty E).
unfold not in |- *; auto with algebra.
Qed.
Hint Resolve empty_prop: algebra.

Lemma full_prop : x : E, in_part x (full E).
unfold full in |- *; simpl in |- *; auto with algebra.
Qed.
Hint Resolve full_prop: algebra.

Definition full_to_set : MAP (full E) E.
apply (Build_Map (Ap:=fun x : full Efull E x)).
red in |- ×.
intros x y; try assumption.
elim x.
elim y.
simpl in |- ×.
unfold subtype_image_equal in |- ×.
simpl in |- *; auto with algebra.
Defined.

Definition set_to_full : MAP E (full E).
apply
(Build_Map (A:=E) (B:=full E)
(Ap:=fun x : E
Build_subtype (E:=E) (P:=full E) (subtype_elt:=x) (full_prop x))).
red in |- ×.
simpl in |- *; auto with algebra.
Defined.

Lemma set_full_set : Equal (comp_map_map full_to_set set_to_full) (Id E).
simpl in |- *; auto with algebra.
red in |- ×.
simpl in |- *; auto with algebra.
Qed.

Lemma full_set_full :
Equal (comp_map_map set_to_full full_to_set) (Id (full E)).
simpl in |- *; auto with algebra.
red in |- ×.
simpl in |- *; auto with algebra.
intros x; try assumption.
elim x.
simpl in |- *; auto with algebra.
intros subtype_elt' subtype_prf'; red in |- ×.
simpl in |- *; auto with algebra.
Qed.
The inclusion of parts:

Definition included (A B : part_set E) : Prop :=
x : E, in_part x A in_part x B.
The relation of inclusion is an order relation:

Lemma included_refl : A : part_set E, included A A.
simpl in |- *; unfold included in |- *; auto with algebra.
Qed.
Hint Resolve included_refl: algebra.

Lemma included_antisym :
A B : part_set E, included A B included B A Equal A B.
simpl in |- *; unfold eq_part, included in |- *; auto with algebra.
Qed.

Lemma included_trans :
A B C : part_set E, included A B included B C included A C.
simpl in |- *; unfold included in |- *; auto with algebra.
Qed.
The inclusion relation is compatible with equality:

Lemma included_comp :
A A' B B' : part_set E,
Equal A A' Equal B B' included A B included A' B'.
simpl in |- *; unfold eq_part, included in |- ×.
intros A A' B B' H' H'0 H'1 x H'2; try assumption.
elim (H'0 x); intros H'4 H'5; apply H'4.
lapply (H'1 x); [ intros H'6; apply H'6 | idtac ].
elim (H' x); intros H'6 H'7; apply H'7; auto with algebra.
Qed.

Lemma eq_part_included : A B : part_set E, Equal A B included A B.
simpl in |- *; unfold eq_part, included in |- ×.
intros A B H' x H'0; try assumption.
specialize 1H' with (x := x); rename H' into H'1; try exact H'1.
elim H'1; intros H'2 H'3; try exact H'2; clear H'1; auto with algebra.
Qed.
Hint Resolve eq_part_included: algebra.

Lemma empty_included : A : part_set E, included (empty E) A.
simpl in |- *; unfold included in |- *; auto with algebra.
intros A x H'; try assumption.
absurd (in_part x (empty E)); auto with algebra.
Qed.

Lemma full_included : A : part_set E, included A (full E).
simpl in |- *; unfold included in |- *; auto with algebra.
Qed.
Hint Resolve empty_included full_included: algebra.

Definition inj_part : A : part_set E, MAP A E.
intros A; try assumption.
apply (Build_Map (Ap:=fun x : Asubtype_elt x)).
red in |- ×.
auto with algebra.
Defined.

Lemma inj_part_injective : A : part_set E, injective (inj_part A).
intros A; try assumption.
red in |- ×.
auto with algebra.
Qed.

Definition inj_part_included :
A B : part_set E, included A B MAP A B.
intros A B H'; try assumption.
red in H'.
apply
(Build_Map (A:=A) (B:=B)
(Ap:=fun x : ABuild_subtype (H' (A x) (subtype_prf (E:=E) (P:=A) x)))).
red in |- ×.
simpl in |- *; auto with algebra.
Defined.

Lemma inj_part_included_prop :
(A B : part_set E) (p : included A B) (x : A),
Equal (B (inj_part_included p x)) (A x).
simpl in |- *; auto with algebra.
Qed.

Lemma inj_part_included_injective :
(A B : part_set E) (p : included A B),
injective (inj_part_included p).
intros A B p; red in |- ×.
intros x y; try assumption.
elim x.
elim y.
simpl in |- *; auto with algebra.
Qed.

Definition id_map_parts_equal : A B : part_set E, Equal A B MAP A B.
intros A B H'; try assumption.
exact (inj_part_included (eq_part_included H')).
Defined.

Lemma id_map_parts_equal_prop :
(A B : part_set E) (p : Equal A B) (x : A),
Equal (subtype_elt (id_map_parts_equal p x)) (subtype_elt x).
simpl in |- *; auto with algebra.
Qed.
End Inclusion.
Section Union_of_part.
Variable E : Setoid.
We define the union of a part of E)
Variable P : part_set (part_set E).

Definition union_part : part_set E.
apply
(Build_Predicate
(Pred_fun:=fun x : E A : part_set E, in_part A P in_part x A)).
red in |- ×.
intros x y H' H'0; try assumption.
elim H'; intros A E0; elim E0; clear H'.
intros H' H'1; try assumption.
A; split; [ try assumption | idtac ].
apply in_part_comp_l with x; auto with algebra.
Defined.

Lemma union_part_prop :
x : E,
in_part x union_part A : part_set E, in_part A P in_part x A.
intros x H'; red in H'; auto with algebra.
Qed.

Lemma union_part_prop_rev :
A : part_set E,
in_part A P x : E, in_part x A in_part x union_part.
unfold union_part in |- *; simpl in |- *; auto with algebra.
intros A H' x H'0; try assumption.
A; split; [ try assumption | idtac ].
auto with algebra.
Qed.

Lemma union_part_included :
A : part_set E, in_part A P included A union_part.
intros A H'; try assumption.
unfold included in |- *; auto with algebra.
intros x H'0; try assumption.
apply union_part_prop_rev with (A := A); auto with algebra.
Qed.

Lemma union_part_upper_bound :
Y : part_set E,
( A : part_set E, in_part A P included A Y)
included union_part Y.
intros Y H'; try assumption.
unfold included in |- ×.
intros x H'0; try assumption.
case (union_part_prop H'0).
intros A H'1; try assumption.
elim H'1.
intros H'2 H'3; try assumption.
unfold included in H'.
apply H' with (A := A); auto with algebra.
Qed.
End Union_of_part.
Section Part_set_greater.
A nice theorem:
Variable E : Setoid.
Variable f : MAP E (part_set E).
Hypothesis fsurj : surjective f.

Let X_def (x : E) : Prop := ¬ in_part x (f x).

Let X : part_set E.
apply (Build_Predicate (E:=E) (Pred_fun:=X_def)).
unfold X_def in |- ×.
red in |- ×.
unfold not in |- ×.
intros x y H' H'0 H'1; try assumption.
apply H'.
apply in_part_comp_l with y; auto with algebra.
apply in_part_comp_r with (Ap f y); auto with algebra.
Defined.

Let invX : x : E, Equal X (f x).
exact (fsurj X).
Qed.

Lemma not_inpart_comp_r :
(E : Setoid) (x : E) (A B : part_set E),
¬ in_part x A Equal A B ¬ in_part x B.
unfold not in |- ×.
intros E0 x A B H' H'0 H'1; try assumption.
apply H'.
apply in_part_comp_r with B; auto with algebra.
Qed.

Theorem part_set_is_strictly_greater_than_set1 : False.
case invX.
intros x H'; try assumption.
cut (¬ in_part x X).
intros H'0; try assumption.
absurd (in_part x X); auto with algebra.
simpl in |- ×.
unfold X_def in |- ×.
apply not_inpart_comp_r with X; auto with algebra.
unfold not in |- ×.
intros H'0; try assumption.
absurd (in_part x X); auto with algebra.
apply not_inpart_comp_r with (Ap f x); auto with algebra.
Qed.
End Part_set_greater.

Theorem part_set_is_strictly_greater_than_set :
(E : Setoid) (f : MAP E (part_set E)), ¬ surjective f.
exact part_set_is_strictly_greater_than_set1.
Qed.
Hint Unfold pred_compatible: algebra.
Hint Resolve empty_prop full_prop included_refl eq_part_included
empty_included full_included inj_part_injective inj_part_included_injective
id_map_parts_equal_prop union_part_included union_part_upper_bound
not_inpart_comp_r: algebra.