Merge pull request #2 from anfelor/master

 Fix dioid instance as suggested by @Rotsor in #1

src/Algebra/Dioid.agda

@@ -1,41 +1,38 @@
 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
+record Dioid A (_≡_ : A -> A -> Set) : Set where
+  field
+    zero : A
+    one  : A
+    _+_  : A -> A -> A
+    _*_  : A -> A -> A
+
+    reflexivity  : ∀ {r     : A} ->                   r ≡ r
+    symmetry     : ∀ {r s   : A} -> r ≡ s ->          s ≡ r
+    transitivity : ∀ {r s t : A} -> r ≡ s -> s ≡ t -> r ≡ t
+
+    +left-congruence  : ∀ {r s t : A} -> r ≡ s -> (r + t) ≡ (s + t)
+    +right-congruence : ∀ {r s t : A} -> r ≡ s -> (t + r) ≡ (t + s)
+    *left-congruence  : ∀ {r s t : A} -> r ≡ s -> (r * t) ≡ (s * t)
+    *right-congruence : ∀ {r s t : A} -> r ≡ s -> (t * r) ≡ (t * s)
+
+    +idempotence   : ∀ {r : A}      -> (r + r)       ≡ r
+    +commutativity : ∀ {r s : A}    -> (r + s)       ≡ (s + r)
+    +associativity : ∀ {r s t : A}  -> (r + (s + t)) ≡ ((r + s) + t)
+    +zero-identity : ∀ {r : A}      -> (r + zero)    ≡ r
+
+    *associativity  : ∀ {r s t : A} -> (r * (s * t)) ≡ ((r * s) * t)
+    *left-zero      : ∀ {r : A}     -> (zero * r)    ≡ zero
+    *right-zero     : ∀ {r : A}     -> (r * zero)    ≡ zero
+    *left-identity  : ∀ {r : A}     -> (one * r)     ≡ r
+    *right-identity : ∀ {r : A}     -> (r * one)     ≡ r
+
+    left-distributivity  : ∀ {r s t : A} -> (r * (s + t)) ≡ ((r * s) + (r * t))
+    right-distributivity : ∀ {r s t : A} -> ((r + s) * t) ≡ ((r * t) + (s * t))
+
+  -- For convenience to avoid `Dioid._+_ d r s`
+  plus : A -> A -> A
+  plus x y = x + y
+
+  times : A -> A -> A
+  times x y = x * y

src/Algebra/Dioid/Bool.agda

@@ -1,6 +1,6 @@
 module Algebra.Dioid.Bool where
 
-open import Algebra.Dioid using (Dioid; zero; one; _+_; _*_)
+open import Algebra.Dioid
 
 data Bool : Set where
   true  : Bool
@@ -18,9 +18,3 @@ _ 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

@@ -1,7 +1,6 @@
 module Algebra.Dioid.Bool.Theorems where
 
-open import Algebra.Dioid using (Dioid; zero; one; _+_; _*_)
-import Algebra.Dioid
+open import Algebra.Dioid
 open import Algebra.Dioid.Bool
 
 or-left-congruence : ∀ {b c d : Bool} -> b ≡ c -> (b or d) ≡ (c or d)
@@ -80,22 +79,32 @@ 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
+bool-dioid : Dioid Bool _≡_
+bool-dioid = record
+  { zero = false
+  ; one  = true
+  ; _+_  = _or_
+  ; _*_  = _and_
+  ; reflexivity  = reflexivity
+  ; symmetry     = symmetry
+  ; transitivity = transitivity
+
+  ; +left-congruence  = or-left-congruence
+  ; +right-congruence = or-right-congruence
+  ; *left-congruence  = and-left-congruence
+  ; *right-congruence = and-right-congruence
+
+  ; +idempotence   = or-idempotence
+  ; +commutativity = or-commutativity
+  ; +associativity = or-associativity
+  ; +zero-identity = or-false-identity
+
+  ; *associativity  = and-associativity
+  ; *left-zero      = λ {r} → reflexivity
+  ; *right-zero     = and-right-false
+  ; *left-identity  = and-left-true
+  ; *right-identity = and-right-true
+
+  ; left-distributivity  = left-distributivity
+  ; right-distributivity = right-distributivity
+  }

