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

「(reverse (reverse x))がどんなリストについてもxになるか」…（略）…読者への宿題にしておきます。

付録Cやってるあいだに証明も忘れかけてる気がするのでちょうどいいおさらい
最初は、これを証明すればいいかな、と思ったんですけどね

(defun reverse2 (x res)
  (if (atom x)
      res
      (reverse2 (cdr x) (cons (car x) res))))

(defun reverse (x)
  (reverse2 x '()))

(dethm reverse/reverse (x)
  (equal (reverse (reverse x)) x))

証明するとうまく行きません
よく見たらxが'()以外のアトムだとそもそもreverse/reverseが成り立ってません
そんなのは定義域じゃありませんといいたいところですがそうも行かず
ということでバグ発見しました！ブラボー証明（そうか？

ところで、付録Cやってみて気がついたんですが、上のように直接定義してやると
dethmもそのまま評価できるんですね
J-Bob/proveとかJ-Bob/defineの中だけの存在だと思ってました
J-Bob/langの定義中にはdethmはでてこないのになんでマクロが定義されてるんだろう、と思ったら

こんな感じです

> (reverse/reverse '(a b c))
t

で、

> (reverse/reverse 'a)
nil

だめじゃん、と

reverse/reverseの形は変えたくないから、(reverse 'a)が'aになるようにしましょうか
reverseのほうで吸収するのが自然ですかね
こうかな

(defun reverse (x)
  (if (atom x)
      x
      (reverse2 x '())))

どれ

> (reverse/reverse '(a b c))
t
> (reverse/reverse 'a)
t

おｋ

(J-Bob/prove (prelude)
  '(((defun reverse2 (x res)
       (if (atom x)
           res
           (reverse2 (cdr x) (cons (car x) res))))
     (size x))
    ((defun reverse (x)
       (if (atom x)
           x
           (reverse2 x '())))
     nil)

ここまでの全域性の証明は後回しにします
まずは定理の証明から

    ((dethm reverse/reverse (x)
       (equal (reverse (reverse x)) x))
     (list-induction x)

reverseが入れ子になってるけど、reverse2は普通にリストをたどる再帰だから
list-inductionでいいのかなあ
一応そうだと信じでるけどちょっと自信がないところもある

ここでの主張はこう

(if (atom x)
    (equal (reverse (reverse x)) x)
    (if (equal (reverse (reverse (cdr x))) (cdr x))
        (equal (reverse (reverse x)) x)
        't))

A部から

     ((A 1 1) (reverse x))
     ((A 1 1) (if-nest-A (atom x) x (reverse2 x '())))
     ((A 1) (reverse x))     
     ((A 1) (if-nest-A (atom x) x (reverse2 x '())))
     ((A) (equal-same x))

すんなり'tに

(if (atom x)
    't
    (if (equal (reverse (reverse (cdr x))) (cdr x))
        (equal (reverse (reverse x)) x)
        't))

ではE部
E Aの内側のreverseから展開していく感じかな
まずはreverseをreverse2に

     ((E A 1 1) (reverse x))
     ((E A 1 1) (if-nest-E (atom x) x (reverse2 x '())))

↓

(if (atom x)
    't
    (if (equal (reverse (reverse (cdr x))) (cdr x))
        (equal (reverse (reverse2 x '())) x)
        't))

そしてreverse2を展開

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

↓

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

どうもうまく行きそうな気がしませんね
繰り返しタイプの再帰だったりするのがよくないのかなあ？
でもそのために不自然な書き方や非効率な書き方をするのでは本末転倒だしなあ
もうちょっとやってみよう
いじるとしたら前提のほうじゃないか

     ((E Q 1 1) (reverse (cdr x)))

↓

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

どうにかなる気がしませんね
作戦を考える必要がありそうです