proposition: Lemma weak_perfect_aux (G : sgraph) (x0 : G) : perfect G -> exists2 K, cliqueb K & [forall S in maxstabsets [set: G], K :&: S != set0].
proof: Proof. move => perfG. pose M := maxstabsets [set: G]. pose k := #|M|. pose S (i : 'I_k) : {set G} := enum_val i. pose m (x : G) := #|[set i : 'I_k | x \in S i]|. pose G' := Lovasz m. pose before (x : G) (i : 'I_k) := [set j : 'I_k | j < i & x \in S j]. pose B (i : 'I_k) := [set xn : G' | tag xn \in S i & #|before (tag xn) i| == tagged xn :> nat]. pose P := [set B i | i : 'I_k]. have BiP (i : 'I_k) : B i \in P by apply/imsetP; exists i. have beforeI (i : 'I_k) x : [set j in [set i0 | x \in S i0] | j < i] = before x i. { by apply/setP => j; rewrite !inE andbC. } have ltn_before (i : 'I_k) x : x \in S i -> #|before x i| < m x. { move=> x_Si; rewrite /before /m. apply: proper_card; apply/properP; split. by apply/subsetP => j; rewrite !inE => /andP[_ ->]. by exists i; rewrite !inE ?ltnn. } have coverP : cover P = [set: G']. { apply/eqP; rewrite eqEsubset subsetT; apply/subsetP => -[x n] _. have/nth_ord [i] := ltn_ord n; rewrite !inE beforeI => x_Si b_xi. by apply/bigcupP; exists (B i) => //; rewrite !inE /= x_Si b_xi eqxx. } have tagB (i : 'I_k) : tag @: B i = S i. { apply/setP => x; apply/imsetP/idP => /= [[[z n] xn_Bi ->]|x_Si]. by move: xn_Bi; rewrite inE => /andP[-> _]. by exists ⟨ x , Ordinal (ltn_before _ _ x_Si) ⟩; rewrite // !inE /= x_Si eqxx. } have disjB (i j : 'I_k) : j != i -> [disjoint B i & B j]. { move =>jDi; apply/pred0Pn => -[[/= x n]]. rewrite !inE /= -!andbA => /and4P[/= x_Si /eqP <- x_Sj]; apply/negP. wlog lt_i_j : i j {jDi} x_Si x_Sj / i < j => [W|]. { case: (ltnP i j); [exact: W|rewrite leq_eqVlt eq_sym]. by rewrite (inj_eq (@ord_inj _)) eq_sym (negbTE jDi) eq_sym /=; apply: W. } rewrite eq_sym eqn_leq negb_and -!ltnNge [X in _ || X]proper_card ?orbT //. apply/properP; split. - by apply/subsetP => o; rewrite !inE => /andP[H ->]; rewrite (ltn_trans H lt_i_j). - by exists i; rewrite !inE ?lt_i_j ?ltnn. } have inhB (i : 'I_k) : B i != set0. { rewrite -(imset_eq0 tag) tagB -cards_eq0 (@card_maxstabset _ _ [set: G]). by rewrite alpha_eq0; apply/set0Pn; exists x0. exact: enum_valP. } have [partP injP] : partition P [set: G'] /\ injective B. { have [/= ? inj] := (indexed_partition (J := predT) (in2W disjB) (in1W inhB)). by rewrite -coverP; split => //; apply: in2T inj. } have cardP : #|P| = k by rewrite /P card_imset ?card_ord. have stabB (i : 'I_k) : stable (B i). { apply/stableP => -[/= x n] [/= y n']; rewrite !inE /=. have [xEy|xDy] := eqVneq x y. - by subst y => /andP[_ /eqP->] /andP[_ /eqP/ord_inj<-]; rewrite sgP. - move=> /andP[xSi _] /andP[ySi _]; rewrite /edge_rel/=/LovaszRel/= (negbTE xDy). by move: (enum_valP i); rewrite -/(S i) => /maxstabset_stable/stableP; apply. } have maxB (i : 'I_k) : B i \in maxstabsets [set: G']. { rewrite !inE subsetT /= stabB /=; apply: leq_trans (alpha_Lovasz _) _. rewrite -Lovasz_stable_card // tagB. by move: (enum_valP i); rewrite -/(S i) inE => /andP[_ ->]. } have : ω([set: G']) = k. { have perfG' : perfect G' by apply: Lovasz_perfect. rewrite perfect_eq ?perfectT // -cardP; apply: maxstabset_coloring => //. move => ? /imsetP[i _ ->]; exact: maxB. } have [K' maxK' cardK'] := omegaP. have cutK' (i : 'I_k) : K' :&: B i != set0. { apply: partition_pigeonhole partP _ _ _ _ _ => // {i}. by rewrite cardK' cardP. move=> ? /imsetP[i _ ->]; apply: cliqueIstable. exact: maxclique_clique maxK'. exact: maxstabset_stable. } exists (tag @: K'). - by apply/cliqueP/Lovasz_tag_clique; exact: maxclique_clique maxK'. - apply/forall_inP => A A_M; pose i : 'I_k := enum_rank_in A_M A. have defA : A = S i by rewrite /S enum_rankK_in. have [z /setIP[z_Bi z_K']] := set0Pn _ (cutK' i). by apply/set0Pn; exists (tag z); rewrite defA -tagB inE !imset_f. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)