定理証明手習い (25) 6 最後まで考え抜くのです

本書の目標は、帰納法を使うことで再帰的な関数についての事実を明らかにする方法を読者に知ってもらうことです。

って話でしたがやっと帰納法です

証明にも再帰を使えるんですか？
はい、使えます。
証明における再帰のことを、帰納法と呼びます。

ここでは「種」にlist-inductionという関数を使います
これはなんでしょうか
関数名は「リスト帰納法」ですね

実体はpreludeに入っていました
こういう関数です

(defun list-induction (x)
  (if (atom x)
      '()
      (cons (car x)
            (list-induction (cdr x)))))

・・・なんこれ？
リストをそのまま返すだけの関数にしか見えませんが
リストじゃなければ'()を返しますがそこは大事じゃなさそうな気が

ここはこういうものとして、my/preludeで定義してやってから・・・

> (J-Bob/prove (dethm.memb?/remb2)
    '(((dethm memb?/remb (xs)
         (equal (memb? (remb xs)) 'nil))
       (list-induction xs))))
(if (atom xs)
    (equal (memb? (remb xs)) 'nil)
    (if (equal (memb? (remb (cdr xs))) 'nil) 
        (equal (memb? (remb xs)) 'nil)
        't))

うんできました

数学的帰納法と言えばこんな感じのやつですが

• A(1)が成り立つ
• A(k)が成り立つと仮定するとA(k+1)も成り立つ
• ゆえに、任意の自然数nに対してA(n)が成り立つ

これに合わせて上の結果を読んでやると

• (equal (memb? (remb '())) 'nil)が成り立つ
• (equal (memb? (remb (cdr xs))) 'nil)が成り立つと仮定すると
  (equal (memb? (remb xs)) 'nil)が成り立つ
• ゆえに、任意のリストxsについて(equal (memb? (remb xs)) 'nil)が成り立つ

てとこですかね
ぴったり

memb?/rembの定理でxsになっている箇所が、この式では(cdr xs)になっています。ここが、今証明しようとしている主張における、自然な再帰ということなんでしょうね。
主張について言うときは、（自然な）再帰ではなく、**帰納法のための前提**と呼びます。

ここテストに出るよ
しらんけど

list-inductionと、上のJ-Bob/proveの結果を見比べると
種に書いた関数は、それを呼んでどうこうするというより
証明の最初のステップのテンプレートみたいにして使われるっぽいようにも見えます
ただ、list-inductionのE部からそのままJ-Bob/proveの結果のE部が
出てくるってわけでもないし
ここにもうひとカラクリあるのか、それともテンプレートっていう予想が見当違いなのか

関数の全域の証明では(size xs)を種にしましたが
これもテンプレートっぽくはない
定理と関数で違う動きなんでしょうか

種を入れて証明すべき式が出てきたらあとはそれを'tにしてやるだけです
長いけど特別なことをするわけではありません