(** * Fundamental set theory
Original file by Carlos Simpson (CNRS/UNSA)

Copyright INRIA (2009-2013) Apics-Marelle Team (Jose Grimm).
*)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

(** ** Axioms *)
Module Axioms.

(** Some definitions *)

Definition fterm:= Set -> Set. 
Definition fterm2:= Set -> Set -> Set. 
Definition property := Set -> Prop.
Definition relation := Set -> Set -> Prop.
Definition reflexive_r (R: relation) := forall x, R x x.
Definition symmetric_r (R: relation) := forall x y, R x y -> R y x.
Definition transitive_r (R: relation) := forall y x z, R x y -> R y z -> R x z.
Definition antisymmetric_r (R: relation) := forall x y, R x y -> R y x -> x = y.
Definition singl_val (p: property):=
   forall x y, p x -> p y -> x = y.
Definition singl_val2 (p q: property):=
   forall x y, p x -> q x -> p y -> q y -> x = y.

Definition singl_val_fp (p: property) (f: fterm) :=
  forall x y, p x -> p y -> f x = f y.

Definition exactly_one (P Q: Prop) := (P \/ Q) /\ ~(P /\ Q).


(** This destructures a conjunction *)

Lemma proj31 A B C: [/\ A, B & C] -> A.
Proof. by destruct 1.  Qed.
Lemma proj32 A B C: [/\ A, B & C] -> B.
Proof. by destruct 1.  Qed.
Lemma proj33 A B C: [/\ A, B & C] -> C.
Proof. by destruct 1.  Qed.

Lemma proj31_1 a b c d : [/\ a, b & c] /\ d -> a. 
Proof. by move/proj1 /proj31. Qed.

Lemma proj32_1 a b c d : [/\ a, b & c] /\ d -> b. 
Proof. by move/proj1/proj32. Qed.


Lemma proj41 A B C D: [/\ A, B, C & D] -> A.
Proof. by destruct 1.  Qed.
Lemma proj42 A B C D: [/\ A, B, C & D] -> B.
Proof. by destruct 1.  Qed.
Lemma proj43 A B C D: [/\ A, B, C & D] -> C.
Proof. by destruct 1.  Qed.
Lemma proj44 A B C D: [/\ A, B, C & D] -> D.
Proof. by destruct 1.  Qed.

Lemma iff_sym (P Q: Prop): (P <-> Q) -> (Q <-> P).
Proof. exact: Logic.iff_sym. Qed.

Lemma iff_trans (P Q R: Prop): (P <-> Q) -> (Q <-> R) -> (P <-> R).
Proof. exact: Logic.iff_trans.  Qed.

Lemma iff_neg (P Q: Prop): (P <-> Q) -> ( ~ P <->  ~ Q).
Proof. by move => h; split => np q; case: np; apply/h. Qed.


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

Parameter Ro : forall x : Set, x -> Set.

(** Injectivity of [Ro] *)

Axiom R_inj : forall (x : Set),  injective (@Ro x).

(** Defines [inc] as "is element of" and [sub] as "is subset of" *)

Definition inc (x y : Set) := exists a : y, Ro a = x.
Definition sub (a b : Set) := forall x : Set, inc x a -> inc x b.
Definition ssub (a b : Set) :=  (sub a b) /\ (a <> b).
(** Extensionality for sets *)

Axiom extensionality : antisymmetric_r sub.

(** [nonempty]: the set has an element. *) 

CoInductive nonempty (x : Set) : Prop :=
    nonempty_intro : forall y : Set, inc y x -> nonempty x.

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

Section Choose.
Variable (t : Type).
Implicit Type (p : t -> Prop)  (q:inhabited t).

Parameter chooseT : forall p q,  t.
Axiom chooseT_pr : forall p q, ex p -> p (chooseT p q).

End Choose.

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

Parameter IM : forall (x : Set) (f : x -> Set), Set.

Axiom IM_P :  forall (x : Set) (f : x -> Set) (y : Set),
          inc y (IM f) <-> exists a : x, f a = y.

(** Excluded middle and consequences. *)

Axiom p_or_not_p: forall P:Prop,  P \/ ~ P.

Lemma ixm (P: Prop): P + ~P.
Proof.
apply: (chooseT (fun _ => True)).
by case: (p_or_not_p P) => H;constructor; [ left | right ].
Qed.

Ltac ex_middle u := match goal with
  | |- ?p => case: (p_or_not_p p) ; [ done | move => u ]
end.

Lemma excluded_middle (p:Prop): ~ ~ p -> p.
Proof. move => nnp; ex_middle np; case: (nnp np). Qed.

Lemma equal_or_not (x y: Set) :  x = y \/ x <> y.
Proof. apply: p_or_not_p. Qed.

Lemma inc_or_not (x y:Set): inc x y \/ ~ (inc x y).
Proof. apply: p_or_not_p.  Qed.

Ltac dneg u := match goal with 
  H : ~ _ |- ~ _ => move => u; apply:H
end.

Ltac in_TP4:= solve [by constructor 1 | by constructor 2 |
   by constructor 3 |  by constructor 4]. 

Definition Yo (P : Prop) (x y : Set) := 
  match (ixm P) with inl _ => x | inr _ => y end.

Lemma Y_true (P:Prop) (hyp :P) x y: Yo P x y = x.
Proof. by rewrite /Yo; case: (ixm P). Qed.

Lemma Y_false (P:Prop) (hyp : ~P) x y: Yo P x y = y.
Proof. by rewrite /Yo; case: (ixm P). Qed.

Lemma Y_same (P: Prop) x : Yo P x x = x.
Proof. by rewrite /Yo;case: (ixm P). Qed.

End Axioms.
Export Axioms.

(** ** Tactics *)
Module Tactics1.


(** Tatics like [aw] use autorewite and trivial;
  tactics like [fprops] use auto  *)
Ltac aw := autorewrite with aw; trivial.
Ltac bw := autorewrite with bw; trivial. 

Ltac fprops := auto with fprops.

Ltac set_extens v:= apply: extensionality=> v.

Ltac ue := 
  match goal with
    | H:?a = ?b |- _ => solve [ rewrite  H ; fprops | rewrite - H ; fprops] 
end.

End Tactics1.
Export Tactics1.

(** ** Constructions *)

Module Constructions.

Lemma sub_trans: transitive_r sub.
Proof. move => b a c sab sbc t ta; apply: sbc; exact: sab. Qed.

Lemma sub_refl: reflexive_r sub.
Proof. by move => x y. Qed. 

Lemma ssub_trans1 b a c: ssub a b -> sub b c -> ssub a c.
Proof.
move => [sab nab] sbc; split; first by apply: (sub_trans sab).
by dneg ac;apply: (extensionality sab); rewrite ac.
Qed.

Lemma ssub_trans2 b a c: sub a b -> ssub b c -> ssub a c.
Proof. 
move => sab [sbc nbc]; split; first by apply: (sub_trans sab).
by dneg ac;apply: (extensionality sbc); rewrite -ac.
Qed.

(** [emptyset] is a type without constructor; [empty] is classical. *)

Definition empty (x : Set) := forall y : Set, ~ inc y x. 
CoInductive emptyset : Set :=.

(** Basic property of [Ro]. *)

Lemma R_inc (x : Set) (a : x): inc (Ro a) x.
Proof. by exists a. Qed.

(** Equivalence between [nonempty] and [~ empty]. *)

Lemma in_set0 x: ~ inc x emptyset.
Proof. move=> [[]]. Qed.

Lemma set0_P x: empty x <-> x = emptyset.
Proof.
split; last by move => -> y /in_set0.
by move => Iyx; set_extens t => Ht; [ case: (Iyx t) | case: (in_set0 Ht) ].  
Qed.

Lemma emptyset_dichot x: x = emptyset \/ nonempty x.
Proof. 
case: (p_or_not_p (nonempty x)); [ by right | move => nex; left].
by apply /set0_P => t tx; case: nex; exists t.
Qed.

Lemma nonemptyP x: nonempty x <-> (x <> emptyset).
Proof.
split => xne; last by case: (emptyset_dichot x) => // ->.
move => xe; case: xne; rewrite xe; exact:in_set0.
Qed.

Lemma sub0_set x : sub emptyset x.
Proof. by move=> t /in_set0. Qed.

Hint Resolve sub0_set sub_refl : fprops.

Lemma sub_set0 x: sub x emptyset <-> (x = emptyset).
Proof.  
split;move => h; [ by apply/set0_P => t /h/in_set0 | ue].
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]. *)

Definition Bo (x y : Set) (Hxy : inc x y) :=
 chooseT (fun a : y => Ro a = x)
    (match Hxy with | ex_intro w _ => inhabits w end).

Lemma B_eq x y (Hxy : inc x y): Ro (Bo Hxy) = x.
Proof. apply: chooseT_pr Hxy. Qed.

Lemma B_back  (x:Set) (y:x) (hyp : inc (Ro y) x): Bo hyp = y.
Proof. by apply: R_inj; apply: B_eq. Qed.

(** Genereralised axiom of choice. [choose p] is satisfied by [p]
   if somebody satisfies [p] *)

Definition choose (p: property) := chooseT p (inhabits emptyset).

Lemma choose_pr p: ex p -> p (choose p).
Proof. by apply: chooseT_pr. Qed.

(** Axiom of choice applied to [inc]. If [x] not empty, [rep x] is in [x]. *)

Definition rep (x : Set) := choose (fun y : Set => inc y x). 

Lemma rep_i x: nonempty x -> inc (rep x) x. 
Proof. by move => [y iyx]; apply: (choose_pr (p:= inc ^~ x)); exists y. Qed.

(** Given a function [f], [Zorec] remembers [a] and [f a] *)

CoInductive Zorec (x : Set) (f : x -> Prop) : Set :=
  Zorec_c :forall (a: x), f a -> Zorec f.

Definition Zo (x:Set) (p:property) :=
  IM (fun  (z : Zorec (fun (a : x) => p (Ro a))) => let (a, _) := z in Ro a).

Lemma Zo_i x (p:property) y: inc y x -> p y -> inc y (Zo x p).
Proof. 
rewrite /Zo => -[a Roa]; rewrite -{1} Roa => py.
by apply/ IM_P; exists (Zorec_c (f:= (fun a : x => p (Ro a))) py).  
Qed.

Lemma Zo_hi x (p: property) y: inc y (Zo x p) -> p y.
Proof. by case /IM_P => v <-; case:v.  Qed.

Lemma Zo_S x (p: property): sub (Zo x p) x.
Proof. move=> y /IM_P [v <-];case:v => z _; apply: R_inc. Qed.

Lemma Zo_P x (p: property) y: inc y (Zo x p) <-> (inc y x /\ p y).
Proof.
split=> [H | [u v]]; last by apply: Zo_i.
split; [ exact: (Zo_S H) | exact: (Zo_hi H) ].
Qed.

Lemma Zo_exten1 (X : Set) (p q: property):
   (forall x, inc x X -> (p x <-> q x)) -> Zo X p = Zo X q.
Proof.
by move => h; set_extens t => /Zo_P [pa /(h _ pa) pb];apply: Zo_i. 
Qed.

Lemma Zo_exten2 (X Y: Set) (p q: property):
   (forall x, (inc x X /\ p x <-> inc x Y /\ q x)) -> Zo X p = Zo Y q.
Proof.
by move => h; set_extens t => /Zo_P pa; apply/Zo_P /h.
Qed.

End Constructions.

Export Constructions.

(** ** Little*)
Module Little.

Definition doubleton (x y : Set) :=
  IM (fun z => if z then x else y).

Lemma set2_1 x y: inc x (doubleton x y).
Proof. by apply /IM_P; exists true. Qed.

