Prove equivalence of LabelledGraph Bool A and Graph A

src/Algebra/Dioid.agda

@@ -1,6 +1,5 @@
 module Algebra.Dioid where
 
-
 record Dioid A (_≡_ : A -> A -> Set) : Set where
   field
     zero : A

src/Algebra/Graph/Theorems.agda

@@ -124,3 +124,99 @@ absorption {_} {x} {y} =
 ⊆right-monotony : ∀ {A} {op : BinaryOperator} {x y z : Graph A} -> x ⊆ y -> apply op z x ⊆ apply op z y
 ⊆right-monotony {_} {+op} {x} {y} {z} p = ⊆right-overlay-monotony p
 ⊆right-monotony {_} {*op} {x} {y} {z} p = ⊆right-connect-monotony p
+
+
+-- | Helper theorems
+
+flip-end : ∀ {A} {x y z : Graph A} -> (x + y + z) ≡ (x + z + y)
+flip-end = symmetry +associativity >> R +commutativity >> +associativity
+
+*+ltriple : ∀ {A} {x y z : Graph A} -> (x * (y + z)) ≡ (x * y) + (x * z) + (y + z)
+*+ltriple {_} {x} {y} {z} =
+  begin
+    (x * (y + z)) ≡⟨ left-distributivity ⟩
+    (x * y + x * z) ≡⟨ L (symmetry absorption) ⟩
+    (x * y + x + y + x * z) ≡⟨ R (symmetry absorption) ⟩
+    ((x * y + x + y) + (x * z + x + z)) ≡⟨ symmetry +associativity ⟩
+    ((x * y + x) + (y + (x * z + x + z))) ≡⟨ R +commutativity ⟩
+    ((x * y + x) + ((x * z + x + z) + y)) ≡⟨ symmetry +associativity ⟩
+    (x * y + (x + (x * z + x + z + y))) ≡⟨ R +commutativity ⟩
+    (x * y + (x * z + x + z + y + x)) ≡⟨ R flip-end ⟩
+    (x * y + (x * z + x + z + x + y)) ≡⟨ R (L flip-end) ⟩
+    (x * y + (x * z + x + x + z + y)) ≡⟨ R (L (L (symmetry +associativity >> R +idempotence))) ⟩
+    (x * y + (x * z + x + z + y)) ≡⟨ R (L (L (L (symmetry absorption)))) ⟩
+    (x * y + (x * z + x + z + x + z + y)) ≡⟨ R (L (L flip-end)) ⟩
+    (x * y + (x * z + x + x + z + z + y)) ≡⟨ R (L (L (L (symmetry +associativity >> R +idempotence)))) ⟩
+    (x * y + (x * z + x + z + z + y)) ≡⟨ R (L (L absorption)) ⟩
+    (x * y + (x * z + z + y)) ≡⟨ R (symmetry +associativity) ⟩
+    (x * y + (x * z + (z + y))) ≡⟨ +associativity ⟩
+    (x * y + (x * z) + (z + y)) ≡⟨ +right-congruence +commutativity ⟩
+    (x * y) + (x * z) + (y + z)
+  ∎
+
++*ltriple : ∀ {A} {x y z : Graph A} -> (x + (y * z)) ≡ (x + y) + (x + z) + (y * z)
++*ltriple {_} {x} {y} {z} =
+  begin
+    (x + (y * z)) ≡⟨ R (symmetry absorption) ⟩
+    (x + (y * z + y + z)) ≡⟨ R (symmetry +associativity >> +commutativity) ⟩
+    (x + (y + z + y * z)) ≡⟨ L (symmetry +idempotence) ⟩
+    (x + x + (y + z + y * z)) ≡⟨ +associativity ⟩
+    (x + x + (y + z) + y * z) ≡⟨ L (+associativity) ⟩
+    (x + x + y + z + y * z) ≡⟨ L (L flip-end) ⟩
+    (x + y + x + z + y * z) ≡⟨ L (symmetry +associativity) ⟩
+    (x + y + (x + z) + (y * z))
+  ∎
+
+++ltriple : ∀ {A} {x y z : Graph A} -> (x + (y + z)) ≡ (x + y) + (x + z) + (y + z)
+++ltriple {_} {x} {y} {z} =
+  begin
+    (x + (y + z)) ≡⟨ +associativity ⟩
+    (x + y + z) ≡⟨ L (symmetry +idempotence) ⟩
+    (x + y + (x + y) + z) ≡⟨ symmetry +associativity ⟩
+    (x + y + (x + y + z)) ≡⟨ R flip-end ⟩
+    (x + y + (x + z + y)) ≡⟨ R (L (R (symmetry +idempotence))) ⟩
+    (x + y + (x + (z + z) + y)) ≡⟨ R (L (+associativity)) ⟩
+    (x + y + (x + z + z + y)) ≡⟨ R (symmetry +associativity) ⟩
+    (x + y + ((x + z) + (z + y))) ≡⟨ +associativity ⟩
+    (x + y + (x + z) + (z + y)) ≡⟨ R (+commutativity) ⟩
+    (x + y + (x + z) + (y + z))
+  ∎
+
+*+rtriple : ∀ {A} {x y z : Graph A} -> ((x * y) + z) ≡ (x * y) + (x + z) + (y + z)
+*+rtriple {_} {x} {y} {z} =
+  begin
+    (x * y + z) ≡⟨ L (symmetry absorption) ⟩
+    (x * y + x + y + z) ≡⟨ R (symmetry +idempotence) ⟩
+    (x * y + x + y + (z + z)) ≡⟨ +associativity ⟩
+    (x * y + x + y + z + z) ≡⟨ L flip-end ⟩
+    (x * y + x + z + y + z) ≡⟨ symmetry +associativity ⟩
+    (x * y + x + z + (y + z)) ≡⟨ L (symmetry +associativity) ⟩
+    (x * y + (x + z) + (y + z))
+  ∎
+
++*rtriple : ∀ {A} {x y z : Graph A} -> ((x + y) * z) ≡ (x + y) + (x * z) + (y * z)
++*rtriple {_} {x} {y} {z} =
+  begin
+    ((x + y) * z) ≡⟨ right-distributivity ⟩
+    (x * z + y * z) ≡⟨ L (symmetry absorption) ⟩
+    (x * z + x + z + y * z) ≡⟨ R (symmetry absorption) ⟩
+    (x * z + x + z + (y * z + y + z)) ≡⟨ symmetry (R +associativity) ⟩
+    (x * z + x + z + (y * z + (y + z))) ≡⟨ R +commutativity ⟩
+    (x * z + x + z + (y + z + y * z)) ≡⟨ +associativity ⟩
+    (x * z + x + z + (y + z) + y * z) ≡⟨ L +associativity ⟩
+    (x * z + x + z + y + z + y * z) ≡⟨ L flip-end ⟩
+    (x * z + x + z + z + y + y * z) ≡⟨ L (L (symmetry +associativity)) ⟩
+    (x * z + x + (z + z) + y + y * z) ≡⟨ L (L (R +idempotence)) ⟩
+    (x * z + x + z + y + y * z) ≡⟨ L (L (L (R (symmetry +idempotence)))) ⟩
+    (x * z + (x + x) + z + y + y * z) ≡⟨ L (L (L +associativity)) ⟩
+    (x * z + x + x + z + y + y * z) ≡⟨ L (L (symmetry +associativity)) ⟩
+    (x * z + x + (x + z) + y + y * z) ≡⟨ L (L (R +commutativity)) ⟩
+    (x * z + x + (z + x) + y + y * z) ≡⟨ L (L +associativity)⟩
+    (x * z + x + z + x + y + y * z) ≡⟨ L (L (L absorption)) ⟩
+    (x * z + x + y + y * z) ≡⟨ symmetry (L +associativity) ⟩
+    (x * z + (x + y) + y * z) ≡⟨ L +commutativity ⟩
+    (x + y + (x * z) + (y * z))
+  ∎
+
+++rtriple : ∀ {A} {x y z : Graph A} -> ((x + y) + z) ≡ (x + y) + (x + z) + (y + z)
+++rtriple {_} {x} {y} {z} = symmetry +associativity >> ++ltriple

