Mercurial > hg > Members > atton > agda-proofs
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 |