finished proofs of cycle detection and topological sort spec

DerivedProofs.v

@@ -9,6 +9,16 @@ Require Import Helper.
 Require Import Coq.Arith.PeanoNat.
 Require Import Omega.
 
+(* This module consists of proofs of both properties and applications of DFS that use only the specification
+    defined in DFSBase and thus are independent of any actual DFS algorithm. The significant results include
+    - A necessary and sufficient condition for graph reachability - u is reachable from v iff when we start
+        DFS from v, u is a descendant
+    - The existence of a path between two vertices is decidable
+    - A necessary and sufficient condition for (nontrivial) cycle existence - there is a nontrivial cycle
+      (ie, a cycle that contains more than 1 vertex) iff there is a back edge (an edge (u,v) in g such that
+      u is a descendant of v in the DFS forest). This does not yet give a cycle detection algorithm
+    - A proof of the CLRS topological sorting algorithm: A list of vertices sorted in reverse order of their
+      finish times is topologically sorted*)
 Module DerivedProofs(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S G)(D: DFSBase O S G F).
 
 Module P:= D.P. 
@@ -72,10 +82,13 @@ Qed.
 
 (** ** Application 2: Cycle Detection **)
 
-(*A back edge is an edge (u, v) in g such that v is gray when u is discovered*)
-Definition back_edge g s u v o := D.time_of_state g s = D.d_time o g u /\ G.contains_edge g u v = true
-   /\ D.gray o g s v = true.
+Definition back_edge g u v o := G.contains_edge g u v = true /\ F.desc (D.dfs_forest o g) v u.
+
 
+(*We want to be able to reason about the vertex in the cycle that is discovered first. So we need a few
+  helper definitions and lemmas*)
+
+(*A function to compute the vertex with the smallest discovery time*)
 Fixpoint first_vertex o g (l: list G.vertex) (d: G.vertex) : G.vertex :=
   match l  with
   | nil => d
@@ -85,6 +98,7 @@ Fixpoint first_vertex o g (l: list G.vertex) (d: G.vertex) : G.vertex :=
               end
   end.
 
+(*The result of [first_vertex] is in the original list*)
 Lemma first_vertex_in_list: forall o g l d,
   l <> nil ->
   In (first_vertex o g l d) l.
@@ -97,6 +111,8 @@ Proof.
       left. reflexivity. right. apply IHl. intro. inversion H0.
 Qed.
 
+(*[first_vertex] actually finds the vertex with the (strictly) smallest discovery time as long as
+  everything in the list is in the graph*)
 Lemma first_vertex_finds_smallest: forall g o l d u,
   l <> nil ->
   G.contains_vertex g u = true ->
@@ -126,6 +142,7 @@ Proof.
         right. apply H5. apply H3. apply H4.
 Qed. 
 
+(*A path has a vertex that finishes first*)
 Lemma path_has_smallest_vertex: forall o g l (v: G.vertex),
   l <> nil ->
   (forall x, In x l -> G.contains_vertex g x = true) ->
@@ -136,56 +153,176 @@ Proof.
   apply H0. reflexivity.
 Qed.
 
+(*A more specific and helper lemma for cycles: If we have a cycle from v to v, then there is a cycle
+  from u to u such that every vertex in the original cycle is also in the new cycle and
+   u has a smaller finish time than every vertex in the cycle. This allows us to directly work with
+  the first vertex discovered in a cycle without having to destruct into cases*)
 Lemma cycle_smallest: forall o g l v,
   l <> nil ->
   P.path_list_rev g v v l = true ->
-  exists l1 u, P.path_list_rev g u u l1 = true /\ (u <> v -> In u l) /\ (u <> v -> In v l1) /\ l1 <> nil /\ (forall x, In x l1 -> x <> u ->
-  D.d_time o g u < D.d_time o g x).
+  exists l1 u, P.path_list_rev g u u l1 = true /\ (u <> v -> In u l) /\ (u <> v -> In v l1)
+   /\ l1 <> nil /\ (forall x, In x l1 -> x <> u -> D.d_time o g u < D.d_time o g x) /\
+  (forall x, x <> u -> x <> v -> (In x l <-> In x l1)).
 Proof.
   intros. assert (A:=H0). assert (forall x, In x l -> G.contains_vertex g x = true). intros.
   eapply D.P.path_implies_in_graph in H0. destruct_all. apply H3. apply H1. assert (B:= H).
   eapply (path_has_smallest_vertex o g) in H. destruct_all.
   assert (D.d_time o g x < D.d_time o g v \/ D.d_time o g v < D.d_time o g x \/ D.d_time o g x = D.d_time o g v)
   by omega. destruct H3. eapply (P.any_cycle _ _ x) in H0. destruct_all. exists x0.
   exists x. split. apply H0. split. intros. apply H. split. intros. apply H4. split. intro. subst. inversion H4.
