Make Graph parameterised

src/Graph.agda

@@ -1,59 +1,44 @@
-module Graph (A : Set) where
+module Graph where
 
 -- Core graph construction primitives
-data Graph : Set where
-    ε   : Graph                   -- Empty graph
-    [_] : A -> Graph              -- Graph comprising a single vertex
-    _+_ : Graph -> Graph -> Graph -- Overlay two graphs
-    _*_ : Graph -> Graph -> Graph -- Connect two graphs
+data Graph (A : Set) : Set where
+    ε   : Graph A                       -- Empty graph
+    v   : A -> Graph A                  -- Graph comprising a single vertex
+    _+_ : Graph A -> Graph A -> Graph A -- Overlay two graphs
+    _*_ : Graph A -> Graph A -> Graph A -- Connect two graphs
 
 infixl 4  _≡_
 infixl 8  _+_
 infixl 9  _*_
 infix  10 _⊆_
 
 -- Equational theory of graphs
-data _≡_ : (x : Graph) -> (y : Graph) -> Set where
+data _≡_ {A} : (x y : Graph A) -> Set where
     -- Equivalence relation
-    reflexivity  : ∀ {x}     ->                   x ≡ x
-    symmetry     : ∀ {x y}   -> x ≡ y ->          y ≡ x
-    transitivity : ∀ {x y z} -> x ≡ y -> y ≡ z -> x ≡ z
+    reflexivity  : ∀ {x     : Graph A} ->                   x ≡ x
+    symmetry     : ∀ {x y   : Graph A} -> x ≡ y ->          y ≡ x
+    transitivity : ∀ {x y z : Graph A} -> x ≡ y -> y ≡ z -> x ≡ z
 
     -- Congruence
-    +left-congruence  : ∀ {x y z} -> x ≡ y -> x + z ≡ y + z
-    +right-congruence : ∀ {x y z} -> x ≡ y -> z + x ≡ z + y
-    *left-congruence  : ∀ {x y z} -> x ≡ y -> x * z ≡ y * z
-    *right-congruence : ∀ {x y z} -> x ≡ y -> z * x ≡ z * y
+    +left-congruence  : ∀ {x y z : Graph A} -> x ≡ y -> x + z ≡ y + z
+    +right-congruence : ∀ {x y z : Graph A} -> x ≡ y -> z + x ≡ z + y
+    *left-congruence  : ∀ {x y z : Graph A} -> x ≡ y -> x * z ≡ y * z
+    *right-congruence : ∀ {x y z : Graph A} -> x ≡ y -> z * x ≡ z * y
 
     -- Axioms of +
-    +commutativity : ∀ {x y}   -> x + y       ≡ y + x
-    +associativity : ∀ {x y z} -> x + (y + z) ≡ (x + y) + z
+    +commutativity : ∀ {x y : Graph A}   -> x + y       ≡ y + x
+    +associativity : ∀ {x y z : Graph A} -> x + (y + z) ≡ (x + y) + z
 
     -- Axioms of *
-    *left-identity  : ∀ {x}     -> ε * x       ≡ x
-    *right-identity : ∀ {x}     -> x * ε       ≡ x
-    *associativity  : ∀ {x y z} -> x * (y * z) ≡ (x * y) * z
+    *left-identity  : ∀ {x     : Graph A} -> ε * x       ≡ x
+    *right-identity : ∀ {x     : Graph A} -> x * ε       ≡ x
+    *associativity  : ∀ {x y z : Graph A} -> x * (y * z) ≡ (x * y) * z
 
     -- Other axioms
-    left-distributivity  : ∀ {x y z} -> x * (y + z) ≡ x * y + x * z
-    right-distributivity : ∀ {x y z} -> (x + y) * z ≡ x * z + y * z
-    decomposition        : ∀ {x y z} -> x * y * z   ≡ x * y + x * z + y * z
+    left-distributivity  : ∀ {x y z : Graph A} -> x * (y + z) ≡ x * y + x * z
+    right-distributivity : ∀ {x y z : Graph A} -> (x + y) * z ≡ x * z + y * z
+    decomposition        : ∀ {x y z : Graph A} -> x * y * z   ≡ x * y + x * z + y * z
 
-_⊆_ : Graph -> Graph -> Set
+-- Subgraph relation
+_⊆_ : ∀ {A} -> Graph A -> Graph A -> Set
 x ⊆ y = x + y ≡ y
-
-data BinaryOperator : Set where
-  overlay : BinaryOperator
-  connect : BinaryOperator
-
-apply : BinaryOperator -> Graph -> Graph -> Graph
-apply overlay a b = a + b
-apply connect a b = a * b
-
-L : ∀ {op : BinaryOperator} -> ∀ {x y z} -> x ≡ y -> apply op x z ≡ apply op y z
-L {overlay} {x} {y} {z} eq = +left-congruence {x} {y} {z} eq
-L {connect} {x} {y} {z} eq = *left-congruence {x} {y} {z} eq
-
-R : ∀ {op : BinaryOperator} -> ∀ {x y z} -> x ≡ y -> apply op z x ≡ apply op z y
-R {overlay} {x} {y} {z} eq = +right-congruence {x} {y} {z} eq
-R {connect} {x} {y} {z} eq = *right-congruence {x} {y} {z} eq

src/Reasoning.agda

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

src/Theorems.agda

@@ -1,10 +1,10 @@
-module Theorems (A : Set) where
+module Theorems where
 
-open import Graph A
-open import Reasoning A
+open import Graph
+open import Reasoning
 