Lemma set2_2 x y : inc y (doubleton x y).
Proof. by apply /IM_P; exists false. Qed.

Lemma set2_hi z x y: inc z (doubleton x y) -> z = x \/ z = y.
Proof. by move/IM_P => [][]; [left | right]. Qed.

Hint Resolve set2_1 set2_2: fprops.

Lemma set2_P z x y : inc z (doubleton x y) <-> (z = x \/ z = y).
Proof. split; [apply: set2_hi | by case => ->; fprops]. Qed.

Lemma doubleton_inj  x y z w:
  doubleton x y = doubleton z w -> (x = z /\ y = w) \/ (x = w /\ y = z). 
Proof.
move=> eql. 
have x_zw: inc x (doubleton z w) by rewrite -eql; fprops.
have y_zw: inc y (doubleton z w) by rewrite -eql; fprops.
have w_xy: inc w (doubleton x y) by rewrite eql; fprops.
have z_xy: inc z (doubleton x y) by rewrite eql; fprops.
case: (set2_hi x_zw) => xs.
  left; split => //; case: (set2_hi w_xy) => //.
  by case: (set2_hi y_zw); move: xs => -> ->.
case: (set2_hi y_zw);first by right.
by case: (set2_hi z_xy); move => -> ->; left.
Qed.

Lemma set2_ne x y: nonempty (doubleton x y).
Proof. by exists x; fprops. Qed.

Lemma sub_set2 x y z: inc x z -> inc y z -> sub (doubleton x y) z.
Proof. by move=> xz yz t /set2_P [] ->. Qed.

Lemma set2_C : commutative doubleton.
Proof. 
move => a b; apply:extensionality; apply/sub_set2 /set2_P;fprops.
Qed.

Lemma set2_pr a b X:
  inc a X -> inc b X ->
  (forall z, inc z X -> z = a \/ z = b) ->
  X = doubleton a b.
Proof.
move => ax bx h; set_extens t; first by move => ta; apply /set2_P /h.
by case /set2_P => ->.
Qed.


(** [singleton x] is a set with one element *)

Definition singleton x := doubleton x x.

Lemma set1_eq x y: inc y (singleton x) -> y = x.
Proof. by case/set2_P. Qed.

Lemma set1_1 x: inc x (singleton x).
Proof. by apply/set2_P;left. Qed.

Hint Resolve set1_1: fprops.

Lemma set1_P y x: inc y (singleton x) <-> (y = x).
Proof. by split; [ apply:set1_eq| move => ->; fprops ]. Qed.

Lemma set1_inj: injective singleton. 
Proof. by move => x y eq; apply: set1_eq; rewrite -eq; fprops. Qed.

Lemma set1_ne x: nonempty (singleton x).
Proof. by apply: set2_ne. Qed.

Lemma set1_sub x X: inc x X -> sub (singleton x) X.
Proof. by move=> ixy; apply: sub_set2. Qed.

Hint Resolve set1_ne: fprops.

Definition C0 := emptyset.
Definition C1 := singleton C0.
Definition C2 := doubleton C0 C1. 

Lemma C1_P x:  inc x C1 <-> x = C0.
Proof. exact: set1_P. Qed.

Lemma C1_ne_C0: C1 <> C0.
Proof. by apply /nonemptyP; exists C0; apply: set1_1. Qed.

Lemma C0_ne_C1: C0 <> C1.
Proof. exact: nesym C1_ne_C0. Qed.

Lemma C2_P x: inc x C2 <-> (x = C0 \/ x = C1).
Proof. exact: set2_P. Qed.

Lemma inc_C0_C2: inc C0 C2.
Proof. exact: set2_1. Qed. 

Lemma inc_C1_C2: inc C1 C2.
Proof. exact: set2_2. Qed.

Hint Resolve C0_ne_C1 C1_ne_C0: fprops.
Hint Resolve inc_C0_C2 inc_C1_C2: fprops.


Ltac Ytac eq:= 
  match goal with
  | |- context  [Yo ?p _ _ ] =>
      case: (p_or_not_p p) => eq; 
   [rewrite (Y_true eq) | rewrite (Y_false eq) ]
end.

Ltac Ytac0 := match goal with
  | h: ?p |- context  [Yo ?p  _ _ ] => rewrite (Y_true h)
  | h: (~ ?p) |- context  [Yo ?p  _ _ ] => rewrite (Y_false h)
  | h: ?j <> ?i |- context  [Yo (?i = ?j) _ _ ] 
     => rewrite (Y_false (nesym h))
  | |- context  [Yo (?i = ?i) _ _ ] => rewrite (Y_true (refl_equal i))
  | |- context  [Yo (C0 = C1) _ _ ] => rewrite (Y_false C0_ne_C1)
  | |- context  [Yo (C1 = C0) _ _ ] => rewrite (Y_false C1_ne_C0)
  | |- context  [Yo ?p  ?x ?x ] => rewrite (Y_same p x)
end.

Definition alls (X: Set)(P: property) := forall a, inc a X -> P a.

(** A set is small if it has zero or one elements *)
(** [singletonp x]  says [x] has the form [singleton y] *)
Definition small_set x := singl_val (inc ^~x).
Definition singletonp x := exists u, x = singleton u.
Definition doubletonp x:= exists a b, a <> b /\ x = doubleton a b.

Lemma small0: small_set emptyset.
Proof. by move=> u v /= /in_set0. Qed.

Lemma small1 x: small_set (singleton x).
Proof. by move=> u v /set1_P -> /set1_P ->. Qed.

Lemma set1_pr x X: inc x X -> alls X (eq^~ x) -> X = singleton x.
Proof. 
move=> xX zy; set_extens t; first by move => ty;apply/set1_P;apply: zy.
by move /set1_P ->. 
Qed.

Lemma set1_pr1 x X: nonempty X ->  alls X (eq^~ x) -> X = singleton x.
Proof.
by move=> [y yx] p; apply: set1_pr => //; rewrite - (p _ yx).
Qed.

Lemma singletonP x: singletonp x <-> (nonempty x /\ small_set x).
Proof. 
split; first by move=> [z ->]; split;[fprops | apply: small1].
by move=> [[y yx] sx]; exists y; apply: (set1_pr yx) => z zx; apply: sx.
Qed.

Lemma small_set_pr x: small_set x -> x = emptyset \/ singletonp x.
Proof. 
move=> sx; case: (emptyset_dichot x); first by left.
by move=> ne; right; apply/singletonP.
Qed.

Lemma subset1P X x : sub X (singleton x) <-> (X = emptyset \/ X = singleton x).
Proof.
split; last by case => ->; fprops. 
move => xsx; case: (emptyset_dichot X); first by left.
by move => nea; right; apply: set1_pr1 => // z /xsx /set1_P.
Qed.
 
Lemma sub1setP X x : sub (singleton x) X <-> inc x X.
Proof. by split; [ apply; fprops | move => xX t /set1_P ->]. Qed.

End Little.

Export Little. 


(** ** Image *)
Module Image. 

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

Definition fun_image (x : Set) (f : fterm) := IM (fun a : x => f (Ro a)). 

Lemma funI_i x f y: inc y x -> inc (f y) (fun_image x f).
Proof. by move => yx; apply/IM_P; exists (Bo yx); rewrite (B_eq yx). Qed.

Lemma funI_P f x y:
  inc y (fun_image x f) <-> exists2 z, inc z x & y = f z.
Proof. 
split; last by move=> [a ax ->]; apply:funI_i.
case/IM_P => a <-; exists (Ro a) => //; apply: R_inc.
Qed.

End Image.
Export Image.

(** ** Complement *)
Module Complement. 

(** Set of all elements in a not in b *)

Definition complement (A B : Set) := Zo A (fun x : Set => ~ inc x B).
Notation "a -s b" := (complement a b) (at level 50).

Lemma setC_P A B x: inc x (A -s B) <-> (inc x A /\ ~ inc x B).
Proof. exact: Zo_P. Qed.

Lemma setC_i x A B: inc x A -> ~ inc x B -> inc x (A -s B).
Proof. by move => xa xb; apply /setC_P. Qed.

Hint Resolve  setC_i: fprops.

Lemma nin_setC x A B: inc x A -> ~ inc x (A -s B) -> inc x B.
Proof. move=> xa nx_cab; ex_middle h; case: nx_cab; fprops. Qed.

Lemma empty_setC A B: A -s B = emptyset -> sub A B.
Proof.  
move=> eql t ta; apply:(nin_setC ta); rewrite eql; apply: in_set0.
Qed. 

Lemma setC_T A B: sub A B -> A -s B = emptyset.
Proof. 
by move => sab; apply /set0_P => x /setC_P [xa] []; apply: sab.
Qed.

Lemma sub_setC A B: sub (A -s B) A.
Proof. by move => t;case /setC_P. Qed. 

Lemma setC_ne A B: ssub A B -> nonempty (B -s A).
Proof. 
move=> [s neq]; apply /nonemptyP;dneg ceq; move: (empty_setC ceq).
by apply: extensionality.
Qed. 

Lemma setC_K A B: sub A B -> B -s (B -s A) = A.
Proof. 
move=> sax; set_extens t.
  by move /setC_P => [tx /setC_P notp];ex_middle h; case: notp.
move =>ta; apply/setC_P; split; [apply: (sax _ ta) | by apply/setC_P; case ].
Qed.

Lemma setC_v A: A -s A = emptyset.
Proof. by apply:setC_T. Qed. 

Lemma setC_0 A: A -s emptyset = A.
Proof. 
apply: extensionality; first by apply:sub_setC.
move => y yA; apply/setC_P; split => //;apply /in_set0.
Qed.

Lemma set_SC A B C : sub A B -> sub (A -s C) (B -s C).
Proof.
by move => sab x /setC_P [xa xnc]; apply /setC_P;split =>//; apply: sab.
Qed.

Lemma set_CS A B C : sub A B -> sub (C -s B) (C -s A).
Proof.
move => sac t/setC_P [tc ntb]; apply /setC_P.
by split => //;dneg ta; apply: sac.
Qed.

Lemma set_CSS A B C D : sub A C -> sub D B -> sub (A -s B)(C -s D).
Proof. move => sAC sDB; apply: (sub_trans (set_CS sDB) (set_SC sAC)). Qed.

Lemma set_CSm A B X:
  sub A X -> sub B X -> (sub A B <-> sub (X -s B) (X -s A)).
Proof.
move=> ax bx; split; first by apply: set_CS.
by move => h; rewrite -(setC_K ax) -(setC_K bx); apply: set_CS.
Qed.

Lemma subsetC_P A B E : sub A E -> sub B E ->
  (sub A (E -s B) <-> sub B (E -s A)).
Proof.
move => aE bE;split => i1 t ts;apply/setC_P; split.
- by apply bE.
- by move /i1 => /setC_P; case.
- by apply aE.
- by move /i1 => /setC_P; case.
Qed.

Lemma subCset_P A B E: sub A E -> sub B E ->
  (sub (E -s A) B <-> sub (E -s B) A).
Proof. 
move => ae be; rewrite -{2} (setC_K ae) -{1} (setC_K be).
apply: subsetC_P; apply: sub_setC.
Qed.

(** [a -s1 b] contains all elements of [a] but [b] *)

Notation "a -s1 b" := (a -s (singleton b))  (at level 50). 

Lemma setC1_P x A b: inc x (A -s1 b) <-> (inc x A /\ x <> b).
Proof. 
split; first by case /setC_P => xa /set1_P xb. 
by move => [xA xb]; apply /setC_P; split => //;apply /set1_P.
Qed.

Lemma setC1_1 x A: ~ (inc x (A -s1 x)).
Proof. by apply /setC_P=> [[_]] /set1_P. Qed.

