Merge pull request #1 from anfelor/master

Implement proofs for edge labelled graphs and dioids

.travis.yml

@@ -8,8 +8,5 @@ services:
 before_install:
 - docker pull scottfleischman/agda:2.5.2
 
-env:
-- AGDA_FILE="src/API/Theorems.agda"
-
 script:
-- docker run -v $TRAVIS_BUILD_DIR:/opt/agda-build scottfleischman/agda:2.5.2 /bin/sh -c 'cd /opt/agda-build; agda '$AGDA_FILE
+- docker run -v $TRAVIS_BUILD_DIR:/opt/agda-build scottfleischman/agda:2.5.2 /bin/sh -c 'cd /opt/agda-build; ./verify.sh'

README.md

@@ -9,13 +9,26 @@ and prove a few key theorems.
 
 This repository is fully self-contained and does not depend on any Agda libraries. We use
 [this Travis build script](https://github.com/scott-fleischman/agda-travis) for continuous
-verification of the proofs.
+verification of the proofs. To verify whether your implementation is correct, 
+you can invoke the `verify.sh` script.
 
 Below we describe the purpose of all source files contained in the `src` directory.
 
-* `Algebra` defines the equational theory of graphs.
-* `Reasoning` provides standard syntax sugar for writing equational proofs.
+* Inside the `Algebra` folder, we define the following structures:
+
+  * `Dioid`, a semiring (or rng) where the `+` operation is idempotent.
+  * `Bool`, an implementation of a dioid.
+  * `ShortestDistance`, another instance.
+  * `Graph`, an [algebraic graphs](https://github.com/snowleopard/alga-paper).
+  * `LabelledGraph`, an extension of a `Graph`.
+
+  for each of these there are three files:
+
+  * `Structure.agda`, the main implementation.
+  * `Structure/Reasoning.agda`, syntactic sugar for writing equational proofs.
+  * `Structure/Theorems.agda`, some theorems of the structure.
+
+
 * `Prelude` defines products, lists and other functionality for describing Haskell APIs.
 * `API` defines key functions from the API of the algebraic-graphs library.
-* `Algebra/Theorems` proves theorems of the algebra of graphs.
 * `API/Theorems` proves theorems of the API.

src/API.agda

@@ -1,6 +1,6 @@
 module API where
 
-open import Algebra
+open import Algebra.Graph
 open import Prelude
 
 empty : ∀ {A} -> Graph A

src/API/Theorems.agda

@@ -1,10 +1,10 @@
 module API.Theorems where
 
-open import Algebra
-open import Algebra.Theorems
+open import Algebra.Graph
+open import Algebra.Graph.Theorems
+open import Algebra.Graph.Reasoning
 open import API
 open import Prelude
-open import Reasoning
 
 -- vertices [x] == vertex x
 vertices-vertex : ∀ {A} {x : A} -> vertices [ x ] ≡ vertex x

src/Algebra/Dioid.agda

@@ -0,0 +1,41 @@
+module Algebra.Dioid where
+
+data Dioid : Set where
+  zero : Dioid
+  one  : Dioid
+  _+_  : Dioid -> Dioid -> Dioid
+  _*_  : Dioid -> Dioid -> Dioid
+
+infixl 4  _≡_
+infixl 8  _+_
+infixl 9  _*_
+
+-- Equational theory of dioids
+data _≡_ : (r s : Dioid) -> Set where
+    -- Equivalence relation
+    reflexivity  : ∀ {r     : Dioid} ->                   r ≡ r
+    symmetry     : ∀ {r s   : Dioid} -> r ≡ s ->          s ≡ r
+    transitivity : ∀ {r s t : Dioid} -> r ≡ s -> s ≡ t -> r ≡ t
+
+    -- Congruence
+    +left-congruence  : ∀ {r s t : Dioid} -> r ≡ s -> r + t ≡ s + t
+    +right-congruence : ∀ {r s t : Dioid} -> r ≡ s -> t + r ≡ t + s
+    *left-congruence  : ∀ {r s t : Dioid} -> r ≡ s -> r * t ≡ s * t
+    *right-congruence : ∀ {r s t : Dioid} -> r ≡ s -> t * r ≡ t * s
+
+    -- Axioms of +
+    +idempotence   : ∀ {r : Dioid}     -> r + r       ≡ r
+    +commutativity : ∀ {r s : Dioid}   -> r + s       ≡ s + r
+    +associativity : ∀ {r s t : Dioid} -> r + (s + t) ≡ (r + s) + t
+    +zero-identity : ∀ {r : Dioid}     -> r + zero    ≡ r
+
+    -- Axioms of *
+    *associativity  : ∀ {r s t : Dioid} -> r * (s * t) ≡ (r * s) * t
+    *left-zero      : ∀ {r : Dioid}     -> zero * r    ≡ zero
+    *right-zero     : ∀ {r : Dioid}     -> r * zero    ≡ zero
+    *left-identity  : ∀ {r : Dioid}     -> one * r     ≡ r
+    *right-identity : ∀ {r : Dioid}     -> r * one     ≡ r
+
+    -- Distributivity
+    left-distributivity  : ∀ {r s t : Dioid} -> r * (s + t) ≡ r * s + r * t
+    right-distributivity : ∀ {r s t : Dioid} -> (r + s) * t ≡ r * t + s * t

src/Algebra/Dioid/Bool.agda

@@ -0,0 +1,26 @@
+module Algebra.Dioid.Bool where
+
+open import Algebra.Dioid using (Dioid; zero; one; _+_; _*_)
+
+data Bool : Set where
+  true  : Bool
+  false : Bool
+
+data _≡_ : (x y : Bool) -> Set where
+  reflexivity  : ∀ {x     : Bool} ->                   x ≡ x
+  symmetry     : ∀ {x y   : Bool} -> x ≡ y ->          y ≡ x
+  transitivity : ∀ {x y z : Bool} -> x ≡ y -> y ≡ z -> x ≡ z
+
+_or_ : Bool -> Bool -> Bool
+false or false = false
+_ or _ = true
+
+_and_ : Bool -> Bool -> Bool
+true and true = true
+_ and _ = false
+
+bool-dioid : Dioid -> Bool
+bool-dioid zero = false
+bool-dioid one  = true
+bool-dioid (r + s) = bool-dioid r or  bool-dioid s
+bool-dioid (r * s) = bool-dioid r and bool-dioid s

src/Algebra/Dioid/Bool/Theorems.agda

@@ -0,0 +1,101 @@
+module Algebra.Dioid.Bool.Theorems where
+
+open import Algebra.Dioid using (Dioid; zero; one; _+_; _*_)
+import Algebra.Dioid
+open import Algebra.Dioid.Bool
+
+or-left-congruence : ∀ {b c d : Bool} -> b ≡ c -> (b or d) ≡ (c or d)
+or-left-congruence {b} {.b} {d} reflexivity = reflexivity
+or-left-congruence {b} {c} {d} (symmetry eq) = symmetry (or-left-congruence eq)
+or-left-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (or-left-congruence eq) (or-left-congruence eq₁)
+
+or-right-congruence : ∀ {b c d : Bool} -> c ≡ d -> (b or c) ≡ (b or d)
+or-right-congruence {b} {c} {.c} reflexivity = reflexivity
+or-right-congruence {b} {c} {d} (symmetry eq) = symmetry (or-right-congruence eq)
+or-right-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (or-right-congruence eq) (or-right-congruence eq₁)
+
+and-left-congruence : ∀ {b c d : Bool} -> b ≡ c -> (b and d) ≡ (c and d)
+and-left-congruence {b} {.b} {d} reflexivity = reflexivity
+and-left-congruence {b} {c} {d} (symmetry eq) = symmetry (and-left-congruence eq)
+and-left-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (and-left-congruence eq) (and-left-congruence eq₁)
+
+and-right-congruence : ∀ {b c d : Bool} -> c ≡ d -> (b and c) ≡ (b and d)
+and-right-congruence {b} {c} {.c} reflexivity = reflexivity
+and-right-congruence {b} {c} {d} (symmetry eq) = symmetry (and-right-congruence eq)
+and-right-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (and-right-congruence eq) (and-right-congruence eq₁)
+
+or-idempotence : ∀ {b : Bool} -> (b or b) ≡ b
+or-idempotence {true} = reflexivity
+or-idempotence {false} = reflexivity
+
+or-commutativity : ∀ {b c : Bool} -> (b or c) ≡ (c or b)
+or-commutativity {true} {true} = reflexivity
+or-commutativity {true} {false} = reflexivity
+or-commutativity {false} {true} = reflexivity
+or-commutativity {false} {false} = reflexivity
+
+or-associativity : ∀ {b c d : Bool} -> (b or (c or d)) ≡ ((b or c) or d)
+or-associativity {true} {c} {d} = reflexivity
+or-associativity {false} {true} {d} = reflexivity
+or-associativity {false} {false} {true} = reflexivity
+or-associativity {false} {false} {false} = reflexivity
+
+or-false-identity : ∀ {b : Bool} -> (b or false) ≡ b
+or-false-identity {true} = reflexivity
+or-false-identity {false} = reflexivity
+
+and-associativity : ∀ {b c d : Bool} -> (b and (c and d)) ≡ ((b and c) and d)
+and-associativity {true} {true} {true} = reflexivity
+and-associativity {true} {true} {false} = reflexivity
+and-associativity {true} {false} {d} = reflexivity
+and-associativity {false} {c} {d} = reflexivity
+
+and-left-false : ∀ {b : Bool} -> (false and b) ≡ false
+and-left-false {b} = reflexivity
+
+and-right-false : ∀ {b : Bool} -> (b and false) ≡ false
+and-right-false {true} = reflexivity
+and-right-false {false} = reflexivity
+
+and-left-true : ∀ {b : Bool} -> (true and b) ≡ b
+and-left-true {true} = reflexivity
+and-left-true {false} = reflexivity
+
+and-right-true : ∀ {b : Bool} -> (b and true) ≡ b
+and-right-true {true} = reflexivity
+and-right-true {false} = reflexivity
+
+left-distributivity : ∀ {b c d : Bool} -> (b and (c or d)) ≡ ((b and c) or (b and d))
+left-distributivity {true} {true} {d} = reflexivity
+left-distributivity {true} {false} {true} = reflexivity
+left-distributivity {true} {false} {false} = reflexivity
+left-distributivity {false} {c} {d} = reflexivity
+
+right-distributivity : ∀ {b c d : Bool} -> ((b or c) and d) ≡ ((b and d) or (c and d))
+right-distributivity {true} {true} {true} = reflexivity
+right-distributivity {true} {true} {false} = reflexivity
+right-distributivity {true} {false} {true} = reflexivity
+right-distributivity {true} {false} {false} = reflexivity
+right-distributivity {false} {true} {true} = reflexivity
+right-distributivity {false} {true} {false} = reflexivity
+right-distributivity {false} {false} {d} = reflexivity
+
+bool-dioid-lawful : ∀ {r s : Dioid} -> r Algebra.Dioid.≡ s -> bool-dioid r ≡ bool-dioid s
+bool-dioid-lawful {r} {.r} Algebra.Dioid.reflexivity = reflexivity
+bool-dioid-lawful {r} {s} (Algebra.Dioid.symmetry eq) = symmetry (bool-dioid-lawful eq)
+bool-dioid-lawful {r} {s} (Algebra.Dioid.transitivity eq eq₁) = transitivity (bool-dioid-lawful eq) (bool-dioid-lawful eq₁)
+bool-dioid-lawful {.(_ + _)} {.(_ + _)} (Algebra.Dioid.+left-congruence eq) = or-left-congruence (bool-dioid-lawful eq)
+bool-dioid-lawful {.(_ + _)} {.(_ + _)} (Algebra.Dioid.+right-congruence eq) = or-right-congruence (bool-dioid-lawful eq)
+bool-dioid-lawful {.(_ * _)} {.(_ * _)} (Algebra.Dioid.*left-congruence eq) = and-left-congruence (bool-dioid-lawful eq)
+bool-dioid-lawful {.(_ * _)} {.(_ * _)} (Algebra.Dioid.*right-congruence eq) = and-right-congruence (bool-dioid-lawful eq)
+bool-dioid-lawful {.(s + s)} {s} Algebra.Dioid.+idempotence = or-idempotence
+bool-dioid-lawful {.(_ + _)} {.(_ + _)} Algebra.Dioid.+commutativity = or-commutativity
+bool-dioid-lawful {.(_ + (_ + _))} {.(_ + _ + _)} Algebra.Dioid.+associativity = or-associativity
+bool-dioid-lawful {.(s + zero)} {s} Algebra.Dioid.+zero-identity = or-false-identity
+bool-dioid-lawful {.(_ * (_ * _))} {.(_ * _ * _)} Algebra.Dioid.*associativity = and-associativity
+bool-dioid-lawful {.(zero * _)} {.zero} Algebra.Dioid.*left-zero = reflexivity
+bool-dioid-lawful {.(_ * zero)} {.zero} Algebra.Dioid.*right-zero = and-right-false
+bool-dioid-lawful {.(one * s)} {s} Algebra.Dioid.*left-identity = and-left-true
+bool-dioid-lawful {.(s * one)} {s} Algebra.Dioid.*right-identity = and-right-true
+bool-dioid-lawful {.(_ * (_ + _))} {.(_ * _ + _ * _)} Algebra.Dioid.left-distributivity = left-distributivity
+bool-dioid-lawful {.((_ + _) * _)} {.(_ * _ + _ * _)} Algebra.Dioid.right-distributivity = right-distributivity

src/Algebra/Dioid/Reasoning.agda

@@ -0,0 +1,40 @@
+module Algebra.Dioid.Reasoning where
+
+open import Algebra.Dioid
+
+-- Standard syntax sugar for writing equational proofs
+infix 4 _≈_
+data _≈_ (x y : Dioid) : Set where
+    prove : x ≡ y -> x ≈ y
+
+infix 1 begin_
+begin_ : ∀ {x y : Dioid} -> x ≈ y -> x ≡ y
+begin prove p = p
+
+infixr 2 _≡⟨_⟩_
+_≡⟨_⟩_ : ∀ (x : Dioid) {y z : Dioid} -> x ≡ y -> y ≈ z -> x ≈ z
+_ ≡⟨ p ⟩ prove q = prove (transitivity p q)
+
+infix 3 _∎
+_∎ : ∀ (x : Dioid) -> x ≈ x
+_∎ _ = prove reflexivity
+
+infixl 8 _>>_
+_>>_ : ∀ {x y z : Dioid} -> x ≡ y -> y ≡ z -> x ≡ z
+_>>_ = transitivity
+
+data BinaryOperator : Set where
+  +op : BinaryOperator
+  *op : BinaryOperator
+
+apply : BinaryOperator -> Dioid -> Dioid -> Dioid
+apply +op a b = a + b
+apply *op a b = a * b
+
+L : ∀ {op : BinaryOperator} -> ∀ {x y z : Dioid} -> x ≡ y -> apply op x z ≡ apply op y z
+L {+op} {x} {y} {z} eq = +left-congruence {x} {y} {z} eq
+L {*op} {x} {y} {z} eq = *left-congruence {x} {y} {z} eq
+
+R : ∀ {op : BinaryOperator} -> ∀ {x y z : Dioid} -> x ≡ y -> apply op z x ≡ apply op z y
+R {+op} {x} {y} {z} eq = +right-congruence {x} {y} {z} eq
+R {*op} {x} {y} {z} eq = *right-congruence {x} {y} {z} eq

src/Algebra/Dioid/ShortestDistance.agda

@@ -0,0 +1,41 @@
+module Algebra.Dioid.ShortestDistance where
+
+module Nat where
+  data Nat : Set where
+    zero : Nat
+    succ : Nat -> Nat
+
+  min : Nat -> Nat -> Nat
+  min zero n = n
+  min n zero = n
+  min (succ n) (succ m) = min n m
+
+  _+_ : Nat -> Nat -> Nat
+  zero + n = n
+  n + zero = n
+  (succ n) + m = succ (n + m)
+
+open import Algebra.Dioid using (Dioid; zero; one; _+_; _*_)
+
+data ShortestDistance : Set where
+  Distance : Nat.Nat -> ShortestDistance
+  Unreachable : ShortestDistance
+
+data _≡_ : (x y : ShortestDistance) -> Set where
+  reflexivity  : ∀ {x     : ShortestDistance} ->                   x ≡ x
+  symmetry     : ∀ {x y   : ShortestDistance} -> x ≡ y ->          y ≡ x
+  transitivity : ∀ {x y z : ShortestDistance} -> x ≡ y -> y ≡ z -> x ≡ z
+
+shortest-distance-dioid : Dioid -> ShortestDistance
+shortest-distance-dioid zero = Unreachable
+shortest-distance-dioid one  = Distance Nat.zero
+shortest-distance-dioid (r + s) with shortest-distance-dioid r
+... | Unreachable = shortest-distance-dioid s
+... | Distance n with shortest-distance-dioid s
+... | Unreachable = Distance n
+... | Distance m = Distance (Nat.min n m)
+shortest-distance-dioid (r * s) with shortest-distance-dioid r
+... | Unreachable = Unreachable
+... | Distance n with shortest-distance-dioid s
+... | Unreachable = Unreachable
+... | Distance m = Distance (n Nat.+ m)

src/Algebra/Dioid/Theorems.agda

@@ -0,0 +1,12 @@
+module Algebra.Dioid.Theorems where
+
+open import Algebra.Dioid
+open import Algebra.Dioid.Reasoning
+
+left-zero-identity : ∀ {r : Dioid} -> (zero + r) ≡ r
+left-zero-identity {r} =
+  begin
+    zero + r ≡⟨ +commutativity ⟩
+    r + zero ≡⟨ +zero-identity ⟩
+    r
+  ∎

src/Algebra.agda → src/Algebra/Graph.agda

@@ -1,4 +1,4 @@
-module Algebra where
+module Algebra.Graph where
 
 -- Core graph construction primitives
 data Graph (A : Set) : Set where

src/Reasoning.agda → src/Algebra/Graph/Reasoning.agda

@@ -1,6 +1,6 @@
-module Reasoning where
+module Algebra.Graph.Reasoning where
 
-open import Algebra
+open import Algebra.Graph
 
 -- Standard syntax sugar for writing equational proofs
 infix 4 _≈_

src/Algebra/Theorems.agda → src/Algebra/Graph/Theorems.agda

@@ -1,7 +1,7 @@
-module Algebra.Theorems where
+module Algebra.Graph.Theorems where
 
-open import Algebra
-open import Reasoning
+open import Algebra.Graph
+open import Algebra.Graph.Reasoning
 
 +pre-idempotence : ∀ {A} {x : Graph A} -> x + x + ε ≡ x
 +pre-idempotence {_} {x} =