Implement proofs for edge labelled graphs and dioids

src/API.agda

@@ -1,6 +1,6 @@
 module API where
 
-open import Algebra
+open import Algebra.Graph
 open import Prelude
 
 empty : ∀ {A} -> Graph A

src/API/Theorems.agda

@@ -1,10 +1,10 @@
 module API.Theorems where
 
-open import Algebra
-open import Algebra.Theorems
+open import Algebra.Graph
+open import Algebra.Graph.Theorems
+open import Algebra.Graph.Reasoning
 open import API
 open import Prelude
-open import Reasoning
 
 -- vertices [x] == vertex x
 vertices-vertex : ∀ {A} {x : A} -> vertices [ x ] ≡ vertex x

src/Algebra/Dioid.agda

@@ -0,0 +1,41 @@
+module Algebra.Dioid where
+
+data Dioid : Set where
+  zero : Dioid
+  one  : Dioid
+  _+_  : Dioid -> Dioid -> Dioid
+  _*_  : Dioid -> Dioid -> Dioid
+
+infixl 4  _≡_
+infixl 8  _+_
+infixl 9  _*_
+
+-- Equational theory of dioids
+data _≡_ : (r s : Dioid) -> Set where
+    -- Equivalence relation
+    reflexivity  : ∀ {r     : Dioid} ->                   r ≡ r
+    symmetry     : ∀ {r s   : Dioid} -> r ≡ s ->          s ≡ r
+    transitivity : ∀ {r s t : Dioid} -> r ≡ s -> s ≡ t -> r ≡ t
+
+    -- Congruence
+    +left-congruence  : ∀ {r s t : Dioid} -> r ≡ s -> r + t ≡ s + t
+    +right-congruence : ∀ {r s t : Dioid} -> r ≡ s -> t + r ≡ t + s
+    *left-congruence  : ∀ {r s t : Dioid} -> r ≡ s -> r * t ≡ s * t
+    *right-congruence : ∀ {r s t : Dioid} -> r ≡ s -> t * r ≡ t * s
+
+    -- Axioms of +
+    +idempotence   : ∀ {r : Dioid}     -> r + r       ≡ r
+    +commutativity : ∀ {r s : Dioid}   -> r + s       ≡ s + r
+    +associativity : ∀ {r s t : Dioid} -> r + (s + t) ≡ (r + s) + t
+    +zero-identity : ∀ {r : Dioid}     -> r + zero    ≡ r
+
+    -- Axioms of *
+    *associativity  : ∀ {r s t : Dioid} -> r * (s * t) ≡ (r * s) * t
+    *left-zero      : ∀ {r : Dioid}     -> zero * r    ≡ zero
+    *right-zero     : ∀ {r : Dioid}     -> r * zero    ≡ zero
+    *left-identity  : ∀ {r : Dioid}     -> one * r     ≡ r
+    *right-identity : ∀ {r : Dioid}     -> r * one     ≡ r
+
+    -- Distributivity
+    left-distributivity  : ∀ {r s t : Dioid} -> r * (s + t) ≡ r * s + r * t
+    right-distributivity : ∀ {r s t : Dioid} -> (r + s) * t ≡ r * t + s * t

src/Algebra/Dioid/Bool.agda

@@ -0,0 +1,26 @@
+module Algebra.Dioid.Bool where
+
+open import Algebra.Dioid using (Dioid; zero; one; _+_; _*_)
+
+data Bool : Set where
+  true  : Bool
+  false : Bool
+
+data _≡_ : (x y : Bool) -> Set where
+  reflexivity  : ∀ {x     : Bool} ->                   x ≡ x
+  symmetry     : ∀ {x y   : Bool} -> x ≡ y ->          y ≡ x
+  transitivity : ∀ {x y z : Bool} -> x ≡ y -> y ≡ z -> x ≡ z
+
+_or_ : Bool -> Bool -> Bool
+false or false = false
+_ or _ = true
+
+_and_ : Bool -> Bool -> Bool
+true and true = true
+_ and _ = false
+
+boolDioid : Dioid -> Bool
+boolDioid zero = false
+boolDioid one  = true
+boolDioid (r + s) = boolDioid r or  boolDioid s
+boolDioid (r * s) = boolDioid r and boolDioid s

src/Algebra/Dioid/Bool/Theorems.agda

