proposition: Lemma dfs1_is_correct dfs' (x : V) e : (dfs'_correct dfs' [set y in successors x] (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_stack_uniq e_wf. case: post_dfs' => //=. split => //; do?[exact: add_stack_ewf|exact: add_stack_gwf]; last first. move=> y /Nbw; rewrite whites_add_stack. rewrite ![[disjoint successors _ & _]]disjoint_sym. by apply/disjointWl/subsetDl. move=> y; rewrite grays_add_stack // => /setU1P [->|]; last first. move=> y_gray z; rewrite inE => /(@connect1 _ edge). by apply/connect_trans/access_to_x; rewrite ?set11. by move=> z; rewrite inE => /(@connect1 _ edge). move=> succ_bVg [[e1_wf e1_gwf Nbw1 keep_gray black_sccs1] [[s/= s_def sb] mo_b mo_sccs] [pc1 pc2 pc3]]. set s2 := rcons s x. have e1_uniq := wf_stack_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 keep_gray grays_add_stack ?setU11. 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 s_def rank_catl ?mem_head // 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 !(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_stack_uniq. by rewrite mem_cat mem_rcons mem_head. case: ltnP => [m1_small|m1_big] //=; rewrite !inE eqxx /=; split=> //. have [x1 rank_x1 x_to_x1] : exists2 x1, rank x1 (stack e1) = m1 & gconnect x x1. case: pc2 m1_small => [->|]; first by rewrite /m ltnNge ?rank_le. move=> [y]; rewrite inE => /(@connect1 _ edge) x_to_y. move=> [x1 y_to_x1 rank_x1 _]; exists x1 => //. by rewrite (connect_trans x_to_y). 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. - rewrite (leq_ltn_trans rank_z) // (leq_trans rank_x1) // /m. by rewrite s_def rank_catl ?mem_head. - 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 // {2}s_def rank_catl ?mem_head. - 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. have /subsetP /(_ z) := succ_bVg. rewrite 2!inE => /implyP. by case: (_ \in successors _) (_ == _) colorP => [] [] []. + rewrite grays_add_blacks keep_gray grays_add_stack //. by rewrite setU1K // whites_graysF. + 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. - split=> //=. + exists (rcons s x); first by rewrite cat_rcons. apply/subsetP=> y; rewrite !inE mem_rcons in_cons=> /predU1P [->|]. by rewrite eqxx. by move=> y_s; rewrite (subsetP sb) ?orbT. + by rewrite subsetU // mo_b orbT. - split=> //=. + move=> y; rewrite inE => /eqP->. by rewrite s_def rank_catl ?mem_head // ltnW. + by right; exists x; rewrite ?set11 //; exists x1. + move=> y; rewrite inE => /andP [y_stack /existsP]. move=> [z /and3P[z_stack1 zNstack zy]]. have [eq_zx|neq_zx] := eqVneq z x. by rewrite pc1 // -eq_zx inE. apply: pc3; rewrite inE in_cons y_stack orbT /=. apply/existsP; exists z. by rewrite z_stack1 in_cons negb_or neq_zx zNstack. 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 [x' [y' [x'_s2 y'Ns xx' x'y' y'y]]] := path_xset_xedge xy x_s2 yNs2. apply: contraNN y'Ns => _. have: y' \in ([set y in stack e1] :|: (\bigcup_(scc in esccs e1) scc :|: whites e1)). by rewrite !inE; case: colorP. rewrite 3!inE => /or3P[]. - rewrite s_def -cat_rcons mem_cat => /orP[//|y'_stack]. have xNstack: x \notin stack e. rewrite -(@uniq_catLR _ x s2) ?mem_cat ?x_s2 //. by rewrite cat_rcons -s_def wf_stack_uniq. have x'Nstack: x' \notin stack e. rewrite -(@uniq_catLR _ x' s2) ?mem_cat ?x'_s2 //. by rewrite cat_rcons -s_def wf_stack_uniq. have rank_y': rank y' (x :: stack e) < rank x (x :: stack e). by rewrite rank_le_head //. have neq_y'x : y' != x by apply: contraTneq rank_y' => ->; rewrite ltnn. have [eq_x'x|neq_x'x] := eqVneq x' x. have := pc1 y'; rewrite inE -eq_x'x => /(_ x'y'). rewrite leqNgt (leq_trans _ m1_big) // /m. by rewrite s_def rank_catl ?in_cons ?y'_stack ?orbT. apply: contraTT rank_y' => y'Ns2; rewrite -leqNgt. rewrite [rank y' _]rank_cons (negPf neq_y'x) /=. have := pc3 y'; rewrite inE in_cons y'_stack orbT /=. rewrite {2}s_def -cat_rcons rank_catl // => /(_ _) /(leq_trans _) -> //. apply/existsP; exists x'; rewrite s_def -cat_rcons mem_cat x'_s2 /=. by rewrite in_cons (negPf neq_x'x) /= x'Nstack. - 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. - move: x'_s2; rewrite mem_rcons in_cons => /predU1P [eq_x'x|x_s]. have /subsetP /(_ y') := succ_bVg. by rewrite 2!inE -eq_x'x => /(_ x'y'); case: colorP. have /(_ x') := Nbw1; rewrite (subsetP sb) => // /(_ isT). by move=> /pred0P /(_ y') /=; rewrite [_ \in _]x'y' /= => ->. 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_stack_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_stack_uniq //. rewrite mem_head /= ?s_def drop_cat ltnNge leqW //. by rewrite subSn // subnn //= drop0. have g1Nx : grays e1 :\ x = grays e. by rewrite keep_gray grays_add_stack // setU1K // whites_graysF. 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 //=. rewrite 2!inE; have /subsetP /(_ z) := succ_bVg. by rewrite 2!inE => /implyP; rewrite -negb_imply orbC => ->. + by rewrite grays_add_sccs ?take_s ?g1Nx. + 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. - split=> //. + rewrite stack_add_sccs drop_s; exists [::] => //. by apply/subsetP=> y; rewrite inE. + by rewrite blacks_add_sccs ?take_s// (subset_trans mo_b) ?subsetU1. + by rewrite sccs_add_sccs take_s (subset_trans mo_sccs) ?subsetU1. - split=> //; do ?by [left]. + move=> y; rewrite inE => /eqP->. by rewrite stack_add_sccs drop_s leqNgt rank_lt ?whites_stackF. + move=> y; rewrite inE stack_add_sccs drop_s => /andP[_ /existsP]. by move=> [z /and3P[->]]. Qed.
imports: mathcomp(all_ssreflect) extra