+  split.
   intros. destruct (O.eq_dec x1 v). unfold O.eq in e. subst. apply H3. apply H2.
-  rewrite H5. apply H6. apply n. apply H7. apply H7. apply H.
+  rewrite H5. apply H6. apply n. apply H7. apply H7. intros. apply H5; auto. apply H.
   destruct H3. exists l. exists v. split. apply H0. split. intros. contradiction. split. intros.
-  contradiction. split. apply B. intros. destruct (O.eq_dec x x0). unfold O.eq in e. subst.
-  apply H3. apply H2 in H4. omega. auto. assert (x = v). eapply D.d_times_unique.
+  contradiction. split. apply B. split. intros.  destruct (O.eq_dec x x0). unfold O.eq in e. subst.
+  apply H3. apply H2 in H4. omega. auto. intros. reflexivity. assert (x = v). eapply D.d_times_unique.
   apply H1. apply H. eapply D.P.path_implies_in_graph in H0. simplify. apply H3. subst.
    exists l. exists v. split. apply H0. split. intros. contradiction. split. intros. contradiction.
-  split. apply B. apply H2. apply v. apply H1.
+  split. apply B. split. apply H2. intros. reflexivity. apply v. apply H1.
+Qed.
+
+Lemma desc_iff_gray_when_discovered: forall (g : G.graph) o u v,
+  G.contains_vertex g v = true ->
+  G.contains_vertex g u = true ->
+  u <> v ->
+  F.desc (D.dfs_forest o g) u v <-> (forall s, D.time_of_state g s = D.d_time o g v -> D.gray o g s u = true).
+Proof.
+  intros. split; intros.
+  - apply D.descendant_iff_interval in H2. destruct_all.
+    unfold D.gray. simplify. rewrite H3. apply Nat.ltb_lt. omega. rewrite H3. apply Nat.leb_le. omega.
+    apply F.desc_in_forest in H2. destruct_all. eapply D.same_vertices. apply H2.
+    apply F.desc_in_forest in H2. destruct_all. eapply D.same_vertices. apply H5.
+  - pose proof (D.discovery_exists o g v H). destruct_all. specialize (H2 x H3). 
+    unfold D.gray in H2. simplify. rewrite Nat.ltb_lt in H4. rewrite Nat.leb_le in H5.
+    rewrite H3 in H4. rewrite H3 in H5. assert (D.d_time o g u < D.d_time o g v).
+    assert ((D.d_time o g u < D.d_time o g v) \/ (D.d_time o g u = D.d_time o g v)) by omega.
+    destruct H2. apply H2. apply D.d_times_unique in H2. subst. contradiction.
+    all: try(assumption). clear H5. pose proof (D.parentheses_theorem
+    o g u v H0 H H1). destruct H5. eapply D.descendant_iff_interval. apply H0. apply H. apply H5.
+    repeat (destruct H5; omega).
 Qed.
 
+(*Alternative definition of back edge: an edge (u, v) in g such that v is gray when u is discovered*)
+Definition back_edge' g u v o := exists s, u <> v /\ D.time_of_state g s = D.d_time o g u /\ G.contains_edge g u v = true
+   /\ D.gray o g s v = true.
 