@@ -0,0 +1,101 @@
+module Algebra.Dioid.Bool.Theorems where
+
+open import Algebra.Dioid using (Dioid; zero; one; _+_; _*_)
+import Algebra.Dioid
+open import Algebra.Dioid.Bool
+
+or-left-congruence : ∀ {b c d : Bool} -> b ≡ c -> (b or d) ≡ (c or d)
+or-left-congruence {b} {.b} {d} reflexivity = reflexivity
+or-left-congruence {b} {c} {d} (symmetry eq) = symmetry (or-left-congruence eq)
+or-left-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (or-left-congruence eq) (or-left-congruence eq₁)
+
+or-right-congruence : ∀ {b c d : Bool} -> c ≡ d -> (b or c) ≡ (b or d)
+or-right-congruence {b} {c} {.c} reflexivity = reflexivity
+or-right-congruence {b} {c} {d} (symmetry eq) = symmetry (or-right-congruence eq)
+or-right-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (or-right-congruence eq) (or-right-congruence eq₁)
+
+and-left-congruence : ∀ {b c d : Bool} -> b ≡ c -> (b and d) ≡ (c and d)
+and-left-congruence {b} {.b} {d} reflexivity = reflexivity
+and-left-congruence {b} {c} {d} (symmetry eq) = symmetry (and-left-congruence eq)
+and-left-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (and-left-congruence eq) (and-left-congruence eq₁)
+
+and-right-congruence : ∀ {b c d : Bool} -> c ≡ d -> (b and c) ≡ (b and d)
+and-right-congruence {b} {c} {.c} reflexivity = reflexivity
+and-right-congruence {b} {c} {d} (symmetry eq) = symmetry (and-right-congruence eq)
+and-right-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (and-right-congruence eq) (and-right-congruence eq₁)
+
+or-idempotence : ∀ {b : Bool} -> (b or b) ≡ b
+or-idempotence {true} = reflexivity
+or-idempotence {false} = reflexivity
+
+or-commutativity : ∀ {b c : Bool} -> (b or c) ≡ (c or b)
+or-commutativity {true} {true} = reflexivity
+or-commutativity {true} {false} = reflexivity
+or-commutativity {false} {true} = reflexivity
+or-commutativity {false} {false} = reflexivity
+
+or-associativity : ∀ {b c d : Bool} -> (b or (c or d)) ≡ ((b or c) or d)
+or-associativity {true} {c} {d} = reflexivity
+or-associativity {false} {true} {d} = reflexivity
+or-associativity {false} {false} {true} = reflexivity
+or-associativity {false} {false} {false} = reflexivity
+
+or-false-identity : ∀ {b : Bool} -> (b or false) ≡ b
+or-false-identity {true} = reflexivity
+or-false-identity {false} = reflexivity
+
+and-associativity : ∀ {b c d : Bool} -> (b and (c and d)) ≡ ((b and c) and d)
+and-associativity {true} {true} {true} = reflexivity
+and-associativity {true} {true} {false} = reflexivity
+and-associativity {true} {false} {d} = reflexivity
+and-associativity {false} {c} {d} = reflexivity
+
+and-left-false : ∀ {b : Bool} -> (false and b) ≡ false
+and-left-false {b} = reflexivity
+
+and-right-false : ∀ {b : Bool} -> (b and false) ≡ false
+and-right-false {true} = reflexivity
+and-right-false {false} = reflexivity
+
+and-left-true : ∀ {b : Bool} -> (true and b) ≡ b
+and-left-true {true} = reflexivity
+and-left-true {false} = reflexivity
+
+and-right-true : ∀ {b : Bool} -> (b and true) ≡ b
+and-right-true {true} = reflexivity
+and-right-true {false} = reflexivity
+
+left-distributivity : ∀ {b c d : Bool} -> (b and (c or d)) ≡ ((b and c) or (b and d))
+left-distributivity {true} {true} {d} = reflexivity
+left-distributivity {true} {false} {true} = reflexivity
+left-distributivity {true} {false} {false} = reflexivity
+left-distributivity {false} {c} {d} = reflexivity
+
+right-distributivity : ∀ {b c d : Bool} -> ((b or c) and d) ≡ ((b and d) or (c and d))
+right-distributivity {true} {true} {true} = reflexivity
+right-distributivity {true} {true} {false} = reflexivity
+right-distributivity {true} {false} {true} = reflexivity
+right-distributivity {true} {false} {false} = reflexivity
+right-distributivity {false} {true} {true} = reflexivity
+right-distributivity {false} {true} {false} = reflexivity
+right-distributivity {false} {false} {d} = reflexivity
+
+boolDioidLawful : ∀ {r s : Dioid} -> r Algebra.Dioid.≡ s -> boolDioid r ≡ boolDioid s
+boolDioidLawful {r} {.r} Algebra.Dioid.reflexivity = reflexivity
+boolDioidLawful {r} {s} (Algebra.Dioid.symmetry eq) = symmetry (boolDioidLawful eq)
+boolDioidLawful {r} {s} (Algebra.Dioid.transitivity eq eq₁) = transitivity (boolDioidLawful eq) (boolDioidLawful eq₁)
+boolDioidLawful {.(_ + _)} {.(_ + _)} (Algebra.Dioid.+left-congruence eq) = or-left-congruence (boolDioidLawful eq)
+boolDioidLawful {.(_ + _)} {.(_ + _)} (Algebra.Dioid.+right-congruence eq) = or-right-congruence (boolDioidLawful eq)
+boolDioidLawful {.(_ * _)} {.(_ * _)} (Algebra.Dioid.*left-congruence eq) = and-left-congruence (boolDioidLawful eq)
+boolDioidLawful {.(_ * _)} {.(_ * _)} (Algebra.Dioid.*right-congruence eq) = and-right-congruence (boolDioidLawful eq)
+boolDioidLawful {.(s + s)} {s} Algebra.Dioid.+idempotence = or-idempotence
+boolDioidLawful {.(_ + _)} {.(_ + _)} Algebra.Dioid.+commutativity = or-commutativity
+boolDioidLawful {.(_ + (_ + _))} {.(_ + _ + _)} Algebra.Dioid.+associativity = or-associativity
+boolDioidLawful {.(s + zero)} {s} Algebra.Dioid.+zero-identity = or-false-identity
+boolDioidLawful {.(_ * (_ * _))} {.(_ * _ * _)} Algebra.Dioid.*associativity = and-associativity
+boolDioidLawful {.(zero * _)} {.zero} Algebra.Dioid.*left-zero = reflexivity
+boolDioidLawful {.(_ * zero)} {.zero} Algebra.Dioid.*right-zero = and-right-false
+boolDioidLawful {.(one * s)} {s} Algebra.Dioid.*left-identity = and-left-true
+boolDioidLawful {.(s * one)} {s} Algebra.Dioid.*right-identity = and-right-true
+boolDioidLawful {.(_ * (_ + _))} {.(_ * _ + _ * _)} Algebra.Dioid.left-distributivity = left-distributivity
+boolDioidLawful {.((_ + _) * _)} {.(_ * _ + _ * _)} Algebra.Dioid.right-distributivity = right-distributivity

