Generalize graph, rename old def to finite graph

.gitignore

@@ -22,3 +22,5 @@ target
 elba.lock
 build
 compare
+*.ttc
+*.ttm

idris2/Free/Graph.idr

@@ -22,6 +22,6 @@ edgeTarget : {0 i : vertices g} -> {j : vertices g} -> Edge g i j -> vertices g
 edgeTarget _ = j
 
 -- data TriangleVertices = One | Two | Three
--- 
+--
 -- triangle : Graph
 -- triangle = MkGraph TriangleVertices [(One, Two), (Two, Three), (Three, One)]

src/CoLimits/Pushout.lidr

@@ -33,10 +33,28 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >
 > data PushoutIndexObject = X | Y | Z
 >
+> XnotY : X = Y -> Void
+> XnotY Refl impossible
+>
+> XnotZ : X = Z -> Void
+> XnotZ Refl impossible
+>
+> YnotZ : Y = Z -> Void
+> YnotZ Refl impossible
+>
+> DecEq PushoutIndexObject where
+>   decEq X X = Yes Refl
+>   decEq X Y = No XnotY
+>   decEq X Z = No XnotZ
+>   decEq Y X = No (negEqSym XnotY)
+>   decEq Y Y = Yes Refl
+>   decEq Y Z = No YnotZ
+>   decEq Z X = No (negEqSym XnotZ)
+>   decEq Z Y = No (negEqSym YnotZ)
+>   decEq Z Z = Yes Refl
+>
 > PushoutIndexGraph : Graph
-> PushoutIndexGraph = MkGraph
->   PushoutIndexObject
->   [(Z, X), (Z, Y)]
+> PushoutIndexGraph = edgeList [(Z, X), (Z, Y)]
 >
 > PushoutIndexCategory : Category
 > PushoutIndexCategory = pathCategory PushoutIndexGraph

src/Free/FreeFunctor.lidr

@@ -23,7 +23,6 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >
 > import Basic.Category
 > import Basic.Functor
-> import Data.Vect
 > import Free.Graph
 > import Free.Path
 > import Free.PathCategory
@@ -34,7 +33,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 > record GraphEmbedding (g : Graph) (cat : Category) where
 >   constructor MkGraphEmbedding
 >   mapVertices : vertices g -> obj cat
->   mapEdges    : (i, j : vertices g) -> Edge g i j -> mor cat (mapVertices i) (mapVertices j)
+>   mapEdges    : (i, j : vertices g) -> edges g i j -> mor cat (mapVertices i) (mapVertices j)
 >
 > foldPath :
 >      (g : Graph)

src/Free/Graph.lidr

@@ -29,18 +29,17 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 > record Graph where
 >   constructor MkGraph
 >   vertices : Type
->   edges    : Vect n (vertices, vertices)
+>   edges    : vertices -> vertices -> Type
 >
-> Edge : (g : Graph) -> (i, j : vertices g) -> Type
-> Edge g i j = Elem (i, j) (edges g)
+> decEqFilter : DecEq a => (v : a) -> Vect n a -> (k ** Vect k (e ** e = v))
+> decEqFilter v [] = (0 ** [])
+> decEqFilter v (x :: xs) with (decEq x v)
+>   decEqFilter v (x :: xs) | Yes prf = let (i ** vs) = decEqFilter v xs in (S i ** (x ** prf) :: vs)
+>   decEqFilter v (x :: xs) | No cont = decEqFilter v xs
 >
-> edgeOrigin : {g : Graph} -> Edge g i j -> vertices g
-> edgeOrigin {i} _ = i
->
-> edgeTarget : {g : Graph} -> Edge g i j -> vertices g
-> edgeTarget {j} _ = j
-
-data TriangleVertices = One | Two | Three
-
-triangle : Graph
-triangle = MkGraph TriangleVertices [(One, Two), (Two, Three), (Three, One)]
+> edgeList : DecEq vertices
+>         => (edges : Vect n (vertices, vertices))
+>         -> Graph
+> edgeList edges = MkGraph
+>   vertices
+>   (\v1, v2 => Fin $ fst $ decEqFilter (v1, v2) edges)

src/Free/Path.lidr

@@ -21,26 +21,17 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 
 > module Free.Path
 >
-> import Data.List
+> import Data.Vect
 > import Free.Graph
 >
 > %access public export
 > %default total
 >
 > data Path : (g : Graph) -> vertices g -> vertices g -> Type where
 >   Nil  : Path g i i
->   (::) : (a : Edge g i j) -> Path g j k -> Path g i k
-
-nullPath : Path Graph.triangle One One
-nullPath = Nil
-
-oneToThree : Path Graph.triangle One Three
-oneToThree = [Here, There Here]
-
-oneToThree' : Path Graph.triangle One Three
-oneToThree' = Here :: There Here :: Nil
-
-> edgeToPath : {g : Graph} -> (a : Edge g i j) -> Path g (edgeOrigin a) (edgeTarget a)
+>   (::) : edges g i j -> Path g j k -> Path g i k
+>
+> edgeToPath : {g : Graph} -> edges g i j -> Path g i j
 > edgeToPath a = [a]
 >
 > joinPath : Path g i j -> Path g j k -> Path g i k