src/Algebra/LabelledGraph/Theorems.agda

@@ -5,8 +5,12 @@ open import Algebra.LabelledGraph.Reasoning
 open import Algebra.Dioid
 open import Algebra.Graph using (Graph)
 import Algebra.Graph as Graph
+import Algebra.Graph.Reasoning as Graph
+import Algebra.Graph.Theorems as Graph
 import Algebra.Dioid.Bool as Bool
+import Algebra.Dioid.Bool.Theorems as Bool
 
+-- | Laws of labelled graphs
 
 associativity : ∀ {A D eq} {d : Dioid D eq} {a b c : LabelledGraph d A} {r : D} -> (a [ r ]> b) [ r ]> c ≡ a [ r ]> (b [ r ]> c)
 associativity {_} {_} {_} {_} {a} {b} {c} {r} = right-decomposition >> symmetry left-decomposition
@@ -86,14 +90,50 @@ left-distributivity {_} {_} {_} {_} {a} {b} {c} {r} =
     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} {d : Dioid Bool.Bool Bool._≡_} -> LabelledGraph d A -> Graph A
+-- | Conversion functions
+-- These allow for a conversion between LabelledGraphs labelled by Bools and ordinary Graphs.
+-- As `graph-laws` and `labelled-graph-laws` demonstrates, these preserve their respective laws.
+
+to-graph : ∀ {A} -> LabelledGraph Bool.bool-dioid A -> Graph A
 to-graph ε = Graph.ε
 to-graph (v x) = Graph.v x
 to-graph (x [ Bool.false ]> y) = to-graph x Graph.+ to-graph y
 to-graph (x [ Bool.true  ]> y) = to-graph x Graph.* to-graph y
 