-(** The big result (Lemma 22.11 in CLRS) **)
-(*Note that this doesn't work for self loops - although the CLRS proof fails for this case as well. However,
-  this is a trivial case, since cycle detection is easy and efficient - 
-  iterate over all the vertices and check for self loops*)
-
-(*Need to know that there is another vertex in the cycle - cycle with no dups*)
-(*So I don't have to repeat the same proof 3 times*)
-(*Lemma smallest_at_cycle_back_edge: forall g o u l,
-  P.path_list_rev g u u l = true ->
-  (forall x, In x l -> D.d_time o g u < D.d_time o g x) ->
-  (exists s u v, back_edge g s u v o).
+(*The two definitions are equivalent*)
+Lemma back_edge_equiv: forall o g u v,
+  back_edge g u v o <->  back_edge' g u v o.
 Proof.
-Admitted.*)
+  intros. split; intros.
+  - unfold back_edge in H. unfold back_edge'. destruct_all.
+    assert (G.contains_vertex g u = true). eapply G.contains_edge_1. apply H.
+    pose proof (D.discovery_exists o g u H1). destruct_all. assert (A:= H0). 
+    eapply desc_iff_gray_when_discovered in H0. exists x. split. assert (v <> u). eapply F.desc_neq. apply A.
+    auto. split. apply H2. split. apply H. apply H0. apply H1. eapply G.contains_edge_2. apply H.
+    eapply F.desc_neq. apply H0. apply H2.
+  - unfold back_edge' in H. unfold back_edge. destruct_all. split. apply H1.
+    eapply desc_iff_gray_when_discovered. eapply G.contains_edge_1. apply H1.
+    eapply G.contains_edge_2. apply H1. auto. intros.
+    assert (s = x). eapply D.state_time_unique. omega. subst. apply H2.
+Qed.
+
 
+
+(** The big result (Lemma 22.11 in CLRS) **)
+(*There is a nontrivial cycle (ie, a cycle that does not consist of a single vertex) iff there is a back
+  edge.*)
 Lemma cycle_iff_back_edge: forall g o,
-  P.cyclic_no_self_loop g <-> (exists s u v, back_edge g s u v o).
+  P.nontrivial_cyclic g <-> (exists u v, back_edge' g u v o).
 Proof.
   intros. split; intros.
-  - unfold P.cyclic_no_self_loop in H. destruct_all.
+  - unfold P.nontrivial_cyclic in H. destruct_all.
     eapply (cycle_smallest o) in H0. destruct_all.
     eapply P.cycle_no_dups_strong in H0. destruct_all. 
-    destruct x4. contradiction. simpl in *. unfold back_edge. 
-    simplify.  
-    (*The plan from here: (I have all the pieces)
-      - At tmie d(x3), there is a white path to v
-      - Therefore v is a descendant of x3
-      - Therefore, x3 finishes after v
-      - Therefore, at time d(v), x3 is gray
-      - Then use that time for a back edge *)
-
+    destruct x4. contradiction. simpl in *. unfold back_edge'. 
+    simplify.
+    assert (F.desc (D.dfs_forest o g) x3 v). { eapply D.white_path_theorem.
+    eapply G.contains_edge_2. apply H11. intros.
+    exists x4. rewrite D.P.path_list_ind_rev. split. apply H12. split. intros.
+    unfold D.white. rewrite H8. apply Nat.ltb_lt. apply H5. apply H10. right. apply H14.
+    intro. subst. contradiction. unfold D.white. apply Nat.ltb_lt. rewrite H8. apply H5.
+    apply H10. left. reflexivity. apply H0. }
+    pose proof (D.discovery_exists o g v). assert (G.contains_vertex g v = true). 
+    eapply G.contains_edge_1. apply H11. apply H14 in H15; clear H14. destruct_all.
+    eapply desc_iff_gray_when_discovered in H8. exists v. exists x3. exists x5.
+    split. apply H0. split. apply H14. split. apply H11. apply H8. eapply G.contains_edge_1. apply H11.
+    eapply G.contains_edge_2. apply H11. auto. apply H14. destruct (O.eq_dec x x3). unfold O.eq in e.
+    subst. exists x1. split. rewrite <- H6. apply H1. auto. auto. auto. exists x. split. apply H3.
+    auto. auto. intro. subst. inversion H1.
+  - destruct_all. assert (A:=H). rewrite <- back_edge_equiv in H. unfold back_edge in H.
+    unfold P.nontrivial_cyclic. destruct_all.
+    unfold back_edge' in A. destruct_all. rewrite <- F.desc_list_iff_desc in H0.
+    destruct_all. apply desc_implies_path in H0. exists x0. exists (x :: x2). split.
+    exists x. split. auto. solve_in. simpl. simplify.
+Qed.
+
+(** ** Topological Sorting **)
+
+(*CLRS defines a simple topological sorting algorithm: run DFS and return a list of the vertices reverse sorted
+  by finish time. We will prove that this is a valid topological ordering*)
+
+(*A topological ordering is one where there are no edges going backward in the list and every vertex in the 
+  graph is in the list*)
+Definition topological_sort (l: list G.vertex) (g: G.graph):=
+  (forall v, G.contains_vertex g v = true <-> In v l) /\ 
+  (forall l1 l2 l3 u v, l = l1 ++ u :: l2 ++ v :: l3 -> G.contains_edge g v u = false).
+
+(*The resulting list is sorted in reverse order of finish time*)
+Definition rev_f_time o g (u v: G.vertex) : Prop :=
+  D.f_time o g u > D.f_time o g v.
+
+(*Helpful to know that color is total*)
+Lemma color_total: forall g o s u,
+  D.white o g s u = true \/ D.gray o g s u = true \/ D.black o g s u = true.
+Proof.
+  intros. unfold D.white. unfold D.gray. unfold D.black. simplify. repeat(rewrite Nat.ltb_lt).
+  repeat(rewrite Nat.leb_le). omega.
+Qed.
+
+(*A key lemma for topological sorting: If the edge (u,v) exists, then u finishes after v*)
+Lemma finish_time_edge: forall g o u v,
+  P.acyclic g ->
+  G.contains_edge g u v = true ->
+  D.f_time o g v < D.f_time o g u.
+Proof.
+  intros. assert (G.contains_vertex g u = true) by (eapply G.contains_edge_1; apply H0).
+  pose proof (D.discovery_exists o g u H1). destruct_all.
+  pose proof (color_total g o x v). destruct H3.
+  - assert (F.desc (D.dfs_forest o g) u v). eapply D.white_path_theorem.
+    apply H1. intros. exists nil. rewrite P.path_list_ind_rev. split.
+    simpl. apply H0. split. intros. inversion H5.
+    assert (s = x). eapply D.state_time_unique. omega. subst. apply H3.
+    eapply D.descendant_iff_interval in H4. omega. apply H1. eapply G.contains_edge_2. apply H0.
+  - destruct H3. assert (H4:= H). apply P.acylic_no_nontrivial in H. exfalso. apply H.
+    rewrite (cycle_iff_back_edge _ o). unfold back_edge'. exists u. exists v. exists x. split.
+    intro. subst. unfold P.acyclic in H4. apply H4. exists v. 
+    constructor. apply H0. split. apply H2. split. apply H0. apply H3.
+    unfold D.black in H3. rewrite Nat.leb_le in H3. 
+    assert ((D.f_time o g v = D.time_of_state g x) \/ (D.f_time o g v < D.time_of_state g x)) by omega.
+    assert (G.contains_vertex g v = true). eapply G.contains_edge_2. apply H0.
+    destruct H4. pose proof (D.all_times_unique o g v u H5 H1). omega. assert (u <> v).
+    intro. subst. unfold P.acyclic in H. apply H. exists v. constructor. apply H0.
+    pose proof (D.parentheses_theorem o g u v H1 H5 H6). omega.
+Qed.
+
+(** Topological Sort Correctness **)
+(*Given a list of vertices sorted by reverse order of finish time, if g is a DAG and every vertex in g is in
+  the list, then the list is a topological sorting of g*)
+Lemma topological_sort_correct: forall l g o,
+  P.acyclic g ->
+  (forall v, G.contains_vertex g v = true <-> In v l) ->
+  StronglySorted (rev_f_time o g) l ->
+  topological_sort l g.
+Proof.
+  intros. unfold topological_sort. split. apply H0.
+  intros. subst. apply sort_app in H1. destruct H1. inversion H2; subst.
+  rewrite Forall_forall in H6. destruct (G.contains_edge g v u) eqn : ?.
+  specialize (H6 v). assert (rev_f_time o g u v). apply H6. solve_in.
+  unfold rev_f_time in H3. apply (finish_time_edge g o v u) in Heqb.
+  omega. apply H. reflexivity.
+Qed. 
+
+End DerivedProofs.
+
+

Forest.v

@@ -389,7 +389,14 @@ Qed.
       rewrite <- desc_list_iff_desc. exists l. apply H1.
       eapply IHl. apply H0. apply H1.
   Qed. 
-
+
+Parameter child_neq: forall f u v,
+  is_child f u v = true -> u <> v.
+(*TODO:see which is best: prove acyclicty of graph and then relate to path, prove directly in impl, etc*)
+Parameter desc_neq: forall f u v,
+  desc f u v ->
+  u <> v.
+
 
 (*might need equal lemma to ensure it is acyclic but we 
 will see*)

Path.v

@@ -126,13 +126,21 @@ Qed.
   Definition cyclic (g: graph) := exists v, path g v v.
 
   (*There is a cycle that does not consist only of a single vertex*)
-  Definition cyclic_no_self_loop (g: graph) := exists v l, (exists x, x <> v /\ In x l)
+  Definition nontrivial_cyclic (g: graph) := exists v l, (exists x, x <> v /\ In x l)
    /\ path_list_rev g v v l = true.
 
   Definition acyclic (g: graph):= ~ exists v, path g v v.
 
   Definition acyclic' (g: graph) := forall v, ~path g v v.
 
+  Lemma acylic_no_nontrivial: forall g,
+    acyclic g ->
+    ~nontrivial_cyclic g.
+  Proof.
+   intros. intro.  unfold acyclic in H. unfold nontrivial_cyclic in H0. destruct_all.
+    apply H. exists x. rewrite path_path_list_rev. exists x0. apply H1.
+  Qed.
+
   Lemma acyclic_equiv: forall g,
     acyclic' g <-> acyclic g.
   Proof.

_CoqProject

@@ -5,4 +5,5 @@ AdjacencyMap.v
 Path.v
 Forest.v
 DFSSpec.v
+DerivedProofs.v
 DFS.v