Lemma setC1_proper A x : inc x A -> ssub (A -s1 x) A.
Proof.
move => xa; split; first by apply: sub_setC.
move => eq1; move: xa; rewrite -eq1; exact: setC1_1.
Qed.

Lemma setC1_eq A x: ~(inc x A) -> A -s1 x = A.
Proof.
move=> h.
set_extens t; first by move => /setC1_P [].
by move => tA; apply /setC1_P; split => // tx; case: h; rewrite - tx.
Qed.


End Complement.
Export Complement.

(** ** Union *)
Module Union. 

(** Uaux: like Zo_rec, but f has a different type. *)

Section UnionDef.
Variable (I:Set)(f : I->Set).

CoInductive Uaux : Set := Uaux_c : forall a:I, f a -> Uaux.

Definition uniont := 
   IM (fun a : Uaux  => (let:  Uaux_c u v := a in @Ro (f u) v)). 
End UnionDef.

Lemma setUt_P (I:Set) (f:I->Set) x:
  inc x (uniont f) <-> exists z, inc x (f z).
Proof. 
split; first by move/IM_P=>[a <-]; case: a => b fb; exists b; apply: R_inc.
by move => [z xf]; apply /IM_P;exists (Uaux_c (Bo xf)); rewrite B_eq. 
Qed.

Definition union (X: Set) := uniont (@Ro X). 

Lemma setU_P z x:
  inc x (union z) <-> exists2 y, inc x y & inc y z.
Proof. 
split; first by move/setUt_P => [y xr]; exists (Ro y); [ | apply: R_inc].
by move => [y xy yz]; apply/setUt_P; exists (Bo yz); rewrite (B_eq yz).
Qed. 

Lemma setU_i x y z: inc x y -> inc y z -> inc x (union z).
Proof. by move => xy yz; apply/setU_P; exists y. Qed.

Lemma setU_hi x z: inc x (union z) -> exists2 y, inc x y & inc y z.
Proof. by case /setU_P => t pt; exists t. Qed.

Lemma setU_s1 y z: inc y z -> sub y (union z).
Proof. by move=> yz x xy ; apply: setU_i yz. Qed.

Lemma setU_s2 x z: (forall y, inc y z -> sub y x) -> sub (union z) x.
Proof. by move=> H t /setU_P [a ta /H]; apply. Qed. 

Lemma setU_0: union emptyset = emptyset.
Proof. by apply /set0_P => x /setU_P [y _ /in_set0]. Qed.

(** Union of two sets *)

Definition union2 (x y : Set) := union (doubleton x y).

Notation "a \cup b" := (union2 a b) (at level 50).

Lemma setU2_hi x A B: inc x (A \cup B) -> inc x A \/ inc x B.
Proof. by case /setU_P => t tab /set2_P [] <-; [left | right]. Qed.

Lemma setU2_1 x A B: inc x A -> inc x (A \cup B).
Proof. move => xa; apply (setU_i xa); fprops. Qed.

Lemma setU2_2 x A B: inc x B -> inc x (A \cup B).
Proof. move => xb;apply: (setU_i xb); fprops. Qed.

Hint Resolve setU2_1 setU2_2: fprops.

Lemma setU2_P x A B: inc x (A \cup B) <-> (inc x A \/ inc x B).
Proof. by split; [apply: setU2_hi | case; fprops ]. Qed. 

Lemma subsetU2l A B: sub A (A \cup B).
Proof. move => x; fprops. Qed.

Lemma subsetU2r A B: sub B (A \cup B).
Proof. move => x; fprops. Qed.

Lemma setU2_C: commutative union2.
Proof. 
move => x y; set_extens t; case/setU2_P => ts; apply /setU2_P; fprops.
Qed.

Lemma setU2_id: idempotent union2.
Proof. move => x;set_extens t; [ by case /setU2_P | fprops]. Qed.

Lemma setU2_A: associative union2.
Proof.
move => a b c; rewrite setU2_C.
set_extens t; case /setU2_P; (try case /setU2_P); move => tx;
   apply/setU2_P;fprops; left; apply/setU2_P;fprops. 
Qed.

Lemma setU2_CA : left_commutative union2.
Proof. by move =>A B C; rewrite !setU2_A (setU2_C B). Qed.

Lemma setU2_AC : right_commutative union2.
Proof. by move => A B C;rewrite -!setU2_A (setU2_C B). Qed.

Lemma set2_UUl : left_distributive union2 union2.
Proof.
by move => A B C; rewrite setU2_A !(setU2_AC _ C) -(setU2_A _ C) setU2_id.
Qed.

Lemma set2_UUr : right_distributive union2 union2.
Proof. move => a b c; rewrite !(setU2_C a); exact: set2_UUl. Qed.

Lemma setU2_S1 A B C : sub A B -> sub (C \cup A) (C \cup B).
Proof. move=> sAB t; case /setU2_P => ts; apply/setU2_P; fprops. Qed.

Lemma setU2_S2 A B C : sub A B -> sub (A \cup C) (B \cup C).
Proof. by move=> sAB; rewrite -!(setU2_C C); exact: setU2_S1. Qed.

Lemma setU2_SS A B C D : sub A C -> sub B D -> sub (A \cup B) (C \cup D).
Proof.  
move => s1 s2; apply: sub_trans (setU2_S1 (C:=C) s2); apply: (setU2_S2 s1).
Qed.

Lemma setU2_12S A B C: sub A C -> sub B C -> sub (A \cup B) C.
Proof. rewrite -{3}(setU2_id C); exact:setU2_SS. Qed.

Lemma subU2_setP A B C : (sub (B\cup C) A) <-> (sub B A /\ sub C A).
Proof. 
split. 
  move => h;split; apply: (sub_trans _ h);[apply: subsetU2l |apply: subsetU2r].
by move => [h1 h2];apply: setU2_12S.
Qed.

Lemma sub_setU2 A B C : (sub A B) \/ (sub A C) -> sub A (B \cup C).
Proof. 
case => h; apply: (sub_trans h);[apply: subsetU2l |apply: subsetU2r].
Qed.

Lemma setU2id_Pl A T: sub A T <-> A \cup T = T.
Proof. 
split; last by move => <-;apply: subsetU2l.
move => sat; apply: extensionality; last by apply: subsetU2r.
by rewrite - {2}(setU2_id T); apply:setU2_S2.  
Qed.

Lemma setU2id_Pr A T: sub A T <-> T \cup A = T.
Proof. rewrite setU2_C; exact: setU2id_Pl. Qed.

Lemma setU2_0 A : A \cup emptyset  = A.
Proof. apply/setU2id_Pr; fprops. Qed.

Lemma set0_U2 A : emptyset \cup A = A.
Proof. rewrite setU2_C; exact: setU2_0. Qed.

Lemma setU_1 x: union (singleton x) = x.
Proof. apply: setU2_id. Qed.

Lemma setU2_11 x y: (singleton x) \cup (singleton y) = doubleton x y.
Proof. apply:set2_pr; fprops => z /setU2_P [] /set1_P ->; fprops. Qed.

Lemma subCset_P2 A B C : sub (A -s B) C <-> sub A (B \cup C).
Proof.
split => h t.
  move => ta; apply/setU2_P; case: (inc_or_not t B) => ax; [by left | right].
  by apply:h; apply/setC_P.
by case /setC_P => ta tb; case/setU2_P: (h _ ta). 
Qed.

Lemma setU2_eq0P A B : (A \cup B = emptyset) <-> (A = emptyset /\ B = emptyset).
Proof. 
split; [move => sube | by  move => [-> ->]; rewrite setU2_id ].
split;  apply /set0_P => t ta;case: (in_set0 (x:= t));
  rewrite - sube; apply /setU2_P;fprops.
Qed.

Lemma setU2Cr1 A B:  A \cup (A -s B) = A.
Proof. apply /setU2id_Pr; apply: sub_setC. Qed.

Lemma setU2Cr2 A B:  A \cup (B -s A) = A \cup B.
Proof. 
set_extens t; case /setU2_P => t1; apply/setU2_P; fprops. 
  by right;case /setC_P:t1.
case: (inc_or_not t A)=> ta; fprops.
Qed.

Lemma setU2_Cr A T: sub A T -> A \cup (T -s A) = T.
Proof. by move => sat; rewrite setU2Cr2; apply /setU2id_Pl. Qed.


(** Union of [x] and a single element [y] *)

Notation "A +s1 b" := (A \cup (singleton b)) (at level 50).  

Lemma setU1_P A b z: inc z (A +s1 b) <-> inc z A \/ z = b.
Proof. 
split; first by case /setU2_P; [left | move /set1_P; right].
by case =>h; apply/setU2_P; [by left | right; apply/set1_P].
Qed.

Lemma setU1_1 A b: inc b (A +s1 b).
Proof. by apply/setU1_P; right. Qed.

Lemma sub_setU1 A b: sub A (A +s1 b).
Proof. by move=> x xA; apply/setU1_P; left. Qed.

Lemma setU1_r A b x: inc x A -> inc x (A +s1 b).
Proof. apply: sub_setU1. Qed.

Hint Resolve setU1_1 setU1_r sub_setU1: fprops.

Lemma setU1_eq A b: inc b A -> A +s1 b = A.
Proof. 
move=> ba; apply: extensionality; last by fprops.
by move => t /setU1_P [] // ->.
Qed.

Lemma setU1_sub A b x: sub A x -> inc b x -> sub (A +s1 b) x.
Proof. by move=> Ax bx t /setU1_P []; [ apply: Ax | move=> -> ]. Qed.

Lemma setCU_K A B: sub B A <-> (A -s B) \cup B = A.
Proof.
split; last by move => h t tb; rewrite -h; apply/setU2_P; right.  
move => BA; set_extens t; first by case /setU2_P; [ by case/setC_P| apply: BA].
move => tA; apply/setU2_P; case: (inc_or_not t B) => ty;fprops. 
Qed.

Lemma setU1_K A b: ~(inc b A) -> (A +s1 b) -s1 b = A.
Proof.
move => nba; set_extens t;first by case /setC1_P; case /setU1_P.
move => tA; apply/setC1_P; split; [fprops | dneg ta;ue ].
Qed.

Lemma setC1_K A b: inc b A -> (A -s1 b) +s1 b = A.
Proof. by move => bA; apply/setCU_K => t /set1_P ->. Qed.

Lemma setU1_inj x A B: ~(inc x A) -> ~(inc x B) ->
  A +s1 x = B +s1 x -> A = B.
Proof. by move => /setU1_K -{2} <- /setU1_K -{2} <- ->. Qed.

Lemma setC1_inj x A B: inc x A -> inc x B -> A -s1 x = B -s1 x -> A = B.
Proof. by move => /setC1_K - {2} <- /setC1_K -{2} <- ->. Qed.

Definition tripleton a b c := (doubleton a b) +s1 c. 

Lemma set3_P a b c x:
   inc x (tripleton a b c) <-> [\/ x = a , x = b | x = c].
Proof.
split; last by rewrite /tripleton;case => ->; fprops.
case /setU1_P; [case /set2_P | ]; in_TP4.
Qed.


Definition C3 := C2 +s1 C2.
Definition C4 := C3 +s1 C3.

Lemma C3_P x: inc x C3 <-> [\/ x = C0, x = C1 | x = C2].
Proof. exact:set3_P. Qed.

Lemma C4_P x: inc x C4 <-> [\/ x = C0, x = C1, x = C2 | x = C3].
Proof.
split.
  case /setU1_P; last (by constructor 4); by case /C3_P; in_TP4.
case => ->; apply/setU1_P; last (by right); left; apply /C3_P; in_TP4.
Qed.

