(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Sets.
(** Title "Parts of a set" *)
Comments
  "We define here the set of parts of a set, inclusion, union of a part,".
Comments
  "and we prove that there is no surjection from a set in its part set".
Section Subtype.
Comments "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.
Comments "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.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: and (@transitive (Predicate E) eq_part) (@symmetric (Predicate E) eq_part) *)
split; [ try assumption | idtac ].
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
unfold subtype_image_equal in |- *; unfold app_rel in |- *; simpl in |- *;
(* Goal: @in_part E x A *)
 auto with algebra.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: and (@transitive (Predicate E) eq_part) (@symmetric (Predicate E) eq_part) *)
split; [ try assumption | idtac ].
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
unfold subtype_image_equal in |- *; unfold app_rel in |- *; simpl in |- *;
(* Goal: @in_part E x A *)
 auto with algebra.
(* Goal: forall (x y z : F) (_ : @Equal E (i x) (i y)) (_ : @Equal E (i y) (i z)), @Equal E (i x) (i z) *)
(* Goal: @symmetric F subtype_image_equal *)
intros x y z H' H'0; try assumption.
(* Goal: @Equal E (i x) (i z) *)
(* Goal: @symmetric F subtype_image_equal *)
apply Trans with (i y); auto with algebra.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
unfold subtype_image_equal in |- *; unfold app_rel in |- *; simpl in |- *;
(* Goal: @in_part E x A *)
 auto with algebra.
Qed.

Definition subtype_image_set : Setoid := Build_Setoid subtype_image_equiv.
End Subtype.
Section Part_type.
Comments "We define now a general structure for this kind of subset:".
Variable E : Setoid.

Record subtype_image : Type := 
  {subtype_image_carrier : Type;
   subtype_image_inj :> subtype_image_carrier -> E}.

Definition set_of_subtype_image (S : subtype_image) :=
  subtype_image_set (subtype_image_inj (s:=S)).
Comments "Parts of" E "will be nothing more than predicates on" E
  " which are compatible with equality:".

Definition pred_compatible (P : E -> Prop) : Prop :=
  forall 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.
Comments "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}.
Comments "Then elements of subsets are composed of an element of" E
  "and a proof that they verify the predicate" "given by" P.
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.
Comments "We can see a subset as a set with these coercions:".
Coercion set_of_subtype_image : subtype_image >-> Setoid.
Coercion part : Predicate >-> subtype_image.
Comments "We define" (in_part 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.
Comments "The equality between parts of" E ":".

Definition eq_part (A B : Predicate E) : Prop :=
  forall 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.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: and (@transitive (Predicate E) eq_part) (@symmetric (Predicate E) eq_part) *)
