digraph.v

(* Directed finite graph  *)


Require Import
  Ssreflect.ssreflect Ssreflect.ssrbool
  Ssreflect.ssrfun Ssreflect.eqtype
  Ssreflect.ssrnat Ssreflect.seq
  Ssreflect.path Ssreflect.fintype
  Ssreflect.fingraph.

Set Implicit Arguments.


Lemma connectP_uniq {T: finType}(e: rel T) x y:
  reflect (exists p, path e x p /\ y = last x p /\ uniq (x::p)) (connect e x y).
Proof.
  apply /iffP.
  apply connectP.
  - move => [p Hp Heq].
    apply shortenP in Hp.
    rewrite -Heq in Hp.
    destruct Hp.
    exists p'.
    repeat split; done.
  - move => [p [Hp [Heq Huniq]]].
    exists p; done.
Qed.

Lemma in_uniq_cat {T: eqType}(s1 s2: seq T):
  uniq (s1 ++ s2) -> forall x, x \in s1 -> x \notin s2.
Proof.
  rewrite cat_uniq.
  move => /and3P [Huniq1 Hnhas Huniq2] x.
    by move: Hnhas => /hasPn //= H; apply contraL, H.
Qed.
  
Lemma uniq_last_nil {T: eqType}(x: T) p:
  uniq (x::p) -> x = last x p -> p = [::].
Proof.
  move: p => [| h t] //=.
                     move => /and3P [Hninx Hninh Huniq] Heq.
  rewrite Heq in Hninx.
  rewrite mem_last //= in Hninx.
Qed.

Lemma last_cat_notin {T: eqType}(x y: T) s1 s2:
  x = last y (s1 ++ s2) -> x \notin s2 -> s2 = [::].
Proof.
  move: x y s1.
  pattern s2.
  apply last_ind; try done.
  move => s x IH y z s1.
  rewrite last_cat last_rcons mem_rcons in_cons negb_or;
    move => -> /andP [Hneq _] //=; move: Hneq => /eqP //=.
Qed.    


