Skip to content

Commit

Permalink
Make working with congruence more convenient
Browse files Browse the repository at this point in the history
  • Loading branch information
snowleopard committed Apr 16, 2017
1 parent a7e9830 commit 4edd93d
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 19 deletions.
24 changes: 20 additions & 4 deletions src/Graph.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

30 changes: 15 additions & 15 deletions src/Theorems.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down

0 comments on commit 4edd93d

Please sign in to comment.