split; [ try assumption | idtac ].
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: forall (x y : Predicate E) (_ : @app_rel (Predicate E) eq_part x y), @app_rel (Predicate E) eq_part y x *)
unfold eq_part, app_rel in |- *; simpl in |- *.
(* Goal: forall (_ : forall _ : @in_part E x A, @in_part E x B) (_ : forall _ : @in_part E x B, @in_part E x A), @in_part E x B *)
intuition.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: and (@transitive (Predicate E) eq_part) (@symmetric (Predicate E) eq_part) *)
split; [ try assumption | idtac ].
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: forall (x y : Predicate E) (_ : @app_rel (Predicate E) eq_part x y), @app_rel (Predicate E) eq_part y x *)
unfold eq_part, app_rel in |- *; simpl in |- *.
(* Goal: forall (x y z : Predicate E) (_ : forall x0 : Carrier E, and (forall _ : @in_part E x0 x, @in_part E x0 y) (forall _ : @in_part E x0 y, @in_part E x0 x)) (_ : forall x0 : Carrier E, and (forall _ : @in_part E x0 y, @in_part E x0 z) (forall _ : @in_part E x0 z, @in_part E x0 y)) (x0 : Carrier E), and (forall _ : @in_part E x0 x, @in_part E x0 z) (forall _ : @in_part E x0 z, @in_part E x0 x) *)
(* Goal: @symmetric (Predicate E) eq_part *)
intros x y z H' H'0 x0; try assumption.
(* Goal: and (forall _ : @in_part E x0 x, @in_part E x0 z) (forall _ : @in_part E x0 z, @in_part E x0 x) *)
(* Goal: @symmetric (Predicate E) eq_part *)
elim (H'0 x0); intros H'2 H'3; try exact H'2.
(* Goal: and (forall _ : @in_part E x0 x, @in_part E x0 z) (forall _ : @in_part E x0 z, @in_part E x0 x) *)
(* Goal: @symmetric (Predicate E) eq_part *)
elim (H' x0); intros H'1 H'4; try exact H'1.
(* Goal: forall (_ : forall _ : @in_part E x A, @in_part E x B) (_ : forall _ : @in_part E x B, @in_part E x A), @in_part E x B *)
intuition.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: forall (x y : Predicate E) (_ : @app_rel (Predicate E) eq_part x y), @app_rel (Predicate E) eq_part y x *)
unfold eq_part, app_rel in |- *; simpl in |- *.
(* Goal: forall (x y : Predicate E) (_ : forall x0 : Carrier E, and (forall _ : @in_part E x0 x, @in_part E x0 y) (forall _ : @in_part E x0 y, @in_part E x0 x)) (x0 : Carrier E), and (forall _ : @in_part E x0 y, @in_part E x0 x) (forall _ : @in_part E x0 x, @in_part E x0 y) *)
intros x y H' x0; try assumption.
(* Goal: and (forall _ : @in_part E x0 y, @in_part E x0 x) (forall _ : @in_part E x0 x, @in_part E x0 y) *)
elim (H' x0); intros H'2 H'3; try exact H'2.
(* Goal: forall (_ : forall _ : @in_part E x A, @in_part E x B) (_ : forall _ : @in_part E x B, @in_part E x A), @in_part E x B *)
intuition.
Qed.
Comments "We define the set" (part_set E) "of all parts of" E
  ", with its equality:".

Definition part_set : Setoid := Build_Setoid eq_part_equiv.
Comments "The empty part" (empty E) ":".
Hint Unfold pred_compatible: algebra.

Definition empty : part_set.
(* Goal: Carrier part_set *)
apply (Build_Predicate (E:=E) (Pred_fun:=fun x : E => False)).
(* Goal: @in_part E x A *)
auto with algebra.
Defined.
Comments "And the full part:".

Definition full : part_set.
(* Goal: Carrier part_set *)
apply (Build_Predicate (E:=E) (Pred_fun:=fun x : E => True)).
(* Goal: @in_part E x A *)
auto with algebra.
Defined.
End Part_set.
Hint Unfold pred_compatible: algebra.
Section Inclusion.
Variable E : Setoid.
Comments "The relation of belonging is compatible with equality:".

Lemma in_part_comp_l :
 forall (A : part_set E) (x y : E), in_part x A -> Equal y x -> in_part y A.
(* Goal: forall A : Carrier (part_set E), @injective (@set_of_subtype_image E (@part E A)) E (inj_part A) *)
intros A; try assumption.
(* Goal: forall (x y : Carrier E) (_ : @in_part E x A) (_ : @Equal E y x), @in_part E y A *)
exact (Pred_compatible_prf (E:=E) (p:=A)).
Qed.

Lemma in_part_comp_r :
 forall (x : E) (A B : part_set E), in_part x A -> Equal A B -> in_part x B.
(* Goal: forall (x : Carrier E) (A B : Carrier (part_set E)) (_ : @in_part E x A) (_ : @Equal (part_set E) A B), @in_part E x B *)
simpl in |- *; unfold eq_part in |- *.
(* Goal: forall (x : Carrier E) (A B : Predicate E) (_ : @in_part E x A) (_ : forall x0 : Carrier E, and (forall _ : @in_part E x0 A, @in_part E x0 B) (forall _ : @in_part E x0 B, @in_part E x0 A)), @in_part E x B *)
intros x A B H' H'0; try assumption.
(* Goal: @in_part E x B *)
elim (H'0 x).
(* Goal: forall (_ : forall _ : @in_part E x A, @in_part E x B) (_ : forall _ : @in_part E x B, @in_part E x A), @in_part E x B *)
intuition.
Qed.

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

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

Definition full_to_set : MAP (full E) E.
(* Goal: Carrier (MAP (@set_of_subtype_image E (@part E (full E))) E) *)
apply (Build_Map (Ap:=fun x : full E => full E x)).
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: forall (x y : Carrier (@set_of_subtype_image E (@part E A))) (_ : @Equal (@set_of_subtype_image E (@part E B)) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) x) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) y)), @Equal (@set_of_subtype_image E (@part E A)) x y *)
intros x y; try assumption.
(* Goal: forall _ : @Equal (@set_of_subtype_image E (@part E B)) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) x) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) y), @Equal (@set_of_subtype_image E (@part E A)) x y *)
elim x.
(* Goal: forall (subtype_elt : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt) (_ : @Equal (@set_of_subtype_image E (@part E B)) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) (@Build_subtype E A subtype_elt subtype_prf)) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) y)), @Equal (@set_of_subtype_image E (@part E A)) (@Build_subtype E A subtype_elt subtype_prf) y *)
elim y.
(* Goal: @in_part E x X *)
(* Goal: not (@in_part E x X) *)
simpl in |- *.
(* Goal: forall (subtype_elt0 : Carrier E) (subtype_prf : True) (subtype_elt1 : Carrier E) (subtype_prf0 : True) (_ : @subtype_image_equal E (@subtype E (full E)) (@subtype_elt E (full E)) (@Build_subtype E (full E) subtype_elt1 subtype_prf0) (@Build_subtype E (full E) subtype_elt0 subtype_prf)), @Equal E subtype_elt1 subtype_elt0 *)
unfold subtype_image_equal in |- *.
(* Goal: @in_part E x A *)
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))).
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: @in_part E x A *)
simpl in |- *; auto with algebra.
Defined.

