From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype finfun bigop finset.
From mathcomp Require Import path fingraph.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Section Kosaraju.

Variable T : finType.
Implicit Types s : {set T}.
Implicit Types l : seq T.
Implicit Types A B C : pred T.
Implicit Types x y z : T.

(* Some missing theorems of the library *)
Section Lib.

Lemma disjoint_setU s1 s2 A  :
   [disjoint s1 :|: s2 & A] = [disjoint s1 & A] && [disjoint s2 & A].
Proof.
apply/pred0P/andP => [H|[/pred0P H1 /pred0P H2 y]].
  by split; apply/pred0P => y; have := H y; rewrite !inE; do 3 case (_ \in _).
by have:= H1 y; have:= H2 y; rewrite !inE; do 3 case (_ \in _).
Qed.

Lemma disjoint_setUr s1 s2 A :
   [disjoint A & s1 :|: s2] = [disjoint A & s1] && [disjoint A & s2].
Proof.
apply/pred0P/andP => [H|[/pred0P H1 /pred0P H2 y]].
  by split; apply/pred0P => y; have := H y; rewrite !inE; do 3 case (_ \in _).
by have:= H1 y; have:= H2 y; rewrite !inE; do 3 case (_ \in _).
Qed.

Lemma disjoint_catr l1 l2 A :
       [disjoint A & l1 ++ l2 ] = [disjoint A & l1] && [disjoint A & l2].
Proof.  by rewrite ![[disjoint A & _]]disjoint_sym; exact: disjoint_cat. Qed.

Lemma disjoint_set1 x A : [disjoint [set x] & A] = (x \notin A).
Proof.
apply/pred0P/idP => [/(_ x)|H y]; first by rewrite !inE eqxx; case: (_ \in _).
by rewrite !inE; case: eqP => [->|]; move: H; case: (_ \in _).
Qed.

Lemma disjoint_setU1 x s A :
   [disjoint x |: s & A] = (x \notin A) && [disjoint s & A].
Proof. by rewrite disjoint_setU disjoint_set1. Qed.

Lemma disjoint_setU1r x s A :
   [disjoint A & x |: s] = (x \notin A) && [disjoint A & s].
Proof. by rewrite ![[disjoint A & _]]disjoint_sym; exact: disjoint_setU1. Qed.

Lemma disjoint_consr x l A :
   [disjoint A & x :: l] = (x \notin A) && [disjoint A & l].
Proof.  by rewrite ![[disjoint A & _]]disjoint_sym disjoint_cons. Qed.

Lemma disjoint_transr A B C :
   B \subset C -> [disjoint A & C] -> [disjoint A & B].
Proof.  by rewrite ![[disjoint A & _]]disjoint_sym; exact: disjoint_trans. Qed.

End Lib.

Section Stack.

Section Rconnect.

Variable r : rel T.

(* x is connected to y avoiding elements of l *)
Definition rconnect s := 
   connect [rel x y | (r x y) && (y \notin s)].

Local Notation "x -[ s ]-> y" := (rconnect s x y) 
  (at level 10, format "x  -[ s ]->  y").

Local Notation "x -[]-> y" := (rconnect set0 x y) 
  (at level 10, format "x  -[]->  y").

Lemma path_relE s x p : 
  path [rel x y | (r x y) && (y \notin s)] x p = path r x p && [disjoint p & s].
Proof.
elim: p x => //= [_|y p IH x]; first by rewrite disjoint_has.
rewrite IH disjoint_cons -!andbA.
by case: (_ \notin _); rewrite ?andbF.
Qed.

Lemma rconnectP s x y :
   reflect 
    (exists2 p, path r x p & ((y = last x p) /\ [disjoint p & s]))
    (x -[s]-> y).
Proof.
apply: (iffP connectP) => [[p Hp Hr]|[p Hp [Hr1 Hr2]]].
  by exists p; move: Hp; rewrite path_relE => /andP[].
by exists p; rewrite ?path_relE ?Hp.
Qed.

Lemma rconnect_set0  : rconnect set0 =2 connect r.
Proof. by apply: eq_connect => x y; rewrite /= inE andbT. Qed.

Lemma rconnect_ref s : reflexive (rconnect s).
Proof. by rewrite /rconnect. Qed.

Lemma rconnect1 s x y : y \notin s -> r x y -> x -[s]-> y.
Proof.
move=> yNIs Rxy; apply/rconnectP; exists [::y]; first by rewrite /= Rxy.
by split=> //; rewrite disjoint_cons yNIs; apply/pred0P.
Qed.

Lemma rconnect_trans s : transitive (rconnect s).
Proof. by apply: connect_trans. Qed.

Lemma rconnect_subset (s1 s2 : {set T}) x y : 
  {subset s1 <= s2} ->  x -[s2]-> y -> x -[s1]-> y.
Proof.
move=> Hs /rconnectP[p Hp [Hr Hl]].
apply/rconnectP; exists p => //; split => //.
by apply: disjoint_transr Hl; apply/subsetP; exact: Hs.
Qed.

Lemma rconnect_setU s1 s2 x y : 
  [disjoint [set z | x -[s1]-> z && z -[s1]-> y] & s2] ->
  x -[s1]-> y ->  x -[s2 :|: s1]-> y.
