From 4edd93da49d0f1bc449ef42223ee63fdbb5a837e Mon Sep 17 00:00:00 2001
From: Andrey Mokhov <andrey.mokhov@gmail.com>
Date: Sun, 16 Apr 2017 02:25:46 +0100
Subject: [PATCH] Make working with congruence more convenient

---
 src/Graph.agda    | 24 ++++++++++++++++++++----
 src/Theorems.agda | 30 +++++++++++++++---------------
 2 files changed, 35 insertions(+), 19 deletions(-)

diff --git a/src/Graph.agda b/src/Graph.agda
index 6f60c50..ee8e5d5 100644
--- a/src/Graph.agda
+++ b/src/Graph.agda
@@ -19,10 +19,10 @@ data _≡_ : (x : Graph) -> (y : Graph) -> Set where
     transitivity : ∀ {x y z} -> (x ≡ y) -> (y ≡ z) -> x ≡ z
 
     -- Congruence
-    +lc : ∀ {x y z} -> (x ≡ y) -> x + z ≡ y + z
-    +rc : ∀ {x y z} -> (x ≡ y) -> z + x ≡ z + y
-    *lc : ∀ {x y z} -> (x ≡ y) -> x * z ≡ y * z
-    *rc : ∀ {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} -> (x ≡ y) -> x * z ≡ y * z
+    *right-congruence : ∀ {x y z} -> (x ≡ y) -> z * x ≡ z * y
 
     -- Axioms of +
     +commutativity : ∀ {x y}   -> x + y       ≡ y + x
@@ -38,3 +38,19 @@ 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
 
+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/Theorems.agda b/src/Theorems.agda
index bf05860..c95cba7 100644
--- a/src/Theorems.agda
+++ b/src/Theorems.agda
@@ -6,27 +6,27 @@ open import Reasoning A
 +pre-idempotence : ∀ {x} -> x + x + ε ≡ x
 +pre-idempotence {x} =
   begin
-    (x + x) + ε             ≡⟨ +lc (+lc (symmetry *right-identity)) ⟩
-    (x * ε + x) + ε         ≡⟨ +lc (+rc (symmetry *right-identity)) ⟩
-    (x * ε + x * ε) + ε     ≡⟨ +rc (symmetry *right-identity)       ⟩
-    (x * ε + x * ε) + ε * ε ≡⟨ symmetry decomposition               ⟩
-    (x * ε) * ε             ≡⟨ *right-identity                      ⟩
-    x * ε                   ≡⟨ *right-identity                      ⟩
+    (x + x) + ε             ≡⟨ L (L (symmetry *right-identity)) ⟩
+    (x * ε + x) + ε         ≡⟨ L (R (symmetry *right-identity)) ⟩
+    (x * ε + x * ε) + ε     ≡⟨ R (symmetry *right-identity)     ⟩
+    (x * ε + x * ε) + ε * ε ≡⟨ symmetry decomposition           ⟩
+    (x * ε) * ε             ≡⟨ *right-identity                  ⟩
+    x * ε                   ≡⟨ *right-identity                  ⟩
     x
   ∎
 
 +identity : ∀ {x} -> x + ε ≡ x
 +identity {x} =
   begin
-    x + ε                   ≡⟨ symmetry +pre-idempotence           ⟩
-    ((x + ε) + (x + ε)) + ε ≡⟨ +lc +associativity                  ⟩
-    (((x + ε) + x) + ε) + ε ≡⟨ +lc (+lc (symmetry +associativity)) ⟩
-    ((x + (ε + x)) + ε) + ε ≡⟨ +lc (+lc (+rc +commutativity))      ⟩
-    ((x + (x + ε)) + ε) + ε ≡⟨ +lc (+lc +associativity)            ⟩
-    (((x + x) + ε) + ε) + ε ≡⟨ +lc (symmetry +associativity)       ⟩
-    ((x + x) + (ε + ε)) + ε ≡⟨ symmetry +associativity             ⟩
-    (x + x) + ((ε + ε) + ε) ≡⟨ +rc +pre-idempotence                ⟩
-    (x + x) + ε             ≡⟨ +pre-idempotence                    ⟩
+    x + ε                   ≡⟨ symmetry +pre-idempotence       ⟩
+    ((x + ε) + (x + ε)) + ε ≡⟨ L +associativity                ⟩
+    (((x + ε) + x) + ε) + ε ≡⟨ L (L (symmetry +associativity)) ⟩
+    ((x + (ε + x)) + ε) + ε ≡⟨ L (L (R +commutativity))        ⟩
+    ((x + (x + ε)) + ε) + ε ≡⟨ L (L +associativity)            ⟩
+    (((x + x) + ε) + ε) + ε ≡⟨ L (symmetry +associativity)     ⟩
+    ((x + x) + (ε + ε)) + ε ≡⟨ symmetry +associativity         ⟩
+    (x + x) + ((ε + ε) + ε) ≡⟨ R +pre-idempotence              ⟩
+    (x + x) + ε             ≡⟨ +pre-idempotence                ⟩
     x
   ∎