Lemma set_full_set : Equal (comp_map_map full_to_set set_to_full) (Id E).
(* Goal: @in_part E x A *)
simpl in |- *; auto with algebra.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: @in_part E x A *)
simpl in |- *; auto with algebra.
Qed.

Lemma full_set_full :
 Equal (comp_map_map set_to_full full_to_set) (Id (full E)).
(* Goal: @in_part E x A *)
simpl in |- *; auto with algebra.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: @in_part E x A *)
simpl in |- *; auto with algebra.
(* Goal: forall x : @subtype E (full E), @subtype_image_equal E (@subtype E (full E)) (@subtype_elt E (full E)) (@Build_subtype E (full E) (@subtype_elt E (full E) x) (full_prop (@subtype_elt E (full E) x))) x *)
intros x; try assumption.
(* Goal: forall _ : @Equal (@set_of_subtype_image E (@part E B)) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) x) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) y), @Equal (@set_of_subtype_image E (@part E A)) x y *)
elim x.
(* Goal: @in_part E x A *)
simpl in |- *; auto with algebra.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
intros subtype_elt' subtype_prf'; red in |- *.
(* Goal: @in_part E x A *)
simpl in |- *; auto with algebra.
Qed.
Comments "The inclusion of parts:".

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

Lemma included_refl : forall A : part_set E, included A A.
(* Goal: @in_part E x A *)
simpl in |- *; unfold included in |- *; auto with algebra.
Qed.
Hint Resolve included_refl: algebra.

Lemma included_antisym :
 forall A B : part_set E, included A B -> included B A -> Equal A B.
(* Goal: @in_part E x A *)
simpl in |- *; unfold eq_part, included in |- *; auto with algebra.
Qed.

Lemma included_trans :
 forall A B C : part_set E, included A B -> included B C -> included A C.
(* Goal: @in_part E x A *)
simpl in |- *; unfold included in |- *; auto with algebra.
Qed.
Comments "The inclusion relation is compatible with equality:".

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

Lemma eq_part_included : forall A B : part_set E, Equal A B -> included A B.
(* Goal: forall (A B : Carrier (part_set E)) (_ : @Equal (part_set E) A B), included A B *)
simpl in |- *; unfold eq_part, included in |- *.
(* Goal: forall (A B : Predicate E) (_ : forall x : Carrier E, and (forall _ : @in_part E x A, @in_part E x B) (forall _ : @in_part E x B, @in_part E x A)) (x : Carrier E) (_ : @in_part E x A), @in_part E x B *)
intros A B H' x H'0; try assumption.
specialize  H' with (x := x); rename H' into H'1; try exact H'1.
(* Goal: @in_part E x A *)
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 : forall A : part_set E, included (empty E) A.
(* Goal: @in_part E x A *)
simpl in |- *; unfold included in |- *; auto with algebra.
(* Goal: forall (A : Predicate E) (x : Carrier E) (_ : @in_part E x (empty E)), @in_part E x A *)
intros A x H'; try assumption.
(* Goal: @in_part E x A *)
absurd (in_part x (empty E)); auto with algebra.
Qed.

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

Definition inj_part : forall A : part_set E, MAP A E.
(* Goal: forall A : Carrier (part_set E), @injective (@set_of_subtype_image E (@part E A)) E (inj_part A) *)
intros A; try assumption.
(* Goal: Carrier (MAP (@set_of_subtype_image E (@part E A)) E) *)
apply (Build_Map (Ap:=fun x : A => subtype_elt x)).
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: @in_part E x A *)
auto with algebra.
Defined.

