(** * Fundamental set theory
Original file by Carlos Simpson 

Changes: R and Z renamed to Re and Zo
E renamed to Bset 
B Y X renamed to Bo Yo Xo

Defines following one letter symbols:  J P Q L V W 
*)

Set Implicit Arguments.
Require Export Arith. 


(** ** Axioms *)
Module Axioms.

Definition Bset:=Type.

(** Realisation: if x is a set, maps an  object of type x to a set *)

Unset Strict Implicit.
Parameter Ro : forall x : Bset, x -> Bset.
Set Strict Implicit.

(** Injectivity of [Ro] *)

Axiom R_inj : forall (x : Bset) (a b : x), Ro a = Ro b -> a = b.

(** Defines is_element_of and is_subset_of *)

Definition inc (x y : Bset) := exists a : y, Ro a = x.
Definition sub (a b : Bset) := forall x : Bset, inc x a -> inc x b.

(** extensionality for sets *)

Axiom extensionality : forall a b : Bset, sub a b -> sub b a -> a = b.

(** extensionality for products *)

Axiom prod_extensionality :
  forall (x : Type) (y : x -> Type) (u v : forall a : x, y a),
    (forall a : x, u a = v a) -> u = v.

Lemma arrow_extensionality :
  forall (x y : Type) (u v : x -> y), (forall a : x, u a = v a) -> u = v.
Proof.  intros x y.
  change  (forall u v : forall a : x, (fun _ : x => y) a,
      (forall a : x, u a = v a) -> u = v).
  intros.  apply prod_extensionality; assumption.
Qed. 

(** nonempty: type is populated, or set has an element *) 

Inductive nonemptyT (t : Type) : Prop :=
    nonemptyT_intro : t -> nonemptyT t.
Inductive nonempty (x : Bset) : Prop :=
    nonempty_intro : forall y : Bset, inc y x -> nonempty x.

(** Axiom of choice: let [t] be a nonempty type, [p] a predicated on [t].
 If [p] is true for some object it is for  [(chooseT p ne)] *)

Parameter chooseT : forall (t : Type) (p : t -> Prop)(q:nonemptyT t),  t.

Axiom chooseT_pr :
  forall (t : Type) (p : t -> Prop) (ne : nonemptyT t),
    ex p -> p (chooseT p ne).

(** Image: if [f:x->Bset] is an abstraction, the [IM f] is a set,
   it contains [y] if and only if [y] is [f z] for some [z:x] *)

Parameter IM : forall x : Bset, (x -> Bset) -> Bset.

Axiom IM_exists :
          forall (x : Bset) (f : x -> Bset) (y : Bset),
          inc y (IM f) -> exists a : x, f a = y.
Axiom IM_inc :
          forall (x : Bset) (f : x -> Bset) (y : Bset),
          (exists a : x, f a = y) -> inc y (IM f). 


(** Excluded middle and consequences *)

Axiom excluded_middle : forall P : Prop, ~ ~ P -> P.
Axiom proof_irrelevance : forall (P : Prop) (q p : P), p = q.
Axiom iff_eq : forall P Q : Prop, (P -> Q) -> (Q -> P) -> P = Q.

Lemma excluded_middle':forall A B:Prop, (~ B->A)->(~A->B).
  intros a b H c. apply excluded_middle. auto. Qed.

Lemma p_or_not_p : forall P : Prop, P \/ ~ P.
Proof. intros. apply excluded_middle. intro. apply H.  
  assert P. apply excluded_middle. unfold not. intros. apply H. 
  right; assumption.
  left ; assumption. Qed.


(** Roalisation of nat as ordinals *)

Axiom nat_realization_O : forall x : Bset, ~ inc x (Ro 0). 
Axiom nat_realization_S :
          forall (n : nat) (x : Bset),
          inc x (Ro (S n)) = (inc x (Ro n) \/ x = Ro n). 


(** Roalisation of Prop and True *)
Axiom prop_realization : forall x : Prop, Ro x = x.

Axiom true_proof_realization_empty : forall t : True, Ro t = Ro 0.
End Axioms.
Export Axioms.

(** ** Tactics *)
Module Tactics1.



(** Shorthands, for instance [E3 = E -> E -> E -> E] *)
Notation EE := (Bset -> Bset).
Notation EEE := (Bset -> EE).
Notation EP := (Bset -> Prop).
Notation EEP := (Bset -> EP).

Infix "&":= and (right associativity, at level 100).


Definition type_of (T : Type) (t : T) := T.


Lemma seq_deconj : forall P Q : Prop, P -> (P -> Q) -> (P & Q). 
  intros P Q p H. split ; [idtac | apply H]; assumption. Qed. 


Lemma uneq : forall (f:EE) x y,
  x = y -> f x = f y.
Proof. intros f x y H. rewrite H. trivial. Qed. 


Lemma forup : forall A B (f g:A -> B) (a b : A),
  f = g -> a = b -> f a = g b.
Proof.  intros T1 T2 f g a b H1 H2. rewrite H2; rewrite H1; trivial. Qed. 

Ltac ir := intros.
Ltac rw u := rewrite u.
Ltac rwi u h := rewrite u in h.
Ltac wr u := rewrite <- u.
Ltac wri u h := rewrite <- u in h.
Ltac ap h := apply h.
Ltac om := omega.
Ltac am := assumption.
Ltac tv := trivial.
Ltac eau := eauto.
Ltac sy := symmetry.
Ltac uf u := unfold u.
Ltac ufi u h := unfold u in h.
Ltac nin h := induction h.
Ltac uh a := red in a.


Ltac app u := (ap u; try tv; try am).
Ltac rww u := (rw u; try tv; try am).
Ltac rwii u h:= (rwi u h; try tv; try am).
Ltac wrr u := (wr u; try tv; try am). 
Ltac aw := autorewrite with aw; try tv; try am. 

Ltac au := first [ solve [am] | auto ].

Ltac set_extens:= app extensionality; unfold sub; intros.

Ltac EasyDeconj :=
  match goal with
  |  |- (_ & _) => ap conj; [ EasyDeconj | EasyDeconj ]
  |  |- (and _ _) => ap conj; [ EasyDeconj | EasyDeconj ]
  |  |- (_ /\ _) => ap conj; [ EasyDeconj | EasyDeconj ]
  |  |- _ => idtac
  end.


Ltac EasyExpand :=
  match goal with
  | id1:(?X1 /\ ?X2) |- _ => nin id1; EasyExpand
  |  |- _ => EasyDeconj
  end.


Ltac ee := EasyExpand.

Ltac Remind u :=
  set (recalx := u);
   match goal with
   | recalx:?X1 |- _ => assert X1; [ exact recalx | clear recalx ]
   end.

Ltac cp := Remind. 

End Tactics1.
Export Tactics1.

(** ** Constructions *)

Module Constructions.

(** This definition is rarely used *)

Definition exists_unique t (p : t->Prop) :=
  (ex p) & (forall x y : t, p x -> p y -> x = y).


(** Defines [neq] as different, and [strict_sub] as strict subset *)
Definition neq (x y : Bset) := x <> y.
Definition strict_sub (a b : Bset) :=  (neq a b) & (sub a b).
Definition elt x y := inc y x.


Lemma sub_trans : forall a b c, sub a b -> sub b c -> sub a c.
Proof. unfold sub; auto. Qed.

Lemma sub_refl : forall x, sub x x. 
Proof. unfold sub; auto. Qed. 

Lemma strict_sub_trans1 :
  forall a b c, strict_sub a b -> sub b c -> strict_sub a c.
