Play with Idris to prove correct way of building paths in directed graph and proof of properties of the paths

GraphPath.idr

module Path

import Data.Vect

||| Graph defined by hops vector
Ways : Nat -> Type -> Type
Ways n a = Vect n (a, a)

||| Helper that points which transaction ways we need to use to traverse the given path
data PathElem : (ways : Ways k a) -> (begin : a) -> (path : Vect n a) -> (end : a) -> Type where
  PathHere  : PathElem ways p [] p
  PathThere : (hopPrf : Elem (begin, p) ways) -> (reminderPath: PathElem ways p path end) -> PathElem ways begin (p :: path) end

||| Show that if we have a proof that begin and end are distinct the empty PathElem is absurd
contraEndPath : (contra : (begin = end) -> Void) -> PathElem ways begin [] end -> Void
contraEndPath contra PathHere = contra Refl

||| States that if the path is absurd then the extention of the path is also a absurd
noNextPathScourge : (contra : PathElem ways x xs end -> Void) -> PathElem ways begin (x :: xs) end -> Void
noNextPathScourge contra (PathThere hopPrf reminderPath) = contra reminderPath

||| Show that if we have proof that there is no hop in ways, so path with that hop is a absurd
isPathContraWithoutHop : (contra : Elem (begin, x) ways -> Void) -> PathElem ways begin (x :: xs) end -> Void
isPathContraWithoutHop contra (PathThere hopPrf reminderPath) = contra hopPrf

||| Construct proof that the path is located in the ways
isPath : DecEq a
  => (ways : Ways k a)
  -> (begin : a)
  -> (path : Vect n a)
  -> (end : a)
  -> Dec (PathElem ways begin path end)
isPath ways begin [] end with (decEq begin end)
  isPath ways end [] end | (Yes Refl) = Yes PathHere
  isPath ways begin [] end | (No contra) = No (contraEndPath contra)
isPath ways begin (x :: xs) end with (isElem (begin, x) ways)
  isPath ways begin (x :: xs) end | (Yes prfHop) = case isPath ways x xs end of
    (Yes reminderPath) => Yes (PathThere prfHop reminderPath)
    (No contra) => No (noNextPathScourge contra)
  isPath ways begin (x :: xs) end | (No contra) = No (isPathContraWithoutHop contra)

||| States that if we have two paths then we can glue them
gluePaths :
     (PathElem ways begin path1 p)
  -> (PathElem ways p path2 end)
  -> (PathElem ways begin (path1 ++ path2) end)
gluePaths PathHere y = y
gluePaths (PathThere hopPrf reminderPath) y = PathThere hopPrf (gluePaths reminderPath y)

||| Debug graph
graph : Ways 6 Nat
graph = [(1, 2), (1, 3), (2, 1), (2, 4), (3, 4), (3, 2)]

||| Debug path1, should be Yes
path1 : (graph : Ways n Nat) -> Dec (PathElem graph 1 [2, 4] 4)
path1 gr = isPath gr 1 [2, 4] 4

||| Debug path1, should be Yes
path2 : (graph : Ways n Nat) -> Dec (PathElem graph 1 [3, 2, 1, 3, 4] 4)
path2 gr = isPath gr 1 [3, 2, 1, 3, 4] 4

||| Debug path3, should be No
path3 : (graph : Ways n Nat) -> Dec (PathElem graph 1 [3, 2, 1, 4] 4)
path3 gr = isPath gr 1 [3, 2, 1, 4] 4