定理証明手習い(94) しゅくだい(3)

(atom x)でなければ(if (atom (reverse2 x '()))が成り立つことはない、を証明します

(J-Bob/prove (defun.reverse)
  '(((dethm atom/reverse2 (x res)
       (if (atom x)
           't
           (equal (atom (reverse2 x res)) 'nil)))
     (reverse2 x res) ; ←

ここ！これ！きっと！
本番はreverse2/reverse2的なものの証明だけど予行演習的に

こうなります

(if (atom x)
    (if (atom x) 't (equal (atom (reverse2 x res)) 'nil))
    (if (if (atom (cdr x)) 
            't
            (equal (atom (reverse2 (cdr x) (cons (car x) res))) 'nil))
        (if (atom x) 
            't 
            (equal (atom (reverse2 x res)) 'nil))
        't))

A部は'tですね

     ((A) (if-nest-A (atom x) 't (equal (atom (reverse2 x res)) 'nil)))

E部もちょっと整理してreverse2のところを開いてやります

     ((E A) (if-nest-E (atom x) 't (equal (atom (reverse2 x res)) 'nil)))
     ((E A 1 1) (reverse2 x res))

こうなります

(if (atom x)
    't
    (if (if (atom (cdr x))
            't
            (equal (atom (reverse2 (cdr x) (cons (car x) res)))
                   'nil))
        (equal (atom (if (atom x) 
                         res
                         (reverse2 (cdr x) (cons (car x) res))))
               'nil)
        't))

お
いい感じ

equal-ifを使うためにE Qの((if (atom (cdr x)) ...)をなんとかしてやらないといけません
ifの持ち上げを使って外に出します

ちょっとひとつ整理してから

     ((E A 1 1) (if-nest-E (atom x)
                           res
                           (reverse2 (cdr x) (cons (car x) res))))

if-sameして

     ((E A Q) (if-nest-A
               (atom (cdr x))
               't
               (equal (atom (reverse2 (cdr x) (cons (car x) res))) 'nil)))

A部を整理

     ((E A) (if-true
             (equal (atom (reverse2 (cdr x) (cons (car x) res))) 'nil)
             't))
     ((E A 1 1) (reverse2 (cdr x) (cons (car x) res)))
     ((E A 1 1) (if-nest-A
                 (atom (cdr x))
                 (cons (car x) res)
                 (reverse2 (cdr (cdr x)) (cons (car (cdr x)) (cons (car x) res)))))
     ((E A 1) (atom/cons (car x) res))
     ((E A) (equal 'nil 'nil))

A部は'tになりました

(if (atom x)
    't
    (if (atom (cdr x))
        't
        (if (if (atom (cdr x)) 't (equal (atom (reverse2 (cdr x) (cons (car x) res))) 'nil))
            (equal (atom (reverse2 (cdr x) (cons (car x) res))) 'nil)
            't)))

Q部

     ((E E Q) (if-nest-E
               (atom (cdr x))
               't
               (equal (atom (reverse2 (cdr x) (cons (car x) res))) 'nil)))

で

(if (atom x)
  't
  (if (atom (cdr x))
    't
    (if (equal (atom (reverse2 (cdr x) (cons (car x) res))) 'nil) ; ←
      (equal (atom (reverse2 (cdr x) (cons (car x) res))) 'nil) ; ←
      't)))

よっしゃきたー

     ((E E A 1) (equal-if (atom (reverse2 (cdr x) (cons (car x) res))) 'nil))
     ((E E A) (equal 'nil 'nil))
     ((E E) (if-same
             (equal (atom (reverse2 (cdr x) (cons (car x) res))) 'nil)
             't))
     ((E) (if-same (atom (cdr x)) 't))
     (() (if-same (atom x) 't)))))

証明完了

帰納法のための前提としてうまく使えるようにするには、関数add-atomsの
引数が変数になっている必要があります。

はこういうことだったのかー
やっとわかった