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

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
comparison
equal deleted inserted replaced
47:49de29c12c7b 48:fe5755744071
1 module named-product where 1 module named-product where
2
3 2
4 open import Data.Bool 3 open import Data.Bool
5 open import Data.Nat 4 open import Data.Nat
6 open import Data.Nat.Show 5 open import Data.Nat.Show
7 open import Data.String hiding (_++_ ; show) 6 open import Data.String hiding (_++_ ; show ; toList ; fromList)
8 open import Data.List 7 open import Data.List
8 open import Data.AVL.Sets
9 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
10
11
12 10
13 11
14 record Context : Set where 12 record Context : Set where
15 field 13 field
16 cycle : ℕ 14 cycle : ℕ
63 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" } 61 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
64 equiv = refl 62 equiv = refl
65 63
66 64
67 data CodeSegment (A B : Set) : (List Set) -> Set where 65 data CodeSegment (A B : Set) : (List Set) -> Set where
68 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (B ∷ A ∷ l) 66 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B l
69 67
70 BasicCS : Set -> Set -> Set 68 BasicCS : Set -> Set -> Set
71 BasicCS A B = CodeSegment A B (A ∷ B ∷ []) 69 BasicCS A B = CodeSegment A B (A ∷ B ∷ [])
72
73 70
74 71
75 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context 72 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
76 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (get i c)) 73 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (get i c))
77 74
84 csInc : BasicCS LoopCounter LoopCounter 81 csInc : BasicCS LoopCounter LoopCounter
85 csInc = cs inc 82 csInc = cs inc
86 83
87 84
88 85
89
90 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext 86 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext
91 equiv-exec = refl 87 equiv-exec = refl
92 88
93 89
94 csComp : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}} {l ll : List Set} 90 csComp : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}} {l ll : List Set}
95 -> CodeSegment C D (D ∷ C ∷ l) -> CodeSegment A B (B ∷ A ∷ ll) -> CodeSegment A D (D ∷ A ∷ C ∷ B ∷ (l ++ ll)) 91 -> CodeSegment C D l -> CodeSegment A B ll -> CodeSegment A D (l ++ ll)
96 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} {l} {ll} (cs g) (cs f) 92 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} {l} {ll} (cs g) (cs f)
97 = cs {l = (C ∷ B ∷ (l ++ ll))} {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f) 93 = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f)
98
99 94
100 comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ []) 95 comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ [])
101 comp-sample {c} = (csComp {c} csInc csInc) 96 comp-sample {c} = (csComp {c} csInc csInc)
102 97
103 98
104 apply-sample : Context 99 apply-sample : Context
105 apply-sample = exec (comp-sample {firstContext}) firstContext 100 apply-sample = exec (comp-sample {firstContext}) firstContext
106 101
113 csUpdateSignature : BasicCS SignatureWithNum SignatureWithNum 108 csUpdateSignature : BasicCS SignatureWithNum SignatureWithNum
114 csUpdateSignature = cs updateSignature 109 csUpdateSignature = cs updateSignature
115 110
116 111
117 112
118 comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum (SignatureWithNum ∷ LoopCounter ∷ SignatureWithNum ∷ LoopCounter ∷ []) 113 --comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum (SignatureWithNum ∷ LoopCounter ∷ SignatureWithNum ∷ LoopCounter ∷ [])
119 comp-sample-2 {c} = csComp {c} csUpdateSignature csInc 114 --comp-sample-2 = csComp csUpdateSignature csInc
120 115
121 apply-sample-2 : Context 116 --apply-sample-2 : Context
122 apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext 117 --apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext
118
119
120 open ≡-Reasoning
121
122 ++empty : {A : Set} -> (l : List A) -> l ++ [] ≡ l
123 ++empty [] = refl
124 ++empty (x ∷ l) = cong (\l -> x ∷ l) (++empty l)
125
126
127
128 list-associative : {A : Set} -> (l ll lll : List A) -> l ++ (ll ++ lll) ≡ (l ++ ll) ++ lll
129 list-associative [] ll lll = refl
130 list-associative (x ∷ l) [] [] = begin
131 (x ∷ l) ++ [] ++ []
132 ≡⟨ ++empty ((x ∷ l)) ⟩
133 x ∷ l
134 ≡⟨ sym (++empty (x ∷ l)) ⟩
135 x ∷ l ++ []
136 ≡⟨ sym (++empty ((x ∷ l) ++ [])) ⟩
137 ((x ∷ l) ++ []) ++ []
138
139 list-associative (x ∷ l) [] (xxx ∷ lll) = {!!}
140 list-associative (x ∷ l) (x₁ ∷ ll) [] = {!!}
141 list-associative (x ∷ l) (x₁ ∷ ll) (x₂ ∷ lll) = {!!}
142
143
144
145
146
147 comp-associative : {A B C D E F : Set} {l ll lll : List Set} {con : Context}
148 {{da : Datum A}} {{db : Datum B}} {{dc : Datum C}} {{dd : Datum D}} {{de : Datum E}} {{df : Datum F}}
149 -> {a : CodeSegment A B l} {b : CodeSegment C D ll} {c : CodeSegment E F lll}
150 -> csComp {con} c (csComp {con} b a) ≡ {!!} -- csComp (csComp c b) a -- cannot define directly
151 -- csComp c (csComp b a) has CodeSegment A F (lll ++ ll ++ l)
152 -- csComp (csComp c b) a has CodeSegment A F ((lll ++ ll) ++ l)
153 comp-associative = {!!}
154