chip.acyclic

From mathcomp
Require Import all_ssreflect.

From chip
Require Import connect.

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

Section Cycles.

Variable V : finType.
Variable g : rel V.

Lemma self_loop_cycle : forall x, g x x -> cycle g [:: x].
Proof.
move => x H_in.
rewrite /cycle /=.
by apply/andP.
Qed.

Lemma diconnect_path_cycle :
  forall x y, x != y -> diconnect g x y -> exists p, cycle g (x :: p).
Proof.
move => x y H_neq /andP /= [H_x H_y].
move/connectP: H_x; case => px H_px H_pl.
move/connectP: H_y; case => py H_py H_pl'.
case: py H_py H_pl' => /=; first by move => H_py H_eq; rewrite H_eq in H_neq; move/negP: H_neq.
move => y' py' /andP [H_in H_py'] H_x.
exists (px ++ belast y' py').
rewrite rcons_cat /= {2}H_x -lastI cat_path -H_pl /=.
apply/andP; split => //.
by apply/andP.
Qed.

Lemma cycle_path_diconnect :
  forall x p, cycle g (x :: p) ->
  x \in g x \/ (exists y, diconnect g x y /\ x != y).
Proof.
move => x p.
move: x.
rewrite /=.
case: p => //=.
- move => x /andP [H_p ?].
  by left.
- move => y p x.
  case H_eq: (x == y).
  * move/eqP: H_eq => H_eq.
    rewrite H_eq.
    move/andP => [H_in H_p].
    by left.
  * move/negP: H_eq => H_eq.
    move/andP => [H_in H_p].
    right.
    exists y; split; last by apply/negP.
    apply/andP.
    split; first by apply/connectP; exists [:: y]; first by rewrite /=; apply/andP.
    apply/connectP.
    exists (rcons p x); first by [].
    by rewrite last_rcons.
Qed.

End Cycles.

Section Acyclic.

Variable V : finType.
Variable g : rel V.

Definition acyclic := forall x p, path g x p -> ~~ cycle g (x :: p).

Hypothesis g_acyclic: acyclic.

Lemma acyclic_no_self_loop : forall x, ~~ g x x.
Proof.
move => x.
apply/negP.
case => Hg.
move/g_acyclic: (self_loop_cycle Hg).
move/negP; case => /=.
by apply/and3P; split.
Qed.

Lemma acyclic_diconnect : forall x y, diconnect g x y -> x = y.
Proof.
move => x y Hd.
case Hx: (x == y); first by apply/eqP.
move/negP/negP: Hx => Hx.
have [p Hc] := diconnect_path_cycle Hx Hd.
have Hp: path g x p by move: Hc; rewrite /= rcons_path; move/andP => [Hp Ha].
by move/negP: (g_acyclic Hp); case.
Qed.

End Acyclic.

Section AcyclicSub.

Variable V : finType.
Variable g : rel V.

Hypothesis g_acyclic : acyclic g.

Variable P : pred V.

Local Notation I := (sig_finType P).

Local Notation gsub := [rel x y : I | g (val x) (val y)].

Lemma gsub_acyclic : acyclic gsub.
Proof.
move => x p.
move/gsub_path.
move/g_acyclic => Hc.
rewrite /= rcons_path.
apply/negP => Hc'.
move/andP: Hc' => [Hp Hg].
move/negP: Hc.
case.
rewrite /= rcons_path.
apply/andP.
split; first by apply/gsub_path.
rewrite /= in Hg.
by rewrite last_map.
Qed.

End AcyclicSub.

Section AcyclicRev.

Variable V : finType.

Variable g : rel V.

Hypothesis g_acyclic : acyclic g.

Local Notation grev := [rel x y | g y x].

Lemma acyclic_rev : acyclic grev.
Proof.
move => x p Hp.
apply/negP => H_c; move: H_c.
move/cycle_path_diconnect.
case.
- move => H_in.
  have Hg: g x x by [].
  move/self_loop_cycle: Hg => Hg.
  contradict Hg.
  apply/negP.
  exact: g_acyclic.
- move => [y [Hd Hn]].
  have H_rev: g =2 [rel x y | grev y x] by [].
  have Hd': diconnect g x y.
  have Heq := eq_diconnect H_rev.
    rewrite Heq.
    move/andP: Hd => [Hc1 Hc2].
    apply/andP.
    by split; apply connect_rev.
  have Hc := diconnect_path_cycle _ Hd'.
  have [p' Hc'] := Hc Hn.
  have Hp': path g x p'.
    rewrite /= in Hc'.
    rewrite rcons_path in Hc'.
    by move/andP:Hc' => [Hp' Hgl].
  contradict Hc'.
  apply/negP.
  exact: g_acyclic.
Qed.

End AcyclicRev.

Section Acyclicity.

Variable V : finType.
Variable sccs : rel V -> seq (seq V).
Variable g : rel V.

Hypothesis uniq_flatten : uniq (flatten (sccs g)).

Hypothesis all_in_flatten : forall v : V, v \in (flatten (sccs g)).

Hypothesis class_diconnected :
  forall c, c \in sccs g ->
  exists x, forall y, (y \in c) = diconnect g x y.

Lemma in_flatten (A : seq (seq V)) s :
  s \in A ->
  subseq s (flatten A).
Proof.
elim: A => //=.
move => vs c IH H_in.
have H_or: s = vs \/ s \in c.
  move/orP: H_in.
  case; first by move/eqP; left.
  by right.
case: H_or => H_in'.
  by rewrite H_in' prefix_subseq.
have IH' := IH H_in'.
have ->: s = [::] ++ s by [].
by apply cat_subseq; first exact: sub0seq.
Qed.

