Mercurial > hg > Papers > 2020 > soto-midterm
comparison src/AgdaNPushNPopProof.agda.replaced @ 1:73127e0ab57c
(none)
| author | soto@cr.ie.u-ryukyu.ac.jp |
|---|---|
| date | Tue, 08 Sep 2020 18:38:08 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| 0:b919985837a3 | 1:73127e0ab57c |
|---|---|
| 1 pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ | |
| 2 pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta | |
| 3 @$\equiv$@ M.exec (n-push n) meta | |
| 4 where | |
| 5 meta = id-meta cn ce s | |
| 6 | |
| 7 pop-n-push : (n cn ce : @$\mathbb{N}$@) @$\rightarrow$@ (s : SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ pop-n-push-type n cn ce s | |
| 8 pop-n-push zero cn ce s = refl | |
| 9 pop-n-push (suc n) cn ce s = begin | |
| 10 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta cn ce s) | |
| 11 @$\equiv$@@$\langle$@ refl @$\rangle$@ | |
| 12 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s) | |
| 13 @$\equiv$@@$\langle$@ exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) @$\rangle$@ | |
| 14 M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) | |
| 15 @$\equiv$@@$\langle$@ cong (\x @$\rightarrow$@ M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) @$\rangle$@ | |
| 16 M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) | |
| 17 @$\equiv$@@$\langle$@ refl @$\rangle$@ | |
| 18 M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) | |
| 19 @$\equiv$@@$\langle$@ sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) @$\rangle$@ | |
| 20 M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) | |
| 21 @$\equiv$@@$\langle$@ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) @$\rangle$@ | |
| 22 M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) | |
| 23 @$\equiv$@@$\langle$@ refl @$\rangle$@ | |
| 24 M.exec (n-push n) (pushOnce (id-meta cn ce s)) | |
| 25 @$\equiv$@@$\langle$@ refl @$\rangle$@ | |
| 26 M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) | |
| 27 @$\equiv$@@$\langle$@ refl @$\rangle$@ | |
| 28 M.exec (n-push (suc n)) (id-meta cn ce s) | |
| 29 @$\blacksquare$@ | |
| 30 | |
| 31 | |
| 32 | |
| 33 n-push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ | |
| 34 n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta @$\equiv$@ meta | |
| 35 where | |
| 36 meta = id-meta cn ce st | |
| 37 | |
| 38 n-push-pop : (n cn ce : @$\mathbb{N}$@) @$\rightarrow$@ (s : SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ n-push-pop-type n cn ce s | |
| 39 n-push-pop zero cn ce s = refl | |
| 40 n-push-pop (suc n) cn ce s = begin | |
| 41 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s) | |
| 42 @$\equiv$@@$\langle$@ refl @$\rangle$@ | |
| 43 M.exec (M.csComp (M.cs (\m @$\rightarrow$@ M.exec (n-pop n) (popOnce m))) (n-push (suc n))) (id-meta cn ce s) | |
| 44 @$\equiv$@@$\langle$@ exec-comp (M.cs (\m @$\rightarrow$@ M.exec (n-pop n) (popOnce m))) (n-push (suc n)) (id-meta cn ce s) @$\rangle$@ | |
| 45 M.exec (M.cs (\m @$\rightarrow$@ M.exec (n-pop n) (popOnce m))) (M.exec (n-push (suc n)) (id-meta cn ce s)) | |
| 46 @$\equiv$@@$\langle$@ refl @$\rangle$@ | |
| 47 M.exec (n-pop n) (popOnce (M.exec (n-push (suc n)) (id-meta cn ce s))) | |
| 48 @$\equiv$@@$\langle$@ refl @$\rangle$@ | |
| 49 M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce s))) | |
| 50 @$\equiv$@@$\langle$@ cong (\x @$\rightarrow$@ M.exec (n-pop n) x) (sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce s))) @$\rangle$@ | |
| 51 M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s)) | |
| 52 @$\equiv$@@$\langle$@ cong (\x @$\rightarrow$@ M.exec (n-pop n) x) (pop-n-push n cn ce s) @$\rangle$@ | |
| 53 M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) | |
| 54 @$\equiv$@@$\langle$@ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) @$\rangle$@ | |
| 55 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) | |
| 56 @$\equiv$@@$\langle$@ n-push-pop n cn ce s @$\rangle$@ | |
| 57 id-meta cn ce s | |
| 58 @$\blacksquare$@ |