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 := rank x _. move=> x_white [access_to_x [e_wf e_gwf Nbw black_sccs]]. have e_uniq := @wf_uniq _ e_wf. case: post_dfs' => //=. split => //. move=> y z; rewrite grays_add_stack // => /setU1P [->|y_gray]; rewrite inE => /(@connect1 _ edge) //. by apply/connect_trans/access_to_x; rewrite ?set11. split=> //; do?[exact: add_stack_ewf|exact: add_stack_gwf]. move=> y /Nbw; rewrite whites_add_stack. rewrite ![[disjoint successors _ & _]]disjoint_sym. by apply/disjointWl/subsetDl. move=> [e1_wf e1_gwf Nbw1 black_sccs1] sube1 whites1 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_grays : x \in grays e1. by rewrite (subenv_grays sube1) grays_add_stack ?setU11. have rkx : rank x (x :: stack e) = rank x (stack e1). by rewrite s_def rank_catl ?mem_head. have sx_subscc : is_subscc edge [set y in rcons s x]. apply: (@is_subscc1 _ _ x); first by rewrite inE mem_rcons mem_head. move=> y; rewrite !inE mem_rcons in_cons => /predU1P [->//|y_s]; split. apply: (@wf_grays_to_stack e1) => //; first by rewrite s_def mem_cat y_s. rewrite -rkx s_def rank_catr //=; last first. by rewrite -(@uniq_catLR _ _ s) ?mem_cat ?y_s // -?s_def //. rewrite rankE mem_head (leq_trans (index_size _ _)) //. by rewrite size_rev leq_addr. have [] := @wf_stack_to_grays _ e1_gwf y; first by rewrite s_def mem_cat y_s. move=> z [z_gray rank_z] /connect_trans; apply. rewrite (@wf_grays_to_stack e1) // s_def. have := z_gray; rewrite graysE !(inE, s_def) mem_cat. case: (boolP (z \in s)) => [/(subsetP sb)->//|_ /= /andP [_ z_xe]]. rewrite !rank_catl ?mem_head //. move: z_xe; rewrite in_cons. have [->//|neq_zx /= z_s] := altP eqP. rewrite ltnW // rank_le_head //. rewrite -(@uniq_catLR _ _ (rcons s x)) ?mem_rcons ?mem_head //. by rewrite cat_rcons -s_def wf_uniq. by rewrite mem_cat mem_rcons mem_head. have wreachex : wreach e x = x |: \bigcup_(y in [set y in successors x]) wreach (add_stack x e) y. rewrite /wreach whites_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 #|V| (rank y (stack e1)). by rewrite wreachex bigmin_setU big_set1 //= /m rkx ord_rank // m_min. have succ_whiteF z : z \in successors x -> z \in whites e1 = false. move=> z_successor; apply/negbTE. rewrite whites1 whites_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 rank_x1 x_to_x1] : exists2 x1, rank x1 (stack e1) = m1 & gconnect x x1. have [] := @eq_bigmin_cond _ _ (pred_of_set (wreach e x)) (fun y => @inord #|V| (rank y (stack e1))). by apply/card_gt0P; exists x; rewrite mem_wreach. move=> y; rewrite !inE=> xy /(congr1 val)/=. rewrite -m2_min ord_rank // => m1_eq; exists y => //. by apply: connect_sub xy => u v /= /andP [_]; apply: connect1. have [x' [rank_x' x'_gray x_to_x' ]] : exists x', [/\ rank x' (stack e1) < rank x (stack e1), x' \in grays e1 & gconnect x x']. move: m1_small; rewrite -{}rank_x1 => rank_x1. have x1_stack : x1 \in stack e1. by rewrite -rank_lt ?(leq_trans rank_x1) // rank_le. have [z [z_gray rank_z y_to_z]] := wf_stack_to_grays e1_gwf x1_stack. exists z; split=> //; rewrite 2?inE ?z_gray ?andbT. - by rewrite (leq_ltn_trans rank_z) // (leq_trans rank_x1) /m ?rkx. - by rewrite (connect_trans x_to_x1). have neq_x'x : x' != x by apply: contraTneq rank_x' => ->; rewrite -ltnNge. split=> //. - split=> //; first exact: add_blacks_ewf. + split => //. move=> y z /=; rewrite grays_add_blacks => y_gray z_stack. apply: wf_grays_to_stack => //; apply: subsetP y_gray. by rewrite subD1set. move=> y /= y_stack; rewrite grays_add_blacks. have [z] // := wf_stack_to_grays 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 whites_add_blacks. 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_grays_to_stack e1_gwf) // ltnW. have /scc_sub := x'_scc. rewrite !inE (negPf neq_x'x) /=. by case: colorP x'_gray. - apply/and4P; split => //=. + rewrite grays_add_blacks (subenv_grays sube1) grays_add_stack ?setU1K //. by rewrite whites_graysF. + by rewrite (subset_trans (subenv_blacks sube1)) // subsetUr. + by rewrite -[esccs e]/(esccs (add_stack x e)) subenv_sccs. + apply/'exists_eqP/uniq_ex_drop; rewrite // s_def /=. by exists (rcons s x); rewrite cat_rcons. - rewrite whites_add_blacks big_set1 wreachex whites1 whites_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 _) // /m rkx => rkx_min. have rkx_le y : y \in wreach e x -> rank y (stack e1) >= rank x (stack e1). by move=> xy; rewrite rkx_min -ord_rank // geq_bigmin_cond. 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 whites e1, y' \in cover (esccs e1) | y' \in stack e1] by case: colorP. - 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: colorP x_grays. - 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_whites: {subset s2 <= whites 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: colorP. by rewrite s_def -cat_rcons mem_cat z_s2. wlog: / z \in stack e by case: colorP; 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 /rkx_le : y' \in wreach e x. rewrite s_def !rank_catl ?mem_head ?in_cons ?y'_stack ?orbT //=. by rewrite leqNgt rank_le_head. rewrite !inE (@connect_trans _ _ x') //; last first. by rewrite connect1 /= ?s2_whites. apply: connect_sub xx's2 => u v /= /andP[/s2_whites uw uv]. by rewrite connect1 /= ?uw. have g1Nx : grays e1 :\ x = grays e. by rewrite (subenv_grays sube1) grays_add_stack // setU1K // whites_graysF. 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=> //; rewrite ?grays_add_sccs ?stack_add_sccs ?take_s ?drop_s// ?g1Nx. exact: wf_grays_to_stack. exact: wf_stack_to_grays. + move=> y; rewrite !inE whites_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 blacks_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 grays_add_sccs ?take_s ?sb ?g1Nx ?eqxx /= ?drop_s //=. rewrite (subset_trans (subenv_blacks sube1)) ?subsetUr //=. rewrite (subset_trans (subenv_sccs sube1)) ?subsetUr //=. by apply/'exists_eqP; exists ord0; rewrite drop0. - rewrite whites_add_sccs ?take_s ?sb //. by rewrite whites1 whites_add_stack big_set1 wreachex setDDl. - rewrite big_set1 /= drop_s; apply/eqP; rewrite eqn_leq leq_ord andbT. rewrite -[#|V|]/(val ord_max); apply/bigmin_geqP => y /= /rkx_le. apply: contraTT; rewrite -!ltnNge ord_rank// rank_lt // => y_stack. rewrite !s_def !rank_catl ?mem_head ?in_cons ?y_stack ?orbT //=. by rewrite rank_le_head //; case: colorP x_white. Qed.
imports: mathcomp(all_ssreflect) bigmin extra