定理証明手習い (92) おさらい(2)
5 何回も何回も何回も考えよう
定理の証明
- 洞察：内側から外側へと書き換えるべし
- Ifの持ち上げ
- 洞察：Ifを外側へ
- 洞察：いつも心に定理を
6 最後まで考え抜くのです
再帰的な関数を含む定理の証明
- 証明における再帰のことを、帰納法と呼ぶ
- 再帰における「自然な再帰」は、帰納法における「帰納法の前提」に相当する
- 洞察：帰納法のための前提には手をつけるな
- 洞察：一歩ずつ考えていって帰納法にたどり着こう
- リスト型帰納法による証明
7 びっくりスター！
スター型関数を含む定理の証明
8 これがルールです
全域性の主張の構成
- 連言
(if <式1> <式2> 'nil)
- 全域性についての主張の作り方
- 尺度が減っていくという主張を作る
- 尺度に出てくる仮引数を、再帰的な関数適用の実引数で置き換える
- ifのQ部は残す
9 ルールを変えるには
帰納法の構成
- どんな全域的な再帰関数についても、その関数に含まれる再帰を元にして帰納的な主張を書き下すことができる
- 帰納法の前提としてうまくつかえるようにするには、関数の引数が変数になっている必要がある
- 主張が成立するように条件を付け加える
- 帰納法のための前提
- 主張に出てくる仮引数を、関数適用の実引数で置き換える
- 含意
(if <前提> <帰結> 't)
- Defun式帰納法
- どんな関数についても全域性の主張や帰納法を構成することができるわけではない
- 関数適用の内側にifがあったらifの持ち上げを使う
- 証明できない主張が構成される場合もある
- if-trueの公理を使って前提を導入する
10 いつかはスターで一直線
尺度の構成
- 洞察：繰り返しを避けるために補助定理を用意しよう
- identity-+の公理
- commute-+の公理
- associate-+の公理
- positives-+の公理
- natp/+の公理
- common-addends-<の公理
尺度の構成は職人技、ってことかな
