proposition: Lemma dfs1_is_correct dfs (x : V) e : (dfs_correct dfs [set y | edge x y] (add_stack x e)) -> dfs1_correct (dfs1 dfs) x e.
proof: Proof. rewrite /dfs1 /dfs1_correct /dfs_correct; case: (dfs _ _) => m1 e1. move=> post_dfs; set m := sn e. move=> x_white [access_to_x [e_wf e_cwf e_gwf Nbw black_sccs]]. have e_uniq := @wf_uniq _ e_wf. case: post_dfs => //=. split => //. move=> y z; rewrite gray_add_stack // => /setU1P [->|y_gray]; rewrite inE => /(@connect1 _ edge) //. by apply/connect_trans/access_to_x; rewrite ?set11. split=> //; do?[exact: add_stack_cwf|exact: add_stack_gwf|exact: add_stack_nwf]. move=> y /Nbw; rewrite white_add_stack. rewrite ![[disjoint successors _ & _]]disjoint_sym. by apply/disjointWl/subsetDl. move=> [e1_wf e1_cwf e1_gwf Nbw1 black_sccs1] sube1 white1 m_min. have [//|s s_def sb] := subenv_stackP _ sube1. set s2 := rcons s x. have e1_uniq := @wf_uniq _ e1_wf. have xe_uniq : uniq (x :: stack e). by have := e1_uniq; rewrite s_def cat_uniq => /and3P []. have x_stack : x \in stack e1 by rewrite s_def mem_cat mem_head orbT. have x_gray : x \in gray e1. by rewrite (subenv_gray sube1) gray_add_stack ?setU11. have sx_subscc : is_subscc edge [set y in rcons s x]. apply: (@is_subscc1 _ edge x); first by rewrite inE mem_rcons mem_head. move=> y; rewrite !inE mem_rcons in_cons => /predU1P [->//|y_s]; split. apply: (@wf_stack_to_stack e1) => //; first by rewrite s_def mem_cat y_s. rewrite wf_num_stack //s_def; last by rewrite mem_cat y_s. rewrite !index_cat y_s ifN. by rewrite (leq_trans (index_size _ _) (leq_addr _ _)). by apply/negP=> /(subsetP sb); case: color4P x_gray. have [] := @wf_stack_to_gray _ e1_gwf y; first by rewrite s_def mem_cat y_s. move=> z [z_gray rank_z] /connect_trans; apply. rewrite (@wf_stack_to_stack e1) ?gray_stack //. by rewrite (subenv_gray_le sube1). have wreachex : wreach e x = x |: \bigcup_(y in [set y in successors x]) wreach (add_stack x e) y. rewrite /wreach white_add_stack. apply/eqP; rewrite eqEsubset subUset sub1set mem_wreach /=. apply/andP; split; last first. apply/bigcupsP => y; rewrite inE => xy; apply/subsetP=> z; rewrite !inE. move=> /connectP [p]; rewrite path_from => /andP[yp pw]->. apply/connectP; exists (y :: p); rewrite // path_from /= xy yp topredE /=. by rewrite x_white (sub_all _ pw) // => t; rewrite topredE inE => /andP[]. apply/subsetP=> y; rewrite !inE. move=> /connectP [_] /shortenP [p exp /andP[xNp _] _ -> {y}]. case: p => [|y p /=] //= in exp xNp *; first by rewrite eqxx. move: exp xNp; rewrite in_cons -andbA => /and3P[_ xy eyp] /norP[neq_xy xNp]. apply/orP; right; apply/bigcupP; exists y; rewrite ?inE //=; apply/connectP. exists p => //; elim: p => [|z p ihp] //= in y {xy} neq_xy eyp xNp *. move: eyp xNp; rewrite in_cons -andbA => /and3P[yw yz ezp] /norP[neq_yz xNp]. by rewrite !inE eq_sym neq_xy yw yz /= ihp. have m2_min : minn m m1 = \min_(y in wreach e x) @inord infty (num e1 y). rewrite wreachex bigmin_setU big_set1 //= /m -m_min; congr (minn _ _). rewrite (subenv_num sube1) ?mem_head//= ffunE/= eqxx. by rewrite inordK// ltnS sn_small. have succ_whiteF z : z \in successors x -> z \in white e1 = false. move=> z_successor; apply/negbTE. rewrite white1 white_add_stack !inE !negb_and !negbK. by rewrite (appP bigcupP idP) //; exists z; rewrite !inE. case: ltnP => [m1_small|m1_big] //=. rewrite (minn_idPr _) 1?ltnW// in m2_min. have [x1 num_x1 x_to_x1] : exists2 x1, num e1 x1 = m1 & gconnect x x1. have [] := @eq_bigmin_cond _ _ (pred_of_set (wreach e x)) (fun y => @inord infty (num e1 y)). by apply/card_gt0P; exists x; rewrite mem_wreach. move=> y; rewrite !inE=> xy /(congr1 val)/=. rewrite -m2_min ord_num // => m1_eq; exists y => //. by apply: connect_sub xy => u v /= /andP [_]; apply: connect1. have [x' [num_x' x'_gray x_to_x' ]] : exists x', [/\ num e1 x' < num e1 x, x' \in gray e1 & gconnect x x']. have x1_stack : x1 \in stack e1. rewrite num_stackP// num_x1 (leq_trans m1_small) ?andbT. rewrite m2_min (_ : 1 = @inord infty 1); last by rewrite inordK. apply/bigmin_geqP => i. rewrite ord_num // inordK//= lt0n wf_num0//. rewrite wreachex !inE => /predU1P[->|]. by case: color4P x_stack. by rewrite white1 inE => ->. apply: leq_trans (subenv_sn _ _ sube1); rewrite ?leqW //. by apply: add_stack_nwf. have [z [z_gray num_z y_to_z]] := wf_stack_to_gray e1_gwf x1_stack. exists z; split=> //; rewrite 2?inE ?z_gray ?andbT. - rewrite (leq_ltn_trans num_z)// num_x1 (leq_trans m1_small)// /m. by rewrite (subenv_num sube1) ?mem_head //= ffunE/= eqxx. - by rewrite (connect_trans x_to_x1). have neq_x'x : x' != x by apply: contraTneq num_x' => ->; rewrite -ltnNge. split=> //. - split=> //; first exact: add_black_cwf. + split => //. * move=> y /=. by rewrite white_add_black wf_num0// subND1//; case: color4P x_gray. * by move=> y /=; rewrite wf_num_infty. * by move=> y /= /wf_num_lt; apply. * by rewrite /= gray_add_black wf_sn// setUCA setUA setD1K. * by move=> y z /= y_stack z_stack; rewrite wf_num_stack. + split => //. move=> y z /= y_stack z_stack. by apply: wf_stack_to_stack. move=> y /= y_stack; rewrite gray_add_black. have [z] // := wf_stack_to_gray e1_gwf y_stack. have [->{z} [_ rank_x y_to_x]|] := eqVneq z x; last first. move=> neq_zx [z_gray rank_z y_to_z]. by exists z; split=> //; rewrite 2!inE neq_zx. exists x'; split; rewrite 2?inE ?x'_gray ?andbT //. - by rewrite (leq_trans _ rank_x) 1?ltnW // rkx. - by rewrite (connect_trans y_to_x). + move=> y; rewrite !inE white_add_black. move=> /predU1P [->{y}|y_black]; last first. apply/pred0P=> z /=; rewrite 2!inE. have /pred0P /(_ z) /= := Nbw1 _ y_black. by apply: contraFF=> /and3P[->_->]. apply/pred0P=> z /=; rewrite 2!inE. by have [/succ_whiteF->|]:= boolP (z \in successors x); rewrite ?andbF. + rewrite /= black_sccs1; apply/setP=> scc; rewrite !inE /=. have [scc_gsccs|] //= := boolP (scc \in gsccs). apply/idP/idP; first by move=> /subset_trans; apply; rewrite subsetU1. move=> /subsetP scc_sub; apply/subsetP => y y_scc. have /setU1P [eq_yx|//] := scc_sub y y_scc. rewrite eq_yx in y_scc. have x'_scc : (x' \in scc). rewrite -(def_scc scc_gsccs y_scc) // mem_scc /symconnect /= x_to_x' /=. by rewrite (wf_stack_to_stack e1_gwf) ?gray_stack // ltnW. have /scc_sub := x'_scc. rewrite !inE (negPf neq_x'x) /=. by case: color4P x'_gray. - apply/and5P; split => //=. + rewrite gray_add_black (subenv_gray sube1) gray_add_stack ?setU1K //. by rewrite white_grayF. + by rewrite (subset_trans (subenv_black sube1)) // subsetUr. + by rewrite -[esccs e]/(esccs (add_stack x e)) subenv_sccs. + apply/forall_inP => y y_stack; apply/eqP. rewrite (subenv_num sube1)/= ?in_cons ?y_stack ?orbT// ffunE/=. by rewrite ifN//; apply: contraTneq xe_uniq => <- /=; rewrite y_stack. + apply/'exists_eqP/uniq_ex_drop; rewrite // s_def /=. by exists (rcons s x); rewrite cat_rcons. - rewrite white_add_black big_set1 wreachex white1 white_add_stack. by rewrite !setDDl setUA setUAC setUid. - by rewrite m2_min; congr val; apply: eq_bigl=> y; rewrite /= big_set1. move: m2_min; rewrite (minn_idPl _) // => sn_min. have numx_le y : y \in wreach e x -> num e1 y >= num e1 x. move=> xy; rewrite (@leq_trans m) //; last first. by rewrite sn_min -ord_num// geq_bigmin_cond. by rewrite (subenv_num sube1) ?mem_head//= ffunE/= eqxx. have scc_max : gscc_of x \subset [set y in s2]. apply/subsetP=> y; rewrite inE=> y_sccx; apply: contraTT isT => yNs2. have xy : gconnect x y by have := y_sccx; rewrite mem_scc /= => /andP[]. have x_s2 : x \in s2 by rewrite mem_rcons mem_head. have /(connect_from (mem s2)) /= [y' []] := xy. rewrite (negPf yNs2) andbF implybF => [y'Ns2]. have neq_y'x : y' != x by apply: contraNneq y'Ns2 => ->. move=> /connect1r [] // x' xx's2 /= /andP [x'_s2 x'y'] y'y. have xx' : gconnect x x'. by apply: connect_sub xx's2 => u v /= /andP[_]; apply: connect1. have /or3P[] : [|| y' \in white e1, y' \in cover (esccs e1) | y' \in stack e1] by case: color4P. - move: x'_s2; rewrite mem_rcons in_cons => /predU1P [eq_x'x|x_s]. by rewrite succ_whiteF -?eq_x'x. have /(_ x') := Nbw1; rewrite (subsetP sb) => // /(_ isT). by move=> /pred0P /(_ y') /=; rewrite [_ \in _]x'y' /= => ->. - move=> /bigcupP [scc']. rewrite black_sccs1 inE => /andP[scc'_gsccs scc'_black]. move=> /def_scc - /(_ _ scc'_gsccs) eq_scc'; rewrite -eq_scc' in scc'_black. have : x \in gscc_of y'. have:= y_sccx; rewrite !mem_scc /= /symconnect andbC => /andP[yx _]. by rewrite (connect_trans y'y) //= (connect_trans xx') //= connect1. by move=> /(subsetP scc'_black); case: color4P x_gray. - rewrite s_def -cat_rcons mem_cat (negPf y'Ns2) /= => y'_stack. have xNstack: x \notin stack e. rewrite -(@uniq_catLR _ x s2) ?mem_cat ?x_s2 //. by rewrite cat_rcons -s_def wf_uniq. have x'Nstack: x' \notin stack e. rewrite -(@uniq_catLR _ x' s2) ?mem_cat ?x'_s2 //. by rewrite cat_rcons -s_def wf_uniq. have s2_white: {subset s2 <= white e}. move=> z z_s2; have: z \notin cover (esccs e). apply/negP=> /(subsetP (subset_cover (subenv_sccs sube1))). suff: z \in stack e1 by case: color4P. by rewrite s_def -cat_rcons mem_cat z_s2. wlog: / z \in stack e by case: color4P; do ?[exact|move=>?]. have us2e : uniq (s2 ++ stack e) by rewrite cat_rcons -s_def. by rewrite (uniq_catRL us2e) ?mem_cat ?z_s2. suff /numx_le : y' \in wreach e x. rewrite !(subenv_num sube1) ?mem_head//?in_cons ?y'_stack ?orbT//=. rewrite !ffunE/= eqxx (negPf neq_y'x) leqNgt wf_num_lt//. by rewrite wf_num_infty//; case: color4P y'_stack. rewrite !inE (@connect_trans _ _ x') //; last first. by rewrite connect1 /= ?s2_white. apply: connect_sub xx's2 => u v /= /andP[/s2_white uw uv]. by rewrite connect1 /= ?uw. have g1Nx : gray e1 :\ x = gray e. by rewrite (subenv_gray sube1) gray_add_stack // setU1K // white_grayF. have take_s : take (index x (stack e1)) (stack e1) = s. rewrite s_def index_cat /= eqxx addn0. rewrite (@uniq_catLR _ _ _ (x :: stack e)) -?s_def ?wf_uniq //. by rewrite mem_head /= ?s_def take_cat ltnn subnn take0 cats0. have drop_s : drop (index x (stack e1)).+1 (stack e1) = stack e. rewrite s_def index_cat /= eqxx addn0. rewrite (@uniq_catLR _ _ _ (x :: stack e)) -?s_def ?wf_uniq //. rewrite mem_head /= ?s_def drop_cat ltnNge leqW //. by rewrite subSn // subnn //= drop0. split=> //. - split=> //. + by apply: add_sccs_wf=> //; rewrite take_s //. + split=> //=. * move=> y; rewrite white_add_sccs// ?take_s//. rewrite set_infty_eq0 ?wf_num0//= => z; rewrite mem_rcons in_cons wf_num0//. by move=> /predU1P[->|/(subsetP sb)]; case: color4P x_stack. * move=> y; rewrite !take_s. rewrite /cover big_setU1/= -/(cover _). by rewrite set_infty_eq_infty wf_num_infty// !inE. suff: ~~ ([set y0 in rcons s x] \subset cover (esccs e1)). apply: contra => sx_in. by rewrite /cover (big_setD1 _ sx_in) /= subsetUl. apply: contraTN isT => /subsetP /(_ x); rewrite inE mem_rcons in_cons eqxx/=. by case: color4P x_gray => //= ??; apply. * move=> y /=; rewrite !take_s set_infty_eq_infty/= negb_or => /andP[ysx nNinfty]. by rewrite set_infty_id ?ysx// wf_num_lt. * by rewrite gray_add_sccs// ?take_s// setUCA setUA setD1K // wf_sn. * rewrite drop_s take_s// => z t z_stack t_stack. rewrite !set_infty_id/=; last 2 first. - move: e1_uniq; rewrite s_def stack_add_stack -cat_rcons. by move=>/uniq_catRL<- //; rewrite mem_cat orbC t_stack. - move: e1_uniq; rewrite s_def stack_add_stack -cat_rcons. by move=>/uniq_catRL<- //; rewrite mem_cat orbC z_stack. rewrite !(subenv_num sube1) ?ffunE/=; do ?by rewrite in_cons ?t_stack ?z_stack orbT. rewrite !ifN ?wf_num_stack//. - move: xe_uniq; rewrite /= andbC => /andP[_]. by apply: contra => /eqP<-. - move: xe_uniq; rewrite /= andbC => /andP[_]. by apply: contra => /eqP<-. + split=> //=; rewrite ?gray_add_sccs ?stack_add_sccs ?take_s ?drop_s// ?g1Nx. * move=> y z y_s z_s; rewrite !ffunE; rewrite !ifN /=; last 2 first. - case: (path.splitP x_stack) take_s drop_s e1_uniq => l1 l2 -> -> /uniq_catRL<-//. by rewrite mem_cat orbC z_s. - case: (path.splitP x_stack) take_s drop_s e1_uniq => l1 l2 -> -> /uniq_catRL<-//. by rewrite mem_cat orbC y_s. - by apply: wf_stack_to_stack => //; rewrite s_def mem_cat stack_add_stack inE !(y_s , z_s) !orbT. * move=> y y_s; rewrite !ffunE /= ifN; last first. case: (path.splitP x_stack) take_s drop_s e1_uniq => l1 l2 -> -> /uniq_catRL<-//. by rewrite mem_cat orbC y_s. have y_s1 : y \in stack e1. by rewrite s_def stack_add_stack mem_cat !inE y_s !orbT. have [z [z_g zLy yCz]] := wf_stack_to_gray e1_gwf y_s1. have zDx : z != x. apply: contraTneq zLy => ->. rewrite wf_num_stack // -ltnNge. move: e1_uniq; rewrite s_def !index_cat => uC. rewrite !ifN ?stack_add_stack /= ?eqxx ?addn0 //; last 2 first. - by rewrite -(uniq_catRL uC) stack_add_stack ?(mem_cat, inE, y_s, orbT). - by rewrite -(uniq_catRL uC) stack_add_stack ?(mem_cat, inE, eqxx, orbT). case: eqP y_s => [<-| _] /=; first by case: color4P x_white. by rewrite addnC ltnS leq_addl. exists z; split => //; first by rewrite -g1Nx !inE zDx. rewrite !ffunE ifN //= mem_rcons !inE (negPf zDx) /=. by apply/negP=> /(subsetP sb); case: color4P z_g. + move=> y; rewrite !inE white_add_sccs ?take_s //. move=> /predU1P [->|/Nbw1//]; apply/pred0P=> z //=. by have [/succ_whiteF->|] := boolP (z \in successors x). + rewrite sccs_add_sccs take_s //=; apply/setP=> scc. rewrite !inE black_add_sccs ?take_s//= black_sccs1 !inE. have x_s2 : x \in [set y in s2] by rewrite inE mem_rcons mem_head. have s2_gsccs : [set y in rcons s x] \in gsccs. apply/imsetP => /=; exists x => //. rewrite -[RHS](@def_scc _ edge _ x); last 2 first. * by apply/imsetP; exists x. * by rewrite !inE /symconnect ?connect0. apply/eqP; rewrite eqEsubset scc_max. have [scc' scc'_gsccs sub'] := is_subscc_in_scc sx_subscc. by rewrite (@def_scc _ edge scc') ?sub' //; apply: (subsetP sub'). have [scc_gsccs|] //= := boolP (scc \in gsccs); last first. by apply: contraNF; rewrite orbF => /eqP->. apply/idP/idP. move=> /predU1P [->|]. apply/subsetP => y; rewrite !inE mem_rcons in_cons. by case: eqP=> [->|] //= _ => /(subsetP sb). by move=> /subset_trans; apply; rewrite subsetU1. have [x_scc|xNscc] := boolP (x \in scc). by move=> _; rewrite -(def_scc scc_gsccs x_scc) // (def_scc s2_gsccs) ?eqxx. rewrite -subDset (setDidPl _); first by move->; rewrite orbT. by rewrite disjoint_sym (@eq_disjoint1 _ x) // => y; rewrite !inE. - rewrite /= /subenv gray_add_sccs ?take_s ?sb ?g1Nx ?eqxx /= ?drop_s //=. rewrite (subset_trans (subenv_black sube1)) ?subsetUr //=. rewrite (subset_trans (subenv_sccs sube1)) ?subsetUr //=. apply/andP; split. rewrite take_s. apply/forall_inP => y y_s. have yNIr : y \notin rcons s x. move: e1_uniq; rewrite s_def -cat_rcons => /uniq_catRL<-//. by rewrite mem_cat y_s orbT. have /(subenv_num sube1) : y \in stack (add_stack x e). by rewrite inE y_s orbT. rewrite !ffunE /= !ifN => [->||] //. by apply: contra yNIr => /eqP->; rewrite mem_rcons inE eqxx. by apply/'exists_eqP; exists ord0; rewrite drop0. - rewrite white_add_sccs ?take_s ?sb //. by rewrite white1 white_add_stack big_set1 wreachex setDDl. - rewrite big_set1 /= take_s; apply/eqP; rewrite eqn_leq leq_ord andbT. rewrite [X in X <= _](_ : infty = @inord infty infty); last by rewrite inordK. apply/bigmin_geqP => y /= He. rewrite !ffunE /=. case: (boolP (_ \in _)) => [|yNIs] //. have y_s : y \notin stack e1. apply/negP=> y_s. have := numx_le _ He. rewrite wf_num_stack // s_def. rewrite -cat_rcons !index_cat (negPf yNIs) size_rcons ifT; last first. by rewrite mem_rcons !inE eqxx. rewrite -cats1 index_cat ifN /= ?eqxx ?addn0. by rewrite leqNgt addSn ltnS leq_addr. have := e1_uniq. by rewrite s_def -cat_rcons cat_uniq rcons_uniq -andbA => /and3P[]. have nxP : 0 < num e1 x. by move: x_stack; rewrite num_stackP=> // /andP[]. case: (@color4P y _ e1_wf) y_s (numx_le _ He) => //. by rewrite -wf_num_infty // => /eqP->. rewrite -wf_num0 // => /eqP->; rewrite leqNgt. by move: x_stack; rewrite num_stackP=> // /andP[->]. Qed.
imports: mathcomp(all_ssreflect) bigmin extra