Lemma non_singleton_neq : forall v v' vs,
  [:: v, v' & vs] \in sccs g ->
  v != v'.
Proof.
move => v v' vs H_ks.
apply/negP.
move/eqP => H_eq.
rewrite -H_eq {H_eq} in H_ks.
have H_fl := uniq_flatten.
apply in_flatten in H_ks.
apply subseq_uniq in H_ks => //.
rewrite /= in H_ks.
move/andP: H_ks.
rewrite inE.
move => [H_n H_u].
move/negP: H_n => H_n.
case: H_n.
by apply/orP; left.
Qed.

Lemma non_singleton_cycle : forall v v' vs,
  [:: v, v' & vs] \in sccs g ->
  exists x p, cycle g (x :: p).
Proof.
move => v v' vs H_ks.
have H_c := class_diconnected H_ks.
rewrite /class_diconnected /= in H_c.
move: H_c => /= [x H_y].
have H_v := H_y v.
have H_v' := H_y v'.
have H_neq := non_singleton_neq H_ks.
have H_in_v: v \in [:: v, v' & vs] by rewrite inE; apply/orP; left.
have H_in_v': v' \in [:: v, v' & vs] by rewrite inE; apply/orP; right; apply/orP; left.
rewrite H_v {H_v} in H_in_v.
rewrite H_v' {H_v'} in H_in_v'.
rewrite /diconnect in H_in_v H_in_v'.
move/andP: H_in_v => [H_cn_v H_cn'_v].
move/connectP: H_cn_v => [pv H_pv] H_vl.
move/connectP: H_cn'_v => [p'v H_p'v] H_vl'.
move/andP: H_in_v' => [H_cn_v' H_cn'_v'].
move/connectP: H_cn_v' => [pv' H_pv'] H_v'l.
move/connectP: H_cn'_v' => [p'v' H_p'v'] H_v'l'.
have H_pvv': connect g v v'.
  apply/connectP.
  exists (p'v ++ pv'); last by rewrite last_cat -H_vl'.
  rewrite cat_path.
  rewrite -H_vl'.
  by apply/andP.
have H_p'vv': connect g v' v.
  apply/connectP.
  exists (p'v' ++ pv); last by rewrite last_cat -H_v'l'.
  rewrite cat_path.
  rewrite -H_v'l'.
  by apply/andP.
have H_di: diconnect g v v'.
  rewrite /diconnect.
  by apply/andP.
have [p H_p] := diconnect_path_cycle H_neq H_di.
by exists v, p.
Qed.

Lemma all_in_sccs :
 forall v, exists vs, vs \in sccs g /\ v \in vs.
Proof.
move => v.
have H_all := all_in_flatten v.
move/flattenP: H_all => [vs [H_vs H_in]].
by exists vs.
Qed.

Lemma diconnect_neq_sccs :
  forall x y, diconnect g x y -> x != y ->
  exists v v' vs, [:: v, v' & vs] \in sccs g.
Proof.
move => x y H_y H_neq.
have [vs [H_vs H_in]] := all_in_sccs x.
have [x' H_c] := class_diconnected H_vs.
have H_eq: x \in vs by [].
have H_c' := H_c x.
rewrite H_c' in H_eq.
have H_di: diconnect g x' y.
  move/andP: H_eq => [H_x'x H_xx'].
  move/andP: H_y => [H_xy H_yx].
  apply/andP; split.
  - move: H_x'x H_xy.
    exact: connect_trans.
  - move: H_yx H_xx'.
    exact: connect_trans.
rewrite -H_c in H_di.
move {H_y H_c H_c' H_eq}.
case: vs H_in H_di H_vs => //.
move => v.
case.
- rewrite 2!inE.
  move/eqP => H_xv.
  rewrite -H_xv.
  move/eqP => H_yx.
  move/negP: H_neq => H_neq.
  case: H_neq.
  by apply/eqP.
- move => v' vs H_x H_y.
  by exists v, v', vs.
Qed.

Definition class_acyclic (c : seq V) :=
match c with
| [::] => true
| [:: v] => ~~ g v v
| [:: _, _ & _] => false
end.

Definition sccs_acyclic :=
  all [pred c | class_acyclic c] (sccs g).

Lemma sccs_acyclicP :
  reflect (acyclic g) sccs_acyclic.
Proof.
  apply: (iffP idP).
- move/allP => /=.
  move => H_in_ac v p H_p.
  apply/negP => H_ce.
  apply cycle_path_diconnect in H_ce.
  case: H_ce => H_ce.
  * have [vs [H_vs H_v]] := all_in_sccs v.
    move: H_vs H_v.
    move/H_in_ac.
    case: vs => //=.
    move => v'.
    case => //=.
    move/negP.
    rewrite inE => H_in.
    move/eqP => H_eq.
    by rewrite H_eq in H_ce.
  * move: H_ce => [y [H_d H_neq]].
    have [v0 [v1 [vs H_ks]]] := diconnect_neq_sccs H_d H_neq.
    by move/H_in_ac: H_ks.
- move => H_gc.
  apply/allP.
  case => //= v.
  case => //=.
  * move => H_in.
    apply/negP.
    move => H_in'.
    have H_ce: cycle g [:: v] by apply/andP.
    contradict H_ce.
    apply/negP.
    exact: H_gc.
  * move => v' vs.
    move/non_singleton_cycle.
    move => [x [p H_ce]].
    have H_ce' := H_ce.
    rewrite /= in H_ce'.
    rewrite rcons_path in H_ce'.
    move/andP: H_ce' => [H_p H_l].
    contradict H_ce.
    apply/negP.
    exact: H_gc.
Qed.

End Acyclicity.