proposition: Lemma exercise3_8 G G': correspondence G -> correspondence G' -> source G = target G' -> source G' = target G -> (forall x, inc x (source G) -> Vfs G' (Vfs G (singleton x)) = singleton x) -> (forall x, inc x (source G') -> Vfs G (Vfs G' (singleton x)) = singleton x) -> [/\ bijection G, bijection G' & G = inverse_fun G'].
proof: Proof. rewrite /Vfs=> cG cG' sG sG' G'Gx GG'x. have gG: sgraph (graph G) by fprops. have gG': sgraph (graph G') by fprops. have sGdgG: source G = domain (graph G). apply: extensionality; last by fprops. move=> x xs; move: (set1_1 x); rewrite - (G'Gx _ xs). move /dirim_P => [y] /dirim_P [t /set1_P -> aa _]; ex_tac. have sGdgG': source G' = domain (graph G'). apply: extensionality; last by fprops. move=> x xs; move: (set1_1 x); rewrite - (GG'x _ xs). move /dirim_P => [y] /dirim_P [t /set1_P -> aa _]; ex_tac. have JGG' x y z: inc (J x y)(graph G) -> inc (J y z)(graph G') -> x = z. move=> Jxy Jyz. have xG: inc x (source G) by rewrite sGdgG; ex_tac. symmetry; apply: set1_eq. rewrite - (G'Gx _ xG); apply /dirim_P; ex_tac; apply /dirim_P; ex_tac. fprops. have JG'G x y z: inc (J x y)(graph G') -> inc (J y z)(graph G) -> x = z. move=> Jxy Jyz. have xG: inc x (source G') by rewrite sGdgG'; ex_tac. symmetry; apply: set1_eq. rewrite - (GG'x _ xG); apply /dirim_P; ex_tac; apply /dirim_P; ex_tac. fprops. have xGy x: inc x (source G) -> exists2 y, inc (J x y) (graph G) & inc (J y x) (graph G'). move=> xsG; move: (set1_1 x). rewrite - (G'Gx _ xsG); move /dirim_P => [y /dirim_P [z /set1_P -> pb pc]]. ex_tac. have xG'y x: inc x (source G') -> exists2 y, inc (J x y) (graph G') & inc (J y x) (graph G). move=> xsG; move: (set1_1 x). rewrite - (GG'x _ xsG); move /dirim_P => [y /dirim_P [z /set1_P -> pb pc]]. ex_tac. have fgG: fgraph (graph G). split=>//; move=> x y xG yG Pxy. have px: pairp x by apply: gG. have py: pairp y by apply: gG. apply: pair_exten =>//. rewrite - px in xG. rewrite - py -Pxy in yG. have Pxs: inc (P x) (source G) by rewrite sGdgG; ex_tac. move: (xGy _ Pxs) => [z _ J2g]. by rewrite - (JG'G _ _ _ J2g xG) - (JG'G _ _ _ J2g yG). have fgG': fgraph (graph G'). split=>//; move=> x y xG yG Pxy. have px: pairp x by apply: gG'. have py: pairp y by apply: gG'. apply: pair_exten =>//. rewrite - px in xG. rewrite - py -Pxy in yG. have Pxs: inc (P x) (source G') by rewrite sGdgG'; ex_tac. move: (xG'y _ Pxs) => [z _ J2g]. by rewrite - (JGG' _ _ _ J2g xG) - (JGG' _ _ _ J2g yG). have fg: function G by []. have fg': function G' by []. have GiG: (graph G = inverse_graph(graph G')). set_extens x => xs. have px: pairp x by apply: gG. rewrite - px in xs |- *; apply/igraph_pP. have Ps: inc (P x) (source G) by rewrite sGdgG; ex_tac. move: (xGy _ Ps)=> [y J1 J2]. by rewrite -(JG'G _ _ _ J2 xs). have gi: (sgraph (inverse_graph (graph G'))) by fprops. have px: pairp x by apply: gi. move: xs; rewrite - px;move/igraph_pP => xs; rewrite -px. have Ps: inc (P x) (source G). rewrite sG; apply: corresp_sub_range=>//; ex_tac. move: (xGy _ Ps)=> [y J1 J2]. by aw;rewrite (JG'G _ _ _ xs J1). have GiG2: (G = inverse_fun G'). rewrite /inverse_fun - sG sG' -GiG. by symmetry; apply: corresp_recov1. have bG: bijection G. split. split=>// x y xs ys sW. move: (Vf_pr3 fg xs) => HGx. move: (Vf_pr3 fg ys) => HGy; rewrite - sW in HGy. have Ws: inc (Vf G x) (source G') by rewrite sG'; fprops. move: (xG'y _ Ws) => [z J1 J2]. by rewrite (JGG' _ _ _ HGx J1) (JGG' _ _ _ HGy J1). apply: surjective_pr5 =>// x. rewrite - sG' => xs. move: (xG'y _ xs) => [z J1 J2]. rewrite /related; ex_tac; apply: (p1graph_source fg J2). have GiG3: G' = inverse_fun G by rewrite GiG2 ifun_involutive. by split => //; rewrite GiG3; apply: inverse_bij_fb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)