+labelled-graph-laws : ∀ {A} {x y : LabelledGraph Bool.bool-dioid A} -> x ≡ y -> (to-graph x) Graph.≡ (to-graph y)
+labelled-graph-laws reflexivity = Graph.reflexivity
+labelled-graph-laws (symmetry eq) = Graph.symmetry (labelled-graph-laws eq)
+labelled-graph-laws (transitivity eq eq₁) = Graph.transitivity (labelled-graph-laws eq)
+                                              (labelled-graph-laws eq₁)
+labelled-graph-laws (left-congruence {r = r} eq) with r
+... | Bool.true = Graph.*left-congruence (labelled-graph-laws eq)
+... | Bool.false = Graph.+left-congruence (labelled-graph-laws eq)
+labelled-graph-laws (right-congruence {r = r} eq) with r
+... | Bool.true = Graph.*right-congruence (labelled-graph-laws eq)
+... | Bool.false = Graph.+right-congruence (labelled-graph-laws eq)
+labelled-graph-laws zero-commutativity = Graph.+commutativity
+labelled-graph-laws (left-identity {r = r}) with r
+... | Bool.true = Graph.*left-identity
+... | Bool.false = Graph.+commutativity Graph.>> Graph.+identity
+labelled-graph-laws (right-identity {r = r}) with r
+... | Bool.true = Graph.*right-identity
+... | Bool.false = Graph.+identity
+labelled-graph-laws (left-decomposition {r = r} {s}) with r | s
+... | Bool.true  | Bool.true  = Graph.*associativity Graph.>> Graph.decomposition
+... | Bool.true  | Bool.false = Graph.*+ltriple
+... | Bool.false | Bool.true  = Graph.+*ltriple
+... | Bool.false | Bool.false = Graph.++ltriple
+labelled-graph-laws (right-decomposition {r = r} {s}) with r | s
+... | Bool.true  | Bool.true  = Graph.decomposition
+... | Bool.true  | Bool.false = Graph.*+rtriple
+... | Bool.false | Bool.true  = Graph.+*rtriple
+... | Bool.false | Bool.false = Graph.++rtriple
+labelled-graph-laws (label-addition {r = r} {s}) with r | s
+... | Bool.true  | Bool.true  = Graph.+idempotence
+... | Bool.true  | Bool.false = Graph.+associativity Graph.>> Graph.absorption
+... | Bool.false | Bool.true  = (Graph.+commutativity Graph.>> Graph.+associativity) Graph.>> Graph.absorption
+... | Bool.false | Bool.false = Graph.+idempotence
+
 from-graph : ∀ {A D eq} {d : Dioid D eq} -> Graph A -> LabelledGraph d A
 from-graph Graph.ε = ε
 from-graph (Graph.v x) = v x