Lemma inj_part_injective : forall A : part_set E, injective (inj_part A).
(* Goal: forall A : Carrier (part_set E), @injective (@set_of_subtype_image E (@part E A)) E (inj_part A) *)
intros A; try assumption.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: @in_part E x A *)
auto with algebra.
Qed.

Definition inj_part_included :
  forall A B : part_set E, included A B -> MAP A B.
(* Goal: forall (A B : Carrier (part_set E)) (_ : @Equal (part_set E) A B), Carrier (MAP (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B))) *)
intros A B H'; try assumption.
(* Goal: Carrier (MAP (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B))) *)
red in H'.
apply
 (Build_Map (A:=A) (B:=B)
    (Ap:=fun x : A => Build_subtype (H' (A x) (subtype_prf (E:=E) (P:=A) x)))).
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: @in_part E x A *)
simpl in |- *; auto with algebra.
Defined.

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

Lemma inj_part_included_injective :
 forall (A B : part_set E) (p : included A B),
 injective (inj_part_included p).
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
intros A B p; red in |- *.
(* Goal: forall (x y : Carrier (@set_of_subtype_image E (@part E A))) (_ : @Equal (@set_of_subtype_image E (@part E B)) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) x) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) y)), @Equal (@set_of_subtype_image E (@part E A)) x y *)
intros x y; try assumption.
(* Goal: forall _ : @Equal (@set_of_subtype_image E (@part E B)) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) x) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) y), @Equal (@set_of_subtype_image E (@part E A)) x y *)
elim x.
(* Goal: forall (subtype_elt : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt) (_ : @Equal (@set_of_subtype_image E (@part E B)) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) (@Build_subtype E A subtype_elt subtype_prf)) (@Ap (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B)) (@inj_part_included A B p) y)), @Equal (@set_of_subtype_image E (@part E A)) (@Build_subtype E A subtype_elt subtype_prf) y *)
elim y.
(* Goal: @in_part E x A *)
simpl in |- *; auto with algebra.
Qed.

Definition id_map_parts_equal : forall A B : part_set E, Equal A B -> MAP A B.
(* Goal: forall (A B : Carrier (part_set E)) (_ : @Equal (part_set E) A B), Carrier (MAP (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B))) *)
intros A B H'; try assumption.
(* Goal: Carrier (MAP (@set_of_subtype_image E (@part E A)) (@set_of_subtype_image E (@part E B))) *)
exact (inj_part_included (eq_part_included H')).
Defined.

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

Definition union_part : part_set E.
apply
 (Build_Predicate
    (Pred_fun:=fun x : E => exists A : part_set E, in_part A P /\ in_part x A)).
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: forall (x y : Carrier E) (_ : @ex (Carrier (part_set E)) (fun A : Carrier (part_set E) => and (@in_part (part_set E) A P) (@in_part E x A))) (_ : @Equal E y x), @ex (Carrier (part_set E)) (fun A : Carrier (part_set E) => and (@in_part (part_set E) A P) (@in_part E y A)) *)
intros x y H' H'0; try assumption.
(* Goal: @ex (Carrier (part_set E)) (fun A : Carrier (part_set E) => and (@in_part (part_set E) A P) (@in_part E y A)) *)
elim H'; intros A E0; elim E0; clear H'.
(* Goal: forall (_ : @in_part (part_set E) A P) (_ : @in_part E x A), @ex (Carrier (part_set E)) (fun A : Carrier (part_set E) => and (@in_part (part_set E) A P) (@in_part E y A)) *)
intros H' H'1; try assumption.
(* Goal: and (@transitive (Predicate E) eq_part) (@symmetric (Predicate E) eq_part) *)
exists A; split; [ try assumption | idtac ].
(* Goal: @in_part E x A *)
apply in_part_comp_l with x; auto with algebra.
Defined.

Lemma union_part_prop :
 forall x : E,
 in_part x union_part -> exists A : part_set E, in_part A P /\ in_part x A.
(* Goal: @in_part E x A *)
intros x H'; red in H'; auto with algebra.
Qed.

Lemma union_part_prop_rev :
 forall A : part_set E,
 in_part A P -> forall x : E, in_part x A -> in_part x union_part.
(* Goal: @in_part E x A *)
unfold union_part in |- *; simpl in |- *; auto with algebra.
(* Goal: forall (A : Predicate E) (_ : @in_part (part_set E) A P) (x : Carrier E) (_ : @in_part E x A), @ex (Predicate E) (fun A0 : Predicate E => and (@in_part (part_set E) A0 P) (@in_part E x A0)) *)
intros A H' x H'0; try assumption.
(* Goal: and (@transitive (Predicate E) eq_part) (@symmetric (Predicate E) eq_part) *)
exists A; split; [ try assumption | idtac ].
(* Goal: @in_part E x A *)
auto with algebra.
Qed.

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

Lemma union_part_upper_bound :
 forall Y : part_set E,
 (forall A : part_set E, in_part A P -> included A Y) ->
 included union_part Y.
(* Goal: forall (Y : Carrier (part_set E)) (_ : forall (A : Carrier (part_set E)) (_ : @in_part (part_set E) A P), @included E A Y), @included E union_part Y *)
intros Y H'; try assumption.
(* Goal: @included E union_part Y *)
unfold included in |- *.
(* Goal: forall (x : Carrier E) (_ : @in_part E x union_part), @in_part E x Y *)
intros x H'0; try assumption.
(* Goal: @in_part E x Y *)
case (union_part_prop H'0).
(* Goal: forall (x0 : Carrier (part_set E)) (_ : and (@in_part (part_set E) x0 P) (@in_part E x x0)), @in_part E x Y *)
intros A H'1; try assumption.
(* Goal: @in_part E x Y *)
elim H'1.
(* Goal: forall (_ : @in_part (part_set E) A P) (_ : @in_part E x A), @in_part E x Y *)
intros H'2 H'3; try assumption.
(* Goal: @in_part E x Y *)
unfold included in H'.
(* Goal: @in_part E x A *)
apply H' with (A := A); auto with algebra.
Qed.
End Union_of_part.
Section Part_set_greater.
Comments "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.
(* Goal: Carrier (part_set E) *)
apply (Build_Predicate (E:=E) (Pred_fun:=X_def)).
(* Goal: X_def x *)
(* Goal: not (@in_part E x X) *)
unfold X_def in |- *.
(* Goal: @pred_compatible E (fun x : Carrier E => not (@in_part E x (@Ap E (part_set E) f x))) *)
red in |- *.
(* Goal: not (@in_part E x X) *)
unfold not in |- *.
(* Goal: forall (x y : Carrier E) (_ : forall _ : @in_part E x (@Ap E (part_set E) f x), False) (_ : @Equal E y x) (_ : @in_part E y (@Ap E (part_set E) f y)), False *)
intros x y H' H'0 H'1; try assumption.
(* Goal: False *)
apply H'.
(* Goal: @in_part E x A *)
apply in_part_comp_l with y; auto with algebra.
(* Goal: @in_part E x A *)
apply in_part_comp_r with (Ap f y); auto with algebra.
Defined.

Let invX : exists x : E, Equal X (f x).
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal (part_set E) X (@Ap E (part_set E) f x)) *)
exact (fsurj X).
Qed.