Lemma C2_ne_C01: C2 <> C0 /\ C2 <> C1.
Proof.
split => h; first by move: inc_C0_C2; rewrite h /C0; case; case.
move: inc_C1_C2; rewrite h; move /set1_P; fprops.
Qed.

Lemma C3_ne_C012: [/\ C3 <> C0, C3 <> C1 & C3 <> C2].
Proof.
have pa: inc C0 C3 by apply/C3_P; constructor 1.
have pb: inc C1 C3 by apply/C3_P; constructor 2.
have pc: inc C2 C3 by apply/C3_P; constructor 3.
move:C2_ne_C01 => [pd pe].
split => h; first by move: pa ; rewrite h; case; case.
  by move: pb ; rewrite h; move/set1_P; fprops.
move: pc; rewrite h; case/set2_P; fprops.
Qed.


Lemma funI_set0 f: fun_image emptyset f = emptyset.
Proof. by apply /set0_P => t /funI_P [z /in_set0]. Qed.

Lemma funI_setne1 f x: fun_image x f = emptyset -> x = emptyset.
Proof.
by move => dr;apply /set0_P => t /(funI_i f); rewrite dr => /in_set0.
Qed.

Lemma funI_setne f x: nonempty x ->  nonempty (fun_image x f).
Proof. by move/nonemptyP => xE; apply/nonemptyP=> /funI_setne1. Qed.

Lemma funI_set2 f a b: fun_image (doubleton a b) f = doubleton (f a) (f b).
Proof. 
set_extens t; first by move/funI_P => [z] /set2_P;case => -> <-; fprops.
move /set2_P; case => ->; apply: funI_i; fprops.
Qed.

Lemma funI_set1 f x: fun_image  (singleton x) f = singleton (f x).
Proof. apply:funI_set2. Qed.

Lemma funI_setU f X: 
   fun_image (union X) f = union (fun_image X (fun_image^~ f)).
Proof.
set_extens t.
  move /funI_P => [y /setU_P[x yx xz] ->].
  by apply/setU_P; exists (fun_image x f); apply:funI_i.
move/setU_P => [x tx /funI_P [y yz dy]].
move:tx; rewrite dy; move/funI_P => [u ua ->]; apply: funI_i.
apply (setU_i ua yz).
Qed.

Lemma funI_setU2 f: {morph (fun_image ^~ f): x y / x \cup y}.
Proof. by move => x y;rewrite /union2 funI_setU funI_set2. Qed.

Lemma funI_setU1 g X a:
   fun_image (X +s1 a) g = fun_image X g +s1 (g a).
Proof. by rewrite funI_setU2 funI_set1. Qed.

Lemma funI_S f a b: sub a b -> sub (fun_image a f) (fun_image b f).
Proof. by move => h t /funI_P [z za ->]; apply: funI_i; apply: h. Qed.


(** If a set [E] contains a unique [x] satisfying [p], then [select p E] is this element 
*)

Definition select (p: property) (E: Set) := union (Zo E p).

Lemma select_uniq (p: property) E: 
  (singl_val2 (inc ^~ E) p) ->
  forall x, inc x E -> p x -> x = (select p E).
Proof.
move => h x xE px; rewrite /select.
suff: (Zo E p) = singleton x by move => ->; rewrite setU_1.
by apply: set1_pr; [ apply: Zo_i | move => z; case/Zo_P => ze pz; apply: h].
Qed.

Lemma select_pr (p : property) E:
  (exists2 x, inc x E & p x) -> (singl_val2 (inc ^~ E) p) ->
  (p (select p E) /\ inc (select p E) E).
Proof. by move => [z ze pz] pc; rewrite -(select_uniq pc ze pz). Qed.

Lemma select_pr1 (p : property) E:
  (exists2 x, inc x E & p x) -> (singl_val2 (inc ^~ E) p) ->
  p (select p E).
Proof. move => ha hb; exact: (proj1 (select_pr ha hb)). Qed.


End Union. 

Export Union. 

(** ** Powerset *)
Module Powerset. 

(** Forall all [p:X-> 2], we consider the inverse image of [0]. 
The set of all these quantities is the set of subsets of [X] *)

Definition powerset (x : Set) := 
 IM (fun p : x -> C2 =>
    Zo x (fun y : Set => forall hyp : inc y x, Ro (p (Bo hyp)) = C0)).

Lemma setP_i y x : sub y x -> inc y (powerset x). 
Proof. 
have fp: forall a:x, inc (Yo (inc (Ro a) y) C0 C1) C2.
  by move => a; Ytac h; fprops.
move => sxy; apply/IM_P; exists (fun  a => Bo (fp a)); set_extens t.
  move /Zo_P => [tz h]; move: (h tz); rewrite B_eq. 
  by Ytac w; [ move: w; rewrite B_eq | move: C1_ne_C0 ].
by move => ty; apply:(Zo_i (sxy _ ty)) => hyp; rewrite B_eq B_eq; Ytac0.
Qed.

Lemma setP_hi x y: inc x (powerset y) -> sub x y.
Proof. by case /IM_P => t <-; apply: Zo_S. Qed.

Lemma setP_P x y : inc x (powerset y) <-> sub x y.
Proof. split; [ apply: setP_hi | apply: setP_i]. Qed. 

Lemma setP_Ti x: inc x (powerset x).
Proof. by apply/setP_P. Qed.

Lemma setP_0i x: inc emptyset (powerset x).
Proof. apply/setP_P; fprops. Qed.

Lemma setP_S a b: sub a b <-> sub (powerset a) (powerset b).
Proof. 
split => sab.
  move=> x /setP_P sxa; apply /setP_P; apply: (sub_trans sxa sab).
by apply /setP_P;apply: sab; apply /setP_P.
Qed.

Lemma setP_0: powerset emptyset = singleton emptyset.
Proof. 
set_extens t; first by move /setP_P /sub_set0 ->; fprops.
move /set1_P ->; apply: setP_0i.
Qed.

Lemma setP_1 x: powerset (singleton x) = doubleton emptyset (singleton x).
Proof. 
set_extens t.
  by move /setP_P /subset1P => [] ->; apply/set2_P; [left | right].
case /set2_P => ->; fprops; apply /setP_P; fprops.
Qed.

Lemma setP_00 : powerset (powerset emptyset) = C2.
Proof. rewrite setP_0 setP_1 //. Qed.

End Powerset. 
Export Powerset.


(** ** Intersection *)
Module Intersection. 


(** Intersection: set of all [z] in some element of [x], 
  that are in all elements of [x]
*) 

Definition intersection (x : Set) :=
  Zo (union x) (fun y : Set => forall z : Set, inc z x -> inc y z). 

Lemma setI_0: intersection emptyset = emptyset.
Proof. apply /set0_P => t /Zo_S;rewrite setU_0; apply /in_set0. Qed.

Lemma setI_i x a:
  nonempty x -> (forall y, inc y x -> inc a y) -> inc a (intersection x). 
Proof. 
move => [y yx] all_ayx; apply: Zo_i=> //.  
move: (all_ayx _ yx) (yx); apply: setU_i.
Qed.

Lemma setI_hi x a y: inc a (intersection x) -> inc y x -> inc a y.
Proof. move/Zo_hi; apply. Qed.

Lemma setI_s1 x y: inc y x -> sub (intersection x) y.
Proof. by move=> yx t ti; move: ti yx; apply: setI_hi. Qed.

Lemma setI_s2 x y: nonempty y ->
  (forall i, inc i y -> sub x i) ->  sub x (intersection y).
Proof. by move=> ne hyp t tx; apply:(setI_i ne) => v /hyp; apply. Qed.

Lemma setI_sub2 x y: (forall i, inc i y -> sub i x) -> sub (intersection y) x.
Proof. 
move=> hyp.
case: (emptyset_dichot y) => ie; first by  rewrite ie setI_0; fprops.
case: ie => i iy; exact:(sub_trans (setI_s1 iy) (hyp _ iy)).
Qed.


(** Intersection of two sets *)

Definition intersection2 x y := intersection (doubleton x y).

Notation "a \cap b" := (intersection2 a b) (at level 50).

Lemma setI2_i x A B: inc x A -> inc x B -> inc x (A \cap B).
Proof. 
move => xa xb.
by apply: setI_i; [ apply: set2_ne | move=> t /set2_P [] -> ].
Qed.

Hint Resolve setI2_i : fprops.

Lemma setI2_1 A B: sub (A \cap B) A.
Proof. move => x xi; apply: (setI_hi xi); fprops. Qed.

Lemma setI2_2 A B: sub(A \cap B)  B.
Proof. move => x xi; apply: (setI_hi xi); fprops. Qed.

Lemma setI2_P x A B: inc x (A \cap B) <-> (inc x A /\ inc x B).
Proof. 
split => [xi | [xa xb]]; last by fprops.
by split; [apply: (setI2_1 xi) | apply:(setI2_2 xi)].
Qed.

Lemma subsetI2l A B: sub (A \cap B) A.
Proof. move => x;apply: setI2_1. Qed.

Lemma subsetI2r A B: sub (A \cap B) B.
Proof. move => x;apply: setI2_2. Qed.

Lemma setI2_id: idempotent intersection2.
Proof.  
by move => A;set_extens t; [case/setI2_P | move=> tA; apply/setI2_P; split].
Qed.

Lemma setI_1 x: intersection (singleton x) = x.
Proof. apply: setI2_id. Qed.

Lemma setI2_C: commutative intersection2.
Proof. move => A B; set_extens t; move /setI2_P => [pa pb]; fprops. Qed.

Lemma setI2_A: associative intersection2.
Proof. 
move => A B C; rewrite setI2_C.
set_extens t; case /setI2_P; case /setI2_P=> tx ty tz; apply/setI2_P;fprops.
Qed.

Lemma setI2_CA : left_commutative intersection2.
Proof. by move =>A B C; rewrite !setI2_A (setI2_C B). Qed.

Lemma setI2_AC : right_commutative intersection2.
Proof. by move => A B C;rewrite -!setI2_A (setI2_C B). Qed.

Lemma setI2_4 A B C D:
  (A \cap B) \cap (C \cap D)= (A \cap C) \cap (B \cap D).
Proof.
rewrite -2! setI2_A; apply:f_equal.
by rewrite 2! setI2_A (setI2_C B C). 
Qed.

Lemma set2_IIl : left_distributive intersection2 intersection2.
Proof.
by move => A B C; rewrite setI2_A !(setI2_AC _ C) -(setI2_A _ C) setI2_id.
Qed.

Lemma set2_IIr : right_distributive intersection2 intersection2.
Proof. move => A B C; rewrite !(setI2_C A); exact: set2_IIl. Qed.

Lemma setI2_S1 A B C : sub A B -> sub (C \cap A) (C \cap B).
Proof. move=> sAB t; case /setI2_P => ta tc; fprops. Qed.

Lemma setI2_S2 A B C : sub A B -> sub (A \cap C) (B \cap C).
Proof. by move=> sAB; rewrite -!(setI2_C C); exact: setI2_S1. Qed.

Lemma setI2_SS A B C D : sub A C -> sub B D -> sub (A \cap B) (C \cap D).
Proof.  
move => s1 s2; apply: sub_trans (setI2_S1 (C:=C) s2); apply: (setI2_S2 s1).
Qed.

Lemma setI2_12S A B C: sub C A -> sub C B -> sub C (A \cap B).
Proof. rewrite -{3}(setI2_id C); exact:setI2_SS. Qed.

Lemma subsetI2_P A B C : sub C (A\cap B)  <-> (sub C A /\ sub C B).
Proof. 
split; last by move => [h1 h2]; apply: setI2_12S.
move => h;split; apply: (sub_trans  h); [apply: subsetI2l |apply: subsetI2r].
Qed.

