Mercurial > hg > Members > atton > agda-proofs

comparison cbc/product.agda @ 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 892f8b3aa57e
children
comparison
equal deleted inserted replaced
30:8ce6a3f51523 31:dc6a09d4f900
1 module product where 1 module product where
2 2
3 open import Data.String 3 open import Data.String
4 open import Data.Product 4 open import Data.Product
5 open import Data.Nat 5 open import Data.Nat
6 open import Data.Unit
6 open import Function using (_∘_ ; id) 7 open import Function using (_∘_ ; id)
7 open import Data.Unit 8 open import Relation.Binary.PropositionalEquality
8 9
9 data CodeSegment (I O : Set) : Set where 10 data CodeSegment (I O : Set) : Set where
10 cs : (I -> O) -> CodeSegment I O 11 cs : (I -> O) -> CodeSegment I O
11 12
12 13
55 --◎-double = csDouble ◎ csDouble ◎ csDouble -- ok 56 --◎-double = csDouble ◎ csDouble ◎ csDouble -- ok
56 ◎-double = csDouble ◎ (cs (\s -> tt)) ◎ (cs (\t -> ("yo" , 100))) -- ok 57 ◎-double = csDouble ◎ (cs (\s -> tt)) ◎ (cs (\t -> ("yo" , 100))) -- ok
57 --◎-double = csDouble ◎ (cs (\s -> tt)) ◎ csDouble -- ng (valid type check) 58 --◎-double = csDouble ◎ (cs (\s -> tt)) ◎ csDouble -- ng (valid type check)
58 59
59 60
61
62 open ≡-Reasoning
63
64 ◎-associative : {A B C D : Set} -> (a : CodeSegment A B) (b : CodeSegment B C) (c : CodeSegment C D) -> (a ◎ b) ◎ c ≡ a ◎ (b ◎ c)
65 ◎-associative (cs _) (cs _) (cs _) = refl