Lemma not_inpart_comp_r :
 forall (E : Setoid) (x : E) (A B : part_set E),
 ~ in_part x A -> Equal A B -> ~ in_part x B.
(* Goal: not (@in_part E x X) *)
unfold not in |- *.
(* Goal: forall (E : Setoid) (x : Carrier E) (A B : Carrier (part_set E)) (_ : forall _ : @in_part E x A, False) (_ : @Equal (part_set E) A B) (_ : @in_part E x B), False *)
intros E0 x A B H' H'0 H'1; try assumption.
(* Goal: False *)
apply H'.
(* Goal: @in_part E x A *)
apply in_part_comp_r with B; auto with algebra.
Qed.

Theorem part_set_is_strictly_greater_than_set1 : False.
(* Goal: False *)
case invX.
(* Goal: forall (x : Carrier E) (_ : @Equal (part_set E) X (@Ap E (part_set E) f x)), False *)
intros x H'; try assumption.
(* Goal: False *)
cut (~ in_part x X).
(* Goal: forall _ : @in_part E x X, False *)
intros H'0; try assumption.
(* Goal: @in_part E x A *)
absurd (in_part x X); auto with algebra.
(* Goal: @in_part E x X *)
(* Goal: not (@in_part E x X) *)
simpl in |- *.
(* Goal: X_def x *)
(* Goal: not (@in_part E x X) *)
unfold X_def in |- *.
(* Goal: @in_part E x A *)
apply not_inpart_comp_r with X; auto with algebra.
(* Goal: not (@in_part E x X) *)
unfold not in |- *.
(* Goal: forall _ : @in_part E x X, False *)
intros H'0; try assumption.
(* Goal: @in_part E x A *)
absurd (in_part x X); auto with algebra.
(* Goal: @in_part E x A *)
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 :
 forall (E : Setoid) (f : MAP E (part_set E)), ~ surjective f.
(* Goal: forall (E : Setoid) (f : Carrier (MAP E (part_set E))), not (@surjective E (part_set E) 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.