Proof.
move=> /pred0P Hr /rconnectP[p Hp [Hl Hd]].
apply/rconnectP; exists p => //; split => //.
rewrite disjoint_setUr Hd andbT.
apply/pred0P => t /=.
have [tIp|//] := boolP (t \in p); have [tIs2|//] := boolP (t \in s2).
have := Hr t; rewrite !inE tIs2 andbT => /idP[].
move/splitPr: tIp Hp Hl Hd => [l3 l4 Hp Hl Hd].
apply/andP; split; apply/rconnectP.
  exists (rcons l3 t).
    by move: Hp; rewrite -cat_rcons cat_path => /andP[].
  split; first by rewrite last_rcons.
  by move: Hd; rewrite -cat_rcons disjoint_cat => /andP[].
exists l4.
  by move: Hp; rewrite -cat_rcons cat_path last_rcons => /andP[].
split; first by move: Hl; rewrite last_cat.
by move: Hd; rewrite -cat_rcons disjoint_cat => /andP[].
Qed.

Lemma rconnect_setU1r s x y z :
  ~~ z -[s]-> y ->  x -[s]-> y -> x -[z |: s]-> y.
Proof.
move=> NCzy /rconnectP[p Prxp [Lxp Dps]].
elim: p x Prxp Lxp Dps NCzy =>
   /= [x _ -> _ _| t p IH x /andP[Rxt Prtp] Ltp Dtps NCzy].
  by rewrite rconnect_ref.
have/rconnectP[p1 Prtp1 [Ltp1 Dp1zs]] : t -[z |: s]-> y.
  apply: IH => //.
  apply: disjoint_trans Dtps; apply/subsetP=> i.
  by rewrite inE orbC => ->.
apply/rconnectP; exists (t :: p1) => //=; first by rewrite Rxt.
split=> //.
rewrite disjoint_cons Dp1zs andbT inE negb_or.
have /pred0P/(_ t)/= := Dtps.
rewrite !inE eqxx /= andbC => -> /=.
apply: contra NCzy => /eqP<-.
apply/rconnectP; exists p1 => //; split=> //.
apply: disjoint_transr Dp1zs.
by apply/subsetP=> j; rewrite inE orbC => ->.
Qed.

Lemma rconnect_setU1l s x y z : 
  ~~ (x -[s]-> z) ->  x -[s]-> y -> x -[z |: s]-> y.
Proof.
move=> NCxz /rconnectP[p Pxp [Lxp Dps]].
elim: p x Pxp Lxp Dps NCxz =>
        /= [x _ -> _ _|t p IH x /andP[Rxt Prtp] Lzp Dtps NCxz].
  by rewrite rconnect_ref.
have/rconnectP[p1 Przp1 [Ltp1 Dp1s]] : t -[z |: s]-> y.
  apply: IH => //.
    by move: Dtps; rewrite disjoint_cons => /andP[].
  apply: contra NCxz => /rconnectP[p1 Przp1 [Ltp1 Dp1s]].
  apply/rconnectP; exists (t :: p1) => /=; first by rewrite Rxt.
  split => //.
  rewrite disjoint_cons.
  have [zIs|//] := boolP (_ \in _); have /pred0P/(_ t)/= := Dtps.
  by rewrite !inE eqxx zIs.
have [/eqP tEz | tDz] := boolP (t == z).
  case/negP: NCxz; rewrite -tEz.
  apply/rconnectP; exists [:: t] => //=; first by rewrite Rxt.
  split => //.
  apply: disjoint_trans Dtps; apply/subsetP=> i; rewrite !inE => /eqP->.
  by rewrite eqxx.
apply/rconnectP; exists (t :: p1) => //=; first by rewrite Rxt.
split=> //.
rewrite disjoint_cons !inE negb_or tDz.
have /pred0P/(_ t)/= := Dtps.
by rewrite !inE eqxx /= => ->.
Qed.

Lemma rconnect_id_setU1 s x y : x -[x |: s]-> y = x -[s]-> y.
Proof.
apply/idP/idP.
  by apply: rconnect_subset => i; rewrite inE orbC => ->.
case/rconnectP=> p; elim/last_ind: p y => /= [_ y [-> _]|p /= z IH y].
  by exact: rconnect_ref.
rewrite last_rcons => Prx {y}[->].
have  [/eqP-> _|zDx] := boolP (z == x); first by exact: rconnect_ref.
elim/last_ind: p IH Prx => /= [_ /andP[Rxz _] HD|p t _].
  apply/rconnectP; exists [::z] => /=; first by rewrite Rxz.
  split=> //.
  by move: HD; rewrite !disjoint_setU1r !inE eq_sym (negPf zDx).
rewrite !(last_rcons, rcons_path) => IH /andP[HH Rtz] HD.
have [/eqP- tEx |tDx] := boolP (t == x).
  apply/rconnectP; exists [::z] => /=; first by rewrite -tEx Rtz.
  split => //; rewrite disjoint_cons /=.
  have/pred0P/(_ z)/= := HD.
  rewrite !mem_rcons !inE eqxx (negPf zDx) /= => ->/=.
  by apply/pred0P=> i.
have /rconnectP[p1 Prap1 [Lxp1 Dp1s]] : x -[x |: s]-> t.
  apply: IH => //; split => //; apply: disjoint_trans HD.
  by apply/subsetP => i; rewrite !(mem_rcons, inE); case: (i == z).
apply/rconnectP; exists (rcons p1 z) => /=.
  by rewrite rcons_path Prap1 -Lxp1.
split; first by rewrite last_rcons.
rewrite -cats1 disjoint_cat Dp1s disjoint_cons /=.
have/pred0P/(_ z)/= := HD.
rewrite !mem_rcons !inE eqxx (negPf zDx) /= => ->/=.
by apply/pred0P=> i.
Qed.

(* x is biconnected to y avoiding the elements of s *)
Definition requiv s x y  :=  x -[s]-> y && y -[s]-> x.

Local Notation "x =[ s ]= y" := (requiv s x y) 
  (at level 10, format "x  =[ s ]=  y").

Local Notation "x =[]= y" := (requiv set0 x y) 
  (at level 10, format "x  =[]=  y").

Lemma requiv_set0 : requiv set0 =2 (fun x y => connect r x y && connect r y x).
Proof. by move=> x y; rewrite /requiv !rconnect_set0. Qed.

Lemma requiv_ref s : reflexive (requiv s).
Proof. by move=> x; apply/andP; rewrite /rconnect. Qed.

Lemma requiv_sym s : symmetric (requiv s).
Proof. by move=> x y; apply/andP/andP=> [] []. Qed.

Lemma requiv_trans s : transitive (requiv s).
Proof.
move=> x y z /andP[Cyx Cxy] /andP[Cxz Czx].
by rewrite /requiv (rconnect_trans Cyx) ?(rconnect_trans Czx).
Qed.

Lemma lrequiv_subset s1 s2 x y : {subset s1 <= s2} -> x =[s2]= y -> x =[s1]= y.
Proof. 
by move=> Hs /andP[Cxy Cyx]; rewrite /requiv !(rconnect_subset Hs).
Qed.

(* Canonical element in a list : find the first element of l1
   that is equivalent to x avoiding l2 *)
Definition rcan x p := nth x p.2 (find (requiv p.1 x) p.2).

Notation "C[ x ]_ p" := (rcan x p) 
  (at level 9, format "C[ x ]_ p").

Lemma mem_rcan x p : x \in p.2 -> C[x]_p \in p.2.
Proof.
move=> xIp1; rewrite /rcan.
by case: (leqP (size p.2) (find (requiv p.1 x) p.2)) => H1;
  [rewrite nth_default | rewrite mem_nth].
Qed.

Lemma rcan_cons x y s l : 
  C[x]_(s, y :: l) =  if x =[s]= y then y else C[x]_(s,l).
Proof.  by rewrite /rcan /=; case: (boolP (requiv _ _ _)) => Hr. Qed.

Lemma rcan_cat x s l1 l2 : x \in l1 -> C[x]_(s, l1 ++ l2) = C[x]_(s, l1).
Proof.
move=> xIl1.
rewrite /rcan find_cat; case: (boolP (has _ _)).
  by rewrite nth_cat has_find => ->.
by move/hasPn/(_ x xIl1); rewrite requiv_ref.
Qed.

Lemma requiv_can x s l : x \in l -> C[x]_(s, l) =[s]= x.
Proof.
move=> xIl; rewrite requiv_sym; apply: nth_find.
by apply/hasP; exists x => //; exact: requiv_ref.
Qed.

(* x occurs before y in l *)
Definition before l x y  := index x l <= index y l.

Lemma before_filter_inv a x y l (l1 := [seq i <- l | a i]) :
  x \in l1 -> y \in l1 -> before l1 x y -> before l x y.
Proof.
rewrite {}/l1 /before; elim: l => //= z l IH.
case E : (a z) => /=.
  rewrite !inE ![_ == z]eq_sym.
  by case: eqP => //= Hx; case: eqP.
move=> xIl yIl; move: (xIl) (yIl).
rewrite !mem_filter.
case: eqP => [<-|_ _]; first by rewrite E.
case: eqP => [<-|_ _]; first by rewrite E.
by apply: IH.
Qed.

Lemma before_filter x y l a (l1 := [seq i <- l | a i]) :
  x \in l1 -> before l x y -> before l1 x y.
Proof.
rewrite {}/l1 /before; elim: l => //= z l IH.
case E : (a z) => /=.
  rewrite inE eq_sym.
  by case: eqP => //= Hx; case: eqP.
move=> xIl Hi; apply: IH => //.
by case: eqP xIl Hi => [<-| _]; [rewrite mem_filter E | case: eqP].
Qed.

Lemma leq_index_nth x l i : index (nth x l i) l  <= i.
Proof.
elim: l i => //= y l IH [|i /=]; first by rewrite eqxx.
by case: eqP => // _; apply: IH.
Qed.

Lemma index_find x l a :  has a l -> index (nth x l (find a l)) l = find a l.
Proof.
move=> Hal.
apply/eqP; rewrite eqn_leq leq_index_nth.
case: leqP => // /(before_find x).
by rewrite nth_index ?nth_find // mem_nth // -has_find.
Qed.

Lemma before_can x  y s l : 
  x \in l -> y \in l -> x =[s]= y -> before l C[x]_(s, l) y.
Proof.
move=> Hx Hy; rewrite requiv_sym => Hr.
have F : has (requiv s x) l.
  by apply/hasP; exists y => //; rewrite requiv_sym.
rewrite /before /rcan index_find //.
case: leqP => // /(before_find x).
by rewrite nth_index // requiv_sym Hr.
Qed.

Lemma before_canW x s1 s2 l : 
 x \in l -> {subset s1 <= s2} -> before l C[x]_(s1, l) C[x]_(s2, l).
Proof.
move=> xIl Hs.
have Hs1 : has (requiv s1 x) l.
  by apply/hasP; exists x => //; exact: requiv_ref.
have Hs2 : has (requiv s2 x) l.
  by apply/hasP; exists x => //; exact: requiv_ref.
rewrite /before /rcan !index_find //.
by apply: sub_find => z; apply: lrequiv_subset.
Qed.

(* well formed list : rconnected elements are inside and
                      canonical elements are on top *)
Definition rwf (p : {set T} * seq T) := 
  [disjoint p.1 & p.2] /\
 forall x y , 
   x \in p.2 -> x -[p.1]-> y -> y \in p.2 /\ before p.2 C[x]_p y.

Local Notation "W_[ s ] l" := (rwf (s, l)) (at level 10).
Local Notation "W_[] l " := (rwf (set0,l)) (at level 10).

Lemma rwf_nil s : W_[s] [::].
Proof. by split => //=; apply/pred0P=> i /=; rewrite andbF. Qed.

(* Removing the equivalent elements of the top preserve well-formedness *)
Lemma rwf_inv x s l : 
  W_[s] (x :: l) -> W_[s] [seq y <- x :: l | ~~ x =[s]= y].
Proof.
move=> [Ds1xs2 HR]; split => [|y z].
  apply: disjoint_transr Ds1xs2.
  by apply/subsetP/mem_subseq/filter_subseq.
rewrite !mem_filter => /andP[NRy yIxl] Cyz.
have uIl : y \in l.
  by move: yIxl NRy; rewrite inE => /orP[/eqP<-|//]; rewrite requiv_ref.
have->: C[y]_(s, [seq i <- x :: l | ~~ x =[s]= i]) = C[y]_(s, x :: l).
  elim: (x :: l) => //= t l1 IH.
  case : (boolP (requiv _ _ _)) => Ext /=.
    rewrite IH /rcan /=.
    case : (boolP (requiv _ _ _)) => Eyt //=.
    by case/negP: NRy; apply: requiv_trans Ext _; rewrite requiv_sym.
  by rewrite /rcan /=; case : (boolP (requiv _ _ _)).
have [zIxl Rz] := HR y z yIxl Cyz.
have F : ~~ x =[s]= z.
  apply: contra NRy => NRz.
  have/HR[//|_] : y -[s]-> x.
    by apply: rconnect_trans Cyz _; case/andP: NRz.
  rewrite /before index_head /=.
  by case: eqP => //-> _; apply: requiv_can.
split; first by rewrite F.
apply: before_filter => //.
rewrite mem_filter mem_rcan // ?andbT.
apply: contra NRy => NRc.
by apply: requiv_trans NRc (requiv_can _ _).
Qed.

(* Computing the connected elements for the reversed graph gives
   the equivalent class of the top element of an well_formed list *)
Lemma rwf_equiv x y s l : 
  W_[s] (x :: l) -> x =[s]= y = (y \in (x :: l)) && y -[s]-> x.
Proof.
move=> [_ HR].
apply/idP/idP=> [/andP[Cxy Cyx]|/andP[yIxl Cyx]].
  case: (HR x y) => // [|->]; first by rewrite inE eqxx.
  by rewrite Cyx.
have F := requiv_can _ yIxl.
case: (HR y x) => // _.
by rewrite /before /= eqxx; case: eqP => //->.
Qed.

(* Computing well_formed list by accumulation *)
Lemma rwf_cat s1 l1 l2 : W_[s1] l1 -> W_[s1 :|: [set x in l1]] l2 -> W_[s1] (l2 ++ l1).
Proof.
move=> [Ds1l1 Rl1] [Ds1s2l2 Rl2]; split => [|x y].
  rewrite disjoint_sym disjoint_cat /= ![[disjoint _ & s1]]disjoint_sym Ds1l1 andbT.
  apply: disjoint_trans Ds1s2l2.
  by apply/subsetP=> i; rewrite !inE => ->.
have [xIl2 _ Hc|xNIl2] := boolP (x \in l2); last first.
  rewrite mem_cat (negPf xNIl2) /= => xIl1 Cxy.
  have /Rl1 - /(_ _ Cxy)[yIl1 Bxy] := xIl1.
  split; first by rewrite mem_cat yIl1 orbT.
  rewrite /before [index y _]index_cat.
  have [yIl2|yNil2] := boolP (y \in l2).
    have/pred0P/(_ y)/= := Ds1s2l2; rewrite yIl2 .
    by rewrite !inE yIl1 orbC.
  rewrite index_cat; have [rIl2| rNIl2] := boolP (_ \in l2).
    by apply: leq_trans (index_size _ _) (leq_addr _ _).
  rewrite leq_add2l.
  move: rNIl2; rewrite /rcan find_cat.
  have [HH|HH] := boolP (has _ _).
    by rewrite nth_cat -has_find HH mem_nth // -has_find.
  rewrite nth_cat ltnNge leq_addr /= => _.
  by rewrite addnC addnK.
have [Hn|] := boolP [disjoint [set z | x -[s1]-> z & z -[s1]-> y] & [set x in l1]].
  have := rconnect_setU Hn Hc; rewrite setUC.
  move=> /(Rl2 _ _ xIl2) [yIl2 HB]; split => //.
    by rewrite mem_cat yIl2.
  rewrite /before [index y _]index_cat yIl2.
  apply: leq_trans HB.
  rewrite rcan_cat // index_cat mem_rcan //.
  apply: before_canW => // i.
  by rewrite !inE => ->.
move=> /pred0Pn[z].
rewrite !inE => /andP[/andP[Cxz Czy]] /Rl1 /= /(_ _ Czy) [yIl1 Hyr].
split; first by rewrite mem_cat yIl1 orbT.
rewrite /before [index y _]index_cat.
have [yIl2|_] := boolP (_ \in _).
  have/pred0P/(_ y)/= := Ds1s2l2.
  by rewrite !inE yIl1 yIl2 orbC.
rewrite index_cat.
have [_|/negP[]] := boolP (_ \in _).
  by apply: leq_trans (index_size _ _) (leq_addr _ _).
rewrite /rcan; elim: (l2) xIl2 => //= a l IH.
rewrite inE => /orP[/eqP->|/IH]; first by rewrite requiv_ref inE eqxx.
case: requiv => //=; first by rewrite inE eqxx.
by rewrite inE orbC => ->.
Qed.

Lemma rwf_setU1_l x s l : x \notin l ->  W_[s] l -> W_[x |: s] l.
Proof.
move=> xNIl [Hd H]; split => [|t z tIl Ryz].
  by rewrite disjoint_setU1 xNIl.
case: (H t z) => // [|zIl Btz].
  by apply: rconnect_subset Ryz => i; rewrite inE orbC => ->.
split => //; suff->: C[t]_(x |: s, l) = C[t]_(s, l) by [].
congr nth; apply: eq_in_find => y yIl.
have [xIs|xNIs] := boolP (x \in s).
  congr (_ =[_]= _); apply/setP=> i.
  by rewrite !inE /=; case: eqP => // ->; rewrite xIs.
apply/idP/idP => /=. 
  by apply: lrequiv_subset => u; rewrite inE orbC => ->.
by case/andP=> Cty Cyt; apply/andP; split;
   apply: rconnect_setU1l => //; apply: contra xNIl => /H[].
Qed.

(* Computing well_formed list by accumulation *)
Lemma rwf_cons_r x s l :
 (forall y, y \in l -> x -[s]-> y) ->
 (forall y, r x y -> y \notin x |: s -> y \in l) ->
  x \notin s -> W_[x |: s] l ->  W_[s] (x :: l).
Proof.
move=> Cx CyIl xNIs [Dsl Hl]; split => [|y z].
   by move: Dsl; rewrite disjoint_setU1 /= disjoint_consr xNIs => /andP[].
have F t : t != x -> x -[x |: s]-> t -> t \in l.
  move=> tDx /rconnectP[[_ [/eqP]|v p]] /=; first by rewrite (negPf tDx).
  case/andP=> Rxv Prvp [Lvp Dvpxs].
  have: v \in l.
    apply: CyIl => //; rewrite inE.
    have/pred0P/(_ v)/= := Dvpxs.
    by rewrite /= !inE eqxx /= orbC => -> /=.
  case/(Hl v t) => //; apply/rconnectP; exists p => //; split => //.
  by apply: disjoint_trans Dvpxs; apply/subsetP => i; rewrite inE orbC => ->.
rewrite inE.
have [/eqP-> /= _ Cxz|yDx /= yIl Cyz] := boolP (y == x).
  split; last by rewrite /before /= rcan_cons requiv_ref eqxx.
  have [/eqP<-|zDx] := boolP (z == x); first by rewrite !inE eqxx.
  by rewrite inE (F z) ?orbT // 1?eq_sym // rconnect_id_setU1.
have [Cyz'|NCyz'] := boolP (y -[x |: s]-> z).
  have [zIxs Byz] := Hl _ _ yIl Cyz'.
  split; first by rewrite inE zIxs orbT.
  have [/eqP xEz|xDz] := boolP (x == z).
    rewrite rcan_cons.
    suff->: y =[s]= x by rewrite /before /= eqxx.
    rewrite /requiv {1}xEz Cyz /=.
    by apply: Cx.
  rewrite rcan_cons; case: requiv; first by rewrite /before /= eqxx.
  rewrite /before /= (negPf xDz); case: eqP => //= _.
  rewrite ltnS.
  apply: leq_trans Byz => /=.
  by apply: before_canW => // i; rewrite inE orbC => ->.
have [Cyx|NCyx] := boolP (y -[s]-> x); last first.
  by case/negP: NCyz';  apply: rconnect_setU1l.
have [Cxz|NCxz] := boolP (x -[s]-> z); last first.
  by case/negP: NCyz'; apply: rconnect_setU1r.
split.
  rewrite inE.
  have [//|zDx/=] := boolP (z == x).
  by apply: F => //; rewrite rconnect_id_setU1.
rewrite /before rcan_cons.
suff->: y =[s]= x; first by rewrite /before /= eqxx.
rewrite /requiv Cyx /=.
by apply: rconnect_subset (Cx _ yIl).
Qed.

End Rconnect.

Variable r : rel T.

Local Notation "x -[ l ]-> y" := (rconnect r l x y) 
  (at level 10, format "x  -[ l ]->  y").
Local Notation "x -[]-> y" := (rconnect r [::] x y) 
  (at level 10, format "x  -[]->  y").
Local Notation "x =[ l ]= y" := (requiv r l x y) 
  (at level 10, format "x  =[ l ]=  y").
Local Notation "x =[]= y" := (requiv r [::] x y) 
  (at level 10, format "x  =[]=  y").
Local Notation "W_[ l1 ] l2 " := (rwf r (l1, l2)) (at level 10).
Local Notation "W_[] l" := (rwf r (set0, l)) (at level 10).

Section Pdfs.

Variable g : T -> seq T.

Fixpoint rpdfs m (p : {set T} * seq T) x :=
  if x \in p.1  then p else 
  if m is m1.+1 then 
     let p1 := foldl (rpdfs m1) (x |: p.1, p.2) (g x) in (p1.1, x :: p1.2)
  else p.

Definition pdfs := rpdfs #|T|.

End Pdfs.

Lemma pdfs_correct (p : {set T} * seq T) x :
  let (s, l) := p in 
  uniq l /\  {subset l <= s} ->
  let p1 := pdfs (rgraph r) p x in
  let (s1, l1) := p1 in
  if x \in s then p1 = p else
       [/\ #|s| <= #|s1| & uniq l1]
    /\
       exists l2 : seq T,
       [/\ x \in l2, s1 = s :|: [set y in l2], l1 = l2 ++ l, W_[s] l2 &
           forall y, y \in l2 -> x -[s]-> y].
Proof.
rewrite /pdfs.
have: #|T| <= #|p.1| + #|T| by exact: leq_addl.
elim: {-1}#|T| x p => /= [x [s l]|n IH x [s l]]/=.
  rewrite if_same addn0 => Hl [HUl HS].
  have [//|/negP[]] := boolP (x \in s).
  have/subset_cardP->: s \subset T by apply/subsetP.
    by rewrite inE.
  apply/eqP; rewrite eqn_leq Hl andbT.
  by apply/subset_leq_card/subsetP=>i.
have [xIs Hl [HUl HS] //|xNIs Hl [HUl HS]] := boolP (x \in s).
set p := (_, l); set F := rpdfs _ _; set L := rgraph _ _.
have: 
     [/\ #|s| < #|p.1| & uniq p.2]
  /\
     exists l2,
      [/\  x \in p.1, p.1 = (x |: s) :|: [set z in l2], p.2 = l2 ++ l, W_[x |: s] l2 &
          forall y, y \in l2 -> x -[x |: s]-> y].
  split; [split => // | exists [::]; split => //=].
  - by rewrite /= cardsU1 xNIs.  
  - by rewrite !inE eqxx.
  - by rewrite setU0.
  by exact: rwf_nil.
have: forall y, r x y -> (y \in p.1) || (y \in L).
  by move=> y; rewrite [_ \in rgraph _ _]rgraphK orbC => ->.
have: forall y, (y \in L) -> r x y.
  by move=> y; rewrite [_ \in rgraph _ _]rgraphK.
rewrite {}/p.
elim: L (_, _) => /=
    [[s1 l1] /= _ yIp [[sSs1 Ul1] [l2 [xIs1 s1E l1E Rwl2 Cxy]]]|
    y l' IH1 [s1 l1] /= Rx yIp [[sSs1 Ul1] [l2 [xIs1 s1E l1E Rwl2 Cxy]]]].
  split; [split=> // |exists (x :: l2); split] => // [||||||y].
  - by rewrite subset_leqif_cards // s1E !subsetU // subxx_hint orbT.
  - rewrite Ul1 andbT; apply: contra xNIs.
     have[Dl2 _] := Rwl2.
     have /pred0P/(_ x)/= := Dl2.
     rewrite !inE eqxx l1E mem_cat /= => ->/=.
     by apply: HS.
  - by rewrite inE eqxx.
  - by apply/setP => z; rewrite s1E !inE; case: eqP; rewrite ?orbT.
  - by rewrite l1E.
  - apply: rwf_cons_r => // [y yInl2|y /yIp].
      by rewrite -rconnect_id_setU1 Cxy.
    by rewrite orbF s1E 2!inE => /orP[Hv /negP[]|->//].
  rewrite inE => /orP[/eqP->|yIl2].
    by apply: rconnect_ref.
  by apply: rconnect_subset (Cxy _ yIl2) => i; rewrite inE orbC => ->.
have F1 : #|T| <= #|s1| + n.
  by rewrite -ltnS -addnS (leq_ltn_trans Hl) // ltn_add2r.
have F2 : {subset l1 <= s1}.
  by move=> i; rewrite l1E s1E !inE mem_cat => /orP[->//|/HS->]; rewrite !orbT.
have := IH y (s1, l1) F1 (conj Ul1 F2).
rewrite /F /=; case: rpdfs => s3 l3 /= Hv.
apply: IH1 => [z zIl|z Rxz /=|]; first by apply: Rx; rewrite inE zIl orbT.
- case: (boolP (y \in s1)) Hv =>
       [yIs1 [-> _]|yNIs1 [[Ss1s3 Ul3] [l4 [yIl4 s3E l3E Rwl4 Cyz]]]].
    case: (yIp _ Rxz) => /orP[->//|].
    by rewrite inE => /orP[/eqP->|->];[rewrite yIs1|rewrite orbT].
  rewrite s3E !inE.
  case: (yIp _ Rxz) => /orP[->//|].
  rewrite inE => /orP[/eqP->|->]; last by rewrite orbT.
  by rewrite yIl4 orbT.
case: (boolP (y \in s1)) Hv =>
      [yIs1 [-> ->]|yNIs1 [[Ss1s3 Ul3] [l4 [yIl4 s3E l3E Rwl4 Cyz]]]].
  by split=> //; exists l2; split.
split; [split=> //= | exists (l4 ++ l2); split => //= [||||z]]. 
- by apply: leq_trans Ss1s3.
- by rewrite s3E s1E !inE eqxx.
- apply/setP => i; rewrite s3E s1E !inE mem_cat -!orbA.
  by rewrite [_ || (_ \in l2)]orbC.
- by rewrite l3E l1E catA.
- by apply: rwf_cat => //; rewrite -s1E.
rewrite mem_cat => /orP[] zIl4; last by apply: Cxy.
apply: rconnect_trans (_: y -[_]-> z).
  apply: rconnect1; last by apply: Rx; rewrite inE eqxx.
  by apply: contra yNIs1; rewrite s1E !inE orbC => ->.
apply: rconnect_subset (Cyz _ zIl4) => i.
by rewrite s1E !inE orbC => ->.
Qed.

Lemma pdfs_connect s x : 
  x \notin s ->
  let (s1, l1) := pdfs (rgraph r) (s, [::]) x in
  [/\ uniq l1, s1 = s :|: [set x in l1], [disjoint s & l1] & 
      forall y, y \in l1 = x -[s]-> y].
Proof.
move=> xNIs.
set p := (_, _).
have UN : [/\ uniq p.2 & {subset p.2 <= p.1}] by [].
case: pdfs (pdfs_correct (_, _) x UN) => s1 l1.
rewrite (negPf xNIs) => /=[[[_ Ul1] [l2 [xIl2 s1E l1E WH Cy]]]].
split => // [||y].
- by apply/setP=> i; rewrite s1E l1E !inE cats0.
- rewrite disjoint_sym.
  apply/pred0P=> z /=; rewrite l1E cats0 andbC.
  by have [/pred0P/(_ z)]/= := WH.
apply/idP/idP => [|H].
  by rewrite l1E cats0; exact: Cy.
rewrite l1E cats0.
by have [_ /(_ x y xIl2 H)[]] := WH.
Qed.

(* Building the stack of all nodes *)
Definition stack :=
  (foldl (pdfs (rgraph r)) (set0, [::]) (enum T)).2.

(* The stack is well-formed and contains all the nodes *)
Lemma stack_correct : W_[] stack /\ forall x, x \in stack.
Proof.
suff: [/\
        {subset (set0 : {set T}, [::]).2  <= stack},
        W_[] stack &
         forall x : T, x \in (enum T) ->  x \in stack].
  by case=> H1 H2 H3; split => // x; rewrite H3 // mem_enum.
rewrite /stack; set F := foldl _; set p := (_, _).
have : W_[] p.2 by apply: rwf_nil.
have: p.1 = [set x in p.2] by [].
have: uniq p.2 by [].
elim: (enum T) p => /= [|y l IH [s1 l1] HUl1 /= Hi Rw].
  by split.
have HS : {subset l1 <= s1} by move=> i; rewrite Hi inE.
have :=  pdfs_correct (_, _) y (conj HUl1 HS).
have [yIs1|yNIs1] := boolP (y \in s1).
  case: pdfs => s2 l2 [-> ->].
  have /= [Sl2 HR xI] := IH (s1,l1) HUl1 Hi Rw.
  split => // x.
  rewrite inE => /orP[/eqP->|xIl].
    by apply: Sl2; move: yIs1; rewrite Hi inE.
  by apply: xI.
case: pdfs => s2 l2 /= [[Ss1s2 Ul2] [l3 [yIl3 s2E l2E RWl3 Cyz]]].
case: (IH (s2, l2)) => //= [|| Sl2F RwF FI]. 
- by apply/setP=> i; rewrite s2E Hi l2E !inE mem_cat orbC.
  rewrite l2E; apply: (rwf_cat Rw).
- by rewrite set0U -Hi.
split=> // [i iIl1|x]; first by rewrite Sl2F // l2E mem_cat iIl1 orbT.
rewrite inE => /orP[/eqP->|//]; last exact: FI.
by apply: Sl2F; rewrite l2E mem_cat yIl3.
Qed.

Lemma rconnect_rev l s1 s2 x y : 
     {subset s1 <= s2} -> [disjoint s2 & x :: l] ->
     (forall z, z \in s2 :|: [set t in x :: l]) ->
     W_[s1] (x :: l) ->
     ((y \in x :: l) && y -[s1]-> x) = (rconnect [rel x y | r y x] s2 x y).
Proof.
move=> HS HD HA HW.
have [yIxl|yNIxl]/= := boolP (y \in _); last first.
  apply/sym_equal/idP/negP; apply: contra yNIxl.
  case/rconnectP=> p.
  have: x \in x :: l by rewrite inE eqxx.
  elim: p {1 3 4}x => /= [x1 x1Ixl _ [->]//|
                          z p /= IH x1 x1Ixl /andP[Rzx Pz] [Lz Dz]].
  apply: (@IH z) => //.
  - have/pred0P/(_ z)/= := Dz; have := HA z; have/pred0P/(_ z)/= := HD.
    by rewrite !inE eqxx; case: (_ \in _).
  - split => //=; apply: disjoint_trans Dz; apply/subsetP=> i.
    by rewrite inE orbC => ->.
apply/idP/idP.
  case/rconnectP=> p.
  elim: p y yIxl => /= [y yIxl _ [-> _]|
                         z p /= IH y yIxl /andP[Rzx Pz] [Lz Dz]].
    by apply: rconnect_ref.
  apply: rconnect_trans (_ : rconnect _ _ z y); last first.
    apply: rconnect1 => //=.
    by have /pred0P/(_ y)/= := HD; rewrite yIxl andbT => ->.
  apply: IH => //.
    have [_ /(_ y z yIxl)] := HW; case=> //.
    apply: rconnect1 => //.
    by have /pred0P/(_ z)/= := Dz; rewrite inE eqxx => /=->.
  split => //; apply: disjoint_trans Dz; apply/subsetP=> i.
  by rewrite inE orbC => ->.
case/rconnectP=> p.
have xIxl : x \in x :: l by rewrite inE eqxx.
elim: p {1 3 4 5}x xIxl => /= [x1 x1Ixl1 _ [-> _]|
                                z p /= IH x1 x1Ixl /andP[Rzx Pz] [Lz Dz]].
  by apply: rconnect_ref.
apply: rconnect_trans (_ : z -[s1]-> x1); last first.
  apply: rconnect1 => //=.
  have /pred0P/(_ x1)/= := HD; rewrite x1Ixl.
  by case: (boolP (x1 \in s1)) => // /HS->.
apply: IH => //.
  have := HA z; rewrite !inE.
  have /pred0P/(_ z)/= := Dz.
  by rewrite inE eqxx => /=->.
split => //; apply: disjoint_trans Dz; apply/subsetP=> i.
by rewrite inE orbC => ->.
Qed.

End Stack.

Variable r : rel T.

Definition kosaraju :=
  let f := pdfs (rgraph [rel x y | r y x]) in 
  (foldl  (fun (p : {set T} * seq (seq T)) x => if x \in p.1 then p else 
                      let p1 := f (p.1, [::]) x in  (p1.1, p1.2 :: p.2))
          (set0, [::]) (stack r)).2.

Lemma kosaraju_correct :
    let l := flatten kosaraju in 
 [/\ uniq l, forall i, i \in l &
     forall c : seq T, c \in kosaraju -> 
        exists x, forall y, (y \in c) = (connect r x y && connect r y x)]. 
Proof.
rewrite /kosaraju.
set f := pdfs (rgraph [rel x y | r y x]).
set g := fun p x => if _ then _ else _.
set p := (_, _).
have: uniq (flatten p.2) by [].
have: forall c, c \in (flatten p.2) ++ (stack r).
  by move=>c; case: (stack_correct r) => _ /(_ c).
have: forall c, c \in p.2 -> exists x, c =i (requiv r set0 x) by [].
have: p.1 =i flatten p.2 by move=> i; rewrite !inE in_nil.
have: rwf r (set0, [seq i <- stack r | i \notin p.1]).
  have->: [seq i <- stack r | i \notin p.1] = stack r.
    by apply/all_filterP/allP=> y; rewrite inE.
  by case: (stack_correct r).
elim: stack p => [[s l]/= HR HI HE HFI HUF|].
   split=> // [i|i /HE [x Hx]].
     by have := HFI i; rewrite cats0.
  by exists x => y; rewrite  Hx -requiv_set0.
move=> x l IH [s1 l1] HR HI HE HFI HUF.
rewrite /g /f /=.
have [xIs1|xNIs1] := boolP (x \in s1).
  apply: IH => //= [|i]; first by move: HR; rewrite /= xIs1.
  have:= HFI i; rewrite !mem_cat inE /=.
  by case: eqP => //->; rewrite -HI xIs1.
have := (@pdfs_connect ([rel x y | r y x]) s1 x xNIs1).
case: pdfs => s2 l2 /= [Ul2 s2E Dl2 Cxy].
move: HR; rewrite /= xNIs1; set L := [seq _ <- _ | _] => HR.
have l2R : l2 =i (requiv r set0 x).
  move=> y.
  rewrite Cxy -(@rconnect_rev r L set0) //.
  - by rewrite -(@rwf_equiv r x y set0 L).
  - by move=> i; rewrite inE.
  - apply/pred0P=> z /=; rewrite !(inE, mem_filter).
  - by case: eqP => [->|]; 
      [rewrite (negPf xNIs1) |case: (_ \in _)].
  move=> z.
  have := HFI z.
  rewrite !mem_cat -HI !inE mem_filter /=.
  by case: (z \in s1).
apply: IH => [|i|i|i|] //=.
- suff->: [seq i <- l | i \notin s2] =
          [seq i <- x :: L | ~~ requiv r set0 x i].
    by apply: rwf_inv.
  rewrite /= requiv_ref /=.
  rewrite -filter_predI.
  apply: eq_filter => y /=.
  by rewrite s2E !inE negb_or l2R andbC.
- by rewrite s2E !mem_cat !inE HI orbC.
- by rewrite inE => /orP[/eqP->|//]; [exists x | apply: HE].
- have:= HFI i.
  rewrite /= !mem_cat !inE => /or3P[->|/eqP->|->].
  - by rewrite orbT.
  - by rewrite Cxy rconnect_ref.
  by rewrite !orbT.
rewrite cat_uniq Ul2 HUF /= andbT.
apply/hasPn => i /=.
have/pred0P/(_ i)/= := Dl2.
by rewrite -HI /=; do 2 case: (_ \in _).
Qed.

End Kosaraju.

Print rpdfs.
Print pdfs.
Print stack.
Print kosaraju.
Print dfs.