diff --git a/src/API.agda b/src/API.agda index a17b9a7..659f9fe 100644 --- a/src/API.agda +++ b/src/API.agda @@ -1,6 +1,6 @@ module API where -open import Algebra +open import Algebra.Graph open import Prelude empty : ∀ {A} -> Graph A diff --git a/src/API/Theorems.agda b/src/API/Theorems.agda index 520acc8..1d85d66 100644 --- a/src/API/Theorems.agda +++ b/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 diff --git a/src/Algebra/Dioid.agda b/src/Algebra/Dioid.agda new file mode 100644 index 0000000..98b72a3 --- /dev/null +++ b/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 diff --git a/src/Algebra/Dioid/Bool.agda b/src/Algebra/Dioid/Bool.agda new file mode 100644 index 0000000..244aece --- /dev/null +++ b/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 diff --git a/src/Algebra/Dioid/Bool/Theorems.agda b/src/Algebra/Dioid/Bool/Theorems.agda new file mode 100644 index 0000000..8b39b97 --- /dev/null +++ b/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 diff --git a/src/Algebra/Dioid/Reasoning.agda b/src/Algebra/Dioid/Reasoning.agda new file mode 100644 index 0000000..32d61b2 --- /dev/null +++ b/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 diff --git a/src/Algebra/Dioid/ShortestDistance.agda b/src/Algebra/Dioid/ShortestDistance.agda new file mode 100644 index 0000000..e391ce3 --- /dev/null +++ b/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) diff --git a/src/Algebra/Dioid/Theorems.agda b/src/Algebra/Dioid/Theorems.agda new file mode 100644 index 0000000..f5b6536 --- /dev/null +++ b/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 + ∎ diff --git a/src/Algebra.agda b/src/Algebra/Graph.agda similarity index 98% rename from src/Algebra.agda rename to src/Algebra/Graph.agda index 231a436..c40cddc 100644 --- a/src/Algebra.agda +++ b/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 diff --git a/src/Reasoning.agda b/src/Algebra/Graph/Reasoning.agda similarity index 95% rename from src/Reasoning.agda rename to src/Algebra/Graph/Reasoning.agda index 5a051d2..2486602 100644 --- a/src/Reasoning.agda +++ b/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 _≈_ diff --git a/src/Algebra/Theorems.agda b/src/Algebra/Graph/Theorems.agda similarity index 98% rename from src/Algebra/Theorems.agda rename to src/Algebra/Graph/Theorems.agda index 1dbdaea..3d157cd 100644 --- a/src/Algebra/Theorems.agda +++ b/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} = diff --git a/src/Algebra/LabelledGraph.agda b/src/Algebra/LabelledGraph.agda new file mode 100644 index 0000000..32fdfdb --- /dev/null +++ b/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 diff --git a/src/Algebra/LabelledGraph/Reasoning.agda b/src/Algebra/LabelledGraph/Reasoning.agda new file mode 100644 index 0000000..58385e2 --- /dev/null +++ b/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 diff --git a/src/Algebra/LabelledGraph/Theorems.agda b/src/Algebra/LabelledGraph/Theorems.agda new file mode 100644 index 0000000..d1f4345 --- /dev/null +++ b/src/Algebra/LabelledGraph/Theorems.agda @@ -0,0 +1,116 @@ +module Algebra.LabelledGraph.Theorems where + +open import Algebra.LabelledGraph +open import Algebra.LabelledGraph.Reasoning +open import Algebra.Dioid using (Dioid) +import Algebra.Dioid as Dioid +open import Algebra.Graph using (Graph) +import Algebra.Graph as Graph +import Algebra.Dioid.Bool as Bool + + +associativity : ∀ {A} {a b c : LabelledGraph A} {r : Dioid} -> (a -[ r ]> b) -[ r ]> c ≡ a -[ r ]> (b -[ r ]> c) +associativity {_} {a} {b} {c} {r} = right-decomposition >> symmetry left-decomposition + +absorption : ∀ {A} {a b : LabelledGraph A} {r : Dioid} -> a -[ r ]> b ≡ a -[ r ]> b + a + b +absorption {_} {a} {b} {r} = + begin + (a -[ r ]> b) ≡⟨ symmetry right-identity ⟩ + (a -[ r ]> b) -[ Dioid.zero ]> ε ≡⟨ right-decomposition ⟩ + (a -[ r ]> b) + (a + ε) + (b + ε) ≡⟨ L (R right-identity ) ⟩ + (a -[ r ]> b) + a + (b + ε) ≡⟨ R right-identity ⟩ + (a -[ r ]> b) + a + b + ∎ + +idempotence : ∀ {A} {a : LabelledGraph A} -> a ≡ a + a +idempotence {_} {a} = + begin + a ≡⟨ symmetry right-identity ⟩ + a + ε ≡⟨ symmetry right-identity ⟩ + a + ε + ε ≡⟨ right-decomposition ⟩ + (a + ε) + (a + ε) + (ε + ε) ≡⟨ right-congruence left-identity ⟩ + (a + ε) + (a + ε) + ε ≡⟨ right-identity ⟩ + (a + ε) + (a + ε) ≡⟨ right-congruence right-identity ⟩ + (a + ε) + a ≡⟨ left-congruence right-identity ⟩ + a + a + ∎ + +right-distributivity : ∀ {A} {a b c : LabelledGraph A} {r : Dioid} -> (a + b) -[ r ]> c ≡ a -[ r ]> c + b -[ r ]> c +right-distributivity {_} {a} {b} {c} {r} = + begin + (a + b) -[ r ]> c ≡⟨ right-decomposition ⟩ + ((a + b) + (a -[ r ]> c)) + (b -[ r ]> c) ≡⟨ L (R absorption) ⟩ + (a + b) + ((a -[ r ]> c) + a + c) + (b -[ r ]> c) ≡⟨ R absorption ⟩ + (a + b) + ((a -[ r ]> c) + a + c) + ((b -[ r ]> c) + b + c) ≡⟨ L (associativity)⟩ + a + (b + ((a -[ r ]> c) + a + c)) + ((b -[ r ]> c) + b + c) ≡⟨ L (R zero-commutativity)⟩ + a + (((a -[ r ]> c) + a + c) + b) + ((b -[ r ]> c) + b + c) ≡⟨ associativity ⟩ + a + ((((a -[ r ]> c) + a + c) + b) + ((b -[ r ]> c) + b + c)) ≡⟨ R (associativity) ⟩ + a + (((a -[ r ]> c) + a + c) + (b + ((b -[ r ]> c) + b + c))) ≡⟨ R (R zero-commutativity)⟩ + a + (((a -[ r ]> c) + a + c) + (((b -[ r ]> c) + b + c) + b)) ≡⟨ R (R associativity) ⟩ + a + (((a -[ r ]> c) + a + c) + ((b -[ r ]> c) + b + (c + b))) ≡⟨ R (R (R zero-commutativity)) ⟩ + a + (((a -[ r ]> c) + a + c) + ((b -[ r ]> c) + b + (b + c))) ≡⟨ R (R (symmetry associativity)) ⟩ + a + (((a -[ r ]> c) + a + c) + ((b -[ r ]> c) + b + b + c)) ≡⟨ R (R (L associativity)) ⟩ + a + (((a -[ r ]> c) + a + c) + ((b -[ r ]> c) + (b + b) + c)) ≡⟨ R (R (L (R (symmetry idempotence))))⟩ + a + (((a -[ r ]> c) + a + c) + ((b -[ r ]> c) + b + c)) ≡⟨ R (R (symmetry absorption)) ⟩ + a + (((a -[ r ]> c) + a + c) + (b -[ r ]> c)) ≡⟨ symmetry associativity ⟩ + a + ((a -[ r ]> c) + a + c) + (b -[ r ]> c) ≡⟨ L zero-commutativity ⟩ + ((a -[ r ]> c) + a + c) + a + (b -[ r ]> c) ≡⟨ L associativity ⟩ + ((a -[ r ]> c) + a + (c + a)) + (b -[ r ]> c) ≡⟨ L (R zero-commutativity)⟩ + ((a -[ r ]> c) + a + (a + c)) + (b -[ r ]> c) ≡⟨ L (symmetry associativity)⟩ + ((a -[ r ]> c) + a + a + c) + (b -[ r ]> c) ≡⟨ L (L associativity)⟩ + ((a -[ r ]> c) + (a + a) + c) + (b -[ r ]> c) ≡⟨ L (L (R (symmetry idempotence))) ⟩ + ((a -[ r ]> c) + a + c) + (b -[ r ]> c) ≡⟨ L (symmetry absorption) ⟩ + (a -[ r ]> c) + (b -[ r ]> c) + ∎ + +left-distributivity : ∀ {A} {a b c : LabelledGraph A} {r : Dioid} -> a -[ r ]> (b + c) ≡ a -[ r ]> b + a -[ r ]> c +left-distributivity {_} {a} {b} {c} {r} = + begin + a -[ r ]> (b + c) ≡⟨ left-decomposition ⟩ + a -[ r ]> b + a -[ r ]> c + (b + c) ≡⟨ symmetry associativity ⟩ + a -[ r ]> b + a -[ r ]> c + b + c ≡⟨ L associativity ⟩ + a -[ r ]> b + (a -[ r ]> c + b) + c ≡⟨ L (R zero-commutativity) ⟩ + a -[ r ]> b + (b + a -[ r ]> c) + c ≡⟨ L (symmetry associativity) ⟩ + a -[ r ]> b + b + a -[ r ]> c + c ≡⟨ L (L (L absorption)) ⟩ + (a -[ r ]> b + a + b) + b + a -[ r ]> c + c ≡⟨ L (L associativity) ⟩ + a -[ r ]> b + a + (b + b) + a -[ r ]> c + c ≡⟨ L (L (R (symmetry idempotence))) ⟩ + a -[ r ]> b + a + b + a -[ r ]> c + c ≡⟨ L (L (symmetry absorption)) ⟩ + a -[ r ]> b + a -[ r ]> c + c ≡⟨ L (R absorption) ⟩ + a -[ r ]> b + (a -[ r ]> c + a + c) + c ≡⟨ associativity ⟩ + a -[ r ]> b + (a -[ r ]> c + a + c + c) ≡⟨ (R associativity) ⟩ + a -[ r ]> b + (a -[ r ]> c + a + (c + c)) ≡⟨ R (R (symmetry idempotence)) ⟩ + a -[ r ]> b + (a -[ r ]> c + a + c) ≡⟨ R (symmetry absorption) ⟩ + a -[ r ]> b + a -[ r ]> c + ∎ + +-- Notice that we can't define 'graph-laws' below for 'to-graph' as we can't derive the +-- labelled graph laws from a graph alone. The two constructs are therefore not isomorphic. +to-graph : ∀ {A} -> LabelledGraph A -> Graph A +to-graph ε = Graph.ε +to-graph (v x) = Graph.v x +to-graph (x -[ r ]> y) with Bool.boolDioid r +... | Bool.false = to-graph x Graph.+ to-graph y +... | Bool.true = to-graph x Graph.* to-graph y + +from-graph : ∀ {A} -> Graph A -> LabelledGraph A +from-graph Graph.ε = ε +from-graph (Graph.v x) = v x +from-graph (x Graph.+ y) = from-graph x -[ Dioid.zero ]> from-graph y +from-graph (x Graph.* y) = from-graph x -[ Dioid.one ]> from-graph y + +graph-laws : ∀ {A} {x y : Graph A} -> x Graph.≡ y -> from-graph x ≡ from-graph y +graph-laws {x = x} {.x} Graph.reflexivity = reflexivity +graph-laws {x = x} {y} (Graph.symmetry eq) = symmetry (graph-laws eq) +graph-laws {x = x} {y} (Graph.transitivity eq eq₁) = transitivity (graph-laws eq) (graph-laws eq₁) +graph-laws {x = .(_ Graph.+ _)} {.(_ Graph.+ _)} (Graph.+left-congruence eq) = left-congruence (graph-laws eq) +graph-laws {x = .(_ Graph.+ _)} {.(_ Graph.+ _)} (Graph.+right-congruence eq) = right-congruence (graph-laws eq) +graph-laws {x = .(_ Graph.* _)} {.(_ Graph.* _)} (Graph.*left-congruence eq) = left-congruence (graph-laws eq) +graph-laws {x = .(_ Graph.* _)} {.(_ Graph.* _)} (Graph.*right-congruence eq) = right-congruence (graph-laws eq) +graph-laws {x = .(_ Graph.+ _)} {.(_ Graph.+ _)} Graph.+commutativity = zero-commutativity +graph-laws {x = .(_ Graph.+ (_ Graph.+ _))} {.(_ Graph.+ _ Graph.+ _)} Graph.+associativity = symmetry associativity +graph-laws {x = .(Graph.ε Graph.* y)} {y} Graph.*left-identity = left-identity +graph-laws {x = .(y Graph.* Graph.ε)} {y} Graph.*right-identity = right-identity +graph-laws {x = .(_ Graph.* (_ Graph.* _))} {.(_ Graph.* _ Graph.* _)} Graph.*associativity = symmetry associativity +graph-laws {x = .(_ Graph.* (_ Graph.+ _))} {.(_ Graph.* _ Graph.+ _ Graph.* _)} Graph.left-distributivity = left-distributivity +graph-laws {x = .((_ Graph.+ _) Graph.* _)} {.(_ Graph.* _ Graph.+ _ Graph.* _)} Graph.right-distributivity = right-distributivity +graph-laws {x = .(_ Graph.* _ Graph.* _)} {.(_ Graph.* _ Graph.+ _ Graph.* _ Graph.+ _ Graph.* _)} Graph.decomposition = right-decomposition