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

またもアドバイスいただきました

(rev2 (rev2 l nil) nil) = l なら (rev2 (rev2 l (cons a nil)) nil) = (cons a l)
ですね。この証明にも、rev2の引数がrcons（またはappend）である場合の補題が必要になるとおもいます。

— SUHARA Hiromichi (@suharahiromichi) 2018年5月13日

意味はわかるような気がする
J-Bobが出してくれた主張の方も見直してみよう

もとの定義はちょっと複雑だし、どうせそれでも不足なので開き直って定義は単純化します
reverse2/reverse2のresはいつも'()であることは脳内で補完

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

(J-Bob/prove (dethm.atom/reverse2)
  '(((dethm reverse2/reverse2 (x res)
       (equal (reverse2 (reverse2 x res) res) x))
     (reverse2 x res))))

主張はこうなります

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

resが'()で、xがシンボルだったりドット対だったりしないとするとどう読めるか
いただいたツイートに合わせてxを(cons a l)と読み替えると

(reverse2 (reverse2 l (cons a '())) (cons a '()))ならば
(reverse2 (reverse2 (cons a l) '()) '()は(cons a l)に等しい

ちょっと違う

リストlに対する帰納法で、

ここか？
list-inductionにしてみる

(J-Bob/prove (dethm.atom/reverse2)
  '(((dethm reverse2/reverse2 (x res)
       (equal (reverse2 (reverse2 x res) res) x))
     (list-induction x))))
↓
(if (atom x)
  (equal (reverse2 (reverse2 x res) res) x)
  (if (equal (reverse2 (reverse2 (cdr x) res) res)
             (cdr x))
      (equal (reverse2 (reverse2 x res) res) x)
      't))

これだと

(reverse2 (reverse2 l '()) '())がlに等しければ
(reverse2 (reverse2 (cons a l) '()) '())が(cons a l)

これもちょっと違うな
list-inductionの2引数版がいるのかな

もう一度このへんの式がどういう意味なのか考え直さないとだな
それと、何を種に使うか

この証明にも、rev2の引数がrcons（またはappend）である場合の補題が必要になるとおもいます。

lastitemもrconsの変形みたいなものだしなあ

ちょっとゆっくり考えられるときにやりたい感じがしてきた
この週末もう一度考えて、それでもダメだったらいったん終わりにしよう