proposition: Lemma n_comp_dfsP (s: seq T) : connect_sym (grel g) -> closed (grel g) s -> n_comp (grel g) s = n_comp_dfs s.
proof: Proof. move=> csym_g; rewrite /n_comp_dfs; move: {-1}(size s) (leqnn (size s)) => n. have [m Hm] := ubnP (size s); elim: m s Hm n => // m IH [_|y s /ltnSE Hm [//|n]]. by move => n _ _; rewrite n_comp0 //; case: n. move=> leq_s_n closed_y; set p := connect_dfs y. have y_p : y \in p by rewrite /p/connect_dfs kT; exact: dfs_start. have Hp : p =i connect (grel g) y by move => ?; apply/esym/connectEdfs. have sub_p : {subset p <= y::s}. { move=> z; rewrite Hp inE => con_yz. by rewrite -(closed_connect closed_y con_yz) mem_head. } rewrite (n_compD (mem p)) [RHS]/= -/p -add1n; congr(_ + _). - suff S : [predI y :: s & mem p] =i connect (grel g) y. by rewrite (eq_n_comp_r S) n_comp_connect. by move=> z; rewrite -[RHS]Hp inE /= andb_idl//; exact: sub_p. - rewrite -IH. + apply: eq_n_comp_r => z; rewrite mem_filter !inE. have [//|zNp/=] := boolP (z \in p); rewrite (_ : z == y = false) //. by apply: contraNF zNp => /eqP->. + by apply: leq_trans Hm; rewrite size_filter /= ltnS count_size. + rewrite /= ltnS in leq_s_n. apply: leq_trans leq_s_n. by rewrite size_filter count_size. + have -> : [seq x <- s | [predC p] x] = [seq x <- y::s | [predC p] x]. by rewrite /= y_p. have i : [seq x <- y :: s | [predC p] x] =i [predD (y :: s) & p]. by move=> z; rewrite mem_filter /= !inE. rewrite (eq_closed_r i); apply: predD_closed => //. by rewrite (eq_closed_r Hp); apply: connect_closed. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)