\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 の作成}