proposition: Lemma dfs1P dfs x e (A := [set y in successors x]): dfs_correct dfs A (visit x e) -> dfs1_correct (dfs1 dfs) x e.
proof: Proof. rewrite /dfs1 => dfsP e_wf xNseen x_connected. have subexe: subenv e (visit x e) by exact: sub_visit. have num0x : num e x = infty by apply: notseen_num. have xNstack : x \notin stack e. by rewrite inE num0x ltnNge 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 (~: seen e) [set x] = x |: nexts (~: (x |: seen 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 seen1E]. have sube1 : subenv e e1 by apply: sub_trans subxe1. have num1x : num e1 x = sn e. by rewrite (sub_snum subxe1)// ?inE ?ffunE ?serialE/= ?eqxx// ltnS max_card. rewrite ?seen_visit ?serialE// in seen1E *. have lt_sn_sn1 : sn e < sn e1. by rewrite (leq_trans _ (leq_sn subxe1))// seen_visit// cardsU1 xNseen. have x_seen1 : x \in seen e1 by rewrite seen1E inE setU11. have x_stack : x \in stack e1. by rewrite (subsetP (sub_stack subxe1))//= stack_visit// setU11. have -> : (x |: new_stack (visit x e) e1) = new_stack e e1. by rewrite stack_visit// [_ |: stack e]setUC -setDDl setD1K// inE xNstack. have [min_after|min_before] := leqP; last first. do 2!constructor => //=. - rewrite nexts1E bigmin_setU big_set1 /= inordK ?num1x ?ltnS ?max_card//. by rewrite (minn_idPr _)// ltnW. - 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. rewrite seen_visit// !ffunE ?serialE//=. by rewrite eqxx cardsU1 xNseen 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 |: seen e)) A)) (@inord #|V| \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 num_lt_infty seen1E 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). - by rewrite nexts1E setUCA setUA seen1E. have all_geq y : y \in nexts (~: seen e) [set x] -> (#|seen e| <= num e1 y) * (num e1 y < infty). have := min_after; have sn_inord : sn e = @inord #|V| (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. by rewrite ltnS max_card leqnn. rewrite sn_inord (leq_trans (y_ge _))// ?inordK//; by rewrite num_lt_infty seen1E 2!inE yA orbT. constructor=> //=. - constructor=> //=; rewrite ?serialE ?seen_store ?sub_new_stack_seen//. + 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 num0x -leqNgt leqW ?max_card//= 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_seen (visit x e) e1. by apply: subsetP y_xee1; rewrite sub_new_stack_new_seen. rewrite inE seen1E in_setU seen_visit//; case: (y \in _ |: _) => //=. move=> /in_nextsW[z]; rewrite inE=> /(@connect1 _ edge). exact: connect_trans. have /(connect_from (mem (~: seen e))) [z []] := xy; rewrite inE. move=> eq_yz xz zy; have /all_geq [] : z \in nexts (~: seen e) [set x]. by apply/bigcupP; exists x; rewrite !inE. rewrite leqNgt -sub_num_lt// -num_lt_V// -leqNgt ltnS => 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 zNseen : z \notin seen e. rewrite inE -leqNgt ltn_neqAle eq_sym num_sccs// zNstack andbT. apply: contraTN isT => /(zNcover _ e_wf). by rewrite -num_sccs// num0x; elim: #|V|. move: eq_yz; rewrite zNseen /= => /andP[/eqP eq_yz _]. rewrite -eq_yz in zNstack z_stack. by rewrite !inE -num_lt_V// -leqNgt zNstack. + by move=> v; rewrite ffunE/=; case: ifP; rewrite ?max_num //. + move=> v; rewrite ffunE/=; case: ifPn; rewrite ?ltnn// => vNe12. by rewrite num_lt_V// seen_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 ?seen_store ?sub_new_stack_seen//. rewrite setDDr setDUl setDv set0D set0U setDIl !setDv setI0. split; do ?by [move=> ?; rewrite ?inE//=|]; last first. by rewrite seen1E -setUA setUCA -nexts1E. rewrite big1// => y xy; rewrite ffunE new_stackE ?inE//=. have y_seen1 : num e1 y < infty. by rewrite num_lt_infty seen1E -setUA setUCA -nexts1E inE xy orbT. apply/val_inj=> /=; case: ifPn; rewrite ?inordK//. rewrite all_geq//= -num_lt_V// -leqNgt; move: y_seen1; rewrite ltnS. by case: ltngtP. Qed.
imports: mathcomp(all_ssreflect) bigmin extra