From f14f68bd4e584fa043e1be89d26d1cde3c703432 Mon Sep 17 00:00:00 2001 From: Andrey Mokhov Date: Sun, 16 Apr 2017 15:55:56 +0100 Subject: [PATCH] Make Graph parameterised --- src/Graph.agda | 63 ++++++++++++++++++---------------------------- src/Reasoning.agda | 30 ++++++++++++++++------ src/Theorems.agda | 48 +++++++++++++++++------------------ 3 files changed, 71 insertions(+), 70 deletions(-) diff --git a/src/Graph.agda b/src/Graph.agda index 0e28667..520e6c8 100644 --- a/src/Graph.agda +++ b/src/Graph.agda @@ -1,11 +1,11 @@ -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 _+_ @@ -13,47 +13,32 @@ 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 diff --git a/src/Reasoning.agda b/src/Reasoning.agda index 2362a88..fefd953 100644 --- a/src/Reasoning.agda +++ b/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 diff --git a/src/Theorems.agda b/src/Theorems.agda index c500920..77416ff 100644 --- a/src/Theorems.agda +++ b/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,11 +30,11 @@ 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 ⟩ @@ -42,8 +42,8 @@ saturation {x} = 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 ⟩