proposition: Lemma dfs1P dfs x e (A := successors x) : dfs_correct dfs A (visit x e) -> dfs1_correct (dfs1 dfs) x e.
proof: Proof. rewrite /dfs1 => dfsP e_wf xNvisited x_connected. have subexe: subenv e (visit x e) by exact: sub_visit. have numx : num e x > infty by apply: num_gt_V. have xNstack : x \notin stack e. by rewrite inE -leqNgt (leq_trans _ numx) ?leqW ?max_card. have xe_wf : wf_env (visit x e). by apply: wf_visit => // y y_lt; rewrite x_connected ?inE. have nexts1E : nexts (~: visited e) [set x] = x |: nexts (~: (x |: visited e)) A. by rewrite nexts1_split ?setDE ?setCU 1?setIC 1?inE. case: dfsP => //=. rewrite stack_visit// => u v; rewrite in_setU1=> /predU1P[->|ue]; rewrite inE => /(@connect1 _ edge)// /(connect_trans _)->//. by rewrite x_connected// set11. move=> _ _ e1 //= -> -> e1_wf subxe1 [newc new_old visited1E]. have sube1 : subenv e e1 by apply: sub_trans subxe1. have num1x : num e1 x = sn e. by rewrite (sub_snum subxe1)// ?inE ?ffunE/= ?eqxx// max_card. rewrite visited_visit in visited1E *. have lt_sn_sn1 : sn e < sn e1. by rewrite (leq_trans _ (leq_sn subxe1))// visited_visit cardsU1 xNvisited. have x_visited1 : x \in visited e1 by rewrite visited1E inE setU11. have x_stack : x \in stack e1. by rewrite (subsetP (sub_stack subxe1))//= stack_visit// setU11. have [min_after|min_before] := leqP; last first. constructor => //=. rewrite nexts1E bigmin_setU big_set1 /= inordK ?num1x ?ltnS ?max_card//. by rewrite (minn_idPr _)// ltnW. constructor=> //=; last by rewrite nexts1E setUCA setUA visited1E. move=> y z; have [-> _|neq_yx] := eqVneq y x. by rewrite new_stackE ?inE// -num1x; apply: le_connect. rewrite -(@setUD _ (stack (visit x e))) ?sub_stack//. rewrite [in X in _ :|: X]stack_visit// setDUl setDv setU0. rewrite [_ :\: stack e](setDidPl _) ?disjoint1s//. rewrite setUC !in_setU1 (negPf neq_yx)/=. move=> y_e1 /predU1P[->|]; last exact: newc y_e1. have [t] := new_old y y_e1; rewrite !inE => t_le /connect_trans->//. rewrite (@le_connect (visit x e))// andbC; move: t_le. by rewrite visited_visit !ffunE /= eqxx cardsU1 xNvisited add1n !ltnS leqnn. move=> y; have [v ve xv] : exists2 v, v \in stack e & gconnect x v. have [|v] := @eq_bigmin_cond _ _ (mem (nexts (~: (x |: visited e)) A)) (inord \o num e1). rewrite card_gt0; apply: contraTneq min_before => ->. by rewrite big_set0 -leqNgt max_card. rewrite !inE => v_in min_is_v; move: min_before; rewrite min_is_v/=. rewrite inordK; last by rewrite ltnS num_le_infty visited1E inE v_in orbT. rewrite -sub_num_lt// => v_lt; exists v; rewrite ?inE//. move: v_in => /in_nextsW[z]; rewrite inE => /(@connect1 _ edge). by apply: connect_trans. rewrite -(@setUD _ (stack (visit x e))) ?sub_stack//. rewrite [in X in _ :|: X]stack_visit// setDUl setDv setU0. rewrite [_ :\: stack e](setDidPl _) ?disjoint1s// setUC !in_setU1. move=> /predU1P[->|]; first by exists v. move=> /new_old[z]; rewrite stack_visit// in_setU1. move=> /predU1P[->|]; last by exists z. by move=> yx; exists v; rewrite // (connect_trans yx). have all_geq y : y \in nexts (~: visited e) [set x] -> (#|visited e| <= num e1 y) * (num e1 y <= infty). have := min_after; have sn_inord : sn e = inord (sn e). by rewrite inordK// ltnS max_card. rewrite {1}sn_inord; move/bigmin_geqP => /(_ y) y_ge. rewrite nexts1E !inE => /predU1P[->|yA]; rewrite ?num1x ?max_card ?leqnn//. rewrite sn_inord (leq_trans (y_ge _))// ?inordK//; by rewrite ?ltnS num_le_infty visited1E 2!inE yA orbT. constructor => //=. - rewrite big1// => y xy; rewrite ffunE new_stackE ?inE//=. have y_visited1 : num e1 y <= infty. by rewrite num_le_infty visited1E -setUA setUCA -nexts1E inE xy orbT. apply/val_inj=> /=; case: ifPn; rewrite ?inordK//. by rewrite all_geq//= -num_lt_V// -leqNgt; move: y_visited1; case: ltngtP. - constructor => //=; rewrite ?visited_store ?sub_new_stack_visited//. + rewrite subUset sub_gsccs// andbT sub1set. suff -> : new_stack e e1 = gscc_of x by rewrite pblock_mem ?cover_sccs. apply/setP=> y; rewrite mem_scc /symconnect. have [->|neq_yx] := eqVneq y x. by rewrite connect0 inE xNstack inE num1x lt_sn_sn1. apply/idP/andP=> [|[xy yx]]. move=> y_ee1; have y_xee1 : y \in new_stack (visit x e) e1. by rewrite inE stack_visit// in_setU1 (negPf neq_yx)/= -in_setD. split; last first. have [z] := new_old _ y_xee1. rewrite stack_visit// in_setU1 => /predU1P[->//|/x_connected]. by move=> /(_ _ (set11 x))/(connect_trans _) xz /xz. have: y \in new_visited (visit x e) e1. by apply: subsetP y_xee1; rewrite sub_new_stack_new_visited. rewrite inE visited1E in_setU visited_visit//; case: (y \in _) => //=. move=> /in_nextsW[z]; rewrite inE=> /(@connect1 _ edge). exact: connect_trans. have /(connect_from (mem (~: visited e))) [z []] := xy; rewrite inE. move=> eq_yz xz zy; have /all_geq [] : z \in nexts (~: visited e) [set x]. by apply/bigcupP; exists x; rewrite !inE. rewrite leqNgt -sub_num_lt// -num_lt_V// -leqNgt => zNstack. have zNcover e' : wf_env e' -> z \in cover (esccs e') -> x \in cover (esccs e'). move=> e'_wf /bigcupP[C] Ce zC; apply/bigcupP; exists C => //. have /def_scc: C \in gsccs by apply: subsetP Ce; apply: sub_gsccs. move=> /(_ _ zC)<-; rewrite mem_scc /= /symconnect (connect_trans zy)//=. by apply: connect_sub xz => ?? /andP[_ /connect1]. rewrite leq_eqVlt num_sccs// num_lt_V// => /orP[|z_stack]. move=> /zNcover; rewrite -num_sccs// num1x => /(_ _) /eqP eq_V. by rewrite eq_V// ltnNge max_card in lt_sn_sn1. have zNvisited : z \notin visited e. rewrite inE -ltnNge ltn_neqAle zNstack andbT/= eq_sym num_sccs//. by apply: contraTN isT => /(zNcover _ e_wf); rewrite -num_sccs// gtn_eqF. move: eq_yz; rewrite zNvisited /= => /andP[/eqP eq_yz _]. rewrite -eq_yz in zNstack z_stack. by rewrite !inE -num_lt_V// -leqNgt zNstack. + move=> v; rewrite ffunE/=; case: ifPn; rewrite ?ltnn// => vNe12. by rewrite num_lt_V// visited_store. + move=> v; rewrite ffunE /= cover1U [in RHS]inE. by case: ifPn; rewrite ?eqxx//= => vNe12; rewrite -num_sccs//. + move=> y z; rewrite !ffunE; case: ifPn => _. by move=> /andP[/leq_ltn_trans Vsmall/Vsmall]; rewrite ltnNge max_card. by case: ifPn => _; [by rewrite ltnNge max_card andbF|exact : le_connect]. - rewrite /subenv /= (subset_trans (sub_sccs sube1)) ?subsetUr//=. apply/andP; split; apply/forallP => v; apply/implyP; rewrite ffunE/= new_stackE// ?inE. move=> vs; rewrite (sub_snum sube1)// leqNgt -!num_lt_V// -leqNgt ifN//. by apply/negP => /andP[/leq_ltn_trans Vlt/Vlt]; rewrite ltnNge max_card. by case: ifPn; [move=> _; rewrite ltnNge max_card|rewrite -sub_num_lt]. - rewrite /outenv stack_store ?visited_store ?sub_new_stack_visited//. rewrite setDDr setDUl setDv set0D set0U setDIl !setDv setI0. split; do ?by move=> ?; rewrite inE. by rewrite visited1E -setUA setUCA -nexts1E. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors