定理証明手習い (27) 証明スタート
こんな定理を証明します
(dethm ctx?/sub (x y)
(if (ctx? x)
(if (ctx? y)
(equal (ctx? (sub x y)) 't)
't)
't))
そういえばこの間
定理証明手習い (9) 「2 もう少し、いつものゲームを」 - kb84tkhrのブログ
't
ってなんだよ't
って、と思いましたがこれはたぶん定理は常に't
でないと
いけないので入れてあるってことでしょう
なんて書きましたがこれ見てるときに思い出しました
自分でこんなこと書いてたのを
「AならばB」っていうのは「もしAが真ならばB」ってことだよね
Aが偽のときについては何も言ってないね
何も言ってないけど実はこういうことなんだよもしAが真ならばB
(妄想)「ならば」の教え方 - kb84tkhrのブログ
そうでなければ (Bが何だろうと気にしないで)真
そうか「ならば」を素直に書いてただけだったか
定理を真にしないと、っていうのはちょっと見当外れだったぽいです
さて
種としてはリストの帰納法でlist-induction
を使ったように、
スター型の機能法ではstar-induction
を使います
(defun star-induction (x)
(if (atom x)
x
(cons (star-induction (car x))
(star-induction (cdr x)))))
やっぱり木を木のまま返すだけの関数
これが種になっているわけですがここからどうやって証明すべき式が出てくるのか
ちょっと見えてきません
とにかく種を与えてみます
(J-Bob/prove (defun.ctx?)
'(((dethm ctx?/sub (x y)
(if (ctx? x)
(if (ctx? y)
(equal (ctx? (sub x y)) 't)
't)
't))
(star-induction y))))
どれどれ
(if (atom y)
(if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't)
(if (if (ctx? x) (if (ctx? (car y)) (equal (ctx? (sub x (car y))) 't) 't) 't)
(if (if (ctx? x) (if (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't) 't)
(if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't)
't)
't))
見るからにきっつい感じです
最初はifの持ち上げから
(if (ctx? x) ...)
という形が何度も出てきているので、
ifの持ち上げを使ってやるとひとつにまとめることができます
分配法則を使ってるようなイメージ
ifの持ち上げ+アルファでこれくらいに
(if (ctx? x)
(if (atom y)
(if (ctx? y) (equal (ctx? (sub x y)) 't) 't)
(if (if (ctx? (car y))
(equal (ctx? (sub x (car y))) 't)
't)
(if (if (ctx? (cdr y))
(equal (ctx? (sub x (cdr y))) 't)
't)
(if (ctx? y) (equal (ctx? (sub x y)) 't) 't)
't)
't))
't)
終わるんでしょうか