Mercurial > hg > Members > atton > agda-proofs

annotate cbc/named-product.agda @ 48:fe5755744071

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying prove associativity of composition of code segments
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 05 Jan 2017 07:01:32 +0000
parents 49de29c12c7b
children 8031568638d0
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module named-product where
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
3 open import Data.Bool
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Nat
45
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
5 open import Data.Nat.Show
48
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
6 open import Data.String hiding (_++_ ; show ; toList ; fromList)
41
2abf1cd97f10 Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
7 open import Data.List
48
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
8 open import Data.AVL.Sets
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
9 open import Relation.Binary.PropositionalEquality
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
10
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
12 record Context : Set where
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
13 field
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
14 cycle : ℕ
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
15 led : String
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
16 signature : String
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
17
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
18 record Datum (A : Set) : Set where
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
19 field
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
20 get : Context -> A
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
21 set : Context -> A -> Context
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
22 open Datum
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
23
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
24 record LoopCounter : Set where
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 field
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
26 count : ℕ
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
27 name : String
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
29 record SignatureWithNum : Set where
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 field
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 signature : String
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
32 num : ℕ
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
33
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 instance
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
35 contextHasLoopCounter : Datum LoopCounter
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
36 contextHasLoopCounter = record {get = (\c -> record {count = Context.cycle c ;
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
37 name = Context.led c });
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
38 set = (\c l -> record {cycle = LoopCounter.count l;
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
39 led = LoopCounter.name l;
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
40 signature = Context.signature c})}
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
41 contextHasSignatureWithNum : Datum SignatureWithNum
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
42 contextHasSignatureWithNum = record {get = (\c -> record { signature = Context.signature c
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
43 ; num = Context.cycle c})
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
44 ;set = (\c s -> record { cycle = SignatureWithNum.num s
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
45 ; led = Context.led c
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
46 ; signature = SignatureWithNum.signature s})
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
47 }
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
49
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
50 inc : LoopCounter -> LoopCounter
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
51 inc l = record l {count = suc (LoopCounter.count l)}
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 firstContext : Context
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
56
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
57 incContextCycle : {{_ : Datum LoopCounter }} -> Context -> Context
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
58 incContextCycle {{l}} c = Datum.set l c (inc (Datum.get l c))
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
38
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
61 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
a0ca5e29a9dc Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
62 equiv = refl
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
64
41
2abf1cd97f10 Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
65 data CodeSegment (A B : Set) : (List Set) -> Set where
48
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
66 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B l
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
67
48
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
68 BasicCS : Set -> Set -> Set
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
69 BasicCS A B = CodeSegment A B (A ∷ B ∷ [])
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
70
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
71
42
f7916d13e2b1 Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
72 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
73 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (get i c))
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
74
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
75
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
76 comp : {con : Context} -> {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}}
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
77 -> (C -> D) -> (A -> B) -> A -> D
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
78 comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
79
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
80
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
81 csInc : BasicCS LoopCounter LoopCounter
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
82 csInc = cs inc
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
83
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
84
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
85
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
86 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext
42
f7916d13e2b1 Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
87 equiv-exec = refl
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
88
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
90 csComp : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}} {l ll : List Set}
48
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
91 -> CodeSegment C D l -> CodeSegment A B ll -> CodeSegment A D (l ++ ll)
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
92 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} {l} {ll} (cs g) (cs f)
48
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
93 = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f)
42
f7916d13e2b1 Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
94
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
95 comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ [])
48
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
96 comp-sample {c} = (csComp {c} csInc csInc)
44
72cf35fb82af Add composition sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
97
46
af1fe3bd9f1e Define code segment compose operator using type -> ds cast
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 45
diff changeset
98
44
72cf35fb82af Add composition sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
99 apply-sample : Context
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
100 apply-sample = exec (comp-sample {firstContext}) firstContext
45
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
101
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
102
45
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
103
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
104 updateSignature : SignatureWithNum -> SignatureWithNum
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
105 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num}
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
106
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
107
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
108 csUpdateSignature : BasicCS SignatureWithNum SignatureWithNum
45
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
109 csUpdateSignature = cs updateSignature
08b695ca359c Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
110
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
111
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
112
48
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
113 --comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum (SignatureWithNum ∷ LoopCounter ∷ SignatureWithNum ∷ LoopCounter ∷ [])
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
114 --comp-sample-2 = csComp csUpdateSignature csInc
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
115
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
116 --apply-sample-2 : Context
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
117 --apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
118
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
119
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
120 open ≡-Reasoning
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
121
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
122 ++empty : {A : Set} -> (l : List A) -> l ++ [] ≡ l
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
123 ++empty [] = refl
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
124 ++empty (x ∷ l) = cong (\l -> x ∷ l) (++empty l)
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
125
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
126
47
49de29c12c7b Define code segment compose operator using type -> ds cast!
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
127
48
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
128 list-associative : {A : Set} -> (l ll lll : List A) -> l ++ (ll ++ lll) ≡ (l ++ ll) ++ lll
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
129 list-associative [] ll lll = refl
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
130 list-associative (x ∷ l) [] [] = begin
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
131 (x ∷ l) ++ [] ++ []
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
132 ≡⟨ ++empty ((x ∷ l)) ⟩
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
133 x ∷ l
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
134 ≡⟨ sym (++empty (x ∷ l)) ⟩
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
135 x ∷ l ++ []
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
136 ≡⟨ sym (++empty ((x ∷ l) ++ [])) ⟩
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
137 ((x ∷ l) ++ []) ++ []
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
138 ∎
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
139 list-associative (x ∷ l) [] (xxx ∷ lll) = {!!}
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
140 list-associative (x ∷ l) (x₁ ∷ ll) [] = {!!}
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
141 list-associative (x ∷ l) (x₁ ∷ ll) (x₂ ∷ lll) = {!!}
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
142
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
143
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
144
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
145
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
146
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
147 comp-associative : {A B C D E F : Set} {l ll lll : List Set} {con : Context}
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
148 {{da : Datum A}} {{db : Datum B}} {{dc : Datum C}} {{dd : Datum D}} {{de : Datum E}} {{df : Datum F}}
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
149 -> {a : CodeSegment A B l} {b : CodeSegment C D ll} {c : CodeSegment E F lll}
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
150 -> csComp {con} c (csComp {con} b a) ≡ {!!} -- csComp (csComp c b) a -- cannot define directly
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
151 -- csComp c (csComp b a) has CodeSegment A F (lll ++ ll ++ l)
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
152 -- csComp (csComp c b) a has CodeSegment A F ((lll ++ ll) ++ l)
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
153 comp-associative = {!!}
fe5755744071 Trying prove associativity of composition of code segments
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 47
diff changeset
154