Proof. unfold strict_sub; unfold neq. ir. nin H. split. red. ir. ap H.
  wri H2 H0. app extensionality. apply sub_trans with b; am.
Qed.

Lemma strict_sub_trans2 :
 forall a b c, sub a b -> strict_sub b c -> strict_sub a c.
Proof. unfold strict_sub; unfold neq. ir. nin H0. split.  red. ir. ap H0.
  rwi H2 H. app extensionality. apply sub_trans with b; am. 
Qed.


(** Emptyset is a type without constructor; empty is classical *)

Definition empty (x : Bset) := forall y : Bset, ~ inc y x. 
Inductive emptyset : Bset :=.

(** Basic property of Ro*)
Lemma R_inc : forall (x : Bset) (a : x), inc (Ro a) x.
Proof. ir. uf inc. exists a; tv.
Qed.

(** Equivalence between [nonempty] and [~ empty] *)
Lemma inc_nonempty : forall x y, inc x y -> nonemptyT y.
Proof. uf inc. ir. destruct H as [H _]. app nonemptyT_intro. 
Qed.

Lemma nonemptyT_not_empty : forall x, nonemptyT x -> ~ empty x.
Proof. ir. nin H. unfold not. ir. unfold empty in H. apply H with (Ro X).
  apply R_inc. 
Qed.


(** Axiom of choice applied to [inc x y], and the property [P a]
 that says realisation of [a] is [x]. This gives a partial inverse of [Ro]
and more properties of the emptyset *)
Definition Bo (x y : Bset) (hyp : inc x y) :=
  chooseT (fun a : y => Ro a = x) (inc_nonempty hyp).

Lemma B_eq : forall x y (hyp : inc x y), Ro (Bo hyp) = x.
Proof. unfold inc; unfold Bo. ir. app chooseT_pr.  
Qed.

Lemma B_back : forall (x:Bset) (y:x) (hyp : inc (Ro y) x), Bo hyp = y.
Proof. ir. ap R_inj. ap B_eq. Qed.

Lemma not_empty_nonemptyT : forall x , ~ empty x -> nonemptyT x.
Proof. intro. ap excluded_middle'. ir. red.  intros y H0. ap H. 
  ap nonemptyT_intro. exact (Bo H0). 
Qed. 

Lemma emptyset_empty : forall x, ~ inc x emptyset.
Proof. intros x H. assert (e:= Bo H). elim e. Qed.

Lemma exT_exists : forall p : EP, (exists x : Bset, p x) -> ex p.
Proof. ir. nin H. exists x; am. Qed.

(** Let [T] be a type, [P] a proposition, [a] a function that maps a proof
   of [P] into [T] and [b] a function that maps a proof of [~P] into [T].
   Let [q x] the property that [a p =x] and [b q = x]. We show that there 
   exists [x] with this property  *)
Definition by_cases_pr (T : Type) (P : Prop) (a : P -> T) 
  (b : ~ P -> T) (x : T) :=
   (forall p : P, a p = x) & (forall q : ~ P, b q = x).


Lemma by_cases_exists :
  forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T),
    exists x : T, by_cases_pr a b x.
Proof. ir. assert (H: P \/ ~ P). app p_or_not_p. nin H.
  exists (a H). red. split. ir. assert (p=H). ap proof_irrelevance. rww H0.
  ir. assert (e:=q H); elim e.  
  exists (b H). red. split. ir. assert (e:= H p); elim e. 
  ir. assert (H = q). ap proof_irrelevance. rww H0. 
Qed.

Lemma by_cases_nonempty :
 forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T), nonemptyT T.
Proof. ir. assert (P \/ ~ P). ap p_or_not_p. nin H; ap nonemptyT_intro. 
  app a. app b. 
Qed.

(** We can apply the axiom of choice. We have 4 lemmas: fundamental
property, uniqueness, case where P is true, case where P is false. *)

Definition by_cases (T : Type) (P : Prop) (a : P -> T)  (b : ~ P -> T) :=
  chooseT (fun x : T => by_cases_pr a b x) (by_cases_nonempty a b).


Lemma by_cases_property :
 forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T),
 by_cases_pr a b (by_cases a b).
Proof. ir. set (H:=  (by_cases_exists a b)).
  set (H1:=(by_cases_nonempty a b)).
  set (H2:=(chooseT_pr H1 H)).
  unfold by_cases.
  assert  (by_cases_nonempty a b = H1). apply proof_irrelevance.
  rewrite H0. apply H2. 
Qed.


Lemma by_cases_unique :
  forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (x : T),
    by_cases_pr a b x -> by_cases a b = x.
Proof. ir.  red in H.  destruct H as [PT PF].
  set (H1:= (by_cases_property a b)).  unfold by_cases_pr in H1. 
  destruct H1 as [APT APF].
  assert  (P \/ ~ P). apply p_or_not_p. induction H.
  rewrite <- APT with H; auto. rewrite <- APF with H;  auto. 
Qed.


Lemma by_cases_if :
  forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (p : P),
    by_cases a b = a p.
Proof. ir. ap by_cases_unique. red. split. ir. 
  assert (p0=p). apply proof_irrelevance. rww H.  ir; elim q; tv. 
Qed.

Lemma by_cases_if_not :
  forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (q : ~ P),
    by_cases a b = b q.
Proof. ir. ap by_cases_unique. red. split.
  intro p; elim q; auto.
  ir. assert (q0=q). ap proof_irrelevance. rww H. Qed.

(** Constructs q from p, such that, if p is true for some value, then q is p,
 otherwise, [q x] is [x=emptyset]. Two lemmas that restate this, 
 and another that says taht theres exists at least one x with [q x] *)
Definition refined_pr (p:EP) (x:Bset) :=
  (ex p -> p x) & ~(ex p) -> x = emptyset.


Lemma refined_pr_if : forall p x, ex p -> refined_pr p x = p x.
Proof. ir. unfold refined_pr. ap iff_eq; ir. 
  destruct H0. auto. split; [idtac | intro; destruct H1]; auto.  Qed.


Lemma refined_pr_not : forall p x,
  ~(ex p) -> refined_pr p x = (x = emptyset).
Proof. ir. unfold refined_pr. ap iff_eq; ir.
  destruct H0; auto. split; [intro; destruct H | idtac]; auto.
Qed. 

Lemma exists_refined_pr : forall p, ex (refined_pr p). 
Proof.  ir. apply by_cases with (ex p); ir.
  elim H; intros x Hx. exists x.  rww refined_pr_if. 
  exists emptyset. rww refined_pr_not. 
Qed.

(** Genereralised axiom of choice. [choose p] is satisfied by [p]
   if somebody satisfies p, is the emptyset otherwise *)
Definition choose' : EP -> Bset
  := fun X:EP => chooseT X (nonemptyT_intro Prop).

Lemma choose'_pr : forall p : EP, ex p -> p (choose' p).
Proof. ir. unfold choose'. app chooseT_pr. Qed.

Definition choose (p:EP) := choose' (refined_pr p).