Lemma subI2_set A B C : (sub A C) \/ (sub B C) -> sub (A \cap B) C.
Proof. 
case => h; apply: (sub_trans _ h);[apply: subsetI2l |apply: subsetI2r].
Qed.

Lemma setIC2 A B C:  A \cap (B -s C) =  A \cap B -s  (A \cap C).
Proof.
set_extens t.
  move => /setI2_P [tA /setC_P [tb ntc]]; apply /setC_P; split; fprops.
  by move /setI2_P => [].
move => /setC_P [/setI2_P [ha hb] /setI2_P hc]; apply/setI2_P; split => //.
by apply/setC_P; split => //; dneg hd.
Qed.

Lemma setI2id_Pl A T: sub A T <-> A \cap T = A.
Proof. 
split; last by move => <-;apply: subsetI2r.
move => sat; apply: extensionality; first by apply: subsetI2l.
by rewrite - {1}(setI2_id A); apply:setI2_S1.  
Qed.

Lemma setI2id_Pr A T: sub A T <-> T \cap A = A.
Proof. rewrite setI2_C; apply: setI2id_Pl. Qed.

Lemma setPI : morphism_2 powerset intersection2  intersection2.
Proof. 
move => A B; set_extens t.
  move/setP_P /subsetI2_P => [ta tb];apply/setI2_P.
  by split; apply/setP_P.
by move /setI2_P=> [ta tb]; apply/setP_P; apply: setI2_12S;apply/setP_P.
Qed.

Lemma set_UI2l: left_distributive union2 intersection2.
Proof.
move => A B C; set_extens t.
  case /setU2_P. 
    by case /setI2_P => ta tb;apply/setI2_P; split; apply/setU2_P; left.
  by move => tc;apply/setI2_P; split; apply/setU2_P; right.
case/setI2_P;case /setU2_P=> tac; case /setU2_P => tbc;apply/setU2_P; fprops.
Qed.

Lemma set_UI2r: right_distributive union2 intersection2.
Proof. move => a b c; rewrite !(setU2_C a); apply: set_UI2l. Qed.

Lemma set_IU2l: left_distributive intersection2 union2.
Proof.
move => A B C; set_extens t.
  case /setI2_P; case /setU2_P=> tab tc; apply/setU2_P; fprops.
case/setU2_P; case/setI2_P => tab tc; apply/setI2_i => //; apply/setU2_P;fprops.
Qed.

Lemma set_IU2r: right_distributive intersection2 union2.
Proof. move => a b c; rewrite !(setI2_C a); apply: set_IU2l. Qed.

Lemma set_U2K A B: (A \cup B) \cap A = A.
Proof.
apply: extensionality; first by apply:subsetI2r.
apply/subsetI2_P;split; [ apply:subsetU2l | fprops].
Qed.

Lemma set_K2U A B: A \cap (B \cup A) = A.
Proof. rewrite setU2_C setI2_C; exact: set_U2K. Qed.

Lemma set_I2K A B: (A \cap B) \cup A = A.
Proof.
apply: extensionality; last by apply:subsetU2r.
apply/subU2_setP;split; [ apply:subsetI2l | fprops].
Qed.

Lemma set_K2I A B: A \cup (B \cap A) = A.
Proof. rewrite setU2_C setI2_C; exact: set_I2K. Qed.

Lemma setU2_ni x A B: ~inc x (A\cup B) -> (~ inc x A  /\ ~ inc x B).
Proof. by move => h; split;dneg xab; apply/setU2_P; [left | right]. Qed.

Lemma setI2_ni x A B: ~inc x (A\cap B) -> (~ inc x A \/ ~ inc x B).
Proof. 
move => h; case: (inc_or_not x A); fprops => xa; right => xB; case: h; fprops.
Qed.

Lemma setC_ni x A B: ~inc x (A -s B) -> (~ inc x A \/ inc x B).
Proof. 
move => h; case: (inc_or_not x B) => nxb; [by right  |  left].
move => xa; case: h; fprops.
Qed.

Lemma set_CU2 A B X: X -s (A\cup B) = (X -s A) \cap (X -s B).
Proof.
set_extens t.
  case/setC_P => tX tu; apply/setI2_P; move: (setU2_ni tu) => [ta tb].
  split; fprops.
case /setI2_P => /setC_P [tx ta] /setC_P [_] tb.
by apply/setC_P;split; [ | case/setU2_P].
Qed.

Lemma set_CI2 A B X: X -s (A\cap B) = (X -s A) \cup (X -s B).
Proof.
set_extens t.
  case/setC_P => tX tu; apply/setU2_P; case: (setI2_ni tu) => ti; fprops.
by case /setU2_P => /setC_P [ta tab]; apply/setC_P;split => //; case/setI2_P.
Qed.

Lemma setCI2_pr1 A B E: sub A E -> A -s  B = A \cap (E -s B).
Proof.
move => ae; set_extens t.
  case /setC_P => ta tb; apply/setI2_P; split; first by exact. 
  by apply/setC_P; split; [ apply: ae |].
case /setI2_P => ta /setC_P [_] tb; fprops.
Qed.

Lemma set_CC A B E: sub B E -> (E -s (A -s B)) = (E -s A) \cup B.
Proof.
move => be; set_extens t.
  case/setC_P => te td; apply/setU2_P. 
  case: (setC_ni td)=> ta; [left | right]; fprops.
move => h; apply /setC_P;case /setU2_P :h.
  by case /setC_P => te ta;split => //;case/setC_P.
by move => tB;split; [ apply: be |case/setC_P ].
Qed.

Lemma setI2_Cr A B : (A \cap B) \cup (A -s B) = A.
Proof. by rewrite set_UI2l  setU2Cr1  setU2Cr2 set_K2U. Qed.

Lemma setCU2_l A B C : (A \cup B) -s C = (A -s C) \cup (B -s C).
Proof. 
set_extens t. 
  case/setC_P => /setU2_P [] tab tc; apply/setU2_P; fprops.
case/setU2_P => /setC_P [tab tc];apply/setC_P; split; fprops. 
Qed.

Lemma setCU2_r A B C : A -s (B \cup C) = (A -s B) \cap (A -s C).
Proof. 
set_extens t. 
  case/setC_P => ta /setU2_ni [tb tc]; apply/setI2_P; fprops. 
case/setI2_P => /setC_P [ta tb] /setC_P [_] tc.
by apply/setC_P;split; [ |  case /setU2_P].
Qed.

Lemma setCI2_l A B C : (A \cap B) -s C = (A -s C) \cap (B -s C).
Proof.
set_extens t. 
  by case/setC_P;case/setI2_P => ta tb tc; apply/setI2_P;split; apply/setC_P.
case/setI2_P => /setC_P [ta tc] /setC_P  [tb _]; apply/setC_P; fprops. 
Qed.

Lemma setCI2_r A B C : A -s (B \cap C) = (A -s B) \cup (A -s C).
Proof. 
set_extens t. 
  case/setC_P => ta tbc; apply/setU2_P; case:(setI2_ni tbc)=> tb; fprops.
by case/setU2_P; case/setC_P => ta tc; apply/setC_P; split => //; case /setI2_P.
Qed.

Lemma setCC_l A B C : (A -s B) -s C = A -s (B \cup C).
Proof. 
set_extens t; case /setC_P.
  by case /setC_P => ta tb tc; apply/setC_P; split; [ | case/setU2_P ].
move => ta /setU2_ni [tb tc]; apply/setC_P;fprops.
Qed.

Lemma setCC_r A B C : A -s (B -s C) = (A -s B) \cup (A \cap C).
Proof. 
set_extens t. 
  case /setC_P => ta tbc; apply/setU2_P;case: (setC_ni tbc) => tbc'; fprops.
by case /setU2_P; [case /setC_P => ta tb | case /setI2_P => ta tc];
    apply/setC_P;split => // ;case /setC_P.
Qed.

(** Two sets are disjoint if the intersection is empty *)

Definition disjoint (x y: Set) := x \cap y = emptyset.
Definition disjointVeq (x y: Set) := x = y \/ disjoint x y.

Ltac empty_tac1 u :=
  case: (in_set0 (x:= u));
  match goal with 
      H: ?x = emptyset |- _ => rewrite - H 
    | H: emptyset = ?x |- _ =>  rewrite H 
    | H: disjoint _ _ |- _ => rewrite - H; apply /setI2_P; split end;
   fprops. 

Lemma setI2_0 A : disjoint A emptyset.
Proof. apply/setI2id_Pr;fprops. Qed.

Lemma set0_I2 A : disjoint emptyset A.
Proof. rewrite /disjoint setI2_C; exact: setI2_0. Qed.

Lemma disjoint_pr A B:
  (forall x, inc x A -> inc x B -> False) -> disjoint A B.
Proof. move=> p; apply /set0_P => u; case/setI2_P; apply: p. Qed.

Lemma set_IC1r A B:  A \cap (A -s B) =  A -s B.
Proof. apply/ setI2id_Pr; apply: sub_setC. Qed.

Lemma set_I2Cr A B: disjoint B (A -s B).
Proof. by apply: disjoint_pr => u uy; case /setC_P. Qed.

Ltac mdi_tac v:= match goal with 
 | |- ?a = ?b \/ _ 
     => case: (equal_or_not a b); first (by left); move=> v; 
        right; apply: disjoint_pr
 | |- disjointVeq ?a ?b 
    => case: (equal_or_not a b); first (by left); move=> v; 
     right; apply: disjoint_pr
 end.

Lemma subsets_disjoint_P A B E: sub A E ->
  (sub A B <-> disjoint A (E -s B)).
Proof.
move => ae;split.
  by move => ab; apply: disjoint_pr => u ua; case /setC_P; move: (ab _ ua). 
move => dae t ta; ex_middle tb; empty_tac1 t; apply/setC_P; split; fprops.
Qed.

Lemma disjoint_subsets_P A E: sub A E -> forall B, 
  (disjoint A B <-> sub A (E -s B)).
Proof.
move => sae B; split.
  move => dab t ta; apply/setC_P; split; first by apply: sae. 
  move => tb;empty_tac1 t.
by move => sd; apply: disjoint_pr => u ua; move: (sd _ ua); case /setC_P.
Qed.

Lemma setCId_Pl A B: A -s B = A <->  disjoint A B.
Proof.
split => eq1. 
  apply/(disjoint_subsets_P (@sub_refl A)); rewrite eq1; fprops.
apply:extensionality; first by apply:sub_setC.
move => t tA; apply/setC_P;split => // tB; empty_tac1 t.
Qed.

Lemma subCset_P3 A B C : sub A (B -s C) <-> (sub A B /\ disjoint A C).
Proof. 
split => [h | [sab dac t ta]].
  by split; [move => t ta | apply: disjoint_pr => t ta]; case /setC_P: (h _ ta).
apply/setC_P; split; [by apply: sab | move => tC; empty_tac1 t].
Qed.

Lemma nondisjoint x A B: inc x A -> inc x B -> ~ disjoint A B.
Proof. by move=> xa xb dg; empty_tac1 x. Qed.

Lemma disjointVeq_pr x y z: disjointVeq x y -> inc z x -> inc z y -> x = y.
Proof. by move => H zx zy; case: H => //; move: (nondisjoint zx zy). Qed.

Lemma disjoint_S: symmetric_r disjoint.
Proof. by move => x y;rewrite /disjoint setI2_C. Qed.

Lemma subsetC1_P A B x: (sub A (B -s1 x)) <-> (sub A B /\ ~inc x A).
Proof.
split; first by case/subCset_P3=> [pa pb]; split => // xa; empty_tac1 x; fprops.
move => [pa pb] t ta; apply/setC1_P; split; fprops; dneg tx; ue.
Qed.