src/Algebra/Dioid/Reasoning.agda

@@ -0,0 +1,40 @@
+module Algebra.Dioid.Reasoning where
+
+open import Algebra.Dioid
+
+-- Standard syntax sugar for writing equational proofs
+infix 4 _≈_
+data _≈_ (x y : Dioid) : Set where
+    prove : x ≡ y -> x ≈ y
+
+infix 1 begin_
+begin_ : ∀ {x y : Dioid} -> x ≈ y -> x ≡ y
+begin prove p = p
+
+infixr 2 _≡⟨_⟩_
+_≡⟨_⟩_ : ∀ (x : Dioid) {y z : Dioid} -> x ≡ y -> y ≈ z -> x ≈ z
+_ ≡⟨ p ⟩ prove q = prove (transitivity p q)
+
+infix 3 _∎
+_∎ : ∀ (x : Dioid) -> x ≈ x
+_∎ _ = prove reflexivity
+
+infixl 8 _>>_
+_>>_ : ∀ {x y z : Dioid} -> x ≡ y -> y ≡ z -> x ≡ z
+_>>_ = transitivity
+
+data BinaryOperator : Set where
+  +op : BinaryOperator
+  *op : BinaryOperator
+
+apply : BinaryOperator -> Dioid -> Dioid -> Dioid
+apply +op a b = a + b
+apply *op a b = a * b
+
+L : ∀ {op : BinaryOperator} -> ∀ {x y z : Dioid} -> x ≡ y -> apply op x z ≡ apply op y z
+L {+op} {x} {y} {z} eq = +left-congruence {x} {y} {z} eq
+L {*op} {x} {y} {z} eq = *left-congruence {x} {y} {z} eq
+
+R : ∀ {op : BinaryOperator} -> ∀ {x y z : Dioid} -> x ≡ y -> apply op z x ≡ apply op z y
+R {+op} {x} {y} {z} eq = +right-congruence {x} {y} {z} eq
+R {*op} {x} {y} {z} eq = *right-congruence {x} {y} {z} eq

