Mercurial > hg > Members > atton > agda-proofs

changeset 31:dc6a09d4f900

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove associativity of code segment composition
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 30 Dec 2016 05:35:09 +0000
parents 8ce6a3f51523
children 5af5f1a930bc
files cbc/product.agda
diffstat 1 files changed, 7 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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