Mercurial > hg > Papers > 2021 > soto-prosym
diff Paper/src/AgdaNPushNPopProof.agda.replaced @ 0:c59202657321
init
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 02 Nov 2021 06:55:58 +0900 |
| parents | |
| children | 339fb67b4375 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/AgdaNPushNPopProof.agda.replaced Tue Nov 02 06:55:58 2021 +0900 @@ -0,0 +1,58 @@ +pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ +pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta + @$\equiv$@ M.exec (n-push n) meta + where + meta = id-meta cn ce s + +pop-n-push : (n cn ce : @$\mathbb{N}$@) @$\rightarrow$@ (s : SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ pop-n-push-type n cn ce s +pop-n-push zero cn ce s = refl +pop-n-push (suc n) cn ce s = begin + M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta cn ce s) + @$\equiv$@@$\langle$@ refl @$\rangle$@ + M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s) + @$\equiv$@@$\langle$@ exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) @$\rangle$@ + M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) + @$\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$@ + M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) + @$\equiv$@@$\langle$@ refl @$\rangle$@ + M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) + @$\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$@ + M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) + @$\equiv$@@$\langle$@ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) @$\rangle$@ + M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) + @$\equiv$@@$\langle$@ refl @$\rangle$@ + M.exec (n-push n) (pushOnce (id-meta cn ce s)) + @$\equiv$@@$\langle$@ refl @$\rangle$@ + M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) + @$\equiv$@@$\langle$@ refl @$\rangle$@ + M.exec (n-push (suc n)) (id-meta cn ce s) + @$\blacksquare$@ + + + +n-push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ +n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta @$\equiv$@ meta + where + meta = id-meta cn ce st + +n-push-pop : (n cn ce : @$\mathbb{N}$@) @$\rightarrow$@ (s : SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ n-push-pop-type n cn ce s +n-push-pop zero cn ce s = refl +n-push-pop (suc n) cn ce s = begin + M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s) + @$\equiv$@@$\langle$@ refl @$\rangle$@ + M.exec (M.csComp (M.cs (\m @$\rightarrow$@ M.exec (n-pop n) (popOnce m))) (n-push (suc n))) (id-meta cn ce s) + @$\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$@ + M.exec (M.cs (\m @$\rightarrow$@ M.exec (n-pop n) (popOnce m))) (M.exec (n-push (suc n)) (id-meta cn ce s)) + @$\equiv$@@$\langle$@ refl @$\rangle$@ + M.exec (n-pop n) (popOnce (M.exec (n-push (suc n)) (id-meta cn ce s))) + @$\equiv$@@$\langle$@ refl @$\rangle$@ + M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce s))) + @$\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$@ + M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s)) + @$\equiv$@@$\langle$@ cong (\x @$\rightarrow$@ M.exec (n-pop n) x) (pop-n-push n cn ce s) @$\rangle$@ + M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) + @$\equiv$@@$\langle$@ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) @$\rangle$@ + M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) + @$\equiv$@@$\langle$@ n-push-pop n cn ce s @$\rangle$@ + id-meta cn ce s + @$\blacksquare$@