-+pre-idempotence : ∀ {x} -> x + x + ε ≡ x
-+pre-idempotence {x} =
++pre-idempotence : ∀ {A} {x : Graph A} -> x + x + ε ≡ x
++pre-idempotence {_} {x} =
   begin
     (x + x) + ε             ≡⟨ L (L (symmetry *right-identity)) ⟩
     (x * ε + x) + ε         ≡⟨ L (R (symmetry *right-identity)) ⟩
@@ -15,8 +15,8 @@ open import Reasoning A
     x
   ∎
 
-+identity : ∀ {x} -> x + ε ≡ x
-+identity {x} =
++identity : ∀ {A} {x : Graph A} -> x + ε ≡ x
++identity {_} {x} =
   begin
     x + ε                   ≡⟨ symmetry +pre-idempotence       ⟩
     ((x + ε) + (x + ε)) + ε ≡⟨ L +associativity                ⟩
@@ -30,20 +30,20 @@ open import Reasoning A
     x
   ∎
 
-+idempotence : ∀ {x} -> x + x ≡ x
++idempotence : ∀ {A} {x : Graph A} -> x + x ≡ x
 +idempotence = transitivity (symmetry +identity) +pre-idempotence
 
-saturation : ∀ {x} -> x * x * x ≡ x * x
-saturation {x} =
+saturation : ∀ {A} {x : Graph A} -> x * x * x ≡ x * x
+saturation {_} {x} =
   begin
     (x * x) * x             ≡⟨ decomposition  ⟩
     (x * x + x * x) + x * x ≡⟨ L +idempotence ⟩
     x * x + x * x           ≡⟨ +idempotence   ⟩
     x * x
   ∎
 
-absorption : ∀ {x y} -> x * y + x + y ≡ x * y
-absorption {x} {y} =
+absorption : ∀ {A} {x y : Graph A} -> x * y + x + y ≡ x * y
+absorption {_} {x} {y} =
   begin
     (x * y + x) + y         ≡⟨ L (R (symmetry *right-identity)) ⟩
     (x * y + x * ε) + y     ≡⟨ R (symmetry *right-identity)     ⟩
@@ -53,32 +53,32 @@ absorption {x} {y} =
   ∎
 
 -- Subgraph relation
-⊆reflexivity : ∀ {x} -> x ⊆ x
+⊆reflexivity : ∀ {A} {x : Graph A} -> x ⊆ x
 ⊆reflexivity = +idempotence
 
-⊆antisymmetry : ∀ {x y} -> x ⊆ y -> y ⊆ x -> x ≡ y
+⊆antisymmetry : ∀ {A} {x y : Graph A} -> x ⊆ y -> y ⊆ x -> x ≡ y
 ⊆antisymmetry p q = symmetry q      -- x = y + x
                  >> +commutativity  --     y + x = x + y
                  >> p               --             x + y = y
 
-⊆transitivity : ∀ {x y z} -> x ⊆ y -> y ⊆ z -> x ⊆ z
+⊆transitivity : ∀ {A} {x y z : Graph A} -> x ⊆ y -> y ⊆ z -> x ⊆ z
 ⊆transitivity p q = symmetry
     (symmetry q              -- z = y + z
   >> L (symmetry p)          --     y + z = (x + y) + z
   >> symmetry +associativity --             (x + y) + z = x + (y + z)
   >> R q)                    --                           x + (y + z) = x + z
 
-⊆least-element : ∀ {x} -> ε ⊆ x
+⊆least-element : ∀ {A} {x : Graph A} -> ε ⊆ x
 ⊆least-element = +commutativity >> +identity
 
-⊆overlay : ∀ {x y} -> x ⊆ (x + y)
+⊆overlay : ∀ {A} {x y : Graph A} -> x ⊆ (x + y)
 ⊆overlay = +associativity >> L +idempotence
 
-⊆connect : ∀ {x y} -> (x + y) ⊆ (x * y)
+⊆connect : ∀ {A} {x y : Graph A} -> (x + y) ⊆ (x * y)
 ⊆connect = +commutativity >> +associativity >> absorption
 
-⊆overlay-monotony : ∀ {x y z} -> x ⊆ y -> (x + z) ⊆ (y + z)
-⊆overlay-monotony {x} {y} {z} p =
+⊆overlay-monotony : ∀ {A} {x y z : Graph A} -> x ⊆ y -> (x + z) ⊆ (y + z)
+⊆overlay-monotony {_} {x} {y} {z} p =
   begin
     (x + z) + (y + z) ≡⟨ symmetry +associativity     ⟩
     x + (z + (y + z)) ≡⟨ R +commutativity            ⟩
@@ -89,16 +89,16 @@ absorption {x} {y} =
     y + z
   ∎
 
-⊆left-connect-monotony : ∀ {x y z} -> x ⊆ y -> (x * z) ⊆ (y * z)
-⊆left-connect-monotony {x} {y} {z} p =
+⊆left-connect-monotony : ∀ {A} {x y z : Graph A} -> x ⊆ y -> (x * z) ⊆ (y * z)
+⊆left-connect-monotony {_} {x} {y} {z} p =
   begin
     (x * z) + (y * z) ≡⟨ symmetry right-distributivity ⟩
     (x + y) * z       ≡⟨ L p                           ⟩
     y * z
   ∎
 
-⊆right-connect-monotony : ∀ {x y z} -> x ⊆ y -> (z * x) ⊆ (z * y)
-⊆right-connect-monotony {x} {y} {z} p =
+⊆right-connect-monotony : ∀ {A} {x y z : Graph A} -> x ⊆ y -> (z * x) ⊆ (z * y)
+⊆right-connect-monotony {_} {x} {y} {z} p =
   begin
     (z * x) + (z * y) ≡⟨ symmetry left-distributivity ⟩
     z * (x + y)       ≡⟨ R p                          ⟩