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

想定以上に寝かせることになってしまいましたがアドバイスいただきましたので考えてみます
寝かせたわりには特にアイデアは思いついていません

reverse2/reverse2 の証明は、私も考えてみましたが、累積変数を使った定義と逆consを使った定義とが同じである、ということを証明してしまうのが一番易しいようです。でも、末尾再帰になっている関数を証明する技法を考えてみるのも面白そうですね。

— SUHARA Hiromichi (@suharahiromichi) 2018年4月28日

reverse2/reverse2　を直接証明しようとすると、おそらく、
(rcons (rev2 x nil) a) = (rev2 x '(a)) と (cons a (rev2 x nil)) = (rev2 (rcons x a) nil) のふたつの補題を証明する必要があり、どちらも帰納法が必要で、ちょっと大変な気がします。rcons はリストの後ろにconsする関数です。

— SUHARA Hiromichi (@suharahiromichi) 2018年4月29日

さてアドバイスが雰囲気でしかわかってないので最初から考えていきます

まず逆consとはなにか
rconsと逆consは同じものでしょうからrconsと書くことにすると
(rcons '(a b) 'c)が'(a b c)になるようなものでしょう
特殊ケースとして(rcons '() 'a)は'(a)になる、というのはいいとして
(rcons 'a 'b)はどうなるべきでしょうか
(a . b)かな？

じゃあそれはそういうものとして
rconsというものがある、という前提に立って公理を作るのかな？
rcarとかrcdrも考えるのかな？
それともconsを使ってrconsを定義するんでしょうか

rcons、rcar、rcdrまで全部作ってしまうとそれだけで完結してしまって
cons、car、cdrの世界とのつながりがなくなってしまいそうです
それも公理でつなげてもできそうではありますが

まずはconsを使って書く方式で考えてみようと思います
まず考えたのはこれ

(defun rcons (x y)
  (if (atom x)
      (cons y x)
      (cons (car x) (rcons (cdr x) y))))

ただしこれだと(rcons 'a 'b)が'(b . a)になってしまいます
'(a . b)にしようとすると場合分けになる？

(defun rcons (x y)
  (if (atom x)
      (if (equal x '())
          (cons y '())
          (cons x y))
      (cons (car x) (rcons (cdr x) y))))

yが第1引数になったり第2引数になったりするのがどうも気分がよくありません
複雑だと証明が面倒になるし最初の定義で進めてみようかな
全域にしたいから(rcons 'a 'b)にも値を持たせるけど、何を返すかは気にするな、という考え方で

rconsがあればreverseはすぐ書ける

(defun reverse (x)
  (if (atom x)
      x
      (rcons (reverse (cdr x)) (car x))))

動かす

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

よさそう
イレギュラーなケースはどうなるかな

> (reverse 'a)
a
> (reverse '(a . b))
(a . b)
> (reverse '(a b . c))
(b a . c)

reverseしてるとは言えませんがここは何か値が帰ればいいことにしておいて進みます

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

成り立つか

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

よさげ