Lemma properI2_r A B : ~(sub B A) <-> ssub (A \cap B) B.
Proof.
split; first by move => nba; split;[ apply:subsetI2r | move /setI2id_Pr].
by move =>[_ hb] /setI2id_Pr.
Qed.

Lemma properI2_l A B : ~(sub A B) <-> ssub (A \cap B) A.
Proof. by rewrite setI2_C; apply: properI2_r.  Qed.

Lemma properU2_r A B : ~(sub A B) <-> ssub B (A \cup B).
Proof.  
split.
move => nba; split; [ apply:subsetU2r | dneg hh ;by apply /setU2id_Pl].
by move => [_ hb] /setU2id_Pl h; case: hb.
Qed.

Lemma properU2_l A B : ~(sub B A) <-> ssub A (A \cup B).
Proof. rewrite setU2_C; apply: properU2_r. Qed.

Lemma properI2_set A B C : (ssub B A) \/ (ssub C A) -> (ssub (B \cap C) A).
Proof. by case; apply: ssub_trans2 => t; case/setI2_P. Qed.

Lemma properI2 A B C : ssub A (B \cap C) -> (ssub A B /\ ssub A C).
Proof.
by move=> ta; split; apply: (ssub_trans1 ta) => t; case/setI2_P.
Qed.

Lemma properU2 A B C : ssub (B \cup C) A -> ssub B A /\ ssub C A.
Proof. move=> ta; split; apply: ssub_trans2 ta => t tb; fprops.  Qed.

Lemma properD A B C : ssub A (B -s C) -> ssub A B /\ disjoint A C.
Proof.
move => [pa pb]; move/subCset_P3: pa => [pc pd]; split => //; split => //.
by dneg ab; rewrite -ab; symmetry; apply/setCId_Pl. 
Qed.

End Intersection.

Export Intersection. 


(** ** Ordered Pair *)

Module Pair.

(** The object [(J x y)] is a set from which [x] and [y] can be recovered. 
   Bourbaki (English edition) uses an  axiom; he uses a doubleton in the French
   version;  we use here another doubleton and an axiom. *)

Definition kpair x y := doubleton (singleton x) (doubleton x y).
Definition kpr1 x := union (intersection x).
Definition kpr2 x := 
   union (Zo (union x) (fun z => (doubleton (kpr1 x) z) = (union x))).

Module Type PairSig.
Parameter first_proj second_proj : Set -> Set.
Parameter pair_ctor : Set -> Set -> Set.
Axiom kpr1E: first_proj = kpr1.
Axiom kpr2E: second_proj = kpr2.
Axiom kprE: pair_ctor = kpair. 
End PairSig.

Module Pair : PairSig.
Definition pair_ctor := kpair.
Definition first_proj := kpr1.
Definition second_proj := kpr2.
Lemma kprE: pair_ctor = kpair. Proof. by []. Qed.
Lemma kpr1E: first_proj = kpr1. Proof. by []. Qed.
Lemma kpr2E: second_proj = kpr2. Proof. by []. Qed.
End Pair.

Notation J := Pair.pair_ctor.
Notation P := Pair.first_proj.
Notation Q := Pair.second_proj.

Lemma pr1_pair x y: P (J x y) = x.
Proof.
rewrite Pair.kpr1E /kpr1 Pair.kprE -{2} (setU_1 x); congr union.
have sx_k: inc (singleton x) (kpair x y) by rewrite /kpair; fprops.
apply: set1_pr.
  apply: setI_i;first by exists (singleton x).
  move => z /set2_P [] ->; fprops.
move=> z zi; apply/set1_P; apply: (setI_hi zi sx_k).
Qed.

Lemma pr2_pair x y: Q (J x y) = y.
Proof.
rewrite Pair.kpr2E /kpr2 - Pair.kpr1E pr1_pair -{3}(setU_1 y); congr (union _).
have ->: (union (J x y) = doubleton x y). 
  rewrite Pair.kprE /kpair; set_extens t =>ts.
    case /setU2_P: ts => // /set1_P ->; fprops.
  by apply: (setU_i ts); fprops.
apply: set1_pr; first by apply: Zo_i; fprops.
move => z /Zo_P [] /set2_P [] // -> sd.
by move: (set2_2 x y); rewrite - sd ; move/set1_P.
Qed.

Hint Rewrite pr1_pair pr2_pair : aw. 

Lemma pr1_def a b c d: J a b = J c d -> a = c.
Proof. move/(congr1 P); aw. Qed.

Lemma pr2_def a b c d: J a b = J c d -> b = d.
Proof. move/(congr1 Q); aw. Qed.


Lemma pr12_def a b c d : J a b = J c d -> a = c /\ b = d.
Proof. by move => h; rewrite (pr1_def h)(pr2_def h). Qed.


Definition pairp (x : Set) := (J (P x) (Q x) = x).

Lemma pair_is_pair x y: pairp (J x y). 
Proof. rewrite /pairp; aw. Qed.

Hint Resolve pair_is_pair: fprops.

Lemma pair_exten x y:
  pairp x -> pairp y -> P x = P y -> Q x = Q y -> x = y.
Proof. by move => {3} <- {3} <- -> ->. Qed.

End Pair.

Export Pair.


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

(**  This is the set of all pairs [J x y] with x in A, y in B *)

Module Cartesian.

Definition product (A B : Set) :=
  union (fun_image A (fun x => (fun_image B (J x)))).

Definition coarse A := product A A.

Notation "A \times B" := (product A B) (at level 40).  

Lemma setX_P x A B:
  inc x (A \times B) <-> [/\ pairp x, inc (P x) A & inc (Q x) B].
Proof.
split. 
  move/setU_P => [a xa /funI_P [t ty ft]].
  move: xa; rewrite ft; move/funI_P => [u uz ->]; aw; split; fprops.
move => [px Px Qx];apply/setU_P; exists  (fun_image B (J (P x)));
  apply/funI_P; [ exists (Q x); fprops; aw | by exists (P x) ]. 
Qed.

Lemma setX_pair x A B: inc x (A \times B) -> pairp x.
Proof. by case/setX_P. Qed.

Lemma setX_i x A B:
  pairp x -> inc (P x) A -> inc (Q x) B -> inc x (A \times B).
Proof. by move => pa pb pc; apply/setX_P. Qed.

Lemma setXp_i x y A B:
  inc x A -> inc y B -> inc (J x y) (A \times B).
Proof. move => pa pb; apply setX_i; aw; fprops. Qed.

Lemma setXp_P x y A B:
  inc (J x y) (A \times B) <-> (inc x A /\ inc y B).
Proof. 
by split; [move/setX_P=> [_]; aw | move=> [xa ya]; apply: setXp_i].
Qed.

Hint Resolve setXp_i: fprops.


(** A product is empty if and only one factor is empty *)

Lemma setX_0l B: emptyset \times B = emptyset.
Proof. by apply /set0_P => x /setX_P [_ /in_set0]. Qed.
  
Lemma setX_0r A: A \times emptyset = emptyset.
Proof. by apply /set0_P => y /setX_P [_ _ /in_set0]. Qed.
  
Lemma setX_0 A B:
  A \times B = emptyset -> (A = emptyset \/ B = emptyset).
Proof. 
move=> pe; case: (emptyset_dichot A);first by left.
by case => t tx; right; apply /set0_P => u up; empty_tac1 (J t u).
Qed.

Hint Rewrite setX_0r setX_0l : bw.

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