Section CFG.

  Variables (V: finType)(E: rel V)(r: V).

  Hypothesis reachable:
    forall (v: V), connect E r v.

  Definition dominate (u v: V) :=
    forall (p: seq V),
      path E r p -> v = last r p -> u \in (r::p).

  Lemma dominate_root u:
    dominate r u.
  Proof.
    rewrite /dominate; move => p Hp Heq.
    by rewrite in_cons; apply /orP; left.
  Qed.

  Lemma dominate_refl u:
    dominate u u.
  Proof.
    by rewrite /dominate; move => p Hp ->; apply mem_last.
  Qed.

  Lemma dominate_sym u v:
    dominate u v -> dominate v u -> u == v.
  Proof.
    rewrite /dominate.
    move => Huv Hvu.
    move: (reachable u) => /connectP_uniq [p1 [Hp1 [Heq1 Huniq1]]].
    move: (Hvu p1 Hp1 Heq1); rewrite in_cons; move => /orP.
    move => [Heqvr | Hin1].
    - move: Heqvr (eq_refl r) => /eqP Heqvr /eqP H.
      rewrite Heqvr in Huv; rewrite Heqvr.
      by move: (Huv [::] is_true_true H) => //=; rewrite mem_seq1.
    - move: (splitPr Hin1) => Hsplit1; destruct Hsplit1.
      rewrite -cat1s catA cat_path cats1 in Hp1.
      move: Hp1 => /andP [Hp1 _].
      move:  (Huv (rcons p1 v) Hp1 (esym (last_rcons r p1 v))) => Hin.
      move: Heq1 Huniq1 Hin1;
        rewrite -(cat1s v) catA cats1;
        move => Heq1 Huniq1 Hin1.
      rewrite -cat_cons in Huniq1.
      move: (last_cat_notin _ _ _ Heq1 (in_uniq_cat _ _ Huniq1 u Hin)) => Heq.
      rewrite Heq cats0 last_rcons in Heq1.
      rewrite Heq1 //=.
  Qed.      

  Lemma dominate_trans u v w:
    dominate u v -> dominate v w -> dominate u w.
  Proof.
    rewrite {2 3}/dominate.
    move => Huv Hvw p Hp Heq.
    move: (Hvw p Hp Heq); rewrite in_cons; move => /orP [Heqv | Hinv].
    - move: Heqv => /eqP Heqv; subst v.
      move: (dominate_sym (@dominate_root u) Huv) => /eqP <- //=.
      by rewrite in_cons; apply /orP; left.
    - move: (splitPr Hinv) => Hsplit.
      destruct Hsplit as [pl pr].
      rewrite /dominate in Huv.
      rewrite -cat1s catA cat_path cats1 in Hp.
      move: Hp => /andP [Hp _].
      move: (Huv (rcons pl v) Hp (esym (last_rcons r pl v))) => Hin.
      by rewrite -(cat1s v) catA -cat_cons cats1 mem_cat; apply /orP; left.
  Qed.


  Lemma dominate_lemma:
    forall (u1 u2 v: V),
      dominate u1 v -> dominate u2 v ->
      dominate u1 u2\/dominate u2 u1.
  Proof.
    rewrite /dominate.
    move => u1 u2 v Hdom1 Hdom2;
      move: (reachable v) => /connectP_uniq [p [Hp [Heq Huniq]]];
      move: (reachable u1) => /connectP_uniq [p1 [Hp1 [Heq1 Huniq1]]];
      move: (reachable u2) => /connectP_uniq [p2 [Hp2 [Heq2 Huniq2]]];
      move: (Hdom1 p Hp Heq) => Hin1;
      move: (Hdom2 p Hp Heq) => Hin2.
    rewrite in_cons in Hin1.
    rewrite in_cons in Hin2.
    move: Hin1 => /orP [Heqr1 | Hin1].
    - move: Heqr1 => /eqP Heqr1; subst.
      rewrite Heqr1.
      left.
      move => p' _ _; rewrite in_cons; apply /orP; by left.
    - move: Hin2 => /orP [Heqr2 | Hin2].
      move: Heqr2 => /eqP Heqr2.
      rewrite Heqr2.
      right.
      move => p' _ _; rewrite in_cons; apply /orP; by left.

    apply splitPr in Hin1.
    destruct Hin1.
    rewrite cons_uniq in Huniq.
    move: Huniq => /andP [Hnin Huniq].
    move: (in_uniq_cat _ _ Huniq) => Hinin.
    rewrite cat_path in Hp.
    rewrite mem_cat in Hin2.
    move: Hp => /andP [Hp0 Hp3].
    move: Hin2 => /orP [Hin2l | Hin2r].
    - right.
      move => p' Hp' Heq'.
      move: Hp3 => //= /andP; rewrite Heq'; move => [He Hp3].
      move: (conj Hp' Hp3) => /andP; rewrite -cat_path; move => H.
      rewrite last_cat in Heq.
      rewrite last_cons in Heq.
      rewrite Heq' in Heq.
      rewrite -last_cat in Heq.
      move: (Hdom2 (p'++p3) H Heq) ; rewrite in_cons mem_cat.
      move: (Hinin u2 Hin2l) => Hnin2.
      rewrite in_cons negb_or in Hnin2.
      move: Hnin2 => /andP [Hneq Hnin3].
      move /or3P => [Heqr2 | Hin' | Hin3].
        by move: Heqr2 => /eqP ->; rewrite in_cons; apply /orP; left.
        by apply /orP; right.
        by rewrite Hin3 //= in Hnin3.
    - rewrite in_cons in Hin2r.
      move: Hin2r => /orP [Heq12 | Hin2].
      + left.
        move: Heq12 => /eqP Heq12; rewrite Heq12.
        rewrite Heq12 in Heq2.
        clear Heq12 Hdom2 u2.
        move => p' Hp' Heq'.
        move: Hp3 => //= /andP; rewrite Heq'; move => [He Hp3].
        move: (conj Hp' Hp3) => /andP; rewrite -cat_path; move => H.
        rewrite last_cat in Heq.
        rewrite last_cons in Heq.
        rewrite Heq' in Heq.
        rewrite -last_cat in Heq.
        move: (Hdom1 (p'++p3) H Heq); rewrite in_cons mem_cat.
        rewrite -Heq'.
        move => /or3P [Heqr1 | Hin1' | Hin3].
          by move: Heqr1 => /eqP ->; rewrite in_cons; apply /orP; left.
          by rewrite in_cons; apply /orP; right.
          rewrite cat_uniq in Huniq.
          move: Huniq => /and3P //=; move => [Huniq H1 H2].
          move: H2 => /andP [Hnin3 _].
          by rewrite Hin3 //= in Hnin3.
      + left.
        move => p' Hp' Heq'.
        apply splitPr in Hin2.
        destruct Hin2.
        rewrite -cat_cons in Hp3.
        rewrite cat_path last_cons -(cat1s u2) cat_path last_cons //= in Hp3.
        move: Hp3 => /and3P [? ? Hp4].
        rewrite Heq' in Hp4.
        rewrite last_cat last_cons last_cat last_cons Heq' -last_cat in Heq.
        move: (conj Hp' Hp4) => /andP; rewrite -cat_path; move => H.
        move: (Hdom1 (p' ++ p4) H Heq); rewrite in_cons mem_cat.
        move /or3P => [Heqr1 | Hin' | Hin4] //=.
          by move: Heqr1 => /eqP ->; rewrite in_cons; apply /orP; left.
          by rewrite in_cons; apply /orP; right.
        rewrite cat_uniq cons_uniq mem_cat negb_or in_cons negb_or in Huniq.
        move: Huniq => /and3P [_ _ H'];
          move: H' => /andP [H' _];
          move: H' => /and3P [_ _ Hnin4].
        rewrite Hin4 //= in Hnin4.
  Qed.

End CFG.