\chapter{Left Learning Red Black Tree の検証}
本章では、Left Learning Red Black Tree の
検証方法について述べる

\section{Meta Data Gearの記述}
検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と
比較することで Hoare Triple に当てはめることは第5章で前述した。
\subsection{大小関係を検証する Meta Data Gear}
Red Black Tree は Binary Search Tree の 定義を持っているので、
parent から見て left node には parent の値より小さい値が、
right node には大きい値が入る。これを検証する必要がある。

大小関係を検証するにあたり、Fresh List を用いた検証手法が考えられた。
Fresh Listの記述を\coderef{fresh}に示す。
% ソースコードを載せる。
\lstinputlisting[label=fresh, caption=Fresh List の定義, firstline=47,lastline=49] {src/agda/_fresh.agda}

これを用いて Frash List への定数の insert を\coderef{fresh-test}に示す。
\lstinputlisting[label=fresh-test, caption=Fresh List への定数のinsert, firstline=10,lastline=15] {src/agda/fresh_test.agda}

Fresh Listは一つの値に対して、それより後の値との大小関係の証明が入っている。
そのため、正確性が増すが、関数内でFresh List への insert は困難であったため、
証明付き Data 構造を持った List を \coderef{list_v}
のように定義した。

\lstinputlisting[label=list_v, caption=証明付き Data 構造を持った List,firstline=12,lastline=30] {src/agda/rbt_varif.agda}
証明付き Data 構造を持った List の定義は right-List で行っている。
List の Top と比較した際に、
Topの値より大きい値でなければ insert できない。
加えて insert できた値が Top より大きい事を示す証明も持つ事ができる。

mutual は 以下の記述全てに対して掛かっている。
これは right-List の定義の中で、top-r　を呼び出しており、
top-r は定義の部分で right-List を使用している。
したがって相互呼び出しとなっている。
Agdaは 逐次処理であるため、プログラムの上に宣言してある関数や型しか使用できない。
mutual を掛けることで、プログラムの下で宣言している関数や型を使用する事ができる。

right-List の定義は、何も入っていない場合は right-List で停止するようにしている。
List に一つしか値が入っていない場合は、証明付き Data 構造を持つ必要がない。
そのため特記して記述している。
List に他の値が入っている場合は、top とその次の値との比較を証明を持っている。

top-r は Listに入っている Top の値を持ってくる関数を記述している。
insert-r は right-List に 値を insert するための関数で、
right-List の top と入れる引数を比較し、
inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を
持った List となっている。

これを Left Learning Red Black Tree の 仕様を満たすように、
全てに対して行う。
その後、条件が接続されているのかを検証したのち、健全性について示す事で
Hoare Logic による検証ができる。




%\subsection{Black node の数え上げ}
%他にも、Left Learning Red Brack Tree の black node の数え上げを記述した。

%\subsection{Meta Data Gear の作成}