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. move=> [gto_roots e_wf e_gwf black_sccs]; split=> //. by apply/subsetP=> x; rewrite !inE no_roots. split=> //; first by split=> //; first by exists [::] => //; apply/subsetP. split=> //; first by move=> x; rewrite no_roots. by left. by move=> y; rewrite inE => /andP[_ /existsP [x /and3P[->]]]. move=> x_root; have := dfs'_is_correct _ x_root; rewrite /dfs'_correct. case: ifPn=> [x_stack|xNstack]. move=> /(_ _ (subxx _)); case: (dfsrec' _ _) => [m2 e']. move=> e'_correct [to_roots e_wf e_gwf Nbw black_sccs]. have e_uniq := wf_stack_uniq e_wf. case: e'_correct; first exact: (pre_dfs_subroots (subD1set _ _)). move=> change_color [invariants monotony [pc1 pc2 pc3]]. split=> //. - rewrite -(setD1K x_root) subUset change_color sub1set !inE. have [//|xNblack /=] := boolP (x \in blacks _). by have [[s ->]] := monotony; rewrite mem_cat x_stack orbT. split=> //; split=> //. - move=> y y_root; have [->|neq_yx]:= eqVneq y x; last first. by rewrite geq_min pc1 ?orbT // !inE neq_yx. by have [[s -> _ _ _]] := monotony; rewrite rank_catl // geq_min leqnn. - right; case: (leqP (rank x (stack e)) m2) => [rx_small|/ltnW rx_big]. exists x => //; exists x; rewrite ?inE ?connect0 //. by have [[s ->]] := monotony; rewrite rank_catl. case: pc2 rx_big=> [->|[y]]; first by rewrite leqNgt rank_lt ?x_stack. rewrite !inE => /andP[neq_yx y_roots [z y_to_z m_def]]. by move=> m_small; exists y => //; exists z. - by move=> y y_xedge; rewrite (@leq_trans m2) ?pc3 // geq_min leqnn orbT. case: ifPn=> [x_black|xNblack] //=. move=> /(_ _ (subxx _)); case: (dfsrec' _ _) => [m2 e']. move=> e'_correct [to_roots e_wf e_gwf Nbw black_sccs]. case: e'_correct; first exact: (pre_dfs_subroots (subD1set _ _)). move=> change_color [[e'_wf e'_gwf keep_gray Nbw' sccs'_black] [mon1 mon2 mon3] [pc1 pc2 pc3]]. have e'_uniq := wf_stack_uniq e'_wf. split=> //. by rewrite -(setD1K x_root) subUset change_color sub1set !inE (subsetP mon2). have m2_rank: m2 <= infty by case: pc2=> [->|[?? [??->]]]; rewrite ?rank_le. split=> //; split=> //. - move=> y y_root; have [->{y y_root}|neq_yx]:= eqVneq y x; last first. by rewrite geq_min pc1 ?orbT // !inE neq_yx. rewrite rank_infty ?geq_min ?leqnn // sccs_stackF //. by apply: (subsetP (subset_cover mon3)); case: colorP x_black xNstack. - rewrite (minn_idPr _) //; case: pc2 => [->//|]; first by left. by move=> [y]; rewrite !inE => /andP[_ ?]; right; exists y. - by move=> y y_xedge; rewrite (@leq_trans m2) ?pc3 // geq_min leqnn orbT. have := dfs1_is_correct _ x_root; rewrite /dfs1_correct. case: (dfs1 _ _) => [m1 e1] post_dfs1. move=> /(_ e1); case: (dfsrec' _ _) => [m2 e2] post_dfs'. move=> pre {dfs1_is_correct dfs'_is_correct}. have [e_access_to e_wf e_gwf Nbw sccs_black] := pre. have e_uniq := wf_stack_uniq e_wf. have x_white : x \in whites e by case: colorP xNstack xNblack. have := post_dfs1 x_white (pre_dfs_subroots _ pre). rewrite sub1set x_root => /(_ isT) {post_dfs1}. case=> [x_black [[e1_wf e1_gwf Nbw1 keep_gray sccs_e1] [[s1 s1_def s1b] mo_b1 mo_sccs1] [pc1 pc2 pc3]]]. have e1_uniq := wf_stack_uniq e1_wf. case: post_dfs'. - by rewrite subCset setCK setUSS // keep_gray. - split=> // y; rewrite !inE s1_def mem_cat. case: (y \in s1) (subsetP s1b y) => //= [->//|_ /andP[yNb ys]]. move=> z; rewrite inE => /andP[_ z_roots]; rewrite e_access_to //. by rewrite !inE ys andbT; apply: contraNN yNb; apply/subsetP. move=> rootsDx_subset [[e2_wf e2_gwf Nbw2 keep_gray2 sccs_e2] [[s2 s2_def s2b] mo_b2 mo_sccs2] [pc21 pc22 pc23]]. have e2_uniq := wf_stack_uniq e2_wf. split. rewrite -(setD1K x_root) subUset rootsDx_subset andbT sub1set. by rewrite inE (subsetP mo_b2). split; first by rewrite keep_gray2 keep_gray. split. + exists (s2 ++ s1); first by rewrite s2_def s1_def catA. apply/subsetP=> y; rewrite mem_cat => /orP [/(subsetP s2b) //|]. by apply/subsetP/(subset_trans s1b). + exact/(subset_trans mo_b1). + exact/(subset_trans mo_sccs1). have m1_rank: m1 <= infty by case: pc2=> [->|[?? [??->]]]; rewrite ?rank_le. have m2_rank: m2 <= infty by case: pc22=> [->|[?? [??->]]]; rewrite ?rank_le. split. - move=> y y_roots; have [->|neq_yx] := eqVneq y x; last first. by rewrite (@leq_trans m2) ?geq_minr // pc21 // !inE neq_yx. have [xs|xNs] := boolP (x \in stack e1). by rewrite s2_def rank_catl // (@leq_trans m1) ?geq_minl // pc1 ?inE. have x_sccs2 : x \in cover (esccs e2). apply: (subsetP (subset_cover mo_sccs2)). by case: colorP xNs x_black. by rewrite rank_infty ?geq_min ?m1_rank //; case: colorP x_sccs2. - case: pc22 => [->|m2_reachable]. + rewrite (minn_idPl _) //; case: pc2=> [->|pc2]; [by left|]. case: ltngtP m1_rank => // [m1_lt _|]; last by left. right; exists x => //. case: pc2=> z; rewrite inE => /eqP -> [t x_to_t m1_def]. by exists t => //; rewrite s2_def rank_catl // -rank_lt -?m1_def. + case: (leqP m1 m2) => [m12|/ltnW m21]; last first. case: m2_reachable => y; rewrite !inE => /andP[_ y_root] [z y_to_z m2_def]. by right; exists y => //; exists z => //. case: ltngtP m1_rank => // [m1_lt _|]; last by left. right; exists x => //; case: pc2=> [m1_infty|[z]]. by rewrite m1_infty ltnn in m1_lt. rewrite inE => /eqP -> [t x_to_t m1_def]. by exists t => //; rewrite s2_def rank_catl // -rank_lt -?m1_def. - move=> y. rewrite !inE => /andP [y_s0 /existsP[z /and3P [z_s2 zNs0 z_to_y]]]. move: z_s2; rewrite s2_def mem_cat orbC. have [z_s1 _|/= zNs1 z_s2] := boolP (z \in stack e1). rewrite rank_catl; last by rewrite s1_def mem_cat y_s0 orbT. rewrite (@leq_trans m1) ?geq_minl // pc3 // inE y_s0. by apply/existsP; exists z; rewrite z_s1 zNs0. rewrite -s2_def (@leq_trans m2) ?geq_minr // pc23 // inE. rewrite s1_def mem_cat y_s0 orbT /=. apply/existsP; exists z; rewrite s2_def mem_cat z_s2 /= [X in _ && X]z_to_y. by rewrite -s1_def zNs1. Qed.
imports: mathcomp(all_ssreflect) extra