From 9f6f3450eebf904e91ed74663c783573f4242c3b Mon Sep 17 00:00:00 2001 From: Alexandre Moine Date: Sat, 23 Jun 2018 13:26:18 +0200 Subject: [PATCH] Demote right congruence of + to a theorem (#3) * + Right congruence can be proven * Move the proof --- src/Algebra/Graph.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Graph.agda b/src/Algebra/Graph.agda index c40cddc..49e052b 100644 --- a/src/Algebra/Graph.agda +++ b/src/Algebra/Graph.agda @@ -21,7 +21,7 @@ data _≡_ {A} : (x y : Graph A) -> Set where -- Congruence +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 + -- +right-congruence holds as a theorem, please see below *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 @@ -39,6 +39,9 @@ data _≡_ {A} : (x y : Graph A) -> Set where 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 ++right-congruence : ∀ {A} {x y z : Graph A} -> x ≡ y -> z + x ≡ z + y ++right-congruence {_} {x} {y} {z} eq = transitivity +commutativity (transitivity (+left-congruence eq) +commutativity) + -- Subgraph relation _⊆_ : ∀ {A} -> Graph A -> Graph A -> Set x ⊆ y = x + y ≡ y