(** ** Bourbaki Sets 1 Exercises Copyright INRIA (2009-2012) Apics/Marelle Team (Jose Grimm). *) (* $Id: ssete1.v,v 1.54 2016/05/19 08:34:58 grimm Exp$ *) Require Import ssreflect ssrfun ssrbool eqtype ssrnat. Require Export sset4. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Module Exercise1. Lemma rel_False: emptyset = False. Proof. by symmetry;apply /set0_P => t; case; case. Qed. Lemma rel_True: singleton (Ro I) = True. Proof. apply: extensionality. move => t /set1_P ->; apply: R_inc. move => t [a <-]; apply /set1_P. have -> //: a = I by case:a. Qed. (** [\not\in] is not collectivizing *) Lemma not_collectivizing_notin: ~ (exists z, forall y, inc y z <-> not (inc y y)). Proof. case=> x hx; move: (hx x) => [p p']. pose H:= (fun h : inc x x => (p h h));exact (H (p' H)). Qed. (** There is a set containing no set, and no set containg all sets *) Lemma collectivizing_special : (exists x, forall y, ~ (inc y x)) /\ ~ (exists x, forall y, inc y x). Proof. split; first by exists emptyset; apply: in_set0. move=> [x Px]; apply: not_collectivizing_notin. exists (Zo x (fun z => ~ (inc z z))) => z. by split;[ case /Zo_P | move => zz; apply:Zo_i]. Qed. (** Any property [p] is true for the elements of the empty set *) Lemma emptyset_pra x (p: property): inc x emptyset -> (p x). Proof. case; case. Qed. (** ** Section 1 *) (** Exercise 1.1: reverted extensionality *) Section exercise1_1. Variable x y:Set. Lemma exercise1_1: (x=y) <-> (forall X, inc x X -> inc y X). Proof. split; first by move=> ->. move=> spec_sub; symmetry; apply: set1_eq; apply: spec_sub; fprops. Qed. End exercise1_1. (** Exercise 1.2: [emptyset <> singleton x] and there are at least two different sets *) Lemma exercise1_2: exists x y:Set, x <> y. Proof. have theorem:forall x, emptyset <> singleton x. by move=> x esx; empty_tac1 x. by exists emptyset; exists (singleton emptyset); apply: theorem. Qed. (** Exercise 1.3: [sub] and [complement] *) Lemma exercise1_3 X A B (compl := fun z => X -s z) : sub A X -> sub B X -> ((sub (compl B) A <-> sub (compl A) B) /\ (sub B (compl A) <-> sub A (compl B))). Proof. have aux1: forall a b, sub a X -> sub b X -> (sub (compl a) b <-> a \cup b = X). move => a b aX bX; split. move => s1; set_extens t; first by case /setU2_P => ts; fprops. rewrite - (setU2_Cr aX); case /setU2_P => ts; fprops. by rewrite /compl => <- t /setC_P [/setU2_P] []. have aux2: forall a b, sub a X -> sub b X -> (sub b (compl a) <-> a \cap b = emptyset). move => a b aX bX; split. move => s1; apply /set0_P =>t /setI2_P [ta tb]. by move /setC_P: (s1 _ tb) => []. move => abe t tb; apply /setC_P; split; fprops. move => ta; empty_tac1 t. move => ax bx; split. apply: (iff_trans (aux1 _ _ bx ax)); rewrite setU2_C. by apply: iff_sym; apply/aux1. apply: (iff_trans (aux2 _ _ ax bx)); rewrite setI2_C. by apply: iff_sym; apply/aux2. Qed. (** Exercise 1.4: subsets of a singleton *) Lemma exercise1_4 X x: sub X (singleton x) <-> (X = singleton x \/ X = emptyset). Proof. split; last by case => ->; fprops. move => asx; case: (emptyset_dichot X); first by right. by move => nea; left; apply: set1_pr1 => // z /asx /set1_P. Qed. (** Exercise 1.5: Alternate definition of emptyset *) Lemma exercise1_5: emptyset = choose (fun X => ~ (inc (rep X) X)). Proof. pose p := fun z => ~ inc (rep z) z. have pe: p emptyset by exact: in_set0. move:(choose_pr (ex_intro p emptyset pe)) => pcp. case:(emptyset_dichot (choose p)) => // ney; by move: (rep_i ney). Qed. (** Exercise 1.6: Variant of the axiom of extent. *) (** We need an axiom that says [choose p = choose q] for equivalent propositions *) Section Ex1_6. Hypothesis choose_equiv: forall (p q: property), (forall x, p x <-> q x) -> choose p = choose q. Lemma exercise1_6: (forall y, y = choose (fun x => (forall z, (inc z x) <-> (inc z y)))) -> (forall a b : Set, sub a b -> sub b a -> a = b). Proof. move=> hyp a b; rewrite /sub => sab sba. rewrite (hyp a) (hyp b). apply: choose_equiv; move=> x. split; move=> aux z; rewrite aux; split; auto. Qed. End Ex1_6. (** ** Section 2 *) (** Exercise 2.1: binary to unary relations. *) Lemma exercise2_1 (R: relation) : ((exists x, exists y, R x y) <-> (exists z, pairp z /\ R(P z) (Q z))) /\ ((forall x, forall y, R x y) <-> (forall z, pairp z -> R(P z) (Q z))). Proof. split;split. - move=> [x] [y] Rxy; exists (J x y); aw;fprops. - by move => [z [zp Rz]]; exists (P z); exists (Q z). - move=> hyp z _; apply: hyp. - move => hyp x y; move: (hyp _ (pair_is_pair x y)); aw. Qed. (** Exercise 2.2: the axiom of the pair. *) Definition xpair (x y : Set) := doubleton (singleton x) (doubleton x (singleton y)). Lemma exercise2_2 x y z w: (xpair x y = xpair z w) <-> (x = z /\ y = w). Proof. split; last by move=> [] -> ->. move => eq. have fp2: inc (singleton x) (xpair z w) by rewrite -eq /xpair; fprops. have sp2: inc (doubleton x (singleton y)) (xpair z w). by rewrite -eq /xpair; fprops. have xz: x=z. case /set2_P: fp2; first by apply: set1_inj. by move=> sd; symmetry; apply: set1_eq; ue. split=>//. rewrite xz in sp2. case /set2_P: sp2 => hyp. symmetry. have syz: (singleton y = z) by apply: set1_eq; ue. have: (inc (doubleton z (singleton w)) (xpair x y)). by rewrite eq /xpair; fprops. rewrite xz /xpair hyp; move/set1_P => zwz. have: (singleton w = z) by apply: set1_eq; ue. by rewrite - syz; apply: set1_inj. apply: set1_inj. have sp3: (inc (singleton w) (doubleton z (singleton y))) by ue. case /set2_P: sp3 => sp4; last by symmetry. have sp5: (inc (singleton y) (doubleton z (singleton w))) by ue. by case /set2_P: sp5; try ue. Qed. (** ** Section 3 *) (** Exercise 3.1: Some equivalences without graph *) Definition has_no_graph (r:relation):= ~(exists G, forall x y, r x y -> inc (J x y) G). Definition is_universal (r:relation):= forall x, exists y, r x y \/ r y x. Lemma is_universal_pr r: is_universal r -> has_no_graph r. Proof. move=> u [X h]. case:(proj2 collectivizing_special). exists ((domain X) \cup (range X)) => y. move: (u y) => [x [] /h jg]; apply /setU2_P; [left | right];ex_tac. Qed. Lemma exercise3_1: [/\ has_no_graph (fun x y => inc x y), has_no_graph (fun x y => sub x y) & has_no_graph (fun x y => x = singleton y) ]. Proof. split; apply: is_universal_pr; move=> x; [ exists (singleton x) | exists x | exists (singleton x) ] ; fprops. Qed. (** Exercise 3.2: Some properties of a graph *) Lemma exercise3_2 G X: sgraph G -> ( sub X (domain G) <-> sub X (direct_image (inverse_graph G) (direct_image G X))). Proof. move=> gG. split; move=> hyp t ts; move: (hyp _ ts). move/(domainP gG)=> [y Jg]; apply/dirim_P;exists y. apply/dirim_P; ex_tac. by apply/igraph_pP. move/dirim_P => [x _] /igraph_pP h; ex_tac. Qed. (** Exercise 3.3: Some properties of a graph *) Lemma exercise3_3a G H: sgraph G -> sgraph H -> ( sub (domain H) (domain G) <-> sub H (H \cg ((inverse_graph G) \cg G))). Proof. move=> gG gH. split => h t ts. move: (gH _ ts) => Jt; rewrite - Jt in ts. have: (inc (P t) (domain G)) by apply: h; ex_tac. move /(domainP gG)=> [y JG]; apply /compg_P; split => //; ex_tac. by apply /compg_pP; ex_tac; apply/igraph_pP. move /(domainP gH): ts => [y JH]. move: (h _ JH) => /compg_pP [z /compg_pP [u q _] _]; ex_tac. Qed. Lemma exercise3_3b G: sgraph G -> sub G (G \cg ((inverse_graph G) \cg G)). Proof. move=> gG; apply /(exercise3_3a gG gG); fprops. Qed. (** Exercise 3.4: Some properties of the empty graph *) Lemma exercise3_4a G: ( emptyset \cg G = emptyset /\ G \cg emptyset = emptyset). Proof. split; apply /set0_P => x /compg_P [_]. by move => [y _ /in_set0]. by move => [y /in_set0]. Qed. Lemma exercise3_4b G: sgraph G -> ((inverse_graph G) \cg G = emptyset <-> G = emptyset). Proof. move=> gG; split => h; last by rewrite h; apply: (proj2 (exercise3_4a _)). apply /set0_P => x xG; empty_tac1 (J (P x) (P x)). move:(eq_ind_r (inc^~ G) xG (gG x xG)) => px. by apply/compg_pP; exists (Q x) => //; apply /igraph_pP. Qed. (** Exercise 3.5: graphs and products *) Lemma exercise3_5 G A B: ((A \times B) \cg G = (inverse_image G A) \times B /\ G \cg (A \times B) = A \times (direct_image G B)). Proof. split; set_extens x. - move /compg_P => [px [y yG /setXp_P [pa pb]]]. apply/setX_P;split => //; apply/iim_graph_P; ex_tac. - move /setX_P => [px /iim_graph_P [y uA JG] QB]. apply /compg_P; split => //; ex_tac; fprops. - move /compg_P => [px [y /setXp_P [pa pb pc]]]. apply /setX_P;split => //; apply/dirim_P; ex_tac. - move /setX_P => [px pxa /dirim_P [y ya yb]]. apply/compg_P; split => //; ex_tac; fprops. Qed. (** Exercise 3.6: complements of a graph *) Definition complement_graph G := ((domain G) \times (range G)) -s G. Lemma complement_graph_g G: sgraph (complement_graph G). Proof. by move => t /setC_P [] /setX_P [ok _] _. Qed. Lemma exercise3_6a G: sgraph G -> commutes_at complement_graph inverse_graph G. Proof. move => gG. have gc: sgraph (complement_graph G) by apply: complement_graph_g. rewrite /commutes_at/complement_graph (igraph_range gG)(igraph_domain gG). set_extens t. move /setC_P => [/setX_P [pt pa pb] pc]. apply /igraphP; split => //; apply/ setC_P;split; first by fprops. by move /igraph_pP; rewrite pt. move /igraphP => [px /setC_P [/setXp_P [pa pb] pc]]. apply/setC_P; rewrite - px; split; [ fprops | by move /igraph_pP]. Qed. Lemma exercise3_6b G B: sgraph G -> sub (range G) B -> sub (G \cg (complement_graph (inverse_graph G))) (complement_graph (diagonal B)). Proof. move=> gG srB; rewrite exercise3_6a // => t. move /compg_P => [pt [y /igraph_pP /setC_P [/setXp_P [pa pb] pc] pd]]. apply/setC_P; split; last by move /diagonal_i_P => [_ _ eq]; case: pc; ue. move:(@identity_sgraph B); rewrite - diagonal_is_identity => aux. apply /setX_i => //. apply/(domainP aux); exists(P t); apply /diagonal_pi_P; fprops. apply/(rangeP aux); exists(Q t);apply /diagonal_pi_P. split => //; apply: srB; ex_tac. Qed. Lemma exercise3_6c A G: sgraph G -> sub (domain G) A -> sub ((complement_graph (inverse_graph G)) \cg G) (complement_graph (diagonal A)). Proof. move=> gG sd. rewrite (exercise3_6a gG) => t. move /compg_P => [pt [y pa /igraph_pP /setC_P [/setXp_P [pb pc] pd]]]. apply/setC_P; split; last by move /diagonal_i_P => [_ _ eq];case: pd; ue. move:(@identity_sgraph A); rewrite - diagonal_is_identity => aux. apply /setX_i => //. apply/(domainP aux); exists(P t); apply /diagonal_pi_P. split => //; apply: sd; ex_tac. apply/(rangeP aux); exists(Q t); apply /diagonal_pi_P; fprops. Qed. Lemma exercise3_6d G: sgraph G -> ( G = (domain G) \times (range G) <-> G \cg ((complement_graph (inverse_graph G)) \cg G) = emptyset ). Proof. move=> gG; rewrite (exercise3_6a gG). transitivity (complement_graph G = emptyset). rewrite /complement_graph; split;first by move => <-; apply: setC_v. move => h; move:(empty_setC h) => aux; apply: extensionality => //. apply: (sub_graph_setX gG). split. move=> ->; rewrite igraph0. by move: (exercise3_4a G) => [-> ->]. move=> ce; apply /set0_P => x xK. move: (xK); move /setC_P => [] /setX_P [pa] /(domainP gG) [u J1G] /(rangeP gG) [v J2G] _. empty_tac1 (J v u); apply /compg_pP; ex_tac; apply /compg_pP; ex_tac. by apply/igraph_pP; rewrite pa. Qed. (** Exercise 3.7: Functional graphs *) Lemma exercise3_7 G: sgraph G -> (fgraph G <-> forall X, sub (direct_image G (inverse_image G X)) X). Proof. move=>gG; split. move=> fgG X x /dirim_P [y /iim_graph_P [u ux pug] pxg]. by rewrite (fgraph_pr fgG pxg pug). move=> hyp; split =>// x y xG yG sP. move:(gG _ xG) (gG _ yG)=> px py. apply: pair_exten=>//; apply: set1_eq. apply: (hyp (singleton (Q y))). apply/dirim_P; exists (P x); last by rewrite px. by apply /iim_graph_P; exists (Q y); fprops; rewrite sP py. Qed. (** Exercise 3.8: Characterisation of an inverse via images of singletons *) 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. 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. (** Exercise 3.9: property of bijections *) Lemma exercise3_9 f g h: function f -> function g -> function h-> source g = target f -> source h = target g -> bijection (g \co f) -> bijection (h \co g) -> [/\ bijection f, bijection g & bijection h]. Proof. move=> ff fg fh sgtf shtg bgf bhg. have cgf : g \coP f by []. have chg : h \coP g by []. have ig: injection g. by move: bhg=>[ia sa]; apply: (right_compose_fi chg ia). have sg: surjection g. by move: bgf=>[ia sa]; apply: (left_compose_fs cgf sa). have bg: bijection g by split. split => //. apply: (right_compose_fb cgf bgf bg). apply: (left_compose_fb chg bhg bg). Qed. (** Exercise 3.10: property of bijections *) Lemma exercise3_10 f g h: function f -> function g -> function h-> source g = target f -> source h = target g -> source f = target h -> injection (h \co (g \co f)) -> surjection (g \co (f \co h)) -> (injection (f \co (h \co g)) \/ surjection (f \co (h \co g))) -> [/\ bijection f, bijection g & bijection h]. Proof. move=> ff fg fh sgtf shtg sfth ihgf sgfh is_fgh. have cfh: f \coP h by []. have chg: h \coP g by []. have cgf: g \coP f by []. rewrite compfA // in ihgf. have fhg: function (h \co g) by fct_tac. have chgf: (h \co g) \coP f by hnf; aw. move: (right_compose_fi chgf ihgf) => inf. have ffh: function (f \co h) by fct_tac. have cgfh: g \coP (f \co h) by hnf; aw. move: (left_compose_fs cgfh sgfh) => sg. case is_fgh. rewrite compfA// => ifhg. have cfhg: (f \co h) \coP g by hnf; aw. move: (right_compose_fi cfhg ifhg) => ig. move: (left_compose_fs2 cgfh sgfh ig)=> sfh. move: (left_compose_fs cfh sfh) =>sf. move: (left_compose_fi2 cfhg ifhg sg) => ifh. have bfh: (bijection (f \co h)) by []. have bf: (bijection f) by []. have bg: (bijection g) by []. move: (right_compose_fb cfh bfh bf). done. move=> sfhg. have cfhg: (f \coP (h \co g)) by hnf; aw. move: (left_compose_fs cfhg sfhg) => sf. have bf: (bijection f) by []. move: (left_compose_fs2 cfhg sfhg inf) => shg. move:(left_compose_fi2 chgf ihgf sf) => ihg. move: (right_compose_fi chg ihg) => ig. have bg: (bijection g) by []. have bhg: (bijection (h \co g)) by []. move: (left_compose_fb chg bhg bg). done. Qed. (** Exercise 3.11: no associated code *) (** ** Section 4 *) (** Exercise 4.1: functional graph and inverse image *) Lemma exercise4_1a g: sgraph g -> (functional_graph g <-> {morph inverse_image g : x y / x \cap y}). Proof. move=> gg. have gig: sgraph (inverse_graph g) by fprops. split. move=> fgg x y; set_extens t. move /iim_graph_P => [u /setI2_P [ux uy] jg]. apply /setI2_P;split;apply /iim_graph_P; ex_tac. move /setI2_P => [ /iim_graph_P [u ux ua] /iim_graph_P [v vx va]]. rewrite -(fgg _ _ _ ua va) in vx. apply /iim_graph_P; exists u; fprops. move=> hyp x y y' gxy gxy'. move: (hyp (singleton y)(singleton y')). set u:= _ \cap _ => hyp1. have:inc x (inverse_image g u). rewrite /u hyp1;apply: setI2_i; apply /iim_graph_P. exists y; fprops. exists y'; fprops. by move /iim_graph_P => [t /setI2_P [/set1_P <- /set1_P <-]]. Qed. Lemma exercise4_1b g: sgraph g -> (functional_graph g <-> (forall x y, disjoint x y -> disjoint (inverse_image g x) (inverse_image g y))). Proof. rewrite /disjoint;move=> gg; split. move /(exercise4_1a gg) => h x y ie; rewrite /disjoint -h ie. by rewrite /inverse_image dirim_set0. move=> hyp x y y' gxy gxy'. have gig: sgraph (inverse_graph g) by fprops. case: (emptyset_dichot ((singleton y) \cap (singleton y'))). move=>aux; move:(hyp _ _ aux). set v:= _ \cap _ => ve. have: (inc x v) by rewrite /v; apply: setI2_i; apply /iim_graph_P; ex_tac. by rewrite ve => /in_set0. by move=> [z /setI2_P [/set1_P -> /set1_P ->]]. Qed. (** Exercise 4.2: Image and interesection *) Lemma exercise4_2a g x: direct_image g x = range (g \cap (x \times (range g))). Proof. set_extens y. move /dirim_P => [a ax pg]; apply/funI_P; exists (J a y); aw. apply /setI2_P; split => //; apply:setXp_i => //; ex_tac. move /funI_P => [a /setI2_P [pg /setX_P [pa pb pc]] ->]. by apply/dirim_P; ex_tac; rewrite pa. Qed. Lemma exercise4_2b g x: direct_image g x = direct_image g (x \cap (domain g)). Proof. set_extens t; move /dirim_P => [y ys Jg]; apply/dirim_P. ex_tac; apply /setI2_P; split=> //; ex_tac. move /setI2_P: ys => [pa pb]; ex_tac. Qed. (** Exercise 4.3: composition of product *) Lemma exercise4_3a x y y' z: disjoint y y' -> (y' \times z) \cg (x \times y) = emptyset. Proof. rewrite /disjoint => ie; apply /set0_P. move=> t => /compg_P [_ [u /setXp_P [_ uy] /setXp_P [uy' _]]]. by empty_tac1 u. Qed. Lemma exercise4_3b x y y' z: nonempty(y \cap y') -> (y' \times z) \cg (x \times y) = x \times z. Proof. move=> [t /setI2_P [ty ty']]. set_extens u. move /compg_P => [pu [v /setXp_P [pa _] /setXp_P [_ pb]]]. by apply:setX_i. move => /setX_P [pu Px Qy]; apply/compg_P; split => //; exists t; fprops. Qed. (** Exercise 4.4: image of union or intersection *) Definition graph_morph op ui g := op (ui g) = ui (Lg (domain g) (fun i => op (Vg g i))). Lemma exercise4_4a g x: graph_morph (direct_image^~x) unionb g. Proof. set_extens y. move => /dirim_P [a ax /setUb_P [u ud Jv]]. apply: (@setUb_i _ u); bw; apply /dirim_P; ex_tac. move /setUb_P => [z]; rewrite Lg_domain => zd; bw. move /dirim_P => [u ux Jv]; apply /dirim_P; ex_tac; union_tac. Qed. Lemma exercise4_4b g x: singletonp x -> graph_morph (direct_image^~x) intersectionb g. Proof. move=> [y ->]; set_extens t. move => /dirim_P [a /set1_P ->]. case: (emptyset_dichot g) => gne; first by rewrite gne setIb_0 => /in_set0. move => pi; apply: setIb_i. move /domain_set0P: gne => [u udg]. pose ff i := direct_image (Vg g i) (singleton y). exists (J u (ff u)); apply /funI_P; ex_tac. bw; move => i idg; bw; apply/dirim_P; exists y; fprops. exact (setIb_hi pi idg). set f := Lg _ _. have dfdf: domain f = domain g by rewrite /f; bw. case: (emptyset_dichot g) => gne. by rewrite /f gne domain_set0 /Lg funI_set0 setIb_0 => /in_set0. move => ti; apply /dirim_P; exists y; first by fprops. apply/(setIb_P gne) => i idg; move: (idg); rewrite -dfdf=> idf. by move: (setIb_hi ti idf); rewrite /f; bw; move /dirim_P => [u /set1_P ->]. Qed. Lemma exercise4_4c: exists z, not {morph (direct_image ^~z): x y / x \cap y}. Proof. exists C2. set (G:= doubleton(J C0 C0)(J C1 C1)); set (H:= doubleton(J C0 C1)(J C1 C0)). move => h; move: {h} (h G H). have ->: direct_image G C2 = C2. set_extens u. move=> /dirim_P [v vz /set2_P] [] h; rewrite (pr2_def h); fprops. case /set2_P => h; apply /dirim_P; exists u; rewrite h /G; fprops. have -> :direct_image H C2 = C2. set_extens u. move=> /dirim_P [v vz /set2_P] [] h; rewrite (pr2_def h); fprops. case /set2_P => ->; apply /dirim_P; [ exists C1 | exists C0]; rewrite /H;fprops. rewrite setI2_id => bad. move: inc_C0_C2; rewrite -bad; move/dirim_P => [t _ /setI2_P[pa]]. have : P (J t C0) = Q (J t C0) by case/set2_P: pa => ->; aw. aw => ->; case/set2_P => h; [move: (pr2_def h) | move: (pr1_def h)]; fprops. Qed. (** Exercise 4.5: compose and union *) Lemma exercise4_5 G H: graph_morph (composeg ^~H) unionb G /\ graph_morph (composeg H) unionb G. Proof. split. set_extens x. move /compg_P => [px [y ph/setUb_P [z zd JV]]]. apply/setUb_P; bw; ex_tac; bw; apply /compg_P;split => //; ex_tac. move /setUb_P; bw; move => [y ydg]; bw; move /compg_P => [px [t pa pb]]. apply /compg_P;split=> //;ex_tac; union_tac. set_extens x. move /compg_P => [px [y /setUb_P [z zd JV] ph]]. apply/setUb_P; bw; ex_tac; bw; apply /compg_P;split => //; ex_tac. move /setUb_P; bw; move => [y ydg]; bw; move /compg_P => [px [t pa pb]]. apply /compg_P;split => //;ex_tac; union_tac. Qed. (** Exercise 4.6: functional graph: compose and intersection *) Lemma exercise4_6 G: sgraph G -> (fgraph G <-> {when sgraph &, {morph (composeg ^~G) : H H' / H \cap H'}}). Proof. move => gG; split. move=> fG H H' _ _; set_extens x. move /compg_P => [px [y J1 /setI2_P [J2 J3]]]. apply: setI2_i; apply /compg_P; split => //;ex_tac. move /setI2_P => [] /compg_P [px [y J1 J2 /compg_P [_ [y' J1' J2']]]]. rewrite (fgraph_pr fG J1 J1') in J2. apply/compg_P; split => //; ex_tac; fprops. move=> hyp; split=>// x y xG yG Pxy. set (H:= singleton(J (Q x) (P x))). set (H':= singleton(J (Q y) (P y))). have gh: sgraph H by move=> t /set1_P ->; fprops. have gh': sgraph H' by move=> t /set1_P->; fprops. move: (gG _ xG)(gG _ yG)=> xp yp. rewrite - xp in xG. rewrite - yp in yG. apply: pair_exten=>//. have p1: inc (J (P x)(P x)) (H \cg G). apply /compg_P; split;fprops; aw;ex_tac; rewrite /H; fprops. have p2: inc (J (P y)(P y)) (H' \cg G). apply /compg_P; split;fprops; aw;ex_tac; rewrite /H'; fprops. have : (inc (J (P x)(P x)) ((H \cap H') \cg G)). by rewrite hyp//; apply: setI2_i => //;rewrite Pxy. move/compg_P => [_ [z _]]; aw. move /setI2_P => [] /set1_P r1 /set1_P r2. by rewrite -(pr1_def r1) -(pr1_def r2). Qed. Lemma exercise4_6bis G: sgraph G -> (fgraph G <-> {morph (composeg^~G) : H H' / H \cap H'}). Proof. move => gG; split. move=> fG H H'; set_extens x. move /compg_P => [px [y J1 /setI2_P [J2 J3]]]. apply :setI2_i; apply /compg_P;split => //;ex_tac. move /setI2_P => [] /compg_P [px [y J1 J2 /compg_P [_ [y' J1' J2']]]]. rewrite (fgraph_pr fG J1 J1') in J2. apply/compg_P; split => //; ex_tac; fprops. move=> hyp; split=>// x y xG yG Pxy. set (H:= singleton(J (Q x) (P x))). set (H':= singleton(J (Q y) (P y))). move: (gG _ xG)(gG _ yG)=> xp yp. rewrite - xp in xG. rewrite - yp in yG. apply: pair_exten=>//. have p1: inc (J (P x)(P x)) (H \cg G). apply /compg_P; split;fprops; aw;ex_tac; rewrite /H; fprops. have p2: inc (J (P y)(P y)) (H' \cg G). apply /compg_P; split;fprops; aw;ex_tac; rewrite /H'; fprops. have: (inc (J (P x)(P x)) ((H \cap H') \cg G)). by rewrite hyp; apply: setI2_i => //;rewrite Pxy. move/compg_P => [_ [z _]]; aw. move /setI2_P => [] /set1_P r1 /set1_P r2. by rewrite -(pr1_def r1) -(pr1_def r2). Qed. (** Exercise 4.7: properties of graphs *) Lemma exercise4_7 G H K: sub ((H \cg G) \cap K) ((H \cap (K \cg (inverse_graph G))) \cg (G \cap ((inverse_graph H) \cg K))). Proof. move=> t /setI2_P [] /compg_P [tp [y JG JH]] tK. apply /compg_P;split =>// ;rewrite - tp in tK. by exists y; apply : setI2_i => //; apply/compg_P; split;fprops; aw; ex_tac; apply /igraph_pP. Qed. (** Exercise 4.8: A property of coarser coverings and two counter-examples *) Lemma exercise4_8a r s x: covering r x -> covering s x -> partition_w_fam s x -> coarser_cg s r -> nonempty_fam s -> forall k, inc k (domain s) -> exists2 i, inc i(domain r) & sub (Vg r i) (Vg s k). Proof. move=> [fgr co1] [fgs co2] [fgL md usx] [_ _ co] alne k kds. move: (alne _ kds)=> [y ysk]. have yx: inc y x by rewrite -usx;apply: (@setUb_i _ k);bw. have yu: inc y (unionb r) by apply: co1. move: (setUf_hi yu)=> [z zdr yrz]. move: (co _ zdr)=> [i ids rsi]. have yri: inc y (Vg s i) by apply: rsi. move: md; rewrite /mutually_disjoint; bw=> aux; case: (aux _ _ kds ids). by move=> ->; ex_tac. by move=> h; empty_tac1 y; bw; aw; split. Qed. Hint Rewrite variant_d variant_V_a variant_V_b: bw. Lemma exercise4_8b (r:= Lg (singleton C0) (fun _ => C2)) (s:= variantL C0 C1 C2 (singleton C0)) : [/\ covering r C2, covering s C2, coarser_cg s r, nonempty_fam s & ~(forall k, inc k (domain s) -> exists i, inc i (domain r) /\ sub (Vg r i) (Vg s k))]. Proof. have ba := C1_ne_C0. rewrite /r/s;split. - split; fprops; move=> t tx; apply: (@setUb_i _ C0); fprops; bw; fprops. - split; fprops; move=> y yx;apply: (@setUb_i _ C0); fprops; bw; fprops. - split; [ fprops | fprops | bw]. move=> t /set1_P ->; exists C0; bw;fprops. - move=> k; bw; case /set2_P=> ->; bw; [apply: set2_ne | apply: set1_ne]. bw; move=> h; move: (h _ inc_C1_C2)=> [i [/set1_P ->]]; bw; fprops => xa. by move: (xa _ inc_C1_C2) => /set1_P. Qed. Lemma exercise4_8c (x:= C4) (r:= (Lg C3 (fun i=> Yo (i = C0) (singleton C0) (Yo (i = C2) (singleton C1) (doubleton C2 C3))))) (s:= variantL C0 C1 (doubleton C0 C2) (doubleton C1 C3)): [/\ partition_w_fam s x, partition_w_fam r x, (forall k, inc k (domain s) -> exists2 i, inc i (domain r) & sub (Vg r i) (Vg s k)) & ~(coarser_cg s r)]. Proof. move:C2_ne_C01 => [n1 n2]. move:C3_ne_C012 => [n3 n4 n5]. have nba: C1 <> C0 by fprops. have sab: (disjoint (Vg s C0) (Vg s C1)). rewrite /s; bw; apply: disjoint_pr=>u ud1 ud2. case /set2_P: ud1=> h; case /set2_P: ud2; rewrite h; auto. have ra: inc C0 C3 by apply /C3_P; in_TP4. have rb: inc C1 C3 by apply /C3_P; in_TP4. have rc: inc C2 C3 by apply /C3_P; in_TP4. have dab: disjoint (Vg r C0) (Vg r C1). rewrite /r; bw; Ytac0; Ytac0; Ytac0; Ytac0. apply: disjoint_pr=> u /set1_P -> /set2_P; case; auto. have dac: disjoint (Vg r C0) (Vg r C2). rewrite /r; bw; Ytac0; Ytac0; Ytac0; Ytac0. apply: disjoint_pr=> u /set1_P -> /set1_P; auto. have dcb: disjoint (Vg r C2) (Vg r C1). rewrite /r; bw; Ytac0; Ytac0; Ytac0; Ytac0. apply: disjoint_pr=> u /set1_P -> /set2_P; case; auto. split. (* S partition *) rewrite /s;split; fprops. rewrite /variantL;red; bw; move=> i j ids jds. case /set2_P: ids => ->; case /set2_P: jds =>->; auto. by right; apply:disjoint_S. set_extens y => ys. case (setUb_hi ys); bw; move=> z zd. case /set2_P: zd => ->; bw=> yd; case /set2_P: yd => ->; apply/C4_P;in_TP4. case /C4_P: ys; move => ->. by apply :(@setUb_i _ C0);bw; fprops. by apply :(@setUb_i _ C1);bw; fprops. by apply :(@setUb_i _ C0);bw; fprops. by apply :(@setUb_i _ C1);bw; fprops. (* R partition *) split; first by rewrite /r; fprops. red; rewrite {1 2} /r; bw; move=> i j idr jdr. case /C3_P:idr => ->;case /C3_P:jdr;try move => ->; auto; try case => ->; auto; by right;apply: disjoint_S. set_extens t => ts. move: (setUb_hi ts); rewrite /r;bw; move => [y ydr]; bw. case /C3_P:ydr => ->; Ytac0; Ytac0; try move /set1_P ->; try case/set2_P => ->; apply /C4_P;in_TP4. rewrite /r; case /C4_P: ts; [set v := C0 | set v := C2 | set v := C1 | set v := C1 ]; move => ->; apply: (@setUb_i _ v); bw; Ytac0; Ytac0; fprops. (* property *) rewrite /s/r; bw;move => k kds; case /set2_P: kds =>->. exists C0 => //; bw; Ytac0; Ytac0 => t /set1_P ->; fprops. exists C2 => //; bw; Ytac0; Ytac0 => t /set1_P ->; fprops. (* not refinement *) move=> [_ _ ]; rewrite {1}/r;bw => cc. move: (cc _ rb) => [i]; rewrite /s; bw=> ids. rewrite /r; bw; Ytac0; Ytac0. case /set2_P: ids=> ->; bw => h. move: (h _ (set2_2 C2 C3)) => /set2_P; case; auto. move: (h _ (set2_1 C2 C3)) => /set2_P; case; auto. Qed. (** ** Section 5 *) (** Exercise 5.1: (french only) monotonicity of setP *) Lemma powerset_mono A B: sub A B -> sub (powerset A)(powerset B). Proof. move=> sAB t /setP_P ta; apply/setP_P; apply:(sub_trans ta sAB). Qed. Lemma exercise5_f1 x y: sub (powerset x) (powerset y) -> sub x y. Proof. move=> sxy z zx. have p2: sub (singleton z) y. by apply /setP_P; apply: sxy; apply /setP_P => t /set1_P ->. apply: (p2 z); fprops. Qed. (** Exercise 5.2 (french only): greatest and least fix-point *) Lemma exercise5_f2 f x v w: function f -> source f = (powerset x) -> target f = powerset x -> (forall a b, inc a (powerset x) -> inc b (powerset x) -> sub a b -> sub (Vf f a) (Vf f b)) -> v = intersection(Zo (powerset x) (fun z=> sub (Vf f z) z)) -> w = union(Zo (powerset x) (fun z=> sub z (Vf f z))) -> [/\ Vf f v = v, Vf f w = w & (forall z, sub z x -> Vf f z = z -> (sub v z /\ sub z w))]. Proof. move=> ff sf tf fprop vd wd. set (q:= (Zo (powerset x) (fun z => sub (Vf f z) z))). have xpx: inc x (powerset x) by apply :setP_Ti. have xiq: inc x q. apply: Zo_i=>//. by apply /setP_P; rewrite -tf; apply: Vf_target =>//; rewrite sf. have neq:nonempty q by exists x. set (p:= (Zo (powerset x) (fun z => sub z (Vf f z)))). have fzv:forall z, sub z x -> Vf f z = z -> sub v z. move => z zx Wz. have zq:inc z q by apply: Zo_i; [by apply /setP_P | rewrite Wz; fprops]. by rewrite vd; apply: setI_s1. have fzw:forall z, sub z x -> Vf f z = z -> sub z w. move => z zx Wz. have zp: inc z p by apply: Zo_i; [by apply /setP_P | rewrite Wz; fprops]. by rewrite wd; apply: setU_s1. have qW: forall z, inc z q -> inc (Vf f z) q. move=> z /Zo_P [] /setP_P zx Wzz. have aux := sub_trans Wzz zx. by apply: Zo_i; [ apply/setP_P | apply: fprop => //; apply/setP_P]. have pW: forall z, inc z p -> inc (Vf f z) p. move=> z /Zo_P [] /setP_P zx Wzz. have aux: inc (Vf f z) (powerset x). by rewrite -tf; apply: Vf_target=>//;rewrite sf; apply /setP_P. by apply: Zo_i => //; apply: fprop => //; apply/setP_P. have vp: inc v (powerset x) by apply /setP_P; rewrite vd; apply: setI_s1. have wp: inc w (powerset x). by apply /setP_P; rewrite wd; apply: setU_s2 => y /Zo_P []/setP_P. have pv:sub (Vf f v) v. move=> t tW; rewrite vd; apply: setI_i=>// y /Zo_P [yp sW]. have vy: sub v y by rewrite vd; apply: setI_s1; apply: Zo_i=>//. by apply: sW;apply: (fprop _ _ vp yp vy). have pw:sub w (Vf f w). move=> t; rewrite {1} wd=> /setU_P [y ty] /Zo_P [yp yW]. have tw: (sub y w) by rewrite wd;apply: setU_s1; apply: Zo_i=>//. by move: (fprop _ _ yp wp tw); apply; apply: yW. split. apply: extensionality=>//. have vq: (inc v q) by apply: Zo_i. by move: (qW _ vq)=> aux; rewrite {1} vd;apply: setI_s1. apply: extensionality=>//. have iwp: inc w p by apply: Zo_i. by move: (pW _ iwp) => aux; rewrite {2} wd;apply: setU_s1. move=> z zw wz; split; fprops. Qed. (** Exercise 5.1: Properties of product *) Lemma exercise5_1 I x y: (forall i, inc i I -> sub (y i) (x i)) -> nonempty I -> productf I y = intersectionf I (fun i=> Vfi (pr_i (Lg I x) i) (y i)). Proof. move=> syxi neI. have fgL: fgraph (Lg I x) by fprops. have fpj: forall j, inc j I-> function (pr_i (Lg I x) j). move=> j jI; apply: pri_f=>//;bw. set_extens t. move /setXf_P=> [fgt dt iVy]; apply: setIf_i=>//. move=> j jI; apply /iim_graph_P. exists (Vg t j); first by apply: iVy. have jd: inc j (domain (Lg I x)) by bw. have tp:(inc t (productb (Lg I x))). by apply/setXb_P; split; bw => i iI; bw; apply: syxi=>//; apply: iVy. by rewrite -(pri_V jd tp); Wtac; rewrite /pr_i lf_source. have rI: inc (rep I) I by apply: rep_i. move => h; move:(setIf_hi h rI) => /iim_graph_P [u uy Jg]. move: (p1graph_source (fpj _ rI) Jg). rewrite /pr_i;aw; move /setXf_P=>[fgt dt iVV]. apply/setXf_P;split => // i idt. move: (setIf_hi h idt) => /iim_graph_P [v vi Jgv]. move: (Vf_pr (fpj _ idt) Jgv); rewrite pri_V =>//; bw. by move=> <-. by apply/setXb_P; split; bw => k ki; bw; apply: iVV. Qed. (** Exercise 5.2: Powerset of a product *) Lemma exercise5_2 a b: bijection (Lf(fun g => Lg a (fun x => direct_image g (singleton x))) (powerset (a \times b)) (gfunctions a (powerset b))). Proof. set tilde := Lf _ _. apply: lf_bijective. move=> c /setP_P cp; apply:gfunctions_i1 => t ta; apply/setP_P => u. by move /dirim_P => [x _ pb]; move/setXp_P: (cp _ pb) => []. move => u v; set fx := Lg a _; set fy:= Lg a _. move /setP_P => up /setP_P => vp fxy. set_extens x => xs. move /setX_P: (up _ xs) => [px Px Qx]. have: inc (Q x) (Vg fy (P x)). by rewrite -fxy /fx; bw; apply/dirim_P; ex_tac; rewrite px. by rewrite /fy; bw; move/dirim_P=> [w /set1_P ->]; rewrite px. move /setX_P: (vp _ xs) => [px Px Qx]. have: inc (Q x) (Vg fx (P x)). by rewrite fxy /fy; bw; apply/dirim_P; ex_tac; rewrite px. by rewrite /fx; bw; move/dirim_P=> [w /set1_P ->]; rewrite px. move=> y ys; move: (gfunctions_hi ys)=> [f [fs sf tg gf]]. set (g:=Zo (a \times b) (fun z => inc (Q z) (Vg y (P z)))). have gp: inc g (powerset (a \times b)) by apply/setP_P;apply: Zo_S. rewrite -gf; ex_tac; apply: fgraph_exten; fprops. bw; aw. red; rewrite - (proj33 fs) sf => x xa; bw;rewrite gf;set_extens u. move=> h; apply/dirim_P; exists x; first by fprops. apply: Zo_i; aw; apply: setXp_i => //. rewrite - sf in xa; move: (Vf_target fs xa). by rewrite tg /Vf gf; move/setP_P; apply. move /dirim_P => [v /set1_P ->] /Zo_P []; aw. Qed. (** Exercise 5.3: TODO *) (** ** Section 6 *) (** Exercise 6.1: Characterisation of equivalence *) Lemma exercise6_1 x g: sgraph g -> ((equivalence g /\ substrate g = x) <-> [/\ domain g = x, range g = x, g \cg ((inverse_graph g) \cg g) = g & sub (diagonal x) g]). Proof. move=> gg; split. move=> [eg sg]; split => //. - by rewrite (domain_sr eg). - rewrite - sg /substrate; set_extens t => ts; first by fprops. case /setU2_P:ts => // /(domainP gg) [y Jh]; apply/(rangeP gg). exists y; equiv_tac. - set_extens y. move /compg_P => [py [z /compg_pP [u pa /igraph_pP pb pc]]]. have J4: inc (J u z) g by equiv_tac. have J5: inc (J (P y) z) g by equiv_tac. have: inc (J (P y) (Q y)) g by equiv_tac. by rewrite py. move=> yg. have py: pairp y by apply: gg. have yv:J (P y) (Q y) = y by aw. rewrite - py; apply /compg_pP; exists (P y); last by ue. apply /compg_pP; exists (Q y); [| apply/igraph_pP]; ue. - move => t /diagonal_i_P [pt Pt PQt]. by rewrite -pt -PQt; rewrite - sg in Pt; equiv_tac. move=> [dg rg cg si]. have sg: (substrate g = x) by rewrite /substrate dg rg; apply: setU2_id. split=>//. have p1: forall u, inc u x -> inc (J u u) g. by move=> u ux; apply: si; apply /diagonal_pi_P. have p2: symmetricp g. move=> a b ab; red in ab. have Jag: (inc (J a a) g) by apply: p1; rewrite -dg; aw; ex_tac. have Jbg: (inc (J b b) g) by apply: p1; rewrite -rg; aw; ex_tac. rewrite -cg; apply /compg_pP; ex_tac; apply /compg_pP; ex_tac. by apply /igraph_pP. have p3: transitivep g. move => a b c ab bc; rewrite -cg; apply /compg_pP. exists a => //; apply /compg_pP; exists b => //. by apply: p1; rewrite - sg; substr_tac. by apply/igraph_pP; apply p2. by apply:symmetric_transitive_equivalence. Qed. (** Exercise 6.2: equivalence from a graph *) Lemma exercise6_2 g: sgraph g -> g \cg ( (inverse_graph g) \cg g) = g -> [/\ equivalence ((inverse_graph g) \cg g), substrate ((inverse_graph g) \cg g) = domain g, equivalence (g \cg (inverse_graph g)) & substrate (g \cg (inverse_graph g)) = range g]. Proof. move=> gg cg. have gig:sgraph (inverse_graph g) by apply: igraph_graph. have gcigg:sgraph ((inverse_graph g) \cg g) by apply: compg_graph. have gcgig: sgraph (g \cg (inverse_graph g)) by apply: compg_graph. have t3:forall x y z t, related g x y -> related g z y -> related g z t -> related g x t. move=> x y z t xy zy zt; rewrite -cg; apply/compg_pP. by exists z=>//;apply/compg_pP;exists y => //;apply /igraph_pP. have s1: substrate ((inverse_graph g) \cg g) = domain g. set_extens x. case /(substrate_P gcigg) => [] [y /compg_pP [z J1] /igraph_pP J2]; ex_tac. move/(domainP gg) => [y Jg]. have Jxx: (inc (J x x) ((inverse_graph g) \cg g)). by apply/compg_pP; ex_tac; apply /igraph_pP. apply: (arg1_sr Jxx). have s2:substrate (g \cg (inverse_graph g)) = range g. set_extens x. case/(substrate_P gcgig)=> [][y /compg_pP [z /igraph_pP J1 J2]]; ex_tac. move/(rangeP gg) => [y Jg]. have Jxx: (inc (J x x) (g \cg (inverse_graph g))). by apply/compg_pP; ex_tac; apply /igraph_pP. apply: (arg1_sr Jxx). split => //; rewrite equivalence_pr; split; try rewrite compg_inverse igraph_involutive //. by rewrite - compgA cg. by rewrite compgA in cg; by rewrite compgA cg. Qed. (** Exercise 6.3: equivalence associated to [a \cap c] *) Definition intersection_with x a := Lf (intersection2 a) (powerset x)(powerset x). Definition intersection_with_canon x a := Lf (fun b => Zo (powerset x)(fun c=> b = a \cap c)) (powerset a)(quotient (equivalence_associated (intersection_with x a))). Lemma exercise6_3 a x: sub a x -> bijection (intersection_with_canon x a). Proof. move=> ax. have ta: lf_axiom (intersection2 a) (powerset x) (powerset x). move=> y /setP_P ay; apply /setP_i;apply: sub_trans ay ;apply: subsetI2r. have fai: function (intersection_with x a) by apply: lf_function. move:(graph_ea_equivalence fai). set r:= equivalence_associated (intersection_with x a); move => [er sr]. have rr: forall u v, related r u v <-> [/\ inc u (powerset x), inc v (powerset x) & a \cap u = a \cap v]. move => u v; split. move/(ea_relatedP fai); rewrite lf_source; move => [pa pb]. by rewrite /intersection_with; aw. move => [pa pb pc]; apply/(ea_relatedP fai). by rewrite /intersection_with; aw. have aux: forall y, sub y a -> y = a \cap y by move => y; move/setI2id_Pr. apply: lf_bijective. move=> y /setP_P=> ya;set w:= Zo _ _ . have new: nonempty w. exists y;apply: Zo_i; [apply/setP_P; apply: (sub_trans ya ax) | auto]. have swp: sub w (powerset x) by apply: Zo_S. have rp: inc (rep w) (powerset x) by apply: swp;apply: rep_i. apply /(setQ_P er); split => //. move: rp;rewrite sr /intersection_with; aw. have ira: (a \cap (rep w) = y). have: (inc (rep w) w) by apply: rep_i. by move /Zo_hi => ->. set_extens z. move=> zw; apply /(class_P er); apply /rr;split => //; first by apply:swp. by rewrite ira; move /Zo_P: zw => []. by move/(class_P er)/rr => [pa pb pc]; apply: Zo_i => //; rewrite -pc ira. move=> u v /setP_P ua /setP_P va; set fs:= Zo _ _ => eql. have iua: u = a \cap u by apply: aux. have: inc u fs by apply: Zo_i => //; apply/setP_P; apply:(sub_trans ua ax). by rewrite eql; move/ Zo_hi => ->. move=> y /(setQ_P er) cy. have ip: inc (a \cap (rep y)) (powerset a) by apply/setP_P; apply subsetI2l. move: sr; rewrite lf_source => sr2. ex_tac; symmetry;set_extens t. move /Zo_P => []; move /setP_P => pd pe. apply: (rel_in_class2 er cy); apply/rr;split => //; last by apply /setP_P. rewrite - sr2; exact (proj1 cy). move => ty; apply /Zo_i; first by rewrite - sr2; apply: (sub_class_sr er cy ty). by move: (rel_in_class er cy ty) => /rr [_ _]. Qed. (** Exercise 6.4: some properties of equivalence: composition, intersection *) Lemma exercise6_4 g a b x: let comm F G b := F (G b) = G (F b) in equivalence g -> sgraph a -> sgraph b -> substrate g = x -> sub a g -> [/\ (domain a = x -> g \cg a = g), (range a = x -> a \cg g = g), (domain a = x -> comm (composeg^~a) (intersection2 g) b) & (range a = x -> comm (composeg a) (intersection2 g) b)]. Proof. move=> comm eg ga gb sg ag. have gg: sgraph g by fprops. split. + move=> ax; set_extens y. move /compg_P=> [py [z J1a J2g]]. move: (ag _ J1a) => J1g. rewrite - py; equiv_tac. move=> yg; move: (gg _ yg)=> py; apply/compg_P. split =>//. have : (inc (P y) (domain a)) by rewrite ax - sg; substr_tac. move/(domainP ga)=> [z Ja]; exists z =>//. move: (ag _ Ja)=> Jg. have J2g:inc (J z (P y)) g by equiv_tac. rewrite - py in yg; equiv_tac. + move=> ax; rewrite /comp; set_extens y. move /compg_P => [py [z J1g J2a]]. move: (ag _ J2a) => J2g. rewrite - py; equiv_tac. move=> yg; move: (gg _ yg)=> py; apply/compg_P =>//. have : (inc (Q y) (range a)) by rewrite ax - sg; substr_tac. move/(rangeP ga); move=> [z Ja]; split => //;exists z =>//. move: (ag _ Ja)=> Jg. have J2g:inc (J (Q y) z) g by equiv_tac. rewrite - py in yg; equiv_tac. + move=> ax; set_extens y. move /compg_P => [py [z J1a/setI2_P [J2g J3b]]]; apply/setI2_i. move: (ag _ J1a) => J1g; rewrite - py; equiv_tac. apply/compg_P;split=>//;exists z=>//. move=> /setI2_P [yg] /compg_P [py [z J1a J2b]]. apply/compg_P; split => //; exists z => //; apply:setI2_i => //. move: (ag _ J1a)=> Jg. have J2g:inc (J z (P y)) g by equiv_tac. rewrite - py in yg; equiv_tac. + move=> ax; set_extens y. move /compg_P => [py [z /setI2_P [J2g J3b] J1a]]; apply/setI2_i. move: (ag _ J1a) => J1g; rewrite - py; equiv_tac. apply/compg_P;split=>//;exists z =>//. move=> /setI2_P [yg] /compg_P [py [z J1a J2b]]. apply/compg_P; split => //; exists z => //; apply:setI2_i => //. move: (ag _ J2b)=> Jg. have J2g:inc (J (Q y) z) g by equiv_tac. rewrite - py in yg; equiv_tac. Qed. (** Exercise 6.5: intersection of equivalence is equivalence. We show here that union is not *) Lemma symmetric_union a b: symmetricp a -> symmetricp b -> symmetricp (a \cup b). Proof. by move=> sa sb x y; case /setU2_P=> h; apply/setU2_P; [left; apply: sa | right; apply: sb ]. Qed. Lemma substrate_union_diag x g: sub g (coarse x) -> substrate (g \cup (diagonal x)) = x. Proof. move=> gc. have gg: sgraph g by move=> t tg; move: (gc _ tg) => /setX_P []. have gu: sgraph (g \cup (diagonal x)). by move=> t; case /setU2_P; [ auto | move/diagonal_i_P => []]. set_extens y. case /(substrate_P gu) => [] [z] /setU2_P []. - by move => h; move: (gc _ h); move /setXp_P=> []. - by move/diagonal_pi_P => []. - by move => h; move: (gc _ h); move /setXp_P=> []. - by move/diagonal_pi_P => [ h <-]. move=> yx. have aux: inc (J y y) (g \cup (diagonal x)). by apply: setU2_2; apply /diagonal_pi_P; split. substr_tac. Qed. Definition special_equivalence a b x := (doubleton (J a b) (J b a)) \cup (diagonal x). Lemma substrate_special_equivalence a b x: inc a x -> inc b x -> substrate(special_equivalence a b x) = x. Proof. move=> ax bx; rewrite/ special_equivalence. apply: substrate_union_diag. by move=> t /set2_P => [][] ->; apply/setXp_i. Qed. Lemma special_equivalence_ea a b x: inc a x -> inc b x -> equivalence(special_equivalence a b x). Proof. move=> ax bx. have gs: sgraph (special_equivalence a b x). move=> t; move/setU2_P; case; first by case/set2_P => ->; fprops. by move /diagonal_i_P => []. have pair_symm: forall a b c d, J a b = J c d -> J b a = J d c. move=> u v u' v' eql. apply: pair_exten; fprops; aw. apply: (pr2_def eql). apply: (pr1_def eql). apply: symmetric_transitive_equivalence => //. move=> u v h; case/setU2_P: (h). case /set2_P => ww; apply/setU2_P; left; rewrite (pr1_def ww)(pr2_def ww); fprops. by move => /diagonal_pi_P [_ uv]; move: h;rewrite uv. move=> u v w ra rb. case /setU2_P: (ra); last by move => /diagonal_pi_P [_ ->]. case /setU2_P: (rb); last by move => /diagonal_pi_P [_ <-]. move => h1 h2; apply/setU2_P. case /set2_P: h1 => h11; rewrite (pr2_def h11); case /set2_P: h2 => h22; rewrite (pr1_def h22). - left; fprops. - by right; apply /diagonal_pi_P. - by right; apply /diagonal_pi_P. - left; fprops. Qed. Lemma exercise6_5 (x := C3) (g1:= special_equivalence C0 C1 x) (g2:= special_equivalence C0 C2 x): [/\ equivalence g1, equivalence g2, substrate g1 = x, substrate g2 = x & ~ (equivalence (g1 \cup g2))]. Proof. split. apply: special_equivalence_ea; apply /C3_P; in_TP4. apply: special_equivalence_ea; apply /C3_P; in_TP4. rewrite substrate_special_equivalence //; apply /C3_P; in_TP4. rewrite substrate_special_equivalence //; apply /C3_P; in_TP4. move=> bad. have p1: (related (g1 \cup g2) C1 C0). apply /setU2_P; left;apply/setU2_P; left; fprops. have p2: (related (g1 \cup g2) C0 C2). apply /setU2_P; right;apply/setU2_P; left; fprops. have :(related (g1 \cup g2) C1 C2) by equiv_tac. move: C2_ne_C01 => [n1 n2]. case /setU2_P; case/setU2_P. by case/set2_P=> eq2; move: (pr2_def eq2); auto. by move /diagonal_pi_P => [_]; auto. by case/set2_P=> eq2; move: (pr1_def eq2); fprops. by move /diagonal_pi_P => [_]; auto. Qed. (** Exercise 6.6: Commposition of two equivalences; if it is an equivalence, it is the supremum *) Lemma exercise6_6a G H: equivalence G -> equivalence H -> (equivalence (G \cg H) <-> (G \cg H = H \cg G)). Proof. move=> eG eH. set (K:= G \cg H). split. move => eK. have aux a b: inc (J a b) K -> inc (J b a) K by move => h;equiv_tac. set_extens x => xK. have px: (pairp x) by apply: (@compg_graph G H). move: xK ; rewrite - px => /aux. move /compg_pP=> [y JH JG]; apply/compg_pP; exists y => //; equiv_tac. move: xK =>/compg_P [px [y JG JH]]. rewrite - px; apply: aux; apply/compg_pP;exists y => //; equiv_tac. move=> eq. move: eG eH; rewrite ! equivalence_pr. move=> [GG iG] [HH iH]; split. by rewrite {2} /K compgA eq - (compgA H G G) GG - compgA -/K eq compgA HH. by rewrite {2}/K compg_inverse -iH -iG. Qed. Lemma exercise6_6b G H: equivalence G -> equivalence H -> substrate G = substrate H -> substrate (G \cg H) = substrate G. Proof. move=> eG eH sG. set_extens x. have xx:sgraph (G \cg H) by fprops. case /setU2_P; [move /(domainP xx) | move /(rangeP xx)]; move => [z] /compg_pP [t ta tb]; [rewrite sG | ] ; substr_tac. move=> xsG. have p3: related (G \cg H) x x. apply/compg_pP; exists x;equiv_tac => //; ue. substr_tac. Qed. Lemma exercise6_6c G H: equivalence G -> equivalence H -> substrate G = substrate H -> [/\ sub G (G \cg H), sub H (G \cg H) & forall W, equivalence W -> sub G W -> sub H W -> sub (G \cg H) W]. Proof. move=> eG eH sG. have gg: sgraph G by fprops. have gh: sgraph H by fprops. have gc: sgraph (G \cg H) by apply: compg_graph. split. - move=> y yG. move: (gg _ yG) => py. rewrite - py in yG. apply/ compg_P;split=>//;exists (P y) => //; equiv_tac=>//. rewrite - sG; substr_tac. - move=> y yH. move: (gh _ yH) => py. rewrite - py in yH. apply/compg_P; split=>//;exists (Q y)=>//; equiv_tac=>//. rewrite sG; substr_tac. - move=> w ew gW hW t. move /compg_P=> [tp [y JH JG]]. move: (gW _ JG) (hW _ JH)=> J1G J2G. have: inc (J (P t) (Q t)) w by equiv_tac. by rewrite tp. Qed. Lemma range_is_substrate g: equivalence g -> range g = substrate g. Proof. move=> eg; rewrite /substrate; set_extens x. move => pa; fprops. move:(eg) => [fgg _ _ _]. case /setU2_P => //; move /(domainP (proj41 eg))=> [y Jg]. apply/(rangeP fgg); exists y; equiv_tac. Qed. Lemma sub_coarse g: equivalence g -> sub g (coarse (substrate g)). Proof. move=> eg; move: (sub_graph_setX (proj41 eg)). by rewrite range_is_substrate // domain_sr. Qed. Lemma exercise6_6d G H: equivalence G -> equivalence H -> substrate G = substrate H -> G \cg H = H \cg G -> (G \cg H) = intersection(Zo (powerset (coarse (substrate G))) (fun W => [/\ equivalence W, sub G W & sub H W])). Proof. move=> eG eH sG cGH. set (E:= substrate G). have sGE: sub G (coarse E) by apply: sub_coarse. have sHE: sub H (coarse E) by rewrite /E sG; apply: sub_coarse. move: (exercise6_6c eG eH sG)=> [sGc sHc lew]. set_extens t => ts. apply: setI_i. exists (coarse E); apply: Zo_i; first by apply: setP_Ti. split=> //;apply: proj1 (coarse_equivalence E). by move=> y /Zo_P [_ [ey gy hy]]; apply: (lew _ ey gy hy). move: cGH;rewrite - exercise6_6a // => cGH. apply: (setI_hi (y:=(G \cg H)) ts); apply: Zo_i; last by done. apply /setP_P;rewrite /E - (exercise6_6b eG eH sG); apply: sub_coarse=>//. Qed. (** Exercise 6.7: Is this property true ? *) Remark exercise6_7 G0 G1 H0 H1 E x: equivalence G0 -> substrate G0 = E -> equivalence H0 -> substrate H0 = E -> equivalence G1 -> substrate G1 = E -> equivalence H1 -> substrate H1 = E -> G1 \cap H0 = G0 \cap H1 -> G1 \cg H0 = G0 \cg H1 -> inc x E -> ( let G1x := direct_image G1 (singleton x) in let H1x := direct_image H1 (singleton x) in let R0 := induced_relation G0 G1x in let S0 := induced_relation H0 H1x in equipotent (quotient R0) (quotient S0)). Proof. Abort. (** Exercise 6.8: Inverse image of an equivalence *) Lemma exercise6_8 f r: equivalence r -> function f -> target f = substrate r -> (exists g, bijection_prop g (quotient (inv_image_relation f r)) (quotient (induced_relation r (Imf f)))). Proof. move => er ff tf. set (s := inv_image_relation f r). set (A:= (Imf f)). set (Ra := induced_relation r A). have ia: (iirel_axioms f r) by []. have rf: A = range (graph f). rewrite /A/Imf -image_by_fun_source //. have [es _]:= (iirel_relation ia). have iA: induced_rel_axioms r A. by split =>//; rewrite -tf rf; apply: corresp_sub_range; case: ff. have [eR _]:=(induced_rel_equivalence iA). set (f1:= fun x y => [/\ classp r y, nonempty (y \cap A) & x = Vfi f y]). have qsp:forall x, inc x (quotient s) -> exists y, f1 x y. by move=> x /(setQ_P es); move /(iirel_classP ia); rewrite -rf. set (f2:= fun x => choose (fun y => f1 x y)). have f2p: (forall x, inc x (quotient s) -> f1 x (f2 x)). move=> x xq; rewrite /f2;apply: choose_pr; apply: (qsp _ xq). set (f3:= fun x => (f2 x) \cap A). have f3p: (forall x, inc x (quotient s) -> inc (f3 x) (quotient Ra)). move=> x xs; rewrite /Ra; move: (f2p _ xs) => [pa pb pc]. apply/(setQ_P eR); apply/(induced_rel_classP iA). by exists (f2 x). set (g:= Lf f3 (quotient s) (quotient Ra)). have sgf: sgraph (graph f) by fprops. exists g; rewrite /g;split; aw; apply: lf_bijective => //. move => u v uq vq; rewrite /f3 => ii. move: (f2p _ uq)(f2p _ vq); rewrite /f1; move=> [cfu niu uv][cfv niv vv]. move: niv=> [y] /setI2_P [y2v yiA]. have y2u: inc y (f2 u). apply: (@setI2_1 (f2 u) A);rewrite ii; fprops. have : inc y (range (graph f)) by rewrite -rf. move /(rangeP sgf)=> [x Jg]. have xb: (inc x v) by rewrite vv; apply/iim_graph_P;ex_tac. have xu:(inc x u) by rewrite uv; apply/iim_graph_P; ex_tac. move : uq vq; move/(setQ_P es) => c1 /(setQ_P es) => c2. by case: (class_dichot es c1 c2) => // dj; empty_tac1 x. move=> y; move /(setQ_P eR) /(induced_rel_classP iA)=> [x [cx nex yi]]. set (u:= Vfi f x). have uq: inc u (quotient s). by apply/ (setQ_P es) /(iirel_classP ia); exists x; rewrite -rf. ex_tac. rewrite /f3 yi. move:(f2p _ uq); rewrite /f1; move=> [cf2 ni ui]. move: nex=> [t] /setI2_P [tx]. rewrite {1} rf ; move/ (rangeP sgf)=> [z Jg]. have: inc z u by apply/iim_graph_P; ex_tac. rewrite {1} ui; move/iim_graph_P => [t' t'2u Jg']. have tt': t = t' by move: (Vf_pr ff Jg) (Vf_pr ff Jg') => <-. suff: f2 u = x by move->. case:(class_dichot er cf2 cx)=> // di. by empty_tac1 t ;rewrite tt'. Qed. (** Exercise 6.9: decomposition of some function *) Lemma exercise6_9 F G p f r: equivalence r -> F = substrate r -> p = canon_proj r -> surjection f -> source f = G -> target f = quotient r -> exists E g h, [/\ surjection_prop g E F, surjection_prop h E G & p \co g = f \co h]. Proof. move=> er sr xr sjf sf tf. have ff: function f by fct_tac. have ba:= C1_ne_C0. set Ea:= F \times (singleton C0). set Eb:= G \times (singleton C1). set E:= Ea \cup Eb. have gE: sgraph E by move => T /setU2_P; case; move /setX_P => [ok _]. have xep: forall x, inc x E -> (Q x = C0 \/ Q x = C1). move=> x /setU2_P; case; move /setX_P => [_ _ ] /set1_P ->; fprops. have xgp:forall x, inc x G -> inc (Vf f x) (quotient r). move=> x xg; rewrite - tf;apply: Vf_target => //; ue. have xgp1:forall x, inc x G -> inc (rep (Vf f x)) F. move=> x xG; rewrite sr;fprops. set (gz :=fun z=> Yo (Q z = C0) (P z) (rep (Vf f (P z)))). have gzP:forall z, inc z Ea -> gz z = P z. move=> z /setX_P [_ _] /set1_P h; rewrite /gz Y_true //. have gzp': forall z, inc z Ea -> inc (gz z) F. by move=> z zEa; rewrite gzP//; move /setX_P : zEa => [_ ok _]. have gzQ:forall z, inc z Eb -> gz z = rep (Vf f (P z)). move=> z/setX_P [_ _] /set1_P => h; rewrite /gz Y_false //; ue. have gzq':forall z, inc z Eb -> inc (gz z) F. by move=> z zE; rewrite gzQ //; apply: xgp1; move /setX_P : zE => [_ ok _]. have tag:lf_axiom gz E F. move=> t; case /setU2_P; [apply: gzp'| apply: gzq']. set (g:= Lf gz E F). have sj: surjection g. rewrite /g;apply: lf_surjective =>//; move=> y yF. have p1: inc (J y C0) Ea by rewrite /Ea; fprops. have p2: inc (J y C0) E by rewrite /E; aw;fprops. by ex_tac; rewrite gzP; aw. have gp: forall x, inc x Eb -> Vf (canon_proj r) (gz x) = Vf f (P x). move=> x xEb. have gzs: inc (gz x) (substrate r) by rewrite - sr; apply: gzq'. have xE: inc x E by move: xEb; rewrite /E;aw; intuition. aw;rewrite gzQ //; apply: class_rep=>//; apply: xgp. by move /setX_P : xEb => [_ ok _]. set (ha:= fun x => rep (Vfi1 f (Vf (canon_proj r) x))). have haF:forall x, inc x F -> ha x = rep (Vfi1 f (class r x)). move=> x xF; rewrite /ha; aw; ue. have haF':forall x, inc x F -> sub (Vfi1 f (class r x)) G. move=> x xF t /iim_graph_P [u _ jg]; rewrite - sf; Wtac. have haF'': forall x, inc x F -> inc (ha x) (Vfi1 f (class r x)). move => x xF; rewrite haF //; apply: rep_i. have ct: inc (class r x) (target f) by rewrite tf; rewrite sr in xF; fprops. move:((proj2 sjf) _ ct)=> [u us]; move => <-. exists u; apply /iim_graph_P; ex_tac; apply: Vf_pr3=>//. have haG: forall x, inc x F -> inc (ha x) G. by move=> x xF; apply: (haF' _ xF); apply: haF''. set(hz:= fun z=> Yo (Q z = C0) (ha (P z)) (P z)). have hzG: forall z, inc z E -> inc (hz z) G. rewrite /hz;move=> z /setU2_P [] /setX_P [_ pa] /set1_P ->; Ytac0 => //. by apply: haG. set(h:=Lf hz E G). have sh: surjection h. rewrite /h;apply: lf_surjective=>// y yG. have JEb:inc (J y C1) Eb by rewrite /Eb;aw; fprops. have JE: (inc (J y C1) E) by rewrite /E; aw; fprops. by ex_tac; rewrite /hz; aw; rewrite Y_false. have WWh: forall x, inc x Ea -> Vf f (hz x) = Vf (canon_proj r) (P x). move=> x xEa. have xE: inc x E by rewrite /E; aw; intuition. have Ps: inc (P x) (substrate r) by rewrite - sr -gzP//; apply: gzp'. rewrite /hz; aw. move /setX_P: xEa=> [px PF] /set1_P ->; Ytac0. move /iim_graph_P: (haF'' _ PF) => [u ] /set1_P <- Jg; Wtac. exists E; exists g; exists h; rewrite /surjection_prop/g/h;aw;split => //. have cpg: p \coP g. split; first by rewrite xr;apply: canon_proj_f. by fct_tac. rewrite xr /g; aw; ue. have cfh: composable f h by split => //; try fct_tac; rewrite /h; aw. have sg: source g = source h by rewrite /g/h; aw. have tp: target p = target f by rewrite xr; aw. move: sj => [fg _]. apply: function_exten; try fct_tac; aw. move=> x xE /=; aw. move /setU2_P: (xE) => [] xE'. have Ps: inc (P x) (substrate r) by rewrite - sr -gzP //; apply: gzp'. rewrite WWh // /g; aw; rewrite gzP // xr; aw. rewrite xr gp /h /hz; aw =>//; rewrite Y_false //. by move /setX_P: xE'=> [_ _ ] /set1_P ->. Qed. (** Exercise 6.10: least equivalence associated to a relation; connected components *) Lemma set1_pr2 a X: inc a X -> small_set X -> X = singleton a. Proof. by move => tX sX; apply (set1_pr tX) => u zX; exact: (sX _ _ zX tX). Qed. Section Exercise6_10. Lemma Exercise6_10_a (r: relation): symmetric_r (fun x y => r x y /\ r y x). Proof. by move=> x y; case. Qed. Lemma exercise6_10_b r E: reflexive_re r E -> reflexive_re (fun x y => r x y /\ r y x) E. Proof. move => rr y; split; [by move/rr | by case; move /rr]. Qed. Variables (R:relation) (E:Set). Hypotheses (A1: reflexive_re R E)(A2: symmetric_r R) (A3: forall x y, R x y -> inc x E). (** Let [setF] be the set of all [A] such that that no element of [A] is related to an element of the complementary; let [connected_comp x] be the intersection of all [A] that contains [x] this is the class of [x] for [relS] *) Definition setF:= Zo (powerset E)(fun A => forall y z, inc y A -> inc z (E -s A) -> not (R y z)). Definition connected_comp x := intersection(Zo setF (fun A => inc x A)). Lemma setF_pr A a b: inc A setF -> inc a A -> R a b -> inc b A. Proof. move /Zo_P => [] /setP_P AE Ap aA Rab. case: (inc_or_not b A)=> // nba. have bc: inc b (E -s A) by apply:setC_i =>//; apply: (A3 (A2 Rab)). by case: (Ap _ _ aA bc). Qed. Lemma setF_pr2 A a b: inc A setF -> inc a A -> chain_related R a b -> inc b A. Proof. move=> As aA [c [cc hcx <-]]. rewrite - hcx in aA; clear hcx. elim: c cc aA. move=> u v /= Ruv uA; apply: (setF_pr As uA Ruv). move=> u c h /= [uh cc] uA. apply: h=>//;apply: (setF_pr As uA uh). Qed. Lemma setF_pr3 A a: inc A setF -> inc a A -> sub (class (chain_equivalence R E) a) A. Proof. move:(chain_equivalence_eq A1 A2 A3)=> [es sr]. move=> As aA t /(class_P es) /graph_on_P1 [_ _ ]. apply: (setF_pr2 As aA). Qed. Lemma setF_pr0 a b: R a b -> related (chain_equivalence R E) a b. Proof. move => rab. move:(A3 rab) (A3 (A2 rab)) => aE bE. by apply/graph_on_P1; split => //;exists (chain_pair a b). Qed. Lemma setF_pr4 a: inc a E -> inc (class (chain_equivalence R E) a) setF. Proof. move=> aE; rewrite /setF. move:(chain_equivalence_eq A1 A2 A3)=> [es sr]. apply: Zo_i. apply/setP_P; rewrite - {2} sr; apply: (sub_class_substrate es). move=> y z ya /setC_P [zE nzc]; dneg yz; apply/(class_P es). move/(class_P es):ya => way; exact: (proj43 es y _ _ way (setF_pr0 yz)). Qed. Lemma connected_comp_class x: inc x E -> class (chain_equivalence R E) x = connected_comp x. Proof. move=> xE;set_extens t; rewrite /connected_comp. move=> tc;apply: setI_i. exists E; apply: Zo_i =>//; rewrite /setF; apply: Zo_i. aw; apply /setP_Ti. by move=> y z yE /setC_P []. move=> y /Zo_P [yS xy];apply: ((setF_pr3 yS xy) _ tc). move:(chain_equivalence_eq A1 A2 A3)=> [eq sr]. have cx:inc (class (chain_equivalence R E) x) (Zo setF (fun A => inc x A)). apply: Zo_i; first by apply: setF_pr4. apply/(class_P eq); rewrite - sr in xE; equiv_tac. move=> h;apply: (setI_hi h cx). Qed. (** Exercise 6.11: Intransitive relations of order [n]. Given [n+4] distinct elements [x(i)], if for all pairs but one, [x(i)] is related to [x(j)], then the last pair is related too. We consider only the case [n=1]. The relation [R] is assumed reflexive and symmetric. We give here an alternate definition, assuming only one inequality *) Definition intransitive1 := forall x y z t, x <> y -> R x y -> R x z -> R x t -> R y z -> R y t -> R z t. Lemma intransitive1pr : let intransitive_alt:= forall x y z t, x <> y -> x <> z -> x <> t -> y <> z -> y <> t -> z <> t -> inc x E -> inc y E -> inc z E -> inc t E -> R x y -> R x z -> R x t -> R y z -> R y t -> R z t in intransitive1 <-> intransitive_alt. Proof. rewrite /intransitive1; split. move=> h x y z t H0 _ _ _ _ _ _ _ _ _ H10 H11 H12 H13 H14. apply: (h x y z t H0 H10 H11 H12 H13 H14). move=> h x y z t nxy xy xz xt yz yt. move: (A3 xy) (A3 yz)(A3 (A2 xz))(A3 (A2 yt)) => xE yE sE tE. case: (equal_or_not x z) => nxz; first by ue. case: (equal_or_not x t) => nxt; first by apply: A2; ue. case: (equal_or_not y z) => nyz; first by ue. case: (equal_or_not y t) => nyt; first by apply: A2; ue. case: (equal_or_not z t)=> nzt; first by rewrite nzt -A1. apply: (h x y z t) =>//. Qed. (** Let [Cab a b] be the set of elements related to both [a] and [b], assuming [a] and [b] related. It is stable by [R]; [a] and [b] can be replaced by any element of [Cab] *) Definition stableR A:= forall a b, inc a A -> inc b A -> R a b. Definition Cab a b:= Zo E (fun x => R a x /\ R b x). Lemma Cab_stable a b: a<> b -> R a b -> intransitive1 -> stableR (Cab a b). Proof. move=> nab Rab i1; rewrite /Cab=> u v. move /Zo_P=> [_ [r1 r2]] /Zo_P [_ [r3 r4]]; apply: (i1 a b u v) =>//. Qed. Lemma Cab_trans a b x y: a<> b -> R a b -> intransitive1 -> x<> y -> inc x (Cab a b) -> inc y (Cab a b) -> (Cab a b)= (Cab x y). Proof. move=> nab rab i1 nxy /Zo_P [xE [r1 r2]] /Zo_P [yE [r3 r4]]. set_extens t; move /Zo_P=> [tE [r5 r6]]; apply/Zo_i => //; split. - apply: (i1 a b x t) =>//. - apply: (i1 a b y t) =>//; apply: A2. - apply: (i1 x y a t) =>//; first apply: (i1 a b x y)=>//; apply: A2=> //. - apply: (i1 x y b t) =>//; first apply: (i1 a b x y)=>//; apply: A2=> //. Qed. (** A set [X] is said to be a constituant if it is [Cab] or a connected component (a class for [relS]) that is a singleton *) Definition is_constituant A := (exists a, [/\ A = singleton a, inc a E & forall b, R a b -> a = b]) \/ (exists a b, [/\ A = Cab a b, a<> b & R a b]). Lemma singleton_component A: sub A E -> ( (inc A (quotient (chain_equivalence R E) ) /\ singletonp A) <-> (exists2 a, A = singleton a & forall b, R a b -> a = b)). Proof. move=> AE. move:(chain_equivalence_eq A1 A2 A3)=> [eq sr]. split. move=> [Asq [x Asx]]; exists x => //. move=> b /setF_pr0. move /(in_class_relatedP eq) => [y [cy xy]]. have <- : A = y. move: Asq => /(setQ_P eq) => cA; case: (class_dichot eq cy cA)=> //. move=> dy; red in dy; empty_tac1 x; apply:setI2_i => //. rewrite Asx; fprops. by rewrite Asx; move /set1_P. move=> [x As Ap]; rewrite As; split; last by exists x. have xse: inc x (substrate (chain_equivalence R E)). rewrite sr; apply: AE; rewrite As; fprops. have Aq: forall b, R b x -> b = x. by move => b ba; rewrite (Ap b) //; apply: A2. suff: (class (chain_equivalence R E) x = singleton x). move => <-; apply /(setQ_P eq); apply: (class_class eq xse). apply: set1_pr; first by apply /(class_P eq); equiv_tac. move => w; move /(class_P eq) => /(proj44 eq). move/graph_on_P1 => [ pa qa [c [cc <-]]]. elim: c cc. by move=> u v /= uv vx; rewrite vx in uv; apply: Aq. by move=> p c h1 /= [Rp cc] tc; apply: Aq; rewrite - (h1 cc tc). Qed. (** The intersection of two distinct constituants is empty or a singleton *) Lemma constituant_inter2 A B: is_constituant A -> is_constituant B -> intransitive1 -> A = B \/ small_set (A \cap B). Proof. move=> cA cB i1. case: (equal_or_not A B); first (by left); move => AB;right; move=> u v. case: cA. move=>[a [Aa aE ap]]; rewrite Aa. by move/setI2_P => [/set1_P -> _] /setI2_P [/set1_P -> _]. case: cB. move=>[c [Ac cE cp]] _; rewrite Ac. by move/setI2_P => [_ /set1_P ->] /setI2_P [_ /set1_P ->]. move=> [a [b [Aab nab Rab]]] [a' [b' [Aab' nab' Rab']]]. case: (equal_or_not u v)=>// nuv. rewrite Aab Aab';move => /setI2_P [uA uB] /setI2_P [vA vB]. case: AB; rewrite Aab' Aab. rewrite (Cab_trans nab Rab i1 nuv uB vB). by rewrite (Cab_trans nab' Rab' i1 nuv uA vA). Qed. (** Intersection of three constituants *) Lemma constitutant_inter3 A B C: is_constituant A -> is_constituant B -> is_constituant C -> intransitive1 -> A = B \/ A = C \/ B = C \/ A \cap B = emptyset \/ A \cap C = emptyset \/ B \cap C = emptyset \/ (A \cap B = A \cap C /\ B \cap C = A \cap C). Proof. move=> cA cB cC i1. case: (equal_or_not A B); [by left| move=> nAB; right]. case: (equal_or_not A C); [by left| move=> nAC; right]. case: (equal_or_not B C); [by left| move=> nBC; right]. have ssAB: small_set (A \cap B). by case: (constituant_inter2 cA cB i1). have ssAC: small_set (A \cap C). by case: (constituant_inter2 cA cC i1). have ssBC: small_set (B \cap C). by case: (constituant_inter2 cB cC i1). case: cA. move=> [a [Aa aE ap]]; case cB. move=> [b [Bb bE bp]]. left; apply: disjoint_pr=> u ua ub; case: nAB. by move: ua ub;rewrite Aa Bb; move /set1_P => -> /set1_P ->. move => [b1 [b2 [Bbb nbb Rbb]]]. left; apply: disjoint_pr => u; rewrite Aa Bbb; move /set1_P => ->. move/Zo_hi=> [R1 R2]; case: nbb. by rewrite -(ap _ (A2 R1)) (ap _ (A2 R2)). move => [a1 [a2 [Aaa naa Raa]]]. case: cB. move=> [b [Bb bE bp]]; case: cC. move=> [c [Cc cE cp]]. right;right;left; apply: disjoint_pr=> u; rewrite Bb Cc; move /set1_P=> ->. by move/set1_P=> bc; case nBC;rewrite Bb Cc bc. move => [c1 [c2 [Ccc ncc Rcc]]]. right; right;left; apply: disjoint_pr => u; rewrite Bb Ccc; move/set1_P=> ->. by move /Zo_hi=> [R1 R2]; case ncc; rewrite -(bp _ (A2 R1)) (bp _ (A2 R2)). move => [b1 [b2 [Bbb nbb Rbb]]]. case: cC. move=> [c [Cc cE cp]]. right;left;apply: disjoint_pr => u uA uC; move: uC uA; rewrite Aaa Cc. move /set1_P=> -> /Zo_hi [R1 R2]; case: naa. by rewrite -(cp _ (A2 R1)) (cp _ (A2 R2)). move => [c1 [c2 [Ccc ncc Rcc]]]. case: (emptyset_dichot (A \cap B));[ by left | move=> [c ci]; right]. case: (emptyset_dichot (A \cap C));[ by left | move=> [b bi]; right]. case: (emptyset_dichot (B \cap C));[ by left | move=> [a ai]; right]. have iAB: A \cap B = singleton c by apply: set1_pr2. have iAC: A \cap C = singleton b by apply: set1_pr2. have iBC: B \cap C = singleton a by apply: set1_pr2. rewrite iAB iAC iBC. suff: (inc c C). move=> cC. have cAC: inc c (A \cap C) by move/setI2_P: ci => []; fprops. have cBC: inc c (B \cap C) by move/setI2_P: ci => []; fprops. by rewrite (ssAC _ _ bi cAC) (ssBC _ _ ai cBC). case: (equal_or_not a b). move=> ab. have: inc a (A \cap B). apply setI2_i; [by rewrite ab;apply: (setI2_1 bi) | apply: (setI2_1 ai)]. rewrite iAB; move /set1_P => <-; apply: (setI2_2 ai). move=> nab. move: ai bi ci => /setI2_P [aB aC] /setI2_P [bA bC] /setI2_P [cA cB]. move: cA cB bA bC aB aC; rewrite Aaa Bbb Ccc. move => /Zo_P [cE [Ra1c Ra2c]] /Zo_hi [Rb1c Rb2c]. move => /Zo_hi [Ra1b Ra2b] /Zo_hi [Rc1b Rc2b]. move => /Zo_hi [Rb1a Rb2a] /Zo_hi [Rc1a Rc2a]. move: (i1 _ _ _ _ ncc Rcc Rc1a Rc1b Rc2a Rc2b) => Rab. move: (i1 _ _ _ _ nbb Rbb Rb1a Rb1c Rb2a Rb2c) => Rac. move: (i1 _ _ _ _ naa Raa Ra1b Ra1c Ra2b Ra2c) => Rbc. move: (i1 _ _ _ _ nab Rab (A2 Rc1a) Rac (A2 Rc1b) Rbc) => Rc1c. move: (i1 _ _ _ _ nab Rab (A2 Rc2a) Rac (A2 Rc2b) Rbc) => Rc2c. by apply: Zo_i. Qed. End Exercise6_10. (** Let [X] be a covering, satisfying the intersection properties above; Then the associated relation is intransitive and the elements of [X] are the constituants *) Definition exercise6_11b_assumption X E:= [/\ union X = E, (forall A, inc A X -> nonempty A), (forall A B, inc A X -> inc B X -> A = B \/ small_set (A \cap B)) & (forall A B C, inc A X -> inc B X -> inc C X -> ( A=B \/ A = C \/ B = C \/ A \cap B = emptyset \/ A \cap C = emptyset \/ B \cap C = emptyset \/ (A \cap B = A \cap C /\ A \cap B = B \cap C)))]. Definition exercise6_11b_rel X x y := exists A, [/\ inc A X, inc x A & inc y A]. Lemma exercise6_11b1 E X: exercise6_11b_assumption X E -> reflexive_re (exercise6_11b_rel X) E. Proof. move=> [h _] x; rewrite /exercise6_11b_rel -h;split. move => xE; move: (setU_hi xE)=> [y ye xy];ex_tac. move=> [y [yX xy _ ]]; apply: (setU_i xy yX). Qed. Lemma exercise6_11b2 X: symmetric_r (exercise6_11b_rel X). Proof. move=> E y; rewrite /exercise6_11b_rel. by move=>[A [Ax xA yA]]; exists A. Qed. Lemma exercise6_11b3 E X: exercise6_11b_assumption X E -> let R := exercise6_11b_rel X in forall x y z t, x <> y -> x<>z -> x <> t -> y <> z -> y <> t -> z <> t -> R x y -> R x z -> R x t -> R y z -> R y t -> R z t. Proof. move=> [uX alne i2 i3] R x y z t nxy nxz nxt nyz nyt nzt [XY [XYX xXY yXY]] [XZ [XZX xXZ zXZ]] [XT [XTX xXT tXT]] [YZ [YZX yYZ zYZ]] [YT [YTX yYT tYT]]. case: (equal_or_not XZ XT) => XZXT; first by exists XT; split => //; ue. case: (equal_or_not XZ YT) => XZYT; first by exists XZ; split => //; ue. case: (equal_or_not YZ XT) => YZXT; first by exists XT; split => //; ue. case: (equal_or_not YZ YT) => YZYT; first by exists YT; split => //; ue. have iXZXT: (XZ \cap XT = singleton x). by apply: set1_pr2; [ fprops | case: (i2 _ _ XZX XTX)]. have iYZYT: (YZ \cap YT = singleton y). by apply: set1_pr2; [ fprops | case: (i2 _ _ YZX YTX) ]. case: (equal_or_not XY XZ)=> XYXZ. have XYYZ: XY= YZ. have yp1:inc y (XY \cap YZ) by fprops. have zp1:inc z (XY \cap YZ) by rewrite XYXZ; fprops. case: (i2 _ _ XYX YZX) =>// h; case: nyz;apply: (h _ _ yp1 zp1). case: (equal_or_not XY YT)=> XYYT; first by exists XY; aw; split => //; ue. case: (equal_or_not XT YT) => XTYT. have xp: inc x (XY \cap YT) by aw; ue. have yp: inc y (XY \cap YT) by aw; ue. case (i2 _ _ XYX YTX) =>// h. case: nxy;apply: (h _ _ xp yp). case: (i3 _ _ _ XYX XTX YTX); first by move=> h;exists XY; split => //; ue. case; first by move=> h. case; first by move=> h. case; first by move=> h;empty_tac1 x; aw. case; first by rewrite XYYZ; move=> h; empty_tac1 y; aw. case; first by move=> h; empty_tac1 t; aw. move=> [r1 r2]. have : inc t (XT \cap YT) by fprops. by rewrite -r2 XYYZ;move /setI2_P=> [tp _]; exists YZ. have iXYXZ: (XY \cap XZ = singleton x). by apply: set1_pr2; fprops; case: (i2 _ _ XYX XZX). case:(equal_or_not XZ YZ)=> XZYZ. have : inc y (singleton x) by rewrite - iXYXZ; apply/setI2_P; split => //; ue. move/set1_P => h; case: nxy =>//. have iXZYZ: (XZ \cap YZ = singleton z). apply: set1_pr2; fprops; case (i2 _ _ XZX YZX) => //. case: (equal_or_not XY YT)=> XYYT. have XYXY: (XY = XT). have xp: inc x (XY \cap XT) by fprops. have tp: inc t (XY \cap XT) by rewrite XYYT; fprops. case (i2 _ _ XYX XTX) =>// h; case: nxt;apply: (h _ _ xp tp). case: (equal_or_not XY YZ)=> XYYZ; first by exists XY;split => //; ue. case: (i3 _ _ _ XYX XZX YZX); first by move=> h;exists XY. case; first by move=> h. case; first by move=> h. case; first by move=> h;empty_tac1 x; aw. case; first by move=> h; empty_tac1 y; aw. case; first by move=> h; empty_tac1 z; aw. move=> [r1 r2]. have : inc z (XZ \cap YZ) by fprops. rewrite -r2 XYYT;move /setI2_P=> [tp _]; exists YT; by aw. have iXYYT: (XY \cap YT = singleton y). by apply: set1_pr2; fprops; case: (i2 _ _ XYX YTX). case: (equal_or_not XT YT)=> XTYT. have : inc x (singleton y) by rewrite -iXYYT; apply/setI2_P; split => //; ue. move/set1_P => h; case: nxy =>//. have iXTYT: (XT \cap YT = singleton t). by apply:set1_pr2;fprops;case: (i2 _ _ XTX YTX). case (equal_or_not XY XT)=> XYXT. case: (equal_or_not XY YZ)=> XYYZ; first by case: YZXT; ue. case: (i3 _ _ _ XYX XZX YZX); first by move=> h. case; first by move=> h. case; first by move=> h. case; first by move=> h;empty_tac1 x; aw. case; first by move=> h;empty_tac1 y; aw. case; first by move=> h;empty_tac1 z; aw. rewrite iXYXZ iXZYZ; move=> [_ sxz]. by case: nxz; apply: set1_inj. case: (i3 _ _ _ XYX XTX YTX); first by move=> h. case; first by move=> h. case; first by move=> h. case; first by move=> h;empty_tac1 x; aw. case; first by move=> h;empty_tac1 y; aw. case; first by move=> h;empty_tac1 t; aw. rewrite iXYYT iXTYT; move=> [sy st]. by rewrite sy in st; case: nyt; apply: set1_inj. Qed. Lemma exercise6_11b4 E X (R := exercise6_11b_rel X) (p1 := fun u => (exists a b, [/\ a<> b, R a b & u = Zo E (fun x => R a x /\ R b x)])) (p2:= fun u => (exists x, [/\ u = singleton x, inc x E & forall y, inc y E -> R x y -> x = y])) (p3:= fun u => (exists v, [/\ inc v X, u <> v, sub u v & singletonp u])): exercise6_11b_assumption X E -> [/\ (forall u, inc u X -> p1 u \/ p2 u \/ p3 u ), (forall u, p1 u -> inc u X) & (forall u, p2 u -> inc u X)]. Proof. move => [uXE alne i2 i3]; split. move=> u uX. case: (p_or_not_p (singletonp u)) => su. right; case: (p_or_not_p (p3 u)) => p3u; first by right. left; move: (su) => [x sx]. rewrite sx; exists x; split => //. rewrite -uXE; apply: (@setU_i _ u) =>//; rewrite sx; fprops. move=> y yE Rxy; case: (equal_or_not x y) =>//. move=> xy; move: Rxy=> [A [AX xA yA]]. case p3u; exists A; split =>//. by dneg uA; move: yA; rewrite -uA sx;move /set1_P. by move=> t; rewrite sx; move/set1_P => ->. constructor 1; red. move: (alne _ uX) => [y yu]; exists y. case (p_or_not_p (exists2 v, inc v u & v <> y)). move=> [x xu xy]; exists x;split; [auto | by exists u |]. set_extens w. move=> wu; apply: Zo_i. rewrite - uXE; apply: (@setU_i _ u) =>//. split;exists u; split => //. move /Zo_P=> [wE [ [A [AX xA yA]] [A' [AX' xA' yA']]]]. case: (equal_or_not A u)=> Au; first by rewrite -Au. case: (equal_or_not A' u)=> Au'; first by rewrite -Au'. have xi: (inc x (u \cap A')) by fprops. have yi: (inc y (u \cap A)) by fprops. case: (equal_or_not A A') => AA'. case: (i2 _ _ uX AX)=> aux. by case: Au'; rewrite -AA' aux. rewrite -AA' in xi. by case: xy; apply:(aux _ _ xi yi). move: (i3 _ _ _ AX AX' uX). case =>//; case =>//; case =>//. case; first by move=> h; empty_tac1 w; aw. case; first by move=> h; empty_tac1 y; aw. case; first by move=> h; empty_tac1 x; aw. move=> [h1 h2]. rewrite setI2_C -h2 in xi. rewrite setI2_C -h1 in yi. case: (i2 _ _ AX AX')=>// aux. case: xy; by apply: (aux _ _ xi yi). move=> h;case: su; exists y; apply: set1_pr1; first by ex_tac. move => w wu;case: (equal_or_not w y) =>// wy; by case: h; ex_tac. (* last case *) move=> u [a [b [nab [A [AX aA bA]] uZ]]]. suff: (u = A) by move=> ->. rewrite uZ; set_extens t. move /Zo_P=> [tE [[A' [AX' aA' bA']]] [A'' [AX'' aA'' bA'']]]. case: (equal_or_not A A'')=> AA''; first by ue. case: (equal_or_not A A')=> AA'; first by ue. have aAA: inc a (A \cap A') by fprops. have bAA: inc b (A \cap A'') by fprops. case: (equal_or_not A' A'') => aux. case: (i2 _ _ AX AX')=> // ss. rewrite -aux in bAA; case: nab; apply: (ss _ _ aAA bAA). case: (i3 _ _ _ AX AX' AX'') =>//; case =>//; case =>//. case; first by move=> h; empty_tac1 a; aw. case; first by move=> h; empty_tac1 b; aw. case; first by move=> h; empty_tac1 t; aw. move=> [h1 h2]; rewrite - h1 in bAA. case: (i2 _ _ AX AX')=>// ss. case: nab; by apply: (ss _ _ aAA bAA). move=> tA; apply: Zo_i. rewrite -uXE;apply: (@setU_i _ A)=>//. by split;exists A. move=> u [v [uv vE su]]. move: vE;rewrite -uXE; move/setU_P=> [y vy yX]. suff: u = y by move=> ->. rewrite uv; symmetry; apply:set1_pr => // t tv. symmetry;apply: su. rewrite -uXE;apply: (@setU_i _ y) =>//. by exists y. Qed. End Exercise1. Export Exercise1.