Mercurial > hg > Members > atton > agda-proofs

comparison cbc/stack-subtype-sample.agda @ 65:c87e85ffde9a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define n-push/n-pop equiv...
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 14 Jan 2017 05:59:49 +0000
parents 44d448a978d3
children 211fde284b7e
comparison
equal deleted inserted replaced
64:44d448a978d3 65:c87e85ffde9a
199 199
200 200
201 n-push-pop : (n : ℕ) (c : Context) -> 201 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) 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)
203 n-push-pop zero c = push-pop c 203 n-push-pop zero c = push-pop c
204 n-push-pop (suc n) c = begin 204 n-push-pop (suc n) record {n = num ; element = nothing} = begin
205 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta c) 205 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta record {n = num ; element = nothing})
206 ≡⟨ refl ⟩ 206 ≡⟨ refl ⟩
207 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta c) 207 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta record {n = num ; element = nothing})
208 ≡⟨ cong (\f -> M.exec f (id-meta c)) (M.comp-associative (M.cs pushOnce) (n-push (suc n)) (M.cs popOnce) ) ⟩ 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) ) ⟩
209 M.exec (M.csComp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce)) (id-meta c) 209 M.exec (M.csComp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce)) (id-meta record {n = num ; element = nothing})
210 ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce) (id-meta c) ⟩ 210 ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce) (id-meta record {n = num ; element = nothing}) ⟩
211 M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (M.exec (M.cs pushOnce) (id-meta c)) 211 M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = nothing}))
212 ≡⟨ refl ⟩ 212 ≡⟨ refl ⟩
213 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push n) (M.cs pushOnce))) (M.exec (M.cs pushOnce) (id-meta c)) 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}))
214 ≡⟨ {!!} ⟩ 214 ≡⟨ refl ⟩
215 M.exec (n-push (suc n)) (id-meta c) 215 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push n) (M.cs pushOnce))) (id-meta record {n = num ; element = nothing})
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)) ⟩
217 M.exec (M.csComp (M.csComp (M.cs popOnce) (n-push n)) (M.cs pushOnce)) (id-meta record {n = num ; element = nothing})
218 ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push n)) (M.cs pushOnce) (id-meta record {n = num ; element = nothing }) ⟩
219 M.exec (M.csComp (M.cs popOnce) (n-push n)) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = nothing}))
220 ≡⟨ refl ⟩
221 M.exec (M.csComp (M.cs popOnce) (n-push n)) (id-meta record {n = num ; element = nothing})
222 ≡⟨ {!!} ⟩
223 M.exec (n-push (suc n)) (id-meta record {n = num ; element = nothing})
224 ∎
225 n-push-pop (suc n) record {n = num ; element = just x} = begin
226 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta record {n = num ; element = just x})
227 ≡⟨ refl ⟩
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})
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) ) ⟩
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})
231 ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce) (id-meta record {n = num ; element = just x}) ⟩
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}))
233 ≡⟨ 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}))
235 ≡⟨ {!!} ⟩
236 M.exec (n-push (suc n)) (id-meta record {n = num ; element = just x})
216 ∎ 237 ∎
217 238
218 239
219 n-push-pop-equiv : {c : Context} -> (n : ℕ ) 240 n-push-pop-equiv : {c : Context} -> (n : ℕ )
220 -> 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) 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)