定理証明手習い(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 '()))が成り立つことはない、の
証明は分けてやりましょうか