@@ -58,3 +49,52 @@ oneToThree' = Here :: There Here :: Nil
 >   -> joinPath p (joinPath q r) = joinPath (joinPath p q) r
 > joinPathAssoc Nil q r = Refl
 > joinPathAssoc (x :: xs) q r = cong $ joinPathAssoc xs q r
+>
+> data EdgeListPath : (edges : Vect n (vertices, vertices)) -> vertices -> vertices -> Type where
+>   Empty : EdgeListPath edges i i
+>   Cons  : Elem (i, j) edges -> EdgeListPath edges j k -> EdgeListPath edges i k
+>
+> filterElemWhichIsHere : DecEq t => (x : t) -> (l : Vect _ t) -> (k : Nat ** fst $ decEqFilter x (x :: l) = S k)
+> filterElemWhichIsHere x [] with (decEq x x)
+>   filterElemWhichIsHere x [] | Yes Refl  = (0 ** Refl)
+>   filterElemWhichIsHere x [] | No contra = void $ contra Refl
+> filterElemWhichIsHere x xs with (decEq x x)
+>   filterElemWhichIsHere x xs | Yes Refl with (decEqFilter x xs)
+>     filterElemWhichIsHere x xs | Yes Refl | (i ** vs) = (i ** Refl)
+>   filterElemWhichIsHere x xs | No contra = void $ contra Refl
+>
+> countOccurrence : DecEq vertices
+>               => {i, j : vertices}
+>               -> (edges : Vect n (vertices, vertices))
+>               -> Elem (i, j) edges
+>               -> Fin $ fst $ decEqFilter (i, j) edges
+> countOccurrence {i} {j} ((i, j) :: xs) Here with (decEq (i,j) (i,j))
+>   countOccurrence {i} {j} ((i, j) :: xs) Here | Yes Refl with (decEqFilter (i, j) xs)
+>     countOccurrence {i} {j} ((i, j) :: xs) Here | Yes Refl | (k ** vs) = 0
+>   countOccurrence {i} {j} ((i, j) :: xs) Here | No contra = void $ contra Refl
+> countOccurrence {i} {j} ((k, l) :: xs) (There e) with (decEq (i, j) (k, l))
+>   countOccurrence {i} {j} ((i, j) :: xs) (There e) | Yes Refl with (decEq (i, j) (i, j))
+>     countOccurrence {i} {j} ((i, j) :: xs) (There e) | Yes Refl | Yes Refl with (decEqFilter (i, j) xs) proof prf
+>       countOccurrence {i} {j} ((i, j) :: xs) (There e) | Yes Refl | Yes Refl | (k ** vs)
+>         = FS $ rewrite cong {f=DPair.fst} prf in countOccurrence {i} {j} xs e
+>     countOccurrence {i} {j} ((i, j) :: xs) (There e) | Yes Refl | No contra = void $ contra Refl
+>   countOccurrence {i} {j} ((k, l) :: xs) (There e) | No contra with (decEqFilter (i, j) xs) proof prf
+>     countOccurrence {i} {j} ((k, l) :: xs) (There e) | No contra | (m ** vs) with (decEq k i)
+>       countOccurrence {i} {j} ((i, l) :: xs) (There e) | No contra | (m ** vs) | Yes Refl with (decEq l j)
+>         countOccurrence {i} {j} ((i, j) :: xs) (There e) | No contra | (m ** vs) | Yes Refl | Yes Refl
+>           = void $ contra Refl
+>         countOccurrence {i} {j} ((i, l) :: xs) (There e) | No contra | (m ** vs) | Yes Refl | No contra'
+>           = countOccurrence {i} {j} xs e
+>       countOccurrence {i} {j} ((k, l) :: xs) (There e) | No contra | (m ** vs) | No contra' with (decEq l j)
+>         countOccurrence {i} {j} ((k, j) :: xs) (There e) | No contra | (m ** vs) | No contra' | Yes Refl
+>           = countOccurrence {i} {j} xs e
+>         countOccurrence {i} {j} ((k, l) :: xs) (There e) | No contra | (m ** vs) | No contra' | No contra''
+>           = countOccurrence {i} {j} xs e
+>
+> edgeListPath : DecEq vertices
+>             => {edges : Vect n (vertices, vertices)}
+>             -> {i, j : vertices}
+>             -> EdgeListPath edges i j
+>             -> Path (edgeList edges) i j
+> edgeListPath Empty           = Nil
+> edgeListPath (Cons elem elp) = (countOccurrence edges elem) :: (edgeListPath elp)