定理証明手習い(94) しゅくだい(2)
行き詰まり気味なのでまず確実に進捗できそうなところを済ませます
(defun defun.reverse2 ()
(J-Bob/define (prelude)
'(((defun reverse2 (x res)
(if (atom x)
res
(reverse2 (cdr x) (cons (car x) res))))
(size x)
((Q) (natp/size x))
(() (if-true (if (atom x) 't (< (size (cdr x)) (size x))) 'nil))
((E) (size/cdr x))
(() (if-same (atom x) 't))))))
(defun defun.reverse ()
(J-Bob/define (defun.reverse2)
'(((defun reverse (x)
(if (atom x)
x
(reverse2 x '())))
nil))))
さて
作戦を考える必要がありそうです
reverse
はごくふつうにlist-induction
でいけると思ったんですが
というよりもあんまり考えずにlist-induction
でやっちゃったんですが
自然な再帰では、どの引数も、同じままか、与えられた引数の構造の一部分に置き換えられます。
にひっかかってる感じです
reverse2 (x res)
のres
は一部分になってないもんなあ むしろ増えてる
ということでまず
その新しい種類の帰納法を使えるように関数
add-atoms
に関する主張を
書き下す必要があります。
して
帰納法のための前提としてうまく使えるようにするには、関数
add-atoms
の
引数が変数になっている必要があります。
をやってみるのかな
次に証明したいのが(equal (reverse (reverse x)) x)
なんですけれども
ここにはres
が出てきませんのでreverse2
に開いておかないと変数も何もありません
そのあたりから手を付けてみます
(J-Bob/prove (defun.reverse)
'(((dethm reverse/reverse (x)
(equal (reverse (reverse x)) x))
nil
((1 1) (reverse x))
((1) (reverse (if (atom x) x (reverse2 x '()))))
こうなります
(equal
(if (atom (if (atom x) x (reverse2 x '())))
(if (atom x) x (reverse2 x '()))
(reverse2 (if (atom x) x (reverse2 x '())) '()))
x)
(if (atom x)
を外に出して・・・
(() (if-same
(atom x)
(equal
(if (atom (if (atom x) x (reverse2 x '())))
(if (atom x) x (reverse2 x '()))
(reverse2 (if (atom x) x (reverse2 x '())) '()))
x)))
A部を整理
((A 1 Q 1) (if-nest-A (atom x) x (reverse2 x '())))
((A 1) (if-nest-A
(atom x)
(if (atom x) x (reverse2 x '()))
(reverse2 (if (atom x) x (reverse2 x '())) '())))
((A 1) (if-nest-A (atom x) x (reverse2 x '())))
((A) (equal-same x))
めでたく't
になりました
(if (atom x)
't
(equal
(if (atom (if (atom x) x (reverse2 x '())))
(if (atom x) x (reverse2 x '()))
(reverse2 (if (atom x) x (reverse2 x '())) '()))
x))
次はE部
((E 1 Q 1) (if-nest-E (atom x) x (reverse2 x '())))
((E 1 A) (if-nest-E (atom x) x (reverse2 x '())))
((E 1 E 1) (if-nest-E (atom x) x (reverse2 x '())))
ここまで来ました
(if (atom x)
't
(equal
(if (atom (reverse2 x '()))
(reverse2 x '())
(reverse2 (reverse2 x '()) '()))
x))
(atom x)
でなければ(if (atom (reverse2 x '()))
が成り立つことはないので
内側のifは(reverse2 (reverse2 x '()) '())
にできそうです
これがほしかった式
(atom x)
でなければ(if (atom (reverse2 x '()))
が成り立つことはない、の
証明は分けてやりましょうか