chip.tarjan_acyclic

From mathcomp
Require Import all_ssreflect.

From chip
Require Import connect acyclic tarjan.

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

(* TODO: prove everything for foldl version *)

Section SeqSet.

Variable V : finType.

Definition enums (s : seq {set V})
 foldr (fun ( : {set V}) cons (enum )) [::] s.

Definition enums' (s : seq {set V})
 foldl (fun l ( : {set V}) enum l) [::] s.

Lemma enumsP (s : seq {set V}) l :
  reflect
    ( scc, scc \in s & enum scc = l)
    (l \in enums s).
Proof.
apply/(iffP idP).
- rewrite /enums.
  move Hsc.
  suff Hsuff: scc, scc \in enum s & enum scc = l.
    move: Hsuff [scc Hsc'] He.
    move: Hsc'.
    rewrite mem_enum Hsc'.
    by exists scc.
  move: Hsc.
  elim: s //=.
  move IH.
  rewrite in_cons.
  move/orP.
  case.
  * move/eqP .
    exists //=.
    rewrite mem_enum.
    rewrite in_cons.
    apply/orP.
    by left.
  * move/IH [scc Hs] He.
    exists scc //=.
    rewrite mem_enum in_cons.
    apply/orP.
    right.
    by rewrite -mem_enum.
- move [scc Hscc] He.
  move: He Hscc .
  rewrite /enums /= Hsc.
  have Hsc': scc \in enum s by rewrite mem_enum.
  move: Hsc'.
  elim: s {Hsc}; first by rewrite mem_enum.
  move IH.
  rewrite mem_enum in_cons.
  move/orP.
  case.
  * move/eqP .
    rewrite inE.
    by apply/orP; left.
  * rewrite -mem_enum.
    move/IH Hl.
    by apply/orP; right.
Qed.


Lemma enums_enums'_in s :
  enums s =i enums' s.
Proof.
rewrite /enums /enums'.
have {2}: s = rev (rev s) by rewrite revK.
rewrite foldl_rev .
apply/enumsP.
case: ifP.
- move/enumsP [scc Hsc] He.
  exists scc //.
  move: Hsc.
  by rewrite mem_rev.
- move/enumsP.
  move He.
  case x Hx Hex.
  case: He.
  exists x //.
  by rewrite mem_rev.
Qed.


Lemma enums'P (s : seq {set V}) l :
  reflect
    ( scc, scc \in s & enum scc = l)
    (l \in enums' s).
Proof.
apply/(iffP idP).
- rewrite -enums_enums'_in.
  by move/enumsP.
- move/enumsP.
  by rewrite -enums_enums'_in.
Qed.


Lemma uniq_enums l :
  uniq l
  uniq (enums l).
Proof.
elim: l //=.
move s l IH.
move/andP [Hs Hl].
apply/andP.
split; last by apply: IH.
apply/negP Hen.
move/negP: Hs.
case.
move: Hen.
elim: l {IH Hl} //=.
move l IH.
rewrite in_cons.
move/orP.
case.
- move/eqP Hs.
  suff Hsuff: s = .
    rewrite in_cons.
    apply/orP; left.
    by apply/eqP.
  apply/setP.
  move x.
  by rewrite -mem_enum Hs mem_enum.
- move He.
  rewrite in_cons.
  apply/orP.
  right.
  exact: IH.
Qed.


Lemma in_uniq_enums l :
  uniq l
   , \in (enums l) uniq .
Proof.
elim: l //=.
move a l IH.
move/andP [Ha Hl] .
rewrite in_cons.
move/orP.
case //.
- move/eqP .
  exact: enum_uniq.
- move Hla.
  exact: IH.
Qed.


Lemma uniq_flatten : l,
 ( a, a \in l uniq a)
 uniq l
 {in l &, A B : seq V, A != B [disjoint A & B]}
 uniq (flatten l).
Proof.
elim //=.
move a l IH Ha.
move/andP [Hal Hul] Hd.
rewrite cat_uniq.
apply/and3P.
split.
- apply: Ha.
  by rewrite in_cons; apply/orP; left.
- apply/negP Hm.
  move/hasP: Hm [x Hx] /= Ha'.
  move/flattenP: Hx.
  move [y Hy] Hxy.
  have Hla: a \in a l by rewrite in_cons; apply/orP; left.
  have Hly: y \in a l by rewrite in_cons; apply/orP; right.
  have Hn: a != y.
    apply/negP Hn.
    move/eqP: Hn Hn.
    move: Hn Hal .
    move/negP.
    by case.
  have Hd' Hd a y Hla Hly Hn.
  move: Hd'.
  rewrite disjoint_subset.
  move/subsetP Hd'.
  move/negP: (Hd' _ Ha').
  by case.
- apply: IH //.
  move Hl.
  apply: Ha.
  by rewrite in_cons; apply/orP; right.
- move a' Ha' Hneq.
  apply: Hd //.
  * by rewrite in_cons; apply/orP; right.
  * by rewrite in_cons; apply/orP; right.
Qed.


Variable sc : {set {set V}}.

Hypothesis all_in_cover : v : V, v \in cover sc.

Lemma cover_all_in :
   v : V, v \in flatten (enums (enum sc)).
Proof.
move v.
apply/flattenP.
move/bigcupP: (all_in_cover v).
move [s' Hv] Hs.
exists (enum s'); last by rewrite mem_enum.
apply/enumsP.
exists s' //.
by rewrite mem_enum.
Qed.


Hypothesis trivIset_sc : trivIset sc.

Lemma in_enums_disjoint :
   l l', l \in enums (enum sc) l' \in enums (enum sc)
    l != l' [disjoint l & l'].
Proof.
move/trivIsetP: trivIset_sc Ht.
move l l'.
move/enumsP [s Hs] He.
move/enumsP [s' Hs'] He' Hl.
move: Hs.
rewrite mem_enum.
move/(Ht s s') Hts.
move: Hs'.
rewrite mem_enum.
move/Hts.
have Hs: s != s'.
  apply/negP Hs.
  move/eqP: Hs Hs.
  move/negP: Hl.
  case.
  rewrite -He -He'.
  by rewrite Hs.
move Hd.
move/Hd: Hs.
rewrite -He -He' /=.
rewrite 2!disjoint_subset.
move/subsetP Hs.
apply/subsetP.
move x.
rewrite mem_enum.
move/Hs.
rewrite /predC /=.
rewrite 2!inE.
by rewrite mem_enum.
Qed.


End SeqSet.

Section TarjanSeq.

Variable V : finType.

Variable successors : V seq V.

Definition tarjans enums (enum (tarjan successors)).

Definition tarjans' enums' (enum (tarjan successors)).

Lemma tarjansP sccl :
  reflect
    ( scc, scc \in tarjan successors & enum scc = sccl)
    (sccl \in tarjans).
Proof.
apply/(iffP idP).
- move/enumsP [scc Hsc] He.
  exists scc //.
  by rewrite -mem_enum.
- move [scc Hsc] He.
  apply/enumsP.
  exists scc //.
  by rewrite mem_enum.
Qed.


End TarjanSeq.

Section TarjanAcyclic.

Variable V : finType.
Variable g : rel V.

Lemma trivIset_tarjan :
  trivIset (tarjan (rgraph g)).
Proof.
rewrite tarjan_correct.
exact: trivIset_gsccs.
Qed.


Lemma class_diconnected_tarjan :
   c, c \in tarjan (rgraph g)
   x, y, (y \in c) = diconnect g x y.
Proof.
move c.
rewrite tarjan_correct.
rewrite /gsccs /=.
rewrite /equivalence_partition /=.
move/imsetP [x Hx] Hc.
exists x.
move y.
rewrite Hc inE.
rewrite andb_idl //.
set g' : rel V grel (rgraph g).
rewrite -(@eq_diconnect _ g') //.
move .
rewrite /g' /=.
by rewrite mem_enum.
Qed.


Lemma class_diconnected_tarjans :
   c, c \in tarjans (rgraph g)
   x, y, (y \in c) = diconnect g x y.
Proof.
move c.
move/tarjansP [scc Hsc].
move .
move/class_diconnected_tarjan: Hsc.
move [x Hy].
exists x.
move y.
by rewrite mem_enum.
Qed.


Lemma cover_tarjan : cover (tarjan (rgraph g)) = [set: V].
Proof.
rewrite tarjan_correct.
by rewrite cover_gsccs.
Qed.


Lemma all_in_cover_tarjan : v : V, v \in cover (tarjan (rgraph g)).
Proof.
by move v; rewrite tarjan_correct cover_gsccs.
Qed.


Lemma all_in_flatten_tarjans : v : V, v \in flatten (tarjans (rgraph g)).
Proof.
apply: cover_all_in.
exact: all_in_cover_tarjan.
Qed.


Lemma enum_tarjan_non_empty : \notin enum (tarjan (rgraph g)).
Proof.
have Hp gsccs_partition (rgraph g).
rewrite tarjan_correct.
rewrite /partition in Hp.
move/and3P: Hp.
case Hc Ht Hs.
by rewrite mem_enum.
Qed.


Lemma uniq_in_tarjans :
a, a \in tarjans (rgraph g) uniq a.
Proof.
apply: in_uniq_enums.
exact: enum_uniq.
Qed.


Lemma uniq_flatten_tarjans : uniq (flatten (tarjans (rgraph g))).
Proof.
apply: uniq_flatten.
- move a Ht.
  exact: uniq_in_tarjans.
- apply: uniq_enums.
  exact: enum_uniq.
- apply: in_enums_disjoint.
  exact: trivIset_tarjan.
Qed.


Definition tarjans_acyclic
 sccs_acyclic (fun g tarjans (rgraph g)) g.

Lemma tarjans_acyclicP :
  reflect (acyclic g) tarjans_acyclic.
Proof.
apply/sccs_acyclicP.
- exact: uniq_flatten_tarjans.
- exact: all_in_flatten_tarjans.
- exact: class_diconnected_tarjans.
Qed.


End TarjanAcyclic.