proposition: Lemma dfs'_is_correct dfs1 dfsrec' (roots : {set V}) e : (forall x, x \in roots -> dfs1_correct dfs1 x e) -> (forall x, x \in roots -> forall e1, whites e1 \subset whites e -> dfs'_correct dfsrec' (roots :\ x) e1) -> dfs'_correct (dfs' dfs1 dfsrec') roots e.
proof: Proof. move=> dfs1_is_correct dfs'_is_correct; rewrite /dfs'_correct /dfs'. case: pickP => [x|no_roots]; last first. have roots0 : roots = set0 by apply/setP=> y; rewrite no_roots inE. move=> [gto_roots [e_wf e_gwf black_sccs]]. by split=> //; rewrite ?roots0 ?big_set0 ?setD0. move=> x_root; have := dfs'_is_correct _ x_root; rewrite /dfs'_correct. move=> dfsrec'_correct pre. have [to_roots [e_wf e_gwf Nbw black_sccs]] := pre. have e_uniq := @wf_uniq _ e_wf. case: ifPn=> [xsVb|xNsVb]. move: dfsrec'_correct => /(_ _ (subxx _)); case: (dfsrec' _ _) => [m2 e1]. case; first exact: (pre_dfs_subroots (subD1set _ _)). move=> [e1_wf e1_gwf Nbw1 sccs_e1] sube1 whites1 m2_min. have [//|s1 s1_def sb] := subenv_stackP _ sube1. have e1_uniq := wf_uniq e1_wf. split=> //. rewrite -(setD1K x_root) big_setU1 ?setD11 //=. rewrite -setDDl whites1 Nwreach; last by case: colorP xsVb. by rewrite [whites e :\ _](setDidPl _) // disjoints1; case: colorP xsVb. rewrite -(setD1K x_root) big_setU1 ?setD11 // bigmin_setU /= m2_min. congr (minn _ _); rewrite Nwreach; last by case: colorP xsVb. rewrite big_set1 ord_rank // s1_def. case: (boolP (_ \in stack e)) xsVb => /= [/rank_catl->|xNs x_black] //. rewrite !rank_infty // -s1_def; case: colorP xNs x_black => //. by move=> /(subsetP (subset_cover (subenv_sccs sube1))); case: colorP. have := dfs1_is_correct _ x_root; rewrite /dfs1_correct. case: (dfs1 _ _) => [m1 e1] post_dfs1. move: dfsrec'_correct => /(_ e1). case: (dfsrec' _ _) => [m2 e2] post_dfs' {dfs1_is_correct dfs'_is_correct}. have x_white : x \in whites e by case: colorP xNsVb. have := post_dfs1 x_white (pre_dfs_subroots _ pre). rewrite sub1set x_root => /(_ isT) {post_dfs1}. case=> [[e1_wf e1_gwf Nbw1 sccs_e1] sube1 whites1 m1_min]. have [//|s1 s1_def s1b] := subenv_stackP _ sube1. have e1_uniq := wf_uniq e1_wf. rewrite big_set1 in whites1 m1_min. case: post_dfs'. - by rewrite subenv_whites. - split=> // y z; rewrite graysE !inE s1_def mem_cat. case: (y \in s1) (subsetP s1b y) => //= [->//|_ /andP[yNb ys]]. move=> /andP[_ z_roots]; rewrite to_roots // graysE !inE. rewrite ys andbT; apply: contraNN yNb; apply/subsetP. by rewrite subenv_blacks. move=> [e2_wf e2_gwf Nbw2 sccs_e2] sube2 whites2 m2_min. have [//|s2 s2_def s2b] := subenv_stackP _ sube2. have e2_uniq := wf_uniq e2_wf. have split_wreach : \bigcup_(y in roots) wreach e y = wreach e x :|: \bigcup_(y in roots :\ x) wreach e1 y. rewrite -{1}(setD1K x_root) big_setU1 ?setD11 //=; apply/setP => y. rewrite !in_setU; have [//|/=Nxy] := boolP (_ \in wreach _ _). apply/bigcupP/bigcupP=> - [] z z_roots zy; exists z => //; last first. rewrite !inE in zy *; apply: connect_sub zy => u v /= /andP [uw uv]. by rewrite connect1 //= uv andbT; apply: subsetP uw; rewrite subenv_whites. apply: contraTT isT => Nzy; move: zy; rewrite !inE in Nxy Nzy *. move=> /(connect_from (predC (connect (wedge e) x))) /= [t] /= [xtxy zt ty]. move: zt; rewrite (@eq_connect _ _ (wedge e1)); last first. by move=> u v /=; rewrite !inE /= whites1 !inE andbA. case: (altP eqP) xtxy => /= [<-|neq_yt]; first by rewrite (negPf Nzy). by rewrite implybF negbK => /connect_trans /(_ ty); rewrite (negPf Nxy). split => //; first exact: subenv_trans sube2. by rewrite whites2 whites1 split_wreach setDDl. rewrite m1_min m2_min split_wreach bigmin_setU /=. congr (minn (val _) _); apply: eq_bigr => y xy; apply/val_inj=> /=. rewrite !ord_rank //. have /orP[ys|ysccs] : (y \in stack e1) || (y \in cover (esccs e1)). + suff: y \notin whites e1 by case: colorP. by rewrite whites1 inE xy. + by rewrite s2_def rank_catl. + rewrite !rank_infty ?sccs_stackF //. by apply: subsetP ysccs; rewrite subset_cover ?subenv_sccs. Qed.
imports: mathcomp(all_ssreflect) bigmin extra