Library sset2

Theory of Sets EII-3 Correspondences

Copyright INRIA (2009-2013) Apics; Marelle Team (Jose Grimm).


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); move=> t; apply/(domainP gr).
- by move=> x y Hx Hy; set_extens t; rewrite Hx Hy.
- by exists (range r); move=> 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 =>//; move=> 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.
rewrite /triple /source /target /graph => [] [pf pqf].
by apply: pair_exten;aw; fprops.
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 image_by_fun f := direct_image (graph f).
Definition image_of_fun f := image_by_fun 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; [ by move /Zo_hi | move => [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 udr; move: (udr _ 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];apply:Zo_i => //; apply:setX_i => //; ex_tac.
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.
  by case/igraphP => px /igraph_pP; rewrite px.
move => xf; move:(gr _ xf) => px.
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.
  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 => [pa 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 inv_image_by_fun r:= inverse_image (graph r).

Lemma iim_fun_pr r: inv_image_by_fun r = image_by_fun (inverse_fun r).
Proof. rewrite /inv_image_by_fun /inverse_fun /image_by_fun; 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 (inv_image_by_fun 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 => [pa pb pc].
set_extens t.
  move /funI_P => [z pz ->]; apply /compg_pP.
  exists (Vg g z); apply: fdomain_pr1 => //; apply: pc.
  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 pb Pt)(pr2_V pa 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 [ tp [ x ir ir']].
by rewrite -tp; 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 image_by_fun compose.
Proof.
move => r' r x; rewrite /image_by_fun -compg_image; congr (direct_image _).
by rewrite /compose /triple /graph; aw.
Qed.

Lemma compf_inverse: {morph inverse_fun : a b / a \co b >-> b \co a}.
Proof.
move=> a b; rewrite /inverse_fun /compose/triple/source/target/graph.
by 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 ->
  image_of_fun f = range (graph f).
Proof.
move=> ff; rewrite /image_of_fun/image_by_fun -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; move: (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 (image_by_fun f x) <-> exists2 u, inc u x & y = Vf f u).
Proof.
rewrite /image_by_fun=> 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: forall y,
  inc y (image_by_fun f (source f))
    <-> (exists2 u, inc u (source f) & y = Vf f u).
Proof. move => y; exact: (Vf_image_P (@sub_refl (source f))). Qed.

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

Lemma fun_image_Starget: sub (image_of_fun 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) ->
  image_by_fun 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: image_by_fun f emptyset = emptyset.
Proof. by apply /set0_P => t /Zo_hi [x /in_set0]. Qed.

Lemma iim_fun_C g x:
  function g ->
  inv_image_by_fun g ((target g) -s x) = (source g) -s (inv_image_by_fun 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; case: fg => [_ fgg _]; rewrite (fgraph_pr fgg 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 (inv_image_by_fun f (singleton 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 (inv_image_by_fun f (singleton 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 (inv_image_by_fun f (singleton 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 ->
   (inv_image_by_fun f (singleton 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.

We create a function from a map f:a->b

Definition gacreate (a b:Set) (f:a->b) := IM (fun y:a => J (Ro y) (Ro (f y))).
Definition acreate (a b:Set) (f:a->b) := triple a b (gacreate f).

Lemma acreate_triple (a b:Set) (f:a->b): correspondence (acreate f).
Proof.
apply: corresp_create => t tIM.
case /IM_P: tIM=> v <-; apply:setXp_i ; apply: R_inc.
Qed.

Lemma acreate_P (A B:Set) (f:A->B) x:
  inc x (graph (acreate f)) <-> exists u:A, J (Ro u) (Ro (f u)) = x.
Proof. rewrite /acreate /gacreate; aw; apply/IM_P. Qed.

Lemma acreate_source (A B:Set) (f:A->B): source (acreate f)= A.
Proof. by rewrite /acreate; aw. Qed.

Lemma acreate_target (A B:Set) (f:A->B): target (acreate f)= B.
Proof. by rewrite /acreate; aw. Qed.

Hint Rewrite acreate_source acreate_target: aw.

Lemma acreate_function (A B:Set) (f:A->B):
  function (acreate f).
Proof.
move : (acreate_triple f)=>cf.
split=> //.
  split; fprops; move=> x y /acreate_P [v1 <-]/acreate_P [v2 <-]; aw=> eql.
  by rewrite (R_inj eql).
rewrite /acreate /gacreate /domain; aw.
set_extens t.
   move=> tA; apply/funI_P;exists (J t (Ro (f (Bo tA)))); last aw.
   by apply /IM_P; exists (Bo tA); rewrite B_eq.
move/funI_P => [x /IM_P [a <-] ->]; aw; apply: R_inc.
Qed.

Hint Resolve acreate_function: fprops.

Lemma acreate_V (A B:Set) (f:A->B) (x:A):
  Vf (acreate f) (Ro x) = Ro (f x).
Proof.
have rs: (inc (Ro x) (source (acreate f))) by rewrite/acreate; aw; apply: R_inc.
move: (Vf_pr3 (acreate_function f) rs) => /acreate_P [u eql].
by rewrite -(pr2_def eql) (R_inj (pr1_def eql)).
Qed.

We define bcreate1 f of type source f-> target f so that acreate (bcreate1 f) = f

Definition bcreate1 f (H:function f) :=
  fun x:source f => Bo (Vf_target H (R_inc x)).

Lemma prop_bcreate1 f (H:function f) (x:source f):
  Ro (bcreate1 H x) = Vf f (Ro x) .
Proof. by apply: B_eq. Qed.

Lemma bcreate_inv1 f (H:function f):
  acreate (bcreate1 H) = f.
Proof.
apply: function_exten; fprops; rewrite {1}/acreate; aw.
by move=> x xs; rewrite - (B_eq xs) acreate_V; apply: prop_bcreate1.
Qed.


Lemma Vf_mapping f A B x : source f = A -> target f = B ->
  function f -> inc x A -> inc (Vf f x) B.
Proof. move=> Ha Hb ff; rewrite -Ha -Hb; fprops. Qed.

We define bcreate f a b of type a->b, it satisfies acreate (bcreate f a b) = f

Definition bcreate f A B
  (H:function f)(Ha:source f = A)(Hb:target f = B):=
  fun x:A => Bo (Vf_mapping Ha Hb H (R_inc x)).

Lemma prop_bcreate2 f A B
  (H:function f) (Ha:source f = A)(Hb:target f = B)(x:A):
  Ro (bcreate H Ha Hb x) = Vf f (Ro x).
Proof. apply: B_eq. Qed.

Lemma bcreate_inv2 f A B
  (H:function f) (Ha:source f = A)(Hb:target f = B):
  acreate (bcreate H Ha Hb) = f.
Proof.
apply: function_exten; fprops; rewrite /acreate; aw =>//.
by move=> x xs; rewrite -(B_eq xs) acreate_V; apply: prop_bcreate2.
Qed.

Lemma bcreate_inv3 (A B:Set) (f:A->B):
  bcreate (acreate_function f) (acreate_source f)(acreate_target f) =1 f.
Proof. by move=> a;apply: R_inj; rewrite prop_bcreate2 acreate_V. Qed.

Lemma bcreate_eq f (H:function f):
  bcreate1 H =1 bcreate H (refl_equal (source f)) (refl_equal (target f)).
Proof. by move=> a; apply: R_inj; rewrite prop_bcreate2 prop_bcreate1. Qed.

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

Function with empty graph

Definition empty_functionCt x := fun t:emptyset => match t return x with end.
Definition empty_functionC := empty_functionCt emptyset.

Definition empty_function_tg (x: Set) := acreate (empty_functionCt x).
Definition empty_function:= empty_function_tg emptyset.

Lemma empty_function_tg_function x:
   function_prop (empty_function_tg x) emptyset x.
Proof.
red; rewrite /empty_function_tg acreate_source acreate_target;split => //.
apply: acreate_function.
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.
move:(empty_function_tg_function x) => [pa pb pc].
by apply /set0_P => t; move/(p1graph_source1 pa); rewrite pb => /in_set0.
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; move : (empty_source_graph pa pb) => pc.
move:(empty_function_tg_function (target f)) => [qa qb qc].
apply: function_exten3 => //.
  by rewrite empty_function_graph.
by rewrite qb.
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.

Definition identityC (a:Set): a->a := @id a.

Lemma identity_prop1 (a: Set) : acreate (@id a) = identity a.
Proof. apply: function_exten; fprops => t //. Qed.

Lemma identity_prop2 a:
  bcreate (identity_f a) (identity_s a) (identity_t a) =1 @id a.
Proof.
by move=> x; apply: R_inj; rewrite prop_bcreate2 -identity_prop1 acreate_V.
Qed.

Definition of a constant function and of the constant function

Definition constantp x y (f:x->y) := forall a b, f a = f b.
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.

Section ConstantFunction.
Variables (A B y: Set).
Hypothesis (yB: inc y B).

Definition constant_function := acreate ([fun: A => Bo yB]).

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

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

Lemma constant_g: graph (constant_function) = A *s1 y.
Proof.
rewrite/constant_function /acreate /gacreate; aw.
set_extens t.
   move/IM_P => [b] <-; apply/setXp_i; [apply: R_inc| rewrite B_eq; fprops].
move /indexed_P => [pt px qx]; apply/IM_P;exists (Bo px) =>/=.
by rewrite B_eq B_eq -qx pt.
Qed.

Lemma constant_f: function (constant_function).
Proof. rewrite/constant_function; fprops. Qed.

Lemma constant_prop: function_prop (constant_function) A B.
Proof.
rewrite /constant_function /function_prop; aw;split;fprops.
Qed.

Lemma constant_V x: inc x A -> Vf (constant_function) x = y.
Proof.
by move => xA; rewrite - (B_eq xA) acreate_V /= (B_eq yB).
Qed.

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

Lemma constant_fun_constantC x y (a:y):
   constantp ([fun:x => a]).
Proof. done. Qed.

Lemma constant_prop5 x y (f:x->y)(b:x): constantp f ->
  exists a:y, f =1 [fun :x => a].
Proof. move => cf; exists (f b); move=> t; apply: cf. Qed.

Lemma constant_prop6 f:
  constantfp f ->
  f = empty_function_tg (target f) \/
  exists a: target f, f = constant_function (source f) (R_inc 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').
exists (Bo h''); apply: function_exten=>//.
- by apply: constant_f.
- by rewrite /constant_function; aw.
- by rewrite /constant_function acreate_target.
- by move=> y ys /=; rewrite constant_V=>//; rewrite B_eq; apply: pb.
Qed.

EII-3-5 Restrictions and extensions of functions

Composition of Coq function

Lemma compositionC_A a b c d (f: c->d)(g:b->c)(h:a->b):
  (f \o g) \o h = f \o (g \o h).
Proof. trivial. Qed.

Lemma composeC_ev a b c (g:b->c) (f: a->b) x:
   (g \o f) x = g (f x).
Proof. done. Qed.

Lemma compose_id_leftC (a b:Set) (f:a->b):
  (@id b) \o f =1 f.
Proof. done. Qed.

Lemma compose_id_rightC (a b:Set) (f:a->b):
   f \o (@id a) =1 f.
Proof. done. Qed.

Function associated to set inclusion

Definition inclusionC x y (H: sub x y):=
  [fun u:x => Bo (H (Ro u) (R_inc u))].

Lemma inclusionC_pr x y (H: sub x y) (a:x):
  Ro(inclusionC H a) = Ro a.
Proof. by move => /=; apply: B_eq. Qed.

Lemma inclusionC_identity x:
  inclusionC (sub_refl (x:=x)) =1 @id x.
Proof. by move => v; apply: R_inj;rewrite inclusionC_pr. Qed.

Lemma inclusionC_compose x y z (Ha:sub x y)(Hb: sub y z):
  (inclusionC Hb) \o (inclusionC Ha) =1 inclusionC (sub_trans Ha Hb).
Proof. move=> t; by apply: R_inj; rewrite 3! inclusionC_pr. Qed.

Restriction of a Coq function; agreement of subsets

Definition restrictionC (x a b:Set) (f:a->b)(H: sub x a) :=
  f \o (inclusionC H).

Definition agreeC (x a a' b b':Set) (f:a->b) (f':a'-> b')
  (Ha: sub x a)(Hb: sub x a') :=
  forall u:x, Ro(restrictionC f Ha u) = Ro(restrictionC f' Hb u).

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_function f g:
  function f -> function g ->
  (sub (graph f) (graph g) <-> agrees_on (source f) f g).
Proof.
move=> ff fg; split => hyp.
  hnf; 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.
move: (in_graph_Vf ff tg)=> ->; rewrite (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 (image_by_fun 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 (image_by_fun 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 (image_by_fun 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) (image_by_fun f (source 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) ].

Definition extendsC (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a') :=
  sub b b' /\ agreeC g f H (sub_refl (x:=a)).

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).
move: ext => [ff fg sg _].
have pg: (inc (J x (Vf f x)) (graph g)) by apply: sg; Wtac.
by rewrite (Vf_pr fg pg).
Qed.

Lemma extendsC_pr (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a'):
  extendsC g f H -> forall x:a, Ro (f x) = Ro(g (inclusionC H x)).
Proof.
move=> [e1]; rewrite /agreeC => eq x; rewrite eq.
by rewrite /restrictionC composeC_ev inclusionC_identity.
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 function_extends_restC (x a b:Set) (f:a->b)(H:sub x a):
  extendsC f (restrictionC f H) H.
Proof.
split; fprops.
move => t; rewrite /restrictionC compositionC_A 2! composeC_ev.
rewrite inclusionC_compose; congr (Ro (f _)).
by apply: R_inj; rewrite B_eq B_eq.
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 agrees_same_restrictionC (a a' b x:Set) (f:a->b)(g:a'->b)
  (Ha: sub x a)(Hb: sub x a'):
  agreeC f g Ha Hb -> restrictionC f Ha =1 restrictionC g Hb.
Proof. move => ag z; apply: R_inj; apply: ag. 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.
  move/funI_P => [z pa ->].
  have aux: inc (Vg (graph f) z) (target f) by rewrite -/(Vf _ _); Wtac.
  apply:setI2_i => //.
    rewrite -/(Vf _ _); Wtac.
   apply/setX_P; aw;split; fprops.
move/setI2_P => [tg /setX_P [pa pb pc]]; apply /funI_P; ex_tac.
by apply: in_graph_Vf.
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).
rewrite /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].
rewrite (sub_function ff fg); move => [_ sts sg] st.
have au: (sub (image_by_fun 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 red.
apply: function_exten;fprops; try solve [rewrite /restriction2; aw].
  apply: (proj31 (restriction2_prop ax)).
by move => x sf /=; rewrite restriction2_V // sg.
Qed.

Definition restriction2C (a a' b b':Set) (f:a->b)(Ha:sub a' a)
  (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') :=
  fun u=> Bo (H u).

Lemma restriction2C_pr (a a' b b':Set) (f:a->b)(Ha:sub a' a)
  (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') (x:a'):
  Ro (restriction2C H x) = Vf (acreate f) (Ro x).
Proof.
rewrite /restriction2C B_eq; set (y:=inclusionC Ha x).
have RR: (Ro y = Ro x) by rewrite /y/inclusionC B_eq.
by rewrite -RR acreate_V.
Qed.

Lemma restriction2C_pr1 (a a' b b':Set) (f:a->b)
  (Ha:sub a' a)(Hb:sub b' b)
  (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b'):
   f \o (inclusionC Ha) =1 (inclusionC Hb) \o (restriction2C H).
Proof.
by move=> t; rewrite /restriction2C; apply: R_inj; rewrite B_eq B_eq.
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;move=> [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;move=> [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_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 resrtriction_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.

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; move=>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; move=>t; apply: range_i2. Qed.

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

Lemma second_proj_f g: function (second_proj g).
Proof. by apply: lf_function; move=>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=>//;rewrite /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; move=> ->.
move: cgf => [fg ff etc].
apply: function_pr =>//.
  apply: (@sub_trans (range (graph g))).
    apply: composef_range => //.
  by apply: f_range_graph.
by rewrite cd f_domain_graph.
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 => destruct H as [H _ _]; exact H
    | H:composable _ ?X1 |- function ?X1 => destruct H as [_ H _ ]; exact 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 composable_acreate (a b c:Set) (f: a-> b)(g: b->c):
  (acreate g) \coP (acreate f).
Proof. rewrite/composable; aw; split;fprops. Qed.

Lemma compose_acreate (a b c:Set) (g: b->c)(f: a-> b):
  (acreate g) \co (acreate f) = acreate (g \o f).
Proof.
have cfg:= (composable_acreate f g).
apply: function_exten; try fct_tac; fprops; aw.
by move=> x xa /=; aw; rewrite -(B_eq xa) 3! acreate_V.
Qed.

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; hnf;split => //.
move=> 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 -> image_of_fun 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 -> image_of_fun 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.

Bijectivity of Coq functions

Definition injectiveC (a b:Set) (f:a->b) := forall u v, f u = f v -> u =v.
Definition surjectiveC (a b:Set) (f:a->b) := forall u, exists v, f v = u.
Definition bijectiveC (a b:Set) (f:a->b) := injectiveC f /\ surjectiveC f.
Definition right_inverseC (a b:Set) (f: a->b) (H:surjectiveC f) (v:b) :=
   (chooseT (fun k:a => f k = v)
     match H v with | ex_intro x _ => inhabits x end).
Definition inverseC (a b:Set) (f: a->b) (H:bijectiveC f)
   := right_inverseC (proj2 H).

Lemma bijectiveC_pr (a b:Set) (f:a->b) (y:b):
  bijectiveC f -> exists! x:a, f x =y.
Proof.
move=> [fi fs]; apply /unique_existence; split; first by apply: fs.
by move=> x x' <-; move=> veq; symmetry; apply: fi.
Qed.

Lemma identityC_fb (x:Set): bijectiveC (@id x).
Proof. by split => // u; exists u. Qed.

Lemma composeC_inj (a b c:Set) (f:a->b)(f':b->c):
  injectiveC f-> injectiveC f' -> injectiveC (f' \o f).
Proof. by move=> fi fi' x y p; apply: fi; apply: fi'.
Qed.

Lemma composeC_surj (a b c:Set) (f:a->b)(f':b->c):
  surjectiveC f -> surjectiveC f' -> surjectiveC (f' \o f).
Proof.
move => sf sf' y.
move: (sf' y) => [w <-]; move: (sf w) => [z <-].
by exists z.
Qed.

Lemma composeC_bij (a b c:Set) (f:a->b)(f':b->c):
  bijectiveC f -> bijectiveC f' -> bijectiveC (f' \o f).
Proof.
move=> [fi fs] [fi' fs'].
by split; [apply: composeC_inj| apply: composeC_surj ].
Qed.

Lemma right_inverse_pr (a b:Set) (f: a->b) (H:surjectiveC f) (x:b):
  f (right_inverseC H x) = x.
Proof.
by rewrite /right_inverseC; apply:(chooseT_pr (p:= fun k : a => f k = x)).
Qed.

Section InverseProps.
Variables (A B: Set) (f: A -> B).
Hypothesis (H:bijectiveC f).

Lemma inverseC_prb (x: B): f ((inverseC H) x) = x.
Proof. apply: right_inverse_pr. Qed.

Lemma inverseC_pra (x: A): (inverseC H) (f x) = x.
Proof. exact: (proj1 H _ _ (inverseC_prb (f x))). Qed.

Lemma bij_left_inverseC: (inverseC H) \o f =1 @id A.
Proof. by move=> w; rewrite composeC_ev inverseC_pra. Qed.

Lemma bij_right_inverseC: f \o (inverseC H) =1 @id B.
Proof. by move=> t;rewrite composeC_ev inverseC_prb. Qed.

Lemma bijective_inverseC: bijectiveC (inverseC H).
Proof.
split.
  by move=> x y sv; rewrite -(inverseC_prb x) -(inverseC_prb y) sv.
by move=> u; exists (f u); rewrite inverseC_pra.
Qed.
End InverseProps.

Lemma bijection_coq (a b: Set) (f:a->b):
  bijective f <-> bijectiveC f.
Proof.
split.
   move => [g ga gb]; split.
     by move=> x x' feq; move: (f_equal g feq); rewrite 2! ga.
   by move=> x; exists (g x).
move => H; exists (inverseC H).
apply: bij_left_inverseC.
apply: bij_right_inverseC.
Qed.

Lemma inverse_fun_involutiveC (a b:Set) (f:a->b) (H: bijectiveC f):
  f =1 inverseC(bijective_inverseC H).
Proof.
move=> x;move: (bijective_inverseC H) => [i s]; apply: (i).
by rewrite inverseC_pra inverseC_prb.
Qed.

Lemma bcreate_fi f a b
  (H:function f)(Ha:source f = a)(Hb:target f = b):
  injection f -> injectiveC (bcreate H Ha Hb).
Proof.
move=> [ff fi] x y eql; apply: R_inj; apply: fi.
- by rewrite Ha; apply: R_inc.
- by rewrite Ha; apply: R_inc.
- by move: (f_equal (@Ro b) eql); rewrite 2! prop_bcreate2.
Qed.

Lemma bcreate_fs f a b
  (H:function f)(Ha:source f = a)(Hb:target f = b):
  surjection f -> surjectiveC (bcreate H Ha Hb).
Proof.
move=> [ff sf] u.
have Rt: (inc (Ro u) (target f)) by rewrite Hb; apply: R_inc.
have [x xs xv] := (sf _ Rt).
rewrite Ha in xs; exists (Bo xs).
by apply: R_inj; rewrite -xv prop_bcreate2 B_eq.
Qed.

Lemma bcreate_fb f a b
  (H:function f)(Ha:source f =a)(Hb:target f =b):
  bijection f -> bijectiveC (bcreate H Ha Hb).
Proof.
by move=> [fi fs];split ; [apply: bcreate_fi | apply: bcreate_fs].
Qed.

Lemma bcreate1_fi f (H:function f):
  injection f -> injectiveC (bcreate1 H).
Proof.
by move=> fi x y; rewrite !(bcreate_eq H); apply: bcreate_fi.
Qed.

Lemma bcreate1_fs f (H:function f):
  surjection f -> surjectiveC (bcreate1 H).
Proof.
move=> sf x.
move: (bcreate_fs H (refl_equal (source f)) (refl_equal (target f)) sf x).
by move => [v xsf]; exists v; rewrite -xsf -(bcreate_eq H).
Qed.

Lemma bcreate1_fb f (H:function f):
  bijection f -> bijectiveC (bcreate1 H).
Proof.
by move=> [p1 p2];split; [ apply: bcreate1_fi | apply: bcreate1_fs].
Qed.

Lemma acreate_fi (a b:Set) (f:a->b):
  injectiveC f -> injection (acreate f).
Proof.
move=> fi; split; first by fprops.
move=> x y; rewrite {1 2} /acreate; aw => xa ya.
rewrite -(B_eq xa) - (B_eq ya) (acreate_V f (Bo xa)) (acreate_V f (Bo ya)).
by move=> eq; move: (R_inj eq)=> eqv; rewrite (fi _ _ eqv).
Qed.

Lemma acreate_fs (a b:Set) (f:a->b):
  surjectiveC f -> surjection (acreate f).
Proof.
move=> sf; split; fprops.
aw; move => y yb; move: (sf (Bo yb)) => [v fv].
by exists (Ro v); [by apply: R_inc | rewrite acreate_V fv B_eq].
Qed.

Lemma acreate_fb (a b:Set) (f:a->b):
  bijectiveC f -> bijection (acreate f).
Proof.
by move=> [i j]; split; [ apply: acreate_fi| apply: acreate_fs].
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].

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

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

Lemma equipotentC x y: x \Eq y <-> exists f:x->y, bijectiveC f.
Proof.
split.
   move=> [z [bz sz tz]].
   have fz: (function z) by fct_tac.
   by exists (bcreate fz sz tz); apply: bcreate_fb.
move=> [f bf]; exists (acreate f); split; [by apply: acreate_fb | aw | aw].
Qed.

Lemma equipotentR: reflexive_r equipotent.
Proof.
move => x;apply /equipotentC; exists (@id x); apply: identityC_fb.
Qed.

Hint Resolve equipotentR: fprops.

Lemma equipotentT: transitive_r equipotent.
Proof.
move => c b a /equipotentC [f bf] /equipotentC [g bg]; apply /equipotentC.
by exists (g \o f); apply: composeC_bij.
Qed.

Lemma equipotentS: symmetric_r equipotent.
Proof.
move => a b /equipotentC [f bf]; apply /equipotentC.
exists (inverseC bf); apply: bijective_inverseC.
Qed.

Ltac eqtrans u:= apply equipotentT with u; fprops.
Ltac eqsym:= apply: equipotentS.

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.

Injectivity and surjectivity of identity and restriction

Lemma identity_fb x: bijection (identity x).
Proof. rewrite -identity_prop1; apply:acreate_fb; apply: identityC_fb. Qed.

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

Lemma restriction2_fs f x y:
  restriction2_axioms f x y ->
  source f = x -> image_of_fun f = y ->
  surjection (restriction2 f x y).
Proof.
move=> ra sf iy; move: (restriction2_prop ra) => [pa pb pc].
split => // z; rewrite pb pc - {1} iy - {1} sf.
move: (ra) => [ra1 _ _ _].
move /(Vf_image_P1 ra1)=> [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; move: (restriction1_prop ff sxs) => [pa pb pc].
split => //y; rewrite pb pc; move/(Vf_image_P ff sxs) => [b bx Jg].
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.
move: (restriction1_prop ff sxf) => [pa pb pc].
split => //; rewrite pb => a b ax bx.
by do 2 rewrite restriction1_V=>//; apply: fi; apply: sxf.
Qed.

Lemma equipotent_restriction1 f x:
  sub x (source f) -> injection f ->
  x \Eq (image_by_fun f x).
Proof.
move=> wsf bf; rewrite /equipotent/bijection_prop.
exists (restriction1 f x); rewrite corresp_s corresp_t; split => //.
apply: restriction1_fb =>//; move: bf=>[]//.
Qed.

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

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

Lemma restriction_to_image_axioms f: function f ->
  restriction2_axioms f (source f) (image_of_fun 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. 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, image_by_fun f a = inv_image_by_fun (inverse_fun h) a.
Proof.
move => ff a.
move: (proj1 (function_fgraph (proj1 (restriction_to_image_fs ff)))) => aux.
rewrite /inv_image_by_fun/image_by_fun /inverse_image.
rewrite corresp_g (igraph_involutive aux) corresp_g.
congr (direct_image _ a); symmetry;apply/setI2id_Pl.
by move: ff => [[_ p2 _] _].
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.
move: (domain_S(@subsetU2l f (singleton (J x a)))) => sd.
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 =>//.
    apply: fgraph_setU1 =>//.
  by rewrite domain_setU1 dr df.
move=> u; rewrite domain_setU1 dr; case/setU1_P.
  move=> uE.
  have ud: inc u (domain (restr f E)) by rewrite dr.
  rewrite setU1_V_in // restr_ev //.
move=> ->; rewrite 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).
  split.
  - apply: extension_f.
  - rewrite /extension; aw; fprops.
  - rewrite /extension; aw; fprops.
  - move => t /dirim_P [z zsf]; rewrite /extension;aw.
    by case /setU1_P => h; [ Wtac | case: xsf; rewrite -(pr1_def h)].
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 inclusionC_fi a b (H: sub a b):
  injectiveC (inclusionC H).
Proof.
move => x y si; apply: R_inj.
by rewrite - (inclusionC_pr H x) si (inclusionC_pr H y).
Qed.

Lemma canonical_injection_p1 a b (H:sub a b):
   (canonical_injection a b) = acreate (inclusionC H).
Proof.
rewrite /acreate/canonical_injection; congr (triple a b _).
rewrite - diagonal_is_identity.
set_extens t.
  move/diagonal_i_P => [pt pa pq]; apply/IM_P; rewrite -pt -pq.
  by exists (Bo pa); rewrite inclusionC_pr B_eq.
move /IM_P => [x <-]; rewrite inclusionC_pr;apply/diagonal_pi_P.
split => //; apply:R_inc.
Qed.

Lemma ci_fi a b: sub a b -> injection (canonical_injection a b).
Proof.
move => h; rewrite canonical_injection_p1.
apply:acreate_fi; apply:inclusionC_fi.
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 move=> t /set1_P ->; rewrite /y; fprops.
set (g:= canonical_injection (singleton y) (target h)); exists g.
have ysy: inc y (singleton y) by fprops.
set (f:= constant_function (source h) ysy); exists f.
have st: (singletonp (target f)) by rewrite /f constant_t; exists y.
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 sj: surjection f.
  split=>//; rewrite /f tf; move =>z /set1_P ->.
  by exists x; rewrite ?sf ?constant_V.
have c: g \coP f.
  red;rewrite /f /g; split; fprops.
  by rewrite tf /canonical_injection; aw.
split => //; apply: function_exten;aw; fprops; try fct_tac.
   by rewrite /g /canonical_injection; aw.
move=> z zh /=; aw; last (by ue);rewrite (p _ _ zh xs) /f constant_V // ci_V //.
Qed.

Lemma constant_function_pr3 (a:Set) (h:a->Set) (x:a):
  constantp h ->
  exists f: a-> singleton (Ro x), exists g:singleton (Ro x)->Set,
    (forall u:a, h u = g (f u)) /\ (g (Bo (set1_1 (Ro x))) = h x).
Proof.
move=> ch.
exists (fun u=> (Bo (set1_1 (Ro x)))).
by exists (fun t:singleton (Ro x) => h x).
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=>//; rewrite first_proj_V=>//; rewrite first_proj_V=>//; aw.
split=>//; move=>x y xg yg/=; do 2 rewrite first_proj_V=>//.
have [_]: fgraph g by apply /functionalP.
by 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.

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 equipotent_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.

Hint Resolve equipotent_indexed: fprops.

Lemma equipotent_rindexed a b:
  a \Eq (indexedr b a).
Proof.
eqtrans (a *s1 b); fprops; apply: equipotent_product_sym.
Qed.

Lemma equipotent_source_graph f: function f ->
  (graph f) \Eq (source f).
Proof.
move=> ff; eqsym.
apply: (equipotent_aux (f:= (fun z => J z (Vf f z)))); apply: lf_bijective.
    move=> z jz; simpl;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.

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=>//; move=> x x' y.
  move/igraph_pP;rewrite -ifun_g => r1 ;move/igraph_pP; rewrite -ifun_g=> r2.
  by move: fif => [_ fg _ ]; apply: (fgraph_pr fg r1 r2).
apply: surjective_pr4=> //; rewrite - igraph_domain; fprops.
by rewrite -ifun_g /inverse_fun; aw.
Qed.

Lemma inverseC_prc (a b:Set) (f:a-> b) (H:bijectiveC f):
  inverse_fun (acreate f) = acreate(inverseC H).
Proof.
move: (acreate_fb H) => ab.
apply: function_exten.
- by apply: bijective_inv_f.
- by fprops.
- by rewrite/acreate; aw.
- by rewrite/acreate; aw.
move => x; aw => xb.
have [y eq]: exists y:a, f y = (Bo xb) by apply: (proj2 H).
set g := (acreate (inverseC H)).
have ta: a = target (acreate (inverseC H)) by rewrite acreate_target.
set u := Vf g x.
have: x = Vf (acreate f) u.
  by rewrite /u - {2} (B_eq xb) - eq acreate_V inverseC_pra acreate_V eq B_eq.
move => h; symmetry;apply: Vf_pr; first by apply: bijective_inv_f.
rewrite /inverse_fun; aw; apply /igraph_pP; rewrite h; apply: Vf_pr3 => //.
  fct_tac.
aw; rewrite /u ta; apply: Vf_target; first by apply: acreate_function.
by rewrite acreate_source.
Qed.

Lemma bijective_double_inverseC (a b:Set) (f:a->b) g g':
  g \o f =1 @id a -> f \o g' =1 @id b ->
  bijectiveC f.
Proof.
move=> c1 c2; split.
  move=> x x' feq; move: (f_equal g feq); rewrite -!(composeC_ev g f) !c1 //.
move=> x; exists (g' x); rewrite -!(composeC_ev f g') c2 //.
Qed.

Lemma bijective_double_inverseC1 (a b:Set) (f:a->b) g g'
  (Ha: g \o f =1 @id a)(Hb: f \o g' =1 @id b):
  g =1 inverseC (bijective_double_inverseC Ha Hb)
  /\ g' =1 inverseC (bijective_double_inverseC Ha Hb).
Proof.
have sg: (g' =1 g).
  by move=> x; rewrite -{1} (Ha (g' x)) -{2} (Hb x) !composeC_ev.
set h := inverseC _.
have gh: (g' =1 h).
  move => x; have e1: (f (g' x) = x) by apply: (Hb x).
  by rewrite /h -{2} e1 inverseC_pra.
by split =>//; apply: ftrans gh.
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 composable_f_inv f: bijection f -> f \coP (inverse_fun f).
Proof.
move=> bf.
have fif: (function (inverse_fun f)) by apply: bijective_inv_f.
split;[fct_tac | done | aw].
Qed.

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

Lemma acreate_exten (a b: Set) (f g: a-> b):
  f =1 g -> acreate f = acreate g.
Proof.
move=> h; apply: function_exten; fprops; aw.
by move=> x [z za]; rewrite -za ! acreate_V h.
Qed.

Lemma bij_right_inverse f:
  bijection f -> f \co (inverse_fun f) = identity (target f).
Proof.
move=> bf.
move: (refl_equal (source f)) (refl_equal (target f))=> ss tt.
rewrite -(identity_prop1 (target f)).
have ff := (bij_function bf).
rewrite - (bcreate_inv2 ff ss tt) acreate_target
   (inverseC_prc (bcreate_fb ff ss tt bf)) compose_acreate.
apply: acreate_exten; move=> t.
by rewrite (bij_right_inverseC (bcreate_fb ff ss tt bf)) //.
Qed.

Lemma bij_left_inverse f:
  bijection f -> (inverse_fun f) \co f = identity (source f).
Proof.
move=> bf.
move: (refl_equal (source f)) (refl_equal (target f))=> ss tt.
rewrite -(identity_prop1 (source f)).
have ff := (bij_function bf).
rewrite - (bcreate_inv2 ff ss tt).
rewrite (inverseC_prc (bcreate_fb ff ss tt bf))
  acreate_source compose_acreate ;apply: acreate_exten.
by move=> t; rewrite bij_left_inverseC.
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 inverse_V f x:
  bijection f -> inc x (target f) ->
  Vf f (Vf (inverse_fun f) x) = x.
Proof.
move=> bf xt; symmetry.
transitivity (Vf (identity (target f)) x); first by bw.
by rewrite -(bij_right_inverse bf); aw; apply: composable_f_inv.
Qed.

Lemma inverse_V2 f y:
  bijection f -> inc y (source f) ->
  Vf (inverse_fun f) (Vf f y) = y.
Proof.
move=> bf ys; symmetry.
transitivity (Vf (identity (source f)) y); first by bw.
by rewrite -(bij_left_inverse bf); aw; apply: composable_inv_f.
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.
move=>->; apply: Vf_target; aw; apply: (proj1(proj1(inverse_bij_fb bf))).
Qed.

Properties of direct and inverse images

Lemma sub_inv_im_source f y:
  function f -> sub y (target f) ->
  sub (inv_image_by_fun 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 (image_by_fun f (image_by_fun (inverse_fun f) y)) y.
Proof.
move=> ff yt x.
have aux: sub (image_by_fun (inverse_fun f) y) (source f).
  by rewrite /inverse_fun/image_by_fun; 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 (image_by_fun 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) ->
  (image_by_fun f (image_by_fun (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 (image_by_fun (inverse_fun f) (image_by_fun 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) ->
   x = (image_by_fun (inverse_fun f) (image_by_fun f x)).
Proof.
move=> [ff fi] xsf.
apply: extensionality; first 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.
symmetry in Vv.
by rewrite - (fi _ _ (xsf _ vx) (p1graph_source ff Jg) 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).


Definition is_left_inverseC (a b:Set) (f:a->b) r := r \o f =1 @id a.
Definition is_right_inverseC (a b:Set) (f:a->b) s:= f \o s =1 @id b.

Lemma left_i_target f r: is_left_inverse f r -> target r = source f.
Proof. by move=> [_ c]; move: (f_equal target c); 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=> [_ h]; move: (f_equal source h); 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.

Lemma right_i_v (a b:Set) (f:a->b) s (x:b):
  is_right_inverseC f s -> f (s x) = x.
Proof. by move=> e; move: (e x); rewrite composeC_ev. Qed.

Lemma left_i_v (a b:Set) (f:a->b) r (x:a):
  is_left_inverseC f r -> r (f x) = x.
Proof. by move=> e; move: (e x); rewrite composeC_ev. Qed.

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

Lemma inj_if_exists_left_invC (a b:Set) (f:a-> b):
  (exists r, is_left_inverseC f r) -> injectiveC f.
Proof.
move=> [r ilr] x x'.
by move /(congr1 r); move: (ilr x) (ilr x') => /= -> ->.
Qed.

Lemma surj_if_exists_right_invC (a b:Set) (f:a->b):
  (exists s, is_right_inverseC f s) -> surjectiveC f.
Proof.
by move=> [s rsf] u; exists (s u); rewrite (right_i_v u rsf).
Qed.

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.

Left inverse for an injective function (f: a->b)

Definition left_inverseC (a b:Set) (f: a->b)(H:inhabited a)
  (v:b) := (chooseT (fun u:a => (~ (exists x:a, f x = v)) \/ (f u = v)) H).

Lemma left_inverseC_pr (a b:Set) (f: a->b) (H:inhabited a) (u:a):
  f (left_inverseC f H (f u)) = f u.
Proof.
rewrite /left_inverseC.
set p:= fun u:a => _.
have: (p (chooseT p H)) by apply: chooseT_pr; exists u; right.
case=>//; by case; exists u.
Qed.

Lemma left_inverse_comp_id (a b:Set) (f:a->b) (H:inhabited a):
  injectiveC f -> (left_inverseC f H) \o f =1 @id a.
Proof.
move => fi t; apply fi; rewrite composeC_ev;apply: left_inverseC_pr.
Qed.

Lemma exists_left_inv_from_injC (a b:Set) (f:a->b): inhabited a ->
  injectiveC f -> exists r, is_left_inverseC f r.
Proof.
move=> H fi; exists (left_inverseC f H); by apply: left_inverse_comp_id.
Qed.

Lemma right_inverse_comp_id (a b:Set) (f:a-> b) (H:surjectiveC f):
  f \o (right_inverseC H) =1 @id b.
Proof. move=> x; rewrite composeC_ev;apply: right_inverse_pr. Qed.

Lemma exists_right_inv_from_surjC (a b:Set)(f:a-> b) (H:surjectiveC f):
  exists s, is_right_inverseC f s.
Proof. exists (right_inverseC H); apply: right_inverse_comp_id. 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 nesf; move: (inj_function fi) => ff.
move: (bcreate1_fi (H:=ff) fi)=>ib.
have nesf0: inhabited (source f).
 by move: nesf => [y [w _]]; apply: inhabits.
case: (exists_left_inv_from_injC nesf0 ib) => x px.
move: (compose_acreate x (bcreate1 ff));rewrite bcreate_inv1 => aux.
exists (acreate x).
split; first by split; fprops; aw.
rewrite aux;apply: function_exten; fprops; aw.
move=> u usf /=; rewrite identity_V //.
by move: usf => [v vs];rewrite -vs acreate_V px.
Qed.

Theorem exists_right_inv_from_surj f:
  surjection f -> exists s, is_right_inverse f s.
Proof.
move=> sf.
move:(surj_function sf)=> ff; move: (bcreate1_fs ff sf)=> bs.
move:(exists_right_inv_from_surjC bs)=> [s ris].
move:(compose_acreate (bcreate1 ff) s); rewrite bcreate_inv1 => aux.
exists (acreate s); split; first by red; split; aw;fprops.
rewrite aux;apply: function_exten; fprops; aw.
move=> u usf /=; rewrite identity_V //.
by move: usf => [v vs];rewrite -vs acreate_V ris.
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