src/Algebra/Dioid/ShortestDistance.agda

@@ -0,0 +1,41 @@
+module Algebra.Dioid.ShortestDistance where
+
+module Nat where
+  data Nat : Set where
+    zero : Nat
+    succ : Nat -> Nat
+
+  min : Nat -> Nat -> Nat
+  min zero n = n
+  min n zero = n
+  min (succ n) (succ m) = min n m
+
+  _+_ : Nat -> Nat -> Nat
+  zero + n = n
+  n + zero = n
+  (succ n) + m = succ (n + m)
+
+open import Algebra.Dioid using (Dioid; zero; one; _+_; _*_)
+
+data ShortestDistance : Set where
+  Distance : Nat.Nat -> ShortestDistance
+  Unreachable : ShortestDistance
+
+data _≡_ : (x y : ShortestDistance) -> Set where
+  reflexivity  : ∀ {x     : ShortestDistance} ->                   x ≡ x
+  symmetry     : ∀ {x y   : ShortestDistance} -> x ≡ y ->          y ≡ x
+  transitivity : ∀ {x y z : ShortestDistance} -> x ≡ y -> y ≡ z -> x ≡ z
+
+shortestDistanceDioid : Dioid -> ShortestDistance
+shortestDistanceDioid zero = Unreachable
+shortestDistanceDioid one  = Distance Nat.zero
+shortestDistanceDioid (r + s) with shortestDistanceDioid r
+... | Unreachable = shortestDistanceDioid s
+... | Distance n with shortestDistanceDioid s
+... | Unreachable = Distance n
+... | Distance m = Distance (Nat.min n m)
+shortestDistanceDioid (r * s) with shortestDistanceDioid r
+... | Unreachable = Unreachable
+... | Distance n with shortestDistanceDioid s
+... | Unreachable = Unreachable
+... | Distance m = Distance (n Nat.+ m)

src/Algebra/Dioid/Theorems.agda

@@ -0,0 +1,12 @@
+module Algebra.Dioid.Theorems where
+
+open import Algebra.Dioid
+open import Algebra.Dioid.Reasoning
+
+left-zero-identity : ∀ {r : Dioid} -> (zero + r) ≡ r
+left-zero-identity {r} =
+  begin
+    zero + r ≡⟨ +commutativity ⟩
+    r + zero ≡⟨ +zero-identity ⟩
+    r
+  ∎

src/Algebra.agda → src/Algebra/Graph.agda

@@ -1,4 +1,4 @@
-module Algebra where
+module Algebra.Graph where
 
 -- Core graph construction primitives
 data Graph (A : Set) : Set where

src/Reasoning.agda → src/Algebra/Graph/Reasoning.agda

@@ -1,6 +1,6 @@
-module Reasoning where
+module Algebra.Graph.Reasoning where
 
-open import Algebra
+open import Algebra.Graph
 
 -- Standard syntax sugar for writing equational proofs
 infix 4 _≈_

src/Algebra/Theorems.agda → src/Algebra/Graph/Theorems.agda

@@ -1,7 +1,7 @@
-module Algebra.Theorems where
+module Algebra.Graph.Theorems where
 
-open import Algebra
-open import Reasoning
+open import Algebra.Graph
+open import Algebra.Graph.Reasoning
 
 +pre-idempotence : ∀ {A} {x : Graph A} -> x + x + ε ≡ x
 +pre-idempotence {_} {x} =

src/Algebra/LabelledGraph.agda