src/Algebra/Graph/Theorems.agda

@@ -124,3 +124,99 @@ absorption {_} {x} {y} =
 ⊆right-monotony : ∀ {A} {op : BinaryOperator} {x y z : Graph A} -> x ⊆ y -> apply op z x ⊆ apply op z y
 ⊆right-monotony {_} {+op} {x} {y} {z} p = ⊆right-overlay-monotony p
 ⊆right-monotony {_} {*op} {x} {y} {z} p = ⊆right-connect-monotony p
+
+
+-- | Helper theorems
+
+flip-end : ∀ {A} {x y z : Graph A} -> (x + y + z) ≡ (x + z + y)
+flip-end = symmetry +associativity >> R +commutativity >> +associativity
+
+*+ltriple : ∀ {A} {x y z : Graph A} -> (x * (y + z)) ≡ (x * y) + (x * z) + (y + z)
+*+ltriple {_} {x} {y} {z} =
+  begin
+    (x * (y + z)) ≡⟨ left-distributivity ⟩
+    (x * y + x * z) ≡⟨ L (symmetry absorption) ⟩
+    (x * y + x + y + x * z) ≡⟨ R (symmetry absorption) ⟩
+    ((x * y + x + y) + (x * z + x + z)) ≡⟨ symmetry +associativity ⟩
+    ((x * y + x) + (y + (x * z + x + z))) ≡⟨ R +commutativity ⟩
+    ((x * y + x) + ((x * z + x + z) + y)) ≡⟨ symmetry +associativity ⟩
+    (x * y + (x + (x * z + x + z + y))) ≡⟨ R +commutativity ⟩
+    (x * y + (x * z + x + z + y + x)) ≡⟨ R flip-end ⟩
+    (x * y + (x * z + x + z + x + y)) ≡⟨ R (L flip-end) ⟩
+    (x * y + (x * z + x + x + z + y)) ≡⟨ R (L (L (symmetry +associativity >> R +idempotence))) ⟩
+    (x * y + (x * z + x + z + y)) ≡⟨ R (L (L (L (symmetry absorption)))) ⟩
+    (x * y + (x * z + x + z + x + z + y)) ≡⟨ R (L (L flip-end)) ⟩
+    (x * y + (x * z + x + x + z + z + y)) ≡⟨ R (L (L (L (symmetry +associativity >> R +idempotence)))) ⟩
+    (x * y + (x * z + x + z + z + y)) ≡⟨ R (L (L absorption)) ⟩
+    (x * y + (x * z + z + y)) ≡⟨ R (symmetry +associativity) ⟩
+    (x * y + (x * z + (z + y))) ≡⟨ +associativity ⟩
+    (x * y + (x * z) + (z + y)) ≡⟨ +right-congruence +commutativity ⟩
+    (x * y) + (x * z) + (y + z)
+  ∎
+
++*ltriple : ∀ {A} {x y z : Graph A} -> (x + (y * z)) ≡ (x + y) + (x + z) + (y * z)
++*ltriple {_} {x} {y} {z} =
+  begin
+    (x + (y * z)) ≡⟨ R (symmetry absorption) ⟩
+    (x + (y * z + y + z)) ≡⟨ R (symmetry +associativity >> +commutativity) ⟩
+    (x + (y + z + y * z)) ≡⟨ L (symmetry +idempotence) ⟩
+    (x + x + (y + z + y * z)) ≡⟨ +associativity ⟩
+    (x + x + (y + z) + y * z) ≡⟨ L (+associativity) ⟩
+    (x + x + y + z + y * z) ≡⟨ L (L flip-end) ⟩
+    (x + y + x + z + y * z) ≡⟨ L (symmetry +associativity) ⟩
+    (x + y + (x + z) + (y * z))
+  ∎
+
+++ltriple : ∀ {A} {x y z : Graph A} -> (x + (y + z)) ≡ (x + y) + (x + z) + (y + z)
+++ltriple {_} {x} {y} {z} =
+  begin
+    (x + (y + z)) ≡⟨ +associativity ⟩
+    (x + y + z) ≡⟨ L (symmetry +idempotence) ⟩
+    (x + y + (x + y) + z) ≡⟨ symmetry +associativity ⟩
+    (x + y + (x + y + z)) ≡⟨ R flip-end ⟩
+    (x + y + (x + z + y)) ≡⟨ R (L (R (symmetry +idempotence))) ⟩
+    (x + y + (x + (z + z) + y)) ≡⟨ R (L (+associativity)) ⟩
+    (x + y + (x + z + z + y)) ≡⟨ R (symmetry +associativity) ⟩
+    (x + y + ((x + z) + (z + y))) ≡⟨ +associativity ⟩
+    (x + y + (x + z) + (z + y)) ≡⟨ R (+commutativity) ⟩
+    (x + y + (x + z) + (y + z))
+  ∎
+
+*+rtriple : ∀ {A} {x y z : Graph A} -> ((x * y) + z) ≡ (x * y) + (x + z) + (y + z)
+*+rtriple {_} {x} {y} {z} =
+  begin
+    (x * y + z) ≡⟨ L (symmetry absorption) ⟩
+    (x * y + x + y + z) ≡⟨ R (symmetry +idempotence) ⟩
+    (x * y + x + y + (z + z)) ≡⟨ +associativity ⟩
+    (x * y + x + y + z + z) ≡⟨ L flip-end ⟩
+    (x * y + x + z + y + z) ≡⟨ symmetry +associativity ⟩
+    (x * y + x + z + (y + z)) ≡⟨ L (symmetry +associativity) ⟩
+    (x * y + (x + z) + (y + z))
+  ∎
+
++*rtriple : ∀ {A} {x y z : Graph A} -> ((x + y) * z) ≡ (x + y) + (x * z) + (y * z)
++*rtriple {_} {x} {y} {z} =
+  begin
+    ((x + y) * z) ≡⟨ right-distributivity ⟩
+    (x * z + y * z) ≡⟨ L (symmetry absorption) ⟩
+    (x * z + x + z + y * z) ≡⟨ R (symmetry absorption) ⟩
+    (x * z + x + z + (y * z + y + z)) ≡⟨ symmetry (R +associativity) ⟩
+    (x * z + x + z + (y * z + (y + z))) ≡⟨ R +commutativity ⟩
+    (x * z + x + z + (y + z + y * z)) ≡⟨ +associativity ⟩
+    (x * z + x + z + (y + z) + y * z) ≡⟨ L +associativity ⟩
+    (x * z + x + z + y + z + y * z) ≡⟨ L flip-end ⟩
+    (x * z + x + z + z + y + y * z) ≡⟨ L (L (symmetry +associativity)) ⟩
+    (x * z + x + (z + z) + y + y * z) ≡⟨ L (L (R +idempotence)) ⟩
+    (x * z + x + z + y + y * z) ≡⟨ L (L (L (R (symmetry +idempotence)))) ⟩
+    (x * z + (x + x) + z + y + y * z) ≡⟨ L (L (L +associativity)) ⟩
+    (x * z + x + x + z + y + y * z) ≡⟨ L (L (symmetry +associativity)) ⟩
+    (x * z + x + (x + z) + y + y * z) ≡⟨ L (L (R +commutativity)) ⟩
+    (x * z + x + (z + x) + y + y * z) ≡⟨ L (L +associativity)⟩
+    (x * z + x + z + x + y + y * z) ≡⟨ L (L (L absorption)) ⟩
+    (x * z + x + y + y * z) ≡⟨ symmetry (L +associativity) ⟩
+    (x * z + (x + y) + y * z) ≡⟨ L +commutativity ⟩
+    (x + y + (x * z) + (y * z))
+  ∎
+
+++rtriple : ∀ {A} {x y z : Graph A} -> ((x + y) + z) ≡ (x + y) + (x + z) + (y + z)
+++rtriple {_} {x} {y} {z} = symmetry +associativity >> ++ltriple