exercise4

Some basic facts about disjoint where the first element is a set and the second one a list

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.
Qed.

Lemma rconnectP s x y :
   reflect 
    (exists2 p, path r x p & ((y = last x p) /\ [disjoint p & s]))
    (x -[s]-> y).
Proof.
Qed.

Lemma rconnect_set0  : rconnect set0 =2 connect r.
Proof.
Qed.

Lemma rconnect_ref s : reflexive (rconnect s).
Proof.
Qed.

Lemma rconnect1 s x y : y \notin s -> r x y -> x -[s]-> y.
Proof.
Qed.

Lemma rconnect_trans s : transitive (rconnect s).
Proof.
Qed.

Lemma rconnect_subset (s1 s2 : {set T}) x y : 
  {subset s1 <= s2} ->  x -[s2]-> y -> x -[s1]-> y.
Proof.
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.
Qed.

Lemma rconnect_setU1r s x y z :
  ~~ z -[s]-> y ->  x -[s]-> y -> x -[z |: s]-> y.
Proof.
Qed.

Lemma rconnect_setU1l s x y z : 
  ~~ (x -[s]-> z) ->  x -[s]-> y -> x -[z |: s]-> y.
Proof.
Qed.

Lemma rconnect_id_setU1 s x y : x -[x |: s]-> y = x -[s]-> y.
Proof.
Qed.

x is biconnected to y avoiding the elements of s

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.
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.
Qed.

Lemma rcan_cat x s l1 l2 : x \in l1 -> C[x]_(s, l1 ++ l2) = C[x]_(s, l1).
Proof.
Qed.

Lemma requiv_can x s l : x \in l -> C[x]_(s, l) =[s]= x.
Proof.
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.
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.
Qed.

Lemma leq_index_nth x l i : index (nth x l i) l  <= i.
Proof.
Qed.

Lemma index_find x l a :  has a l -> index (nth x l (find a l)) l = find a l.
Proof.
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.
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.
Qed.

well formed list : rconnected elements are inside and canonical elements are on top

Removing the equivalent elements of the top preserve well-formedness

Computing the connected elements for the reversed graph gives the equivalent class of the top element of an well_formed list

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.
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.
apply: ok.
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.
Qed.

Building the stack of all nodes

The stack is well-formed and contains all the nodes

Kosaraju algorithm

save script

load script