@@ -0,0 +1,46 @@
+module Algebra.LabelledGraph where
+
+open import Algebra.Dioid using (Dioid)
+import Algebra.Dioid as Dioid
+
+-- Core graph construction primitives
+data LabelledGraph (A : Set) : Set where
+    ε   : LabelledGraph A      -- Empty graph
+    v   : A -> LabelledGraph A -- Graph comprising a single vertex
+    _-[_]>_ : LabelledGraph A -> Dioid -> LabelledGraph A -> LabelledGraph A
+                               -- Connect two graphs
+
+_+_ : ∀ {A} -> LabelledGraph A -> LabelledGraph A -> LabelledGraph A
+g + h = g -[ Dioid.zero ]> h
+
+_*_ : ∀ {A} -> LabelledGraph A -> LabelledGraph A -> LabelledGraph A
+g * h = g -[ Dioid.one ]> h
+
+infixl 4  _≡_
+infixl 8  _+_
+infixl 9  _*_
+infixl 9  _-[_]>_
+infix  10 _⊆_
+
+-- Equational theory of graphs
+data _≡_ {A} : (x y : LabelledGraph A) -> Set where
+    -- Equivalence relation
+    reflexivity  : ∀ {x     : LabelledGraph A} ->                   x ≡ x
+    symmetry     : ∀ {x y   : LabelledGraph A} -> x ≡ y ->          y ≡ x
+    transitivity : ∀ {x y z : LabelledGraph A} -> x ≡ y -> y ≡ z -> x ≡ z
+
+    -- Congruence
+    left-congruence  : ∀ {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> x -[ r ]> z ≡ y -[ r ]> z
+    right-congruence : ∀ {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> z -[ r ]> x ≡ z -[ r ]> y
+
+    -- Axioms
+    zero-commutativity  : ∀ {x y : LabelledGraph A} -> x + y ≡ y + x
+    left-identity       : ∀ {x     : LabelledGraph A} {r   : Dioid} -> ε -[ r ]> x ≡ x
+    right-identity      : ∀ {x     : LabelledGraph A} {r   : Dioid} -> x -[ r ]> ε ≡ x
+    left-decomposition  : ∀ {x y z : LabelledGraph A} {r s : Dioid} -> x -[ r ]> (y -[ s ]> z) ≡ (x -[ r ]> y) + (x -[ r ]> z) + (y -[ s ]> z)
+    right-decomposition : ∀ {x y z : LabelledGraph A} {r s : Dioid} -> (x -[ r ]> y) -[ s ]> z ≡ (x -[ r ]> y) + (x -[ s ]> z) + (y -[ s ]> z)
+    label-addition      : ∀ {x y   : LabelledGraph A} {r s : Dioid} -> (x -[ r ]> y) + (x -[ s ]> y) ≡ (x -[ r Dioid.+ s ]> y)
+
+-- Subgraph relation
+_⊆_ : ∀ {A} -> LabelledGraph A -> LabelledGraph A -> Set
+x ⊆ y = x + y ≡ y

src/Algebra/LabelledGraph/Reasoning.agda

@@ -0,0 +1,31 @@
+module Algebra.LabelledGraph.Reasoning where
+
+open import Algebra.Dioid using (Dioid)
+open import Algebra.LabelledGraph
+
+-- Standard syntax sugar for writing equational proofs
+infix 4 _≈_
+data _≈_ {A} (x y : LabelledGraph A) : Set where
+    prove : x ≡ y -> x ≈ y
+
+infix 1 begin_
+begin_ : ∀ {A} {x y : LabelledGraph A} -> x ≈ y -> x ≡ y
+begin prove p = p
+
+infixr 2 _≡⟨_⟩_
+_≡⟨_⟩_ : ∀ {A} (x : LabelledGraph A) {y z : LabelledGraph A} -> x ≡ y -> y ≈ z -> x ≈ z
+_ ≡⟨ p ⟩ prove q = prove (transitivity p q)
+
+infix 3 _∎
+_∎ : ∀ {A} (x : LabelledGraph A) -> x ≈ x
+_∎ _ = prove reflexivity
+
+infixl 8 _>>_
+_>>_ : ∀ {A} {x y z : LabelledGraph A} -> x ≡ y -> y ≡ z -> x ≡ z
+_>>_ = transitivity
+
+L : ∀ {A} {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> x -[ r ]> z ≡ y -[ r ]> z
+L = left-congruence
+
+R : ∀ {A} {x y z : LabelledGraph A} {r : Dioid} -> x ≡ y -> z -[ r ]> x ≡ z -[ r ]> y
+R = right-congruence