Library sset2
Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset1.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Theorem range_domain_exists r: sgraph r ->
((exists! a, forall x, inc x a <-> (exists y, inc (J x y) r)) /\
(exists! b, forall y, inc y b <-> (exists x, inc (J x y) r))).
Proof.
move=> gr; split; apply /unique_existence; split.
- exists (domain r); move=> t; apply/(domainP gr).
- by move=> x y Hx Hy; set_extens t; rewrite Hx Hy.
- by exists (range r); move=> t; apply/(rangeP gr).
- by move=> x y Hx Hy; set_extens t; rewrite Hx Hy.
Qed.
A product is a special graph
Lemma sub_graph_setX r: sgraph r ->
sub r ((domain r) \times (range r)).
Proof. move=> gr t tr; apply/setX_P; split; fprops. Qed.
Lemma setX_graph x y: sgraph (x \times y).
Proof. by move=> t /setX_P []. Qed.
Lemma sub_setX_graph u x y: sub u (x \times y) -> sgraph u.
Proof. move=> su t tu; exact: (setX_graph (su _ tu)). Qed.
Hint Resolve setX_graph: fprops.
Lemma setX_relP x y a b:
related (x \times y) a b <-> (inc a x /\ inc b y).
Proof.
by split;[ move/setX_P => [_ ]; aw | move => [ax biy]; apply: setXp_i ].
Qed.
Lemma setX_domain x y: nonempty y -> domain (x \times y) = x.
Proof.
move=> [z zy]; set_extens t.
by case/funI_P => u /setX_P [_ xx _] ->.
move=> tx; apply/funI_P;exists (J t z); aw; fprops.
Qed.
Lemma setX_range x y: nonempty x -> range (x \times y) = y.
Proof.
move=> [z zy]; set_extens t.
by case/(funI_P) => u /setX_P [_ _ xx] ->.
move=> tx; apply/funI_P;exists (J z t); aw; fprops.
Qed.
Hint Rewrite setX_domain setX_range : bw.
Diagonal of a set: this is a functional graph x -> x
Definition diagonal x := Zo (coarse x)(fun y=> P y = Q y).
Lemma diagonal_i_P x u:
inc u (diagonal x) <-> [/\ pairp u, inc (P u) x & P u = Q u].
Proof.
split; first by case/Zo_P => /setX_P [ta tb _] tc.
move=> [ta tb tc]; apply: Zo_i => //;rewrite -ta; apply: setXp_i => //; ue.
Qed.
Lemma diagonal_pi_P x u v:
inc (J u v) (diagonal x) <-> (inc u x /\ u = v).
Proof.
apply: (iff_trans (diagonal_i_P x (J u v))); aw.
split; [by case | move => []; split; fprops ].
Qed.
Lemma diagonal_is_identity x: diagonal x = identity_g x.
Proof.
set_extens t.
move /diagonal_i_P => [pt Pt eql]; rewrite -pt -eql;apply /funI_P; ex_tac.
by move /funI_P => [z zx ->]; apply/diagonal_pi_P.
Qed.
A correspondence is a triple (G,A,B), graph, source and target,
such that G is a subset of the product A \times B.
The domain of G is a subset of A.
The range of G is a subset of B.
Definition triplep f := pairp f /\ pairp (Q f).
Definition source x := P (Q x).
Definition target x := Q (Q x).
Definition graph x := P x.
Definition triple s t g := J g (J s t).
Definition correspondence f :=
triplep f /\ sub (graph f) ((source f) \times (target f)).
Lemma corr_propcc s t g:
sub g (s \times t) <-> [/\ sgraph g, sub (domain g) s & sub (range g) t].
Proof.
split => [sg | [gg sd sr] x xg ].
have gg:= (sub_setX_graph sg).
by split =>//; move=> z /funI_P [y yp ->];move/setX_P: (sg _ yp) => [_].
rewrite - (gg _ xg); apply: setXp_i; [ apply: sd | apply: sr]; fprops.
Qed.
Lemma corr_propc f (g := graph f):
correspondence f ->
[/\ sgraph g, sub (domain g) (source f) & sub (range g) (target f)].
Proof. by move=> [tf sg]; apply /corr_propcc. Qed.
Lemma triple_corr s t g: triplep (triple s t g).
Proof. by rewrite /triple; split; [| aw]; fprops. Qed.
Lemma corresp_recov f: triplep f ->
triple (source f) (target f) (graph f) = f.
Proof.
rewrite /triple /source /target /graph => [] [pf pqf].
by apply: pair_exten;aw; fprops.
Qed.
Lemma corresp_recov1 f: correspondence f ->
triple (source f) (target f) (graph f) = f.
Proof. by move => [t _]; apply: corresp_recov. Qed.
Lemma corresp_s s t g: source (triple s t g) = s.
Proof. rewrite /triple /source; aw. Qed.
Lemma corresp_t s t g: target (triple s t g) = t.
Proof. rewrite /triple /target; aw. Qed.
Lemma corresp_g s t g: graph (triple s t g) = g.
Proof. rewrite /triple /graph; aw. Qed.
Hint Rewrite corresp_s corresp_t corresp_g : aw.
Lemma corresp_create s t g:
sub g (s \times t) -> correspondence (triple s t g).
Proof. by move=> h; split; [apply: triple_corr | aw ]. Qed.
Some properties of a correspondence
Lemma corresp_is_graph g: correspondence g -> sgraph (graph g).
Proof. by case/corr_propc. Qed.
Lemma corresp_sub_range g:
correspondence g -> sub (range (graph g)) (target g).
Proof. by move /corr_propc => [_ _]. Qed.
Lemma corresp_sub_domain g:
correspondence g -> sub (domain (graph g)) (source g).
Proof. by move /corr_propc => [_]. Qed.
Hint Resolve corresp_sub_range corresp_sub_domain corresp_is_graph: fprops.
The set of correspondences E->F is the product of P and singleton E
and singleton F, where P == powerset (E \times F)
is the set of graphs of correspondences
Definition correspondences x y :=
(powerset (x \times y)) \times ( (singleton x) \times (singleton y)).
Lemma correspondences_P x y z:
inc z (correspondences x y) <->
[/\ correspondence z, source z = x & target z = y].
Proof.
rewrite /correspondence /source/target.
split.
by case/setX_P => [pz /setP_P spz/setX_P [p_qz /set1_P -> /set1_P ->]].
move => [ [ [tp sgp] aux] <- <-].
apply:setX_i;[ exact | by apply/ setP_P | apply:setX_i; fprops].
Qed.
Image by the graph r of a set u
Definition direct_image f X:=
Zo (range f) (fun y=>exists2 x, inc x X & inc (J x y) f).
Definition image_by_fun f := direct_image (graph f).
Definition image_of_fun f := image_by_fun f (source f).
Lemma dirim_P f X y:
inc y (direct_image f X) <-> exists2 x, inc x X & inc (J x y) f.
Proof.
split; [ by move /Zo_hi | move => [x xu pr]; apply/Zo_i; ex_tac ].
Qed.
Lemma dirimE f X: fgraph f -> sub X (domain f) ->
direct_image f X = fun_image X (Vg f).
Proof.
move => sgf sxd; set_extens t.
move /dirim_P => [x xX pf]; apply /funI_P.
move: (pr2_V sgf pf); aw => ->; ex_tac.
move /funI_P => [z sX ->]; apply /dirim_P; ex_tac; apply: fdomain_pr1 => //.
by apply: sxd.
Qed.
Lemma dirim_Sr f X: sub (direct_image f X) (range f).
Proof. apply: Zo_S. Qed.
Lemma dirim_domain f: sgraph f -> direct_image f (domain f) = range f.
Proof.
move=> sgf; apply: extensionality; first by apply: dirim_Sr.
move => t /funI_P [y yf ->]; apply: Zo_i; first by fprops.
by exists (P y); fprops;rewrite (sgf _ yf).
Qed.
Lemma dirim_set0 f: direct_image f emptyset = emptyset.
Proof. by apply /set0_P => t /Zo_hi [x /in_set0]. Qed.
Lemma dirim_setn0 f u: sgraph f -> nonempty u -> sub u (domain f)
-> nonempty (direct_image f u).
Proof.
move=> gr [x] xu udr; move: (udr _ xu); case /(domainP gr)=> [y Jr].
exists y;apply: Zo_i; ex_tac.
Qed.
Theorem dirim_S f: {compat (direct_image f): u v / sub u v}.
Proof.
move=> u u' uu' t /dirim_P [x xu pr]; apply/dirim_P.
by exists x => //;apply: uu'.
Qed.
Section of the graph r at x
Definition im_of_singleton f x:= direct_image f (singleton x).
Lemma dirim_set1_P f x y:
inc y (im_of_singleton f x) <-> inc (J x y) f.
Proof.
apply: (iff_trans (dirim_P f _ y)).
split; [ by move => [z /set1_P ->] | move => pf; ex_tac; fprops ].
Qed.
Lemma dirim_set1_S f f': sgraph f -> sgraph f' ->
((forall x, sub (im_of_singleton f x) (im_of_singleton f' x)) <-> sub f f').
Proof.
move=> gr gr'.
split=> s x t.
move: (gr _ t) => eql; rewrite - eql;apply/dirim_set1_P.
by apply: s; apply/dirim_set1_P; rewrite eql.
by move/dirim_set1_P => jf; apply/dirim_set1_P; apply:s.
Qed.
Definition inverse_graph r :=
Zo ((range r) \times (domain r)) (fun y=> inc (J (Q y)(P y)) r).
Lemma igraph_graph r: sgraph (inverse_graph r).
Proof. move=> x /Zo_S xp; apply: (setX_pair xp). Qed.
Hint Resolve igraph_graph: fprops.
Lemma igraphP r y:
inc y (inverse_graph r) <-> (pairp y /\ inc (J (Q y)(P y)) r).
Proof.
split; first by case/Zo_P => yp pr; split => //; apply: (setX_pair yp).
move => [py pr];apply:Zo_i => //; apply:setX_i => //; ex_tac.
Qed.
Lemma igraph_pP r x y: inc (J x y) (inverse_graph r) <-> inc (J y x) r.
Proof.
split; [case/igraphP;aw | move=> pr; apply/igraphP; aw; fprops ].
Qed.
Lemma igraph_alt r: sgraph r ->
inverse_graph r = fun_image r (fun z => J (Q z) (P z)).
Proof.
move=> gr; set_extens t.
by move /igraphP => [pt h];apply/funI_P; ex_tac; aw; rewrite pt.
by move /funI_P => [c zr ->]; apply/igraph_pP; rewrite (gr _ zr).
Qed.
Lemma igraph_involutive : {when sgraph, involutive inverse_graph}.
Proof.
move=> f gr; set_extens x.
by case/igraphP => px /igraph_pP; rewrite px.
move => xf; move:(gr _ xf) => px.
by rewrite -px;apply/igraph_pP /igraph_pP; rewrite px.
Qed.
Lemma igraph_range r: sgraph r -> range (inverse_graph r) = domain r.
Proof.
move=> gr; set_extens x.
move/funI_P => [y /igraphP [_ h] ->]; ex_tac.
move/funI_P => [y yi ->]; apply: (range_i (x:=(Q y))); apply/igraph_pP.
by rewrite (gr _ yi).
Qed.
Lemma igraph_domain r: sgraph r -> domain (inverse_graph r) = range r.
Proof.
move=> gr;rewrite - {2} (igraph_involutive gr) igraph_range //.
apply: igraph_graph.
Qed.
Lemma igraph0: inverse_graph (emptyset) = emptyset.
Proof. by apply /set0_P => t /igraphP [_ /in_set0]. Qed.
Hint Rewrite igraph0: bw.
Lemma igraphX x y: inverse_graph (x \times y) = y \times x.
Proof.
set_extens t.
by move /igraphP => [pt /setX_P]; aw; move => [_ pa pb];apply: setX_i.
move/setX_P=> [pt pa pb]; apply /igraphP; fprops.
Qed.
Lemma igraph_identity_g x:
inverse_graph (identity_g x) = identity_g x.
Proof.
rewrite/inverse_graph identity_r identity_d - diagonal_is_identity.
set_extens z;move /Zo_P => [pa pb]; apply: Zo_i => //.
by move/Zo_hi: pb; aw.
by rewrite -pb;apply/diagonal_pi_P;split => //; move /setX_P: pa => [_].
Qed.
Hint Rewrite igraph_identity_g igraphX: aw.
Inverse correspondence
Definition inverse_fun m :=
triple (target m) (source m) (inverse_graph (graph m)).
Lemma icor_correspondence m:
correspondence m -> correspondence (inverse_fun m).
Proof.
move => [pa pb]; apply: corresp_create => x/igraphP [px pg].
by move /setXp_P: (pb _ pg) => [pc pd]; apply: setX_i.
Qed.
Lemma icor_involutive:
{when correspondence, involutive inverse_fun}.
Proof.
move=> m cm ; rewrite /inverse_fun; aw; rewrite igraph_involutive;fprops.
by apply: corresp_recov1.
Qed.
Lemma ifun_s f: source (inverse_fun f) = target f.
Proof. rewrite/inverse_fun; aw. Qed.
Lemma ifun_t f: target (inverse_fun f) = source f.
Proof. rewrite/inverse_fun; aw. Qed.
Lemma ifun_g f: graph (inverse_fun f) = inverse_graph (graph f).
Proof. rewrite /inverse_fun;aw. Qed.
Hint Rewrite ifun_s ifun_t ifun_g : aw.
Hint Resolve icor_correspondence: fprops.
Inverse image by a graph r of a set x
Definition inverse_image r := direct_image (inverse_graph r).
Definition inv_image_by_fun r:= inverse_image (graph r).
Lemma iim_fun_pr r: inv_image_by_fun r = image_by_fun (inverse_fun r).
Proof. rewrite /inv_image_by_fun /inverse_fun /image_by_fun; aw. Qed.
Lemma iim_graph_P x r y:
(inc y (inverse_image r x)) <-> (exists2 u, inc u x & inc (J y u) r).
Proof.
by apply: (iff_trans (dirim_P _ x y)); split;
move => [u ux pr]; ex_tac; apply /igraph_pP.
Qed.
Lemma iim_fun_P x r y:
inc y (inv_image_by_fun r x) <->(exists2 u, inc u x & inc (J y u) (graph r)).
Proof. exact:iim_graph_P. Qed.
Definition composeg r' r :=
Zo ((domain r) \times (range r'))
(fun w => exists2 y, inc (J (P w) y) r & inc (J y (Q w)) r').
Notation "x \cg y" := (composeg x y) (at level 50).
Lemma compg_graph r r': sgraph (r \cg r').
Proof. by move=> t /Zo_P [/setX_pair]. Qed.
Hint Resolve compg_graph: fprops.
Lemma compg_P r r' x:
inc x (r' \cg r) <->
(pairp x /\ (exists2 y, inc (J (P x) y) r & inc (J y (Q x)) r')).
Proof.
split;first by move/Zo_P => [pa pb];split => //; apply: (setX_pair pa).
move => [pa pb]; apply: Zo_i => //.
move: pb => [z pc pd];apply/setX_P;split => //; ex_tac.
Qed.
Lemma compg_pP r r' x y:
inc (J x y) (r' \cg r) <-> (exists2 z, inc (J x z) r & inc (J z y) r').
Proof.
apply: (iff_trans (compg_P _ _ _) ); aw.
split;[ by case | move => h; fprops].
Qed.
Lemma compg_domain_S r r': sub (domain (r' \cg r)) (domain r).
Proof. move => t /funI_P [y /compg_P [_ [s sa _]] ->]; ex_tac. Qed.
Lemma compg_rangeS r r': sub (range (r' \cg r)) (range r').
Proof. move => t /funI_P [y /compg_P [_ [s _ sa]] ->]; ex_tac. Qed.
Lemma compg_composef f g: f \cfP g -> f \cf g = f \cg g.
Proof.
move => [pa pb pc].
set_extens t.
move /funI_P => [z pz ->]; apply /compg_pP.
exists (Vg g z); apply: fdomain_pr1 => //; apply: pc.
apply /range_gP => //; ex_tac.
move/compg_P => [pt [y Pt Qt]]; apply /funI_P; exists (P t); first by ex_tac.
by move: (pr2_V pb Pt)(pr2_V pa Qt); aw => <- <-.
Qed.
Proposition 3, inverse of composition
Theorem compg_inverse: {morph inverse_graph : a b / a \cg b >-> b \cg a}.
Proof.
move => r r';set_extens x.
move/igraphP => [px] /compg_pP [z pa pb].
by rewrite -px; apply/compg_pP; exists z => //; apply/igraph_pP.
move/compg_P => [px [y /igraph_pP pa /igraph_pP pb]].
by rewrite -px; apply/igraph_pP/compg_pP; exists y.
Qed.
Proposition 4, associativity of composition
Theorem compgA : associative composeg.
Proof.
move => r r' r'';set_extens x.
move /compg_P=> [px [y /compg_pP [z pa pb] pc]].
rewrite -px; apply/compg_pP; ex_tac; apply/compg_pP; ex_tac.
move /compg_P=> [px [y pa /compg_pP [z pb pc]]].
rewrite -px; apply/compg_pP; ex_tac; apply/compg_pP; ex_tac.
Qed.
Proposition 5 Image of composition
Theorem compg_image: action_prop direct_image composeg.
Proof.
move => gr_imegr' r x;set_extens t.
move /dirim_P => [z zx /compg_pP [u pa pb]].
apply/dirim_P; ex_tac; apply/dirim_P; ex_tac.
move /dirim_P => [z /dirim_P [u pa pb] pc].
apply/dirim_P; ex_tac; apply/compg_pP; ex_tac.
Qed.
More properties of composition
Lemma compg_domain r r':
sgraph r' -> domain (r' \cg r) = inverse_image r (domain r').
Proof.
move=>gr; have cg:= (@compg_graph r' r); set_extens t.
move/(domainP cg) => [y /compg_pP [z pa pb]].
apply/iim_graph_P; ex_tac; ex_tac.
move/iim_graph_P => [x /(domainP gr) [y pa] pb].
apply/(domainP cg); exists y; apply /compg_pP; ex_tac.
Qed.
Lemma compg_range r r':
sgraph r -> range (r' \cg r) = direct_image r' (range r).
Proof.
move=>gr;have cg:= (@compg_graph r' r); set_extens t.
move/(rangeP cg) => [y /compg_pP [z pa pb]]; apply/dirim_P; ex_tac; ex_tac.
move/dirim_P => [x /(rangeP gr) [y pa] pb].
apply/(rangeP cg); exists y; apply /compg_pP; ex_tac.
Qed.
Lemma inverse_direct_imageg r x:
sgraph r -> sub x (domain r) ->
sub x (inverse_image r (direct_image r x)).
Proof.
move=> gt xd t tx.
move /funI_P :(xd _ tx)=> [y yr eq].
have aux:inc (J t (Q y)) r by rewrite eq (gt _ yr).
apply/iim_graph_P;ex_tac;apply/dirim_P; ex_tac.
Qed.
Lemma compg_S r r' s s':
sub r s -> sub r' s' -> sub (r' \cg r) (s' \cg s).
Proof.
move=> rs rs' t /compg_P [ tp [ x ir ir']].
by rewrite -tp; apply/compg_pP; exists x; [apply: rs | apply: rs'].
Qed.
Composition of two correspondences
Definition composableC r' r :=
[/\ correspondence r, correspondence r' & source r' = target r].
Definition compose r' r :=
triple (source r)(target r') ((graph r') \cg (graph r)).
Notation "f1 \co f2" := (compose f1 f2) (at level 50).
Lemma compf_correspondence r' r:
correspondence r -> correspondence r' ->
correspondence (r' \co r).
Proof.
rewrite/compose=> cr cr'; apply: corresp_create.
move=>t /compg_P [pt [y ir ir']]; apply:setX_i => //.
move /setX_P: ((proj2 cr) _ ir) => [_ pa _];move: pa; aw.
move /setX_P: ((proj2 cr') _ ir');aw; move => [_ _ pb]; move: pb; aw.
Qed.
Lemma compf_image: action_prop image_by_fun compose.
Proof.
move => r' r x; rewrite /image_by_fun -compg_image; congr (direct_image _).
by rewrite /compose /triple /graph; aw.
Qed.
Lemma compf_inverse: {morph inverse_fun : a b / a \co b >-> b \co a}.
Proof.
move=> a b; rewrite /inverse_fun /compose/triple/source/target/graph.
by aw; rewrite compg_inverse.
Qed.
Identity correspondence, will be shown to be a function later
Definition identity x := triple x x (identity_g x).
Lemma identity_corresp x: correspondence (identity x).
Proof.
by apply: corresp_create; rewrite -diagonal_is_identity; apply: Zo_S.
Qed.
Lemma identity_s x: source (identity x) = x.
Proof. rewrite/identity; aw. Qed.
Lemma identity_t x: target (identity x) = x.
Proof. rewrite/identity; aw. Qed.
Lemma identity_graph0 x: graph (identity x) = identity_g x.
Proof. rewrite/identity; aw. Qed.
Hint Rewrite identity_s identity_t: aw.
Lemma compf_id_left m:
correspondence m -> (identity (target m)) \co m = m.
Proof.
move=> cm.
suff : ((identity_g (target m)) \cg (graph m) = graph m).
by rewrite /compose identity_graph0; aw => ->; apply: corresp_recov1.
rewrite -diagonal_is_identity.
set_extens t.
by move /compg_P=> [ {3} <- [y p1 /diagonal_pi_P [_ <-]]].
have gm: (sgraph (graph m)) by fprops.
move => tg; apply/compg_P; split; first by apply: (gm _ tg).
move /setX_P: ((proj2 cm) _ tg) => [pt _ qt].
by exists (Q t); [ rewrite pt | apply/diagonal_pi_P].
Qed.
Corollary compose_identity_left E:
{when (fun x => correspondence x /\ (target x) = E),
left_id (identity E) compose}.
Proof. move => x [cx <-]; exact:compf_id_left. Qed.
Lemma compf_id_right m:
correspondence m -> m \co (identity (source m)) = m.
Proof.
move=> cm.
suff: ((graph m) \cg (identity_g (source m))= graph m).
by rewrite /compose identity_graph0; aw => ->; apply: corresp_recov1.
rewrite -diagonal_is_identity.
set_extens t.
by move /compg_P => [ {3} <- [y /diagonal_pi_P [pa ->] p1]].
have gm: (sgraph (graph m)) by fprops.
move => tg; apply/compg_P; split; first by apply: (gm _ tg).
move /setX_P: (proj2 cm _ tg) => [pt qt _].
by exists (P t); [ apply/diagonal_pi_P | rewrite pt ].
Qed.
Lemma compf_id_id x:
(identity x) \co (identity x) = (identity x).
Proof. by move: (compf_id_right (@identity_corresp x)); aw. Qed.
Lemma identity_self_inverse x:
inverse_fun (identity x) = (identity x).
Proof. rewrite /inverse_fun /identity; aw. Qed.
End Correspondence.
Export Correspondence.
This is a different but equivalent definition
Definition functional_graph r := forall x, singl_val (related r x).
Lemma functionalP r:
(sgraph r /\ functional_graph r) <-> (fgraph r).
Proof.
rewrite /functional_graph /related; split; last first.
by move=> fr; split; fprops; move=> x y y'; apply: fgraph_pr.
move => [gr eql]; split=>// x y xr yr eqp.
move: (xr) (yr); rewrite -(gr _ xr) - (gr _ yr) -eqp => pa pb.
by rewrite (eql _ _ _ pa pb).
Qed.
A function is a correspondence with a functional graph whose
source is the domain of the graph
Definition function f :=
[/\ correspondence f, fgraph (graph f) & source f = domain (graph f)].
Lemma function_pr s t g:
fgraph g -> sub (range g) t -> s = domain g ->
function (triple s t g).
Proof.
rewrite /function => fg sr d; aw; split => //.
by apply: corresp_create; rewrite d; apply /corr_propcc; split => //;case: fg.
Qed.
Lemma function_fgraph f: function f -> fgraph (graph f).
Proof. by move=> [_]. Qed.
Lemma function_sgraph f: function f -> sgraph (graph f).
Proof. by move=> [_ [h _]]. Qed.
Lemma f_domain_graph f: function f -> domain (graph f) = source f.
Proof. by move=> [_ ]. Qed.
Lemma f_range_graph f: function f -> sub (range (graph f))(target f).
Proof. by move => [cf _ _]; apply:corresp_sub_range. Qed.
Hint Rewrite f_domain_graph : aw.
Hint Resolve function_sgraph function_fgraph : fprops.
Lemma image_by_fun_source f: function f ->
image_of_fun f = range (graph f).
Proof.
move=> ff; rewrite /image_of_fun/image_by_fun -f_domain_graph => //.
by apply: dirim_domain; fprops.
Qed.
The value of the function f at x is Vf x f
Definition Vf f x := Vg (graph f) x.
Section Vf_pr.
Variable f: Set.
Hypothesis ff: function f.
Lemma Vf_pr3 x: inc x (source f) -> inc (J x (Vf f x)) (graph f).
Proof. by move=> xf; apply: fdomain_pr1; fprops; aw. Qed.
Lemma in_graph_Vf x: inc x (graph f) -> x = (J (P x) (Vf f (P x))).
Proof. by move=> xf; apply: in_graph_V; fprops. Qed.
Lemma Vf_pr2 x: inc x (graph f) -> Q x = Vf f (P x).
Proof. by move=> xg; apply: pr2_V; fprops. Qed.
Lemma Vf_pr x y: inc (J x y) (graph f) -> y = Vf f x.
Proof. by move=> Jg; move: (in_graph_Vf Jg); aw; apply: pr2_def. Qed.
Lemma range_fP y:
inc y (range (graph f)) <-> exists2 x, inc x (source f) & y = Vf f x.
Proof. move: ff => [_ fgf ->]; apply/(range_gP fgf). Qed.
Lemma Vf_range_g x: inc x (source f) -> inc (Vf f x) (range (graph f)).
Proof. move=> xsf; apply /range_fP;ex_tac. Qed.
Lemma Vf_target x: inc x (source f) -> inc (Vf f x) (target f).
Proof. move/Vf_range_g;apply: (f_range_graph ff).
Qed.
Lemma p1graph_source x y: inc (J x y) (graph f) -> inc x (source f).
Proof. move: ff => [_ fgf ->] jg; ex_tac. Qed.
Lemma p2graph_target x y : inc (J x y) (graph f) -> inc y (target f).
Proof.
move=> Jgf; rewrite (Vf_pr Jgf); apply: Vf_target; apply: (p1graph_source Jgf).
Qed.
Lemma p1graph_source1 x: inc x (graph f) -> inc (P x) (source f).
Proof.
move=> xgf; apply: (p1graph_source (y:= (Vf f (P x)))).
by rewrite - (in_graph_Vf xgf).
Qed.
Lemma p2graph_target1 x: inc x (graph f) -> inc (Q x) (target f).
Proof.
move=> xgf; move: (in_graph_Vf xgf)=> ->; aw.
by apply: Vf_target => //; apply: p1graph_source1.
Qed.
Lemma Vf_image_P x: sub x (source f) -> forall y,
(inc y (image_by_fun f x) <-> exists2 u, inc u x & y = Vf f u).
Proof.
rewrite /image_by_fun=> ss;split.
by move/dirim_P => [a ax Jg]; ex_tac; apply: Vf_pr.
move=> [u ux ->]; apply/dirim_P; ex_tac;apply: Vf_pr3; fprops.
Qed.
Lemma Vf_image_P1: forall y,
inc y (image_by_fun f (source f))
<-> (exists2 u, inc u (source f) & y = Vf f u).
Proof. move => y; exact: (Vf_image_P (@sub_refl (source f))). Qed.
Lemma fun_image_Starget1 x: sub (image_by_fun f x) (target f).
Proof. apply: sub_trans (f_range_graph ff); apply: dirim_Sr. Qed.
Lemma fun_image_Starget: sub (image_of_fun f) (target f).
Proof. apply: fun_image_Starget1. Qed.
End Vf_pr.
Hint Resolve Vf_target : fprops.
Ltac Wtac :=
match goal with
| |- inc (J ?x (Vf ?f ?x)) (graph ?f) => apply: Vf_pr3 ; fprops
| h:inc (J ?x ?y) (graph ?f) |- Vf ?f ?x = ?y
=> symmetry; apply: Vf_pr ; fprops
| h:inc (J ?x ?y) (graph ?f) |- ?y = Vf ?f ?x => apply: Vf_pr ; fprops
| |- inc (Vf ?f _) (range (graph ?f)) => apply: Vf_range_g ; fprops
| h1: function ?f, h2: inc ?x (source ?f) |- inc (Vf ?f ?x) (target ?f)
=> apply: (Vf_target h1 h2)
| h2:target ?f = ?y |- inc (Vf ?f ?x) ?y
=> rewrite - h2; Wtac
| h2: ?y = target ?f |- inc (Vf ?f ?x) ?y
=> rewrite h2; Wtac
| h1: inc ?x ?y, h2: ?y = source ?f |- inc (Vf ?f ?x) (target ?f)
=> rewrite h2 in h1; Wtac
| h1: inc ?x ?y, h2: source ?f = ?y |- inc (Vf ?f ?x) (target ?f)
=> rewrite - h2 in h1; Wtac
| |- inc (Vf ?f _) (target ?f)
=> apply: (Vf_target); fprops
| Ha:function ?X1, Hb: inc (J _ ?X2) (graph ?X1)
|- inc ?X2 (target ?X1)
=> apply: (p2graph_target Ha Hb)
| Ha:function ?X1, Hb: inc (J ?X2 _) (graph ?X1)
|- inc ?X2 (source ?X1)
=> apply: (p1graph_source Ha Hb)
| Ha:function ?X1, Hb: inc ?X2 (graph ?X1)
|- inc (P ?X2) (source ?X1)
=> apply: (p1graph_source1 Ha Hb)
| Ha:function ?X1, Hb: inc ?X2 (graph ?X1)
|- inc (Q ?X2) (target ?X1)
=> apply: (p2graph_target1 Ha Hb)
end.
Lemma function_functional f: correspondence f ->
(function f <-> (forall x, inc x (source f) ->
exists! y, related (graph f) x y)).
Proof.
rewrite/related=> cf; split.
move=> ff x xsf;exists (Vf f x); split; first by Wtac.
move => y yg; symmetry; apply: (Vf_pr ff yg).
move => eu.
have sd:source f = domain (graph f).
apply: extensionality; last by fprops.
move=> t ts; move: (eu _ ts) => [y [ja jb]].
by apply/funI_P; ex_tac; aw.
split=>//;apply /functionalP; split; first by fprops.
move=> x y y'; rewrite /related => h1.
have isf: inc x (source f) by rewrite sd; apply/funI_P; ex_tac; aw.
move: h1; move/unique_existence: (eu _ isf) => [_]; apply.
Qed.
Lemmas that say when two functions are equal
Definition same_Vf f g:= Vf f =1 Vf g.
Definition cstfp (f E: Set) := singl_val_fp (inc ^~E) (Vf f).
Definition cstgp (f E: Set) := singl_val_fp (inc ^~E) (Vg f).
Notation "f1 =1f f2" := (same_Vf f1 f2)
(at level 70, no associativity) : fun_scope.
Lemma function_exten3 f g:
function f -> function g ->
graph f = graph g -> target f = target g -> source f = source g ->
f = g.
Proof.
move => [[ff _] _ _] [[fg _] _ _] e1 e2 e3.
by rewrite -(corresp_recov ff) -(corresp_recov fg); congr (triple _ _ _).
Qed.
Lemma function_exten1 f g:
function f -> function g ->
graph f = graph g -> target f = target g ->
f = g.
Proof.
move => ff fg e1 e2; apply: function_exten3=>//.
by rewrite -!f_domain_graph // e1.
Qed.
Lemma function_exten f g:
function f -> function g ->
source f = source g -> target f = target g -> {inc (source f), f =1f g}
-> f = g.
Proof.
move=> ff fg e1 r2 e2; apply: function_exten3=> //.
set_extens x => xg.
have Pf : (inc (P x) (source f)) by Wtac.
by rewrite (in_graph_Vf ff xg) (e2 _ Pf); Wtac; rewrite -e1.
have Pg : (inc (P x) (source f)) by rewrite e1; Wtac.
by rewrite (in_graph_Vf fg xg) -(e2 _ Pg); Wtac.
Qed.
The image of singleton by a function is a singleton
Lemma fun_image_set1 f x:
function f -> inc x (source f) ->
image_by_fun f (singleton x) = singleton (Vf f x).
Proof.
move=> ff xsf.
apply: set1_pr; first by apply /dirim_set1_P; Wtac.
by move => z /dirim_set1_P jg; apply:Vf_pr.
Qed.
Lemma fun_image_set0 f: image_by_fun f emptyset = emptyset.
Proof. by apply /set0_P => t /Zo_hi [x /in_set0]. Qed.
Lemma iim_fun_C g x:
function g ->
inv_image_by_fun g ((target g) -s x) = (source g) -s (inv_image_by_fun g x).
Proof.
move => fg.
have gg: sgraph (graph g) by fprops.
set_extens t.
move/iim_graph_P => [u /setC_P [ut nux] Jug];apply/setC_P.
split; first by Wtac.
move/iim_graph_P => [w wx Jwg].
by case: nux; case: fg => [_ fgg _]; rewrite (fgraph_pr fgg Jug Jwg).
move/setC_P => [ts neu].
have Jg: (inc (J t (Vf g t))(graph g)) by Wtac.
apply/iim_graph_P; ex_tac;apply/setC_P; split; fprops.
dneg Wx; apply/iim_graph_P; ex_tac.
Qed.
Lemma iim_fun_set1_hi f x y: function f ->
inc x (inv_image_by_fun f (singleton y)) -> y = Vf f x.
Proof. by move => ff /iim_fun_P [u /set1_P ->]; apply: Vf_pr. Qed.
Lemma iim_fun_set1_i f x y: function f -> inc x (source f) ->
y = Vf f x -> inc x (inv_image_by_fun f (singleton y)).
Proof. move => ff xsf ->; apply /iim_fun_P; ex_tac; Wtac. Qed.
Lemma iim_fun_set1_P f y: function f -> forall x,
inc x (inv_image_by_fun f (singleton y)) <->
(inc x (source f) /\ y = Vf f x).
Proof.
move => ff x; split.
move /iim_fun_P => [u /set1_P -> pa]; split;Wtac.
by move => [pa pb]; apply:iim_fun_set1_i.
Qed.
Lemma iim_fun_set1_E f y: function f ->
(inv_image_by_fun f (singleton y)) = Zo (source f) (fun x => y = Vf f x).
Proof.
move => ff; set_extens t.
by move /(iim_fun_set1_P _ ff) => pa; apply /Zo_P.
by move => /Zo_P pa; apply /(iim_fun_set1_P _ ff).
Qed.
We create a function from a map f:a->b
Definition gacreate (a b:Set) (f:a->b) := IM (fun y:a => J (Ro y) (Ro (f y))).
Definition acreate (a b:Set) (f:a->b) := triple a b (gacreate f).
Lemma acreate_triple (a b:Set) (f:a->b): correspondence (acreate f).
Proof.
apply: corresp_create => t tIM.
case /IM_P: tIM=> v <-; apply:setXp_i ; apply: R_inc.
Qed.
Lemma acreate_P (A B:Set) (f:A->B) x:
inc x (graph (acreate f)) <-> exists u:A, J (Ro u) (Ro (f u)) = x.
Proof. rewrite /acreate /gacreate; aw; apply/IM_P. Qed.
Lemma acreate_source (A B:Set) (f:A->B): source (acreate f)= A.
Proof. by rewrite /acreate; aw. Qed.
Lemma acreate_target (A B:Set) (f:A->B): target (acreate f)= B.
Proof. by rewrite /acreate; aw. Qed.
Hint Rewrite acreate_source acreate_target: aw.
Lemma acreate_function (A B:Set) (f:A->B):
function (acreate f).
Proof.
move : (acreate_triple f)=>cf.
split=> //.
split; fprops; move=> x y /acreate_P [v1 <-]/acreate_P [v2 <-]; aw=> eql.
by rewrite (R_inj eql).
rewrite /acreate /gacreate /domain; aw.
set_extens t.
move=> tA; apply/funI_P;exists (J t (Ro (f (Bo tA)))); last aw.
by apply /IM_P; exists (Bo tA); rewrite B_eq.
move/funI_P => [x /IM_P [a <-] ->]; aw; apply: R_inc.
Qed.
Hint Resolve acreate_function: fprops.
Lemma acreate_V (A B:Set) (f:A->B) (x:A):
Vf (acreate f) (Ro x) = Ro (f x).
Proof.
have rs: (inc (Ro x) (source (acreate f))) by rewrite/acreate; aw; apply: R_inc.
move: (Vf_pr3 (acreate_function f) rs) => /acreate_P [u eql].
by rewrite -(pr2_def eql) (R_inj (pr1_def eql)).
Qed.
We define bcreate1 f of type source f-> target f
so that acreate (bcreate1 f) = f
Definition bcreate1 f (H:function f) :=
fun x:source f => Bo (Vf_target H (R_inc x)).
Lemma prop_bcreate1 f (H:function f) (x:source f):
Ro (bcreate1 H x) = Vf f (Ro x) .
Proof. by apply: B_eq. Qed.
Lemma bcreate_inv1 f (H:function f):
acreate (bcreate1 H) = f.
Proof.
apply: function_exten; fprops; rewrite {1}/acreate; aw.
by move=> x xs; rewrite - (B_eq xs) acreate_V; apply: prop_bcreate1.
Qed.
Lemma Vf_mapping f A B x : source f = A -> target f = B ->
function f -> inc x A -> inc (Vf f x) B.
Proof. move=> Ha Hb ff; rewrite -Ha -Hb; fprops. Qed.
We define bcreate f a b of type a->b,
it satisfies acreate (bcreate f a b) = f
Definition bcreate f A B
(H:function f)(Ha:source f = A)(Hb:target f = B):=
fun x:A => Bo (Vf_mapping Ha Hb H (R_inc x)).
Lemma prop_bcreate2 f A B
(H:function f) (Ha:source f = A)(Hb:target f = B)(x:A):
Ro (bcreate H Ha Hb x) = Vf f (Ro x).
Proof. apply: B_eq. Qed.
Lemma bcreate_inv2 f A B
(H:function f) (Ha:source f = A)(Hb:target f = B):
acreate (bcreate H Ha Hb) = f.
Proof.
apply: function_exten; fprops; rewrite /acreate; aw =>//.
by move=> x xs; rewrite -(B_eq xs) acreate_V; apply: prop_bcreate2.
Qed.
Lemma bcreate_inv3 (A B:Set) (f:A->B):
bcreate (acreate_function f) (acreate_source f)(acreate_target f) =1 f.
Proof. by move=> a;apply: R_inj; rewrite prop_bcreate2 acreate_V. Qed.
Lemma bcreate_eq f (H:function f):
bcreate1 H =1 bcreate H (refl_equal (source f)) (refl_equal (target f)).
Proof. by move=> a; apply: R_inj; rewrite prop_bcreate2 prop_bcreate1. Qed.
Definition function_prop f s t:=
[/\ function f, source f = s & target f = t].
Function with empty graph
Definition empty_functionCt x := fun t:emptyset => match t return x with end.
Definition empty_functionC := empty_functionCt emptyset.
Definition empty_function_tg (x: Set) := acreate (empty_functionCt x).
Definition empty_function:= empty_function_tg emptyset.
Lemma empty_function_tg_function x:
function_prop (empty_function_tg x) emptyset x.
Proof.
red; rewrite /empty_function_tg acreate_source acreate_target;split => //.
apply: acreate_function.
Qed.
Lemma empty_function_function: function_prop empty_function emptyset emptyset.
Proof. apply:empty_function_tg_function. Qed.
Lemma empty_function_graph x: graph (empty_function_tg x) = emptyset.
Proof.
move:(empty_function_tg_function x) => [pa pb pc].
by apply /set0_P => t; move/(p1graph_source1 pa); rewrite pb => /in_set0.
Qed.
Lemma empty_function_p1 f: function f ->
graph f = emptyset -> source f = emptyset.
Proof. move => [_ _ ->] ->; bw. Qed.
Lemma empty_function_p2 f: function f ->
target f = emptyset -> source f = emptyset.
Proof.
by move => ff te; apply /set0_P => x /(Vf_target ff); rewrite te => /in_set0.
Qed.
Lemma empty_source_graph f:
function f -> source f = emptyset -> graph f = emptyset.
Proof.
move => ff sfe; apply /set0_P => x xp.
apply: (@in_set0 (P x)); rewrite - sfe; Wtac.
Qed.
Lemma empty_target_graph f:
function f -> target f = emptyset -> graph f = emptyset.
Proof.
move => ff sfe; apply /set0_P => x xp.
case: (@in_set0 (Vf f (P x))); Wtac; Wtac.
Qed.
Lemma empty_source_graph2 f:
function f -> source f = emptyset ->
f = empty_function_tg (target f).
Proof.
move => pa pb; move : (empty_source_graph pa pb) => pc.
move:(empty_function_tg_function (target f)) => [qa qb qc].
apply: function_exten3 => //.
by rewrite empty_function_graph.
by rewrite qb.
Qed.
Properties of the identity function
Lemma identity_prop x: function_prop (identity x) x x.
Proof.
rewrite /identity /function_prop; aw; split => //; apply: function_pr.
- by apply: identity_fgraph.
- by rewrite identity_r; fprops.
- by rewrite identity_d.
Qed.
Lemma identity_f x: function (identity x).
Proof. exact (proj31 (identity_prop x)). Qed.
Lemma identity_V x y:
inc y x -> Vf (identity x) y = y.
Proof. move =>yx; rewrite /Vf /identity; aw; apply:(identity_ev yx). Qed.
Hint Rewrite identity_V: bw.
Hint Resolve identity_f: fprops.
Definition identityC (a:Set): a->a := @id a.
Lemma identity_prop1 (a: Set) : acreate (@id a) = identity a.
Proof. apply: function_exten; fprops => t //. Qed.
Lemma identity_prop2 a:
bcreate (identity_f a) (identity_s a) (identity_t a) =1 @id a.
Proof.
by move=> x; apply: R_inj; rewrite prop_bcreate2 -identity_prop1 acreate_V.
Qed.
Definition of a constant function and of the constant function
Definition constantp x y (f:x->y) := forall a b, f a = f b.
Definition constantfp f := function f /\ cstfp f (source f).
Definition constantgp f := fgraph f /\ cstgp f (domain f).
Lemma constant_prop1 f: constantgp f -> small_set (range f).
Proof.
move=> [ff eq] t1 t2 /(range_gP ff) [x xd ->] /(range_gP ff) [y yd ->].
by apply: eq.
Qed.
Lemma constant_prop2 f: constantfp f -> constantgp (graph f).
Proof. move=> [ff eq]; split; fprops; by move:ff=> [_ _ <-]. Qed.
Lemma constant_prop3 x y: constantgp (cst_graph x y).
Proof.
split; [ fprops | move => a b; rewrite cst_graph_d => ax bx; bw ].
Qed.
Lemma constant_prop4 f: function f ->
(constantfp f <-> small_set (range (graph f))).
Proof.
move => ff; split => h.
by apply: constant_prop1; apply: constant_prop2.
split=> // x x' xs x's; apply: h; Wtac.
Qed.
Section ConstantFunction.
Variables (A B y: Set).
Hypothesis (yB: inc y B).
Definition constant_function := acreate ([fun: A => Bo yB]).
Lemma constant_s: source (constant_function) = A.
Proof. rewrite /constant_function; aw. Qed.
Lemma constant_t: target (constant_function) = B.
Proof. rewrite /constant_function; aw. Qed.
Lemma constant_g: graph (constant_function) = A *s1 y.
Proof.
rewrite/constant_function /acreate /gacreate; aw.
set_extens t.
move/IM_P => [b] <-; apply/setXp_i; [apply: R_inc| rewrite B_eq; fprops].
move /indexed_P => [pt px qx]; apply/IM_P;exists (Bo px) =>/=.
by rewrite B_eq B_eq -qx pt.
Qed.
Lemma constant_f: function (constant_function).
Proof. rewrite/constant_function; fprops. Qed.
Lemma constant_prop: function_prop (constant_function) A B.
Proof.
rewrite /constant_function /function_prop; aw;split;fprops.
Qed.
Lemma constant_V x: inc x A -> Vf (constant_function) x = y.
Proof.
by move => xA; rewrite - (B_eq xA) acreate_V /= (B_eq yB).
Qed.
Lemma constant_constant_fun: constantfp (constant_function).
Proof.
split; first by apply: constant_f.
rewrite constant_s => u v /= us vs; do 2 rewrite constant_V=>//.
Qed.
End ConstantFunction.
Lemma constant_fun_constantC x y (a:y):
constantp ([fun:x => a]).
Proof. done. Qed.
Lemma constant_prop5 x y (f:x->y)(b:x): constantp f ->
exists a:y, f =1 [fun :x => a].
Proof. move => cf; exists (f b); move=> t; apply: cf. Qed.
Lemma constant_prop6 f:
constantfp f ->
f = empty_function_tg (target f) \/
exists a: target f, f = constant_function (source f) (R_inc a).
Proof.
move => [pa pb].
case: (emptyset_dichot (source f)) => h.
by left; rewrite {1} (empty_source_graph2 pa h).
right; have h':=(rep_i h); have h'' := (Vf_target pa h').
exists (Bo h''); apply: function_exten=>//.
- by apply: constant_f.
- by rewrite /constant_function; aw.
- by rewrite /constant_function acreate_target.
- by move=> y ys /=; rewrite constant_V=>//; rewrite B_eq; apply: pb.
Qed.
Lemma compositionC_A a b c d (f: c->d)(g:b->c)(h:a->b):
(f \o g) \o h = f \o (g \o h).
Proof. trivial. Qed.
Lemma composeC_ev a b c (g:b->c) (f: a->b) x:
(g \o f) x = g (f x).
Proof. done. Qed.
Lemma compose_id_leftC (a b:Set) (f:a->b):
(@id b) \o f =1 f.
Proof. done. Qed.
Lemma compose_id_rightC (a b:Set) (f:a->b):
f \o (@id a) =1 f.
Proof. done. Qed.
Function associated to set inclusion
Definition inclusionC x y (H: sub x y):=
[fun u:x => Bo (H (Ro u) (R_inc u))].
Lemma inclusionC_pr x y (H: sub x y) (a:x):
Ro(inclusionC H a) = Ro a.
Proof. by move => /=; apply: B_eq. Qed.
Lemma inclusionC_identity x:
inclusionC (sub_refl (x:=x)) =1 @id x.
Proof. by move => v; apply: R_inj;rewrite inclusionC_pr. Qed.
Lemma inclusionC_compose x y z (Ha:sub x y)(Hb: sub y z):
(inclusionC Hb) \o (inclusionC Ha) =1 inclusionC (sub_trans Ha Hb).
Proof. move=> t; by apply: R_inj; rewrite 3! inclusionC_pr. Qed.
Restriction of a Coq function; agreement of subsets
Definition restrictionC (x a b:Set) (f:a->b)(H: sub x a) :=
f \o (inclusionC H).
Definition agreeC (x a a' b b':Set) (f:a->b) (f':a'-> b')
(Ha: sub x a)(Hb: sub x a') :=
forall u:x, Ro(restrictionC f Ha u) = Ro(restrictionC f' Hb u).
The functions agree on x if they take the same value
Definition agrees_on x f f' :=
[/\ sub x (source f), sub x (source f') & {inc x, f =1f f'} ].
Lemma same_graph_agrees f f':
function f -> function f' -> graph f = graph f' ->
agrees_on (source f) f f'.
Proof.
move=> ff ff' geq.
have seq: (source f = source f').
by rewrite -(f_domain_graph ff) -(f_domain_graph ff') geq.
rewrite /agrees_on - seq; split; fprops.
move=> a /(Vf_pr3 ff); rewrite geq => aux.
by rewrite -(Vf_pr ff' aux).
Qed.
Lemma function_exten2 f f':
function f -> function f' ->
(f = f' <->
[/\ source f = source f', target f = target f' & agrees_on (source f) f f']).
Proof.
move=> ff ff'; split.
by rewrite /agrees_on; move => -> ;split => //; split.
move => [seq teq [_ _ ag]]; apply: function_exten; fprops.
Qed.
Lemma sub_function f g:
function f -> function g ->
(sub (graph f) (graph g) <-> agrees_on (source f) f g).
Proof.
move=> ff fg; split => hyp.
hnf; split => //.
by do 2 rewrite -f_domain_graph=>//; apply: domain_S.
by move=> a af /=;rewrite- (Vf_pr fg (hyp _ (Vf_pr3 ff af))).
move => t tg; move: hyp => [_ sg ag].
have Ptsf: (inc (P t) (source f)) by Wtac.
move: (in_graph_Vf ff tg)=> ->; rewrite (ag _ Ptsf); Wtac.
Qed.
[/\ sub x (source f), sub x (source f') & {inc x, f =1f f'} ].
Lemma same_graph_agrees f f':
function f -> function f' -> graph f = graph f' ->
agrees_on (source f) f f'.
Proof.
move=> ff ff' geq.
have seq: (source f = source f').
by rewrite -(f_domain_graph ff) -(f_domain_graph ff') geq.
rewrite /agrees_on - seq; split; fprops.
move=> a /(Vf_pr3 ff); rewrite geq => aux.
by rewrite -(Vf_pr ff' aux).
Qed.
Lemma function_exten2 f f':
function f -> function f' ->
(f = f' <->
[/\ source f = source f', target f = target f' & agrees_on (source f) f f']).
Proof.
move=> ff ff'; split.
by rewrite /agrees_on; move => -> ;split => //; split.
move => [seq teq [_ _ ag]]; apply: function_exten; fprops.
Qed.
Lemma sub_function f g:
function f -> function g ->
(sub (graph f) (graph g) <-> agrees_on (source f) f g).
Proof.
move=> ff fg; split => hyp.
hnf; split => //.
by do 2 rewrite -f_domain_graph=>//; apply: domain_S.
by move=> a af /=;rewrite- (Vf_pr fg (hyp _ (Vf_pr3 ff af))).
move => t tg; move: hyp => [_ sg ag].
have Ptsf: (inc (P t) (source f)) by Wtac.
move: (in_graph_Vf ff tg)=> ->; rewrite (ag _ Ptsf); Wtac.
Qed.
Restriction of the function to a part of it source
Lemma restr_range f x:
function f-> sub x (source f) ->
sub (range (restr (graph f) x)) (target f).
Proof.
move=> ff sxdf t /funI_P [z /funI_P [s zg ->] ->]; aw;rewrite -/(Vf _ _); Wtac.
Qed.
Definition restriction f x :=
triple x (target f) (restr (graph f) x).
Definition restriction1 f x :=
triple x (image_by_fun f x) (restr (graph f) x).
Definition restriction2 f x y :=
triple x y ((graph f)\cap (x \times (target f))).
Definition restriction2_axioms f x y :=
[/\ function f,
sub x (source f), sub y (target f) & sub (image_by_fun f x) y].
Lemma restriction_prop f x:
function f -> sub x (source f) ->
function_prop (restriction f x) x (target f).
Proof.
rewrite /restriction /function_prop=> ff xs; aw; split => //.
by apply: function_pr; bw; fprops; apply: restr_range.
Qed.
Lemma restriction1_prop f x:
function f -> sub x (source f) ->
function_prop (restriction1 f x) x (image_by_fun f x).
Proof.
rewrite /restriction1 /function_prop =>ff ssf; aw; split => //.
apply: function_pr; fprops; bw.
rewrite Lg_range => t /funI_P [z zx ->]; apply/dirim_P; ex_tac.
rewrite -/(Vf _ _); Wtac.
Qed.
Lemma restriction2_props f x y:
restriction2_axioms f x y ->
domain ((graph f) \cap (x \times (target f))) = x.
Proof.
move=> ra; set i := _ \cap _.
have gi: sgraph i by rewrite /i => t /setI2_P [_] /setX_P [].
set_extens t.
by move/funI_P => [z /setI2_P [_ /setX_P [_ h _]] ->].
move:ra => [ ff xsf ysf etc] tx.
apply/(domainP gi); exists (Vf f t); apply/setI2_P; split; [Wtac| ].
apply: setXp_i => //; Wtac.
Qed.
Lemma restriction2_prop f x y:
restriction2_axioms f x y -> function_prop (restriction2 f x y) x y.
Proof.
move=> ra; move:(ra) => [ff ss st etc].
rewrite /restriction2 /function_prop; aw; split => //.
move:(restriction2_props ra); set g := _ \cap _ => dg.
have fg: fgraph g.
rewrite /g; apply: (@sub_fgraph _ (graph f)); fprops; apply: setI2_1.
apply: function_pr=>// t tr; apply: etc; apply /dirim_P.
move/(rangeP (proj1 fg)): tr => [z /setI2_P [jg /setXp_P [zx _]]];ex_tac.
Qed.
Lemma restriction_V f x:
function f -> sub x (source f) ->
{inc x, (restriction f x) =1f f}.
Proof. rewrite /Vf/restriction => ff ss a xa; aw; bw; fprops; aw. Qed.
Lemma restriction1_V f x:
function f -> sub x (source f) ->
{inc x, (restriction1 f x) =1f f}.
Proof. rewrite /Vf/restriction1 => ff ss a xa; aw; bw; fprops; aw. Qed.
Lemma restriction2_V f x y:
restriction2_axioms f x y ->
{inc x, (restriction2 f x y) =1f f}.
Proof.
move => ra a ax; move: (ra) => [ff sf tf sif].
rewrite /Vf/restriction2; aw.
apply: sub_graph_ev; fprops;first by apply: setI2_1.
by rewrite (restriction2_props ra).
Qed.
Lemma restriction1_pr f:
function f -> restriction2 f (source f) (image_by_fun f (source f)) =
restriction1 f (source f).
Proof.
rewrite/restriction2/restriction1=> ff.
have rg: (restr (graph f) (source f) = graph f).
rewrite (proj33 ff); apply: restr_to_domain; fprops.
by rewrite (proj1 (setI2id_Pl _ _) (proj2 (proj31 ff))) rg.
Qed.
g extends f if its restriction to the source of f is f
Definition extends g f :=
[/\ function f, function g, sub (graph f) (graph g)
& sub (target f)(target g) ].
Definition extendsC (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a') :=
sub b b' /\ agreeC g f H (sub_refl (x:=a)).
Lemma extends_Ssource f g:
extends g f -> sub (source f) (source g).
Proof.
by move=> [ff fg sg st]; do 2 rewrite -f_domain_graph=>//; apply: domain_S.
Qed.
Lemma extends_sV f g:
extends g f -> {inc (source f), f =1f g}.
Proof.
move=> ext x xf; have ss:= (extends_Ssource ext).
move: ext => [ff fg sg _].
have pg: (inc (J x (Vf f x)) (graph g)) by apply: sg; Wtac.
by rewrite (Vf_pr fg pg).
Qed.
Lemma extendsC_pr (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a'):
extendsC g f H -> forall x:a, Ro (f x) = Ro(g (inclusionC H x)).
Proof.
move=> [e1]; rewrite /agreeC => eq x; rewrite eq.
by rewrite /restrictionC composeC_ev inclusionC_identity.
Qed.
Lemma function_extends_restr f x:
function f -> sub x (source f) ->
extends f (restriction f x).
Proof.
move =>ff ssf; have [pa pb pc] := (restriction_prop ff ssf).
split => //; last by rewrite pc.
rewrite /restriction; aw => s /funI_P [z zx ->].
by apply: Vf_pr3 => //; apply: ssf.
Qed.
Lemma function_extends_restC (x a b:Set) (f:a->b)(H:sub x a):
extendsC f (restrictionC f H) H.
Proof.
split; fprops.
move => t; rewrite /restrictionC compositionC_A 2! composeC_ev.
rewrite inclusionC_compose; congr (Ro (f _)).
by apply: R_inj; rewrite B_eq B_eq.
Qed.
Lemma agrees_same_restriction f g x:
function f -> function g -> agrees_on x f g ->
target f = target g ->
restriction f x =
restriction g x.
Proof.
move=> ff fg [sf sg vfg] t.
move:(restriction_prop ff sf)(restriction_prop fg sg)=>[pa pb pc][pd pe pf].
apply: function_exten; fprops; try solve [rewrite /restriction; aw].
rewrite {1} /restriction; aw=> z zs.
by do 2 rewrite restriction_V => //; apply: vfg.
Qed.
Lemma agrees_same_restrictionC (a a' b x:Set) (f:a->b)(g:a'->b)
(Ha: sub x a)(Hb: sub x a'):
agreeC f g Ha Hb -> restrictionC f Ha =1 restrictionC g Hb.
Proof. move => ag z; apply: R_inj; apply: ag. Qed.
Lemma restriction_graph1 f x:
function f -> sub x (source f) ->
graph (restriction f x) = (graph f) \cap (x \times (target f)).
Proof.
rewrite /restriction => ff xs; aw.
set_extens t.
move/funI_P => [z pa ->].
have aux: inc (Vg (graph f) z) (target f) by rewrite -/(Vf _ _); Wtac.
apply:setI2_i => //.
rewrite -/(Vf _ _); Wtac.
apply/setX_P; aw;split; fprops.
move/setI2_P => [tg /setX_P [pa pb pc]]; apply /funI_P; ex_tac.
by apply: in_graph_Vf.
Qed.
Lemma restriction_recovers f x:
function f -> sub x (source f) ->
restriction f x = triple x (target f)
((graph f) \cap (x \times (target f))).
Proof.
move=> ff ss; rewrite -(restriction_graph1 ff ss).
rewrite /restriction; aw.
Qed.
Restriction of a function on the source and target
Lemma function_rest_of_prolongation f g:
extends g f -> f = restriction2 g (source f) (target f).
Proof.
move=>[ff fg].
rewrite (sub_function ff fg); move => [_ sts sg] st.
have au: (sub (image_by_fun g (source f)) (target f)).
by move =>t /(Vf_image_P fg sts) [u us ->]; rewrite - sg=>//; fprops.
have ax: (restriction2_axioms g (source f) (target f)) by red.
apply: function_exten;fprops; try solve [rewrite /restriction2; aw].
apply: (proj31 (restriction2_prop ax)).
by move => x sf /=; rewrite restriction2_V // sg.
Qed.
Definition restriction2C (a a' b b':Set) (f:a->b)(Ha:sub a' a)
(H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') :=
fun u=> Bo (H u).
Lemma restriction2C_pr (a a' b b':Set) (f:a->b)(Ha:sub a' a)
(H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') (x:a'):
Ro (restriction2C H x) = Vf (acreate f) (Ro x).
Proof.
rewrite /restriction2C B_eq; set (y:=inclusionC Ha x).
have RR: (Ro y = Ro x) by rewrite /y/inclusionC B_eq.
by rewrite -RR acreate_V.
Qed.
Lemma restriction2C_pr1 (a a' b b':Set) (f:a->b)
(Ha:sub a' a)(Hb:sub b' b)
(H: forall u:a', inc (Ro (f (inclusionC Ha u))) b'):
f \o (inclusionC Ha) =1 (inclusionC Hb) \o (restriction2C H).
Proof.
by move=> t; rewrite /restriction2C; apply: R_inj; rewrite B_eq B_eq.
Qed.
EII-3-6 Definition of a function by means of a term
Definition Lf f a b := triple a b (Lg a f).
Lemma lf_source f a b: source (Lf f a b) = a.
Proof. rewrite /Lf/Lg; aw. Qed.
Lemma lf_target f a b: target (Lf f a b) = b.
Proof. rewrite /Lf/Lg; aw. Qed.
Hint Rewrite lf_source lf_target : aw.
Lemma lf_graph1 f a b c:
inc c (graph (Lf f a b)) -> c = J (P c) (f (P c)).
Proof. rewrite/Lf/Lg; aw;move/funI_P;move=> [z _ ->]; aw. Qed.
Lemma lf_graph2 f a b c:
inc c a -> inc (J c (f c)) (graph (Lf f a b)).
Proof. by rewrite /Lf/Lg=> ca; aw; apply/funI_P; ex_tac. Qed.
Lemma lf_graph3 f a b c:
inc c (graph (Lf f a b)) -> inc (P c) a.
Proof. rewrite /Lf/Lg; aw; move/funI_P;move=> [z za ->]; aw. Qed.
Lemma lf_graph4 f a b c:
inc c (graph (Lf f a b)) -> f (P c) = (Q c).
Proof. move=> h; rewrite {2} (lf_graph1 h); aw. Qed.
In order for (Lf f a b) to be a function, the following must be satisfied
Definition lf_axiom f a b :=
forall c, inc c a -> inc (f c) b.
Lemma lf_function f a b:
lf_axiom f a b -> function (Lf f a b).
Proof.
move=> ta; apply: function_pr; bw; fprops.
by move=> t; rewrite Lg_range; move/funI_P=> [z zb ->]; apply: ta.
Qed.
Lemma lf_V f a b c: lf_axiom f a b -> inc c a -> Vf (Lf f a b) c = f c.
Proof.
by move=> /lf_function ff ca; symmetry; apply:Vf_pr => //; apply: lf_graph2.
Qed.
Hint Rewrite lf_V : aw.
Lemma lf_recovers f:
function f -> Lf (Vf f)(source f)(target f) = f.
Proof.
move=> ff.
have ta: (lf_axiom (Vf f) (source f) (target f)) by move=> x /=; fprops.
apply: function_exten;aw; [ by apply: lf_function | move => x sx /=; aw].
Qed.
Lemma identity_Lf x: identity x = Lf id x x.
Proof.
have aux: lf_axiom id x x by done.
apply function_exten; fprops; first by apply :lf_function.
move => t; rewrite lf_source => tx; aw; bw.
Qed.
Lemma resrtriction_Lf f x: function f -> sub x (source f) ->
restriction f x = Lf (Vf f) x (target f).
Proof.
move => h1 h2; move: (restriction_prop h1 h2) => [pa pb pc].
have pd: lf_axiom (Vf f) x (target f) by move => t tw; Wtac.
apply: function_exten; aw.
by rewrite /restriction;aw;move => t rs /=; aw; apply:restriction_V.
Qed.
Functions associated to P and Q
Definition first_proj g := Lf P g (domain g).
Definition second_proj g := Lf Q g (range g).
Lemma first_proj_V g: {inc g, Vf (first_proj g) =1 P}.
Proof. by rewrite /first_proj=> x xg; aw; move=>t; apply: domain_i1. Qed.
Lemma second_proj_V g: {inc g, Vf (second_proj g) =1 Q}.
Proof. by rewrite /second_proj=> x xg; aw; move=>t; apply: range_i2. Qed.
Lemma first_proj_f g: function (first_proj g).
Proof. by apply: lf_function; move=>t; apply: domain_i1. Qed.
Lemma second_proj_f g: function (second_proj g).
Proof. by apply: lf_function; move=>t; apply: range_i2. Qed.
Definition composable g f :=
[/\ function g, function f & source g = target f].
Notation "f1 \coP f2" := (composable f1 f2) (at level 50).
Lemma composable_pr f g: g \coP f -> (graph g) \cfP (graph f).
Proof.
by move=> [fg ff st]; split; fprops; aw; rewrite st; apply: f_range_graph.
Qed.
Lemma compf_graph:
{when: composable, {morph graph: f g / f \co g >-> f \cf g}}.
Proof.
move => a b cfg; move:(composable_pr cfg)=> ac.
by rewrite /compose compg_composef; aw.
Qed.
Lemma compf_domg g f: g \coP f->
domain (graph (g \co f)) = domain (graph f).
Proof.
move => cfg; rewrite compf_graph=>//;rewrite /composef; bw.
Qed.
Lemma compf_s f g: source (g \co f) = source f.
Proof. rewrite /compose; aw. Qed.
Lemma compf_t f g: target (g \co f) = target g.
Proof. rewrite /compose; aw. Qed.
Hint Rewrite compf_s compf_t : aw.
Proposition 6: composition of functions is a function
Theorem compf_f g f: g \coP f -> function (g \co f).
Proof.
move=> cgf;
have cd:=(compf_domg cgf).
have ac:=(composable_pr cgf).
have fgcc:= (composef_fgraph (graph g) (graph f)).
have cg := (compf_graph cgf); rewrite cg in cd.
move: cg; rewrite /compose; aw; move=> ->.
move: cgf => [fg ff etc].
apply: function_pr =>//.
apply: (@sub_trans (range (graph g))).
apply: composef_range => //.
by apply: f_range_graph.
by rewrite cd f_domain_graph.
Qed.
Definition of injectivity, surjectivity and bijectivity
Definition injection f:=
function f /\ {inc source f &, injective (Vf f)}.
Definition surjection f :=
function f /\
(forall y, inc y (target f) -> exists2 x, inc x (source f) & Vf f x = y).
Definition bijection f := injection f /\ surjection f.
We give here here some characterizations of injective, surjective,
bijective functions
Lemma inj_function f: injection f -> function f.
Proof. by case. Qed.
Lemma surj_function f: surjection f -> function f.
Proof. by case. Qed.
Lemma bij_function f: bijection f -> function f.
Proof. by case; case. Qed.
Lemma bij_inj f: bijection f -> {inc source f &, injective (Vf f)}.
Proof. move => h; exact: (proj2 (proj1 h)). Qed.
Lemma bij_surj f: bijection f ->
(forall y, inc y (target f) -> exists2 x, inc x (source f) & Vf f x = y).
Proof. move => h; exact: (proj2 (proj2 h)). Qed.
Ltac fct_tac :=
match goal with
| H:bijection ?X1 |- function ?X1 => exact (bij_function H)
| H:injection ?X1 |- function ?X1 => exact (inj_function H)
| H:surjection ?X1 |- function ?X1 => exact (surj_function H)
| H:function ?X1 |- correspondence ?X1 =>
by case H
| H:function ?g |- sub (range (graph ?g)) (target ?g)
=> apply: (f_range_graph H)
| H:composable ?X1 _ |- function ?X1 => destruct H as [H _ _]; exact H
| H:composable _ ?X1 |- function ?X1 => destruct H as [_ H _ ]; exact H
| H:composable ?f ?g |- function (compose ?f ?g ) =>
apply: (compf_f H)
| H:function ?f |- function (compose ?f ?g ) =>
apply: compf_f; split => //
| H:function ?g |- function (compose ?f ?g ) =>
apply: compf_f; split => //
| Ha:function ?f, Hb:function ?g |- ?f = ?g =>
apply: function_exten
end.
More properties of function composition
Lemma compf_V g f x: g \coP f ->
inc x (source f) -> Vf (g \co f) x = Vf g (Vf f x).
Proof.
rewrite /Vf => cgf xs; rewrite compf_graph=>//.
apply: composef_ev; aw; fct_tac.
Qed.
Hint Rewrite compf_V: aw.
Lemma composable_acreate (a b c:Set) (f: a-> b)(g: b->c):
(acreate g) \coP (acreate f).
Proof. rewrite/composable; aw; split;fprops. Qed.
Lemma compose_acreate (a b c:Set) (g: b->c)(f: a-> b):
(acreate g) \co (acreate f) = acreate (g \o f).
Proof.
have cfg:= (composable_acreate f g).
apply: function_exten; try fct_tac; fprops; aw.
by move=> x xa /=; aw; rewrite -(B_eq xa) 3! acreate_V.
Qed.
Lemma compfA f g h: f \coP g -> g \coP h ->
f \co (g \co h) = (f \co g) \co h.
Proof.
move=> cfg chg.
have [gg fh sgth]: g \coP h by [].
have ffg: (function (f \co g)) by fct_tac.
have fgh: (function (g \co h)) by fct_tac.
have cfgh: (f \co g) \coP h by hnf; aw.
have cfgh': (f \coP (g \co h)) by move: cfg=> [ff _ etc];hnf; aw.
apply: function_exten; try fct_tac; aw.
by move=> x xh /=; aw; rewrite sgth; fprops.
Qed.
Lemma compf_id_l m:
function m -> (identity (target m)) \co m = m.
Proof. move=>fm; apply: compf_id_left; fct_tac. Qed.
Lemma compf_id_r m:
function m -> m \co (identity (source m)) = m.
Proof. move=> fm; apply: compf_id_right; fct_tac. Qed.
Corollary fcomp_identity_left E:
{when (fun x => function x /\ (target x) = E),
left_id (identity E) compose}.
Proof. move => x [cx <-]; exact:compf_id_l. Qed.
Lemma injective_pr f y: injection f ->
singl_val (fun x => related (graph f) x y).
Proof.
rewrite /related;move=> [ff injf] x x' r1 r2; apply: injf.
- by Wtac.
- by Wtac.
- by rewrite - (Vf_pr ff r1) (Vf_pr ff r2).
Qed.
Lemma injective_pr3 f y: injection f ->
singl_val (fun x => inc (J x y) (graph f)).
Proof. apply: injective_pr. Qed.
Lemma injective_pr_bis f:
function f -> (forall y, singl_val (fun x => related (graph f) x y)) ->
injection f.
Proof.
move=> ff prop; hnf;split => //.
move=> x y xs ys Weq; apply: (prop (Vf f x) x y).
by apply: (Vf_pr3 ff xs).
by rewrite Weq; apply: (Vf_pr3 ff ys).
Qed.
Lemma surjective_pr0 f: surjection f -> image_of_fun f = target f.
Proof.
move=> [ff sj]; apply: extensionality; first by apply:(fun_image_Starget ff).
move => t tf; move: (sj _ tf) => [x xsf <-].
apply/dirim_P; ex_tac; Wtac.
Qed.
Lemma surjective_pr1 f: function f -> image_of_fun f = target f ->
surjection f.
Proof.
move=> ff ift; split => // y; rewrite -ift.
move/dirim_P=> [x pa pb];ex_tac; Wtac.
Qed.
Lemma surjective_pr f y:
surjection f -> inc y (target f) ->
exists2 x, inc x (source f) & related (graph f) x y .
Proof.
move => [ff h] ytf; move: (h _ ytf) => [x xsf <-]; ex_tac.
rewrite /related; Wtac.
Qed.
Lemma surjective_pr3 f: surjection f -> range (graph f) = target f.
Proof.
move => sf; rewrite -(surjective_pr0 sf) image_by_fun_source //; fct_tac.
Qed.
Lemma surjective_pr4 f:
function f -> range (graph f) = target f -> surjection f.
Proof.
move=> ff rg; apply surjective_pr1 => //.
rewrite image_by_fun_source //.
Qed.
Lemma surjective_pr5 f:
function f -> (forall y, inc y (target f) ->
exists2 x, inc x (source f) & related (graph f) x y) -> surjection f.
Proof.
move=> ff prop; split => // y yt; move: (prop _ yt) => [x xsf h]; ex_tac.
by symmetry; apply: Vf_pr.
Qed.
Lemma lf_injective f a b: lf_axiom f a b ->
(forall u v, inc u a-> inc v a -> f u = f v -> u = v) ->
injection (Lf f a b).
Proof.
move=> ta prop; split; first by apply: lf_function.
by aw; move=> x y xs ys/=; do 2 rewrite lf_V=>//; apply: prop.
Qed.
Lemma lf_surjective f a b: lf_axiom f a b ->
(forall y, inc y b -> exists2 x, inc x a & y = f x) ->
surjection (Lf f a b).
Proof.
move=> ta prop; split; first by apply: lf_function.
by aw; move=> y yt; case: (prop _ yt)=> x xa fy; ex_tac; rewrite lf_V.
Qed.
Lemma lf_bijective f a b: lf_axiom f a b ->
(forall u v, inc u a -> inc v a -> f u = f v -> u = v) ->
(forall y, inc y b -> exists2 x, inc x a & y = f x) ->
bijection (Lf f a b).
Proof.
by move => ta pi ps; split; [apply: lf_injective| apply: lf_surjective].
Qed.
Lemma bijective_pr f y:
bijection f -> inc y (target f) ->
exists! x, (inc x (source f) /\ Vf f x = y).
Proof.
move=> [[_ inj] [_ sf]] yt; apply /unique_existence; split.
by move: (sf _ yt)=> [x p1 p2]; exists x.
by move=> x x' [xs Wx] [x's Wx']; rewrite -Wx' in Wx; apply: inj.
Qed.
Lemma function_exten4 f g: source f = source g ->
surjection f -> surjection g -> {inc source f, f =1f g}
-> f = g.
Proof.
move=> sfg sf sg Weq.
have ff: function f by fct_tac.
have fg: function g by fct_tac.
have geq: (graph f = graph g) by apply: fgraph_exten; fprops; aw.
apply: function_exten1=>//.
by rewrite -(surjective_pr3 sf) -(surjective_pr3 sg) geq.
Qed.
Bijectivity of Coq functions
Definition injectiveC (a b:Set) (f:a->b) := forall u v, f u = f v -> u =v.
Definition surjectiveC (a b:Set) (f:a->b) := forall u, exists v, f v = u.
Definition bijectiveC (a b:Set) (f:a->b) := injectiveC f /\ surjectiveC f.
Definition right_inverseC (a b:Set) (f: a->b) (H:surjectiveC f) (v:b) :=
(chooseT (fun k:a => f k = v)
match H v with | ex_intro x _ => inhabits x end).
Definition inverseC (a b:Set) (f: a->b) (H:bijectiveC f)
:= right_inverseC (proj2 H).
Lemma bijectiveC_pr (a b:Set) (f:a->b) (y:b):
bijectiveC f -> exists! x:a, f x =y.
Proof.
move=> [fi fs]; apply /unique_existence; split; first by apply: fs.
by move=> x x' <-; move=> veq; symmetry; apply: fi.
Qed.
Lemma identityC_fb (x:Set): bijectiveC (@id x).
Proof. by split => // u; exists u. Qed.
Lemma composeC_inj (a b c:Set) (f:a->b)(f':b->c):
injectiveC f-> injectiveC f' -> injectiveC (f' \o f).
Proof. by move=> fi fi' x y p; apply: fi; apply: fi'.
Qed.
Lemma composeC_surj (a b c:Set) (f:a->b)(f':b->c):
surjectiveC f -> surjectiveC f' -> surjectiveC (f' \o f).
Proof.
move => sf sf' y.
move: (sf' y) => [w <-]; move: (sf w) => [z <-].
by exists z.
Qed.
Lemma composeC_bij (a b c:Set) (f:a->b)(f':b->c):
bijectiveC f -> bijectiveC f' -> bijectiveC (f' \o f).
Proof.
move=> [fi fs] [fi' fs'].
by split; [apply: composeC_inj| apply: composeC_surj ].
Qed.
Lemma right_inverse_pr (a b:Set) (f: a->b) (H:surjectiveC f) (x:b):
f (right_inverseC H x) = x.
Proof.
by rewrite /right_inverseC; apply:(chooseT_pr (p:= fun k : a => f k = x)).
Qed.
Section InverseProps.
Variables (A B: Set) (f: A -> B).
Hypothesis (H:bijectiveC f).
Lemma inverseC_prb (x: B): f ((inverseC H) x) = x.
Proof. apply: right_inverse_pr. Qed.
Lemma inverseC_pra (x: A): (inverseC H) (f x) = x.
Proof. exact: (proj1 H _ _ (inverseC_prb (f x))). Qed.
Lemma bij_left_inverseC: (inverseC H) \o f =1 @id A.
Proof. by move=> w; rewrite composeC_ev inverseC_pra. Qed.
Lemma bij_right_inverseC: f \o (inverseC H) =1 @id B.
Proof. by move=> t;rewrite composeC_ev inverseC_prb. Qed.
Lemma bijective_inverseC: bijectiveC (inverseC H).
Proof.
split.
by move=> x y sv; rewrite -(inverseC_prb x) -(inverseC_prb y) sv.
by move=> u; exists (f u); rewrite inverseC_pra.
Qed.
End InverseProps.
Lemma bijection_coq (a b: Set) (f:a->b):
bijective f <-> bijectiveC f.
Proof.
split.
move => [g ga gb]; split.
by move=> x x' feq; move: (f_equal g feq); rewrite 2! ga.
by move=> x; exists (g x).
move => H; exists (inverseC H).
apply: bij_left_inverseC.
apply: bij_right_inverseC.
Qed.
Lemma inverse_fun_involutiveC (a b:Set) (f:a->b) (H: bijectiveC f):
f =1 inverseC(bijective_inverseC H).
Proof.
move=> x;move: (bijective_inverseC H) => [i s]; apply: (i).
by rewrite inverseC_pra inverseC_prb.
Qed.
Lemma bcreate_fi f a b
(H:function f)(Ha:source f = a)(Hb:target f = b):
injection f -> injectiveC (bcreate H Ha Hb).
Proof.
move=> [ff fi] x y eql; apply: R_inj; apply: fi.
- by rewrite Ha; apply: R_inc.
- by rewrite Ha; apply: R_inc.
- by move: (f_equal (@Ro b) eql); rewrite 2! prop_bcreate2.
Qed.
Lemma bcreate_fs f a b
(H:function f)(Ha:source f = a)(Hb:target f = b):
surjection f -> surjectiveC (bcreate H Ha Hb).
Proof.
move=> [ff sf] u.
have Rt: (inc (Ro u) (target f)) by rewrite Hb; apply: R_inc.
have [x xs xv] := (sf _ Rt).
rewrite Ha in xs; exists (Bo xs).
by apply: R_inj; rewrite -xv prop_bcreate2 B_eq.
Qed.
Lemma bcreate_fb f a b
(H:function f)(Ha:source f =a)(Hb:target f =b):
bijection f -> bijectiveC (bcreate H Ha Hb).
Proof.
by move=> [fi fs];split ; [apply: bcreate_fi | apply: bcreate_fs].
Qed.
Lemma bcreate1_fi f (H:function f):
injection f -> injectiveC (bcreate1 H).
Proof.
by move=> fi x y; rewrite !(bcreate_eq H); apply: bcreate_fi.
Qed.
Lemma bcreate1_fs f (H:function f):
surjection f -> surjectiveC (bcreate1 H).
Proof.
move=> sf x.
move: (bcreate_fs H (refl_equal (source f)) (refl_equal (target f)) sf x).
by move => [v xsf]; exists v; rewrite -xsf -(bcreate_eq H).
Qed.
Lemma bcreate1_fb f (H:function f):
bijection f -> bijectiveC (bcreate1 H).
Proof.
by move=> [p1 p2];split; [ apply: bcreate1_fi | apply: bcreate1_fs].
Qed.
Lemma acreate_fi (a b:Set) (f:a->b):
injectiveC f -> injection (acreate f).
Proof.
move=> fi; split; first by fprops.
move=> x y; rewrite {1 2} /acreate; aw => xa ya.
rewrite -(B_eq xa) - (B_eq ya) (acreate_V f (Bo xa)) (acreate_V f (Bo ya)).
by move=> eq; move: (R_inj eq)=> eqv; rewrite (fi _ _ eqv).
Qed.
Lemma acreate_fs (a b:Set) (f:a->b):
surjectiveC f -> surjection (acreate f).
Proof.
move=> sf; split; fprops.
aw; move => y yb; move: (sf (Bo yb)) => [v fv].
by exists (Ro v); [by apply: R_inc | rewrite acreate_V fv B_eq].
Qed.
Lemma acreate_fb (a b:Set) (f:a->b):
bijectiveC f -> bijection (acreate f).
Proof.
by move=> [i j]; split; [ apply: acreate_fi| apply: acreate_fs].
Qed.
Equipotent means there is a bijection between the sets
Definition bijection_prop f s t :=
[/\ bijection f, source f = s & target f = t].
Definition surjection_prop f x y:=
[/\ surjection f, source f = x & target f = y].
Definition injection_prop f x y:=
[/\ injection f, source f = x & target f = y].
Definition equipotent x y :=
exists z, bijection_prop z x y.
Notation "x \Eq y" := (equipotent x y) (at level 50).
Lemma equipotentC x y: x \Eq y <-> exists f:x->y, bijectiveC f.
Proof.
split.
move=> [z [bz sz tz]].
have fz: (function z) by fct_tac.
by exists (bcreate fz sz tz); apply: bcreate_fb.
move=> [f bf]; exists (acreate f); split; [by apply: acreate_fb | aw | aw].
Qed.
Lemma equipotentR: reflexive_r equipotent.
Proof.
move => x;apply /equipotentC; exists (@id x); apply: identityC_fb.
Qed.
Hint Resolve equipotentR: fprops.
Lemma equipotentT: transitive_r equipotent.
Proof.
move => c b a /equipotentC [f bf] /equipotentC [g bg]; apply /equipotentC.
by exists (g \o f); apply: composeC_bij.
Qed.
Lemma equipotentS: symmetric_r equipotent.
Proof.
move => a b /equipotentC [f bf]; apply /equipotentC.
exists (inverseC bf); apply: bijective_inverseC.
Qed.
Ltac eqtrans u:= apply equipotentT with u; fprops.
Ltac eqsym:= apply: equipotentS.
Lemma equipotent_aux f a b:
bijection (Lf f a b) -> a \Eq b.
Proof. by move => h; exists (Lf f a b); rewrite /bijection_prop; aw; split. Qed.
Injectivity and surjectivity of identity and restriction
Lemma identity_fb x: bijection (identity x).
Proof. rewrite -identity_prop1; apply:acreate_fb; apply: identityC_fb. Qed.
Lemma restriction2_fi f x y:
injection f -> restriction2_axioms f x y
-> injection (restriction2 f x y).
Proof.
move=> [_ fi] ra; move: (ra) => [_ sf _].
move: (restriction2_prop ra) => [pa pb pc].
split => //; rewrite pb => a b ax bx.
by do 2 rewrite restriction2_V=>//; apply: fi; apply: sf.
Qed.
Lemma restriction2_fs f x y:
restriction2_axioms f x y ->
source f = x -> image_of_fun f = y ->
surjection (restriction2 f x y).
Proof.
move=> ra sf iy; move: (restriction2_prop ra) => [pa pb pc].
split => // z; rewrite pb pc - {1} iy - {1} sf.
move: (ra) => [ra1 _ _ _].
move /(Vf_image_P1 ra1)=> [u usf uv].
ex_tac; rewrite restriction2_V //; ue.
Qed.
Lemma restriction1_fs f x:
function f -> sub x (source f) ->
surjection (restriction1 f x).
Proof.
move=> ff sxs; move: (restriction1_prop ff sxs) => [pa pb pc].
split => //y; rewrite pb pc; move/(Vf_image_P ff sxs) => [b bx Jg].
ex_tac; bw; rewrite restriction1_V=> //.
Qed.
Lemma restriction1_fb f x:
injection f -> sub x (source f) ->
bijection (restriction1 f x).
Proof.
move=> [ff fi] sxf; split; last by apply: restriction1_fs.
move: (restriction1_prop ff sxf) => [pa pb pc].
split => //; rewrite pb => a b ax bx.
by do 2 rewrite restriction1_V=>//; apply: fi; apply: sxf.
Qed.
Lemma equipotent_restriction1 f x:
sub x (source f) -> injection f ->
x \Eq (image_by_fun f x).
Proof.
move=> wsf bf; rewrite /equipotent/bijection_prop.
exists (restriction1 f x); rewrite corresp_s corresp_t; split => //.
apply: restriction1_fb =>//; move: bf=>[]//.
Qed.
Lemma equipotent_range f: injection f ->
(source f) \Eq (range (graph f)).
Proof.
move=> injf; rewrite -image_by_fun_source; last by fct_tac.
apply: equipotent_restriction1 => //; fprops.
Qed.
Definition restriction_to_image f :=
restriction2 f (source f) (image_of_fun f).
Lemma restriction_to_image_axioms f: function f ->
restriction2_axioms f (source f) (image_of_fun f).
Proof. by move=> ff; split => //; apply :fun_image_Starget. Qed.
Lemma restriction_to_imageE f: function f ->
restriction_to_image f = restriction1 f (source f).
Proof. move => ff; rewrite - restriction1_pr //. Qed.
Lemma restriction_to_image_fs f: function f ->
surjection (restriction_to_image f).
Proof.
by move => h; rewrite (restriction_to_imageE h);apply: restriction1_fs.
Qed.
Lemma restriction_to_image_fb f: injection f ->
bijection (restriction_to_image f).
Proof.
by move => h; rewrite (restriction_to_imageE (proj1 h));apply: restriction1_fb.
Qed.
Lemma iim_fun_r f (h:=restriction_to_image f): function f ->
forall a, image_by_fun f a = inv_image_by_fun (inverse_fun h) a.
Proof.
move => ff a.
move: (proj1 (function_fgraph (proj1 (restriction_to_image_fs ff)))) => aux.
rewrite /inv_image_by_fun/image_by_fun /inverse_image.
rewrite corresp_g (igraph_involutive aux) corresp_g.
congr (direct_image _ a); symmetry;apply/setI2id_Pl.
by move: ff => [[_ p2 _] _].
Qed.
Extension of a function by adding f(x)=y
Definition extension f x y:=
triple ((source f) +s1 x) ((target f) +s1 y) ((graph f) +s1 (J x y)).
Lemma extension_injective x f g a b:
domain f = domain g -> ~ (inc x (domain f)) ->
(f +s1 (J x a) = g +s1 (J x b)) -> f = g.
Proof.
move=> seq nixsf sv.
set_extens t => tf.
have: inc t (g +s1 J x b) by rewrite - sv; fprops.
case /setU1_P => // ta;case: nixsf; apply /funI_P; ex_tac; rewrite ta;aw.
have: inc t (f +s1 J x a) by rewrite sv; fprops.
case /setU1_P => // ta.
case: nixsf; rewrite seq;apply /funI_P; ex_tac; rewrite ta;aw.
Qed.
Lemma restr_setU1 f x a:
fgraph f -> ~ (inc x (domain f)) ->
restr (f +s1 (J x a)) (domain f) = f.
Proof.
move=> fgf xdf; symmetry.
have aux: fgraph (f +s1 J x a) by apply:fgraph_setU1.
move: (domain_S(@subsetU2l f (singleton (J x a)))) => sd.
apply: fgraph_exten; [done | by apply: restr_fgraph | bw | move=> t tdf /=; bw].
by rewrite setU1_V_in.
Qed.
Lemma setU1_restr f x E: fgraph f -> ~ (inc x E) ->
domain f = E +s1 x->
(restr f E) +s1 (J x (Vg f x)) = f.
Proof.
move=> fgf nxE df.
have sEd: sub E (domain f) by rewrite df; fprops.
have dr: (domain (restr f E)) = E by rewrite restr_d =>//.
have fgr: fgraph (restr f E) by fprops.
have nxe: ~ inc x (domain (restr f E)) by ue.
apply: fgraph_exten =>//.
apply: fgraph_setU1 =>//.
by rewrite domain_setU1 dr df.
move=> u; rewrite domain_setU1 dr; case/setU1_P.
move=> uE.
have ud: inc u (domain (restr f E)) by rewrite dr.
rewrite setU1_V_in // restr_ev //.
move=> ->; rewrite setU1_V_out //.
Qed.
Section Extension.
Variables (f x y: Set).
Hypothesis (ff: function f) (xsf: ~ (inc x (source f))).
Lemma extension_f: function (extension f x y).
Proof.
rewrite /extension; apply: function_pr.
- apply: fgraph_setU1; fprops; aw.
- rewrite range_setU1 => t /setU1_P [] tr; apply/setU1_P;[left | by right].
by apply:f_range_graph.
- by rewrite domain_setU1 - (proj33 ff).
Qed.
Lemma extension_Vf_in: {inc (source f), (extension f x y) =1f f}.
Proof.
move=> u uf; symmetry; apply: Vf_pr; first by apply:extension_f.
rewrite /extension; aw; apply: setU1_r;Wtac.
Qed.
Lemma extension_Vf_out: Vf (extension f x y) x = y.
Proof.
symmetry;apply: Vf_pr; first by apply:extension_f.
rewrite /extension; aw; apply: setU1_1.
Qed.
Lemma extension_fs: surjection f -> surjection (extension f x y).
Proof.
move=> [_ sf].
split => //; first by apply:extension_f.
rewrite /extension; aw => z /setU1_P; case.
move=> zt; move: (sf _ zt)=> [u us wu].
by exists u; [fprops | rewrite extension_Vf_in].
by move =>->; exists x; fprops; rewrite extension_Vf_out.
Qed.
Lemma extension_restr:
restriction2 (extension f x y) (source f) (target f) = f.
Proof.
have pa: restriction2_axioms (extension f x y) (source f) (target f).
split.
- apply: extension_f.
- rewrite /extension; aw; fprops.
- rewrite /extension; aw; fprops.
- move => t /dirim_P [z zsf]; rewrite /extension;aw.
by case /setU1_P => h; [ Wtac | case: xsf; rewrite -(pr1_def h)].
move: (restriction2_prop pa) => [pb pc pd].
apply: function_exten => //; rewrite pc => t tx.
by rewrite (restriction2_V pa tx) (extension_Vf_in tx).
Qed.
End Extension.
Hint Resolve extension_f: fprops.
Lemma extension_f_injective x f g a b:
function f -> function g -> target f = target g ->
source f = source g -> ~ (inc x (source f)) ->
(extension f x a = extension g x b) -> f = g.
Proof.
move=> ff fg teq seq nixsf sv.
rewrite - (extension_restr a ff nixsf) sv seq teq extension_restr //; ue.
Qed.
Canonical injection of a set into a superset
Definition canonical_injection a b :=
triple a b (identity_g a).
Lemma inclusionC_fi a b (H: sub a b):
injectiveC (inclusionC H).
Proof.
move => x y si; apply: R_inj.
by rewrite - (inclusionC_pr H x) si (inclusionC_pr H y).
Qed.
Lemma canonical_injection_p1 a b (H:sub a b):
(canonical_injection a b) = acreate (inclusionC H).
Proof.
rewrite /acreate/canonical_injection; congr (triple a b _).
rewrite - diagonal_is_identity.
set_extens t.
move/diagonal_i_P => [pt pa pq]; apply/IM_P; rewrite -pt -pq.
by exists (Bo pa); rewrite inclusionC_pr B_eq.
move /IM_P => [x <-]; rewrite inclusionC_pr;apply/diagonal_pi_P.
split => //; apply:R_inc.
Qed.
Lemma ci_fi a b: sub a b -> injection (canonical_injection a b).
Proof.
move => h; rewrite canonical_injection_p1.
apply:acreate_fi; apply:inclusionC_fi.
Qed.
Lemma ci_f a b: sub a b -> function (canonical_injection a b).
Proof. move => h; exact (proj1 (ci_fi h)). Qed.
Hint Resolve ci_f : fprops.
Lemma ci_V a b x:
sub a b -> inc x a -> Vf (canonical_injection a b) x = x.
Proof.
by rewrite /Vf /canonical_injection=> ab xa; aw; apply: identity_ev.
Qed.
Lemma ci_range a b: sub a b ->
range (graph (canonical_injection a b)) = a.
Proof. by rewrite /canonical_injection=> ab; aw; rewrite identity_r.
Qed.
triple a b (identity_g a).
Lemma inclusionC_fi a b (H: sub a b):
injectiveC (inclusionC H).
Proof.
move => x y si; apply: R_inj.
by rewrite - (inclusionC_pr H x) si (inclusionC_pr H y).
Qed.
Lemma canonical_injection_p1 a b (H:sub a b):
(canonical_injection a b) = acreate (inclusionC H).
Proof.
rewrite /acreate/canonical_injection; congr (triple a b _).
rewrite - diagonal_is_identity.
set_extens t.
move/diagonal_i_P => [pt pa pq]; apply/IM_P; rewrite -pt -pq.
by exists (Bo pa); rewrite inclusionC_pr B_eq.
move /IM_P => [x <-]; rewrite inclusionC_pr;apply/diagonal_pi_P.
split => //; apply:R_inc.
Qed.
Lemma ci_fi a b: sub a b -> injection (canonical_injection a b).
Proof.
move => h; rewrite canonical_injection_p1.
apply:acreate_fi; apply:inclusionC_fi.
Qed.
Lemma ci_f a b: sub a b -> function (canonical_injection a b).
Proof. move => h; exact (proj1 (ci_fi h)). Qed.
Hint Resolve ci_f : fprops.
Lemma ci_V a b x:
sub a b -> inc x a -> Vf (canonical_injection a b) x = x.
Proof.
by rewrite /Vf /canonical_injection=> ab xa; aw; apply: identity_ev.
Qed.
Lemma ci_range a b: sub a b ->
range (graph (canonical_injection a b)) = a.
Proof. by rewrite /canonical_injection=> ab; aw; rewrite identity_r.
Qed.
if h is constant h = g \co f, where the target of f is a singleton
Lemma constant_function_pr2 x h:
inc x (source h) -> constantfp h ->
exists g f,
[/\ g \coP f, h = g \co f, surjection f & singletonp (target f)].
Proof.
move=> xs [fh p]; set (y := Vf h x).
have ssyth: sub (singleton y) (target h).
by move=> t /set1_P ->; rewrite /y; fprops.
set (g:= canonical_injection (singleton y) (target h)); exists g.
have ysy: inc y (singleton y) by fprops.
set (f:= constant_function (source h) ysy); exists f.
have st: (singletonp (target f)) by rewrite /f constant_t; exists y.
have ff: function f by apply: constant_f.
have tf: target f = (singleton y) by rewrite constant_t.
have sf: source f = source h by rewrite constant_s.
have sj: surjection f.
split=>//; rewrite /f tf; move =>z /set1_P ->.
by exists x; rewrite ?sf ?constant_V.
have c: g \coP f.
red;rewrite /f /g; split; fprops.
by rewrite tf /canonical_injection; aw.
split => //; apply: function_exten;aw; fprops; try fct_tac.
by rewrite /g /canonical_injection; aw.
move=> z zh /=; aw; last (by ue);rewrite (p _ _ zh xs) /f constant_V // ci_V //.
Qed.
Lemma constant_function_pr3 (a:Set) (h:a->Set) (x:a):
constantp h ->
exists f: a-> singleton (Ro x), exists g:singleton (Ro x)->Set,
(forall u:a, h u = g (f u)) /\ (g (Bo (set1_1 (Ro x))) = h x).
Proof.
move=> ch.
exists (fun u=> (Bo (set1_1 (Ro x)))).
by exists (fun t:singleton (Ro x) => h x).
Qed.
inc x (source h) -> constantfp h ->
exists g f,
[/\ g \coP f, h = g \co f, surjection f & singletonp (target f)].
Proof.
move=> xs [fh p]; set (y := Vf h x).
have ssyth: sub (singleton y) (target h).
by move=> t /set1_P ->; rewrite /y; fprops.
set (g:= canonical_injection (singleton y) (target h)); exists g.
have ysy: inc y (singleton y) by fprops.
set (f:= constant_function (source h) ysy); exists f.
have st: (singletonp (target f)) by rewrite /f constant_t; exists y.
have ff: function f by apply: constant_f.
have tf: target f = (singleton y) by rewrite constant_t.
have sf: source f = source h by rewrite constant_s.
have sj: surjection f.
split=>//; rewrite /f tf; move =>z /set1_P ->.
by exists x; rewrite ?sf ?constant_V.
have c: g \coP f.
red;rewrite /f /g; split; fprops.
by rewrite tf /canonical_injection; aw.
split => //; apply: function_exten;aw; fprops; try fct_tac.
by rewrite /g /canonical_injection; aw.
move=> z zh /=; aw; last (by ue);rewrite (p _ _ zh xs) /f constant_V // ci_V //.
Qed.
Lemma constant_function_pr3 (a:Set) (h:a->Set) (x:a):
constantp h ->
exists f: a-> singleton (Ro x), exists g:singleton (Ro x)->Set,
(forall u:a, h u = g (f u)) /\ (g (Bo (set1_1 (Ro x))) = h x).
Proof.
move=> ch.
exists (fun u=> (Bo (set1_1 (Ro x)))).
by exists (fun t:singleton (Ro x) => h x).
Qed.
Diagonal application, maps x to J x x
Definition diagonal_application a :=
Lf (fun x=> J x x) a (coarse a).
Lemma diag_app_V a x:
inc x a -> Vf (diagonal_application a) x = J x x.
Proof.
by rewrite /diagonal_application /coarse=> xa;aw; move=> y/=; fprops.
Qed.
Lemma diag_app_fi a: injection (diagonal_application a).
Proof.
rewrite /diagonal_application/coarse; apply: lf_injective.
by move=> y /=; fprops.
by move => u v _ _; apply: pr1_def.
Qed.
Lemma diag_app_f a: function (diagonal_application a).
Proof. by case: (diag_app_fi a). Qed.
Lemma diag_app_range a:
range (graph (diagonal_application a)) = diagonal a.
Proof.
rewrite /diagonal_application.
set_extens t;rewrite /Lf corresp_g; aw.
by move/Lg_range_P => [b ba ->]; apply/diagonal_pi_P.
move/diagonal_i_P => [pt ta pq]; apply/Lg_range_P; ex_tac.
by rewrite {2} pq pt.
Qed.
Injectivity and surjectivity of P and Q
Lemma second_proj_fs g: surjection (second_proj g).
Proof.
split; first by apply: second_proj_f.
rewrite /second_proj /range/Lf /Vf; aw.
move => y /funI_P [z zg ->]; ex_tac; bw.
Qed.
Lemma first_proj_fs g: surjection (first_proj g).
Proof.
split; first by apply: first_proj_f.
rewrite /first_proj /domain/Lf/Vf; aw.
move => y /funI_P [z zg ->]; ex_tac; bw.
Qed.
Lemma first_proj_fi g:
sgraph g -> (injection (first_proj g) <-> functional_graph g).
Proof.
move=> gg.
have fpf: (function (first_proj g)) by apply: first_proj_f.
have Ht: source (first_proj g) = g by rewrite/first_proj; aw.
rewrite /injection Ht.
split.
move=> [_ hyp] a b b'; rewrite /related => i1 i2.
suff: (J a b = J a b') by apply: pr2_def.
by apply: hyp=>//; rewrite first_proj_V=>//; rewrite first_proj_V=>//; aw.
split=>//; move=>x y xg yg/=; do 2 rewrite first_proj_V=>//.
have [_]: fgraph g by apply /functionalP.
by apply.
Qed.
The function that maps J x y to J y x
Lemma inv_graph_canon_fb g: sgraph g ->
bijection ( Lf (fun x=> J (Q x) (P x)) g (inverse_graph g)).
Proof.
move => gg; apply: lf_bijective.
by move=> c cg /=; apply/igraph_pP; rewrite /related (gg _ cg).
move=> u v ug vg peq; apply: pair_exten; try apply: gg=>//.
by apply: (pr2_def peq).
by apply: (pr1_def peq).
by move=> y /igraphP [py pg]; ex_tac;aw; rewrite py.
Qed.
Lemma equipotent_product_sym a b:
(a \times b) \Eq (b \times a).
Proof.
have pa: sgraph (a \times b) by fprops.
move: (inv_graph_canon_fb pa); aw; apply: equipotent_aux.
Qed.
Lemma equipotent_indexed a b: a \Eq (a *s1 b).
Proof.
rewrite /indexed.
apply: (@equipotent_aux (fun x=> J x b)); apply: lf_bijective.
- by move=> x xa /=; aw; fprops.
- by move=> u v _ _; apply: pr1_def.
- move=> y /setX_P [py pya /set1_P <-]; ex_tac; aw.
Qed.
Hint Resolve equipotent_indexed: fprops.
Lemma equipotent_rindexed a b:
a \Eq (indexedr b a).
Proof.
eqtrans (a *s1 b); fprops; apply: equipotent_product_sym.
Qed.
Lemma equipotent_source_graph f: function f ->
(graph f) \Eq (source f).
Proof.
move=> ff; eqsym.
apply: (equipotent_aux (f:= (fun z => J z (Vf f z)))); apply: lf_bijective.
move=> z jz; simpl;Wtac.
move=> u v _ _ aux; exact (pr1_def aux).
move=> y yG; move: (p1graph_source1 ff yG) => pa; ex_tac.
apply: in_graph_V => //; fprops.
Qed.
Proposition 7 summarizes next two theorems. Let f be a function; then
f is a bijection if and only if its inverse is a function
Theorem bijective_inv_f f:
bijection f -> function (inverse_fun f).
Proof.
rewrite /inverse_fun; move => [fi fs].
have gf: (sgraph (graph f)) by move: fi=> [ff _]; fprops.
have fgf: fgraph (inverse_graph (graph f)).
split; fprops; move=> x y/igraphP [px pf]/igraphP [qx qf] peq.
apply: pair_exten =>//.
by rewrite -peq in qf; apply: (injective_pr3 fi pf qf).
apply: function_pr=>//.
by rewrite igraph_range=>//; aw; fprops; fct_tac.
by symmetry; rewrite igraph_domain =>//; apply: surjective_pr3.
Qed.
Theorem inv_function_fb f:
function f -> function (inverse_fun f) -> bijection f.
Proof.
move=> ff fif.
split.
apply: injective_pr_bis=>//; move=> x x' y.
move/igraph_pP;rewrite -ifun_g => r1 ;move/igraph_pP; rewrite -ifun_g=> r2.
by move: fif => [_ fg _ ]; apply: (fgraph_pr fg r1 r2).
apply: surjective_pr4=> //; rewrite - igraph_domain; fprops.
by rewrite -ifun_g /inverse_fun; aw.
Qed.
Lemma inverseC_prc (a b:Set) (f:a-> b) (H:bijectiveC f):
inverse_fun (acreate f) = acreate(inverseC H).
Proof.
move: (acreate_fb H) => ab.
apply: function_exten.
- by apply: bijective_inv_f.
- by fprops.
- by rewrite/acreate; aw.
- by rewrite/acreate; aw.
move => x; aw => xb.
have [y eq]: exists y:a, f y = (Bo xb) by apply: (proj2 H).
set g := (acreate (inverseC H)).
have ta: a = target (acreate (inverseC H)) by rewrite acreate_target.
set u := Vf g x.
have: x = Vf (acreate f) u.
by rewrite /u - {2} (B_eq xb) - eq acreate_V inverseC_pra acreate_V eq B_eq.
move => h; symmetry;apply: Vf_pr; first by apply: bijective_inv_f.
rewrite /inverse_fun; aw; apply /igraph_pP; rewrite h; apply: Vf_pr3 => //.
fct_tac.
aw; rewrite /u ta; apply: Vf_target; first by apply: acreate_function.
by rewrite acreate_source.
Qed.
Lemma bijective_double_inverseC (a b:Set) (f:a->b) g g':
g \o f =1 @id a -> f \o g' =1 @id b ->
bijectiveC f.
Proof.
move=> c1 c2; split.
move=> x x' feq; move: (f_equal g feq); rewrite -!(composeC_ev g f) !c1 //.
move=> x; exists (g' x); rewrite -!(composeC_ev f g') c2 //.
Qed.
Lemma bijective_double_inverseC1 (a b:Set) (f:a->b) g g'
(Ha: g \o f =1 @id a)(Hb: f \o g' =1 @id b):
g =1 inverseC (bijective_double_inverseC Ha Hb)
/\ g' =1 inverseC (bijective_double_inverseC Ha Hb).
Proof.
have sg: (g' =1 g).
by move=> x; rewrite -{1} (Ha (g' x)) -{2} (Hb x) !composeC_ev.
set h := inverseC _.
have gh: (g' =1 h).
move => x; have e1: (f (g' x) = x) by apply: (Hb x).
by rewrite /h -{2} e1 inverseC_pra.
by split =>//; apply: ftrans gh.
Qed.
Properties of the inverse of a bijection
Lemma ifun_involutive: {when function, involutive inverse_fun}.
Proof. move=> f ff;apply:icor_involutive; fct_tac. Qed.
Lemma inverse_bij_fb f:
bijection f -> bijection (inverse_fun f).
Proof.
move=> bf;move: (bijective_inv_f bf)=> bif.
have ff:function f by fct_tac.
apply: inv_function_fb => //; rewrite ifun_involutive //.
Qed.
Lemma composable_f_inv f: bijection f -> f \coP (inverse_fun f).
Proof.
move=> bf.
have fif: (function (inverse_fun f)) by apply: bijective_inv_f.
split;[fct_tac | done | aw].
Qed.
Lemma composable_inv_f f: bijection f -> (inverse_fun f) \coP f.
Proof.
move=> bf.
have fif: function (inverse_fun f) by apply: bijective_inv_f.
split; [ done | fct_tac | aw].
Qed.
Lemma acreate_exten (a b: Set) (f g: a-> b):
f =1 g -> acreate f = acreate g.
Proof.
move=> h; apply: function_exten; fprops; aw.
by move=> x [z za]; rewrite -za ! acreate_V h.
Qed.
Lemma bij_right_inverse f:
bijection f -> f \co (inverse_fun f) = identity (target f).
Proof.
move=> bf.
move: (refl_equal (source f)) (refl_equal (target f))=> ss tt.
rewrite -(identity_prop1 (target f)).
have ff := (bij_function bf).
rewrite - (bcreate_inv2 ff ss tt) acreate_target
(inverseC_prc (bcreate_fb ff ss tt bf)) compose_acreate.
apply: acreate_exten; move=> t.
by rewrite (bij_right_inverseC (bcreate_fb ff ss tt bf)) //.
Qed.
Lemma bij_left_inverse f:
bijection f -> (inverse_fun f) \co f = identity (source f).
Proof.
move=> bf.
move: (refl_equal (source f)) (refl_equal (target f))=> ss tt.
rewrite -(identity_prop1 (source f)).
have ff := (bij_function bf).
rewrite - (bcreate_inv2 ff ss tt).
rewrite (inverseC_prc (bcreate_fb ff ss tt bf))
acreate_source compose_acreate ;apply: acreate_exten.
by move=> t; rewrite bij_left_inverseC.
Qed.
Lemma compf_lK f g : bijection g -> g \coP f ->
(inverse_fun g) \co (g \co f) = f.
Proof.
move => bg cop.
have co1 := (composable_inv_f bg).
rewrite (compfA co1 cop) (bij_left_inverse bg).
by move: cop => [s1 s2 ->]; rewrite (compf_id_l s2).
Qed.
Lemma compf_rK f g : bijection g -> f \coP g ->
(f \co g) \co (inverse_fun g) = f.
Proof.
move => bg cop.
move: (composable_f_inv bg) => co1.
rewrite -(compfA cop co1) (bij_right_inverse bg).
by move: cop => [s1 s2 s3]; rewrite - s3 (compf_id_r s1).
Qed.
Lemma compf_regl f f' g : bijection g ->
f \coP g -> f' \coP g -> f \co g = f' \co g -> f = f'.
Proof.
move => bg pa pb pc.
by rewrite - (compf_rK bg pa) - (compf_rK bg pb) pc.
Qed.
Lemma compf_regr f f' g : bijection g ->
g \coP f -> g \coP f' -> g \co f = g \co f' -> f = f'.
Proof.
move => bg pa pb pc.
by rewrite - (compf_lK bg pa) - (compf_lK bg pb) pc.
Qed.
Lemma inverse_V f x:
bijection f -> inc x (target f) ->
Vf f (Vf (inverse_fun f) x) = x.
Proof.
move=> bf xt; symmetry.
transitivity (Vf (identity (target f)) x); first by bw.
by rewrite -(bij_right_inverse bf); aw; apply: composable_f_inv.
Qed.
Lemma inverse_V2 f y:
bijection f -> inc y (source f) ->
Vf (inverse_fun f) (Vf f y) = y.
Proof.
move=> bf ys; symmetry.
transitivity (Vf (identity (source f)) y); first by bw.
by rewrite -(bij_left_inverse bf); aw; apply: composable_inv_f.
Qed.
Lemma inverse_Vis f x:
bijection f -> inc x (target f) -> inc (Vf (inverse_fun f) x) (source f).
Proof.
move=> bf xt.
have: source f= (target (inverse_fun f)) by aw.
move=>->; apply: Vf_target; aw; apply: (proj1(proj1(inverse_bij_fb bf))).
Qed.
Properties of direct and inverse images
Lemma sub_inv_im_source f y:
function f -> sub y (target f) ->
sub (inv_image_by_fun f y) (source f).
Proof. by move=> ff yt t /iim_graph_P [u uy Jg]; Wtac. Qed.
Lemma direct_inv_im f y:
function f -> sub y (target f) ->
sub (image_by_fun f (image_by_fun (inverse_fun f) y)) y.
Proof.
move=> ff yt x.
have aux: sub (image_by_fun (inverse_fun f) y) (source f).
by rewrite /inverse_fun/image_by_fun; aw; apply: sub_inv_im_source.
move/(Vf_image_P ff aux) =>[u /dirim_P [z zy /igraph_pP]].
by rewrite - ifun_g (ifun_involutive ff) => xx ->; rewrite -(Vf_pr ff xx).
Qed.
Lemma nonempty_image f x:
function f -> nonempty x -> sub x (source f) ->
nonempty (image_by_fun f x).
Proof.
move=> ff [z zx] xf; exists (Vf f z); apply/dirim_P; ex_tac; Wtac.
Qed.
Lemma direct_inv_im_surjective f y:
surjection f -> sub y (target f) ->
(image_by_fun f (image_by_fun (inverse_fun f) y)) = y.
Proof.
move=> [ff sf] yt.
apply: extensionality; first by apply: direct_inv_im.
move=> x xs; rewrite -iim_fun_pr.
apply/Vf_image_P =>//; first by apply: sub_inv_im_source.
have [u us Jg] := (sf _ (yt _ xs)).
exists u=>//;apply/iim_fun_P; ex_tac;rewrite - Jg; Wtac.
Qed.
Lemma inverse_direct_image f x:
function f -> sub x (source f) ->
sub x (image_by_fun (inverse_fun f) (image_by_fun f x)).
Proof.
move=> ff sxf t tx.
apply/dirim_P; exists (Vf f t).
by apply/Vf_image_P => //; ex_tac.
rewrite ifun_g; apply/igraph_pP; Wtac.
Qed.
Lemma inverse_direct_image_inj f x:
injection f -> sub x (source f) ->
x = (image_by_fun (inverse_fun f) (image_by_fun f x)).
Proof.
move=> [ff fi] xsf.
apply: extensionality; first by apply: inverse_direct_image.
rewrite -iim_fun_pr => y /iim_graph_P [u ui Jg].
move /(Vf_image_P ff xsf): ui => [v vx]; rewrite (Vf_pr ff Jg) => Vv.
symmetry in Vv.
by rewrite - (fi _ _ (xsf _ vx) (p1graph_source ff Jg) Vv).
Qed.
Definition is_left_inverse f r:=
r \coP f /\ r \co f = identity (source f).
Definition is_right_inverse f s:=
f \coP s /\ f \co s = identity (target f).
Definition is_left_inverseC (a b:Set) (f:a->b) r := r \o f =1 @id a.
Definition is_right_inverseC (a b:Set) (f:a->b) s:= f \o s =1 @id b.
Lemma left_i_target f r: is_left_inverse f r -> target r = source f.
Proof. by move=> [_ c]; move: (f_equal target c); aw. Qed.
Lemma left_i_source f r: is_left_inverse f r -> source r = target f.
Proof. by move=> [[_ [_ c] _]]. Qed.
Lemma right_i_source f s: is_right_inverse f s -> source s = target f.
Proof. by move=> [_ h]; move: (f_equal source h); aw. Qed.
Lemma right_i_target f s: is_right_inverse f s -> target s = source f.
Proof. by move=> [[_ [_ c] _]]. Qed.
Lemma right_i_V f s x:
is_right_inverse f s -> inc x (target f) -> Vf f (Vf s x) = x.
Proof.
move=> rsf xtf; move: (xtf);rewrite - (right_i_source rsf).
move: rsf=> [csf c] xs;rewrite - compf_V // c; bw.
Qed.
Lemma left_i_V f r x:
is_left_inverse f r -> inc x (source f) -> Vf r (Vf f x) = x.
Proof. move=> [ltf c] xsf; rewrite- compf_V // c; bw. Qed.
Lemma right_i_v (a b:Set) (f:a->b) s (x:b):
is_right_inverseC f s -> f (s x) = x.
Proof. by move=> e; move: (e x); rewrite composeC_ev. Qed.
Lemma left_i_v (a b:Set) (f:a->b) r (x:a):
is_left_inverseC f r -> r (f x) = x.
Proof. by move=> e; move: (e x); rewrite composeC_ev. Qed.
Proposition 8 concerns the next 4 theorems; it is the link between injectivity, surjectivity and existence of left and right inverse
Lemma inj_if_exists_left_invC (a b:Set) (f:a-> b):
(exists r, is_left_inverseC f r) -> injectiveC f.
Proof.
move=> [r ilr] x x'.
by move /(congr1 r); move: (ilr x) (ilr x') => /= -> ->.
Qed.
Lemma surj_if_exists_right_invC (a b:Set) (f:a->b):
(exists s, is_right_inverseC f s) -> surjectiveC f.
Proof.
by move=> [s rsf] u; exists (s u); rewrite (right_i_v u rsf).
Qed.
Theorem inj_if_exists_left_inv f:
(exists r, is_left_inverse f r) -> injection f.
Proof.
move=> [r lrf]; split; first by move: lrf => [ cp _ ]; fct_tac.
move=> x y xs ys sv.
by rewrite - (left_i_V lrf xs) - (left_i_V lrf ys) sv.
Qed.
Theorem surj_if_exists_right_inv f:
(exists s, is_right_inverse f s) -> surjection f.
Proof.
move=> [s rsf]; move: (rsf) => [cp _]; move: (cp) =>[ff fs ss].
split => // y yt; exists (Vf s y).
rewrite -(right_i_source rsf) in yt; rewrite ss; fprops.
by rewrite (right_i_V rsf yt).
Qed.
Left inverse for an injective function (f: a->b)
Definition left_inverseC (a b:Set) (f: a->b)(H:inhabited a)
(v:b) := (chooseT (fun u:a => (~ (exists x:a, f x = v)) \/ (f u = v)) H).
Lemma left_inverseC_pr (a b:Set) (f: a->b) (H:inhabited a) (u:a):
f (left_inverseC f H (f u)) = f u.
Proof.
rewrite /left_inverseC.
set p:= fun u:a => _.
have: (p (chooseT p H)) by apply: chooseT_pr; exists u; right.
case=>//; by case; exists u.
Qed.
Lemma left_inverse_comp_id (a b:Set) (f:a->b) (H:inhabited a):
injectiveC f -> (left_inverseC f H) \o f =1 @id a.
Proof.
move => fi t; apply fi; rewrite composeC_ev;apply: left_inverseC_pr.
Qed.
Lemma exists_left_inv_from_injC (a b:Set) (f:a->b): inhabited a ->
injectiveC f -> exists r, is_left_inverseC f r.
Proof.
move=> H fi; exists (left_inverseC f H); by apply: left_inverse_comp_id.
Qed.
Lemma right_inverse_comp_id (a b:Set) (f:a-> b) (H:surjectiveC f):
f \o (right_inverseC H) =1 @id b.
Proof. move=> x; rewrite composeC_ev;apply: right_inverse_pr. Qed.
Lemma exists_right_inv_from_surjC (a b:Set)(f:a-> b) (H:surjectiveC f):
exists s, is_right_inverseC f s.
Proof. exists (right_inverseC H); apply: right_inverse_comp_id. Qed.
Existence of left and right inverse for Bourbaki functions
Theorem exists_left_inv_from_inj f:
injection f -> nonempty (source f) -> exists r, is_left_inverse f r.
Proof.
move=> fi nesf; move: (inj_function fi) => ff.
move: (bcreate1_fi (H:=ff) fi)=>ib.
have nesf0: inhabited (source f).
by move: nesf => [y [w _]]; apply: inhabits.
case: (exists_left_inv_from_injC nesf0 ib) => x px.
move: (compose_acreate x (bcreate1 ff));rewrite bcreate_inv1 => aux.
exists (acreate x).
split; first by split; fprops; aw.
rewrite aux;apply: function_exten; fprops; aw.
move=> u usf /=; rewrite identity_V //.
by move: usf => [v vs];rewrite -vs acreate_V px.
Qed.
Theorem exists_right_inv_from_surj f:
surjection f -> exists s, is_right_inverse f s.
Proof.
move=> sf.
move:(surj_function sf)=> ff; move: (bcreate1_fs ff sf)=> bs.
move:(exists_right_inv_from_surjC bs)=> [s ris].
move:(compose_acreate (bcreate1 ff) s); rewrite bcreate_inv1 => aux.
exists (acreate s); split; first by red; split; aw;fprops.
rewrite aux;apply: function_exten; fprops; aw.
move=> u usf /=; rewrite identity_V //.
by move: usf => [v vs];rewrite -vs acreate_V ris.
Qed.
If compositions in both order are the identity, then the functions are bijections
Lemma bijective_from_compose g f:
g \coP f -> f \coP g -> g \co f = identity (source f)
-> f \co g = identity (source g)
-> [/\ bijection f, bijection 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; red; rewrite -teq.
split=>//.
by split=>//; apply: surj_if_exists_right_inv; exists f; red; rewrite - seq.
symmetry.
move: (bijective_inv_f bf)=>fif.
symmetry;apply: function_exten=>//; aw; first by ue.
move=> x xs; apply: Vf_pr=>//; aw; apply/igraph_pP.
have aux : (x = Vf f (Vf g x)).
by rewrite - compf_V=>//;rewrite cfgi identity_V =>//.
rewrite {2} aux; Wtac; rewrite seq; Wtac.
Qed.
More links between left inverse and right inverse
Lemma right_inverse_from_leftC (a b:Set) (r:b->a)(f:a->b):
is_left_inverseC f r -> is_right_inverseC r f.
Proof. trivial. Qed.
Lemma left_inverse_from_rightC (a b:Set) (s:b->a)(f:a->b):
is_right_inverseC f s -> is_left_inverseC s f.
Proof. trivial. Qed.
Lemma left_inverse_surjectiveC (a b:Set) (r:b->a)(f:a->b):
is_left_inverseC f r -> surjectiveC r.
Proof. by move=> h; apply: surj_if_exists_right_invC; exists f. Qed.
Lemma right_inverse_injectiveC (a b:Set) (s:b->a)(f:a->b):
is_right_inverseC f s -> injectiveC s.
Proof. move=> h; apply: inj_if_exists_left_invC; by exists f. Qed.
Lemma section_uniqueC (a b:Set) (f:a->b)(s:b->a)(s':b->a):
is_right_inverseC f s -> is_right_inverseC f s' ->
(forall x:a, (exists u:b, x = s u) = (exists u':b, x = s' u')) ->
s =1 s'.
Proof.
move=> r1 r2 sp x.
have [u' eql]: (exists u' : b, s x = s' u') by rewrite- (sp (s x)); exists x.
move: (f_equal f eql); rewrite (right_i_v x r1) (right_i_v u' r2).
by rewrite eql; move=>->.
Qed.
Lemma right_inverse_from_left f r:
is_left_inverse f r -> is_right_inverse r f.
Proof. by move=> [c e];red; 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]; red; 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.
Lemma left_inverse_composeC (a b c:Set)
(f:a->b) (f':b->c)(r:b->a)(r':c->b):
is_left_inverseC f' r' -> is_left_inverseC f r ->
is_left_inverseC (f' \o f) (r \o r').
Proof.
move=> le' le x;rewrite !composeC_ev.
by rewrite (left_i_v (f x) le') (left_i_v x le).
Qed.
Lemma right_inverse_composeC (a b c:Set)
(f:a->b) (f':b->c)(s:b->a)(s':c->b):
is_right_inverseC f' s' -> is_right_inverseC f s ->
is_right_inverseC (f' \o f) (s \o s') .
Proof.
move=> ri' ri x ;rewrite !composeC_ev (right_i_v (s' x) ri) (right_i_v x ri').
done.
Qed.
Lemma inj_right_composeC (a b c:Set) (f:a->b) (f':b->c):
injectiveC (f' \o f) -> injectiveC f.
Proof. by move=> ci x y sv; apply: ci; rewrite !composeC_ev sv. Qed.
Lemma surj_left_composeCl (a b c:Set) (f:a->b) (f':b->c):
surjectiveC (f' \o f) -> surjectiveC f'.
Proof.
by move=> sc x; move: (sc x)=> [y <-]; exists (f y). Qed.
Lemma surj_left_compose2C (a b c:Set) (f:a->b) (f':b->c):
surjectiveC (f' \o f) -> injectiveC f' -> surjectiveC f.
Proof.
move => sc if' x.
by move: (sc (f' x)) => [y sv]; exists y; apply: if'.
Qed.
Lemma inj_left_compose2C (a b c:Set) (f:a->b) (f':b->c):
injectiveC (f' \o f) -> surjectiveC f -> injectiveC f'.
Proof.
move=> ic sf x x' sv.
move: (sf x) => [y yv]; move: (sf x') => [y' y'v].
have: (y = y') by apply: ic; rewrite !composeC_ev yv y'v sv.
by rewrite -yv -y'v; move=>->.
Qed.
Lemma left_inv_compose_rfC (a b c:Set) (f:a->b) (f':b->c)(r'': c->a):
is_left_inverseC (f' \o f) r'' ->
is_left_inverseC f (r'' \o f') .
Proof. by move=> li x; apply: (left_i_v x li). Qed.
Lemma right_inv_compose_rfC (a b c:Set) (f:a->b) (f':b->c)(s'': c->a):
is_right_inverseC (f' \o f) s'' ->
is_right_inverseC f' (f \o s'').
Proof. move=> ri x; by apply: (right_i_v x ri). Qed.
Lemma left_inv_compose_rf2C (a b c:Set) (f:a->b) (f':b->c)(r'': c->a):
is_left_inverseC (f' \o f) r'' -> surjectiveC f ->
is_left_inverseC f' (f \o r'').
Proof. move=> li s t;move: (s t) => [v <-]; exact: (f_equal f (li v)). Qed.
Lemma right_inv_compose_rf2C (a b c:Set) (f:a->b) (f':b->c)(s'': c->a):
is_right_inverseC (f' \o f) s'' -> injectiveC f'->
is_right_inverseC f (s'' \o f').
Proof. move=> ri inj;move=> t; apply: inj; exact (ri (f' t)). Qed.
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; move: fi=> [ _]; apply=>//.
move:c => [_ ff c]; apply: (proj2 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: (proj2 sf' _ yt) => [x xs <-].
have xt: inc x (target f) by move: c => [_ _ <-].
move: (proj2 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.
move: (left_inverse_composable c1 li1 li2) =>cc.
move: (left_i_target li1)=> tr'sr'.
have sf'sr: (source f' = source r) by rewrite (proj33 cc).
move: (left_i_source li1) => sr'tf'.
move:li1=> [crf' crfi']; move:li2=> [crf crfi].
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.
move: (right_inverse_composable cf'f ri1 ri2)=> css'.
move: (right_i_source ri2)=> sstf.
move: (right_i_target ri2)=> tssf.
have sf'sr: (target f = target s') by rewrite - (proj33 css').
move:ri1=> [cfs' cfsi']; move:ri2=> [cfs cfsi].
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.
by 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 aux: f' \coP f by []; move: aux=> [ff ff' eq].
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.
have sf'tf:(source f' = target f) by move: cff=> [_ _].
rewrite sf'tf=> x y xs ys.
move: ((proj2 sf) _ xs)=> [x' x's e1].
move: ((proj2 sf) _ ys)=> [y' y's e2].
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 aux: f' \coP f by []; move: aux=> [ff' ff seq].
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 aux: f' \coP f by []; move: aux=> [ff' ff seq].
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).
rewrite crrfi sfti compf_id_l // /invf bij_right_inverse //.
by move: cff=> [_ _ ->].
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 red; split; try fct_tac.
have fcsf: function (s'' \co f') by fct_tac.
have cfc: f \coP (s'' \co f') by red; split; try fct_tac; move:cffs=> [_ _]; aw.
move: (bijective_inv_f bf') => bif.
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
Lemma exists_left_composableC (a b c:Set) (f:a->b)(g:a->c):
surjectiveC g ->
((exists h, h \o g =1 f) <->
(forall (x y:a), g x = g y -> f x = f y)).
Proof.
move=> sg; split.
by move=> [h hp] x y; move: (hp x) (hp y) => /= <- <- <-.
move: (exists_right_inv_from_surjC sg) => [h hp] hyp.
by exists (f \o h); move=> t /=; apply: hyp; move:(hp (g t)).
Qed.
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 => ->.
have fg: function g by fct_tac.
move: (bcreate1_fs fg sg) => scb.
set (bf:=bcreate ff sfsg (refl_equal (target f))).
move=> hyp.
have:(exists h : target g -> (target f), h \o (bcreate1 fg) =1 bf).
rewrite (exists_left_composableC bf scb).
move =>x y sv; apply: R_inj; do 2 rewrite prop_bcreate2.
by apply: hyp; try apply: R_inc; rewrite -2! (prop_bcreate1 fg) sv.
move=> [h ch].
exists (acreate h); split; first by split; fprops; aw.
have: (acreate (h \o (bcreate1 fg)) = acreate bf) by apply: acreate_exten.
by rewrite -compose_acreate (bcreate_inv1 fg) bcreate_inv2.
Qed.
Lemma exists_left_composable_auxC (a b c:Set) (f:a->b) (g:a-> c) s h:
is_right_inverseC g s ->
h \o g =1 f -> h =1 f \o s.
Proof.
by move=> ri eq x /=; rewrite -eq /=; move: (ri x) => /= ->.
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.
Lemma exists_unique_left_composableC (a b c:Set) (f:a->b)(g:a->c) h h':
surjectiveC g -> h \o g =1 f -> h' \o g =1 f -> h =1 h'.
Proof.
move=> sg chg chg' x.
move: (exists_right_inv_from_surjC sg) => [j jp].
rewrite (exists_left_composable_auxC jp chg).
by rewrite (exists_left_composable_auxC jp chg').
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.
Lemma left_composable_valueC (a b c:Set) (f:a->b)(g:a->c) s h:
surjectiveC g -> (forall (x y:a), g x = g y -> f x = f y) ->
is_right_inverseC g s -> h =1 f \o s ->
h \o g =1 f.
Proof.
move=> sg hyp rish eq x /=.
by rewrite eq /=; apply: hyp; rewrite -{2} (rish (g x)).
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 ->.
move: (right_i_source rish)=> sstg.
move: rish=> [cgs cgsi].
have cfs: f \coP s by hnf; split; [done |fct_tac | move:cgs => [_ _] <-].
have cfsg: (f \co s) \coP g by red; 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.
Lemma exists_right_composable_auxC (a b c:Set) (f:a->b) (g:c->b) h r:
is_left_inverseC g r -> g \o h =1 f
-> h =1 r \o f.
Proof. move=> li eq x /=; rewrite -(eq x); symmetry;exact: (li (h x)). 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.
Lemma exists_right_composable_uniqueC (a b c:Set)(f:a->b) (g:c->b) h h':
injectiveC g -> g \o h =1 f -> g \o h' =1 f -> h =1 h'.
Proof.
move=> ig c1 c2 x; apply: ig; by move: (c1 x)(c2 x) => /= -> ->.
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 => //; first by ue.
move=> x xsh.
apply: ig.
by rewrite p3; Wtac.
rewrite p6; Wtac; ue.
move: (f_equal (Vf ^~ x) cghf); aw; ue.
Qed.
Lemma exists_right_composableC (a b c:Set) (f:a->b) (g:c->b):
injectiveC g ->
((exists h, g \o h =1 f) <-> (forall u, exists v, g v = f u)).
Proof.
move=> ig; split.
by move=> [h cgh] u; exists (h u); rewrite -cgh.
move => mh.
case: (emptyset_dichot c) => hyp.
have ae: (a = emptyset).
apply /set0_P => y ya.
by move: (mh (Bo ya)) => [x _]; rewrite hyp in x; case: x.
symmetry in hyp; symmetry in ae.
move: empty_function_function => [pa pb pc].
rewrite ae in pb; rewrite hyp in pc.
exists (bcreate pa pb pc); move=> v.
by elimtype False; rewrite -ae in v; case: v.
move: hyp=> [x [xc _]].
move: (exists_left_inv_from_injC (inhabits xc) ig) => [r rv].
exists (r \o f).
move=> y /=; move: (mh y)=> [v <-]; exact (f_equal g (rv v)).
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).
move:(chg) => [_ fh th].
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 hyp.
have cge: (g \coP empty_function).
hnf; split => //; first by apply: (proj31 empty_function_function).
by rewrite /empty_function /empty_function_tg; aw.
exists (empty_function); split=>//; symmetry.
apply: function_exten=>//;
rewrite /empty_function /empty_function_tg;try fct_tac; aw.
rewrite ssfe => x /in_set0 //.
move: ff=> [_ fgf ->].
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.
move: (exists_left_inv_from_inj ig nesg)=> [r rli].
move: (left_i_target rli)=> trsg; move: rli=> [crg crgi].
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.
Lemma right_composable_valueC (a b c:Set) (f:a->b) (g:c->b) r h:
injectiveC g -> is_left_inverseC r g -> (forall u, exists v, g v = f u) ->
h =1 r \o f -> g \o h =1 f.
Proof.
move=> ig lir hyp eq x /=; rewrite eq /=.
by move: (hyp x)=> [v <-]; rewrite (left_i_v).
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 ->.
move: (left_i_target lirg)=> trsg; move: lirg=> [crg crgi].
have srtg: source r = target g by move: 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 ->].
move: (f_equal (fun z=> (Vf z y)) crgi); aw; bw.
by move=> ->.
Qed.
EII-3-9 Functions of two arguments
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; move /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; move /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)).
Section Ext_to_prod.
Variables u v: Set.
Hypothesis (fu: function u) (fv: function v).
Lemma ext_to_prod_f: function (ext_to_prod u v).
Proof.
apply: lf_function => t; move/setX_P =>[_ px py]; apply: setXp_i; fprops.
Qed.
Lemma ext_to_prod_V2 c:
inc c ((source u) \times (source v)) ->
Vf (ext_to_prod u v) c = J (Vf u (P c)) (Vf v (Q c)).
Proof.
rewrite /ext_to_prod=> h; aw.
move=> 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 (ext_to_prod u 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 (ext_to_prod u v) = source u \times source v.
Proof. rewrite/ext_to_prod; aw. Qed.
Lemma ext_to_prod_r:
range (graph (ext_to_prod u v)) =
(range (graph u)) \times (range (graph v)).
Proof.
have fe: (function (ext_to_prod u 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: xs; move/setX_P=> [_ 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.
Lemma ext_to_prod_propP a a' (x: a \times a'): inc (P (Ro x)) a.
Proof.
have: (inc (Ro x) (a \times a')) by apply: R_inc.
by move/setX_P => [_].
Qed.
Lemma ext_to_prod_propQ a a' (x: a \times a'): inc (Q (Ro x)) a'.
Proof.
have: (inc (Ro x) (a \times a')) by apply: R_inc.
by move/setX_P => [_].
Qed.
Lemma ext_to_prod_propJ (b b':Set) (x:b)(x':b'):
inc (J (Ro x)(Ro x')) (b \times b').
Proof. apply/setXp_i;apply: R_inc. Qed.
Definition pr1C a b:= fun x: a \times b => Bo(ext_to_prod_propP x).
Definition pr2C a b:= fun x: a \times b => Bo(ext_to_prod_propQ x).
Definition pairC (a b:Set) := fun (x:a)(y:b) => Bo(ext_to_prod_propJ x y).
Definition ext_to_prodC (a b a' b':Set) (u:a->a')(v:b->b') :=
fun x => pairC (u (pr1C x)) (v (pr2C x)).
Lemma prC_prop (a b:Set) (x: a \times b):
Ro x = J (Ro (pr1C x)) (Ro (pr2C x)).
Proof.
have: (inc (Ro x) (a \times b)) by apply: R_inc.
by rewrite /pr1C/pr2C B_eq B_eq; move/setX_P=> [-> _].
Qed.
Lemma pr1C_prop (a b:Set) (x:a \times b):
Ro (pr1C x) = P (Ro x).
Proof. rewrite (prC_prop x); aw. Qed.
Lemma pr2C_prop (a b:Set) (x:a \times b):
Ro (pr2C x) = Q (Ro x).
Proof. rewrite (prC_prop x); aw. Qed.
Lemma prJ_prop (a b:Set) (x:a)(y:b):
Ro(pairC x y) = J (Ro x) (Ro y).
Proof. by rewrite /pairC B_eq. Qed.
Lemma prJ_recov (a b:Set) (x:a \times b):
pairC (pr1C x) (pr2C x) = x.
Proof.
apply: R_inj; rewrite prJ_prop pr1C_prop pr2C_prop.
rewrite (setX_pair (A:=a)(B:=b)) //; by apply: R_inc.
Qed.
Lemma ext_to_prod_prop (a b a' b':Set) (u:a->a')(v:b->b') (x:a)(x':b):
J(Ro (u x)) (Ro (v x')) = Ro(ext_to_prodC u v (pairC x x')).
Proof.
rewrite /ext_to_prodC prJ_prop.
have <-: (x = (pr1C (pairC x x'))).
by apply: R_inj; rewrite pr1C_prop prJ_prop; aw.
have <- //: (x' = (pr2C (pairC x x'))).
by apply: R_inj; rewrite pr2C_prop prJ_prop; aw.
Qed.
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 (ext_to_prod u 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 (ext_to_prod u 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 (ext_to_prod u 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 (ext_to_prod u v) =
ext_to_prod (inverse_fun u)(inverse_fun v).
Proof.
move=> bu bv.
have Ha:bijection (ext_to_prod u 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.
Composition of products
Lemma composable_ext_to_prod2 u v u' v':
u' \coP u -> v' \coP v -> (ext_to_prod u' v') \coP (ext_to_prod u v).
Proof.
move=> [fu' fu seq] [fv' fv seq'].
split;fprops.
rewrite /ext_to_prod; aw; by rewrite seq seq'.
Qed.
Lemma compose_ext_to_prod2 u v u' v':
u' \coP u -> v' \coP v ->
(ext_to_prod u' v') \co (ext_to_prod u v) =
ext_to_prod (u' \co u)(v' \co v).
Proof.
move=> cuu cvv.
have cee: ((ext_to_prod u' v') \coP (ext_to_prod u v))
by apply: composable_ext_to_prod2.
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)).
move:cuu => [_ _]; move: cvv => [_ _ ]; move=> -> ->.
by 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.
Lemma injective_ext_to_prod2C (a b a' b':Set) (u:a->a')(v:b->b'):
injectiveC u -> injectiveC v -> injectiveC (ext_to_prodC u v).
Proof.
move=> iu iv x x' eql.
move: (f_equal (@Ro (product a' b')) eql).
rewrite -(prJ_recov x) -(prJ_recov x').
rewrite - 2!ext_to_prod_prop; move=> eql'.
by rewrite (iu _ _ (R_inj (pr1_def eql'))) (iv _ _ (R_inj (pr2_def eql'))).
Qed.
Lemma surjective_ext_to_prod2C (a b a' b':Set) (u:a->a')(v:b->b'):
surjectiveC u -> surjectiveC v-> surjectiveC (ext_to_prodC u v).
Proof.
move=> su sv x; rewrite -(prJ_recov x).
have pRx: pairp (Ro x) by case /setX_P: (R_inc x).
move: (su (pr1C x)) => [y yp]; move: (sv (pr2C x)) => [y' y'p].
exists (pairC y y'); apply: R_inj.
rewrite - ext_to_prod_prop yp y'p prJ_recov pr1C_prop pr2C_prop; aw.
Qed.
Lemma bijective_ext_to_prod2C (a b a' b':Set) (u:a->a')(v:b->b'):
bijectiveC u -> bijectiveC v -> bijectiveC (ext_to_prodC u v).
Proof.
rewrite /bijectiveC; move=> [p1 p2][p3 P4].
by split ; [apply: injective_ext_to_prod2C | apply: surjective_ext_to_prod2C].
Qed.
Lemma compose_ext_to_prod2C (a b c a' b' c':Set) (u:b-> c)(v:a->b)
(u':b'-> c')(v':a'->b'):
(ext_to_prodC u u') \o (ext_to_prodC v v') =1
ext_to_prodC (u \o v)(u' \o v').
Proof.
move => x /=; rewrite -(prJ_recov x).
move: (ext_to_prod_prop v v' (pr1C x) (pr2C x));rewrite -prJ_prop=> xx.
rewrite - (R_inj xx).
by apply: R_inj; rewrite -2! ext_to_prod_prop.
Qed.
Lemma inverse_ext_to_prod2C (a b a' b':Set) (u:a->a')(v:b->b')
(Hu: bijectiveC u)(Hv:bijectiveC v):
inverseC (bijective_ext_to_prod2C Hu Hv) =1
ext_to_prodC (inverseC Hu)(inverseC Hv).
Proof.
move => x.
have ww: x = ext_to_prodC u v (ext_to_prodC (inverseC Hu) (inverseC Hv) x).
move: (compose_ext_to_prod2C u (inverseC Hu) v (inverseC Hv))=> eq.
move: (eq x) => /= ->.
rewrite - (prJ_recov x); apply: R_inj.
by rewrite -ext_to_prod_prop /= inverseC_prb inverseC_prb prJ_prop.
by rewrite ww inverseC_pra -ww.
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.
move: (restriction_to_image_axioms ff) => ra.
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
Definition imageC (a b:Set) (f:a->b) := IM (fun u:a => Ro (f u)).
Lemma imageC_inc (a b:Set) (f:a->b) (x:a): inc (Ro (f x)) (imageC f).
Proof. by rewrite /imageC; apply /IM_P; exists x. Qed.
Lemma imageC_exists (a b:Set) (f:a->b) x:
inc x (imageC f) -> exists y:a, x = Ro (f y).
Proof. by rewrite /imageC=> xi; move /IM_P: xi => [y] <-; exists y. Qed.
Lemma sub_image_targetC (a b:Set) (f:a->b): sub (imageC f) b.
Proof. by move=> x xi; move: (imageC_exists xi)=> [y] ->; apply: R_inc. Qed.
Definition restriction_to_imageC (a b:Set) (f:a->b) :=
fun x:a => Bo (imageC_inc f x).
Lemma restriction_to_imageC_pr (a b:Set) (f:a->b) (x:a):
Ro (restriction_to_imageC f x) = Ro (f x).
Proof. by rewrite /restriction_to_imageC B_eq. Qed.
Lemma canonical_decomposition1C (a b:Set) (f:a->b)
(g:a-> imageC f)(i:imageC f ->b):
g = restriction_to_imageC f ->
i = inclusionC (sub_image_targetC (f:=f)) ->
[/\ injectiveC i , surjectiveC g &
(injectiveC f -> bijectiveC g)].
Proof.
move=> gv iv.
have sg: surjectiveC g.
move=> x; rewrite gv.
have aux: (inc (Ro x) (imageC f)) by apply: R_inc.
move: (imageC_exists aux)=> [y]; exists y; apply: R_inj.
by rewrite restriction_to_imageC_pr; symmetry.
split => //.
move=> x x' eq; move: (f_equal (@Ro b) eq).
by rewrite iv 2! inclusionC_pr; apply: R_inj.
move=> fi; split=> //; move=> x y eq ; move: (f_equal (@Ro (imageC f)) eq).
rewrite gv 2!restriction_to_imageC_pr=> eqbis.
by apply: fi; apply: R_inj.
Qed.
End Bfunction.
Export Bfunction.