some refactoring I think

AdjacencyMap.v

@@ -482,4 +482,6 @@ Qed.
     intros. unfold topological_sort. reflexivity.
   Qed.
 
+  Definition undirected (g: graph) := forall u v, contains_edge g u v = true <-> contains_edge g v u = true. 
+
 End AdjacencyMap. 

DFS.v

@@ -19,7 +19,7 @@ Require Import Coq.Logic.EqdepFacts.
   track of the vertices not yet seen), Map (for storing discover/finish times), and UsualOrderedType
   (for the vertices). Also, we could use different sets for the Graph and Tree instances.*)
 Module DFS (O: UsualOrderedType)(M: FMapInterface.Sfun O) (S St: FSetInterface.Sfun O) (G: Graph O S)
-            (F: Forest O S G).
+            (F: Forest O S).
 
 Module P := FMapFacts.WProperties_fun O M.
 Module P2 := FSetProperties.WProperties_fun O S.

DFSCycle.v

@@ -21,7 +21,7 @@ Require Import DerivedProofs.
   track of the vertices not yet seen), Map (for storing discover/finish times), and UsualOrderedType
   (for the vertices). Also, we could use different sets for the Graph and Tree instances.*)
 Module DFSCycle (O: UsualOrderedType)(M: FMapInterface.Sfun O) (S St: FSetInterface.Sfun O) (G: Graph O S)
-            (F: Forest O S G).
+            (F: Forest O S).
 
 Module P := FMapFacts.WProperties_fun O M.
 Module P2 := FSetProperties.WProperties_fun O S.

DFSOrder.v

@@ -19,7 +19,7 @@ Require Import Coq.Logic.EqdepFacts.
   track of the vertices not yet seen), Map (for storing discover/finish times), and UsualOrderedType
   (for the vertices). Also, we could use different sets for the Graph and Tree instances.*)
 Module DFS (O: UsualOrderedType)(M: FMapInterface.Sfun O) (S St: FSetInterface.Sfun O) (G: Graph O S)
-            (F: Forest O S G).
+            (F: Forest O S).
 
 Module P := FMapFacts.WProperties_fun O M.
 Module P2 := FSetProperties.WProperties_fun O S.

DFSSpec.v

@@ -5,7 +5,7 @@ Require Import Forest.
 Require Import Path.
 Require Import Coq.Init.Nat.
 
-Module Type DFSBase (O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S G).
+Module Type DFSBase (O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S).
 
   Module P := (Path.PathTheories O S G).
 
@@ -136,7 +136,7 @@ Module Type DFSBase (O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)
 End DFSBase.
 
 
-Module Type DFSWithCycleDetect(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S G).
+Module Type DFSWithCycleDetect(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S).
   Include (DFSBase O S G F).
 
   Parameter cycle_detect: option G.vertex -> G.graph -> bool.
