proposition: Lemma tarjan_rec_is_correct : tarjan_rec N setT e0 = (infty, Env setT [::] gsccs infty [ffun _ => infty]).
proof: Proof. have := @tarjan_rec_terminates N setT e0; rewrite /dfs_correct. case: tarjan_rec => [m e] []. - by rewrite ?leq_add ?leq_mul ?max_card. - do ![split=> //; rewrite /= ?cover0 ?gray0 ?set0D ?setU0 //]; do ?by[do [move=> ?|move/setP=> ?]; rewrite ?gray0 inE]. + by move=> x; rewrite ffunE whiteE gray0 !inE eqxx. + by move=> x; rewrite ffunE inE eq_sym. + by move=> x; rewrite ffunE. + by rewrite cards0. apply/setP=> y; rewrite !inE /= subset0 andbC; case: eqP => //= ->. by have /and3P [_ _ /negPf->]:= sccs_partition edge. move=> [[stack_wf _ _ e_nwf] _ _] sccse /subenv_gray graye. rewrite (eqP _ : \bigcup_(x in _) _ = setT) ?setDT => [whe ->|]; last first. rewrite -subTset; apply/subsetP=> y _; apply/bigcupP. by exists y; rewrite ?mem_wreach. have blacke : black e = setT. move/eqP: whe; rewrite whiteE graye gray0 set0U. by rewrite -subset0 subCset setC0 subTset => /eqP. rewrite /black_gsccs blacke ?graye ?gray0 ?setTD ?set0U// in sccse stack_wf. have {}sccse: esccs e = gsccs. by apply/setP=> scc; rewrite sccse inE subsetT andbT. have stacke : stack e = [::]. have := stack_wf; rewrite sccse cover_sccs setCT. by case: stack => // x s /(_ x); rewrite !inE eqxx. have sne : sn e = infty. by rewrite wf_sn// graye blacke gray0 set0U cardsT. have nume : num e = [ffun _ => infty]. apply/ffunP => x; rewrite ffunE; apply/eqP; rewrite wf_num_infty //=. by rewrite sccse cover_sccs. congr (_, _); last first. by case: (e) blacke sccse stacke sne nume => //= *; congr Env. rewrite big1 // => x _; apply/val_inj; rewrite /= ord_num //=. by apply/eqP; rewrite wf_num_infty // sccse cover_sccs inE. Qed.
imports: mathcomp(all_ssreflect) bigmin extra