From 3f2751070192410b14b399a1f6d576337cd54123 Mon Sep 17 00:00:00 2001
From: Andrey Mokhov <andrey.mokhov@gmail.com>
Date: Sun, 16 Apr 2017 04:12:57 +0100
Subject: [PATCH] Add subgraph relation and prove associated theorems

---
 src/Graph.agda     | 10 ++++++---
 src/Reasoning.agda |  6 +++++-
 src/Theorems.agda  | 53 ++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 65 insertions(+), 4 deletions(-)

diff --git a/src/Graph.agda b/src/Graph.agda
index 8d76628..8104d8e 100644
--- a/src/Graph.agda
+++ b/src/Graph.agda
@@ -7,9 +7,10 @@ data Graph : Set where
     _+_ : Graph -> Graph -> Graph -- Overlay two graphs
     _*_ : Graph -> Graph -> Graph -- Connect two graphs
 
-infixl 8 _+_
-infixl 9 _*_
-infixl 4 _≡_
+infixl 4  _≡_
+infixl 8  _+_
+infixl 9  _*_
+infix  10 _⊆_
 
 -- Equational theory of graphs
 data _≡_ : (x : Graph) -> (y : Graph) -> Set where
@@ -38,6 +39,9 @@ data _≡_ : (x : Graph) -> (y : Graph) -> Set where
     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
 
+_⊆_ : Graph -> Graph -> Set
+x ⊆ y = x + y ≡ y
+
 data BinaryOperator : Set where
   overlay : BinaryOperator
   connect : BinaryOperator
diff --git a/src/Reasoning.agda b/src/Reasoning.agda
index c030478..2362a88 100644
--- a/src/Reasoning.agda
+++ b/src/Reasoning.agda
@@ -17,4 +17,8 @@ _ ≡⟨ p ⟩ prove q = prove (transitivity p q)
 
 infix 3 _∎
 _∎ : (x : Graph) -> x ≈ x
-_∎ _ = prove reflexivity
\ No newline at end of file
+_∎ _ = prove reflexivity
+
+infixl 8 _>>_
+_>>_ : ∀ {x y z} -> x ≡ y -> y ≡ z -> x ≡ z
+_>>_ = transitivity
diff --git a/src/Theorems.agda b/src/Theorems.agda
index 85875d0..c500920 100644
--- a/src/Theorems.agda
+++ b/src/Theorems.agda
@@ -51,3 +51,56 @@ absorption {x} {y} =
     (x * y) * ε             ≡⟨ *right-identity                  ⟩
     x * y
   ∎
+
+-- Subgraph relation
+⊆reflexivity : ∀ {x} -> x ⊆ x
+⊆reflexivity = +idempotence
+
+⊆antisymmetry : ∀ {x y} -> 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 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 = +commutativity >> +identity
+
+⊆overlay : ∀ {x y} -> x ⊆ (x + y)
+⊆overlay = +associativity >> L +idempotence
+
+⊆connect : ∀ {x y} -> (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 =
+  begin
+    (x + z) + (y + z) ≡⟨ symmetry +associativity     ⟩
+    x + (z + (y + z)) ≡⟨ R +commutativity            ⟩
+    x + ((y + z) + z) ≡⟨ R (symmetry +associativity) ⟩
+    x + (y + (z + z)) ≡⟨ R (R +idempotence)          ⟩
+    x + (y + z)       ≡⟨ +associativity              ⟩
+    (x + y) + z       ≡⟨ L p                         ⟩
+    y + z
+  ∎
+
+⊆left-connect-monotony : ∀ {x y z} -> 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 =
+  begin
+    (z * x) + (z * y) ≡⟨ symmetry left-distributivity ⟩
+    z * (x + y)       ≡⟨ R p                          ⟩
+    z * y
+  ∎