(** * 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.