定理証明手習い (89) J-Bob/prove
(rewrite/prove defs def seed steps)
関数定義なら全域性の主張、
定理なら帰納法の主張を証明します
違うのは種から主張をつくるところだけかな
rewrite/prove+1 (defs pf e)
そこまでの証明が終わっていれば次の証明を行う
rewrite/prove+ (defs pfs)
複数の証明を行う
(list-extend defs (elem1 (car pfs)))というところで
証明済みのものは順次使えるようにしていく
証明は末尾のものから行っていく、というのがここですね
(J-Bob/prove defs pfs) pfsを証明する
引数チェックをしてrewrite/prove+を呼び出すだけ
J-Bob/proveでテストしてたところはあんまりないんですが、
動きそうなとこだけもってきたところうまく動いてるようです
定理証明手習い (88) J-Bob/step
(rewrite/step defs claim step) claimをstepで書き換える
equality/defで組み込み関数を置き換えるとき、defには組み込み関数の
「定義」では（当然ながら）なく、関数名が単に入っていました
どっかでわざわざ組み込み関数かどうかを判断して渡してるのかな、と思ってましたが
lookupで名前を探して見つからなかったときは名前を返すという、
以前ちょっと不思議に感じていた仕様はこのためだったんですね
ちょっとわかりづらいぞ
美容師さんについて徒然
先日、1000円のカット屋に言ってきました
もうずいぶん昔から1000円とか1500円のとこしかいってません
そんなにこだわりはないので
ただ、1000円クラスになるとちょっと、ただのオッサンオバサンにしか
見えないような美容師さんの割合が増える気がします
腕前と身なりが比例するとは限りませんが
ていうか腕前にもそんなこだわりはないと言ったばかりですが
髪型なんて気にしねえぜ、みたいな人にカットされるのもなんか嬉しい気はしません
定理証明手習い (87) equality/def
パターンに分けてequality/pathを呼びます
(defun equality/def (claim path app def)claim 主張
path フォーカスへのパス
app 関数適用
def 定義
定理証明手習い (86) follow-premsの復習とequality/path
(app-of-equal e) equalの適用か
(equality focus a b) focusを書き換えられる式
(equality/equation focus concl-inst) 帰結でフォーカスを書き換える
conclはきっとconclusionでDethmの法則でいうところの帰結のこと
次の場合、置き換えた結果であるbody(e)を使ってフォーカスの書き換えができる。
- body(e)は、(equal p q)または(equal q p)という 帰結 を含む。
instはなんだろう？instance？
はずれではない気もするけどぴったりかというと・・・
