定理証明手習い (65) J-Bob/リスト操作

筆者らのJ-Bob実装で最初に定義しているのはリスト操作です。

list0 要素が0個のリストを作る
list0? 要素が0個のリストかどうか

list1 要素が1個のリストを作る
list1? 要素が1個のリストかどうか
elem1 リストの1個目の要素

list2 要素が2個のリストを作る
list2? 要素が2個のリストかどうか
elem2 リストの2個目の要素

list3 要素が3個のリストを作る
list3? 要素が3個のリストかどうか
elem3 リストの3個目の要素

3個で終わり
3個までしか登場しないということだろうな

リストのn個目の要素を取る関数は要素がn個より少ないときは'()を返します
全域性のためかな
例外処理のために使われることもあるんだろうか

リストの要素は何でも受け付けるので要素がリストでもいいし'()でもいいので
'()が返ってきたときは曖昧さが発生しそう
まず要素の数を確認してから、ってやるのかな

(tag sym x) xにsymというタグを付ける
(tag? sym x) xにsymというタグがついているかどうか
(untag x) xからタグを取って値を取り出す
(member x ys) xがysの要素かどうか

ところでテスト項目

(my/test "tag?/yes" (tag? 'a (tag 'a 1)) 't)
(my/test "tag?/no" (tag? 'b (tag 'a 1)) 'nil)
(my/test "untag" (untag (tag 'a 1)) '1)

こういうテストと

(my/test "tag" (tag 'a 1) '(a . 1))

こういうテスト

上のテストは外部仕様的なところ
証明を書くとしたらこういう感じの定理を証明するんだろうな

下のテストは内部の実装が見えてる形
本来は不要なはずだけど、コード見ながらだとこういうテストも書きたくなるな
上のテストだけで十分、って言える？