Mercurial > hg > Members > atton > agda-proofs

comparison cbc/stack-subtype-sample.agda @ 66:211fde284b7e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying prove n-push/n-pop
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 15 Jan 2017 02:33:47 +0000
parents c87e85ffde9a
children ee2659635734
comparison
equal deleted inserted replaced
65:c87e85ffde9a 66:211fde284b7e
85 pushOnce : Meta -> Meta 85 pushOnce : Meta -> Meta
86 pushOnce m = M.exec pushSingleLinkedStackCS m 86 pushOnce m = M.exec pushSingleLinkedStackCS m
87 87
88 n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta 88 n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
89 n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id 89 n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id
90 n-push {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-push {m} {{mm}} n) (M.cs {{mm}} {{mm}} pushOnce) 90 n-push {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-push {m} {{mm}} n) (M.cs {{mm}} {{mm}} pushOnce)
91 91
92 popOnce : Meta -> Meta 92 popOnce : Meta -> Meta
93 popOnce m = M.exec popSingleLinkedStackCS m 93 popOnce m = M.exec popSingleLinkedStackCS m
94 94
95 n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta 95 n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
157 -} 157 -}
158 158
159 159
160 160
161 161
162 id-meta : Context -> Meta 162 id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta
163 id-meta c = record { context = c ; nextCS = (N.cs id) ; stack = record {top = nothing}} 163 id-meta n e s = record { context = record {n = n ; element = just e}
164 164 ; nextCS = (N.cs id) ; stack = s}
165 165
166 push-pop : (c : Context) -> M.exec (M.csComp {id-meta c} (M.cs popOnce) (M.cs pushOnce)) (id-meta c) ≡ id-meta c 166 exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) -> M.exec (M.csComp {m} f g) m ≡ M.exec f (M.exec g m)
167 push-pop record { n = n ; element = (just x) } = refl 167 exec-comp (M.cs x) (M.cs _) m = refl
168 push-pop record { n = n ; element = nothing } = refl 168
169
170 push-pop-type : ℕ -> ℕ -> ℕ -> Element ℕ -> Set₁
171 push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
172 where
173 meta = id-meta n e record {top = just (cons x (just s))}
174
175 push-pop : (n e x : ℕ) -> (s : Element ℕ) -> push-pop-type n e x s
176 push-pop n e x s = refl
177
178
179
180 {-
169 {- 181 {-
170 n-pop-pop-once-n-push : (n : ℕ) (c : Context) -> 182 n-pop-pop-once-n-push : (n : ℕ) (c : Context) ->
171 M.exec (M.csComp {id-meta c} (M.csComp {id-meta c} (n-pop {id-meta c} n) (M.cs popOnce)) (n-push {id-meta c} (suc n))) (id-meta c) 183 M.exec (M.csComp {id-meta c} (M.csComp {id-meta c} (n-pop {id-meta c} n) (M.cs popOnce)) (n-push {id-meta c} (suc n))) (id-meta c)
172 ≡ 184 ≡
173 M.exec (M.csComp {id-meta c} (n-pop {id-meta c} n) (n-push {id-meta c} n)) (id-meta c) 185 M.exec (M.csComp {id-meta c} (n-pop {id-meta c} n) (n-push {id-meta c} n)) (id-meta c)
191 ≡⟨ {!!} ⟩ 203 ≡⟨ {!!} ⟩
192 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta c) 204 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta c)
193 ∎ 205 ∎
194 -} 206 -}
195 207
196 exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) -> M.exec (M.csComp {m} f g) m ≡ M.exec f (M.exec g m)
197 exec-comp (M.cs x) (M.cs _) m = refl
198 208
199 209
200 210
201 n-push-pop : (n : ℕ) (c : Context) -> 211 n-push-pop : (n : ℕ) (c : Context) ->
202 (M.exec (M.csComp {id-meta c} (M.cs popOnce) (n-push {id-meta c} (suc n))) (id-meta c)) ≡ M.exec (n-push {id-meta c} n) (id-meta c) 212 (M.exec (M.csComp {id-meta c} (M.cs popOnce) (n-push {id-meta c} (suc n))) (id-meta c)) ≡ M.exec (n-push {id-meta c} n) (id-meta c)
203 n-push-pop zero c = push-pop c 213 n-push-pop zero c = push-pop c
204 n-push-pop (suc n) record {n = num ; element = nothing} = begin 214 n-push-pop (suc n) c = {!!}
205 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta record {n = num ; element = nothing}) 215 -}
206 ≡⟨ refl ⟩ 216
207 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta record {n = num ; element = nothing}) 217 pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
208 ≡⟨ cong (\f -> M.exec f (id-meta record {n = num ; element = nothing})) (M.comp-associative (M.cs pushOnce) (n-push (suc n)) (M.cs popOnce) ) ⟩ 218 pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta
209 M.exec (M.csComp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce)) (id-meta record {n = num ; element = nothing}) 219 ≡ M.exec (n-push {meta} n) meta
210 ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce) (id-meta record {n = num ; element = nothing}) ⟩ 220 where
211 M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = nothing})) 221 meta = id-meta cn ce s
212 ≡⟨ refl ⟩ 222
213 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push n) (M.cs pushOnce))) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = nothing})) 223 pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s
214 ≡⟨ refl ⟩ 224 pop-n-push zero cn ce s = refl
215 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push n) (M.cs pushOnce))) (id-meta record {n = num ; element = nothing}) 225 pop-n-push (suc n) cn ce s = begin
216 ≡⟨ cong (\f -> M.exec f (id-meta record {n = num ; element = nothing})) (M.comp-associative (M.cs pushOnce) (n-push n) (M.cs popOnce)) ⟩ 226 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta cn ce s)
217 M.exec (M.csComp (M.csComp (M.cs popOnce) (n-push n)) (M.cs pushOnce)) (id-meta record {n = num ; element = nothing}) 227 ≡⟨ refl ⟩
218 ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push n)) (M.cs pushOnce) (id-meta record {n = num ; element = nothing }) ⟩ 228 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s)
219 M.exec (M.csComp (M.cs popOnce) (n-push n)) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = nothing})) 229 ≡⟨ exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩
220 ≡⟨ refl ⟩ 230 M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s))
221 M.exec (M.csComp (M.cs popOnce) (n-push n)) (id-meta record {n = num ; element = nothing}) 231 ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩
222 ≡⟨ {!!} ⟩ 232 M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s)))
223 M.exec (n-push (suc n)) (id-meta record {n = num ; element = nothing}) 233 ≡⟨ refl ⟩
224 ∎ 234 M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (record { nextCS = (N.cs id) ;
225 n-push-pop (suc n) record {n = num ; element = just x} = begin 235 context = record {n = cn ; element = just ce} ;
226 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta record {n = num ; element = just x}) 236 stack = record {top = just (cons ce (SingleLinkedStack.top s)) }
227 ≡⟨ refl ⟩ 237 }))
228 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta record {n = num ; element = just x}) 238 ≡⟨ {!!} ⟩
229 ≡⟨ cong (\f -> M.exec f (id-meta record {n = num ; element = just x})) (M.comp-associative (M.cs pushOnce) (n-push (suc n)) (M.cs popOnce) ) ⟩ 239 M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) ?
230 M.exec (M.csComp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce)) (id-meta record {n = num ; element = just x}) 240 ≡⟨ {!!} ⟩
231 ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce) (id-meta record {n = num ; element = just x}) ⟩ 241 M.exec (n-push n) (record { nextCS = (N.cs id) ; context = record {n = cn ; element = just ce} ;
232 M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = just x})) 242 stack = record {top = just (cons ce (SingleLinkedStack.top s))}})
233 ≡⟨ refl ⟩ 243 ≡⟨ refl ⟩
234 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push n) (M.cs pushOnce))) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = just x})) 244 M.exec (n-push n) (pushOnce (id-meta cn ce s))
235 ≡⟨ {!!} ⟩ 245 ≡⟨ refl ⟩
236 M.exec (n-push (suc n)) (id-meta record {n = num ; element = just x}) 246 M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s))
237 ∎ 247 ≡⟨ sym (exec-comp (n-push n) (M.cs pushOnce) (id-meta cn ce s)) ⟩
238 248 M.exec (M.csComp (n-push n) (M.cs pushOnce)) (id-meta cn ce s)
239 249 ≡⟨ refl ⟩
250 M.exec (n-push (suc n)) (id-meta cn ce s)
251 ∎
252
253
254 n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
255 n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta ≡ meta
256 where
257 meta = id-meta cn ce st
258
259 n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s
260 n-push-pop zero cn ce s = refl
261 n-push-pop (suc n) cn ce s = begin
262 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s)
263 ≡⟨ refl ⟩
264 M.exec (M.csComp (M.csComp (n-pop n) (M.cs popOnce)) (n-push (suc n))) (id-meta cn ce s)
265 ≡⟨ cong (\f -> M.exec f (id-meta cn ce s)) (sym (M.comp-associative (n-push (suc n)) (M.cs popOnce) (n-pop n))) ⟩
266 M.exec (M.csComp (n-pop n) (M.csComp (M.cs popOnce) (n-push (suc n)))) (id-meta cn ce s)
267 ≡⟨ exec-comp (n-pop n) (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s) ⟩
268 M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s))
269 ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩
270 M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s))
271 ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩
272 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s)
273 ≡⟨ n-push-pop n cn ce s ⟩
274 id-meta cn ce s
275 ∎
276
277 {-
240 n-push-pop-equiv : {c : Context} -> (n : ℕ ) 278 n-push-pop-equiv : {c : Context} -> (n : ℕ )
241 -> M.exec (M.csComp {id-meta c} (n-pop {id-meta c} n) (n-push {id-meta c} n)) (id-meta c) ≡ (id-meta c) 279 -> M.exec (M.csComp {id-meta c} (n-pop {id-meta c} n) (n-push {id-meta c} n)) (id-meta c) ≡ (id-meta c)
242 n-push-pop-equiv zero = refl 280 n-push-pop-equiv zero = refl
243 n-push-pop-equiv {c} (suc n) = begin 281 n-push-pop-equiv {c} (suc n) = begin
244 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta c) 282 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta c)
253 ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta c)) ⟩ 291 ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta c)) ⟩
254 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta c) 292 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta c)
255 ≡⟨ n-push-pop-equiv n ⟩ 293 ≡⟨ n-push-pop-equiv n ⟩
256 id-meta c 294 id-meta c
257 ∎ 295 ∎
296
297 -}