(** * Theory of Sets  EII-3 Correspondences
  Copyright INRIA (2009-2013) Apics; Marelle Team (Jose Grimm).
*)

(* $Id: sset2.v,v 1.76 2016/05/18 14:54:53 grimm Exp $ *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset1.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


(** ** EII-3-1  Graphs et correspondences *)

Module Correspondence.

(** ** Additional lemmas *) 

(** Proposition 1: existence and uniqueness of range and domain *)

Theorem range_domain_exists r: sgraph r -> 
  ((exists! a, forall x, inc x a <-> (exists y, inc (J x y) r)) /\
    (exists! b, forall y, inc y b <-> (exists x, inc (J x y) r))).
Proof.
move=> gr; split; apply /unique_existence; split.
- exists (domain r) => t; apply/(domainP gr).
- by move=> x y Hx Hy; set_extens t; rewrite Hx Hy. 
- by exists (range r) => t;  apply/(rangeP gr).
- by move=> x y Hx Hy; set_extens t; rewrite Hx Hy. 
Qed. 


(** A product is a special graph *)

Lemma sub_graph_setX r: sgraph r -> 
  sub r ((domain r) \times (range r)).
Proof. move=> gr t tr; apply/setX_P; split; fprops.  Qed.

Lemma setX_graph x y: sgraph (x \times y).
Proof. by move=> t /setX_P []. Qed. 

Lemma sub_setX_graph u x y: sub u (x \times y) -> sgraph u.
Proof. move=> su t tu; exact: (setX_graph (su _ tu)). Qed. 

Hint Resolve setX_graph: fprops.

Lemma setX_relP x y a b:
  related (x \times y) a b <-> (inc a x /\ inc b y).
Proof.  
by split;[ move/setX_P => [_ ]; aw | move => [ax biy]; apply: setXp_i ].
Qed.

Lemma setX_domain x y: nonempty y -> domain (x \times y) = x.
Proof.  
move=> [z zy]; set_extens t. 
  by case/funI_P => u /setX_P [_ xx _] ->.
move=> tx; apply/funI_P;exists (J t z); aw; fprops. 
Qed.

Lemma setX_range x y: nonempty x -> range (x \times y) = y.
Proof.  
move=> [z zy]; set_extens t. 
  by case/(funI_P) => u /setX_P [_ _ xx] ->.
move=> tx; apply/funI_P;exists (J z t); aw; fprops. 
Qed.

Hint Rewrite setX_domain setX_range : bw.

(** Diagonal of a set: this is a functional graph [x -> x] *)

Definition diagonal x := Zo (coarse x)(fun y=> P y = Q y).

Lemma diagonal_i_P x u:
  inc u (diagonal x) <-> [/\ pairp u, inc (P u) x & P u = Q u].
Proof.
split; first by case/Zo_P => /setX_P [ta tb _] tc.
move=> [ta tb tc]; apply: Zo_i => //;rewrite -ta; apply: setXp_i => //; ue.
Qed.

Lemma diagonal_pi_P x u v:
  inc (J u v) (diagonal x) <-> (inc u x /\ u = v).
Proof.
apply: (iff_trans (diagonal_i_P x (J u v))); aw.
split; [by case | move => []; split; fprops ].
Qed.

Lemma diagonal_is_identity x: diagonal x = identity_g x.
Proof.
set_extens t.
  move /diagonal_i_P => [pt Pt eql]; rewrite -pt -eql;apply /funI_P; ex_tac.
by move /funI_P => [z zx ->]; apply/diagonal_pi_P.
Qed.

(** A correspondence is a triple (G,A,B), graph, source and target,  
   such that [G] is a subset of the product [A \times B].
   The domain of [G] is a subset of [A].
   The range of [G] is a subset of [B].
 *)

Definition triplep f := pairp f /\ pairp (Q f).
Definition source x := P (Q x). 
Definition target x := Q (Q x). 
Definition graph x := P x. 

Definition triple s t g  := J g (J s t).

Definition correspondence f  :=
  triplep f /\ sub (graph f) ((source f) \times (target f)).

Lemma corr_propcc s t g:
  sub g (s \times t) <-> [/\ sgraph g, sub (domain g) s & sub (range g) t].
Proof.  
split => [sg | [gg sd sr] x xg ].
  have gg:= (sub_setX_graph sg).
  by split =>// z /funI_P [y yp ->];move/setX_P: (sg _ yp) => [_].
rewrite -(gg _ xg); apply: setXp_i; [ apply: sd | apply: sr]; fprops.
Qed.

Lemma corr_propc f (g := graph f):
  correspondence f ->
  [/\ sgraph g, sub (domain g) (source f) & sub (range g) (target f)].
Proof. by move=> [tf sg]; apply /corr_propcc. Qed.

Lemma triple_corr s t g: triplep (triple s t g).
Proof. by rewrite /triple; split; [| aw]; fprops. Qed.

Lemma corresp_recov f: triplep f ->
  triple (source f) (target f) (graph f) = f.
Proof. 
by rewrite /triple /source /target /graph => [] [pf ->].
Qed.

Lemma corresp_recov1 f: correspondence f ->
  triple (source f) (target f) (graph f) = f.
Proof. by move => [t _]; apply: corresp_recov. Qed.

Lemma corresp_s s t g: source (triple s t g) = s.
Proof. rewrite /triple /source; aw. Qed.

Lemma corresp_t s t g: target (triple s t g) = t.
Proof. rewrite /triple /target; aw. Qed.

Lemma corresp_g  s t g: graph (triple s t g) = g.
Proof. rewrite /triple /graph; aw. Qed.

Hint Rewrite corresp_s corresp_t corresp_g : aw.

Lemma corresp_create s t g:
  sub g (s \times t) -> correspondence (triple s t g).
Proof. by move=> h; split; [apply: triple_corr | aw ]. Qed.

(** Some properties of a correspondence *)

Lemma corresp_is_graph g: correspondence g -> sgraph (graph g).
Proof. by case/corr_propc. Qed.

Lemma corresp_sub_range g:
  correspondence g -> sub (range (graph g)) (target g).
Proof. by move /corr_propc => [_ _]. Qed.

Lemma corresp_sub_domain g:
  correspondence g -> sub (domain (graph g)) (source g).
Proof. by move /corr_propc => [_].  Qed.

Hint Resolve corresp_sub_range corresp_sub_domain corresp_is_graph: fprops.

(** The set of correspondences  [E->F] is the product of [P] and [singleton E] 
   and [singleton F], where [P == powerset (E \times F)] 
   is the set of graphs of correspondences *)

Definition correspondences x y :=
  (powerset (x \times y)) \times ( (singleton x) \times (singleton y)).

Lemma correspondences_P x y z:
  inc z (correspondences x y) <->
  [/\ correspondence z, source z = x & target z = y].
Proof. 
rewrite /correspondence /source/target.
split.
  by case/setX_P => [pz /setP_P spz/setX_P [p_qz /set1_P -> /set1_P ->]].
move => [ [ [tp sgp] aux] <- <-].
apply:setX_i;[ exact | by apply/ setP_P | apply:setX_i; fprops].
Qed.


(** Image by the graph [r] of a set [u] *)

Definition direct_image f X:=
  Zo (range f) (fun y=>exists2 x, inc x X & inc (J x y) f). 

Definition Vfs f := direct_image (graph f).
Definition Imf f := Vfs f (source f).

Lemma dirim_P f X y:
  inc y (direct_image f X) <-> exists2 x, inc x X & inc (J x y) f.
Proof. 
split => [ /Zo_hi // | [x xu pr]]; apply/Zo_i; ex_tac.
Qed.

Lemma dirimE f X: fgraph f -> sub X (domain f) ->
  direct_image f X = fun_image X (Vg f).
Proof.
move => sgf sxd; set_extens t.
  move /dirim_P => [x xX pf]; apply /funI_P.
  move: (pr2_V sgf pf); aw => ->; ex_tac.
move /funI_P => [z sX ->]; apply /dirim_P; ex_tac; apply: fdomain_pr1 => //.
by apply: sxd.
Qed.

Lemma dirim_Sr f X: sub (direct_image f X) (range f).
Proof. apply: Zo_S. Qed.

Lemma dirim_domain f: sgraph f -> direct_image f (domain f) =  range f.
Proof.
move=> sgf; apply: extensionality; first by apply: dirim_Sr.
move => t /funI_P [y yf ->]; apply: Zo_i; first by fprops.
by exists (P y); fprops;rewrite (sgf _ yf). 
Qed.

Lemma dirim_set0 f: direct_image f emptyset =  emptyset.
Proof. by apply /set0_P => t /Zo_hi [x /in_set0]. Qed.

Lemma dirim_setn0 f u: sgraph f -> nonempty u -> sub u (domain f)
  -> nonempty (direct_image f u).
Proof. 
move=> gr [x xu] udf; move: (udf _ xu); case /(domainP gr)=> [y Jr].
exists y;apply: Zo_i; ex_tac.
Qed.

Theorem dirim_S f: {compat (direct_image f): u v / sub u v}.
Proof. 
move=> u u' uu' t /dirim_P [x xu pr]; apply/dirim_P.
by exists x => //;apply: uu'.
Qed.

(** Section of the graph [r] at [x] *)

Definition im_of_singleton f x:= direct_image f (singleton x).

Lemma dirim_set1_P f x y:
  inc y (im_of_singleton f x) <-> inc (J x y) f.
Proof.
apply: (iff_trans (dirim_P f _ y)).
split; [ by move =>  [z /set1_P ->] | move => pf; ex_tac; fprops ].
Qed.

Lemma dirim_set1_S f f': sgraph f -> sgraph f' ->
  ((forall x, sub (im_of_singleton f x) (im_of_singleton f' x)) <-> sub f f').
Proof. 
move=> gr gr'; split=> s x t.
  move: (gr _ t) => eql; rewrite - eql;apply/dirim_set1_P.
  by apply: s; apply/dirim_set1_P; rewrite eql.
by move/dirim_set1_P => jf; apply/dirim_set1_P; apply:s.
Qed.

(** ** EII-3-2 Inverse of a correspondence  *)

(** Inverse graph of [r] *)

Definition inverse_graph r :=
  Zo ((range r) \times (domain r))  (fun y=> inc (J (Q y)(P y)) r).

Lemma igraph_graph r: sgraph (inverse_graph r).
Proof. move=> x /Zo_S xp; apply: (setX_pair xp). Qed.

Hint Resolve igraph_graph: fprops.

Lemma igraphP r y: 
  inc y (inverse_graph r) <-> (pairp y /\  inc (J (Q y)(P y)) r).
Proof. 
split; first by case/Zo_P => yp pr; split => //; apply: (setX_pair yp).
move => [py pr]; exact:(Zo_i (setX_i py (range_i pr) (domain_i pr)) pr). 
Qed.

Lemma igraph_pP r x y: inc (J x y) (inverse_graph r) <-> inc (J y x) r.
Proof. 
split; [case/igraphP;aw | move=> pr; apply/igraphP; aw; fprops ].
Qed.

Lemma igraph_alt r: sgraph r ->
  inverse_graph r = fun_image r (fun z => J (Q z) (P z)).
Proof. 
move=> gr; set_extens t. 
  by move /igraphP => [pt h];apply/funI_P; ex_tac; aw; rewrite pt.
by move /funI_P => [c zr ->]; apply/igraph_pP; rewrite (gr _ zr).
Qed.

Lemma igraph_involutive : {when sgraph, involutive inverse_graph}.
Proof. 
move=> f gr; set_extens x;first by case/igraphP => px /igraph_pP; rewrite px.
move => xf; have px:= (gr _ xf).
by rewrite -px;apply/igraph_pP /igraph_pP; rewrite px.
Qed.

Lemma igraph_range r: sgraph r -> range (inverse_graph r) = domain r.
Proof. 
move=> gr; set_extens x; first by move/funI_P => [y /igraphP [_ h] ->]; ex_tac.
move/funI_P => [y yi ->]; apply: (range_i (x:=(Q y))); apply/igraph_pP.
by rewrite (gr _  yi).
Qed.

Lemma igraph_domain r: sgraph r ->  domain (inverse_graph r) = range r.
Proof. 
move=> gr;rewrite - {2} (igraph_involutive gr) igraph_range //.
apply: igraph_graph.
Qed.

Lemma igraph0: inverse_graph (emptyset) = emptyset.
Proof. by apply /set0_P => t /igraphP [_ /in_set0]. Qed.

Hint Rewrite igraph0: bw.

Lemma igraphX x y: inverse_graph (x \times y) =  y \times x.
Proof. 
set_extens t. 
  by move /igraphP => [pt /setX_P]; aw; move => [_ pa pb];apply: setX_i.
move/setX_P=> [pt pa pb]; apply /igraphP; fprops.
Qed.

Lemma igraph_identity_g x:
  inverse_graph (identity_g x) = identity_g x.
Proof.
rewrite/inverse_graph identity_r identity_d - diagonal_is_identity.
set_extens z;move /Zo_P => [pa pb]; apply: Zo_i => //.
  by move/Zo_hi: pb; aw.
by rewrite -pb;apply/diagonal_pi_P;split => //; move /setX_P: pa => [_].
Qed.

Hint Rewrite igraph_identity_g igraphX: aw.

(** Inverse correspondence *)

Definition inverse_fun m :=
  triple (target m) (source m) (inverse_graph (graph m)).

Lemma icor_correspondence m:
  correspondence m -> correspondence (inverse_fun m).
Proof. 
move => [_ pb]; apply: corresp_create => x/igraphP [px pg]. 
by move /setXp_P: (pb _ pg) => [pc pd]; apply: setX_i.
Qed.

Lemma icor_involutive:
  {when correspondence, involutive inverse_fun}.
Proof. 
move=> m cm; rewrite /inverse_fun; aw; rewrite igraph_involutive;fprops.
by apply: corresp_recov1. 
Qed.

Lemma ifun_s f: source (inverse_fun f) = target f.
Proof. rewrite/inverse_fun; aw. Qed.

Lemma ifun_t f: target (inverse_fun f) = source f.
Proof.  rewrite/inverse_fun; aw. Qed.

Lemma ifun_g f: graph (inverse_fun f) = inverse_graph (graph f).
Proof. rewrite /inverse_fun;aw. Qed.

Hint Rewrite ifun_s ifun_t ifun_g : aw.
Hint Resolve icor_correspondence: fprops.

(** Inverse image by a graph r of a set x *)

Definition inverse_image r :=  direct_image (inverse_graph r).
Definition Vfi f:=  inverse_image (graph f).
Definition Vfi1 f x := Vfi f (singleton x).

Lemma iim_fun_pr r: Vfi r = Vfs (inverse_fun r).
Proof. rewrite /Vfi /inverse_fun /Vfs; aw. Qed.

Lemma iim_graph_P x r y:
  (inc y (inverse_image r x)) <-> (exists2 u, inc u x & inc (J y u) r).
Proof. 
by apply: (iff_trans (dirim_P _ x y)); split; 
   move => [u ux pr]; ex_tac; apply /igraph_pP.
Qed.

Lemma iim_fun_P x r y: 
  inc y (Vfi r x) <-> (exists2 u, inc u x & inc (J y u) (graph r)).
Proof. exact:iim_graph_P. Qed.


(** ** EII-3-3  Composition of two correspondences *) 

(** Composition of two graphs *)

Definition composeg r' r :=
  Zo ((domain r) \times (range r'))
  (fun w => exists2 y, inc (J (P w) y) r & inc (J y (Q w)) r').
 
Notation "x \cg y" := (composeg x y) (at level 50).

Lemma compg_graph r r': sgraph (r \cg r').
Proof. by move=> t /Zo_P [/setX_pair]. Qed. 

Hint Resolve compg_graph: fprops.

Lemma compg_P r r' x:
  inc x (r' \cg r) <->
  (pairp x /\ (exists2 y, inc (J (P x) y) r & inc (J y (Q x)) r')).
Proof.
split;first by move/Zo_P => [pa pb];split => //; apply: (setX_pair pa).
move => [pa pb]; apply: Zo_i => //. 
move: pb => [z pc pd];apply/setX_P;split => //; ex_tac.
Qed. 

Lemma compg_pP r r' x y:
  inc (J x y) (r' \cg r) <-> (exists2 z, inc (J x z) r & inc (J z y) r').
Proof.
apply: (iff_trans (compg_P _ _ _) ); aw.
split;[ by case | move => h; fprops].
Qed.

Lemma compg_domain_S r r': sub (domain (r' \cg r)) (domain r).
Proof. move => t /funI_P [y /compg_P [_ [s sa _]] ->]; ex_tac. Qed.

Lemma compg_rangeS r r':  sub (range (r' \cg r)) (range r').
Proof. move => t /funI_P [y /compg_P [_ [s _ sa]] ->]; ex_tac. Qed.

Lemma compg_composef f g: f \cfP g -> f \cf g =  f \cg g.
Proof.
move => [fgf fgg srd].
set_extens t.
  move /funI_P => [z zd ->]; apply /compg_pP.
  exists (Vg g z); apply: fdomain_pr1 => //; apply: srd.
  apply /range_gP => //; ex_tac.
move/compg_P => [pt [y Pt Qt]]; apply /funI_P; exists (P t); first by ex_tac.
by move: (pr2_V fgg Pt)(pr2_V fgf Qt); aw => <- <-. 
Qed.


(** Proposition 3, inverse of composition *)

Theorem compg_inverse: {morph inverse_graph : a b / a \cg b >-> b \cg a}.
Proof.
move => r r';set_extens x. 
  move/igraphP => [px] /compg_pP [z pa pb].
  by rewrite -px; apply/compg_pP; exists z => //; apply/igraph_pP.
move/compg_P => [px [y /igraph_pP pa /igraph_pP pb]]. 
by rewrite -px; apply/igraph_pP/compg_pP; exists y.
Qed.

(** Proposition 4,  associativity of composition *)

Theorem compgA : associative composeg.
Proof.
move => r r' r'';set_extens x.
  move /compg_P=> [px [y /compg_pP [z pa pb] pc]].
  rewrite -px; apply/compg_pP; ex_tac; apply/compg_pP; ex_tac.
move /compg_P=> [px [y pa /compg_pP [z pb pc]]].
rewrite -px; apply/compg_pP; ex_tac; apply/compg_pP; ex_tac.
Qed.

(** Proposition 5 Image of composition *)

Theorem compg_image: action_prop direct_image composeg.
Proof. 
move => gr_imegr' r x;set_extens t.
  move /dirim_P => [z zx /compg_pP [u pa pb]].
  apply/dirim_P; ex_tac; apply/dirim_P; ex_tac.
move /dirim_P => [z /dirim_P [u pa pb] pc].
apply/dirim_P; ex_tac; apply/compg_pP; ex_tac.
Qed.

(** More properties of composition *)

Lemma compg_domain r r':
  sgraph r' -> domain (r' \cg r) = inverse_image r (domain r').
Proof. 
move=>gr; have cg:= (@compg_graph r' r); set_extens t.
  move/(domainP cg) => [y /compg_pP [z pa pb]].
  apply/iim_graph_P; ex_tac; ex_tac.
move/iim_graph_P => [x /(domainP gr) [y pa] pb].
apply/(domainP cg); exists y; apply /compg_pP; ex_tac.
Qed.

Lemma compg_range r r':
  sgraph r -> range (r' \cg r) = direct_image r' (range r).
Proof.
move=>gr;have cg:= (@compg_graph r' r); set_extens t.
  move/(rangeP cg) => [y /compg_pP [z pa pb]]; apply/dirim_P; ex_tac; ex_tac.
move/dirim_P => [x /(rangeP gr) [y pa] pb].
apply/(rangeP cg); exists y; apply /compg_pP; ex_tac.
Qed.

Lemma inverse_direct_imageg r x:
  sgraph r -> sub x (domain r) ->
  sub x (inverse_image r (direct_image r x)).
Proof. 
move=> gt xd t tx.
move /funI_P: (xd _ tx)=> [y yr eq].
have aux:inc (J t (Q y)) r by rewrite eq (gt _ yr).
apply/iim_graph_P;ex_tac;apply/dirim_P; ex_tac.
Qed.

Lemma compg_S r r' s s':
  sub r s -> sub r' s' -> sub (r' \cg r) (s' \cg s).
Proof. 
move=> rs rs' t /compg_P [ {3} <- [ x ir ir']].
by apply/compg_pP; exists x; [apply: rs | apply: rs'].
Qed.

(** Composition of two correspondences *)

Definition composableC r' r := 
  [/\ correspondence r, correspondence r' & source r' = target r].
Definition compose r' r :=
  triple (source r)(target r') ((graph r') \cg (graph r)).

Notation "f1 \co f2" := (compose f1 f2) (at level 50).

Lemma compf_correspondence r' r:
  correspondence r -> correspondence r' -> 
  correspondence (r' \co r).
Proof.  
rewrite/compose=> cr cr'; apply: corresp_create.
move=>t /compg_P [pt [y ir ir']]; apply:setX_i => //.
  move /setX_P: ((proj2 cr) _ ir) => [_ pa _];move: pa; aw.
move /setX_P: ((proj2 cr') _ ir');aw; move => [_ _ pb]; move: pb; aw.
Qed.

Lemma compf_image: action_prop Vfs compose.
Proof. move => r' r x; rewrite /Vfs -compg_image /compose; aw. Qed.

Lemma compf_inverse: {morph inverse_fun : a b / a \co b >-> b \co a}.
Proof.
by move=> a b; rewrite /inverse_fun /compose; aw; rewrite compg_inverse.
Qed.

(** Identity correspondence, will be shown to be a function later *)

Definition identity x := triple x x (identity_g x). 

Lemma identity_corresp x: correspondence (identity x).
Proof. 
by apply: corresp_create; rewrite -diagonal_is_identity; apply: Zo_S.
Qed.

Lemma identity_s x: source (identity x) = x.
Proof. rewrite/identity; aw. Qed.

Lemma identity_t x: target (identity x) = x.
Proof. rewrite/identity; aw.  Qed. 

Lemma identity_graph0 x: graph (identity x) = identity_g x.
Proof. rewrite/identity; aw.  Qed. 

Hint Rewrite identity_s identity_t: aw.

Lemma compf_id_left m:
   correspondence m -> (identity (target m)) \co m = m.
Proof. 
move=> cm.
suff : ((identity_g (target m)) \cg (graph m) = graph m).
  by rewrite /compose identity_graph0; aw => ->; apply: corresp_recov1.
rewrite -diagonal_is_identity.
set_extens t.
  by move /compg_P=> [ {3} <- [y p1 /diagonal_pi_P [_ <-]]].
have gm: (sgraph (graph m)) by fprops.
move => tg; apply/compg_P; split; first by apply: (gm _ tg).
move /setX_P: ((proj2 cm) _ tg) => [pt _ qt].
by exists (Q t); [ rewrite pt | apply/diagonal_pi_P].
Qed. 

Corollary compose_identity_left E:
  {when (fun x => correspondence x /\ (target x) = E),
  left_id (identity E) compose}.
Proof. move => x [cx <-]; exact:compf_id_left. Qed.

Lemma compf_id_right m:
  correspondence m -> m \co (identity (source m)) = m.
Proof. 
move=> cm.
suff: ((graph m) \cg (identity_g (source m))= graph m).
  by rewrite /compose identity_graph0; aw => ->; apply: corresp_recov1.
rewrite -diagonal_is_identity.
set_extens t.
  by move /compg_P => [ {3} <- [y /diagonal_pi_P [pa ->] p1]].
have gm: (sgraph (graph m)) by fprops.
move => tg; apply/compg_P; split; first by apply: (gm _ tg).
move /setX_P: (proj2 cm _ tg) => [pt qt _].
by exists (P t); [ apply/diagonal_pi_P | rewrite pt ].
Qed.

Lemma compf_id_id x: 
  (identity x) \co (identity x) =  (identity x).
Proof. by move: (compf_id_right (@identity_corresp x)); aw. Qed.

Lemma identity_self_inverse x: 
  inverse_fun (identity x) =  (identity x).
Proof. rewrite /inverse_fun /identity; aw. Qed.

End Correspondence.

Export Correspondence.

(** **  EII-3-4 Functions*)
Module Bfunction.

Import Correspondence.

(** This is a different but equivalent definition *)

Definition functional_graph r := forall x, singl_val (related r x).

Lemma functionalP r:
  (sgraph r /\ functional_graph r) <-> (fgraph r).
Proof. 
rewrite /functional_graph /related; split; last first.
  by move=> fr; split; fprops; move=> x y y'; apply: fgraph_pr.
move => [gr eql]; split=>// x y xr yr eqp.
move: (xr) (yr); rewrite -(gr _ xr) - (gr _ yr) -eqp => pa pb.
by rewrite (eql _ _ _ pa pb).
Qed.

(** A function is a correspondence with a functional graph whose
   source is the domain of the graph *)

Definition function f :=
  [/\ correspondence f, fgraph (graph f) & source f = domain (graph f)].

Lemma function_pr s t g:
  fgraph g -> sub (range g) t -> s = domain g ->
  function (triple s t g).
Proof. 
rewrite /function => fg sr d; aw; split => //.
by apply: corresp_create; rewrite d; apply /corr_propcc; split => //;case: fg.
Qed.

Lemma function_fgraph f: function f -> fgraph (graph f).
Proof. by move=> [_]. Qed.

Lemma function_sgraph f: function f -> sgraph (graph f).
Proof. by move=> [_ [h _]]. Qed.

Lemma f_domain_graph f: function f -> domain (graph f) = source f.
Proof. by move=> [_ ]. Qed.

Lemma f_range_graph f: function f -> sub (range (graph f))(target f).
Proof. by move => [cf _ _]; apply:corresp_sub_range. Qed.

Hint Rewrite f_domain_graph : aw.
Hint Resolve function_sgraph function_fgraph : fprops.

Lemma image_by_fun_source f: function f -> 
  Imf f =  range (graph f).
Proof.
move=> ff; rewrite /Imf -f_domain_graph //.
by apply: dirim_domain; fprops.
Qed.


(** The value of the function [f] at [x] is [Vf x f] *)

Definition Vf f x := Vg (graph f) x.

Section Vf_pr.
Variable  f: Set.
Hypothesis ff: function f.

Lemma Vf_pr3 x: inc x (source f) -> inc (J x (Vf f x)) (graph f).
Proof. by move=> xf; apply: fdomain_pr1; fprops; aw. Qed.

Lemma in_graph_Vf x: inc x (graph f) -> x = (J (P x) (Vf f (P x))).
Proof. by move=> xf; apply: in_graph_V; fprops. Qed.

Lemma Vf_pr2 x: inc x (graph f) -> Q x = Vf f (P x).
Proof. by move=> xg; apply: pr2_V; fprops. Qed.

Lemma Vf_pr x y: inc (J x y) (graph f) -> y = Vf f x.
Proof. by move=> Jg; move: (in_graph_Vf Jg); aw; apply: pr2_def. Qed.

Lemma range_fP y: 
  inc y (range (graph f)) <-> exists2 x, inc x (source f) & y = Vf f x.
Proof. move: ff => [_ fgf ->]; apply/(range_gP fgf). Qed.

Lemma Vf_range_g x: inc x (source f) -> inc (Vf f x) (range (graph f)).
Proof. move=> xsf; apply /range_fP;ex_tac.  Qed.

Lemma Vf_target x: inc x (source f) -> inc (Vf f x) (target f).
Proof. move/Vf_range_g;apply: (f_range_graph ff).
Qed.

Lemma p1graph_source x y: inc (J x y) (graph f) -> inc x (source f).
Proof. move: ff => [_ fgf ->] jg; ex_tac. Qed.

Lemma p2graph_target x y : inc (J x y) (graph f) -> inc y (target f).
Proof.
move=> Jgf; rewrite (Vf_pr Jgf); apply: Vf_target; apply: (p1graph_source Jgf).
Qed.

Lemma p1graph_source1 x: inc x (graph f) -> inc (P x) (source f).
Proof. 
move=> xgf; apply: (p1graph_source (y:= (Vf f (P x)))).
by rewrite - (in_graph_Vf xgf).
Qed.

Lemma p2graph_target1 x: inc x (graph f) -> inc (Q x) (target f).
Proof.
move=> xgf; rewrite (in_graph_Vf xgf); aw. 
by apply: Vf_target => //; apply: p1graph_source1.
Qed.

Lemma Vf_image_P x: sub x (source f) -> forall y,
  (inc y (Vfs f x) <-> exists2 u, inc u x & y = Vf f u).
Proof. 
rewrite /Vfs => ss;split.
  by move/dirim_P => [a ax Jg]; ex_tac; apply: Vf_pr.
move=> [u ux ->]; apply/dirim_P; ex_tac;apply: Vf_pr3; fprops.
Qed.

Lemma Vf_image_P1 y:
  inc y (Imf f)  <-> (exists2 u, inc u (source f) & y = Vf f u).
Proof. exact: (Vf_image_P (@sub_refl (source f))). Qed.

Lemma fun_image_Starget1 x: sub (Vfs f x) (target f).
Proof. apply: sub_trans (f_range_graph ff); apply: dirim_Sr. Qed.

Lemma fun_image_Starget: sub (Imf f) (target f).
Proof. apply: fun_image_Starget1. Qed.

End Vf_pr.

Hint Resolve Vf_target : fprops.


Ltac Wtac :=
  match goal with
    | |-  inc (J ?x (Vf ?f ?x)) (graph ?f) => apply: Vf_pr3 ; fprops
    |  h:inc (J ?x ?y) (graph ?f) |- Vf ?f ?x = ?y 
       => symmetry; apply: Vf_pr ; fprops
    |  h:inc (J ?x ?y) (graph ?f) |- ?y  = Vf ?f ?x => apply: Vf_pr ; fprops
    | |- inc (Vf ?f _) (range (graph ?f)) => apply: Vf_range_g ; fprops
    | h1: function ?f, h2: inc ?x (source ?f) |- inc (Vf ?f ?x) (target ?f)  
        => apply: (Vf_target h1 h2)
    | h2:target ?f = ?y |- inc (Vf ?f ?x) ?y 
        =>  rewrite - h2; Wtac
    | h2: ?y = target ?f  |- inc (Vf ?f ?x) ?y 
      =>  rewrite  h2; Wtac
    | h1: inc ?x ?y,  h2: ?y = source ?f |- inc (Vf ?f ?x) (target ?f)  
      =>  rewrite h2 in h1; Wtac
    | h1: inc ?x ?y,  h2: source ?f = ?y |- inc (Vf ?f ?x) (target ?f)  
      => rewrite - h2 in h1; Wtac
    | |- inc (Vf ?f _) (target ?f)  
        => apply: (Vf_target); fprops
    | Ha:function ?X1, Hb: inc (J _ ?X2) (graph ?X1)
      |-  inc ?X2 (target ?X1)
        => apply: (p2graph_target Ha Hb)
    | Ha:function ?X1, Hb: inc (J ?X2 _) (graph ?X1)
      |-  inc ?X2 (source ?X1)
        => apply: (p1graph_source Ha Hb)
    | Ha:function ?X1, Hb: inc ?X2 (graph ?X1)
      |-  inc (P ?X2) (source ?X1)
        => apply: (p1graph_source1 Ha Hb)
    | Ha:function ?X1, Hb: inc ?X2 (graph ?X1)
      |-  inc (Q ?X2) (target ?X1)
        => apply: (p2graph_target1 Ha Hb)
  end.

Lemma function_functional f: correspondence f ->
  (function f <-> (forall x, inc x (source f) -> 
    exists! y, related (graph f) x y)).
Proof.
rewrite/related=> cf; split. 
  move=> ff x xsf;exists (Vf f x); split; first by Wtac.
  move => y yg; symmetry; apply: (Vf_pr ff yg).
move => eu.
have sd:source f = domain (graph f).
  apply: extensionality; last by fprops.
  move=> t ts; move: (eu _ ts) => [y [ja jb]]. 
  by apply/funI_P; ex_tac; aw.
split=>//;apply /functionalP; split; first by fprops.
move=> x y y'; rewrite /related => h1.
have isf: inc x (source f) by rewrite sd; apply/funI_P; ex_tac; aw.
move: h1; move/unique_existence: (eu _ isf) => [_]; apply.
Qed.

(** Lemmas that say when two functions are equal *)

Definition same_Vf  f g:= Vf f =1 Vf g.
Definition cstfp (f E: Set) := singl_val_fp (inc ^~E) (Vf f).
Definition cstgp (f E: Set) := singl_val_fp (inc ^~E) (Vg f).


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

Lemma function_exten3 f g:
  function f -> function g ->
  graph f = graph g -> target f = target g -> source f = source g -> 
  f = g.
Proof. 
move => [[ff _] _ _]  [[fg _] _ _] e1 e2 e3.
by rewrite -(corresp_recov ff) -(corresp_recov fg); congr (triple _ _ _).
Qed.

Lemma function_exten1 f g:
  function f -> function g -> 
  graph f = graph g -> target f = target g -> 
  f = g.
Proof. 
move => ff fg e1 e2; apply: function_exten3=>//. 
by rewrite -!f_domain_graph // e1.
Qed.

Lemma function_exten f g:
  function f -> function g -> 
  source f = source g -> target f = target g ->  {inc (source f), f =1f g} ->
  f = g.
Proof.
move=> ff fg e1 r2 e2; apply: function_exten3=> //. 
set_extens x => xg.
  have Pf : (inc (P x) (source f)) by Wtac. 
  by rewrite (in_graph_Vf ff xg) (e2 _ Pf);  Wtac; rewrite -e1.
have Pg : (inc (P x) (source f)) by rewrite e1; Wtac. 
by rewrite (in_graph_Vf fg xg) -(e2 _ Pg);  Wtac. 
Qed. 

(** The image of singleton by a function is a singleton*)

Lemma fun_image_set1 f x:
  function f -> inc x (source f) ->
  Vfs f (singleton x) = singleton (Vf f x).
Proof. 
move=> ff xsf.
apply: set1_pr; first by apply /dirim_set1_P; Wtac.
by move => z /dirim_set1_P jg; apply:Vf_pr.
Qed.

Lemma fun_image_set0 f: Vfs f emptyset = emptyset.
Proof. by apply /set0_P => t /Zo_hi [x /in_set0]. Qed.

Lemma iim_fun_C g x:
  function g ->
  Vfi g ((target g) -s x) = (source g) -s (Vfi g x).
Proof.
move => fg. 
have gg: sgraph (graph g) by fprops.
set_extens t. 
  move/iim_graph_P => [u /setC_P [ut nux] Jug];apply/setC_P. 
  split; first by Wtac.
  move/iim_graph_P => [w wx Jwg].
  by case: nux; rewrite (fgraph_pr (proj32 fg) Jug Jwg).
move/setC_P =>  [ts neu].
have Jg: (inc (J t (Vf g t))(graph g)) by Wtac.
apply/iim_graph_P; ex_tac;apply/setC_P; split; fprops.
dneg Wx; apply/iim_graph_P; ex_tac.
Qed.

Lemma iim_fun_set1_hi f x y: function f ->
   inc x (Vfi1 f y) -> y = Vf f x.
Proof. by move => ff /iim_fun_P [u /set1_P ->]; apply: Vf_pr. Qed.

Lemma iim_fun_set1_i f x y: function f -> inc x (source f) ->
  y = Vf f x -> inc x (Vfi1 f y).
Proof. move => ff xsf ->; apply /iim_fun_P; ex_tac; Wtac. Qed.

Lemma iim_fun_set1_P f y: function f -> forall x,
   inc x (Vfi1 f y) <-> 
   (inc x (source f) /\ y = Vf f x).
Proof. 
move => ff x; split.
  move /iim_fun_P => [u /set1_P -> pa]; split;Wtac.
by move => [pa pb]; apply:iim_fun_set1_i.
Qed.

Lemma iim_fun_set1_E f y: function f ->
   (Vfi1 f y) = Zo (source f) (fun x => y = Vf f x).
Proof.
move => ff; set_extens t.
  by move /(iim_fun_set1_P _ ff) => pa; apply /Zo_P.
by move => /Zo_P pa; apply /(iim_fun_set1_P _ ff).
Qed.



Definition function_prop f s t:= 
  [/\ function f, source f = s & target f = t]. 

(** Function with empty graph *)

Definition empty_function_tg (x: Set) :=  triple emptyset x emptyset.
Definition empty_function:= empty_function_tg emptyset.

Lemma empty_function_tg_function x: 
  function_prop (empty_function_tg x) emptyset x.
Proof.
hnf; rewrite /empty_function_tg; aw; split => //; apply: function_pr; bw.
- apply: fgraph_set0.
- fprops.
Qed.

Lemma empty_function_function: function_prop empty_function emptyset emptyset.
Proof. apply:empty_function_tg_function. Qed.

Lemma empty_function_graph x: graph (empty_function_tg x) = emptyset.
Proof. rewrite /empty_function_tg; aw. Qed.

Lemma empty_function_p1 f: function f ->
  graph f = emptyset -> source f = emptyset.
Proof. move => [_ _ ->] ->; bw. Qed.

Lemma empty_function_p2 f: function f ->
  target f = emptyset -> source f = emptyset.
Proof. 
by move => ff te; apply /set0_P => x /(Vf_target ff); rewrite te => /in_set0. 
Qed.

Lemma empty_source_graph f:
  function f -> source f = emptyset -> graph f = emptyset.
Proof. 
move => ff sfe; apply /set0_P => x xp.
apply: (@in_set0 (P x)); rewrite - sfe; Wtac.
Qed. 

Lemma empty_target_graph f:
  function f -> target f = emptyset -> graph f = emptyset.
Proof.
move => ff sfe; apply /set0_P => x xp. 
case: (@in_set0 (Vf f (P x))); Wtac; Wtac.
Qed.

Lemma empty_source_graph2 f:
  function f -> source f = emptyset -> 
  f =  empty_function_tg (target f).
Proof. 
move => pa pb;have pc:= (empty_source_graph pa pb).
by rewrite /empty_function_tg -{1} (corresp_recov (proj1 (proj31 pa))) pb pc.
Qed. 

(** Properties of the identity function *)

Lemma identity_prop x: function_prop (identity x) x x.
Proof.
rewrite /identity /function_prop; aw; split => //; apply: function_pr.
- by apply: identity_fgraph. 
- by rewrite identity_r; fprops. 
- by rewrite identity_d.
Qed.

Lemma identity_f x: function (identity x).
Proof. exact: (proj31 (identity_prop x)). Qed.

Lemma identity_V x y: inc y x -> Vf (identity x) y = y.
Proof. move =>yx; rewrite /Vf /identity; aw; apply:(identity_ev yx). Qed.

Hint Rewrite identity_V: bw.
Hint Resolve identity_f: fprops.

Lemma identity_prop0 E f:
  function_prop f E E -> (forall x, inc x E -> (Vf f x) = x) ->
  f = identity E.
Proof.
move: (identity_prop E) =>  [fa sa ta] [fb sb tb] fv.
apply:function_exten => //; try ue.
by rewrite sb => x xE; bw; apply: fv.
Qed.



(** ** EII-3-5 Restrictions and extensions of functions *) 

(**  The functions agree on [x] if they take the same value *)
Definition agrees_on x f f' :=
  [/\ sub x (source f), sub x (source f') & {inc x, f =1f f'} ].

Lemma same_graph_agrees f f':
  function f -> function f' -> graph f = graph f' ->
  agrees_on (source f) f f'.
Proof. 
move=> ff ff' geq. 
have seq: (source f = source f'). 
  by rewrite -(f_domain_graph ff) -(f_domain_graph ff') geq.
rewrite /agrees_on - seq; split; fprops.
move=> a /(Vf_pr3 ff); rewrite geq => aux.
by rewrite -(Vf_pr ff' aux). 
Qed.

Lemma function_exten2 f f':
  function f -> function f' ->
  (f = f' <-> 
   [/\ source f = source f', target f = target f' & agrees_on (source f) f f']).
Proof. 
move=> ff ff'; split. 
  by rewrite /agrees_on; move => -> ;split => //; split. 
move => [seq teq [_ _ ag]]; apply: function_exten; fprops. 
Qed.

Lemma sub_functionP f g:
  function f -> function g -> 
  (sub (graph f) (graph g) <-> agrees_on (source f) f g).
Proof. 
move=> ff fg; split => hyp.
  split => //.
    by do 2 rewrite -f_domain_graph=>//; apply: domain_S.  
  by move=> a af /=;rewrite- (Vf_pr fg (hyp _ (Vf_pr3 ff af))).
move => t tg; move: hyp => [_ sg ag].
have Ptsf: (inc (P t) (source f)) by Wtac.
rewrite (in_graph_Vf ff tg) (ag _ Ptsf);  Wtac. 
Qed.

(** Restriction of the function to a part of it source *)

Lemma restr_range f x:
  function f -> sub x (source f) -> 
  sub (range (restr (graph f) x)) (target f).
Proof. 
move=> ff sxdf t /funI_P [z /funI_P [s zg ->] ->]; aw;rewrite -/(Vf _ _); Wtac. 
Qed.

Definition restriction f x :=
  triple x (target f) (restr (graph f) x).

Definition restriction1 f x :=
  triple x (Vfs f x) (restr (graph f) x).

Definition restriction2 f x y := 
  triple x y ((graph f)\cap (x \times (target f))).

Definition restriction2_axioms f x y :=
  [/\ function f,
  sub x (source f), sub y (target f) & sub (Vfs f x) y].

Lemma restriction_prop f x:
  function f -> sub x (source f) ->
  function_prop (restriction f x) x (target f).
Proof.
rewrite /restriction /function_prop=> ff xs; aw; split => //. 
by apply: function_pr; bw; fprops; apply: restr_range.
Qed.

Lemma restriction1_prop f x:
  function f -> sub x (source f) ->
  function_prop (restriction1 f x) x (Vfs f x).
Proof.
rewrite /restriction1 /function_prop =>ff ssf; aw; split => //.
apply: function_pr; fprops; bw.
rewrite Lg_range => t /funI_P [z zx  ->]; apply/dirim_P; ex_tac.
rewrite -/(Vf _ _); Wtac.
Qed.

Lemma restriction2_props f x y:
  restriction2_axioms f x y ->
  domain ((graph f) \cap (x \times (target f))) = x.
Proof. 
move=> ra; set i := _ \cap _.
have gi: sgraph i by rewrite /i => t /setI2_P [_] /setX_P [].
set_extens t.
  by move/funI_P => [z /setI2_P [_ /setX_P [_ h _]] ->].
move:ra => [ ff xsf ysf etc] tx.
apply/(domainP gi); exists (Vf f t); apply/setI2_P; split; [Wtac| ].
apply: setXp_i => //; Wtac.
Qed.

Lemma restriction2_prop f x y:
  restriction2_axioms f x y -> function_prop (restriction2 f x y) x y.
Proof. 
move=> ra; move:(ra) => [ff ss st etc].
rewrite /restriction2 /function_prop; aw; split => //.
move:(restriction2_props ra); set g :=  _ \cap _  => dg.
have fg: fgraph g.
  rewrite /g; apply: (@sub_fgraph _ (graph f)); fprops; apply: setI2_1.
apply: function_pr=>// t tr; apply: etc; apply /dirim_P.
move/(rangeP (proj1 fg)): tr => [z /setI2_P [jg /setXp_P [zx _]]];ex_tac.
Qed.

Lemma restriction_V f x:
  function f -> sub x (source f) ->
  {inc x, (restriction f x) =1f f}.
Proof. rewrite /Vf/restriction => ff ss a xa; aw; bw; fprops; aw. Qed.

Lemma restriction1_V f x:
  function f -> sub x (source f) ->
  {inc x, (restriction1 f x) =1f f}.
Proof. rewrite /Vf/restriction1 => ff ss a xa; aw; bw; fprops; aw.  Qed.

Lemma restriction2_V f x y:
  restriction2_axioms f x y ->
  {inc x, (restriction2 f x y) =1f f}.
Proof. 
move => ra a ax; move: (ra) => [ff sf tf sif].
rewrite /Vf/restriction2; aw.
apply: sub_graph_ev; fprops;first by apply: setI2_1.
by rewrite (restriction2_props ra).
Qed.

Lemma restriction1_pr f:
  function f -> restriction2 f (source f) (Imf f) =
  restriction1 f (source f).
Proof. 
rewrite/restriction2/restriction1=> ff. 
have rg: (restr (graph f) (source f) = graph f).
  rewrite (proj33 ff); apply: restr_to_domain; fprops.
by rewrite (proj1 (setI2id_Pl _ _) (proj2 (proj31 ff))) rg.
Qed.

(** [g] extends [f] if its restriction to the source of [f] is [f] *)

Definition extends g f := 
  [/\ function f, function g,  sub (graph f) (graph g)
    & sub (target f)(target g) ].

Lemma extends_Ssource f g:
  extends g f -> sub (source f) (source g).
Proof.
by move=> [ff fg sg st]; do 2 rewrite -f_domain_graph=>//; apply: domain_S.
Qed.

Lemma extends_sV f g:
  extends g f -> {inc (source f), f =1f g}.
Proof.
move=> ext x xf; have ss:= (extends_Ssource ext).
have [ff fg sg _] := ext.
have pg:  (inc (J x (Vf f x)) (graph g)) by apply: sg; Wtac. 
by rewrite (Vf_pr fg pg).
Qed.

Lemma function_extends_restr f x:
  function f -> sub x (source f) ->
  extends f (restriction f x).
Proof.
move =>ff ssf; have [pa pb pc] := (restriction_prop ff ssf).
split => //; last by rewrite pc.
rewrite /restriction; aw => s /funI_P [z zx ->]. 
by apply: Vf_pr3 => //; apply: ssf.
Qed.


Lemma agrees_same_restriction f g x:
  function f -> function g -> agrees_on x f g ->
  target f = target g -> 
  restriction f x =
  restriction g x.
Proof.
move=> ff fg [sf sg vfg] t.
move:(restriction_prop ff sf)(restriction_prop fg sg)=>[pa pb pc][pd pe pf].
apply: function_exten; fprops; try solve [rewrite /restriction; aw].
rewrite {1} /restriction; aw=> z zs.
by do 2 rewrite restriction_V => //; apply: vfg.
Qed.

Lemma restriction_graph1 f x:
  function f -> sub x (source f) ->
  graph (restriction f x) =  (graph f) \cap (x \times (target f)).
Proof. 
rewrite /restriction => ff xs; aw;set_extens t; last first.
  move/setI2_P => [tg /setX_P [pa pb pc]]; apply /funI_P; ex_tac.
  by apply: in_graph_Vf.
move/funI_P => [z pa ->]. 
apply:setI2_i; first by rewrite -/(Vf _ _); Wtac.
apply/setX_P; aw;split; fprops; rewrite -/(Vf _ _); Wtac.
Qed.

Lemma restriction_recovers f x:
  function f -> sub x (source f) ->
  restriction f x = triple x (target f) 
    ((graph f) \cap (x \times (target f))).
Proof.
move=> ff ss; rewrite -(restriction_graph1 ff ss) /restriction; aw.
Qed.

(** Restriction of a function on the source and target *)


Lemma function_rest_of_prolongation f g:
  extends g f -> f = restriction2 g (source f) (target f).
Proof.
move=>[ff fg].
move /(sub_functionP ff fg)=> [_ sts sg] st.
have au: (sub (Vfs g (source f)) (target f)).
  by move =>t /(Vf_image_P fg sts) [u us ->]; rewrite - sg=>//; fprops. 
have ax: (restriction2_axioms g (source f) (target f)) by [].
apply: function_exten;fprops; try solve [rewrite /restriction2; aw].
  apply: (proj31 (restriction2_prop ax)).
by move => x sf /=; rewrite restriction2_V // sg.  
Qed.


(** ** EII-3-6 Definition of a function by means of a term *) 

(** Function from [a] to [b] associated to the mapping [f] *)

Definition Lf f a b := triple a b (Lg a f).

Lemma lf_source f a b: source (Lf f a b) = a.
Proof. rewrite /Lf/Lg; aw.  Qed.

Lemma lf_target f a b: target (Lf f a b) = b.
Proof. rewrite /Lf/Lg; aw.  Qed.

Hint Rewrite lf_source lf_target : aw.

Lemma lf_graph1 f a b c: 
  inc c (graph (Lf f a b)) -> c = J (P c) (f (P c)).
Proof. rewrite/Lf/Lg; aw;move/funI_P => [z _ ->]; aw. Qed.

Lemma lf_graph2 f a b c:
  inc c a -> inc (J c (f c)) (graph (Lf f a b)).
Proof. by rewrite /Lf/Lg=> ca; aw; apply/funI_P; ex_tac. Qed.

Lemma lf_graph3 f a b c:
  inc c (graph (Lf f a b)) -> inc (P c) a.
Proof. rewrite /Lf/Lg; aw; move/funI_P=> [z za ->]; aw. Qed.

Lemma lf_graph4 f a b c:
  inc c (graph (Lf f a b)) -> f (P c) = (Q c). 
Proof.  move=> h; rewrite {2} (lf_graph1 h); aw. Qed.

(** In order for [(Lf f a b)] to be a function, the following must be satisfied *)

Definition lf_axiom f a b :=
  forall c, inc c a -> inc (f c) b. 

Lemma lf_function f a b:
  lf_axiom f a b -> function (Lf f a b).
Proof. 
move=> ta; apply: function_pr; bw; fprops.
by move=> t; rewrite Lg_range; move/funI_P=> [z zb ->]; apply: ta.
Qed.

Lemma lf_function_prop f a b:
  lf_axiom f a b -> function_prop (Lf f a b) a b.
Proof. move /lf_function =>h; split =>//; aw. Qed.
  
Lemma lf_V f a b c: lf_axiom f a b ->  inc c a -> Vf (Lf f a b) c = f c.
Proof. 
by move=> /lf_function ff ca; symmetry; apply:Vf_pr => //; apply: lf_graph2.
Qed. 

Hint Rewrite lf_V : aw.

Lemma lf_recovers f: 
  function f -> Lf (Vf f)(source f)(target f) = f.
Proof. 
move=> ff.
have ta: (lf_axiom (Vf f) (source f) (target f)) by move=> x /=; fprops. 
apply: function_exten;aw; [ by apply: lf_function | move => x sx /=; aw]. 
Qed.

Lemma identity_Lf x: identity x = Lf id x x.
Proof.
have aux: lf_axiom id x x by done.
apply function_exten; fprops; first by apply :lf_function.
move => t; rewrite lf_source => tx; aw; bw.
Qed.

Lemma restriction_Lf f x: function f -> sub x (source f) ->
 restriction f x = Lf (Vf f) x (target f).
Proof.
move => h1 h2; move: (restriction_prop h1 h2) => [pa pb pc].
have pd: lf_axiom (Vf f) x (target f) by move => t tw; Wtac.
apply: function_exten; aw.
by rewrite /restriction;aw;move => t rs /=; aw; apply:restriction_V.
Qed.


(** Definition of a constant function and of the constant function *)

Definition constantfp f := function f /\  cstfp f (source f).
Definition constantgp f := fgraph f /\ cstgp f (domain f).

Lemma constant_prop1 f: constantgp f -> small_set (range f).
Proof. 
move=> [ff eq] t1 t2 /(range_gP ff) [x xd ->] /(range_gP ff) [y yd ->]. 
by apply: eq.
Qed.

Lemma constant_prop2 f: constantfp f -> constantgp (graph f).
Proof. move=> [ff eq]; split; fprops; by move:ff=> [_ _ <-].  Qed.

Lemma constant_prop3 x y: constantgp (cst_graph x y).
Proof. 
split; [ fprops | move => a b; rewrite cst_graph_d => ax bx; bw ].
Qed.

Lemma constant_prop4 f: function  f -> 
  (constantfp f <-> small_set (range (graph f))).
Proof. 
move => ff; split => h.
  by apply: constant_prop1; apply: constant_prop2.
split=> // x x' xs x's; apply: h; Wtac.
Qed.

Definition constant_function A B y := Lf (fun _ : Set => y) A B.

Lemma constant_s A B y: source (constant_function A B y) = A.
Proof. rewrite /constant_function; aw. Qed.

Lemma constant_t A B y: target (constant_function A B y) = B.
Proof. rewrite /constant_function; aw. Qed.

Lemma constant_g A B y: graph (constant_function A B y) =  A *s1 y.
Proof. by rewrite /constant_function /Lf corresp_g - cst_graph_pr. Qed.

Lemma constant_f A B y: inc y B -> function (constant_function A B y).
Proof. by move => yB; apply:lf_function. Qed.

Lemma constant_prop A B y: inc y B ->
  function_prop (constant_function A B y) A B.
Proof. by move => yB; apply:lf_function_prop. Qed.

Lemma constant_V A B y x: inc y B -> inc x A ->
 Vf (constant_function A B y) x = y.
Proof. 
by move => ha hb; rewrite /constant_function; aw.
Qed.

Lemma constant_constant_fun A B y: inc y B ->
  constantfp (constant_function A B y).
Proof. 
split; first by apply: constant_f.
rewrite constant_s => u v /= us vs; do 2 rewrite constant_V=>//. 
Qed.

Lemma constant_prop6 f:
  constantfp f ->
  f = empty_function_tg (target f) \/ 
  exists2 a, inc a (target f) & f = constant_function (source f) (target f) a.
Proof.
move => [pa pb].
case: (emptyset_dichot (source f)) => h.
  by left; rewrite {1} (empty_source_graph2 pa h).
right; have h':=(rep_i h); have h'' := (Vf_target pa h').
ex_tac; apply: function_exten; rewrite/constant_function;aw.
- by apply: constant_f.  
- by move => i isf /=; aw => //; apply: pb.
Qed. 

(** Functions associated to P and Q *)

Definition first_proj g := Lf P g (domain g).
Definition second_proj g := Lf Q g (range g).

Lemma first_proj_V g: {inc g, Vf (first_proj g) =1 P}.
Proof. by rewrite /first_proj=> x xg; aw =>t; apply: domain_i1. Qed.

Lemma second_proj_V g: {inc g, Vf (second_proj g) =1 Q}.
Proof. by rewrite /second_proj=> x xg; aw =>t; apply: range_i2. Qed.

Lemma first_proj_f g:  function (first_proj g).
Proof. by apply: lf_function =>t; apply: domain_i1. Qed. 

Lemma second_proj_f g: function (second_proj g). 
Proof. by apply: lf_function =>t; apply: range_i2. Qed.


(** ** EII-3-7  Composition of two functions. Inverse function *) 

(** Condition for composition to be a function  *)

Definition composable g f :=  
  [/\ function g, function f &  source g = target f].

Notation "f1 \coP f2" := (composable f1 f2) (at level 50).

Lemma composable_pr f g: g \coP f -> (graph g) \cfP (graph f).
Proof.
by move=> [fg ff st]; split; fprops; aw; rewrite st; apply: f_range_graph.
Qed.

Lemma compf_graph:
  {when: composable, {morph graph: f g / f \co g >-> f \cf g}}.
Proof. 
move => a b cfg; move:(composable_pr cfg)=> ac.
by rewrite /compose compg_composef; aw.
Qed.

Lemma compf_domg g f:  g \coP f-> 
  domain (graph (g \co f)) = domain (graph f).
Proof. 
move => cfg; rewrite compf_graph /composef; bw.
Qed.

Lemma compf_s f g: source (g \co f) = source f.
Proof. rewrite /compose; aw. Qed.

Lemma compf_t f g: target (g \co f) = target g.
Proof. rewrite /compose; aw. Qed.

Hint Rewrite compf_s compf_t : aw.


(** Proposition 6: composition of functions is a function *)

Theorem compf_f g f: g \coP f -> function (g \co f).
Proof. 
move=> cgf; 
have cd:=(compf_domg cgf).
have ac:=(composable_pr cgf).
have fgcc:= (composef_fgraph (graph g) (graph f)). 
have cg := (compf_graph cgf); rewrite cg in cd.
move: cg; rewrite /compose; aw => ->.
have [fg ff etc] := cgf.
apply: function_pr => //; last by rewrite cd f_domain_graph. 
apply: (sub_trans (composef_range ac)(f_range_graph fg)).
Qed.


(** Definition of injectivity, surjectivity and bijectivity *)

Definition injection f:=
  function f /\ {inc source f &, injective (Vf f)}.

Definition surjection f :=
  function f /\ 
  (forall y, inc y (target f) -> exists2 x, inc x (source f) & Vf f x = y).

Definition bijection f := injection f /\ surjection f.

(** We give here here some characterizations of injective, surjective, 
bijective functions *)


Lemma inj_function f: injection f -> function f.
Proof. by case. Qed.

Lemma surj_function f: surjection f -> function f.
Proof. by case. Qed.

Lemma bij_function f: bijection f -> function f.
Proof.  by case; case. Qed.

Lemma bij_inj f: bijection f -> {inc source f &, injective (Vf f)}.
Proof. move => h; exact: (proj2 (proj1 h)). Qed.

Lemma bij_surj f: bijection f -> 
   (forall y, inc y (target f) -> exists2 x, inc x (source f) & Vf f x = y).
Proof. move => h; exact: (proj2 (proj2 h)). Qed.

Ltac fct_tac := 
  match goal with
    | H:bijection ?X1 |- function ?X1 => exact (bij_function H)
    | H:injection ?X1 |- function ?X1 => exact (inj_function H)
    | H:surjection ?X1 |- function ?X1 => exact (surj_function H)
    | H:function ?X1 |- correspondence ?X1 =>
      by case H
    | H:function ?g |- sub (range (graph ?g)) (target ?g)
      => apply: (f_range_graph H)
    | H:composable ?X1 _ |- function ?X1 => exact (proj31 H)
    | H:composable _ ?X1 |- function ?X1 => exact (proj32 H)
    | H:composable ?f ?g |- function (compose ?f ?g ) =>
     apply: (compf_f H)
    | H:function ?f |- function (compose ?f ?g ) =>
     apply: compf_f; split => //
    | H:function ?g |- function (compose ?f ?g ) =>
     apply: compf_f; split => //
    | Ha:function ?f, Hb:function ?g |- ?f = ?g =>
      apply: function_exten
  end.

(** More properties of function composition *)

Lemma compf_V g f x: g \coP f ->
  inc x (source f) -> Vf (g \co f) x = Vf g (Vf f x).
Proof.  
rewrite /Vf => cgf xs; rewrite compf_graph=>//. 
apply: composef_ev; aw; fct_tac.
Qed.

Hint Rewrite compf_V: aw.


Lemma compfA f g h: f \coP g -> g \coP h ->
   f \co (g \co h) = (f \co g) \co h.
Proof.
move=> cfg chg.
have [gg fh sgth]: g \coP h by []. 
have ffg: (function (f \co g)) by fct_tac.
have fgh: (function (g \co h)) by fct_tac.
have cfgh: (f \co g) \coP h by hnf; aw. 
have cfgh': (f \coP (g \co h)) by move: cfg=> [ff _ etc];hnf; aw.
apply: function_exten; try fct_tac; aw. 
by move=> x xh /=; aw; rewrite sgth; fprops.
Qed.

Lemma compf_id_l m:
  function m -> (identity (target m)) \co m = m.
Proof. move=>fm; apply: compf_id_left; fct_tac. Qed.

Lemma compf_id_r m: 
  function m -> m \co (identity (source m)) = m.
Proof. move=> fm; apply: compf_id_right; fct_tac. Qed.

Corollary fcomp_identity_left E:
  {when (fun x => function x /\ (target x) = E),
  left_id (identity E) compose}.
Proof. move => x [cx <-]; exact:compf_id_l. Qed.


Lemma injective_pr f y: injection f ->
   singl_val (fun x => related (graph f) x y).
Proof.
rewrite /related;move=> [ff injf] x x' r1 r2; apply: injf.
- by Wtac.
- by Wtac.
- by rewrite - (Vf_pr ff r1) (Vf_pr  ff r2). 
Qed.

Lemma injective_pr3 f y: injection f ->
   singl_val (fun x => inc (J x y) (graph f)).
Proof. apply: injective_pr.  Qed.

Lemma injective_pr_bis f:
  function f -> (forall y, singl_val (fun x => related (graph f) x y)) ->
  injection f.
Proof. 
move=> ff prop;split => // x y xs ys Weq; apply: (prop (Vf f x) x y).
  by apply: (Vf_pr3 ff  xs).  
by rewrite Weq; apply: (Vf_pr3 ff ys). 
Qed.

Lemma surjective_pr0 f: surjection f -> Imf f = target f.
Proof.
move=> [ff sj]; apply: extensionality; first by apply:(fun_image_Starget ff).
move => t tf; move: (sj _ tf) => [x xsf <-].
apply/dirim_P; ex_tac; Wtac.
Qed.

Lemma surjective_pr1 f: function f -> Imf f = target f ->
  surjection f.
Proof.
move=> ff ift; split => // y; rewrite -ift. 
move/dirim_P=> [x pa pb];ex_tac; Wtac.
Qed.

Lemma surjective_pr f y:
  surjection f -> inc y (target f) ->
  exists2 x, inc x (source f) & related (graph f) x y .
Proof. 
move => [ff h] ytf; move: (h _ ytf) => [x xsf <-]; ex_tac.
rewrite /related; Wtac.
Qed.

Lemma surjective_pr3 f: surjection f -> range (graph f) = target f.
Proof. 
move => sf; rewrite -(surjective_pr0 sf) image_by_fun_source //; fct_tac.
Qed. 

Lemma surjective_pr4 f:
  function f -> range (graph f) = target f -> surjection f.
Proof. 
move=> ff rg; apply surjective_pr1 => //;rewrite image_by_fun_source //.
Qed. 

Lemma surjective_pr5 f:
  function f -> (forall y, inc y (target f) ->
  exists2 x, inc x (source f) & related (graph f) x y) -> surjection f.
Proof. 
move=> ff prop; split => // y yt; move: (prop _ yt) => [x xsf h]; ex_tac.
by symmetry; apply: Vf_pr.
Qed.

Lemma lf_injective f a b: lf_axiom f a b ->
  (forall u v, inc u a -> inc v a -> f u = f v -> u = v) ->
  injection (Lf f a b).
Proof. 
move=> ta prop; split; first by apply: lf_function. 
by aw; move=> x y xs ys/=; do 2 rewrite lf_V=>//; apply: prop. 
Qed.

Lemma lf_surjective f a b: lf_axiom f a b ->
  (forall y, inc y b -> exists2 x, inc x a & y = f x) -> 
  surjection (Lf f a b).
Proof.  
move=> ta prop; split; first by apply: lf_function.
by aw; move=> y yt; case: (prop _ yt)=> x xa fy; ex_tac; rewrite lf_V.
Qed.

Lemma lf_bijective f a b: lf_axiom f a b ->
  (forall u v, inc u a -> inc v a -> f u = f v -> u = v) ->
  (forall y, inc y b -> exists2 x, inc x a & y = f x) -> 
  bijection (Lf f a b).
Proof. 
by move => ta pi ps; split; [apply: lf_injective| apply:  lf_surjective].
Qed.

Lemma bijective_pr f y:
  bijection f -> inc y (target f) -> 
  exists! x, (inc x (source f) /\ Vf f x = y).
Proof. 
move=> [[_ inj] [_ sf]] yt; apply /unique_existence; split. 
  by move: (sf _ yt)=> [x p1 p2]; exists x.
by move=> x x' [xs Wx] [x's Wx']; rewrite -Wx' in Wx; apply: inj. 
Qed.

Lemma function_exten4 f g: source f = source g ->
  surjection f -> surjection g ->  {inc source f, f =1f g} ->
  f = g.
Proof.
move=> sfg sf sg Weq.
have ff: function f by fct_tac.
have fg: function g by fct_tac.
have geq: (graph f = graph g) by apply: fgraph_exten; fprops; aw.
apply: function_exten1=>//. 
by rewrite -(surjective_pr3 sf) -(surjective_pr3 sg) geq.
Qed.


(** Equipotent means there is a bijection between the sets *)

Definition bijection_prop f s t :=
  [/\ bijection f, source f = s & target f = t]. 
Definition surjection_prop f x y:=
  [/\ surjection f, source f = x & target f = y].
Definition injection_prop f x y:= 
  [/\ injection f, source f = x & target f = y].


Lemma identity_fb x: bijection (identity x).
Proof. by apply: lf_bijective => // y yx; exists y. Qed.

Lemma identity_bp x:  bijection_prop (identity x) x x.
Proof. by split; aw;apply: identity_fb. Qed.


(** Injectivity and surjectivity of identity and restriction *) 

Lemma restriction2_fi f x y:
  injection f -> restriction2_axioms f x y ->
  injection (restriction2 f x y).
Proof.
move=> [_ fi] ra.
have [pa pb pc] := (restriction2_prop ra). 
split => //; rewrite pb => a b ax bx.
by do 2 rewrite restriction2_V=>//; apply: fi; apply: (proj42 ra).
Qed.

Lemma restriction2_fs f x y:
  restriction2_axioms f x y ->
  source f = x -> Imf f = y ->
  surjection (restriction2 f x y).
Proof. 
move=> ra sf iy.
have [pa pb pc] := (restriction2_prop ra). 
split => // z; rewrite pb pc - {1} iy - {1} sf.
move /(Vf_image_P1 (proj41 ra))=>  [u usf uv].
ex_tac; rewrite restriction2_V //; ue.
Qed.

Lemma restriction1_fs f x:
  function f -> sub x (source f) ->
  surjection (restriction1 f x).
Proof. 
move=> ff sxs.
have [pa pb pc] := (restriction1_prop ff sxs).
split => //y; rewrite pb pc; move/(Vf_image_P ff sxs) => [b bx Jg].
by ex_tac; bw; rewrite restriction1_V.
Qed.

Lemma restriction1_fb f x:
  injection f -> sub x (source f) ->
  bijection (restriction1 f x).
Proof. 
move=> [ff fi] sxf; split; last by apply: restriction1_fs.
have [pa pb pc] :=(restriction1_prop ff sxf).
split => //; rewrite pb => a b ax bx.
by do 2 rewrite restriction1_V=>//; apply: fi; apply: sxf.
Qed.

Definition restriction_to_image f := 
  restriction2 f (source f) (Imf f).

Lemma restriction_to_image_axioms f: function f ->
  restriction2_axioms f (source f) (Imf f).
Proof. by move=> ff; split => //; apply :fun_image_Starget. Qed.

Lemma restriction_to_imageE f: function f -> 
  restriction_to_image f = restriction1 f (source f).
Proof. by move => ff; rewrite - restriction1_pr. Qed.

Lemma restriction_to_image_fs f: function f ->
  surjection (restriction_to_image f).
Proof. 
by move => h; rewrite (restriction_to_imageE h);apply: restriction1_fs.
Qed.

Lemma restriction_to_image_fb f: injection f ->
  bijection (restriction_to_image f).
Proof. 
by move => h; rewrite (restriction_to_imageE (proj1 h));apply: restriction1_fb.
Qed.

Lemma iim_fun_r f (h:=restriction_to_image f): function f -> 
   forall a, Vfs f a = Vfi (inverse_fun h) a.
Proof.
move => ff a.
have aux:=(proj1 (function_fgraph (proj1 (restriction_to_image_fs ff)))).
rewrite /Vfi/Vfs /inverse_image. 
rewrite corresp_g (igraph_involutive aux) corresp_g. 
congr (direct_image _ a); symmetry;apply/setI2id_Pl. 
exact:(proj2 (proj31 ff)). 
Qed.

(** Extension of a function by adding [f(x)=y] *)

Definition extension f x y:=
  triple ((source f) +s1 x) ((target f) +s1 y)  ((graph f) +s1 (J x y)).

Lemma extension_injective x f g a b:
  domain f = domain g -> ~ (inc x (domain f)) ->
  (f +s1 (J x a) = g +s1 (J x b)) -> f = g.
Proof. 
move=> seq nixsf sv.
set_extens t => tf.
  have: inc t (g +s1 J x b) by rewrite - sv; fprops.
  case /setU1_P => // ta;case: nixsf; apply /funI_P; ex_tac; rewrite ta;aw.
have: inc t (f +s1 J x a) by rewrite sv; fprops.
case /setU1_P => // ta.
case: nixsf; rewrite seq;apply /funI_P; ex_tac; rewrite ta;aw.
Qed.

Lemma restr_setU1 f x a:
  fgraph f -> ~ (inc x (domain f)) ->
  restr (f +s1 (J x a)) (domain f) = f.
Proof.
move=> fgf xdf; symmetry.
have aux: fgraph (f +s1 J x a) by apply:fgraph_setU1.
have sd:= (domain_S(@subsetU2l f (singleton (J x a)))).
apply: fgraph_exten; [done | by apply: restr_fgraph | bw | move=> t tdf /=; bw].
by rewrite setU1_V_in.
Qed.

Lemma setU1_restr f x E: fgraph f -> ~ (inc x E) ->
   domain f = E +s1 x->
   (restr f E) +s1 (J x (Vg f x)) = f.
Proof.
move=> fgf nxE df.
have sEd: sub E (domain f) by rewrite df; fprops.
have dr: (domain (restr f E)) = E by rewrite restr_d. 
have fgr: fgraph (restr f E) by fprops.
have nxe: ~ inc x (domain (restr f E)) by ue.
apply: fgraph_exten =>//.
    by apply: fgraph_setU1.
  by rewrite domain_setU1 dr df.
move=> u; rewrite domain_setU1 dr; case/setU1_P => uE.
  have ud: inc u (domain (restr f E)) by rewrite dr.
  by rewrite setU1_V_in // restr_ev.
by rewrite uE setU1_V_out.
Qed.

Section Extension.
Variables (f x y: Set).
Hypothesis (ff: function f) (xsf:  ~ (inc x (source f))).

Lemma extension_f: function (extension f x y).
Proof. 
rewrite /extension; apply: function_pr.
- apply: fgraph_setU1; fprops; aw.
- rewrite range_setU1 => t /setU1_P [] tr; apply/setU1_P;[left | by right].
  by apply:f_range_graph.
- by rewrite domain_setU1 - (proj33 ff).
Qed.

Lemma extension_Vf_in: {inc (source f), (extension f x y) =1f f}.
Proof.
move=> u uf; symmetry; apply: Vf_pr; first by apply:extension_f.
rewrite /extension; aw; apply: setU1_r;Wtac. 
Qed.

Lemma extension_Vf_out: Vf (extension f x y) x = y.
Proof. 
symmetry;apply: Vf_pr; first by apply:extension_f.
rewrite /extension; aw; apply: setU1_1.
Qed.

Lemma extension_fs: surjection f -> surjection (extension f x y).
Proof. 
move=> [_ sf].
split; first by apply:extension_f.
rewrite /extension; aw => z /setU1_P; case.
  move=> zt; move: (sf _ zt)=> [u us wu].
  by exists u; fprops; rewrite extension_Vf_in.
by move =>->; exists x; fprops; rewrite extension_Vf_out.
Qed.

Lemma extension_restr: 
  restriction2 (extension f x y) (source f) (target f) = f.
Proof.
have pa: restriction2_axioms (extension f x y) (source f) (target f).
  have ha: function (extension f x y) by apply: extension_f.
  have hb: sub (source f) (source (extension f x y)).
    by rewrite /extension; aw; fprops.
  split => //; rewrite /extension; aw; fprops.
  move => t /(Vf_image_P ha hb) [u usf ->]; rewrite (extension_Vf_in usf); Wtac.
move: (restriction2_prop pa) => [pb pc pd].
apply: function_exten => //; rewrite pc => t tx.
by rewrite (restriction2_V pa tx) (extension_Vf_in tx).
Qed.

End Extension.

Hint Resolve extension_f: fprops.

Lemma extension_f_injective x f g a b:
  function f -> function g -> target f = target g ->
  source f = source g -> ~ (inc x (source f)) ->
  (extension f x a = extension g x b) -> f = g.
Proof.
move=> ff fg teq seq nixsf sv. 
rewrite - (extension_restr a ff nixsf) sv seq teq extension_restr //; ue.
Qed.


(** Canonical injection of a set into a superset *) 
Definition canonical_injection a b :=
  triple a b (identity_g a).

Lemma canonical_injectionE a b: canonical_injection a b = Lf id a b.
Proof. done. Qed.

Lemma ci_fi a b: sub a b -> injection (canonical_injection a b).
Proof. by move => h; rewrite canonical_injectionE; apply:lf_injective. Qed.

Lemma ci_f a b: sub a b -> function  (canonical_injection a b).
Proof. move => h; exact (proj1 (ci_fi h)). Qed.
  
Hint Resolve ci_f : fprops.

Lemma ci_V a b x:
  sub a b -> inc x a -> Vf (canonical_injection a b) x = x.
Proof. 
by rewrite /Vf /canonical_injection=> ab xa; aw; apply: identity_ev.
Qed.

Lemma ci_range a b: sub a b ->
  range (graph (canonical_injection a b)) = a.
Proof. by rewrite /canonical_injection=> ab; aw; rewrite identity_r. 
Qed.


(** if [h] is constant [h = g \co f], where the target of [f] is a singleton *)
Lemma constant_function_pr2 x h:
  inc x (source h) -> constantfp h ->
  exists g f,
  [/\ g \coP f, h = g \co f, surjection f & singletonp (target f)].
Proof.
move=> xs [fh p]; set (y := Vf h x).
have ssyth: sub (singleton y) (target h) by apply:set1_sub; rewrite /y; fprops.
have ysy: inc y (singleton y) by fprops.
set (g:= canonical_injection (singleton y) (target h)); exists g.
set (f:= constant_function (source h) (singleton y) y); exists f.
have ff: function f by apply: constant_f.
have tf: target f = (singleton y) by rewrite constant_t.
have sf: source f = source h by rewrite constant_s.
have tg: target g = target h by rewrite /g /canonical_injection; aw.
have sg: source g = singleton y by rewrite /g /canonical_injection; aw.
have cop: g \coP f by rewrite /g;split; fprops; rewrite tf. 
split => //.
- apply: function_exten;aw; fprops; try fct_tac.
  by move=> z zh /=;aw;last (by ue);rewrite (p _ _ zh xs) /f constant_V // ci_V.
- split=>//; rewrite sf tf; move =>z /set1_P ->.
  by exists x; rewrite ?sf ?constant_V.
- by rewrite tf; exists y.
Qed.

(** Diagonal application, maps [x] to [J x x] *) 

Definition diagonal_application a :=
  Lf (fun x=> J x x) a (coarse a).

Lemma diag_app_V a x:
  inc x a -> Vf (diagonal_application a) x = J x x.
Proof. 
by rewrite /diagonal_application /coarse=> xa;aw; move=> y/=; fprops. 
Qed.

Lemma diag_app_fi a: injection (diagonal_application a).
Proof. 
rewrite /diagonal_application/coarse; apply: lf_injective. 
  by move=> y /=; fprops. 
by move => u v _ _; apply: pr1_def.
Qed.

Lemma diag_app_f a: function (diagonal_application a).
Proof. by case: (diag_app_fi a). Qed.

Lemma diag_app_range a:
  range (graph (diagonal_application a)) = diagonal a.
Proof. 
rewrite /diagonal_application.
set_extens t;rewrite /Lf corresp_g; aw.
  by move/Lg_range_P => [b ba ->]; apply/diagonal_pi_P.
move/diagonal_i_P => [pt ta pq]; apply/Lg_range_P; ex_tac. 
by rewrite {2} pq pt.
Qed.

(** Injectivity and surjectivity of P and Q *)

Lemma second_proj_fs g: surjection (second_proj g).
Proof.
split; first by apply: second_proj_f.
rewrite /second_proj /range/Lf /Vf; aw.
move => y /funI_P [z zg ->]; ex_tac; bw.
Qed.

Lemma first_proj_fs g: surjection (first_proj g).
Proof. 
split; first by apply: first_proj_f.
rewrite /first_proj /domain/Lf/Vf; aw.
move => y /funI_P [z zg ->]; ex_tac; bw.
Qed.

Lemma first_proj_fi g:
  sgraph g -> (injection (first_proj g) <-> functional_graph g).
Proof. 
move=> gg.
have fpf: (function (first_proj g)) by apply: first_proj_f.
have Ht: source (first_proj g) = g by rewrite/first_proj; aw.
rewrite /injection Ht.
split.
  move=> [_ hyp] a b b'; rewrite /related => i1 i2. 
  suff: (J a b = J a b') by apply: pr2_def.
  by apply: hyp=>//; do 2 rewrite first_proj_V=>//; aw.
move => H;split=>//; move=>x y xg yg/=; do 2 rewrite first_proj_V=>//.
by move/functionalP : (conj gg H) => [_]; apply.
Qed.

(** The function that maps [J x y] to [J y x] *) 

Lemma inv_graph_canon_fb g: sgraph g -> 
    bijection ( Lf (fun x=> J (Q x) (P x)) g (inverse_graph g)).
Proof.  
move => gg; apply: lf_bijective.
+ by move=> c cg /=; apply/igraph_pP; rewrite /related (gg _ cg).
+ move=> u v ug vg peq; apply: pair_exten; try apply: gg=>//.
    by apply: (pr2_def peq).
  by apply: (pr1_def peq).
+ by move=> y /igraphP [py pg]; ex_tac;aw; rewrite  py.
Qed.


(** Proposition 7 summarizes next two theorems. Let f be a function; then 
 f is a bijection if and only if its inverse is a function *)

Theorem bijective_inv_f f:
  bijection f -> function (inverse_fun f).
Proof. 
rewrite /inverse_fun; move => [fi fs].
have gf: (sgraph (graph f)) by move: fi=> [ff _]; fprops.
have fgf: fgraph (inverse_graph (graph f)).
  split; fprops; move=> x y/igraphP [px pf]/igraphP [qx qf] peq.
  apply: pair_exten =>//.
  by rewrite -peq in qf; apply: (injective_pr3 fi pf qf). 
apply: function_pr=>//.
  by rewrite igraph_range=>//; aw; fprops; fct_tac.
by symmetry; rewrite igraph_domain =>//; apply: surjective_pr3.
Qed.

Theorem inv_function_fb f:
  function f -> function (inverse_fun f) -> bijection f.
Proof. 
move=> ff fif.
split.
  apply: injective_pr_bis=> // x x' y.
  move/igraph_pP;rewrite -ifun_g => r1 ;move/igraph_pP; rewrite -ifun_g=> r2.
  by apply: (fgraph_pr (proj32 fif) r1 r2).
apply: surjective_pr4=> //; rewrite - igraph_domain; fprops. 
by rewrite -ifun_g /inverse_fun; aw.
Qed.

(** Properties of the inverse of a bijection *)

Lemma ifun_involutive:  {when function, involutive inverse_fun}.
Proof. move=> f ff;apply:icor_involutive; fct_tac. Qed.

Lemma inverse_bij_fb f: bijection f -> bijection (inverse_fun f).
Proof. 
move=> bf;move: (bijective_inv_f bf)=> bif.
have ff:function f by fct_tac.
apply: inv_function_fb => //; rewrite ifun_involutive //.
Qed.

Lemma inverse_V f x:
  bijection f -> inc x (target f) ->
  Vf f (Vf (inverse_fun f) x) = x.
Proof. 
move=> bf xt; move:(bij_surj bf xt) => [y ys xv]; rewrite -{2} xv.
move:(bijective_inv_f bf)=> bif.
congr Vf; symmetry; apply:(Vf_pr bif).
rewrite ifun_g -xv; apply/igraph_pP; Wtac; fct_tac.
Qed.

Lemma inverse_V2 f y:
  bijection f -> inc y (source f) ->
  Vf (inverse_fun f) (Vf f y) = y.
Proof.
move=> bf ys.
have yt: inc y (target (inverse_fun f)) by aw.
move: (inverse_V (inverse_bij_fb bf) yt).
by rewrite (ifun_involutive (proj1 (proj1 bf))).
Qed.

Lemma inverse_Vis f x:
  bijection f -> inc x (target f) -> inc (Vf (inverse_fun f) x) (source f).
Proof.
move=> bf xt.
have -> : source f=  (target (inverse_fun f)) by aw.
apply: Vf_target; aw; apply: (proj1(proj1(inverse_bij_fb bf))).
Qed.

Lemma composable_f_inv f: bijection f -> f \coP (inverse_fun f).
Proof.
move=> bf; have fif:=(bijective_inv_f bf).
split;[fct_tac | done | aw].
Qed.

Lemma composable_inv_f f: bijection f ->  (inverse_fun f) \coP f.
Proof.
move=> bf; have fif:=(bijective_inv_f bf).
split; [ done | fct_tac | aw].
Qed.

Lemma bij_right_inverse f:
  bijection f ->  f \co (inverse_fun f) = identity (target f).
Proof. 
move=> bf.
have ff: function f by fct_tac.
move:(bijective_inv_f bf)(composable_f_inv bf) => iff cop.
apply: function_exten; fprops; aw; first by fct_tac; aw.
by move => a atf /=; aw; bw; apply:inverse_V.
Qed.

Lemma bij_left_inverse f:
  bijection f -> (inverse_fun f) \co f = identity (source f).
Proof.
move=> bf.
have ff: function f by fct_tac.
move:(bijective_inv_f bf)(composable_inv_f bf) => iff cop.
apply: function_exten; fprops; aw; first by fct_tac; aw.
by move => a atf /=; aw; bw; apply:inverse_V2.
Qed.

Lemma compf_lK f g : bijection g -> g \coP f ->
    (inverse_fun g) \co (g \co f) = f.
Proof.
move => bg cop.
have co1 := (composable_inv_f bg).
rewrite (compfA co1 cop) (bij_left_inverse bg).
by move: cop => [s1 s2 ->]; rewrite (compf_id_l s2).
Qed.

Lemma compf_rK f g : bijection g -> f \coP g ->
     (f \co g) \co (inverse_fun g) = f.
Proof.
move => bg cop.
move: (composable_f_inv bg) => co1.
rewrite -(compfA cop co1) (bij_right_inverse bg).
by move: cop  => [s1 s2 s3]; rewrite - s3 (compf_id_r s1).
Qed.

Lemma compf_regl f f' g : bijection g ->
    f \coP g -> f' \coP g -> f \co g = f' \co g -> f = f'.
Proof.
move => bg pa pb pc.
by rewrite - (compf_rK bg pa) - (compf_rK bg pb) pc.
Qed.

Lemma compf_regr f f' g : bijection g ->
    g \coP f -> g \coP f' -> g \co f = g \co f' -> f = f'.
Proof.
move => bg pa pb pc.
by rewrite - (compf_lK bg pa) - (compf_lK bg pb) pc.
Qed.

Lemma bijection_inverse_aux g h: bijection g -> composable g h ->
  g \co h = identity (source h) -> inverse_fun g = h.
Proof.
move => ha hb.
move: (hb) => [fg fh sgth] w.
have hd:= (composable_inv_f ha).
have ra:=(proj31(bijective_inv_f ha)).
move /(f_equal target): (w); aw; move => tgsh.
have sh: (source h) = source (inverse_fun g) by aw.
move/(f_equal (compose (inverse_fun g))): w.
rewrite sh (compf_id_right ra) (compfA hd hb) (bij_left_inverse ha).
by rewrite sgth (compf_id_left (proj31 fh)).
Qed.



(** Properties of direct and inverse images *)

Lemma sub_inv_im_source f y:
  function f -> sub y (target f) -> 
  sub (Vfi f y) (source f).
Proof. by move=> ff yt t /iim_graph_P [u uy Jg]; Wtac. Qed.

Lemma direct_inv_im f y:
  function f ->  sub y (target f) -> 
  sub (Vfs f (Vfs (inverse_fun f) y)) y.
Proof.
move=> ff yt x. 
have aux: sub (Vfs (inverse_fun f) y) (source f). 
  by rewrite /inverse_fun/Vfs; aw; apply: sub_inv_im_source.
move/(Vf_image_P ff aux) =>[u /dirim_P  [z zy /igraph_pP]].
by rewrite - ifun_g (ifun_involutive ff) => xx ->; rewrite -(Vf_pr ff xx).
Qed.

Lemma nonempty_image f x:
  function f -> nonempty x -> sub x (source f) ->
  nonempty (Vfs f x).
Proof.
move=> ff [z zx] xf; exists (Vf f z); apply/dirim_P; ex_tac; Wtac. 
Qed.

Lemma direct_inv_im_surjective f y:
  surjection f -> sub y (target f) -> 
  Vfs f (Vfs (inverse_fun f) y) = y. 
Proof.
move=> [ff sf] yt.
apply: extensionality; first by apply: direct_inv_im. 
move=> x xs; rewrite -iim_fun_pr.
apply/Vf_image_P =>//; first by apply: sub_inv_im_source. 
have [u us Jg] := (sf _ (yt _ xs)). 
exists u=>//;apply/iim_fun_P; ex_tac;rewrite - Jg; Wtac.
Qed.

Lemma inverse_direct_image  f x:
  function f -> sub x (source f) ->
  sub x (Vfs (inverse_fun f) (Vfs f x)).
Proof.
move=> ff sxf t tx.
apply/dirim_P; exists (Vf f t). 
  by apply/Vf_image_P => //; ex_tac.
rewrite ifun_g; apply/igraph_pP; Wtac.
Qed.

Lemma inverse_direct_image_inj f x:
  injection f -> sub x (source f) ->
  Vfs (inverse_fun f) (Vfs f x) = x.
Proof.
move=> [ff fi] xsf. 
apply: extensionality; last by apply: inverse_direct_image.
rewrite -iim_fun_pr => y /iim_graph_P [u ui Jg].
move /(Vf_image_P ff xsf): ui => [v vx]; rewrite (Vf_pr ff Jg) => Vv.
by rewrite - (fi _ _  (xsf _ vx) (p1graph_source ff Jg) (sym_eq Vv)).
Qed.


(** ** EII-3-8 Retractions and sections *)

(** Definition of left and right inverse *)

Definition is_left_inverse f r:=
  r \coP f /\ r \co f = identity (source f).

Definition is_right_inverse f s:=
  f \coP s /\ f \co s = identity (target f).


Lemma left_i_target f r: is_left_inverse f r ->  target r = source f.
Proof. by move=> [_ /(congr1 target)]; aw. Qed.

Lemma left_i_source f r: is_left_inverse f r ->  source r = target f.
Proof. by move=> [[_ [_ c] _]]. Qed.

Lemma right_i_source f s:  is_right_inverse f s ->  source s = target f.
Proof. by move=> [_ /(congr1 source)]; aw. Qed.

Lemma right_i_target f s: is_right_inverse f s ->  target s = source f.
Proof. by move=> [[_ [_ c] _]]. Qed.

Lemma right_i_V f s x:
  is_right_inverse f s -> inc x (target f) -> Vf f (Vf s x) = x.
Proof. 
move=> rsf xtf; move: (xtf);rewrite - (right_i_source rsf).
move: rsf=> [csf c] xs;rewrite - compf_V // c; bw.
Qed.

Lemma left_i_V f r x:
  is_left_inverse f r -> inc x (source f) -> Vf r (Vf f x) = x.
Proof. move=> [ltf c] xsf; rewrite- compf_V // c; bw. Qed.


(** Proposition 8 concerns the next 4 theorems; it is the link between
 injectivity, surjectivity and existence of left and right inverse *)

Theorem inj_if_exists_left_inv f:
  (exists r, is_left_inverse f r) -> injection f.
Proof.
move=> [r lrf]; split; first by move: lrf => [ cp _ ]; fct_tac.
move=> x y xs ys sv.
by rewrite  - (left_i_V lrf xs) - (left_i_V lrf ys) sv. 
Qed.

Theorem surj_if_exists_right_inv f:
  (exists s, is_right_inverse f s) -> surjection f.
Proof. 
move=> [s rsf]; move: (rsf) => [cp _]; move: (cp) =>[ff fs ss].
split => // y yt; exists (Vf s y).
  rewrite -(right_i_source rsf) in yt; rewrite ss; fprops.
by rewrite (right_i_V rsf yt). 
Qed.

(** Existence of left and right inverse for Bourbaki functions *)

Theorem exists_left_inv_from_inj f:
  injection f -> nonempty (source f) -> exists r, is_left_inverse f r.
Proof. 
move=> fi [a asf]; move: (inj_function fi) => ff.
pose p x y := x = Vf f y.
pose gx x := (select (p x) (source f)).
have hc x:  inc x (Imf f) -> p x (gx x) /\ inc (gx x) (source f). 
  move => xI; apply: select_pr; first by move/(Vf_image_P1 ff): xI.
  rewrite /p; move => i j /=  isf e1 jsf e2;apply: (proj2 fi i j isf jsf).
  by rewrite - e1 e2.
pose g x := Yo (inc x (Imf f)) (gx x) a.
have ax: lf_axiom g (target f) (source f).
  rewrite /g => t tt; Ytac h => //; exact:(proj2 (hc _ h)).  
have ha: Lf g (target f) (source f) \coP f.
  by split; aw; apply:lf_function. 
exists (Lf g (target f) (source f)).
split => //; apply: function_exten; aw; fprops; first by fct_tac.
move => y ys /=.
have yi:inc (Vf f y) (Imf f) by  apply/(Vf_image_P1 ff); ex_tac.
have ft: inc (Vf f y) (target f) by Wtac.
move: (hc _ yi) => [hu hv]; move:(proj2 fi _ _ ys hv hu) => yv.
by aw; bw; rewrite /g; Ytac0.
Qed.

Theorem exists_right_inv_from_surj f:
  surjection  f -> exists s, is_right_inverse f s.
Proof. 
move=> [ff sf].
pose p y x := inc x (source f) /\ Vf f x = y.
have ha y: inc y (target f) -> p y (choose (p y)).
  by move => /sf [x xa xb]; apply: choose_pr; exists x.
have ax: lf_axiom (fun y => choose (p y)) (target f) (source f).
  by move => y /ha; case.
have hb: f \coP Lf (fun y : Set => choose (p y)) (target f) (source f).
   by split; aw; apply: lf_function.
exists (Lf (fun y => choose (p y)) (target f) (source f)).
split => //;apply:function_exten; aw; fprops; first by fct_tac.
move => y yt /=; aw; bw. exact:proj2 (ha _ yt).
Qed.

(** If compositions in both order are the identity, then the functions are bijections *)

Lemma bijective_from_compose g f:
  g \coP f -> f \coP g -> g \co f = identity (source f) ->
  f \co g = identity (source g)  ->
  [/\ bijection f, bijection g & g = inverse_fun f].
Proof. 
move=> cgf cfg cgfi cfgi.
move: (cfg) (cgf)=> [ff fg seq] [_ _ teq].
have injf: injection f by apply: inj_if_exists_left_inv; exists g. 
have injg: injection g by apply: inj_if_exists_left_inv; exists f. 
have bf: (bijection f).
  by split =>//; apply: surj_if_exists_right_inv; exists g; hnf; rewrite -teq.
split=>//.
  by split=>//; apply: surj_if_exists_right_inv; exists f; hnf; rewrite - seq.
have fif:= (bijective_inv_f bf).
apply: function_exten=>//; aw; first by ue.
move=> x xs.
have {2} -> : (x = Vf f (Vf g x)).
  by rewrite - compf_V=>//;rewrite cfgi identity_V =>//.
rewrite (inverse_V2 bf) // seq; Wtac.
Qed.

(** More links between left inverse and right inverse *)

Lemma right_inverse_from_left f r:
  is_left_inverse f r -> is_right_inverse r f.
Proof. by move=> [c e];hnf; rewrite (left_i_target (conj c e)). Qed.

Lemma left_inverse_from_right f s:
  is_right_inverse f s -> is_left_inverse s f.
Proof. by move=> [c e]; hnf; rewrite (right_i_source (conj c e)). Qed.

Lemma left_inverse_fs f r:
  is_left_inverse f r -> surjection r.
Proof.
move=> lrf; apply: surj_if_exists_right_inv. 
by exists f; apply: right_inverse_from_left.
Qed.

Lemma right_inverse_fi f s:
  is_right_inverse f s -> injection s.
Proof. 
move=> lrf; apply: inj_if_exists_left_inv. 
by exists f; apply: left_inverse_from_right.
Qed.

Lemma section_unique f:
  {when (is_right_inverse f) &, injective (fun s => range (graph s)) }.
Proof. 
move=> s s' rsf rs'f rg.
move: (proj32_1 rsf)(proj32_1 rs'f) => fs fs'.
move: (right_i_source rsf) (right_i_source rs'f) => ss ss'.
apply: function_exten =>//.
    by rewrite  (right_i_source rsf).
  by rewrite  (right_i_target rsf)  (right_i_target rs'f).
move=> x xs.
have: (inc (Vf s x) (range (graph s))) by apply /range_fP=>//; exists x. 
move: xs;rewrite rg ss => xs /(range_fP fs') [y]; rewrite ss' => ys ww.
move: (f_equal (fun z => Vf f z) ww).
by rewrite(right_i_V rs'f ys)  (right_i_V rsf xs) ww => ->.
Qed.

(** Theorem one is next 14 lemmas. It studies left and right invertibility 
of one of f g and the composition of f and g, given properties of the 
other objects. *)


Theorem compose_fi f f':
  injection f -> injection f' -> f' \coP f -> injection (f' \co f).
Proof. 
move=> [_ fi] [_ fi'] c; split; first by  fct_tac.
aw => x y xs ys; aw=>p; apply: (fi _ _ xs ys).
move:c => [_ ff c]; apply: fi'  => //; rewrite c; fprops.
Qed.

Lemma inj_compose1 f f':
  injection f -> injection f' -> source f' = target f ->
  injection (f' \co f).
Proof. 
move=> injf injf' sff';apply: compose_fi=> //;split => //; fct_tac. 
Qed.

Theorem compose_fs f f':
  surjection f -> surjection f' -> f' \coP f -> surjection (f' \co f).
Proof. 
move=> [_ sf] [_ sf'] c; split; [fct_tac | aw => y yt].
move: (sf' _ yt) => [x xs <-].
have xt: inc x (target f) by rewrite - (proj33 c).
move: (sf _ xt) => [z zs <-]; ex_tac;aw.
Qed.

Lemma compose_fb f f':
  bijection f -> bijection f' -> f' \coP f -> bijection (f' \co f).
Proof. 
by move=> [inf sf] [inf' sf']; split ; [apply: compose_fi | apply: compose_fs].
Qed.

Lemma right_compose_fb f f':
  f' \coP f -> bijection (f' \co f) -> bijection f' -> bijection f.
Proof. 
move=> c bc bf; move: (inverse_bij_fb bf) => bf'.
rewrite - (compf_lK bf c); apply: compose_fb => //; split; aw; fct_tac.
Qed.

Lemma left_compose_fb f f':
  f' \coP f -> bijection (f' \co f) -> bijection f -> bijection f'.
Proof. 
move=> cff bc bf; move: (inverse_bij_fb bf) => bf'.
rewrite - (compf_rK bf cff); apply: compose_fb => //; split; aw; fct_tac.
Qed.

Lemma left_inverse_composable f f' r r': f' \coP f ->
  is_left_inverse f' r' -> is_left_inverse f r -> r \coP r'.
Proof.
move=> [_ _ c] li1 [[fr _ r1] _].
move: (left_i_target li1)=> r2.
move: li1=> [[fr' _] _ _].
by split => //; rewrite r1 - c r2.
Qed.

Lemma right_inverse_composable f f' s s': f' \coP f ->
  is_right_inverse f' s' -> is_right_inverse f s -> s \coP s'.
Proof. 
move=> [_ _ c]  [[_ fs r1] _] ri1.
move: (ri1)=> [[_ fs' _] _].
by  split => //; rewrite (right_i_source ri1) -c. 
Qed.

Theorem left_inverse_compose f f' r r': f' \coP  f ->
  is_left_inverse f' r' -> is_left_inverse f r ->
  is_left_inverse (f' \co f) (r \co r') .
Proof.
move=> c1 li1 li2.
have cc:= left_inverse_composable c1 li1 li2.
have tr'sr':= left_i_target li1.
have sf'sr: (source f' = source r) by rewrite (proj33 cc).
have sr'tf':= left_i_source li1.
have [crf' crfi'] := li1.
have [crf crfi] := li2.
split.
  by split; [ fct_tac | fct_tac | aw;rewrite sr'tf'].
have crrf: (r \co r') \coP f' by split; [ fct_tac | fct_tac| aw ].
rewrite compfA //- (@compfA r r' f') //. 
rewrite crfi' sf'sr compf_id_r ?crfi; aw; fct_tac.
Qed.

Theorem right_inverse_compose f f' s s': f' \coP f ->
  is_right_inverse f' s' -> is_right_inverse f s ->
  is_right_inverse (f' \co f) (s \co s').
Proof.
move=> cf'f ri1 ri2.
have css':= (right_inverse_composable cf'f ri1 ri2).
have sstf:= (right_i_source ri2).
have tssf:=(right_i_target ri2).
have sf'sr: (target f = target s') by rewrite - (proj33 css').
have [cfs' cfsi'] := ri1.
have [cfs cfsi] := ri2.
split.
  by split; [ fct_tac |  fct_tac | aw;rewrite -tssf].
have crrf: f \coP (s \co s') by split; [ fct_tac | fct_tac| aw ].
rewrite - compfA=>//; rewrite (@compfA f s s')=>//. 
by aw; rewrite cfsi sf'sr compf_id_l=>//; fct_tac.
Qed.

Theorem right_compose_fi f f':
  f' \coP f -> injection (f' \co f) -> injection f.
Proof. 
move=> cff [fc ic]; split; first by fct_tac.
by move: ic; aw; move=> ic x y xs ys eql; apply: ic=>//; aw; rewrite eql.
Qed.

Theorem left_compose_fs f f':
  f' \coP f -> surjection (f' \co f) -> surjection f'.
Proof. 
move=> cff sc; split; first by fct_tac.
have: (target f' = target (f' \co f)) by aw.
move=> -> y yt; move: ((proj2 sc) _  yt)=> [x xs <-].
rewrite compf_s in xs; exists (Vf f x); aw.
move:cff=> [_ ff ->]; fprops. 
Qed.

Theorem left_compose_fs2 f f':
  f' \coP f-> surjection (f' \co f) -> injection f' -> surjection f.
Proof. 
move=> cff sc [_ fi].
have  [ff ff' eq] := cff.
split; first by fct_tac.
rewrite - eq=>y ytf.
have ytc: (inc (Vf f' y) (target (f' \co f))) by aw; fprops.
move: ((proj2 sc) _  ytc)=> [x]; rewrite compf_s => xs; aw => wxt.
by exists x => //; apply: fi=>//;  rewrite eq; fprops.
Qed.

Theorem left_compose_fi2 f f':
  f' \coP f -> injection (f' \co f) -> surjection f -> injection f'.
Proof. 
move=>  cff [_ ic] sf.
split; first by fct_tac.
rewrite (proj33 cff) => x y xs ys.
have [x' x's e1] := ((proj2 sf) _  xs).
have [y' y's e2] :=((proj2 sf) _  ys).
rewrite compf_s in ic; move: (ic _ _ x's y's); aw;  rewrite -e1 -e2. 
by move=> e3 e4; rewrite (e3 e4).
Qed.

Theorem left_inv_compose_rf f f' r'':
  f' \coP f -> is_left_inverse (f' \co f) r'' -> 
  is_left_inverse f (r'' \co f').
Proof.
move=> cff [[ aa bb]]; aw; move => crffi cc.
have [ff' ff seq]: f' \coP f by [].
have crf: r'' \coP  f' by hnf.
split; [split; aw; fct_tac | by rewrite - compfA ].
Qed.

Theorem right_inv_compose_rf f f' s'':
  f' \coP f -> is_right_inverse  (f' \co f) s'' -> 
  is_right_inverse f' (f \co s'').
Proof. 
move=> cff [[ fc fs]]; aw => cffsi cc. 
have [ff' ff seq]: (f' \coP f) by [].
have cfs: f \coP s'' by  hnf.
by split; [split; aw; fct_tac | rewrite compfA ].
Qed.

Theorem left_inv_compose_rf2 f f' r'':
  f' \coP f -> is_left_inverse (f' \co f) r'' -> surjection f ->
  is_left_inverse f' (f \co r'').
Proof. 
move=> cff lic sf.
have bf: (bijection f). 
  split=>//.
  have: (injection (f' \co f)) by apply: inj_if_exists_left_inv; exists r''. 
  by apply: (right_compose_fi cff).
move: (left_i_target lic); aw=> trsf; move:lic=> [crrf]; aw=> crrfi.
have cfr: f \coP r'' by  hnf;split; try fct_tac; symmetry.
have fcfr:(function  (f \co r'')) by fct_tac.
split; first by hnf; split;  try fct_tac; move: crrf=> [_  _]; aw.
set (invf:= inverse_fun f).
have sfti: (source f = target invf) by rewrite /invf; aw. 
have fi:(function invf) by  apply: bijective_inv_f.
have cffi: (f' \co f) \coP invf by hnf; aw; split; try fct_tac. 
have co3: r'' \coP ((f' \co f) \co inverse_fun f).
    hnf; split;try fct_tac;move: crrf=> [_ _]; aw.
have co4: r'' \coP f' by hnf; split; try fct_tac;move: crrf=> [_ _]; aw.
rewrite - (compfA cfr co4) -{1} (compf_rK bf cff) (compfA crrf cffi). 
by rewrite crrfi sfti compf_id_l // /invf (proj33 cff) bij_right_inverse. 
Qed.

Theorem right_inv_compose_rf2 f f' s'':
  f' \coP f -> is_right_inverse (f' \co f) s'' -> injection f' ->
  is_right_inverse f (s'' \co f').
Proof. 
move=> cff risc fi.
have sc: (surjection (f' \co f)) by apply:surj_if_exists_right_inv; exists s''.
have bf': (bijection f') by split=>//; apply: (left_compose_fs cff sc).  
move: (right_i_source risc); aw=> sstf.
move: risc=> []; aw => cffs cffsi.
have csf: (s'' \coP f') by hnf; split;  try fct_tac. 
have fcsf: function (s'' \co f') by fct_tac.
have cfc: f \coP (s'' \co f') by hnf; split; try fct_tac; move:cffs=> [_ _]; aw.
have bif:= (bijective_inv_f bf').
have sf'tf: source f' = target f by move: cff=> [_ _].
set (invf:= inverse_fun f').
have cic: composable invf (f' \co f) by split; try fct_tac; rewrite/invf; aw.
have cffsf: (f' \co f) \coP (s'' \co f').
  hnf; split;[ fct_tac |  done | by move:cfc=> [_ _]; aw ].
have ff: function f' by fct_tac.
split=>//.
rewrite - {1} (compf_lK bf' cff) - compfA // (compfA cffs csf).
by rewrite  cffsi compf_id_l // (bij_left_inverse bf') sf'tf.
Qed.


(** Proposition 9  is the next 6 lemmas (each in 2 variants). Given f and g, 
when does there exists h such that the composition with f (in any order) is g *)

Theorem exists_left_composable f g:
  function f -> surjection g -> source f = source g ->
  ((exists h, h \coP g /\ h \co g = f) 
   <->  (forall x y, inc x (source g) -> inc y (source g) -> 
       Vf g x = Vf g y -> Vf f x = Vf f y)).
Proof. 
move=> ff sg sfsg; split.
  by move=> [h [chg]] <- x y xs ys; aw => ->.
move:(exists_right_inv_from_surj sg) => [h [ha hb]] hc.
move: ha => [fg fh sgth].
have ra: f \coP h by split => //; rewrite sfsg. 
have rb: function (f \co h) by apply:compf_f.
have rc: source h = target g by move: (f_equal source hb); aw.
have rd: (f \co h) \coP g by split; aw.
have re: g \coP h by split.
exists (f \co h); split => //.
symmetry; apply: function_exten; aw; first by apply:compf_f.
move => x xsf /=.
have xsg: inc x (source g) by ue.
have gxsh: inc (Vf g x) (source h) by rewrite rc; Wtac.
have hgxsg: inc (Vf h (Vf g x)) (source g) by rewrite  sgth; Wtac.
aw;apply: (hc _ _ xsg hgxsg).
move: (f_equal (Vf ^~ (Vf g x)) hb); bw; aw => //; Wtac.
Qed.

Theorem exists_left_composable_aux f g s h:
  function f -> source f = source g ->
  is_right_inverse g s ->
  h \coP g -> h \co g = f -> h = f \co s.
Proof. 
move=> gg sfsg [csg cshi] chg <-. 
have shtg:(source h= target g) by move: chg=> [_ _].
by rewrite - compfA // cshi - shtg compf_id_r //; fct_tac. 
Qed.

Theorem exists_unique_left_composable f g h h':
  function f -> surjection g -> source f = source g ->
  h \coP g -> h' \coP g -> 
  h \co g = f ->  h' \co g = f -> h = h'.
Proof.
move=> ff sg sfsg chg chg' chgf  chgf'.
move:(exists_right_inv_from_surj sg)=> [j jp].
rewrite (exists_left_composable_aux ff sfsg jp chg chgf).
by rewrite (exists_left_composable_aux ff sfsg jp chg' chgf').
Qed.


Theorem left_composable_value f g s h:
  function f -> surjection g -> source f = source g ->
  (forall x y, inc x (source g) -> inc y (source g) -> 
    Vf g x = Vf g y -> Vf f x = Vf f y) ->
  is_right_inverse g s  ->  h =  f \co s -> h \co g = f.
Proof. 
move=> ff sg sfsg hyp rish ->.
have sstg:= (right_i_source rish).
have [cgs cgsi] := rish.
have cfs: f \coP s by hnf; split; [done |fct_tac | move:cgs => [_ _] <-].
have cfsg: (f \co s) \coP g by hnf; split;aw;fct_tac.
apply: function_exten; aw;[ fct_tac | by symmetry  |].
move=> x xg.
have Ws: (inc (Vf g x) (source s)) by rewrite sstg;Wtac;fct_tac.
have WWs: inc (Vf s (Vf g x)) (source g).
    move:cgs => [_ _ ->]; Wtac; fct_tac.
by aw; apply: hyp =>//; rewrite -compf_V // cgsi; bw; rewrite - sstg. 
Qed.

Theorem exists_right_composable_aux f g h r:
  function f ->  target f = target g ->
  is_left_inverse g r  -> g \coP h -> g \co h = f ->
  h = r \co f.
Proof.
move=> ff tftg [crg crgi] chg <-; rewrite compfA // crgi.
by move:chg=> [_ fh ->];rewrite compf_id_l. 
Qed.


Theorem exists_right_composable_unique f g h h':
  function f -> injection g -> target f = target g ->
  g \coP h ->  g \coP h' -> 
  g \co h = f -> g \co h' = f -> h = h'.
Proof.
move=> ff [_ ig] tftg cgh cgh' cghf cghf'.
move: (cgh)(cgh') => [p1 p2 p3] [_ p5 p6].
rewrite -cghf' in cghf.
have shh': source h = source h' by rewrite -(compf_s h g) -(compf_s h' g) cghf.
apply: function_exten => //; [ ue | move=> x xsh;apply: ig ].
+ by rewrite p3; Wtac.
+ rewrite p6; Wtac; ue.
+ move: (f_equal (Vf ^~  x) cghf);  aw; ue.
Qed.

Theorem exists_right_composable f g:
  function f -> injection g -> target f = target g ->
  ((exists h, g \coP h /\ g \co h = f) <->
  (sub (range (graph f)) (range (graph g)))).
Proof. 
move=> ff ig tftg.
have fg: function g by fct_tac.
split.
  move => [h [chg cghf]] x /(range_fP ff) [u usf ->]; apply/(range_fP fg).
  have [_ fh th] := chg.
  move: usf; rewrite - cghf compf_s => usg; aw.
  exists (Vf h u) => //;rewrite th; Wtac.
case: (emptyset_dichot (source g)).
  case: (emptyset_dichot (source f)). 
    move=> ssfe sge _.
    move: empty_function_function => [qa qb qc].
    have cge: (g \coP empty_function) by split => //; rewrite qc.
    exists (empty_function); split=>//; symmetry.
    apply: function_exten=>//; aw;try fct_tac; rewrite ssfe ?qb //.
    move => x /in_set0 //.
  have [_  fgf ->] := ff.
  move=> [x xsf] sge hyp. 
  move: (hyp _ (inc_V_range fgf xsf)); move/(range_fP fg) => [u].
  by rewrite sge => /in_set0. 
move=> nesg hyp.
have [r rli]:= (exists_left_inv_from_inj ig nesg).
have trsg:= (left_i_target rli).
have [crg crgi] := rli.
have crf: (r \coP f).
   by hnf; split => //; first (by fct_tac); move: crg=> [_ _ ->]; symmetry.
have fcrf: (function (r \co f)) by fct_tac.
have cgrf: (g \coP (r \co f)) by hnf; aw. 
exists (r \co f); split=>//.
symmetry;apply: function_exten; try fct_tac; aw.
move=> x xsf /=; aw.
have aux: (sgraph (graph f)) by fprops.
move: xsf; rewrite -(f_domain_graph ff). 
move/(domainP aux)=> [y Jg]; rewrite - (Vf_pr ff Jg).
have: (inc y (range (graph g))) by apply: hyp; apply/(rangeP aux); ex_tac.
move/(range_fP fg) => [z zs ->].
have: (Vf (r \co g) z = z) by rewrite crgi; bw.
by aw; move => ->.
Qed.


Theorem right_composable_value f g r h:
  function f -> injection g -> target g = target f ->
  is_left_inverse g r ->
  (sub (range (graph f)) (range (graph g))) ->
  h = r \co f -> g \co h = f.
Proof. 
move=> ff ig tgtf lirg hyp ->.
have trsg :=(left_i_target lirg).
have [crg crgi] := lirg.
have srtg:=(proj33 crg).
have crf: (r \coP f)  by split=> //; try fct_tac; rewrite srtg.  
have cgrf: g \coP (r \co f)  by split; try fct_tac; symmetry; aw. 
have cgr: (g \coP r) by split => //; fct_tac. 
apply: function_exten; aw; try fct_tac. 
move=> x xf /=; aw.
have: (inc (Vf f x) (range (graph g))).
  by apply: hyp; apply/(range_fP ff); exists x.
move/(range_fP (proj1 ig))=> [y ys ->].
by move: (f_equal (fun z=> (Vf z y)) crgi); aw; bw => ->.
Qed.

(** Equipotent *)

Definition equipotent x y := 
  exists z, bijection_prop z x y.

Notation "x \Eq y" := (equipotent x y) (at level 50).

Lemma equipotent_aux f a b:
  bijection (Lf f a b) -> a \Eq b.
Proof. by move => h; exists (Lf f a b); rewrite /bijection_prop; aw; split. Qed.

Lemma EqR: reflexive_r equipotent.
Proof. move => x; exists (identity x); apply: identity_bp. Qed.

Hint Resolve EqR: fprops.

Lemma EqT: transitive_r equipotent.
Proof. 
move => c b a [f [bf sf tf]] [g [bg sg tg]]; exists (g \co f).
by split; aw; apply: compose_fb => //; split => //; try fct_tac; rewrite tf.
Qed.

Lemma EqS: symmetric_r equipotent.
Proof.
move => a b [f [bf sf tf]]; exists (inverse_fun f).
by  split; aw; apply:inverse_bij_fb. 
Qed.


Lemma Eq_restriction1 f x:
  sub x (source f) -> injection f ->
  x \Eq (Vfs f x).
Proof. 
move=> wsf bf; have h:=(restriction1_fb bf wsf). 
exists (restriction1 f x); split => //; rewrite/restriction1; aw.
Qed.

Lemma Eq_src_range f: injection f -> 
  (source f) \Eq (range (graph f)).
Proof. 
move=> injf; rewrite -image_by_fun_source; last by fct_tac.
apply: Eq_restriction1; fprops.
Qed.


Lemma equipotent_product_sym a b:
  (a \times b) \Eq (b \times a).
Proof.
have pa: sgraph (a \times b) by fprops.
move: (inv_graph_canon_fb pa); aw; apply: equipotent_aux.
Qed.

Lemma Eq_indexed a b:  a \Eq (a *s1 b).
Proof.
rewrite /indexed.
apply: (@equipotent_aux (fun x=> J x b)); apply: lf_bijective.
- by move=> x xa /=; aw; fprops. 
- by move=> u v _ _; apply: pr1_def.
- move=> y /setX_P [py pya /set1_P <-]; ex_tac; aw.
Qed.

Lemma Eq_indexed2 a b: (a *s1 b) \Eq a.
Proof. apply:EqS; apply: Eq_indexed. Qed.

Lemma Eq_indexed3 a b c: (a *s1 b) \Eq (a *s1 c).
Proof. apply: (EqT (Eq_indexed2 a b) (Eq_indexed a c)). Qed.

Lemma Eq_rindexed a b: a \Eq (indexedr b a).
Proof.
apply: (EqT (Eq_indexed a b)); apply: equipotent_product_sym.
Qed.

Lemma Eq_src_graph f: function f -> (source f) \Eq (graph f).  
Proof.
move=> ff.
apply: (@equipotent_aux (fun z => J z (Vf f z))); apply: lf_bijective.
- move=> z jz /=;Wtac.
- move=> u v _ _ aux; exact: (pr1_def aux).
- move=> y yG; move: (p1graph_source1 ff yG) => pa; ex_tac.
  apply: in_graph_V => //; fprops.
Qed.

Lemma Eq_domain f: fgraph f -> domain f \Eq f.
Proof.
move => h.
apply:(@equipotent_aux (fun z => J z (Vg f z))); apply: lf_bijective.
+ by apply: fdomain_pr1.
+ by move => u v _ _ /pr1_def.
+ by move => y yf; rewrite (in_graph_V h yf); exists (P y); fprops.
Qed. 


(** ** EII-3-9 Functions of two arguments *)

(** Given a function f with two arguments and one argument, 
we obtain a function of one argument*)

Definition partial_fun2 f y :=
  Lf (fun x=> Vf f (J x y)) (im_of_singleton (inverse_graph (source f)) y) 
    (target f).

Definition partial_fun1 f x :=
  Lf(fun y=> Vf f (J x y))(im_of_singleton (source f) x) (target f).

Section Funtion_two_args.
Variable f:Set.
Hypothesis ff: function f.
Hypothesis sgf: sgraph (source f).

Lemma partial_fun1_axioms x: 
  lf_axiom (fun y=> Vf f (J x y))(im_of_singleton (source f) x) (target f).
Proof. move=> t /dirim_P [u /set1_P ->]; fprops. Qed.

Lemma partial_fun1_f x: function (partial_fun1 f x).
Proof. by apply: lf_function; apply: partial_fun1_axioms.  Qed.

Lemma partial_fun1_V x y: 
  inc (J x y) (source f) -> Vf (partial_fun1 f x) y = Vf f (J x y) .
Proof.
rewrite/partial_fun1=> Js; aw; first by apply: partial_fun1_axioms.
apply /dirim_P; ex_tac; fprops.
Qed.

Lemma partial_fun2_axioms  y: 
  lf_axiom (fun x=>Vf f (J x y))(im_of_singleton (inverse_graph (source f)) y)
  (target f).
Proof. move=> t /iim_graph_P [u /set1_P ->]; fprops. Qed.

Lemma partial_fun2_f y: function (partial_fun2 f y).
Proof. by apply: lf_function; apply: partial_fun2_axioms.  Qed.

Lemma partial_fun2_V x y:
  inc (J x y) (source f) -> Vf (partial_fun2 f y) x = Vf f (J x y).
Proof.
rewrite/partial_fun2=> Js; aw; first by apply: partial_fun2_axioms.
apply /iim_graph_P; ex_tac; fprops.
Qed.

End Funtion_two_args.

(** Product of two functions *)

Definition ext_to_prod u v :=
  Lf(fun z=> J (Vf u (P z))(Vf v (Q z)))
  ((source u) \times (source v))
  ((target u)\times (target v)).

Notation "f \ftimes g" := (ext_to_prod f g) (at level 40).  

Section Ext_to_prod.
Variables u v: Set.
Hypothesis (fu: function u) (fv: function v).

Lemma ext_to_prod_f:  function (u \ftimes v).
Proof. 
apply: lf_function => t /setX_P [_ px py]; apply: setXp_i; fprops.
Qed. 

Lemma ext_to_prod_V2 c:
  inc c ((source u) \times (source v)) ->
  Vf (u \ftimes v) c = J (Vf u (P c)) (Vf v (Q c)).
Proof. 
rewrite /ext_to_prod=> h; aw => t /setX_P [_ px py]; apply: setXp_i; fprops.
Qed.

Lemma ext_to_prod_V  a b:
  inc a (source u) -> inc b (source v)->
  Vf (u \ftimes v) (J a b) = J (Vf u a) (Vf v b).
Proof. 
by move => asu bsv; rewrite ext_to_prod_V2; aw; apply: setXp_i.
Qed.

Lemma ext_to_prod_s: source (u \ftimes v) = source u \times source v.
Proof. rewrite/ext_to_prod; aw. Qed.

Lemma ext_to_prod_r:
  range (graph (u \ftimes v)) = 
    (range (graph u)) \times (range (graph v)).
Proof.
have fe: (function (u \ftimes v)) by apply:ext_to_prod_f.
set_extens t.
  move/(range_fP fe) => [x ]; rewrite (ext_to_prod_s) => xs ->.
  rewrite (ext_to_prod_V2 xs); move/setX_P:xs => [_ px qx].
  apply /setXp_i; Wtac.
move/setX_P => [pt  /(range_fP fu) [x xsu xp] /(range_fP fv) [y ysv yp]].
apply/(range_fP fe);rewrite ext_to_prod_s; exists (J x y);first by fprops.
by rewrite (ext_to_prod_V)// - pt xp yp.
Qed.

End Ext_to_prod.

Hint Resolve  ext_to_prod_f: fprops.


(** If the two functions are  injective, surjective, bijective, 
so is the product. The inverse of the product is trivial *)

Lemma ext_to_prod_fi u v:
  injection u -> injection  v -> injection (u \ftimes v).
Proof. 
move=> [fu iu] [fv iv]; split; fprops.
rewrite /ext_to_prod; aw.
move => x y xs ys /=; rewrite ext_to_prod_V2 // ext_to_prod_V2 //.
move: xs ys => /setX_P [px pxs qxs] /setX_P [py pys qys] eq.
apply: pair_exten =>//. 
 by apply: iu=>//; apply: (pr1_def eq).
by apply: iv=>//; apply: (pr2_def eq).
Qed.

Lemma ext_to_prod_fs u v:
  surjection u -> surjection  v -> surjection (u \ftimes v).
Proof. 
move=>  [fu su] [fv sv].
split; first by fprops.
move=> y; rewrite ext_to_prod_s  /ext_to_prod; aw.
move/setX_P=> [py ptu qtv].
move: (su _ ptu)=> [pv prv prw].
move: (sv _ qtv)=> [qv qrv qrw]. 
exists (J pv qv); fprops. 
by rewrite ext_to_prod_V // prw qrw py.
Qed.

Lemma ext_to_prod_fb u v:
  bijection u -> bijection  v -> bijection (u \ftimes v).
Proof.  
move => [p1 p2] [p3 p4]. 
split; [by apply: ext_to_prod_fi | by apply: ext_to_prod_fs ].
Qed.

Lemma ext_to_prod_inverse u v:
  bijection u -> bijection  v-> 
  inverse_fun (u \ftimes v) = 
  (inverse_fun u) \ftimes (inverse_fun v).
Proof.
move=> bu bv.
have Ha:bijection (u \ftimes v) by apply: ext_to_prod_fb.
have Hb:function (inverse_fun u) by  apply: bijective_inv_f. 
have Hc:function (inverse_fun v) by  apply: bijective_inv_f. 
apply: function_exten; fprops; try solve [rewrite /ext_to_prod; aw].
  by apply: bijective_inv_f. 
move=> x.
rewrite /ext_to_prod ifun_s lf_target; move/setX_P=>[xp pxu qxv].
rewrite ext_to_prod_V2 //; last apply:setX_i; aw;fprops.
have p1: (inc (Vf (inverse_fun u) (P x)) (source u)).
  by rewrite -ifun_t; Wtac; rewrite ifun_s.
have p2: (inc (Vf (inverse_fun v) (Q x)) (source v)).
  by rewrite -ifun_t; Wtac; rewrite ifun_s.
have eq: x = Vf  (ext_to_prod u v) (J (Vf (inverse_fun u) (P x)) (Vf 
     (inverse_fun v)(Q x))).
  rewrite ext_to_prod_V //; try fct_tac.
  rewrite inverse_V // inverse_V //.
by rewrite {1} eq inverse_V2 // /ext_to_prod; aw;apply: setXp_i.
Qed.


Lemma ext_to_prod_identity x y:
  (identity x) \ftimes (identity y) = identity (x \times y).
Proof.
move:(identity_f x) (identity_f y) => fx fy. 
apply: (function_exten (ext_to_prod_f fx fy) (identity_f (x\times y))).
- rewrite /ext_to_prod; aw.
- rewrite /ext_to_prod; aw.
- rewrite {1} /ext_to_prod;aw;move => i ip /=;rewrite ext_to_prod_V2; aw.
move /setX_P: (ip) => [ha hb hc].
rewrite !identity_V; aw.
Qed.

(** Composition of products *)


Lemma ext_to_prod_coP f g f' g':
   g \coP f -> g' \coP f' -> (g \ftimes g') \coP (f \ftimes f').
Proof.
move => [ha hb hc][ra rb rc]; split => //.
- by apply:ext_to_prod_f.
- by apply:ext_to_prod_f.
- by rewrite /ext_to_prod; aw; rewrite hc rc.
Qed.



Lemma compose_ext_to_prod2 u v u' v':
  u' \coP u -> v' \coP v -> 
  (u'\ftimes  v') \co (u \ftimes v) = (u' \co  u) \ftimes (v' \co v).
Proof. 
move=> cuu cvv.
move:(ext_to_prod_coP cuu cvv) => cee.
have fcu: (function (u' \co u)) by fct_tac.
have fcv: (function (v' \co v)) by fct_tac. 
apply: function_exten; try fct_tac; fprops; try solve [ rewrite/ext_to_prod;aw].
aw; move => x xs1; move: (xs1); rewrite ext_to_prod_s => xs.
move:(xs); move/setX_P => [xp pxs qxs].
have res1: inc (Vf (ext_to_prod u v) x) (product (source u') (source v')).
  have aux: (product (source u') (source v')= target(ext_to_prod u v)).
    by move:cuu => [_ _ ->]; move: cvv => [_ _ ->]; rewrite /ext_to_prod; aw. 
  Wtac; fct_tac.
aw; rewrite ext_to_prod_V2 //; try fct_tac.  
rewrite ext_to_prod_V2 //; try fct_tac. 
rewrite ext_to_prod_V2 //; aw.
Qed.


(** Canonical decomposition of a function *)


Lemma canonical_decomposition1 f
  (g:= restriction_to_image f)
  (i := canonical_injection (range (graph f)) (target f)):
  function f ->
  [/\ i \coP g, f = i \co g, injection i, surjection g &
  (injection f -> bijection g )].
Proof. 
move=> ff.
move: (restriction_to_image_fs ff); rewrite -/g => sg.
have Ha:sub (range (graph f)) (target f) by move:ff=> [? _];  fprops.
have ii: injection i by apply: ci_fi.
have  cig: (i \coP g).
   by split;try fct_tac; rewrite corresp_t corresp_s image_by_fun_source.
split => //.
  apply: function_exten=>//; aw; try fct_tac; rewrite ?corresp_s ? corresp_t //.
  move => x xsf. 
  have ra:= (restriction_to_image_axioms ff).
  have xsg:  inc x (source g) by  rewrite corresp_s.
  aw; rewrite restriction2_V // ci_V //; Wtac.
apply: restriction_to_image_fb.
Qed.

(** Restriction to its image *)


End Bfunction. 

Export Bfunction.