@@ -146,7 +146,7 @@ Module Type DFSWithCycleDetect(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G:
 
 End DFSWithCycleDetect.
 
-Module Type DFSWithTopologicalSort(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S G).
+Module Type DFSWithTopologicalSort(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S).
   Include (DFSBase O S G F).
 
   (*We have an additional function that produces a list of vertices reverse sorted by finish time*)
@@ -158,7 +158,7 @@ Module Type DFSWithTopologicalSort(O: UsualOrderedType)(S: FSetInterface.Sfun O)
 
 End DFSWithTopologicalSort.
 
-Module Type DFSCustomOrder (O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S G).
+Module Type DFSCustomOrder (O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S).
 
   Module P := (Path.PathTheories O S G).
   Module G' := (Graph.GraphOrder O S G).

DFSTopoSort.v

@@ -18,7 +18,7 @@ Require Import DFS.
 Require Import DerivedProofs.
 
 Module DFSTopoSort (O: UsualOrderedType)(M: FMapInterface.Sfun O) (S St: FSetInterface.Sfun O) (G: Graph O S)
-            (F: Forest O S G).
+            (F: Forest O S).
 
 Module P := FMapFacts.WProperties_fun O M.
 Module P2 := FSetProperties.WProperties_fun O S.

DerivedProofs.v

@@ -21,13 +21,14 @@ Require Import SCCDef.
       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 DerivedProofs(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S)(D: DFSBase O S G F).
 
 Module P:= D.P. 
 Module P2 := FSetProperties.WProperties_fun O S.
 Module O2 := OrderedTypeFacts O.
 Module M := (Helper.MinMax O).
 Module SD := (SCCDef.SCCDef O S G).
+Module Pa := (Helper.Partition O S).
 
 Lemma desc_implies_path: forall g o u v l,
   F.desc_list (D.dfs_forest o g) u v l = true ->
@@ -366,9 +367,9 @@ Proof.
 Qed.
 
 Lemma get_trees_partition_graph : forall o g,
-  P.partition G.contains_vertex g (F.get_trees (D.dfs_forest o g)). 
+  Pa.partition G.contains_vertex g (F.get_trees (D.dfs_forest o g)). 
 Proof.
-  intros. unfold P.partition. pose proof (F.get_trees_partition (D.dfs_forest o g)).
+  intros. unfold Pa.partition. pose proof (F.get_trees_partition (D.dfs_forest o g)).
   unfold F.P.partition in H. destruct_all. split. intros. apply H.
   apply D.same_vertices. apply H1. apply H0.
 Qed.
@@ -439,15 +440,15 @@ Proof.
   eapply get_tree_in_graph. apply H. apply H6.
   assert (G.contains_vertex g v = true). eapply get_tree_in_graph. apply H0. apply H7.
   assert (A :~S.In v t1 /\ ~S.In u t2). { split; intro;
-  pose proof (get_trees_partition_graph o g); unfold P.partition in H11;
+  pose proof (get_trees_partition_graph o g); unfold Pa.partition in H11;
   destruct_all; specialize (H12 t1 t2); destruct (S.equal t1 t2) eqn : ?.
   - apply S.equal_2 in Heqb; rewrite <- Heqb in H2.  assert (r1 = r2). { eapply F.tree_root_unique.
     apply H. apply H3. apply H4. apply H1. apply H2. } subst. omega.
-  - assert (P.disjoint t1 t2). apply H12. reflexivity. assumption. assumption. unfold P.disjoint in H13.
+  - assert (Pa.disjoint t1 t2). apply H12. reflexivity. assumption. assumption. unfold Pa.disjoint in H13.
     apply (H13 v). split; assumption.
   - apply S.equal_2 in Heqb; rewrite <- Heqb in H2.  assert (r1 = r2). { eapply F.tree_root_unique.
     apply H. apply H3. apply H4. apply H1. apply H2. } subst. omega.
-  - assert (P.disjoint t1 t2). apply H12. reflexivity. assumption. assumption. unfold P.disjoint in H13.
+  - assert (Pa.disjoint t1 t2). apply H12. reflexivity. assumption. assumption. unfold Pa.disjoint in H13.
     apply (H13 u). split; assumption. }
   assert (u <> v). { intro. subst. destruct_all. contradiction. }
   pose proof (D.parentheses_theorem o g u v H8 H9 H10). destruct H11.
@@ -531,15 +532,15 @@ Proof.
   assert (G.contains_vertex g v = true). eapply get_tree_in_graph. apply H0. assumption.
   assert (G.contains_vertex g u = true). eapply get_tree_in_graph. apply H. assumption.
   assert (A :~S.In v t1 /\ ~S.In u t2). { split; intro;
-  pose proof (get_trees_partition_graph o g); unfold P.partition in H13;
+  pose proof (get_trees_partition_graph o g); unfold Pa.partition in H13;
   destruct_all; specialize (H14 t1 t2); destruct (S.equal t1 t2) eqn : ?.
   - apply S.equal_2 in Heqb; rewrite <- Heqb in H2.  assert (r1 = r2). { eapply F.tree_root_unique.
     apply H. all: try assumption. }  subst. omega.
-  - assert (P.disjoint t1 t2). apply H14. reflexivity. assumption. assumption. unfold P.disjoint in H15.
+  - assert (Pa.disjoint t1 t2). apply H14. reflexivity. assumption. assumption. unfold Pa.disjoint in H15.
     apply (H15 v). split; assumption.
   - apply S.equal_2 in Heqb; rewrite <- Heqb in H2.  assert (r1 = r2). { eapply F.tree_root_unique.
     apply H. all: try assumption. }  subst. omega.
-  - assert (P.disjoint t1 t2). apply H14. reflexivity. assumption. assumption. unfold P.disjoint in H15.
+  - assert (Pa.disjoint t1 t2). apply H14. reflexivity. assumption. assumption. unfold Pa.disjoint in H15.
     apply (H15 u). split; assumption. } destruct A as [N1 N2].
   assert (N: u <> v). intro. subst. contradiction.
   rewrite P.path_path_list_rev in H8. destruct H8 as [l]. eapply P.path_no_dups in H8.
@@ -571,7 +572,7 @@ Proof.
         pose proof (D.parentheses_theorem o g u v H11 H10 N). omega. omega.
       * assert (G.contains_vertex g fst = true). eapply P.path_implies_in_graph.
         apply H8. apply H. pose proof (get_trees_partition_graph o g).
-        unfold P.partition in H16. destruct H16. specialize (H16 _ H0). destruct H16 as [t3].
+        unfold Pa.partition in H16. destruct H16. specialize (H16 _ H0). destruct H16 as [t3].
         destruct H16 as [R3 H16]. assert (A:= R3). eapply F.get_trees_root in A. destruct A as [r3].
         destruct H19 as [HR3 HI3]. destruct HI3 as [HI3 HD3].
         assert (D.f_time o g r3 > D.f_time o g r2 \/ D.f_time o g r3 = D.f_time o g r2 \/
@@ -604,7 +605,7 @@ Proof.
            ++ assert (r3 = r2). eapply D.f_times_unique. eapply get_tree_in_graph. apply R3. assumption.
               eapply get_tree_in_graph. apply R2. assumption. apply H19. subst.
               destruct (S.equal t2 t3) eqn : ?. apply S.equal_2 in Heqb. rewrite Heqb in n. contradiction.
-              apply H18 in Heqb. unfold P.disjoint in Heqb. apply (Heqb r2). split; assumption.
+              apply H18 in Heqb. unfold Pa.disjoint in Heqb. apply (Heqb r2). split; assumption.
               assumption. assumption.
            ++ assert (A:= H). eapply in_split_app_fst in A. destruct A as [l1]. destruct H20 as  [l2].
               destruct H20; subst. apply P.path_app in H8. destruct H8 as [HP1 HP2].
@@ -615,12 +616,12 @@ Proof.
               rewrite D.white_def. rewrite H8. rewrite Nat.ltb_lt. apply H17. simplify.
               intro. subst. contradiction. destruct (O.eq_dec fst r3). unfold O.eq in e. subst.
               rewrite <- HD3 in H8. destruct (S.equal t2 t3) eqn : ?. apply S.equal_2 in Heqb.
-              rewrite Heqb in n. contradiction. apply H18 in Heqb. unfold P.disjoint in Heqb.
+              rewrite Heqb in n. contradiction. apply H18 in Heqb. unfold Pa.disjoint in Heqb.
               apply (Heqb v). split; assumption. assumption. assumption. intro. subst. contradiction.
               assert (F.desc (D.dfs_forest o g) r3 v). eapply F.is_descendant_trans. apply (HD3 fst).
               auto. assumption. assumption. rewrite <- HD3 in H20. destruct (S.equal t2 t3) eqn : ?.
               apply S.equal_2 in Heqb. rewrite Heqb in n. contradiction. apply H18 in Heqb.
-              unfold P.disjoint in Heqb. apply (Heqb v). split; assumption. assumption. assumption.
+              unfold Pa.disjoint in Heqb. apply (Heqb v). split; assumption. assumption. assumption.
               intro. subst. apply F.desc_neq in H20. contradiction. apply O.eq_dec.
 Qed.
 Import SD.
@@ -724,7 +725,7 @@ End DerivedProofs.
 
 (*In particular, any implementation of [DFSWithCycleDetect] is correct*)
 
-Module CycleCorrect(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S G)
+Module CycleCorrect(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S)
   (D: DFSWithCycleDetect O S G F).
 
   Module A := (DerivedProofs O S G F D).
@@ -748,7 +749,7 @@ Module CycleCorrect(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(
 End CycleCorrect.
 
 (* The same for [DFSWithTopologicalSort] *)
-Module TopoSortCorrect(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S G)
+Module TopoSortCorrect(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S)(F: Forest O S)
   (D: DFSWithTopologicalSort O S G F).
 
   Module A := (DerivedProofs O S G F D).

Forest.v

@@ -1,13 +1,17 @@
-Require Export Graph.
+(*Require Export Graph.*)
 Require Import Helper.
+Require Import Coq.Structures.OrderedTypeEx.
+Require Import Coq.Lists.SetoidList.
+Require Import Coq.Bool.Bool.
 
-Require Export Path.
+(*Require Export Path.*)
 Require Import Coq.Lists.List.
 (*TODO: maybe extend graph instead of providing function*)
 
-Module Type Forest(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S).
+Module Type Forest(O: UsualOrderedType)(S: FSetInterface.Sfun O).
 
-  Module P := (Path.PathTheories O S G).
+  (*Module P := (Path.PathTheories O S G).*)
+  Module P := Helper.Partition O S.
 
   Parameter forest : Type.
 
@@ -29,7 +33,7 @@ Module Type Forest(O: UsualOrderedType)(S: FSetInterface.Sfun O)(G: Graph O S).
 
   (*Parameter get_children: forest -> vertex -> option (list vertex).*)
 
-  Parameter forest_to_graph: forest -> G.graph.
+  (*Parameter forest_to_graph: forest -> G.graph.*)
   (*Input: forest, ancestor, descendant*)
  (* Parameter is_descendant: forest -> vertex -> vertex -> bool.*)
 
@@ -167,14 +171,14 @@ Qed.
     get_children t u = Some l ->
     (is_child t u v = true <-> In v l).*)
 
-  Parameter tree_to_graph_1: forall t u,
+  (*Parameter tree_to_graph_1: forall t u,
     contains_vertex t u = true <-> G.contains_vertex (forest_to_graph t) u = true.
 
   Parameter tree_to_graph_2: forall t u v,
     is_child t u v = true <-> G.contains_edge (forest_to_graph t) u v = true.
 
   Parameter tree_to_graph_3: forall t,
-    P.acyclic (forest_to_graph t).
+    P.acyclic (forest_to_graph t).*)
 (*
   Parameter is_descendant_edge: forall t u v,
     is_child t u v = true ->
@@ -331,7 +335,7 @@ Proof.
   - apply IHdesc. apply H0. reflexivity.
 Qed.
 
-Lemma path_iff_desc: forall f u v,
+(*Lemma path_iff_desc: forall f u v,
   P.path (forest_to_graph f) u v <-> desc f u v.
 Proof.
   intros. split; intro H. remember (forest_to_graph f) as g. induction H; subst.
@@ -340,7 +344,7 @@ Proof.
   - induction H.
     + apply P.p_start. rewrite <- tree_to_graph_2. apply H.
     + eapply P.p_continue. apply IHdesc. rewrite <- tree_to_graph_2. apply H0.
-Qed.
+Qed.*)
 
 Import ListNotations.
 

Graph.v

@@ -28,9 +28,9 @@ Module Type Graph (O: UsualOrderedType)(S: FSetInterface.Sfun O).
 
   Parameter get_transpose: graph -> graph.
 
-  Parameter Equal: graph -> graph -> Prop.
+  (*Parameter Equal: graph -> graph -> Prop.
 
-  Parameter lt: graph -> graph -> Prop.
+  Parameter lt: graph -> graph -> Prop.*)
 
   Parameter empty_1: forall v,
     contains_vertex empty v = false.
@@ -95,7 +95,7 @@ Module Type Graph (O: UsualOrderedType)(S: FSetInterface.Sfun O).
   Parameter transpose_edges: forall g u v,
     contains_edge g u v = true <-> contains_edge (get_transpose g) v u = true.
 
-  Parameter Equal_equiv: Equivalence Equal.
+ (* Parameter Equal_equiv: Equivalence Equal.
 
   Parameter Equal_lt_l: forall g1 g2 g3,
     Equal g1 g2 ->
@@ -111,7 +111,7 @@ Module Type Graph (O: UsualOrderedType)(S: FSetInterface.Sfun O).
 
   Parameter lt_not_eq : forall x y : graph, lt x y -> ~ Equal x y.
 
-  Parameter compare : forall x y : graph, Compare lt Equal x y.
+  Parameter compare : forall x y : graph, Compare lt Equal x y.*)
 
   (*TODO: see if better way to define in interface*)
   (*A topological ordering is one where there are no edges going backward in the list and every vertex in the 

Helper.v

@@ -425,6 +425,22 @@ Qed.
 
 End MinMax.
 
+(*Definitions of a partition of a set and disjoint sets*)
+Module Partition(O:UsualOrderedType)(S: FSetInterface.Sfun O).
+
+(*Two sets are disjoint if there is no vertex in both*)
+Definition disjoint s s' :=
+  forall v, ~(S.In v s /\ S.In v s').
+
+(*For ease with graph/forests, we define the partition of all items satisfying a function (can be
+  \x y -> true to use all instances of type O.t). A partition is defined as a list of pairwise
+  disjoint sets such that every vertex satsifying f is in a set *)
+Definition partition {A: Type} (f: A -> O.t -> bool) (x: A) (l: list (S.t)) :=
+  (forall v, f x v = true -> exists s, InA S.Equal s l /\ S.In v s) /\
+  (forall s s', S.equal s s' = false -> InA S.Equal s l -> InA S.Equal s' l-> disjoint s s').
+
+End Partition.
+
 
 
 

Path.v

@@ -411,15 +411,7 @@ Proof.
     + eapply path_trans. apply p_start. apply G.transpose_edges. apply H0. apply IHpath. reflexivity.
 Qed.
 
-(*Maybe not the best place to put this - TODO: see about this*)
-(*A partition of a graph is a list of sets of vertices such that each vertex is in a set and for any two
-  nonequal sets, they have no vertices in common*)
-Definition disjoint s s' :=
-  forall v, ~(S.In v s /\ S.In v s').
-
-Definition partition {A: Type} (f: A -> O.t -> bool) (x: A) (l: list (S.t)) :=
-  (forall v, f x v = true -> exists s, InA S.Equal s l /\ S.In v s) /\
-  (forall s s', S.equal s s' = false -> InA S.Equal s l -> InA S.Equal s' l-> disjoint s s').
+