Mercurial > hg > Papers > 2020 > soto-midterm
diff src/AgdaNPushNPopProof.agda @ 1:73127e0ab57c
(none)
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 08 Sep 2020 18:38:08 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/AgdaNPushNPopProof.agda Tue Sep 08 18:38:08 2020 +0900 @@ -0,0 +1,58 @@ +pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ +pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta + ≡ M.exec (n-push n) meta + where + meta = id-meta cn ce s + +pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> 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) + ≡⟨ refl ⟩ + M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s) + ≡⟨ exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩ + M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) + ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩ + M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) + ≡⟨ refl ⟩ + M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) + ≡⟨ sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩ + M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) + ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩ + M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) + ≡⟨ refl ⟩ + M.exec (n-push n) (pushOnce (id-meta cn ce s)) + ≡⟨ refl ⟩ + M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) + ≡⟨ refl ⟩ + M.exec (n-push (suc n)) (id-meta cn ce s) + ∎ + + + +n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ +n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta ≡ meta + where + meta = id-meta cn ce st + +n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> 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) + ≡⟨ refl ⟩ + M.exec (M.csComp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n))) (id-meta cn ce s) + ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n)) (id-meta cn ce s) ⟩ + M.exec (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (M.exec (n-push (suc n)) (id-meta cn ce s)) + ≡⟨ refl ⟩ + M.exec (n-pop n) (popOnce (M.exec (n-push (suc n)) (id-meta cn ce s))) + ≡⟨ refl ⟩ + M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce s))) + ≡⟨ cong (\x -> M.exec (n-pop n) x) (sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce s))) ⟩ + M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s)) + ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩ + M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) + ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩ + M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) + ≡⟨ n-push-pop n cn ce s ⟩ + id-meta cn ce s + ∎