Mercurial > hg > Members > atton > agda-proofs

annotate cbc/product.agda @ 77:a2e6f61d5f2b default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add modus-ponens
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 06:32:03 +0000
parents dc6a09d4f900
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
26
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module product where
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.String
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Product
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Nat
31
dc6a09d4f900 Prove associativity of code segment composition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
6 open import Data.Unit
26
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Function using (_∘_ ; id)
31
dc6a09d4f900 Prove associativity of code segment composition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
8 open import Relation.Binary.PropositionalEquality
26
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
27
892f8b3aa57e ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
10 data CodeSegment (I O : Set) : Set where
26
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 cs : (I -> O) -> CodeSegment I O
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 twiceWithName : (String × ℕ ) -> (String × ℕ )
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 twiceWithName (s , n) = s , twice n
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 where
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 twice : ℕ -> ℕ
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 twice zero = zero
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 twice (ℕ.suc n₁) = (ℕ.suc (ℕ.suc (twice n₁)))
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 csDouble : CodeSegment (String × ℕ) (String × ℕ)
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 csDouble = cs twiceWithName
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 ods : {I O : Set} -> CodeSegment I O -> Set
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 ods {i} {o} c = o
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 ods-double : ods csDouble
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 ods-double = "hoge" , zero
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 ids : {I O : Set} -> CodeSegment I O -> Set
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 ids {i} {o} c = i
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 ids-double : ids csDouble
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 ids-double = "fuga" , 3
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 --ids-double : {A : Set} {a : A} -> ids csDouble
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 --ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 executeCS : {A B : Set} -> CodeSegment A B -> (A -> B)
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 executeCS (cs b) = b
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 infixr 30 _◎_
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 _◎_ : {A B C : Set} -> CodeSegment A B -> CodeSegment B C -> CodeSegment A C
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 (cs b1) ◎ (cs b2) = cs (b2 ∘ b1)
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 ◎-double : CodeSegment (String × ℕ) (String × ℕ )
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 --◎-double = csDouble ◎ csDouble ◎ csDouble -- ok
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 ◎-double = csDouble ◎ (cs (\s -> tt)) ◎ (cs (\t -> ("yo" , 100))) -- ok
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 --◎-double = csDouble ◎ (cs (\s -> tt)) ◎ csDouble -- ng (valid type check)
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
31
dc6a09d4f900 Prove associativity of code segment composition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
61
dc6a09d4f900 Prove associativity of code segment composition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
62 open ≡-Reasoning
dc6a09d4f900 Prove associativity of code segment composition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
63
dc6a09d4f900 Prove associativity of code segment composition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
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)
dc6a09d4f900 Prove associativity of code segment composition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
65 ◎-associative (cs _) (cs _) (cs _) = refl