Lemma choose_pr : forall p, ex p -> p (choose p).
Proof. ir. unfold choose. set (H1:=exists_refined_pr p).
  assert (refined_pr p (choose' (refined_pr p))). app choose'_pr. 
  destruct H0 as [HT HF].  app HT. 
Qed.

Lemma choose_not : forall p, ~(ex p) -> choose p = emptyset.
Proof. ir. unfold choose. assert (W:=(exists_refined_pr p)).
  assert (refined_pr p (choose' (refined_pr p))). app choose'_pr. 
  destruct H0 as [HT HF]. app HF.
Qed.

(** Axiom of choice applied to [inc]. If [x] not empty, [rep x] is in [x]  *)
Definition rep (x : Bset) := choose (fun y : Bset => inc y x). 

Lemma nonempty_rep : forall x, nonempty x -> inc (rep x) x. 
Proof. ir. unfold rep. ap choose_pr. induction H. exists y. am.
Qed. 

(** compares: forall x, p(x) false, and the existence of p(x) *)

Lemma exists_proof : forall p : EP, ~ (forall x : Bset, ~ p x) -> ex p.
Proof. intro. ap excluded_middle'. intros H x H0. 
  apply H. exists x. assumption. Qed.

Lemma not_exists_pr : forall p : EP, ~ ex p <-> (forall x : Bset, ~ p x).
Proof. ir. split; ir; intro H1. apply H. exists x; am. 
  induction H1. apply H with x; am. Qed.

(** Defines [Y P x y] to b x if P is true and y otherwise *)

Definition Yo : Prop -> EEE :=
  fun P x y => by_cases (fun _ : P => x) (fun _ : ~ P => y).
    

Lemma Y_if : forall (P : Prop) (hyp : P) x y z, x = z -> Yo P x y = z.
Proof. ir. unfold Yo. set (a := fun p:P => x); set (b := fun p: ~ P => y). 
  assert (z= a hyp). auto. rewrite H0. ap by_cases_if. Qed.


Lemma Y_if_not :
  forall (P : Prop) (hyp : ~ P) x y z, y = z -> Yo P x z = y.
Proof. ir. unfold Yo. set (a := fun p:P => x); set (b := fun p : ~ P => z).
  assert (y = b hyp); auto. rewrite H0. apply by_cases_if_not. 
Qed.

Lemma Y_if_rw : forall (P:Prop) (hyp :P) x y, Yo P x y = x.
Proof. intros. apply Y_if; auto.  Qed. 

Lemma Y_if_not_rw : forall (P:Prop) (hyp : ~P) x y, Yo P x y = y.
Proof.  intros. apply Y_if_not; auto.  Qed. 

(** Given a function f, [Zorec] remembers  a and f(a) *)
Record Zorec (x : Bset) (f : x -> Bset) : Bset :=  
   {Zohead : x; Zotail : f Zohead}.


(**
[Zo x p] is the image of some function [g]; this means that [inc y (Zo x p)] 
if and anly if  [y = g t] for some [t]; [t] is a record, say it remembers [a], 
of type [x], and [p (Ro a)];  [g(t)] is [Ro a]. Thus [inc y x] and [p y]; 
The converse is true.  *)

Definition Zo  := fun (x:Bset) (p:EP) 
  => let P := Zorec (fun a : x => p (Ro a)) in IM (fun t : P => Ro (Zohead t)).

Lemma Z_inc :
  forall (x : Bset) (p : EP) (y : Bset), inc y x -> p y -> inc y (Zo x p).
Proof. ir. unfold Zo. ap IM_inc. ufi inc H. induction H.
  assert (p (Ro x0)). rww H. 
  pose (Build_Zorec (fun a : x => p (Ro a)) x0 H1). exists z. trivial.
Qed.

Lemma Z_sub : forall x p, sub (Zo x p) x.
Proof. unfold sub. ir. pose (IM_exists H). nin e. wr H0. apply R_inc. Qed.

Lemma Z_pr : forall x p y, inc y (Zo x p) -> p y.
Proof.  unfold inc; unfold Zo. ir. induction H.
  pose (R_inc x0). pose (IM_exists i).  induction e. pose (Zotail x1).
  rwi H0 p0. rwi H0 p0. wrr H. Qed.

Lemma Z_all : forall x p y, inc y (Zo x p) -> (inc y x & p y).
Proof. ir. assert (sub (Zo x p) x). ap Z_sub.
  split. app H0. set (Z_pr H); auto. Qed.

Ltac Ztac :=
  match goal with
  | id1:(inc ?X1 (Zo _ _)) |- _ => pose (Z_all id1); ee
  |  |- (inc _ (Zo _ _)) => ap Z_inc; au
  | _ => idtac
  end.

Definition Yy : forall P : Prop, (P -> Bset) -> EE :=
  fun P f x => by_cases f (fun _ : ~ P => x).

Lemma Yy_if :
 forall (P : Prop) (hyp : P) (f : P -> Bset) x z, f hyp = z -> Yy f x = z. 
Proof. ir. unfold Yy. set (b := fun _ : ~ P => x). 
  rewrite <- H. apply by_cases_if. Qed. 

Lemma Yy_if_not :
  forall (P : Prop) (hyp : ~ P) (f : P -> Bset) (x z : Bset), x = z -> Yy f x = z. 
Proof. ir. unfold Yy.  set (b := fun _ : ~ P => x).
  assert (z= b hyp). unfold b. auto. rw H0. ap by_cases_if_not. Qed.

(** Defines [X f y], where f is defined for objects of type x as: f(z) 
if [inc y x], and z expresses this, the emptyset otherwise  *)

Definition Xo (x : Bset) (f : x -> Bset) (y : Bset) :=
  Yy (fun hyp : inc y x => f (Bo hyp)) emptyset. 

Lemma X_eq :
  forall (x : Bset) (f : x -> Bset) (y z : Bset),
    (exists a : x,  (Ro a = y) & (f a = z)) -> Xo f y = z. 
Proof. ir.  induction H. unfold Xo. destruct H. symmetry in H.
  assert (inc y x). rw H. apply R_inc. 
  apply Yy_if with H1. assert (Bo H1 = x0). apply R_inj. rww B_eq. rww H2.
Qed. 

Lemma X_rewrite : forall (x : Bset) (f : x -> Bset) (a : x), Xo f (Ro a) = f a. 
Proof. ir. apply X_eq. exists a. auto. Qed. 

(** Set of all elements of x satisfying p *)
Definition cut (x : Bset) (p : x -> Prop) :=
  Zo x (fun y : Bset => forall hyp : inc y x, p (Bo hyp)). 

Lemma cut_sub : forall (x : Bset) (p : x -> Prop), sub (cut p) x. 
Proof.  ir. unfold cut. apply Z_sub. Qed.


Definition cut_to (x : Bset) (p : x -> Prop) (y : cut p) :=
  Bo (cut_sub (p:=p) (R_inc y)). 

Lemma cut_to_R_eq :
 forall (x : Bset) (p : x -> Prop) (y : cut p), Ro (cut_to y) = Ro y. 
Proof. ir. unfold cut_to. rww B_eq. Qed. 

Lemma cut_pr : forall (x : Bset) (p : x -> Prop) (y : cut p), p (cut_to y).
Proof. ir. unfold cut_to. ufi cut y. 
  set (k := fun y : Bset => forall hyp : inc y x, p (Bo hyp)) in y. 
  pose (R_inc y). pose (Z_all i). induction a. apply H0.
Qed. 

Lemma cut_inc :
 forall (x : Bset) (p : x -> Prop) (y : x), p y -> inc (Ro y) (cut p). 
Proof. ir. unfold cut. ap Z_inc. ap R_inc.
  ir. assert (Bo hyp = y). ap R_inj. ap B_eq. rww H0.
Qed. 

(** If x is in the image of f, chooses y with f(y)=x *)
Definition IM_lift : forall (a : Bset) (f : a -> Bset), IM f -> a. 
ir. assert (exists x : a, f x = Ro X). ap IM_exists. ap R_inc. 
assert (nonemptyT a). induction H. app nonemptyT_intro.
exact (chooseT (fun x : a => f x = Ro X) H0). 
Defined. 


Lemma IM_lift_pr :
  forall (a : Bset) (f : a -> Bset) (x : IM f), f (IM_lift x) = Ro x. 
Proof. ir. assert (exists y : a, f y = Ro x). ap IM_exists. 
  ap R_inc. unfold IM_lift. set
  (K :=
   ex_ind (fun (x0 : a) (_ : (fun u : a => f u = Ro x) x0) => nonemptyT_intro x0)
     (IM_exists (R_inc x))). 
  pose (chooseT_pr K H). assumption. 
Qed. 


End Constructions.

Export Constructions.


(** ** Little*)
Module Little.


(** singleton: image of a set with one point *) 
Inductive one_point : Bset :=
    one_point_intro : one_point.

Definition singleton (x : Bset) := IM (fun p : one_point => x).

Lemma singleton_inc : forall x, inc x (singleton x).
Proof. ir. unfold singleton. ap IM_inc. exists one_point_intro. tv. Qed.

Hint Resolve sub_refl singleton_inc: fprops.
Ltac fprops := auto with fprops.

Lemma singleton_eq : forall x y, inc y (singleton x) -> y = x.
Proof. ir. pose (IM_exists H). elim e. sy. tv. Qed.

Lemma singleton_inj : forall x y, singleton x = singleton y -> x = y. 
Proof. ir. assert (inc x (singleton y)). wr H. fprops. app singleton_eq. Qed.

Lemma nonempty_singleton: forall x, nonempty (singleton x).
Proof. ir. exists x. fprops.
Qed.

(** doubleton: image of a set with two points *) 

Inductive two_points : Bset :=
  | two_points_a | two_points_b.

Lemma two_points_pr: forall x,
  inc x two_points = (x= Ro two_points_a \/ x = Ro two_points_b).
Proof. ir. app iff_eq. ir. nin H. wr H. elim x0. left. tv. right. tv. ir.
  nin H.  rw H. app R_inc. rw H. app R_inc.
Qed.

Lemma two_points_distinct: Ro two_points_a <> Ro two_points_b.
Proof. red. ir. cp (R_inj H). discriminate H0.
Qed.

Lemma two_points_distinctb: Ro two_points_b <> Ro two_points_a.
Proof. red. ir. cp (R_inj H). discriminate H0.
Qed.

Definition doubleton_map : forall x y : Bset, two_points -> Bset.
  intros x y t. induction t. exact x. exact y. Defined.

Definition doubleton (x y : Bset) := IM (doubleton_map x y).

Lemma doubleton_first : forall x y, inc x (doubleton x y).
Proof. ir. unfold doubleton. ap IM_inc. exists two_points_a. tv. Qed.

Lemma doubleton_second : forall x y : Bset, inc y (doubleton x y).
Proof. ir. unfold doubleton. ap IM_inc. exists two_points_b. tv. Qed.

Lemma doubleton_or :
 forall x y z : Bset, inc z (doubleton x y) -> z = x \/ z = y.
Proof. ir. pose (IM_exists H). elim e. intro x0. induction x0. simpl.
  intuition. simpl. intuition. Qed.

Hint Resolve doubleton_first doubleton_second: fprops.

Lemma doubleton_inj :
  forall x y z w,
    doubleton x y = doubleton z w -> ( x = z & y = w) \/ (x = w & y = z). 
Proof. ir. 
  assert (inc x (doubleton z w)). wr H; fprops.
  assert (inc y (doubleton z w)). wr H; fprops.
  assert (inc w (doubleton x y)). rw H; fprops.
  assert (inc z (doubleton x y)). rw H; fprops.
  pose (doubleton_or H0). pose (doubleton_or H1). 
  induction o.
  pose (doubleton_or H2). induction o. left. split. am.
  induction o0. rw H5; rw H4; am. am.  left. auto. 
  right. split. am. induction o0. am. pose (doubleton_or H3).
  sy. wri H4 H5. induction o. rww H5. am.
Qed.

Lemma doubleton_singleton : forall x, doubleton x x = singleton x.
Proof. ir. ap extensionality; unfold sub; ir.
  assert (e:=doubleton_or H). induction e. rw H0. fprops. 
  rw H0;  fprops. assert (H0:=singleton_eq H). rw H0. fprops.
Qed.

Lemma nonempty_doubleton: forall x y, nonempty (doubleton x y).
Proof. ir. exists x. fprops. Qed.

Lemma sub_doubleton: forall x y z,
  inc x z -> inc y z -> sub (doubleton x y) z.
Proof. ir.  red. ir. nin (doubleton_or H1). rw H2. fprops. rw H2. fprops.
Qed.

End Little.

Export Little. 

(** ** Basic Realisations *)
Module Basic_Realizations.

Lemma nat_zero_emptyset : Ro 0 = emptyset.
Proof. set_extens. 
  assert (H0:=nat_realization_O H). auto; elim H0. induction (Bo H).  
Qed.

Lemma false_emptyset : emptyset = False. 
Proof. set_extens. induction (Bo H).  elim (Bo H). Qed.


Lemma R_false_emptyset : Ro False = emptyset.
Proof. rw false_emptyset. ap prop_realization. Qed.

Lemma true_proof_emptyset : forall t : True, Ro t = emptyset.
Proof. ir. assert (H:=true_proof_realization_empty t). rw H. 
  apply nat_zero_emptyset.  Qed.

Lemma true_singleton_emptyset : singleton emptyset = True.
Proof. set_extens. assert (p:=singleton_eq H). unfold inc. exists I. sy. 
  rww true_proof_emptyset.  
  ufi inc H. induction H. assert (Ro x0 = emptyset).
  ap true_proof_emptyset. wr H0. rw H. ap singleton_inc.
Qed.

Lemma R_true_singleton_emptyset : Ro True = singleton emptyset.
Proof. rw prop_realization. sy. ap true_singleton_emptyset. 
Qed.

Lemma R_one_singleton_emptyset : Ro 1 = singleton emptyset.
Proof. set_extens. rwi nat_realization_S H; rwi nat_zero_emptyset H.
  induction H. pose emptyset_empty. elim (n x H).
  rw H. ap singleton_inc.
  rw nat_realization_S; rw nat_zero_emptyset. right. app singleton_eq. 
Qed.

Lemma R_two_prop : Ro 2 = Prop. 
Proof. set_extens. rwi nat_realization_S H; rwi R_one_singleton_emptyset H.
  unfold inc. induction H. set (H0:=(singleton_eq H)). rw H0. 
  exists False. ap R_false_emptyset.  
  rwi true_singleton_emptyset H. rw H. exists True. ap prop_realization.
  rw nat_realization_S. rw R_one_singleton_emptyset. 
  apply by_cases with (Bo H). ir. right. wrr R_true_singleton_emptyset.
  assert (Bo H = True). ap iff_eq; ir; tv. wr H1. rww B_eq. 
  ir. left. wr R_false_emptyset. 
  assert (Bo H = False). ap iff_eq. am. ir. elim H1. 
  assert (x = Ro (Bo H)). rww B_eq. rwi H1 H2. rw H2.  ap singleton_inc.
Qed. 

Lemma emptyset_dichot : forall x, (x = emptyset \/ nonempty x).
Proof. ir. ap excluded_middle. red. intro. 
  cut (x = emptyset & nonempty x); intuition. 
  apply excluded_middle; red; intros. apply H1.
  apply excluded_middle; red; intros.  apply H.  
  apply extensionality; red; intros. assert False.

  apply H2.  apply nonempty_intro with x0. assumption. elim H4.
  assert (~ inc x0 emptyset). apply emptyset_empty. intuition. 
  (* Second case*)
  apply excluded_middle; red; intros.  apply H0.
  apply extensionality; red; intros.  assert False.
  apply H1. apply nonempty_intro with x0. assumption. elim H3.
  assert (~ inc x0 emptyset). apply emptyset_empty. intuition. Qed.

End Basic_Realizations.
Export Basic_Realizations.

(** ** Complement *)
Module Complement. 

(** Set of all elements in a not in b *)
Definition complement (a b : Bset) := Zo a (fun x : Bset => ~ inc x b).

Lemma inc_complement :
 forall a b x, inc x (complement a b) = (inc x a & ~ inc x b).
Proof. ir. unfold complement. apply iff_eq; ir. pose (Z_all H).
  apply a0.  destruct H. app Z_inc. Qed.

Lemma use_complement :
 forall a b x, inc x a -> ~ inc x (complement a b) -> inc x b.
Proof. ir. ap excluded_middle; unfold not; ir. 
  ap H0. unfold complement. app Z_inc. Qed.

Lemma non_nonempty_comp_sub: forall a b, 
  ~ nonempty (complement a b) -> sub a b.
Proof. ir. uf sub. ir. apply use_complement with a. am. red. ir.
  app H. exists x. am.
Qed.

Lemma show_sub_or_aux: forall b c, 
 ~ (sub b c \/ sub c b) -> nonempty (complement c b).
Proof. ir. app excluded_middle. red. ir. app H. right. 
  app non_nonempty_comp_sub.
Qed.

Lemma show_sub_or :
 forall b c ,
 (nonempty (complement b c) -> nonempty (complement c b) -> False) ->
 sub b c \/ sub c b.
Proof.  ir. app excluded_middle. red. ir. ap H. 
  assert (~ (sub c b \/ sub b c)). red. ir. app H0.
  induction H1. right. am. left. am. app show_sub_or_aux.
  app show_sub_or_aux.
Qed. 

Lemma sub_complement: forall a b, sub (complement a b) a.
Proof. ir. uf sub; ir. rwi inc_complement H; ee; am. Qed.


Lemma strict_sub_nonempty_complement : forall x y,
  strict_sub x y -> nonempty (complement y x).
Proof. ir. assert (nonemptyT (complement y x)). 
  ap not_empty_nonemptyT. red; ir. uh H; ee. ap H. 
  set_extens. ap excluded_middle. red; ir. 
  assert (inc x0 (complement y x)).  rw inc_complement. split;am.  
  uh H0. ufi not H0. apply H0 with x0. am. nin H0. cp (R_inc X). 
  exists (Ro X). am.
Qed. 

End Complement.
Export Complement.

(** ** Pair *)
Module Pair.

Export Little.

(** One way of defining an ordered set *)

Definition pair_first (x y:Bset):= singleton x.
Definition pair_second (x y:Bset):= doubleton emptyset (singleton y).

Definition pair (x y : Bset) :=
  doubleton (pair_first x y) (pair_second x y).

Definition is_pair (u : Bset) := exists x, exists y, u = pair x y.

Lemma inc_pair1: forall x y, inc (pair_first x y) (pair x y).
Proof. ir. uf pair. fprops.
Qed.

Lemma inc_pair2: forall x y, inc (pair_second x y) (pair x y).
Proof. ir. uf pair. fprops.
Qed.

Lemma pair_extensionalitya: forall x y u, 
  inc u (pair x y) -> u = pair_first x y \/ u = pair_second x y.
Proof. ir. uf pair. app doubleton_or.
Qed.

Lemma pair_distincta:forall x y z w,
  (pair_first x y = pair_second z w)-> False.
Proof. ir.  ufi pair_first H; ufi pair_second H.
  assert (inc emptyset (singleton x)). rw H. fprops. cp (singleton_eq H0). 
  assert (inc (singleton w) (singleton x)). rw H. fprops.
  cp (singleton_eq H2). assert (inc w emptyset). rw H1; wr H3. fprops.
  nin H4. elim x0.
Qed.

Lemma pair_distinct:forall x y,
  pair_second x y <>  pair_first x y.
Proof. ir. red. ir. symmetry in H. app (pair_distincta H).
Qed.

Lemma pair_extensionality_first : forall x y z w : Bset, 
  pair x y = pair z w -> x = z.
Proof. ir. assert (pair_first x y = pair_first z w).
  assert (inc (pair_first x y) (pair z w)).  wr H. app inc_pair1.
  cp (pair_extensionalitya H0).  nin H1. am. elim (pair_distincta H1). 
  ufi pair_first H0. app singleton_inj. 
Qed.

Lemma pair_extensionality_second : forall x y z w, 
  pair x y = pair z w -> y = w.
Proof. ir. assert (pair_second x y = pair_second z w).
  assert (inc (pair_second x y) (pair z w)).  wr H. app inc_pair2.
  cp (pair_extensionalitya H0).  nin H1. 
  symmetry in H1. elim (pair_distincta H1). am. ufi pair_second H0. 
  assert (inc (singleton y) (doubleton emptyset (singleton w))). wrr H0.
  fprops. pose (doubleton_or H1). induction o. 
  assert (inc y emptyset). wr H2.  fprops. nin H3. elim x0. app singleton_inj. 
Qed. 

(** First and second projections *)
Definition pr1 (u : Bset) :=
  choose (fun x : Bset => ex (fun y : Bset => u = pair x y)).
Definition pr2 (u : Bset) :=
  choose (fun y : Bset => ex (fun x : Bset => u = pair x y)).

Notation J := pair.
Notation P := pr1.
Notation Q := pr2. 


Definition pair_recovers (u : Bset) := J (P u) (Q u) = u.

Lemma pair_recov : forall u, is_pair u -> pair_recovers u.
Proof. unfold is_pair. unfold pair_recovers. ir.
  pose (choose_pr H). induction e.
  assert  (exists y : Bset, exists x : Bset, u = J x y).
  exists x. exists (P u). am. 
  pose (choose_pr H1). induction e. 
  assert (u = J (P u) x). am. assert (u = J x0 (Q u)). am.
  assert (J (pr1 u) x = J x0 (pr2 u)). wrr H3. 
  pose (pair_extensionality_first H5). rw e. sy. am. Qed. 

Lemma pair_is_pair : forall x y : Bset, is_pair (J x y). 
Proof. unfold is_pair.  intros.  exists x.  exists y. trivial. Qed. 

Hint Resolve pair_is_pair: fprops.

Lemma is_pair_rw : forall x, is_pair x = (x = J (P x) (Q x)).
Proof. ir. ap iff_eq;ir. set (H0:=pair_recov H).
  red in (type of H0). sy; am. rw H. fprops. 
Qed. 

Lemma pr1_pair : forall x y, P (J x y) = x.
Proof. ir. set (u := J x y). assert (is_pair u). 
  unfold u. ap pair_is_pair. assert(p:=pair_recov H).  
  ufi pair_recovers p. ufi u p. pose (pair_extensionality_first p). am. Qed. 


Lemma pr2_pair : forall x y, Q (J x y) = y.
Proof. ir. set (u := J x y). assert (is_pair u). 
  unfold u. fprops. assert (p:=pair_recov H). 
  ufi pair_recovers p. ufi u p.  pose (pair_extensionality_second p). am. 
Qed. 


Hint Rewrite pr1_pair pr2_pair : aw. 
Ltac awi u:= autorewrite with aw in u.

Lemma pair_extensionality : forall a b, 
  is_pair a -> is_pair b -> P a = P b -> Q a = Q b -> a = b.
Proof.  ir. transitivity (J (P a) (Q a)).
  assert (pair_recovers a). app pair_recov. sy. ap H3.
  assert (pair_recovers b). app pair_recov.
  rw H1. rw H2. am. 
Qed. 


Lemma pr1_injective: forall a b c d,
  J a b = J c d -> a = c.
Proof. ir. assert (P (J a b) = P (J c d)). rww H. awi H0. am. Qed.

Lemma pr2_injective: forall a b c d,
  J a b = J c d -> b = d.
Proof. ir. assert (Q (J a b) = Q (J c d)). rww H. awi H0. am.
Qed.

Lemma uneq2 : forall (f:Bset-> Bset-> Bset) (a b c d:Bset),
  a=c -> b = d -> f a b = f c d.
Proof. ir. rw H. rw H0. tv. Qed. 

(** [V x f] is the value of x by a graph f; if there is a z such that 
    [J x z] is in f, that V chooses one, otherwise it is the empty set. *)
Definition V (x f : Bset) := choose (fun y : Bset => inc (pair x y) f).

Lemma V_inc : forall x z f, 
  (exists y, inc (J x y) f) -> z = V x f -> inc (J x z) f. 
Proof.  ir. rw H0. pose (choose_pr H). am. Qed. 

Lemma V_or : forall x f,
  (inc (J x (V x f)) f) \/
  ((forall z, ~(inc (J x z) f)) & (V x f = emptyset)).
Proof. ir. apply by_cases with (ex (fun y=> inc (pair x y) f)); ir.
  left. app V_inc.
  right. split. ir.  unfold not; intro; apply H. exists z. am. 
  unfold V. app choose_not. Qed. 


End Pair.
Export Pair.

(** ** Image *)
Module Image. 

(** Image of a set by a function *)

Definition fun_image (x : Bset) (f : EE) := IM (fun a : x => f (Ro a)). 

Lemma inc_fun_image : forall x f a, inc a x -> inc (f a) (fun_image x f).
Proof.  ir. uf fun_image. ap IM_inc. exists (Bo H). rww (B_eq H). Qed. 


Lemma fun_image_rw : forall  f x y,
  inc y (fun_image x f) = exists z, (inc z x & f z = y).
Proof.  ir. ap iff_eq; intros. 
  pose (IM_exists H).  induction e. exists (Ro x0). split.  app R_inc. tv.
  induction H. induction H. wr H0. app inc_fun_image. 
Qed. 
End Image.
Export Image.

(** ** Powerset *)
Module Powerset. 

(** This is the set of all cuts, but in fact is the set of all subsets*)
Definition powerset (x : Bset) := IM (fun p : x -> Prop => cut p).


Lemma powerset_inc : forall x y, sub x y -> inc x (powerset y). 
Proof. ir. uf powerset. ap IM_inc. exists (fun b:y=> inc (Ro b) x).
  set_extens. set (c:= (Bo H0)). 
  assert (x0 = Ro c). pose (B_eq H0); sy; am.
  assert (Ro c = Ro (cut_to c)). sy. ap cut_to_R_eq.
  rw H1; rw H2.  apply (cut_pr c).
  set  (x1:= Bo H0). set (e:=B_eq H0). 
  wr e. unfold cut. ap Z_inc. ap H. rww e. 
  ir. set (w:= B_eq hyp). rw w; rw e.  am. Qed.


Lemma powerset_sub : forall x y, inc x (powerset y) -> sub x y.
Proof. ir. ufi powerset H. set (e:= IM_exists H). 
  induction e. wr H0. ap cut_sub. Qed.


Lemma powerset_inc_rw : forall x y, inc x (powerset y) = sub x y.
Proof. ir. apply iff_eq; ir. app powerset_sub. app powerset_inc. Qed. 

Lemma inc_x_powerset_x: forall x, inc x (powerset x).
Proof. ir. app powerset_inc. red; tv. Qed.

End Powerset. 
Export Powerset. 

(** ** Union *)
Module Union. 

(** Integral: records p and e. Pose [q = Ro p]. By definition, [inc q x]. *)
Record Union_integral (x : Bset) : Bset := 
  {Union_param : x; Union_elt : Ro Union_param}.

(** Union: y is in the union if [y= Ro e]  for some e, this is [inc y q],
q defined above *)
Definition union (x : Bset) :=
  IM (fun i : Union_integral x => Ro (Union_elt (x:=x) i)).

Lemma union_inc : forall x y a, inc x y -> inc y a -> inc x (union a).
Proof. ir. set (w:= Bo H0). assert (Ro w = y). uf w; ap B_eq.
  assert (inc x (Ro w)). rww H1. 
  pose (Bo H2). pose (Build_Union_integral (x:=a) (Union_param:=w) r). uf union.
  ap IM_inc.  exists u. simpl. uf r. apply B_eq. Qed. 

Lemma union_exists : forall x a,
    inc x (union a) -> exists y,  inc x y & inc y a.
Proof. ir. ufi union H. set (e:= IM_exists H). induction e.
  exists (Ro (Union_param x0)). wr H0. split. ap R_inc. ap R_inc. Qed. 

Lemma union_sub: forall x y, inc x y -> sub x (union y).
Proof. ir. red. ir. apply union_inc with x. am. am.
Qed.
  
(** Union of two sets *)
Definition union2 (x y : Bset) := union (doubleton x y). 


Lemma union2_or : forall x y a, inc a (union2 x y) -> inc a x \/ inc a y.
Proof. ir. ufi union2 H. pose (union_exists H). 
  induction e. induction H0. nin (doubleton_or H1). 
  left; wrr H2. right; wrr H2. Qed.


Lemma union2_first : forall x y a, inc a x -> inc a (union2 x y).
Proof. ir. uf union2. apply union_inc with x. am. fprops. Qed. 

Lemma union2_second : forall x y a, inc a y -> inc a (union2 x y).
Proof. ir. uf union2. apply union_inc with y. am. fprops. Qed. 

Lemma inc_union2_rw : forall a b x,
  inc x (union2 a b) = (inc x a \/ inc x b).
Proof. ir. apply iff_eq; ir.  app union2_or. 
  induction H; [app union2_first | app union2_second].
Qed.

Lemma union2_idempotent: forall u, union2 u u= u.
Proof. ir. set_extens. rwi inc_union2_rw H. nin H. am. am.
  rw inc_union2_rw. left. am.
Qed.

(** Union of x and a single element *)
Definition tack_on x y := union2 x (singleton y). 

Lemma tack_on_or : forall x y z, inc z (tack_on x y) ->
  (inc z x \/ z = y). 
Proof. ir. ufi tack_on H. set (H1:= union2_or H). 
  induction H1; [ left | right; ap singleton_eq]; assumption.  
Qed. 

Lemma tack_on_inc: forall x y z,
  (inc z (tack_on x y) ) = (inc z x \/ z = y).
Proof. ir. ap iff_eq. ap tack_on_or. ir.
  uf tack_on. induction H. app union2_first. 
  ap union2_second. wr H. ap singleton_inc. Qed.

(** Like tack, argumenrs reversed *)
Definition tack x y := tack_on y x.

Lemma tack_or : forall x y z, inc z (tack y x) ->   (inc z x \/ z = y).
Proof. ir. ufi tack H. app tack_on_or. Qed.


Lemma tack_inc :  forall x y z,
  (inc z (tack y x) ) = (inc z x \/ z = y).
Proof. ir. uf tack. ap tack_on_inc. Qed. 

Lemma sub_union : forall x z, 
 (forall y, inc y z -> sub y x) -> sub (union z) x.
Proof.  ir. red; ir. pose (union_exists H0). nin e. ee. assert (sub x1 x). 
  app H. app H3.  
Qed. 


End Union. 

Export Union. 

(** ** Intersection *)
Module Intersection. 


(** Intersection: set of of all z in w, that are in all elements of x;
   w is some element of x, the value is irrelevant. 
   Sometimes x must be assumed nonempty *) 
Definition intersection (x : Bset) :=
  Zo (rep x) (fun y : Bset => forall z : Bset, inc z x -> inc y z). 

Lemma intersection_inc :  forall x a,
    nonempty x -> (forall y, inc y x -> inc a y) -> inc a (intersection x). 
Proof. ir. uf intersection. app Z_inc. 
  pose (nonempty_rep H). app H0.
Qed. 

Lemma intersection_forall :
 forall x a y, inc a (intersection x) -> inc y x -> inc a y.
Proof. ir. ufi intersection H. pose (Z_all H).
  induction a0. app H2. Qed.

Lemma intersection_sub : forall x y, inc y x -> sub (intersection x) y.
Proof. ir. uf sub. ir. apply intersection_forall with x. am. am.
Qed.

(** Intersection of two sets *)
Definition intersection2 x y := intersection (doubleton x y).

Lemma intersection2_inc :
 forall x y a, inc a x -> inc a y -> inc a (intersection2 x y).
Proof. ir. uf intersection2. ap intersection_inc. app nonempty_doubleton.
  ir. set (H4:=doubleton_or H1). destruct H4 as [H5 | H6]; [rww H5|rww H6].
Qed.

Lemma intersection2_first :
 forall x y a, inc a (intersection2 x y) -> inc a x.
Proof.  ir. ufi intersection2 H.
  apply intersection_forall with (doubleton x y). am. fprops.
Qed.


Lemma intersection2_second :
 forall x y a, inc a (intersection2 x y) -> inc a y.
Proof. ir. ufi intersection2 H.
  apply intersection_forall with (doubleton x y). am. fprops.
Qed.


Lemma intersection_use_inc :
 forall x y, inc y (intersection x) -> forall z, inc z x -> inc y z.
Proof. ir. apply intersection_forall with x; am.
Qed. 


End Intersection.

Export Intersection. 

(** ** Transposition *)

Module Transposition.

(** Evaluates to j or i if a is i or j; to a otherwise *)
Definition create (i j a : Bset) := Yo (a = i) j (Yo (a = j) i a).

Lemma not_i_not_j : forall i j a, a <> i -> a <> j -> create i j a = a.
Proof. ir. uf create. ap (Y_if_not H). sy. apply (Y_if_not H0). tv. 
Qed.

Lemma i_j_j_i : forall i j a, create i j a = create j i a.
Proof. ir. uf create. apply by_cases with (a = i).
  ir. ap (Y_if H). sy. apply by_cases with (a = j). 
  ir. ap (Y_if H0). wrr H.
  ir. ap (Y_if_not H0). sy. app (Y_if H).
  ir. ap (Y_if_not H). apply by_cases with (a = j). 
  ir. ap (Y_if H0). sy. app (Y_if H0). 
  ir. ap (Y_if_not H0). ap (Y_if_not H0).  app (Y_if_not H). 
Qed. 

Lemma i_j_i : forall i j, create i j i = j.
Proof. ir. uf create. assert (i = i); trivial. app (Y_if H). 
Qed.

Lemma i_j_j : forall i j, create i j j = i.
Proof. ir. rw i_j_j_i. ap i_j_i. Qed. 

Lemma i_i_a : forall i a, create i i a = a.
Proof. ir. apply by_cases with (a = i). ir. rw H. ap i_j_j. ir. 
  uf create. ap (Y_if_not H). sy. app (Y_if_not H). 
Qed.


Lemma surj : forall i j a, exists b, create i j b = a.
Proof. ir. apply by_cases with (a = i). 
  ir. exists j. rw H. ap i_j_j. ir. apply by_cases with (a = j). 
  ir. exists i. rw H0. ap i_j_i. ir. exists a. app not_i_not_j.
Qed.


Lemma involutive : forall i j a, create i j (create i j a) = a. 
Proof.  ir. apply by_cases with (a = i). 
  ir. rw H. rw i_j_i. ap i_j_j. apply by_cases with (a = j). 
  ir. rw H. rw i_j_j. app i_j_i. ir. pose (not_i_not_j H0 H). rww e.
Qed. 

Lemma inj : forall i j a b, create i j a = create i j b -> a = b.
Proof. ir. transitivity (create i j (create i j a)). 
  sy; ap involutive. rw H. ap involutive. 
Qed. 



End Transposition.

(** ** Module Bounded

A property p is "collectivisante" if there exists a set x such that 
[p y] if and only if [inc y x]. Such a set is unique. It exists if p has the 
form [y = f z], where f is defined on a set or a type.
*)
Module Bounded.

Definition property (p : EP) (x : Bset) :=
  forall y : Bset, (p y -> inc y x & inc y x -> p y). 

Definition axioms (p : EP) := ex (property p).

Definition create (p : EP) := choose (property p). 

Lemma criterion : forall p : EP,
 ex (fun x : Bset => forall y : Bset, p y -> inc y x) -> axioms p. 
Proof. intros p (x) H. red. exists (Zo x p). 
  red.  ir. split.  ir. apply (Z_inc _ (H _ H0) H0). ir. apply (Z_pr H0). 
Qed. 


Lemma lem1 : forall (p : EP) (y : Bset), axioms p -> inc y (create p) -> p y.
Proof. ir. red in H. ufi create H0. pose (choose_pr H). ufi property H0. 
  ufi property  p0. pose (p0 y).  induction a. app H2.
Qed.
  
Lemma lem2 : forall (p : EP) (y : Bset), axioms p -> p y -> inc y (create p).
Proof. ir. uf create. ufi axioms H. pose (choose_pr H). 
  set (K := choose (property p)). ufi property  p0. 
  pose (p0 y). induction a. app H1. 
Qed. 


Lemma inc_create :  forall (p : EP) y, axioms p -> inc y (create p) = p y. 
Proof. ir. app iff_eq. ir.  app lem1.  ir. app lem2.
Qed.

Lemma trans_criterion :
  forall (p : EP) (f : EE) (x : Bset),
    (forall y : Bset, p y -> ex (fun z : Bset =>  (inc z x &f z = y))) ->
    axioms p.
Proof. ir. app criterion. exists (fun_image x f). 
  ir. rw fun_image_rw.  app H.
Qed. 

Lemma little_criterion :
  forall (p : EP) (x : Bset) (f : x -> Bset),
    (forall y : Bset, p y -> exists a : x, f a = y) -> axioms p. 
Proof. ir. ap criterion.  exists (IM f). ir. ap IM_inc. app H.
Qed. 


End Bounded.

(** ** Cartesian products of two sets *)

Module Cartesian.

(** Rolation [in_record] is collectivisante, hence we can define a record *) 
Definition in_record (a : Bset) (f : EE) (x : Bset) :=
  is_pair x  & inc (P x) a   & inc (Q x) (f (P x)).

Record Cartesian_record (a : Bset) (f : EE) : Bset := 
  {Cartesian_first : a; Cartesian_second : f (Ro Cartesian_first)}.

Definition recordMap (a : Bset) (f : EE) (i : Cartesian_record a f) :=
  J (Ro (Cartesian_first i)) (Ro (Cartesian_second i)).

Lemma in_record_ex : forall (a : Bset) (f : EE) (x : Bset),
 in_record a f x -> exists i : Cartesian_record a f, recordMap i = x.
Proof. ir. red in H. ee. set (u := Bo H0). 
  assert (Ro u = pr1 x). uf u. apply B_eq.
  assert (inc (pr2 x) (f (Ro u))). rww H2.  
  set (v := Bo H3).
  pose (Build_Cartesian_record f u v).
  exists c. transitivity (pair (Ro u) (Ro v)). trivial.
  assert (Ro v = pr2 x). uf v. app B_eq. rw H4. 
  assert (Ro u = pr1 x); auto. rw H5. app pair_recov.
Qed.

Lemma in_record_bounded :
 forall (a : Bset) (f : EE), Bounded.axioms (in_record a f).
Proof. ir. apply Bounded.criterion. exists (IM (recordMap (a:=a) (f:=f))). 
  ir. ap IM_inc. app in_record_ex. 
Qed.

Definition record (a : Bset) (f : EE) := Bounded.create (in_record a f).

Lemma record_in :
 forall a f x, inc x (record a f) -> in_record a f x.
Proof. ir.  ufi record  H. pose (in_record_bounded a f).
  pose (Bounded.lem1 a0 H). assumption.
Qed.

Lemma record_pr :  forall a f x,
    inc x (record a f) ->
    (is_pair x & inc (P x) a & inc (Q x) (f (P x))).
Proof. intros. pose (record_in H). assumption.
Qed.

Lemma record_inc :  forall a f x, in_record a f x -> inc x (record a f).
Proof. ir. uf record. app Bounded.lem2. ap in_record_bounded.
Qed.

Lemma record_pair_pr :  forall  a f x y,
    inc (J x y) (record a f) -> (inc x a & inc y (f x)).
Proof. ir. split. pose (record_in H). ufi in_record i.
  induction i. induction H1.  awi H1.  am.
  pose (record_in H). ufi in_record  i. ee. awi H2. am.
Qed.

Lemma record_pair_inc : forall a f x y,
 inc x a -> inc y (f x) -> inc (pair x y) (record a f).
Proof. ir. ap record_inc. red.  ee.  fprops. aw.  aw. 
Qed.

(** A product is just a record where the function is constant *)
Definition product (a b : Bset) := record a (fun x : Bset => b).

Lemma product_pr : forall a b u,
    inc u (product a b) -> (is_pair u & inc (P u) a & inc (Q u) b).
Proof. uf product; ir.  pose (record_pr H). intuition. 
Qed.

Lemma product_inc :  forall a b u,
 is_pair u -> inc (P u) a -> inc (Q u) b -> inc u (product a b).
Proof. ir. uf product. ap record_inc. uf in_record. intuition.
Qed.

Lemma product_pair_pr :
 forall a b x y : Bset, inc (J x y) (product a b) -> (inc x a & inc y b).
Proof. ir. ufi product H. pose (record_pair_pr H). assumption.
Qed.

Lemma product_pair_inc :
  forall a b x y, inc x a -> inc y b -> inc (J x y) (product a b).
Proof. ir. uf product. app record_pair_inc.
Qed.

Lemma inc_product : forall x y z,
  inc x (product y z) = (is_pair x & inc (P x) y & inc (Q x) z).
Proof.
  ir. ap iff_eq; ir. cp (product_pr H). am. ap product_inc; ee; am. 
Qed.


(** A product is empty if and only one factor is empty *)
Lemma empty_product1: forall y,
 product emptyset y = emptyset.
Proof. ir. set_extens. rwi inc_product H. ee. nin H0. elim x0.  
  nin H. elim x0. 
Qed.
  
Lemma empty_product2: forall x,
  product x emptyset = emptyset.
Proof. ir. set_extens. rwi inc_product H. ee. nin H1. elim x1.
  nin H. elim x1. 
Qed.

Lemma empty_product_pr: forall x y,
   product x y = emptyset -> (x = emptyset \/ y= emptyset).
Proof. ir. pose (emptyset_dichot x). nin o. left. am. ir. right. nin H0.
  set_extens. assert (inc (J y0 x0) (product x y)). app product_pair_inc.
  rwi H H2. nin H2. elim x1. nin H1. elim x1.
Qed.

(** The product A*B is increasing in A and B, strictly if the other argument
is non empty. *)

Lemma product_monotone_left: forall x x' y,
  sub x x' -> sub (product x y) (product x' y).
Proof. ir. red. ir. rwi inc_product H0. ee. rw inc_product. ee. am. app H. am.
Qed.

Lemma product_monotone_right: forall x y y',
  sub y y' -> sub (product x y) (product x y').
Proof. ir. red. ir. rwi inc_product H0. ee. rw inc_product. ee. am. am. app H. 
Qed.

Lemma product_monotone: forall x x' y y',
  sub x x' -> sub y y' -> sub (product x y) (product x' y').
Proof. ir. apply sub_trans with (product x' y). app product_monotone_left.
   app product_monotone_right.
Qed.

Lemma product_monotone_left2: forall x x' y, nonempty y ->
  sub (product x y) (product x' y) -> sub x x'. 
Proof. ir. red. ir. nin H. assert (inc (J x0 y0) (product x' y)). app H0. 
  rw inc_product. ee.  fprops. aw.  aw. 
  rwi inc_product H2. ee.  awi H3. am.
Qed.

Lemma product_monotone_right2: forall x y y', nonempty x ->
  sub (product x y) (product x y') -> sub y y'. 
Proof. ir. red. ir. nin H. assert (inc (J y0 x0) (product x y')). app H0. 
  rw inc_product. ee.  fprops. aw. aw. rwi inc_product H2. ee. awi H4. am.
Qed.


End Cartesian.

Export Cartesian.



(** ** Back *)

Module Sback.

(** Defines [Bdefault] as a version of [B] where a default
value is given and thus no hypothesis of inclusion is required;
applies this to get [Bnat] sending a set back to a natural with
default value [0]. *)

Definition RBdefault x z (d:z) := Yo (inc x z) x (Ro d).


Lemma RBdefault_in : forall x z (d:z), inc x z -> RBdefault x d = x.
Proof. ir. uf RBdefault. rww Y_if_rw. 
Qed.

Lemma RBdefault_out : forall x z (d:z),
  ~(inc x z) -> RBdefault x d = (Ro d).
Proof. ir. uf RBdefault.  rww Y_if_not_rw. 
Qed.


Lemma inc_RBdefault : forall x z (d:z), inc (RBdefault x d) z.
Proof. ir. apply by_cases with (inc x z); ir. 
  rww RBdefault_in. rww RBdefault_out. app R_inc. Qed.


Definition Bdefault x z (d:z) : z :=
  Bo (inc_RBdefault x d).

Lemma R_Bdefault_in : forall x z (d:z),
  inc x z -> Ro (Bdefault x d) = x.
Proof. ir. uf Bdefault. rw B_eq. rww RBdefault_in. 
Qed.

Lemma Bdefault_out : forall x z (d:z),
~(inc x z) -> (Bdefault x d) = d. 
Proof. ir. uf Bdefault. ap R_inj. rw B_eq. rww RBdefault_out.  
Qed.

Lemma Bdefault_R : forall z (y d:z),
  Bdefault (Ro y) d = y.
Proof. ir. ap R_inj. rww R_Bdefault_in. ap R_inc. 
Qed.

Definition Bnat x := Bdefault x (z:=nat) 0.


Lemma R_Bnat : forall x, inc x nat ->
Ro (Bnat x) = x.
Proof. ir. uf Bnat. rww R_Bdefault_in. 
Qed.

Lemma Bnat_out : forall x, ~(inc x nat) ->
Bnat x = 0.
Proof. ir. uf Bnat. rww Bdefault_out. 
Qed.

Lemma Bnat_R : forall (i:nat), Bnat (Ro i) = i.
Proof. ir. ap R_inj. rww R_Bnat. ap R_inc. 
Qed.

End Sback.