Library ssete1
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.
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.
~ (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.
(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
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.
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.
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.
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.
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.
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.
~(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.
( 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:
(G \cg emptyset = emptyset /\
emptyset \cg G = 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: (proj1 (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).
set (K:= complement_graph G).
transitivity (K = emptyset).
rewrite /K /complement_graph; split.
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) => [p1 p2]; rewrite p2 p1.
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.
((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).
set (K:= complement_graph G).
transitivity (K = emptyset).
rewrite /K /complement_graph; split.
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) => [p1 p2]; rewrite p2 p1.
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.
(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) -> image_by_fun G' (image_by_fun G (singleton x))
= singleton x) ->
(forall x, inc x (source G') -> image_by_fun G (image_by_fun G' (singleton x))
= singleton x) ->
[/\ bijection G, bijection G' & G = inverse_fun G'].
Proof.
rewrite /image_by_fun=> 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':forall x y z, inc (J x y)(graph G) -> inc (J y z)(graph G') -> x = z.
move=> x y z 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:forall x y z, inc (J x y)(graph G') -> inc (J y z)(graph G) -> x = z.
move=> x y z 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: (forall x, inc x (source G) -> exists2 y,
inc (J x y) (graph G) & inc (J y x) (graph G')).
move=> x 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: (forall x, inc x (source G') -> exists2 y,
inc (J x y) (graph G') & inc (J y x) (graph G)).
move=> x 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].
rewrite - (JG'G _ _ _ J2g xG).
by rewrite - (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].
rewrite - (JGG' _ _ _ J2g xG).
by rewrite - (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=>//; move=> 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.
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.
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 _.
have xv: (inc x v).
rewrite /v; apply: setI2_i; apply /iim_graph_P; ex_tac.
by move => ve; move: xv; 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.
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; move=> 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.
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.
set (x:=C0); set (y:= C1); set z := (doubleton x y).
exists z.
set (G:= doubleton(J x x)(J y y)); set (H:= doubleton(J x y)(J y x)).
move => h; move: {h} (h G H).
have ->: direct_image G z = z.
set_extens u.
move=> /dirim_P [v vz /set2_P] [] h; rewrite (pr2_def h) /z; fprops.
case /set2_P => h; apply /dirim_P; exists u; rewrite h /z /G; fprops.
have -> :direct_image H z = z.
set_extens u.
move=> /dirim_P [v vz /set2_P] [] h; rewrite (pr2_def h) /z; fprops.
case /set2_P => ->; apply /dirim_P; [ exists y | exists x];
rewrite /H;fprops.
rewrite setI2_id => bad.
move: (set2_1 x y); rewrite -/z -bad; move/dirim_P => [t _ /setI2_P[pa]].
have : P (J t x) = Q (J t x) 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 p3: (inc (J (P x)(P x)) ((H \cap H') \cg G)).
by rewrite hyp//; apply: setI2_i => //;rewrite Pxy //.
move: p3; 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 p3: (inc (J (P x)(P x)) ((H \cap H') \cg G)).
by rewrite hyp; apply: setI2_i => //;rewrite Pxy //.
move: p3; 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.
move=> h; red in h.
by empty_tac1 y; bw; aw; split.
Qed.
Hint Rewrite variant_d variant_V_a variant_V_b: bw.
Lemma exercise4_8b (a:= C0) (b:= C1)
(x:= doubleton a b)
(r:= Lg (singleton a) (fun _ => x))
(s:= variantL a b x (singleton a)) :
[/\ covering r x, covering s x,
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: b<> a by rewrite /a/b; apply: TP_ne1.
rewrite /r/s/x;split.
split; fprops; move=> t tx; apply: (@setUb_i _ a); fprops; bw; fprops.
split; fprops; move=> y yx;apply: (@setUb_i _ a); fprops; bw; fprops.
split; [ fprops | fprops | bw].
move=> t /set1_P ->; exists a; bw;fprops.
move=> k; bw; case /set2_P=> ->; bw; [apply: set2_ne | apply: set1_ne].
have bd: (inc b (doubleton a b)) by fprops.
bw; move=> h; move: (h _ bd)=> [i [/set1_P ->]]; bw; fprops => xa.
by move: (xa _ bd) => /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_neC01 => [n1 n2].
move:C3_neC012 => [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.
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.
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.
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.
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.
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.
move=> h; red in h.
by empty_tac1 y; bw; aw; split.
Qed.
Hint Rewrite variant_d variant_V_a variant_V_b: bw.
Lemma exercise4_8b (a:= C0) (b:= C1)
(x:= doubleton a b)
(r:= Lg (singleton a) (fun _ => x))
(s:= variantL a b x (singleton a)) :
[/\ covering r x, covering s x,
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: b<> a by rewrite /a/b; apply: TP_ne1.
rewrite /r/s/x;split.
split; fprops; move=> t tx; apply: (@setUb_i _ a); fprops; bw; fprops.
split; fprops; move=> y yx;apply: (@setUb_i _ a); fprops; bw; fprops.
split; [ fprops | fprops | bw].
move=> t /set1_P ->; exists a; bw;fprops.
move=> k; bw; case /set2_P=> ->; bw; [apply: set2_ne | apply: set1_ne].
have bd: (inc b (doubleton a b)) by fprops.
bw; move=> h; move: (h _ bd)=> [i [/set1_P ->]]; bw; fprops => xa.
by move: (xa _ bd) => /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_neC01 => [n1 n2].
move:C3_neC012 => [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.
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.
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.
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.
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.
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.
rewrite /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 (Vf f z) x by apply: (@sub_trans z).
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 rewrite /q;apply: Zo_i.
by move: (qW _ vq)=> aux; rewrite {1} vd;apply: setI_s1.
apply: extensionality=>//.
have iwp: inc w p by rewrite /p; 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=> inv_image_by_fun (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.
set faux:=(Lf (fun x=> direct_image c (singleton x)) a (powerset b)).
suff: (inc (graph faux) (gfunctions (source faux) (target faux))).
by rewrite /faux /Lf; aw.
apply: gfun_set_i ;apply: lf_function => 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: (gfun_set_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.
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.
set faux:=(Lf (fun x=> direct_image c (singleton x)) a (powerset b)).
suff: (inc (graph faux) (gfunctions (source faux) (target faux))).
by rewrite /faux /Lf; aw.
apply: gfun_set_i ;apply: lf_function => 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: (gfun_set_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.
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.
red; 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.
((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.
red; 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; red; 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.
set r:= equivalence_associated (intersection_with x a).
have er: equivalence r by apply: graph_ea_equivalence.
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 graph_ea_substrate /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: (graph_ea_substrate fai); rewrite -/r 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.
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.
set r:= equivalence_associated (intersection_with x a).
have er: equivalence r by apply: graph_ea_equivalence.
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 graph_ea_substrate /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: (graph_ea_substrate fai); rewrite -/r 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.
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_neC01 => [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: forall a b, inc (J a b) K -> inc (J b a) K
by move => a b h;equiv_tac.
set_extens x => xK.
have px: (pairp x) by apply: (@compg_graph G H).
move: xK ; rewrite - px => h; move : (aux _ _ h).
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.
rewrite {2} /K compgA eq.
rewrite - (compgA H G G) GG - compgA.
by rewrite -/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 fgg)=> [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:(eg) => [fgg _ _ _].
move: (sub_graph_setX fgg).
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 rewrite /E; 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: coarse_equivalence.
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.
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: forall a b, inc (J a b) K -> inc (J b a) K
by move => a b h;equiv_tac.
set_extens x => xK.
have px: (pairp x) by apply: (@compg_graph G H).
move: xK ; rewrite - px => h; move : (aux _ _ h).
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.
rewrite {2} /K compgA eq.
rewrite - (compgA H G G) GG - compgA.
by rewrite -/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 fgg)=> [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:(eg) => [fgg _ _ _].
move: (sub_graph_setX fgg).
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 rewrite /E; 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: coarse_equivalence.
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 (image_of_fun f)))).
Proof.
move => er ff tf.
set (s := inv_image_relation f r).
set (A:= (image_of_fun f)).
set (Ra := induced_relation r A).
have ia: (iirel_axioms f r) by red; intuition.
have rf: A = range (graph f).
rewrite /A/image_of_fun -image_by_fun_source // image_by_fun.
have es:equivalence s by rewrite /s; apply: iirel_relation.
have iA: induced_rel_axioms r A.
by split =>//; rewrite -tf rf; apply: corresp_sub_range; move: ff=> [h _].
have eR: equivalence Ra by rewrite /Ra;apply: induced_rel_equivalence.
set (f1:= fun x y => [/\ classp r y,
nonempty (y \cap A) & x = inv_image_by_fun 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.
case (class_dichot es c1 c2) => // dj; red in dj.
by empty_tac1 x; apply: intersection2_inc.
move=> y; move /(setQ_P eR) /(induced_rel_classP iA)=> [x [cx nex yi]].
set (u:= inv_image_by_fun 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; red in di.
empty_tac1 t; apply setI2_i =>//; ue.
Qed.
equivalence r -> function f -> target f = substrate r ->
(exists g, bijection_prop g (quotient (inv_image_relation f r))
(quotient (induced_relation r (image_of_fun f)))).
Proof.
move => er ff tf.
set (s := inv_image_relation f r).
set (A:= (image_of_fun f)).
set (Ra := induced_relation r A).
have ia: (iirel_axioms f r) by red; intuition.
have rf: A = range (graph f).
rewrite /A/image_of_fun -image_by_fun_source // image_by_fun.
have es:equivalence s by rewrite /s; apply: iirel_relation.
have iA: induced_rel_axioms r A.
by split =>//; rewrite -tf rf; apply: corresp_sub_range; move: ff=> [h _].
have eR: equivalence Ra by rewrite /Ra;apply: induced_rel_equivalence.
set (f1:= fun x y => [/\ classp r y,
nonempty (y \cap A) & x = inv_image_by_fun 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.
case (class_dichot es c1 c2) => // dj; red in dj.
by empty_tac1 x; apply: intersection2_inc.
move=> y; move /(setQ_P eR) /(induced_rel_classP iA)=> [x [cx nex yi]].
set (u:= inv_image_by_fun 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; red in di.
empty_tac1 t; apply setI2_i =>//; ue.
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.
set (a:= C0); set (b:= C1).
have ba: b <> a by rewrite /a /b; apply: TP_ne1.
set Ea:= F \times (singleton a).
set Eb:= G \times (singleton b).
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 =a \/ Q x = b).
by move=> x /setU2_P; case; move /setX_P => [_ _ ] /set1_P; auto.
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 = a) (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 a) Ea by rewrite /Ea; fprops.
have p2: inc (J y a) E by rewrite /E; aw; intuition.
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 (inv_image_by_fun f(singleton(Vf (canon_proj r) x)))).
have haF:forall x, inc x F ->
ha x = rep (inv_image_by_fun f (singleton (class r x))).
move=> x xF; rewrite /ha; aw; ue.
have haF':forall x, inc x F ->
sub (inv_image_by_fun f (singleton(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) (inv_image_by_fun f (singleton (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 = a) (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=>//.
move=> y yG.
have JEb:inc (J y b) Eb by rewrite /Eb;aw; fprops.
have JE: (inc (J y b) E) by rewrite /E; aw; intuition.
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.
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.
set (a:= C0); set (b:= C1).
have ba: b <> a by rewrite /a /b; apply: TP_ne1.
set Ea:= F \times (singleton a).
set Eb:= G \times (singleton b).
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 =a \/ Q x = b).
by move=> x /setU2_P; case; move /setX_P => [_ _ ] /set1_P; auto.
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 = a) (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 a) Ea by rewrite /Ea; fprops.
have p2: inc (J y a) E by rewrite /E; aw; intuition.
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 (inv_image_by_fun f(singleton(Vf (canon_proj r) x)))).
have haF:forall x, inc x F ->
ha x = rep (inv_image_by_fun f (singleton (class r x))).
move=> x xF; rewrite /ha; aw; ue.
have haF':forall x, inc x F ->
sub (inv_image_by_fun f (singleton(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) (inv_image_by_fun f (singleton (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 = a) (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=>//.
move=> y yG.
have JEb:inc (J y b) Eb by rewrite /Eb;aw; fprops.
have JE: (inc (J y b) E) by rewrite /E; aw; intuition.
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: forall a X, inc a X -> small_set X -> X = singleton a.
Proof.
by move => w W 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).
A chain is a list with at least two elements; it has a head and a tail;
we may assume two consecutive elements related by R. We consider the relation; there is a chain from x to y
Inductive chain:Type :=
chain_pair: Set -> Set -> chain
| chain_next: Set -> chain -> chain.
Fixpoint chain_head x :=
match x with chain_pair u _ => u | chain_next u _ => u end.
Fixpoint chain_tail x :=
match x with chain_pair _ u => u | chain_next _ u => chain_tail u end.
Fixpoint chained_r x :=
match x with chain_pair u v => R u v
| chain_next u v => R u (chain_head v) /\ chained_r v
end.
Definition relS x y := exists c:chain,
[/\ chained_r c, chain_head c = x & chain_tail c = y].
chain_pair: Set -> Set -> chain
| chain_next: Set -> chain -> chain.
Fixpoint chain_head x :=
match x with chain_pair u _ => u | chain_next u _ => u end.
Fixpoint chain_tail x :=
match x with chain_pair _ u => u | chain_next _ u => chain_tail u end.
Fixpoint chained_r x :=
match x with chain_pair u v => R u v
| chain_next u v => R u (chain_head v) /\ chained_r v
end.
Definition relS x y := exists c:chain,
[/\ chained_r c, chain_head c = x & chain_tail c = y].
We may concatenate two chains; thus relS is transitive
Fixpoint concat_chain x y : chain :=
match x with chain_pair u _ => chain_next u y
| chain_next u v => chain_next u (concat_chain v y) end.
Lemma head_concat x y:
chain_head (concat_chain x y) = chain_head x.
Proof. by case x. Qed.
Lemma tail_concat x y:
chain_tail (concat_chain x y) = chain_tail y.
Proof. by elim x. Qed.
Lemma chained_concat x y:
chained_r x -> chained_r y -> chain_tail x = chain_head y ->
chained_r (concat_chain x y).
Proof.
move=> cx cy txhy;elim: x cx txhy => [a b cp ct| a c r cp ct].
split=>//; by rewrite -ct //.
by move: cp => [pa pb];split; [rewrite head_concat | apply: r].
Qed.
Lemma transitiveS y x z: relS x y -> relS y z -> relS x z.
Proof.
move=> [c [cc hcx tcy]][c' [cc' hcy tcz]].
exists (concat_chain c c'); split => //.
apply: chained_concat=>//; ue.
by rewrite head_concat.
by rewrite tail_concat.
Qed.
We may revert a chais; thus relS is symmetric
Fixpoint reconc_chain (x y:chain) :chain:=
match x with chain_pair u v => chain_next v (chain_next u y)
| chain_next u v => reconc_chain v (chain_next u y) end.
Lemma tail_reconc x y: chain_tail (reconc_chain x y) = chain_tail y.
Proof. by move: x y; elim=> [a b y | a c r] // y; by rewrite r. Qed.
Lemma head_reconc x y:chain_head (reconc_chain x y) = chain_tail x.
Proof. move: x y; elim=> [a b y | a c r] // y; by rewrite r. Qed.
Lemma chained_reconc x y: chained_r x -> chained_r y ->
R (chain_head y) (chain_head x) -> chained_r (reconc_chain x y).
Proof.
move: x y; elim => [a b y c cy | P c r]=>//=; auto.
by move=> y [rPh cc] cy RhyP; apply: r=>//; split => //; apply: A2.
Qed.
Fixpoint chain_reverse x:=
match x with chain_pair u v => chain_pair v u
| chain_next u v =>
match v with chain_pair u' v' => chain_next v' (chain_pair u' u)
| chain_next u' v' => reconc_chain v' (chain_pair u' u)
end end.
Lemma head_reverse x: chain_head (chain_reverse x) = chain_tail x.
Proof. elim x=>// y;elim =>// P c h h1 /=; apply: head_reconc.
Qed.
Lemma tail_reverse x: chain_tail (chain_reverse x) = chain_head x.
Proof. elim x =>// y;elim =>// P c h h1 /=; apply: tail_reconc. Qed.
Lemma chained_reverse x: chained_r x -> chained_r (chain_reverse x).
Proof.
elim x; first by move=> a b; simpl; auto.
move=> a; elim; first by move => b c; simpl; intuition.
move=> b c hr hr1 /= [Rab [Rbc cc]].
apply: chained_reconc=>//; simpl; auto.
Qed.
Lemma symmetricS x y: relS x y -> relS y x.
Proof.
move=> [c [cc hcx tcy]].
exists (chain_reverse c); split.
apply: chained_reverse =>//.
rewrite head_reverse //.
rewrite tail_reverse //.
Qed.
match x with chain_pair u v => chain_next v (chain_next u y)
| chain_next u v => reconc_chain v (chain_next u y) end.
Lemma tail_reconc x y: chain_tail (reconc_chain x y) = chain_tail y.
Proof. by move: x y; elim=> [a b y | a c r] // y; by rewrite r. Qed.
Lemma head_reconc x y:chain_head (reconc_chain x y) = chain_tail x.
Proof. move: x y; elim=> [a b y | a c r] // y; by rewrite r. Qed.
Lemma chained_reconc x y: chained_r x -> chained_r y ->
R (chain_head y) (chain_head x) -> chained_r (reconc_chain x y).
Proof.
move: x y; elim => [a b y c cy | P c r]=>//=; auto.
by move=> y [rPh cc] cy RhyP; apply: r=>//; split => //; apply: A2.
Qed.
Fixpoint chain_reverse x:=
match x with chain_pair u v => chain_pair v u
| chain_next u v =>
match v with chain_pair u' v' => chain_next v' (chain_pair u' u)
| chain_next u' v' => reconc_chain v' (chain_pair u' u)
end end.
Lemma head_reverse x: chain_head (chain_reverse x) = chain_tail x.
Proof. elim x=>// y;elim =>// P c h h1 /=; apply: head_reconc.
Qed.
Lemma tail_reverse x: chain_tail (chain_reverse x) = chain_head x.
Proof. elim x =>// y;elim =>// P c h h1 /=; apply: tail_reconc. Qed.
Lemma chained_reverse x: chained_r x -> chained_r (chain_reverse x).
Proof.
elim x; first by move=> a b; simpl; auto.
move=> a; elim; first by move => b c; simpl; intuition.
move=> b c hr hr1 /= [Rab [Rbc cc]].
apply: chained_reconc=>//; simpl; auto.
Qed.
Lemma symmetricS x y: relS x y -> relS y x.
Proof.
move=> [c [cc hcx tcy]].
exists (chain_reverse c); split.
apply: chained_reverse =>//.
rewrite head_reverse //.
rewrite tail_reverse //.
Qed.
Thus relS is an equivalence, the least equivalenece compatible with R
Lemma equivalenceS: equivalence_re relS E.
Proof.
split; first by split; red; [ apply: symmetricS | apply: transitiveS].
move=> x; split.
by move=> xE; exists (chain_pair x x);split => //; apply /A1.
move=> [c [cc hcx _]].
elim: c cc hcx => [a b | a c _] /= h <-; [|move: h=> [h _]]; apply: (A3 h).
Qed.
Definition Sgraph := graph_on relS E.
Lemma equivalence_Sgraph: equivalence Sgraph.
Proof.
apply equivalence_from_rel; split; [apply: symmetricS | apply: transitiveS ].
Qed.
Lemma substrate_Sgraph: substrate Sgraph = E.
Proof.
apply: graph_on_sr => x xE.
by exists (chain_pair x x); split => //; apply/ A1.
Qed.
Lemma S_is_smallest r: equivalence r ->
(forall x y, R x y -> inc (J x y) r) -> sub Sgraph r.
Proof.
move=> er pr p.
have aux:(forall w, chained_r w -> inc (J (chain_head w) (chain_tail w)) r).
elim => [a b | a c h [aux cc]] //=; first by apply: pr.
move: (h cc)(pr _ _ aux) => r1 r2; equiv_tac.
move /Zo_P => [pp [c [cc hcx htx]]].
have <-: (J (P p)(Q p) = p) by move/setX_P: pp => [pp _].
by rewrite -hcx -htx ; apply: aux.
Qed.
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 interesection 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 -> relS 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 Sgraph a) A.
Proof.
move=> As aA t /(class_P equivalence_Sgraph) /(graph_on_P2 equivalenceS).
apply: (setF_pr2 As aA).
Qed.
Lemma setF_pr4 a: inc a E -> inc (class Sgraph a) setF.
Proof.
move=> aE; rewrite /setF.
move: equivalence_Sgraph => e1.
move: equivalenceS => e2.
apply: Zo_i.
apply/setP_P; rewrite - substrate_Sgraph; apply: (sub_class_substrate e1).
move=> y z ya /setC_P [zE nzc]; dneg yz; apply/(class_P e1).
suff: related Sgraph z a by move=> aux; equiv_tac.
have : related Sgraph y a by move/(class_P e1):ya=> h; equiv_tac.
move /(graph_on_P2 e2) => ra; apply/(graph_on_P2 e2); apply: transitiveS ra.
by exists (chain_pair z y); split => //; apply A2.
Qed.
Lemma connected_comp_class x: inc x E ->
class Sgraph 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: equivalence_Sgraph => eq.
have cx:(inc (class Sgraph x) (Zo setF (fun A => inc x A))).
apply: Zo_i; first by apply: setF_pr4.
apply/(class_P eq); rewrite - substrate_Sgraph 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 Sgraph) /\ singletonp A) <->
(exists2 a, A = singleton a & forall b, R a b -> a = b)).
Proof.
move=> AE.
move: equivalence_Sgraph => e1.
move: equivalenceS => e2.
split.
move=> [Asq [x Asx]]; exists x => //.
move=> b Rb.
have : related Sgraph x b.
by apply/(graph_on_P2 e2); exists (chain_pair x b).
move /(in_class_relatedP e1) => [y [cy xy]].
have <- : A = y.
move: Asq => /(setQ_P e1) => cA; case (class_dichot e1 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 Sgraph).
rewrite substrate_Sgraph; 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 Sgraph x = singleton x).
move => <-; apply /(setQ_P e1); apply: (class_class e1 xse).
apply: set1_pr; first by apply /(class_P e1); equiv_tac.
move => w; move /(class_P e1) => aux.
have : (related Sgraph w x) by equiv_tac.
move /(graph_on_P2 e2) => [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 auto); 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).
case (constituant_inter2 cA cB i1) =>//.
have ssAC: small_set (A \cap C).
case (constituant_inter2 cA cC i1) =>//.
have ssBC: small_set (B \cap C).
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).
apply: set1_pr2;first by fprops.
case (i2 _ _ XZX XTX) =>h; [ contradiction | done].
have iYZYT: (YZ \cap YT = singleton y).
apply: set1_pr2;first by fprops.
case (i2 _ _ YZX YTX) =>h; [ contradiction | done].
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; first by contradiction.
elim 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; intuition.
case; first by rewrite XYYZ; move=> h; empty_tac1 y; aw; intuition.
case; first by move=> h; empty_tac1 t; aw; intuition.
move=> [r1 r2].
have : inc t (XT \cap YT) by aw; intuition.
by rewrite -r2 XYYZ;move /setI2_P=> [tp _]; exists YZ.
have iXYXZ: (XY \cap XZ = singleton x).
apply: set1_pr2; fprops; case (i2 _ _ XYX XZX) => //.
case (equal_or_not XZ YZ)=> XZYZ.
have : inc y (singleton x) by rewrite - iXYXZ; aw;intuition; ue.
move/set1_P => h; elim 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; elim 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; intuition; ue.
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 aw; intuition.
rewrite -r2 XYYT;move /setI2_P=> [tp _]; exists YT; by aw.
have iXYYT: (XY \cap YT = singleton y).
apply: set1_pr2; fprops; case (i2 _ _ XYX YTX) => //.
case (equal_or_not XT YT)=> XTYT.
have : inc x (singleton y) by rewrite -iXYYT; aw;intuition; ue.
move/set1_P => h; elim nxy =>//.
have iXTYT: (XT \cap YT = singleton t).
apply:set1_pr2;fprops;case (i2 _ _ XTX YTX) => //.
case (equal_or_not XY XT)=> XYXT.
case (equal_or_not XY YZ)=> XYYZ; first by elim 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 elim 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].
rewrite sy in st; by elim 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 intuition.
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 elim Au'; rewrite -AA' aux.
rewrite -AA' in xi.
by elim 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.
elim xy; by apply: (aux _ _ xi yi).
move=> h;elim su; exists y; apply: set1_pr1; first by ex_tac.
move => w wu;case (equal_or_not w y) =>// wy; by elim h; ex_tac.
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; elim 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.
elim 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.
[/\ 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).
apply: set1_pr2;first by fprops.
case (i2 _ _ XZX XTX) =>h; [ contradiction | done].
have iYZYT: (YZ \cap YT = singleton y).
apply: set1_pr2;first by fprops.
case (i2 _ _ YZX YTX) =>h; [ contradiction | done].
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; first by contradiction.
elim 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; intuition.
case; first by rewrite XYYZ; move=> h; empty_tac1 y; aw; intuition.
case; first by move=> h; empty_tac1 t; aw; intuition.
move=> [r1 r2].
have : inc t (XT \cap YT) by aw; intuition.
by rewrite -r2 XYYZ;move /setI2_P=> [tp _]; exists YZ.
have iXYXZ: (XY \cap XZ = singleton x).
apply: set1_pr2; fprops; case (i2 _ _ XYX XZX) => //.
case (equal_or_not XZ YZ)=> XZYZ.
have : inc y (singleton x) by rewrite - iXYXZ; aw;intuition; ue.
move/set1_P => h; elim 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; elim 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; intuition; ue.
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 aw; intuition.
rewrite -r2 XYYT;move /setI2_P=> [tp _]; exists YT; by aw.
have iXYYT: (XY \cap YT = singleton y).
apply: set1_pr2; fprops; case (i2 _ _ XYX YTX) => //.
case (equal_or_not XT YT)=> XTYT.
have : inc x (singleton y) by rewrite -iXYYT; aw;intuition; ue.
move/set1_P => h; elim nxy =>//.
have iXTYT: (XT \cap YT = singleton t).
apply:set1_pr2;fprops;case (i2 _ _ XTX YTX) => //.
case (equal_or_not XY XT)=> XYXT.
case (equal_or_not XY YZ)=> XYYZ; first by elim 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 elim 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].
rewrite sy in st; by elim 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 intuition.
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 elim Au'; rewrite -AA' aux.
rewrite -AA' in xi.
by elim 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.
elim xy; by apply: (aux _ _ xi yi).
move=> h;elim su; exists y; apply: set1_pr1; first by ex_tac.
move => w wu;case (equal_or_not w y) =>// wy; by elim h; ex_tac.
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; elim 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.
elim 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.