@@ -116,3 +156,53 @@ graph-laws {x = .(_ Graph.* (_ Graph.* _))} {.(_ Graph.* _ Graph.* _)} Graph.*as
 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
+
+to-from-identity : ∀ {A} {x y : Graph A} -> x Graph.≡ y -> (to-graph (from-graph x)) Graph.≡ (to-graph (from-graph y))
+to-from-identity Graph.reflexivity = Graph.reflexivity
+to-from-identity (Graph.symmetry eq) = Graph.symmetry (to-from-identity eq)
+to-from-identity (Graph.transitivity eq eq₁) = Graph.transitivity (to-from-identity eq) (to-from-identity eq₁)
+to-from-identity (Graph.+left-congruence eq) = Graph.+left-congruence (to-from-identity eq)
+to-from-identity (Graph.+right-congruence eq) = Graph.+right-congruence (to-from-identity eq)
+to-from-identity (Graph.*left-congruence eq) = Graph.*left-congruence (to-from-identity eq)
+to-from-identity (Graph.*right-congruence eq) = Graph.*right-congruence (to-from-identity eq)
+to-from-identity Graph.+commutativity = Graph.+commutativity
+to-from-identity Graph.+associativity = Graph.+associativity
+to-from-identity Graph.*left-identity = Graph.*left-identity
+to-from-identity Graph.*right-identity = Graph.*right-identity
+to-from-identity Graph.*associativity = Graph.*associativity
+to-from-identity Graph.left-distributivity = Graph.left-distributivity
+to-from-identity Graph.right-distributivity = Graph.right-distributivity
+to-from-identity Graph.decomposition = Graph.decomposition
+
+from-to-identity : ∀ {A} {x y : LabelledGraph Bool.bool-dioid A} -> x ≡ y -> _≡_ {A} {Bool.Bool} {Bool._≡_} {Bool.bool-dioid} (from-graph (to-graph x)) (from-graph (to-graph y))
+from-to-identity reflexivity = reflexivity
+from-to-identity (symmetry eq) = symmetry (from-to-identity eq)
+from-to-identity (transitivity eq eq₁) = transitivity (from-to-identity eq) (from-to-identity eq₁)
+from-to-identity (left-congruence {r = r} eq) with r
+... | Bool.true = left-congruence (from-to-identity eq)
+... | Bool.false = left-congruence (from-to-identity eq)
+from-to-identity (right-congruence {r = r} eq) with r
+... | Bool.true = right-congruence (from-to-identity eq)
+... | Bool.false = right-congruence (from-to-identity eq)
+from-to-identity zero-commutativity = zero-commutativity
+from-to-identity (left-identity {r = r}) with r
+... | Bool.true = left-identity
+... | Bool.false = left-identity
+from-to-identity (right-identity {r = r}) with r
+... | Bool.true = right-identity
+... | Bool.false = right-identity
+from-to-identity (left-decomposition {r = r} {s}) with r | s
+... | Bool.true  | Bool.true  = left-decomposition
+... | Bool.true  | Bool.false = left-decomposition
+... | Bool.false | Bool.true  = left-decomposition
+... | Bool.false | Bool.false = left-decomposition
+from-to-identity (right-decomposition {r = r} {s}) with r | s
+... | Bool.true  | Bool.true  = right-decomposition
+... | Bool.true  | Bool.false = right-decomposition
+... | Bool.false | Bool.true  = right-decomposition
+... | Bool.false | Bool.false = right-decomposition
+from-to-identity (label-addition {r = r} {s}) with r | s
+... | Bool.true  | Bool.true  = label-addition
+... | Bool.true  | Bool.false = label-addition
+... | Bool.false | Bool.true  = label-addition
+... | Bool.false | Bool.false = label-addition