proposition: Lemma dfsP dfs1 dfsrec (roots : {set V}) e: (forall x, x \in roots -> dfs1_correct dfs1 x e) -> (forall x, x \in roots -> forall e1, subenv e e1 -> dfs_correct dfsrec (roots :\ x) e1) -> dfs_correct (dfs dfs1 dfsrec) roots e.
proof: Proof. rewrite /dfs => dfs1P dfsP e_wf roots_connected. case: pickP => /= [x x_roots|]; last first. move=> r0; have {r0}r_eq0 : roots = set0 by apply/setP=> x; rewrite inE. do ?constructor=> //=; rewrite ?setDv ?r_eq0 ?nexts0 ?sub0set ?eqxx ?setU0 ?big_set0 //=; by move=> ?; rewrite inE. have [numx_gt|numx_le]/= := ltnP; last first. have x_visited : x \in visited e by rewrite inE. case: dfsP => //= [u v ve|_ _ e1 ->-> e1_wf subee1 [new1c new1old visited1E]]. by rewrite inE => /andP[_ v_roots]; rewrite roots_connected. constructor => //=. rewrite -[in RHS](setD1K x_roots) nextsU nexts1 inE x_visited/= setU0. by rewrite bigmin_setU /= big_set1/= (@sub_snum e e1)// inordK//. constructor=> //=; rewrite -(setD1K x_roots) nextsU nexts1 inE x_visited/=. by rewrite setU0 setUCA setUA [x |: _](setUidPr _) ?sub1set. case: dfs1P => //=; first by rewrite inE -ltnNge. by move=> u v ue; rewrite inE => /eqP->; apply: roots_connected. move=> _ _ e1 -> -> e1_wf subee1 [new1c new1old visited1E]. case: dfsP => //= [u v ue1|_ _ e2 -> -> e2_wf sube12 [new2c new2old visited2E]]. rewrite inE => /andP[_ v_roots]. have [ue|uNe] := boolP (u \in stack e); first by rewrite roots_connected. have [|w we] := new1old u; first by rewrite inE ue1 uNe. by move=> /connect_trans->//; rewrite roots_connected//. have sube2 : subenv e e2 by exact: sub_trans sube12. have nexts_split : nexts (~: visited e) roots = nexts (~: visited e) [set x] :|: nexts (~: visited e1) (roots :\ x). rewrite -[in LHS](setD1K x_roots) nextsU visited1E. by rewrite setCU nextsUI// nexts_id. constructor => //=. rewrite (eq_bigr (inord \o num e2)). by rewrite -[LHS]/(val (ord_minn _ _)) -bigmin_setU /= -nexts_split. move=> y y_in; rewrite /= (@sub_snum e1 e2)// num_le_infty. by rewrite visited1E setUC inE y_in. constructor => /=. + rewrite -(@setUD _ (stack e1)) ?sub_stack//. apply: connectedU => // y z; last first. rewrite !new_stackE// ?inE => /andP[y_ge y_lt] /andP[z_ge z_lt]. rewrite (@le_connect e2) // z_lt (leq_trans _ z_ge)//. by rewrite (sub_vnum sube12)// ltnW. rewrite !new_stackE// ?inE => /andP[y_ge y_lt] /andP[z_ge z_lt]. have [|r] := new2old y; rewrite ?new_stackE ?inE ?y_ge//. move=> r_lt /connect_trans->//; have [rz|zr] := leqP (num e1 r) (num e1 z). by rewrite (@le_connect e1)// rz/=. by rewrite new1c ?new_stackE ?inE ?z_ge ?z_lt //= (leq_trans z_ge)// ltnW. + move=> y; rewrite ?new_stackE ?inE// => /andP[y_ge y_lt]. have [y_lt1|y_ge1] := ltnP (num e1 y) (sn e1). have [|r] := new1old y; last by exists r. by rewrite new_stackE ?inE// ?y_lt1 -(sub_vnum sube12) ?y_ge. have [|r r_lt1 yr] := new2old y; first by rewrite !inE -leqNgt y_ge1//. rewrite ?inE in r_lt1; have [r_lt|r_ge] := ltnP (num e r) (sn e). by exists r; rewrite ?inE. have [|r' r's rr'] := new1old r; first by rewrite ?inE -leqNgt r_ge r_lt1. by exists r'; rewrite // (connect_trans yr rr'). + by rewrite visited2E {1}visited1E nexts_split setUA. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors