# HG changeset patch
# User ryokka
# Date 1519035073 -32400
# Node ID d927f6b3d2b362ef053842117fc71addbdd87a81
# Parent  eafc166804f329688e87eadec2d4629cb17680f4
del tree-proof sub-proof

diff -r eafc166804f3 -r d927f6b3d2b3 final_main/chapter4.tex
--- a/final_main/chapter4.tex	Mon Feb 19 18:44:59 2018 +0900
+++ b/final_main/chapter4.tex	Mon Feb 19 19:11:13 2018 +0900
@@ -108,8 +108,8 @@
 interface は record で列挙し、ソースコード~\ref{src:agda-interface}のように紐付けることができる。
 CbC とは異なり、 Agda では型を明記する必要があるため record 内に型を記述している。
 
-例として Agda で実装した Stack 上の interface (ソースコード\ref{agda-interface})を見る。
-Stack の実装は SingleLinkedStack(ソースコード\ref{agda-single-linked-stack}) として書かれている。それを Stack 側から
+例として Agda で実装した Stack 上の interface (ソースコード\ref{src:agda-interface})を見る。
+Stack の実装は SingleLinkedStack(ソースコード\ref{src:agda-single-linked-stack}) として書かれている。それを Stack 側から
 interface を通して呼び出している。
 
 ここでの interface の型は Stack の record 内にある pushStack や popStack などで、
@@ -144,12 +144,12 @@
 作をしているかを確認するために行なった手法を幾つか示す。
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-今回は実験中にソースコード~\ref{src:agda-stack-test}のような Test を書いた。
+今回は実験中にソースコード\ref{src:agda-stack-test}のような Test を書いた。
 この Test では Stack をターゲットにしていて、 Stack に1、 2の二つの$ \mathbb{N} $型のデー
 タを push した後、 pop2 Interface を使って Stack に入っている 1、 2 が Stack の
-FILO の定義通り 2、 1 の順で取り出せるかを確認するために作成した。
+定義である First in Last out の通りに 2、 1 の順で取り出せるかを確認するために作成した。
 
-\lstinputlisting[label=agda-stack-test, caption=Agdaにおけるテスト]{src/AgdaStackTest.agda.replaced}
+\lstinputlisting[label=src:agda-stack-test, caption=Agdaにおけるテスト]{src/AgdaStackTest.agda.replaced}
 
 上の Test では、02 が 2つのデータを push し、 03 で 二つのデータを pop する pop2
 を行っている。それらをまとめて記述したものが 04 で 2 回 push し、 2つのデータを pop する動
diff -r eafc166804f3 -r d927f6b3d2b3 final_main/chapter5.tex
--- a/final_main/chapter5.tex	Mon Feb 19 18:44:59 2018 +0900
+++ b/final_main/chapter5.tex	Mon Feb 19 19:11:13 2018 +0900
@@ -10,7 +10,7 @@
 % んな感じにするとできるのでは？っていう感じにしよ
 
 \section{Agda による Interface 部分を含めた Stack の部分的な証明}
-\label{agda-interface-stack}
+\label{src:agda-interface-stack}
 
 % Stack の仕様記述
 ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。
@@ -40,7 +40,7 @@
  2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明してい
  る。
 
- \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義とpush->push->pop2 の証明]{src/AgdaStackSomeState.agda.replaced}
+ \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda.replaced}
  
 % Agda でも継続を使った書き方で Interface 部分の実装を示した。
 
@@ -66,7 +66,7 @@
 \begin{itemize}
  \item Tree に対して Node を Put することができる。
  \item Tree に Put された Node は Delete されるまでなくならない。
- \item Tree に 存在する Node とその子の関係は必ず「右の子 > Node」かつ「Node > 左の子」の関係になっている。
+ \item Tree に 存在する Node とその子の関係は必ず「右の子 $>$ Node」かつ「Node $>$ 左の子」の関係になっている。
  \item どのような状態の Tree に値を put しても Node と子の関係は保たれる
  \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。
 \end{itemize}
@@ -112,7 +112,6 @@
 
 % Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
 % 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。
-pp
 %%
 % 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導
 % 入した。
diff -r eafc166804f3 -r d927f6b3d2b3 final_main/main.pdf
Binary file final_main/main.pdf has changed
diff -r eafc166804f3 -r d927f6b3d2b3 final_main/src/AgdaTreeProof.agda
--- a/final_main/src/AgdaTreeProof.agda	Mon Feb 19 18:44:59 2018 +0900
+++ b/final_main/src/AgdaTreeProof.agda	Mon Feb 19 19:11:13 2018 +0900
@@ -1,43 +1,6 @@
 redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ
 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
 
