定理証明手習い(本)
https://cdn.shopify.com/s/files/1/1634/7169/products/tlp-paper-only_530x.png?v=1530866757
本書で使うlispのルールは以下
変数がある，変数名には()'は使えない
x,+,val-1などが変数名に当たる
クオート'されたリテラル
'banana，シンボル
'12，自然数
'(a glass of orange juice)，リスト
(if sleepy 'coffee '(orange juice))
このとき，sleepyが'tなら'coffeeを，'nilなら'(orange juice)
関数適用
(cons x '(with has browns))
(f x (g y z))
組み込み関数
cons e l: リストlの先頭に要素eを追加
car l: 空でないリストl先頭取得
cdr l: 空でないリストl末尾取得
atom l: 空でないリストなら't / if not 'nil
equal a1 a2: 2引数が同じなら't / if not 'nil
natp a: 引数が自然数なら't / if not 'nil
size a: 値を組み立てるために必要なconsの数
+: 引数1と引数2(自然数)を足す
<: 引数1が引数2より小さいなら't / if not 'nil
関数定義defun，関数名，引数リスト，本体
(defun list-length (xs) if (atom xs) '0 (+ '1 (list-length (cdr xs))))
定理定義dethm，定理名，引数リスト，本体
(dethm natp/list-length (xs) (natp (list-length xs)))
メモ
(atom (cons x y))の値は'nil
(cons x y)はyの値がどうなっているのかに関わらず(y)というリストが出来る
(x)は空ではない
よって(atom (cons x y))の値は'nil
(cdr (cons p '()))の値は常に'()
(cons p '())は(p '())と評価されることに注意
より言えば(cdr (cons x y))の値が常にy
公理をまとめる
(dethm atom/cons (x y) (equal (atom (cons x y)) 'nil))
(dethm car/cons (x y) (equal (car (cons x y)) x))
(dethm cdr/cons (x y) (equal (cdr (cons x y)) y))
(dethm cons/car+cdr (x) (if (atom x) 't (equal (cons (car x) (cdr x)) x )))
本文中での公理と定理
公理: 真であると想定した基本的な仮定
定理: 常に真である式 / トートロジー
証明されなければならない！
またまた公理
(dethm equal-same (x) (equal (equal x x) 't))
(dethm equal-swap (x y) (equal (equal x y) (equal y x)))
(dethm equal-if (x y) (if (equal x y) (equal x y) 't))
if公理
(dethm if-true (x y) (equal if 't x y) x)
(dethm if-false (x y) (equal if 'nil x y) y)
(dethm if-same (x y) (equal (if x y y) y))
Dethmの法則
(dethm name (x_1 ... x_n) body_x)について，
body_x中に出て来くるx_1 ... x_nは対応する式e_1 ... e_nで置換できる
次の場合，置換結果のbody_eでフォーカスの置き換えが出来る
body_eが(equal p q)か(equal q p)という帰結がある
帰結が，ifのQuestion部や関数適用の引数ではない
帰結が，ifのAnswer/Else部に含まれているなら，置換対象のフォーカスも同じQuestion部のifのAnswer/Else部に含まれていないければならない
前提: Answer部かElse部にフォーカスがあるとき，そのif式のQuestion部