Lemma setX_Sl x x' y: sub x x' -> sub (x \times y) (x' \times y).
Proof. move => xx' t /setX_P [pt pa pb]; apply/setX_P; split;fprops. Qed.

Lemma setX_Sr x y y': sub y y' -> sub  (x \times y) (x \times y').
Proof. move => xx' t /setX_P [pt pa pb]; apply/setX_P;split;fprops. Qed.

Lemma setX_Slr x x' y y':
  sub x x' -> sub y y' -> sub (x \times y) (x' \times y').
Proof. 
move=> xx' yy'; apply: (@sub_trans  (x \times y')); first by apply:setX_Sr. 
by apply: setX_Sl.
Qed.

Lemma setX_Sll x y:  sub x y -> sub (coarse x) (coarse y).
Proof. by move => s; apply: setX_Slr. Qed.

Lemma setX_lS x x' y: nonempty y ->
  sub (x \times y) (x' \times y) -> sub x x'. 
Proof. 
by move=> [t ty] s z zx; move: (s _ (setXp_i zx ty)); case/setXp_P.  
Qed.

Lemma setX_rS x y y': nonempty x ->
  sub (x \times y) (x \times y') -> sub y y'. 
Proof. 
by move=> [t tx] s z zy; move: (s _ (setXp_i tx zy)); case/setXp_P.  
Qed.

Definition indexed (x i: Set) := x \times singleton i.
Definition indexedr (i x: Set) := singleton i \times x.
Notation "a *s1 b" := (indexed a b) (at level 50).  

Lemma indexed_pi x i y: inc y x -> inc (J y i) (x *s1 i).
Proof. move => pa; apply: setXp_i => //; fprops. Qed.

Lemma indexed_P x i y: 
  inc y (x *s1 i) <-> [/\ pairp y, inc (P y) x & Q y = i].
Proof.
split; first by  move /setX_P => [pa pb /set1_P].
move =>[pa pb <-]; apply: setX_i; fprops.
Qed.

Lemma indexedrP a b c: 
  inc a (indexedr b c) <-> [/\ pairp a, P a = b & inc (Q a) c].
Proof.
split; first by move/setX_P => [pa /set1_P pb pc].
move =>[pa pb pc]; apply/setX_P;split => //; rewrite pb;fprops.
Qed.

End Cartesian.

Export Cartesian.

(** ** Functional graphs *)

Definition prop_inc1 (X : Set) (P: property) 
   & (phantom Prop (forall x0 : Set, P x0)) :=
   forall x, inc x X -> P x.

Definition prop_inc11 X Y (P: relation) 
  & (phantom Prop (forall x y: Set, P x y)) := 
   forall x y, inc x X -> inc y Y -> P x y.
Definition prop_inc2 X (P: relation)
  & (phantom Prop (forall x y: Set, P x y)) :=
   forall x y, inc x X -> inc y X -> P x y.

Notation "{ 'inc' d , P }" :=
  (prop_inc1 d (inPhantom P))
  (at level 0, format "{ 'inc'  d ,  P }") : type_scope.

Notation "{ 'inc' d1 & d2 , P }" :=
  (prop_inc11 d1 d2 (inPhantom P))
  (at level 0, format "{ 'inc'  d1  &  d2 ,  P }") : type_scope.

Notation "{ 'inc' d & , P }" :=
  (prop_inc2 d (inPhantom P))
  (at level 0, format "{ 'inc'  d  & ,  P }") : type_scope.


Definition prop_when1 (X : property) (P: property) 
   & (phantom Prop (forall x : Set, P x)) :=
   forall x, X x -> P x.

Definition prop_when11 (X Y: property) (P: relation) 
  & (phantom Prop (forall x y: Set, P x y)) := 
   forall x y, X x -> Y y -> P x y.
Definition prop_when2 (X: property) (P: relation)
  & (phantom Prop (forall x y: Set, P x y)) :=
   forall x y, X x -> X y -> P x y.


Definition prop_when22 (X:relation) (P: relation)
  & (phantom Prop (forall x y: Set, P x y)) :=
   forall x y, X x y -> P x y.

Notation "{ 'when' d , P }" :=
  (prop_when1 d (inPhantom P))
  (at level 0, format "{ 'when'  d ,  P }") : type_scope.


Notation "{ 'when' d1 & d2 , P }" :=
  (prop_when11 d1 d2 (inPhantom P))
  (at level 0, format "{ 'when'  d1  &  d2 ,  P }") : type_scope.

Notation "{ 'when' d & , P }" :=
  (prop_when2 d (inPhantom P))
  (at level 0, format "{ 'when'  d   & ,  P }") : type_scope.


Notation "{ 'when' : d , P }" :=
  (prop_when22 d (inPhantom P))
  (at level 0, format "{ 'when' :  d ,  P }") : type_scope.

Definition commutes_at (f g: Set -> Set) x:= f (g x) = g (f x).
Definition commutes f g := forall x, commutes_at f g x.

Definition compatible_1 f (p q: property) := 
    forall x, (p x) -> q (f x).
Definition compatible_2 f (p q:relation)  := 
    forall x y, (p x y) -> q (f x) (f y).
Definition compatible_3 f (p q:property)  := 
    forall x y, (p x) -> (p y) -> q (f x y).

Notation "{ 'compat' f : x / p >-> q }" :=
  (compatible_1 f  (fun x => p) (fun x => q))
  (at level 0,  f at level 99, x ident, 
     format "{ 'compat'  f  : x  /  p  >->  q }") : type_scope.

Notation "{ 'compat' f : x / p }" :=
  (compatible_1 f  (fun x => p) (fun x => p))
  (at level 0,  f at level 99, x ident, 
    format "{ 'compat'  f  : x  /  p }") : type_scope.

Notation "{ 'compat' f : x y / p >-> q }" :=
  (compatible_2 f  (fun x y => p) (fun x y => q))
  (at level 0,  f at level 99, x ident, y ident,
    format "{ 'compat'  f  : x  y  /  p  >->  q }") : type_scope.
Notation "{ 'compat' f : x y / p }" :=
  (compatible_2 f  (fun x y => p) (fun x y => p))
  (at level 0,  f at level 99, x ident, y ident,
    format "{ 'compat'  f  : x  y  /  p }") : type_scope.

Notation "{ 'compat' f : x & / p >-> q }" :=
  (compatible_3 f  (fun x => p) (fun x => q))
  (at level 0,  f at level 99, x ident,
     format "{ 'compat'  f  : x  &  /  p  >->  q }") : type_scope.

Notation "{ 'compat' f : x & / p }" :=
  (compatible_3 f  (fun x => p) (fun x => p))
  (at level 0,  f at level 99, x ident, 
     format "{ 'compat'  f  : x  &  /  p }") : type_scope.

Module Function.

(** A graph is a set of pair; the set of first projections is the domain, 
the set of second projections is the range*)

Definition sgraph r := alls r pairp.
Definition domain f := fun_image f P.
Definition range f := fun_image f Q.

(** A functional graph is one for which [P] is injective *)

Definition fgraph f := sgraph f /\ {inc f &, injective P}.
Definition related r x y := inc (J x y) r.

Lemma fgraph_sg f: fgraph f -> sgraph f.
Proof. by case. Qed.


Lemma fgraph_pr f x y y':
  fgraph f -> inc (J x y) f -> inc (J x y') f -> y = y'.
Proof. 
move=> [_ fg] ia ib.
move: (fg _ _ ia ib); aw => h; exact: (pr2_def (h (erefl x))).
Qed. 

Hint Resolve fgraph_sg : fprops.

(** We give here some properties of the domain and range *)


Lemma domain_i1 f x: inc x f -> inc (P x) (domain f). 
Proof. by apply: funI_i. Qed. 

Lemma range_i2 f x: inc x f -> inc (Q x) (range f). 
Proof. by apply: funI_i. Qed.

Hint Resolve domain_i1 range_i2: fprops.

Lemma domain_i f x y: inc (J x y) f -> inc x (domain f). 
Proof. move/domain_i1; aw. Qed.

Lemma range_i f x y: inc (J x y) f -> inc y (range f). 
Proof. move/range_i2; aw. Qed.

Lemma domainP r: sgraph r -> forall x,
  (inc x (domain r) <-> (exists y, inc (J x y) r)).
Proof.
move=> gr; split; last by move=> [y ]; apply domain_i.
by case/funI_P => y yr ->; exists (Q y); rewrite (gr _ yr).
Qed.

Lemma rangeP r : sgraph r ->  forall y,
   (inc y (range r) <->  (exists x, inc (J x y) r)).
Proof.
move=> gr y; split;last by move=> [x]; apply range_i.
by case/funI_P => x xr ->; exists (P x); rewrite (gr _ xr).
Qed.

Ltac ex_tac:=
  match goal with
   | H:inc (J ?x ?y) ?z |- exists x, inc (J x ?y) ?z
     => exists x ; assumption
   | H:inc (J ?x ?y) ?z |- exists y, inc (J ?x y) ?z
     => exists y ; assumption
   | H:inc (J ?x ?y) ?z |- ex2 _  (fun t => inc (J t ?y) ?z)
     => exists x ; trivial
   | H:inc (J ?x ?y) ?z |- ex2 _ (fun t => inc (J ?x t) ?z)
     => exists y ; trivial
   | H:inc (J ?x ?y) ?z |- ex2 (fun t => inc (J t ?y) ?z) _
     => exists x ; trivial
   | H:inc (J ?x ?y) ?z |- ex2 (fun t => inc (J ?x t) ?z) _
     => exists y ; trivial
   | H:inc ?x ?y |- ex2 (fun t=> inc t ?y) _
     => exists x ; fprops
   | H:inc ?x ?y |- ex2 _ (fun t => inc t ?y)
     => exists x ; fprops
   | H:inc ?x ?y |- exists x, inc x ?y /\ _  
     => exists x; split => //
   | H:inc ?x ?y |- exists x, [/\ inc x ?y, _ & _ ] 
     => exists x; split => //
   |  |- ex2 (fun t => inc t (singleton ?y)) _
     => exists y ; fprops
    | H : inc (J ?x ?y) ?g |-  inc ?x (domain ?g)
       => exact: (domain_i H)
    |  H : inc (J ?x ?y) ?g |-  inc ?y (range ?g)
       => exact: (range_i H)
    | H : inc ?x ?y |-  nonempty ?y 
       => exists x;assumption
   | |- exists y, inc (J (P ?x) y) _ 
     => exists (Q x) ; aw
   | |- exists y, inc (J y (Q ?x)) _ 
     => exists (P x) ; aw
end.

Lemma sgraph_exten r r':
  sgraph r -> sgraph r' ->
  (forall u v, (related r u v <-> related r' u v)) -> r = r'.
Proof. 
rewrite /related => gr gr' p.
by set_extens t => tr;  [move: (gr _ tr)=> pt | move: (gr' _ tr)=> pt]; 
  rewrite - pt; apply /p; rewrite pt.
Qed.

Lemma setI2_graph1 x y: sgraph x ->  sgraph (x \cap y).
Proof. by move=> gx t /setI2_P [tx _]; apply: gx. Qed.

Lemma setI2_graph2 x y: sgraph y -> sgraph (x \cap y).
Proof. by move=> gx t /setI2_P [_ tx ]; apply: gx. Qed.

Lemma setU2_graph: {compat union2 : x & / sgraph x}.  
Proof. by move=> x y gx gy t /setU2_P [] tx; [apply: gx | apply: gy]. Qed.

Lemma range_set0: range emptyset = emptyset.
Proof. apply: funI_set0. Qed.

Lemma domain_set0: domain emptyset = emptyset.
Proof. apply: funI_set0. Qed.

Lemma domain_set0_P r: (domain r = emptyset <-> r = emptyset).
Proof. split; [apply :funI_setne1 | by move ->; exact domain_set0 ]. Qed.

Lemma range_set0_P r:  (range r = emptyset <-> r = emptyset).
Proof. split; [apply :funI_setne1 | by move ->; exact range_set0 ]. Qed.

Lemma domain_set0P x: nonempty (domain x) <-> nonempty x.
Proof. 
split; last by move => h; apply:funI_setne.
by move/nonemptyP => h; apply /nonemptyP; dneg xx; apply/domain_set0_P.
Qed.

Lemma domain_set1 x y: domain (singleton (J x y)) = singleton x.
Proof. by rewrite /domain funI_set1; aw. Qed.

Lemma range_set1 x y: range (singleton (J x y)) = singleton y.
Proof. by rewrite /range funI_set1; aw. Qed.

Lemma range_setU2: {morph range: x y /  x \cup y}.
Proof. apply:funI_setU2. Qed.

Lemma domain_setU2: {morph domain: x y /  x \cup y}.
Proof. apply:funI_setU2. Qed.

Lemma domain_setU z: domain (union z) = union (fun_image z domain).
Proof. apply: funI_setU. Qed.

Lemma range_setU z: range (union z) = union (fun_image z range).
Proof. apply: funI_setU. Qed.

Lemma range_setU1 f x y: range (f +s1 (J x y)) = (range f) +s1 y.
Proof. by rewrite range_setU2 range_set1. Qed.

Lemma domain_setU1 f x y: domain (f +s1 (J x y)) = (domain f) +s1 x.
Proof. by rewrite domain_setU2 domain_set1. Qed. 

Lemma sgraph_set0: sgraph emptyset.
Proof. by move=> t [][]. Qed. 

Hint Resolve sgraph_set0 : fprops.
Hint Rewrite range_set0 domain_set0 : bw.

Lemma fgraph_set0: fgraph emptyset.
Proof. by split; [fprops | move=> x y; case; case]. Qed.

Lemma fgraph_set1 a b (f := singleton (J a b)):
  [/\ fgraph f, domain f = singleton a & range f = singleton b ].
Proof.
rewrite /f domain_set1 range_set1; split => //; split.
  move => i /set1_P ->; fprops.
by move => i j /set1_P -> /set1_P ->.
Qed.  

Lemma fgraph_setU2 a b: fgraph a -> fgraph b ->
  disjoint (domain a) (domain b) ->
  fgraph (a \cup b).
Proof. 
move=> [fg fgg] [sg gfg] ei; split.
   move=> t; case/setU2_P; fprops.
move=> x y; case/setU2_P => xab; case /setU2_P=> yab;
  first (by apply: fgg); last (by apply: gfg);
move=> sp;empty_tac1 (P y); apply/funI_P; ex_tac.
Qed.


Lemma fgraph_setU1 f x y:
  fgraph f -> ~ inc x (domain f) -> fgraph (f +s1 (J x y)).
Proof.
move => sa sb; move:(fgraph_set1 x y) => [ha hb hc].
apply:fgraph_setU2 => //; rewrite hb; apply: disjoint_pr => t td /set1_P tx.
by case: sb; rewrite - tx. 
Qed. 


(** [Vg f x] is the value of [x] by a graph [f]; if there is a [z] such that 
    [J x z] is in [f], then [V] chooses one. *)

Definition action_prop (f g: Set -> Set -> Set) :=
   forall a b x, f (g a b) x = (f a (f b x)).

Definition Vg (f x: Set) := select (fun y : Set => inc (J x y) f) (range f).

Definition same_Vg  f g:= Vg f =1 Vg g .

Definition allf (g: Set) (p: property) :=
   forall x, inc x (domain g) -> (p (Vg g x)).

Notation "f1 =1g f2" := (same_Vg f1 f2)
  (at level 70, no associativity) : fun_scope.

(** The function [V] is well-defined for functional graphs. 
Here are some properties  *)

Section Vprops.
Variable f: Set.
Hypothesis fgf: fgraph f.

Lemma fdomain_pr1 x:  inc x (domain f) -> inc (J x (Vg f x)) f.
Proof.
move: fgf => [p1 p2] /funI_P [z zf ->].
have q1: exists2 y, inc y (range f) & inc (J (P z) y) f.
  exists (Q z); [ apply /funI_P; ex_tac | by rewrite (p1 _ zf)].
apply:(select_pr1 q1) => a b pa ar pb br. 
have aux: (P (J (P z) a) = P (J (P z) b)) by aw.
by move: (pr2_def (p2 _ _ ar br aux)).
Qed.

Lemma in_graph_V x: inc x f -> x = J (P x) (Vg f (P x)).
Proof. 
move => xf; apply: (proj2 fgf _ _ xf); aw.
by apply:fdomain_pr1=> //; apply: domain_i1.
Qed.

Lemma pr2_V x: inc x f -> Q x = Vg f (P x).
Proof. by move=> xf; rewrite (in_graph_V xf); aw. Qed.

Lemma range_gP y:
  (inc y (range f) <-> (exists2 x, inc x (domain f) & y = Vg f x)).
Proof. 
move: (fgf) => [sg _]; split.
  case/(rangeP sg)=> x Px; exists x; first by ex_tac.
  by move:(in_graph_V Px); aw; apply: pr2_def.
by move => [x xdf ->]; apply/(rangeP sg); exists x; apply: fdomain_pr1.  
Qed.

Lemma inc_V_range x: inc x (domain f) -> inc (Vg f x) (range f).
Proof. move=> xd; apply/range_gP; ex_tac. Qed.

End Vprops.
Hint Resolve inc_V_range: fprops.


Lemma simple_fct a b A B (f := singleton (J a b)):
  inc a A -> inc b B ->
  [/\ fgraph f, domain f = singleton a, range f = singleton b, 
   sub (domain f) A & (sub (range f) B /\ Vg f a = b) ].
Proof.
move => aA bB. 
move: (fgraph_set1 a b) => [ha hb hc]; rewrite hb hc; split => //.
+ by move => t /set1_P ->.
+ split; [by move => t /set1_P -> | symmetry ].
  by move:(pr2_V ha (set1_1 (J a b))); aw.
Qed.

(** Two functional graphs are equal if they have the same domain and evaluation *)

Lemma fgraph_exten f g:
  fgraph f -> fgraph g -> domain f = domain g ->
  {inc (domain f), f =1g g} -> f = g.
Proof. 
move=> ff fg sd hyp; set_extens t =>  tf.
  have pa:= (domain_i1 tf).
  rewrite (in_graph_V ff tf) (hyp _ pa); apply: fdomain_pr1 => //; ue.
move: (domain_i1 tf); rewrite - sd => pa.
by rewrite (in_graph_V fg tf) - (hyp _ pa); apply: fdomain_pr1.
Qed.


(** Graph associated to a function restricted to some set as domain. *)

Definition Lg (x : Set) (p : fterm) :=
  fun_image x (fun y => J y (p y)).

Lemma Lg_i x y p : inc x y ->  inc (J x (p x)) (Lg y p).
Proof. move => xy; apply/funI_P; ex_tac.  Qed.

Lemma Lg_fgraph p x: fgraph (Lg x p).
Proof.
split; first by move =>t /funI_P [z _ ->]; fprops.
by move=> a b /funI_P [z1 _ ->] /funI_P [z2 _ ->]; aw => ->.
Qed.

Lemma Lg_domain x p: domain (Lg x p) = x.
Proof.
set_extens t.
  case/funI_P => [e /funI_P [z zx ->] ->]; aw.
by move => tw;apply/funI_P; exists (J t (p t)); aw => //;apply:Lg_i.
Qed.

Hint Rewrite Lg_domain : bw. 
Hint Resolve Lg_fgraph: fprops.

Lemma LVg_E x p y: inc y x -> Vg (Lg x p) y = p y. 
Proof. 
by move=> yx; move: (pr2_V (Lg_fgraph p x) (Lg_i p yx)); aw.
Qed.

Hint Rewrite LVg_E : bw. 

Lemma Lg_exten a f g: {inc a, f =1 g} -> Lg a f = Lg a g.
Proof. 
move=> eqv; apply: fgraph_exten; fprops; bw. 
by move => x xa /=; bw; apply: eqv.
Qed.

Lemma Lg_range p x: range (Lg x p) = fun_image x p.
Proof. 
set_extens z.
  by move/funI_P=> [a /funI_P [b ib ->] ->]; aw; apply:funI_i.
move/funI_P => [b ba ->];apply/funI_P.
by exists (J b (p b));aw => //; apply: Lg_i.
Qed.

Lemma Lg_range_P sf f a:
  inc a (range (Lg sf f))  <-> exists2 b, inc b sf & a = f b.
Proof. rewrite Lg_range; apply/funI_P. Qed.

Lemma Lg_recovers f: fgraph f -> Lg (domain f) (Vg f) = f.
Proof.
move=> fg; apply: fgraph_exten; fprops; bw => x xf /=; bw.
Qed.

Lemma simple_fct2 a b (f := singleton (J a b)):
  [/\ fgraph f, domain f = singleton a, range f = singleton b,
   Vg f a = b & f = Lg (singleton a) (fun _ => b)].
Proof.
move: (fgraph_set1 a b) => [ha hb hc]; rewrite hb hc.
move:(pr2_V ha (set1_1 (J a b))); aw => bv.
split => //; apply: fgraph_exten => //; fprops; bw; rewrite hb => x xi; bw.
by move /set1_P: xi => ->.
Qed.

(** Graph of the identity function. *)

Definition identity_g (x : Set) := Lg x id.

Lemma identity_fgraph x: fgraph (identity_g x). 
Proof. rewrite/identity_g; fprops. Qed. 

Lemma identity_sgraph x: sgraph (identity_g x).
Proof. by case: (identity_fgraph x). Qed. 

Lemma identity_d x: domain (identity_g x) = x.
Proof. rewrite/identity_g; bw. Qed. 

Lemma identity_r x: range (identity_g x) = x.
Proof.  
set_extens t; first by move/Lg_range_P => [y yi ->]. 
by move => tx; apply/Lg_range_P; exists t.
Qed. 

Lemma identity_ev x a: inc x a -> Vg (identity_g a) x = x.
Proof. rewrite/identity_g => xa; bw. Qed.

Hint Resolve identity_sgraph : fprops.

Definition cst_graph x y:= Lg x (fun _ => y).

Lemma cst_graph_pr x y: cst_graph x y = x *s1 y.
Proof.
set_extens t.
  by move/funI_P => [z zx ->]; apply: indexed_pi.
move /indexed_P => [pt Pt Qt];apply/funI_P; ex_tac; rewrite - Qt //.
Qed.

Lemma cst_graph_ev x y t : inc t x -> Vg (cst_graph x y) t = y.
Proof.  move => tw; rewrite /cst_graph; bw. Qed.

Lemma cst_graph_d x y : domain (cst_graph x y) = x.
Proof. rewrite /cst_graph; bw. Qed.

Lemma cst_graph_fgraph a b: fgraph (cst_graph a b).
Proof. rewrite /cst_graph; fprops. Qed.

Hint Rewrite cst_graph_d cst_graph_ev : bw.
Hint Resolve cst_graph_fgraph: fprops.

Lemma setU1_V_out f x y:
  fgraph f -> ~ (inc x (domain f)) ->  Vg (f +s1 (J x y)) x = y.
Proof. 
move=>ff /(fgraph_setU1 y ff) fg.
have h1: inc (J x y) (f +s1 (J x y)) by fprops.
by move: (pr2_V fg h1); aw.
Qed.

Lemma setU1_V_in f x y u:
  fgraph f -> ~ (inc x (domain f)) -> inc u (domain f) ->
  Vg (f +s1 (J x y)) u = Vg f u.
Proof.
move=> ff /(fgraph_setU1 y ff) fg /(fdomain_pr1 ff) aux. 
have h1: inc (J u (Vg f u)) (f +s1 (J x y)) by fprops.
by move: (pr2_V fg h1); aw.
Qed.

(** Case of a subgraph *)

Lemma sub_fgraph f g: fgraph g -> sub f g -> fgraph f.
Proof.
move=> [fg ffg] s; split.
  by move=> t tf; apply: (fg _ (s _ tf)). 
by move=> x y xf yf; apply: ffg; apply: s.
Qed.

Lemma domain_S f g: sub f g -> sub (domain f) (domain g).
Proof. apply: funI_S. Qed.

Lemma range_S f g: sub f g -> sub (range f) (range g).
Proof. apply: funI_S. Qed.

Lemma sub_graph_ev f g:
  fgraph g -> sub f g -> {inc (domain f), f =1g g}.
Proof.
move=> fg sfg x xdf.
set ipg:=(sfg _ (fdomain_pr1 (sub_fgraph fg sfg) xdf)).
by move: (in_graph_V fg ipg); aw; apply: pr2_def.
Qed.


(** restriction of a graph to a set *)

Definition restr f x := Lg x (Vg f).

Lemma restr_d f x: domain (restr f x) = x.
Proof. rewrite /restr; bw. Qed.

Lemma restr_fgraph f x: fgraph (restr f x).
Proof. rewrite /restr; fprops. Qed.

Lemma restr_ev f x i: inc i x -> Vg (restr f x) i = Vg f i.
Proof. move=>  ix; rewrite /restr; bw. Qed.

Hint Rewrite restr_ev restr_d: bw.
Hint Resolve restr_fgraph : fprops.

Lemma double_restr f a b: sub a b -> (restr (restr f b) a) = (restr f a).
Proof.  
by move => sb; apply: Lg_exten => t ta /=; bw; apply: sb.
Qed.

Lemma restr_Lg a b f: sub b a -> restr (Lg a f) b = Lg b f.
Proof.
move => sba; apply:fgraph_exten; fprops; bw.
by move => t tb /=; bw; apply: sba.
Qed.

Lemma restr_to_domain f g: fgraph f -> sub g f -> restr f (domain g) = g.
Proof.
move => h1 h2; move: (sub_fgraph  h1 h2) => fgg.
apply:fgraph_exten; bw; fprops.
by move => t tx /=;bw; symmetry; apply: sub_graph_ev.
Qed.

Lemma restr_range1 f x: fgraph f -> sub x (domain f) -> 
  sub (range (restr f x)) (range f).
Proof.
move=> pa pb  t/funI_P [u /funI_P [z zx -> ->]]; aw.
exact: (inc_V_range pa (pb _ zx)).
Qed.


(** Composition of two graphs. If the graphs are composable, 
  we can simplify the definition*)

Definition composablef (f g : Set) :=
  [/\ fgraph f, fgraph g & sub (range g) (domain f)]. 

Definition composef f g := Lg (domain g)  (fun y => Vg f (Vg g y)).

Notation "x \cf y" := (composef x y) (at level 50).
Notation "x \cfP y" := (composablef x y) (at level 50).

Lemma composef_ev x f g: 
  inc x (domain g) -> Vg (f \cf g) x = Vg f (Vg g x).
Proof. move => pa; rewrite /composef; bw. Qed. 

Lemma composef_fgraph f g: fgraph (f \cf g).
Proof. rewrite /composef; fprops. Qed. 

Lemma composef_domain f g: domain (f \cf g) = domain g.
Proof. by rewrite /composef; bw.  Qed. 

Lemma composef_range f g:  f \cfP g ->
  sub (range (f \cf g)) (range f).
Proof.
move => [pa pb pc] t; move /(range_gP (composef_fgraph f g)) => [x].
rewrite composef_domain => xdg; rewrite (composef_ev _ xdg) => ->.
apply /(range_gP pa); exists (Vg g x) => //. 
apply: pc; apply /(range_gP pb); ex_tac.
Qed.

Hint Rewrite composef_ev : bw. 
Hint Resolve composef_fgraph: fprops.


End Function.
Export Function.