# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483076109 0
# Node ID dc6a09d4f90061ad9a033928003ef1ab60ad425c
# Parent  8ce6a3f5152318889491ecfbac869e404f5bd652
Prove associativity of code segment composition

diff -r 8ce6a3f51523 -r dc6a09d4f900 cbc/product.agda
--- a/cbc/product.agda	Fri Dec 30 14:23:22 2016 +0900
+++ b/cbc/product.agda	Fri Dec 30 05:35:09 2016 +0000
@@ -3,8 +3,9 @@
 open import Data.String
 open import Data.Product
 open import Data.Nat
+open import Data.Unit
 open import Function using (_∘_ ; id)
-open import Data.Unit
+open import Relation.Binary.PropositionalEquality
 
 data CodeSegment (I O : Set) : Set where
   cs : (I -> O) -> CodeSegment I O
@@ -57,3 +58,8 @@
 --◎-double = csDouble ◎ (cs (\s -> tt)) ◎ csDouble  -- ng (valid type check)
 
 
+
+open ≡-Reasoning
+
+◎-associative : {A B C D : Set} -> (a : CodeSegment A B) (b : CodeSegment B C) (c : CodeSegment C D) -> (a ◎ b) ◎ c ≡ a ◎ (b ◎ c)
+◎-associative (cs _) (cs _) (cs _) = refl