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, white e1 \subset white 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. rewrite wf_num0 //; have [xw|xNw]/= := boolP (x \in _); last first. move: dfsrec_correct => /(_ _ (subxx _)). case: (dfsrec _ _) => [m2 e1]. case; first exact: (pre_dfs_subroots (subD1set _ _)). move=> [e1_wf e1_nwf e1_gwf Nbw1 sccs_e1] sube1 white1 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 //=. by rewrite -setDDl white1 Nwreach ?(subND1 xNw). rewrite -(setD1K x_root) big_setU1 ?setD11 // bigmin_setU /= m2_min. congr (minn _ _); rewrite Nwreach // big_set1 ord_num //. case: stackP xNw => // [x_stack|x_sccs] _; first exact/esym/subenv_num. rewrite ?(num_inftyP _ _ _) //. by apply: (subsetP (subset_cover (subenv_sccs _))) x_sccs. 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 := post_dfs1 xw (pre_dfs_subroots _ pre). rewrite sub1set x_root => /(_ isT) {post_dfs1}. case=> [[e1_wf e1_cwf e1_gwf Nbw1 sccs_e1] sube1 white1 m1_min]. have [//|s1 s1_def s1b] := subenv_stackP _ sube1. have e1_uniq := wf_uniq e1_wf. rewrite big_set1 in white1 m1_min. case: post_dfs. - by rewrite subenv_white. - split=> // y z; rewrite grayE !inE s1_def mem_cat. case: (y \in s1) (subsetP s1b y) => //= [->//|_ /andP[yNb ys]]. move=> /andP[_ z_roots]; rewrite to_roots // grayE !inE. rewrite ys andbT; apply: contraNN yNb; apply/subsetP. by rewrite subenv_black. move=> [e2_wf e2_cwf e2_gwf Nbw2 sccs_e2] sube2 white2 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_white. 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 /= white1 !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 white2 white1 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_num //. have /orP[ys|ysccs] : (y \in stack e1) || (y \in cover (esccs e1)). + suff: y \notin white e1 by case: color4P. by rewrite white1 inE xy. + exact/esym/subenv_num. rewrite ?(num_inftyP _ _ _) //. by apply: (subsetP (subset_cover (subenv_sccs _))) ysccs. Qed.
imports: mathcomp(all_ssreflect) bigmin extra