-putTest1Lemma2 : (k : ℕ)  -> compare2 k k ≡ EQ
-putTest1Lemma2 zero = refl
-putTest1Lemma2 (suc k) = putTest1Lemma2 k
-
-putTest1Lemma1 : (x y : ℕ)  -> compareℕ x y ≡ compare2 x y
-putTest1Lemma1 zero    zero    = refl
-putTest1Lemma1 (suc m) zero    = refl
-putTest1Lemma1 zero    (suc n) = refl
-putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
-putTest1Lemma1 (suc .m)           (suc .(Data.Nat.suc m + k)) | less    m k = lemma1  m
- where
-    lemma1 : (m :  ℕ) -> LT  ≡ compare2 m (ℕ.suc (m + k))
-    lemma1  zero = refl
-    lemma1  (suc y) = lemma1 y
-putTest1Lemma1 (suc .m)           (suc .m)           | equal   m   = lemma1 m
- where
-    lemma1 : (m :  ℕ) -> EQ  ≡ compare2 m m
-    lemma1  zero = refl
-    lemma1  (suc y) = lemma1 y
-putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m)           | greater m k = lemma1 m
- where
-    lemma1 : (m :  ℕ) -> GT  ≡ compare2  (ℕ.suc (m + k))  m
-    lemma1  zero = refl
-    lemma1  (suc y) = lemma1 y
-
-putTest1Lemma3 : (k : ℕ)  -> compareℕ k k ≡ EQ
-putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  )
-
-compareLemma1 : {x  y : ℕ}  -> compare2 x y ≡ EQ -> x  ≡ y
-compareLemma1 {zero} {zero} refl = refl
-compareLemma1 {zero} {suc _} ()
-compareLemma1 {suc _} {zero} ()
-compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
-   where
-     lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
-      lemma2 = refl
-
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
          -> (k : ℕ) (x : ℕ)
          -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
diff -r eafc166804f3 -r d927f6b3d2b3 final_main/src/AgdaTreeProof.agda.replaced
--- a/final_main/src/AgdaTreeProof.agda.replaced	Mon Feb 19 18:44:59 2018 +0900
+++ b/final_main/src/AgdaTreeProof.agda.replaced	Mon Feb 19 19:11:13 2018 +0900
@@ -1,45 +1,6 @@
-open @$\equiv$@-Reasoning
-
 redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a @$\mathbb{N}$@)) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@
 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
 
-putTest1Lemma2 : (k : @$\mathbb{N}$@)  @$\rightarrow$@ compare2 k k @$\equiv$@ EQ
-putTest1Lemma2 zero = refl
-putTest1Lemma2 (suc k) = putTest1Lemma2 k
-
-putTest1Lemma1 : (x y : @$\mathbb{N}$@)  @$\rightarrow$@ compare@$\mathbb{N}$@ x y @$\equiv$@ compare2 x y
-putTest1Lemma1 zero    zero    = refl
-putTest1Lemma1 (suc m) zero    = refl
-putTest1Lemma1 zero    (suc n) = refl
-putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
-putTest1Lemma1 (suc .m)           (suc .(Data.Nat.suc m + k)) | less    m k = lemma1  m
- where
-    lemma1 : (m :  @$\mathbb{N}$@) @$\rightarrow$@ LT  @$\equiv$@ compare2 m (@$\mathbb{N}$@.suc (m + k))
-    lemma1  zero = refl
-    lemma1  (suc y) = lemma1 y
-putTest1Lemma1 (suc .m)           (suc .m)           | equal   m   = lemma1 m
- where
-    lemma1 : (m :  @$\mathbb{N}$@) @$\rightarrow$@ EQ  @$\equiv$@ compare2 m m
-    lemma1  zero = refl
-    lemma1  (suc y) = lemma1 y
-putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m)           | greater m k = lemma1 m
- where
-    lemma1 : (m :  @$\mathbb{N}$@) @$\rightarrow$@ GT  @$\equiv$@ compare2  (@$\mathbb{N}$@.suc (m + k))  m
-    lemma1  zero = refl
-    lemma1  (suc y) = lemma1 y
-
-putTest1Lemma3 : (k : @$\mathbb{N}$@)  @$\rightarrow$@ compare@$\mathbb{N}$@ k k @$\equiv$@ EQ
-putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  )
-
-compareLemma1 : {x  y : @$\mathbb{N}$@}  @$\rightarrow$@ compare2 x y @$\equiv$@ EQ @$\rightarrow$@ x  @$\equiv$@ y
-compareLemma1 {zero} {zero} refl = refl
-compareLemma1 {zero} {suc _} ()
-compareLemma1 {suc _} {zero} ()
-compareLemma1 {suc x} {suc y} eq = cong ( \z @$\rightarrow$@ @$\mathbb{N}$@.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
-   where
-     lemma2 : compare2 (@$\mathbb{N}$@.suc x) (@$\mathbb{N}$@.suc y) @$\equiv$@ compare2 x y
-      lemma2 = refl
-
 putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@))
          @$\rightarrow$@ (k : @$\mathbb{N}$@) (x : @$\mathbb{N}$@)
          @$\rightarrow$@ putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (redBlackInSomeState {_} @$\mathbb{N}$@ n {Set Level.zero}) k x