Skip to content

Commit

Permalink
Add subgraph relation and prove associated theorems
Browse files Browse the repository at this point in the history
  • Loading branch information
snowleopard committed Apr 16, 2017
1 parent 82a71e8 commit 3f27510
Show file tree
Hide file tree
Showing 3 changed files with 65 additions and 4 deletions.
10 changes: 7 additions & 3 deletions src/Graph.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
6 changes: 5 additions & 1 deletion src/Reasoning.agda
Original file line number Diff line number Diff line change
Expand Up @@ -17,4 +17,8 @@ _ ≡⟨ p ⟩ prove q = prove (transitivity p q)

infix 3 _∎
_∎ : (x : Graph) -> x ≈ x
_∎ _ = prove reflexivity
_∎ _ = prove reflexivity

infixl 8 _>>_
_>>_ : {x y z} -> x ≡ y -> y ≡ z -> x ≡ z
_>>_ = transitivity
53 changes: 53 additions & 0 deletions src/Theorems.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 3f27510

Please sign in to comment.