# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486192763 -32400
# Node ID ec6799ca9d4230ba102041b4c4a5193657c1de92
# Parent  40ae32725e55c3302eedd6a8884fcfefd179e4c6
Add proof description

diff -r 40ae32725e55 -r ec6799ca9d42 paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed
diff -r 40ae32725e55 -r ec6799ca9d42 paper/cbc-type.tex
--- a/paper/cbc-type.tex	Sat Feb 04 12:23:25 2017 +0900
+++ b/paper/cbc-type.tex	Sat Feb 04 16:19:23 2017 +0900
@@ -258,6 +258,7 @@
 
 % }}}
 
+% {{{ スタックの実装の検証
 \section{スタックの実装の検証}
 定義した SingleLinkedStack に対して証明を行なっていく。
 ここでの証明は SingleLinkedStack の処理が特定の性質を持つことを保証することである。
@@ -369,4 +370,70 @@
 実装が異なれば、同様の性質でも証明は異なるものとなる。
 このように、実装そのものを適切に型システムで定義できれば、明示されていない実装依存の仕様も証明時に確定させることができる。
 
-// n-pop / n-push
+証明した定理をより一般的な「任意の自然数回だけスタックへ値を積み、その後同じ回数スタックから値を取り出すとスタックは操作前と変わらない」という形に拡張する。
+この性質を Agda で定義するとリスト~\ref{src:agda-n-push-n-pop}のようになる。
+自然数n回だけ push/pop することを記述するために Agda 上に \verb/n-push/ 関数と \verb/n-pop/ 関数を定義している。
+それぞれ一度操作を行なった後に再帰的に自身を呼び出す再帰関数である。
+
+\lstinputlisting[label=src:agda-n-push-n-pop, caption=Agda におけるスタックの性質の定義(2)] {src/AgdaNPushNPop.agda.replaced}
+
+この性質の証明は少々複雑である。
+結論から先に示すとリスト~\ref{src:agda-n-push-n-pop-proof}のように証明できる。
+
+\lstinputlisting[label=src:agda-n-push-n-pop-proof, caption=Agda におけるスタックの性質の証明(2)] {src/AgdaNPushNPopProof.agda.replaced}
+
+これは以下のような形の証明になっている。
+
+\begin{itemize}
+    \item 「n回pushした後にn回popしても同様になる」という定理を \verb/n-push-pop/ とおく。
+    \item \verb/n-push-pop/ は自然数nと特定の \verb/Meta/ に対して \verb/exec (n-pop (suc n)) . (n-push (suc n))) m = m/ が成り立つことである
+    \item 特定の \verb/Meta/ とは、 push/pop 操作の後の継続が DataSegment を変更しない \verb/Meta/ である。
+    \item また、簡略化のために \verb/csComp/ による CodeSegment の合成を二項演算子 \verb/./ とおく
+        \begin{itemize}
+            \item 例えば \verb/exec (csComp f g) x/ は \verb/exec (f . g) x/ となる。
+        \end{itemize}
+
+    \item \verb/n-push-pop/ を証明するための補題 \verb/pop-n-push/ を定義する
+    \item \verb/n-push-pop/ とは「n+1回push して1回 pop することは、n回pushすることと等しい」という補題である。
+    \item \verb/n-push-pop/ は \verb/exec (pop . n-push (suc n)) m = exec (n-push n) m/ と表現できる。
+    \item \verb/n-push-pop/ の n が zero の時は直ちに成り立つ。
+    \item \verb/n-push-pop/ の n が zero でない時(suc n である時)は以下のように証明できる。
+
+        \begin{itemize}
+            \item \verb/exec (n-push (suc n)) m/ を \verb/X/ とおく
+            \item \verb/exec (pop . n-push (suc (suc n))) m = X/
+            \item n-push の定義より \verb/exec (pop . (n-push (suc n) . push)) m = X/
+            \item 補題 exec-comp より \verb/exec (pop (exec (n-push (suc n) . push) m)) = X/
+            \item 補題 exec-comp より \verb/exec (pop (exec (n-push (suc n) (exec push m)))) = X/
+            \item 一度pushした結果を \verb/m'/とおくと \verb/exec (pop (exec (n-push (suc n) m'))) = X/
+            \item \verb/n-push-pop/ より \verb/exec (exec (n-push n m')) = X/
+            \item push の定義より \verb/exec (exec (n-push n (exec push m))) = X/
+            \item n-push の定義より \verb/exec (exec (n-push (suc n) m) = X/ となる
+            \item 全く同一の項に変更できたので証明終了
+        \end{itemize}
+
+
+    \item 次に \verb/n-push-pop/ の証明を示す。
+    \item \verb/n-push-pop/ の n が zero の時は、 \verb/suc zero/ 回の push/pop が行なわれるため、\verb/push-pop/より成り立つ。
+    \item \verb/n-push-pop/ の n が zero でない時は以下により証明できる。
+
+        \begin{itemize}
+            \item \verb/exec ((n-pop (suc n)) . (n-push (suc n))) m = m / を示せれば良い。
+            \item \verb/X/ に注目した時 n-pop の定義より \verb/exec (n-pop n) . pop . (n-push (suc n)) m = m/
+            \item exec-comp より \verb/exec (n-pop n) (exec pop (n-push (suc n)) m) = m/
+            \item exec-comp より \verb/exec (n-pop n) (exec pop (exec (n-push (suc n)) m)) = m/
+            \item exec-comp より \verb/exec (n-pop n) (exec pop . (n-push (suc n)) m) = m/
+            \item pop-n-push より \verb/exec (n-pop n) (exec (n-push n) m) = m/
+            \item n-push-pop より \verb/m = m/ となり証明終了。
+            \item なお、n-push-pop は (suc n) が n に減少するため、確実に停止することから自身を自身の証明に適用している。
+        \end{itemize}
+\end{itemize}
+
+push-pop を一般化した n-push-pop を証明することができた。
+n-push-pop は証明の途中で補題 pop-n-push と push-pop を利用した定理である。
+このように、CbC で記述されたプログラムを Agda 上に記述することで、データ構造の性質を定理として証明することができた。
+これらの証明機構を CbC のコンパイラやランタイム、モデルチェッカなどに組み込むことにより CbC は CbC で記述されたコードを証明することができるようになる。
+なお、本論文で取り扱っている Agda のソースコードは視認性の向上のために暗黙的な引数を省略して記述している。
+動作する完全なコードは付録に付す。 % TODO: ふろく
+
+% }}}
diff -r 40ae32725e55 -r ec6799ca9d42 paper/src/AgdaNPushNPop.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaNPushNPop.agda	Sat Feb 04 16:19:23 2017 +0900
@@ -0,0 +1,13 @@
+n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
+n-push {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m))
+
+n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
+n-pop {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m))
+
+pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
+pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta
+                         ≡ M.exec (n-push {meta} n) meta
+  where
+    meta = id-meta cn ce s
diff -r 40ae32725e55 -r ec6799ca9d42 paper/src/AgdaNPushNPopProof.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaNPushNPopProof.agda	Sat Feb 04 16:19:23 2017 +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
+  ∎