"アルゴリズムは計算可能な証明である。"(Robert Harper)

命題によるプログラミング

読者への注意: この章で紹介するコンセプトは、初めて見た時には抽象的すぎるように感じられるかもしれません。 たくさんの練習問題を用意しておいたので、テキストの詳細を理解する途中であっても大部分は解けるはずです。 できるかぎり多くの問題、特に★の問題には重点的に挑戦するようにしてください。

これまで宣言したり証明した文は等式の形をしたものだけでした。 しかし、数学で用いられる文や証明にはもっと豊かな表現力があります。 この章では Coq で作れる数学的な文（命題; proposition ）の種類と、その証明を「根拠（ evidence ）を与えること」でどのように進めていくか、もう少し詳しく、基本的な部分から見ていきましょう。

命題（ proposition ）は、"2足す2は4と等しい"のような事実に基づく主張を表現するための文です。 Coq において命題は Prop 型の式として書かれます。 これまであまりそれについて明示的に触れてはきませんでしたが、皆さんはすでに多くの例を見てきています。

証明可能な主張も証明不能な主張も、どちらも完全な命題であると言えます。 しかし単に命題であるということと、証明可能であるということは別ものです！

2 + 2 = 4 も 2 + 2 = 5 も Prop の型をもった妥当な式です。

これまで Coq の中で命題を使う方法は1つしか見ていません。 Theorem（あるいは Lemma、Example）の宣言の中でだけです。

しかし命題にはもっといろいろな使い方があります。 例えば、他の種類の式（数字、関数、型、型関数など）と同様に、Definition を使うことで命題に名前を与えることができます。

こうすることで、命題が使える場所ならどこでも、例えば、Theorem 宣言内の主張などとして使うことができます。

ここまでに登場したすべての命題は等式の形をした命題でした。 それ以外にも新しい命題の形を作ることができます。 例えば、命題 P と Q が与えられば、" P ならば Q "という命題を作れます。

また、自由変数nを含む命題 P が与えられれば、∀ n, P という形の命題を作れます。

最後に、パラメータ化された命題（parameterized proposition ）の定義を紹介します。 例えば、"数nが偶数である"という主張はどのようになるでしょうか？ 偶数を判定する関数は書いてあるので、偶数であるという定義は" n が偶数であることと evenb n = true は同値である"が考えられます。

これは even を関数として定義します。 この関数は数 n を適用されると、n が偶数であることを示す命題を返します。

evenの型 nat → Propは3つの意味を持っています。 (1) "evenは数から命題への関数である。" (2) "evenは数nでインデックスされた命題の集りである"。 (3) "evenは数の性質(property)である。"

命題（パラメータ化された命題も含む）はCoqにおける第一級（first-class）市民です。 このため、ほかの定義の中でこれらの命題を使うことができます。

複数の引数を受け取るように定義することや..

...部分適用もできます。

他の関数に、引数として命題（パラーメータ化された命題も含む）を渡すことすらできます。

2つのアンダースコアを続けた x__y という形式の名前は、" x ならば y である"と読みます。

パラメータ化された命題を引数として渡す関数をさらに2つ紹介します。 1つ目の関数は、ある自然数 n' について P が真ならば常に n' の次の数でも P が真であることを述べています。

そして次の関数は、すべての自然数について与えられた命題が真であることを述べています。

これらを一つにまとめることで、自然数に関する帰納法の原理を自分で再宣言できます。 パラメータ化された命題 P が与えられた場合、0 について P が真であり、P n' が真のとき P (S n') が真であるならば、すべての自然数について P は真である。

根拠

Prop型として妥当な式には証明可能な命題と証明不能な命題の両方があることは既にお話ししました。 当然、証明可能なものの方に興味が向かいます。 P が命題であり e が P の証明である場合、すなわち e が「 P が真である」ということの根拠となっている場合、それを" e : P "と書くことができます。 "型を持っている"や"属している"を表わす記法と同じなのは決して偶然ではありません。 型に属する値と命題に"属する"根拠の間には根本的で有益な類似性があるのです。

次の疑問は"証明とはなにか？"です。 すなわち、ある命題が真であるという根拠として使えるものは、どようなものでしょうか？

帰納的に定義された命題

もちろん、その答は命題の形に依存します。 例えば、含意の命題 P→Q に対する根拠と連言の命題 P∧Q に対する根拠は異なります。 この章では以後、たくさんの具体的な例を示します。

まずは、不可分（ atomic ）な命題を考えましょう。 それは私達が使っている論理にあらかじめ組み込まれているものはなく、特定のドメイン（領域）に有用な概念を導入するものです。 例えば、Basic_J.v で day 型を定義したので、saturday と sunday は"良い"日であるといったような、特定の日に対して何らかの概念を考えてみましょう。 良い日に関する定理を宣言し証明したい場合はまず、"良い"とはどういう意味かをCoqに教えなければなりません。 ある日 d が良い（すなわち d が saturday か sunday である）とする根拠として何を使うかを決める必要があります。 このためには次のように宣言します。

Inductive キーワードは、「データ値の集合を定義する場合( Type の世界)」であっても「根拠の集合を定義する場合( Prop の世界)」であってもまったく同じ意味で使われます。 上記の定義の意味はそれぞれ次のようになっています:

• 最初の行は「 good_day は日によってインデックスされた命題であること」を宣言しています。
  
  
• 二行目は gd_sat コンストラクタを宣言しています。このコンストラクタは good_day saturday という主張の根拠として使えます。
  
  
• 三行目は gd_sun コンストラクタを宣言しています。このコンストラクタは good_day sunday という主張の根拠として使えます。

言い換えると、ある日が良いということを"土曜日は良い、日曜日は良い、それだけだ"と言うことで定義しています。 これによって、日曜日が良いということを証明したいときは、good_day の意味を定義したときにそう言っていたかを調べるだけで済みます。

コンストラクタ gd_sun は、日曜日が良いという主張を正当化する"原始的（primitive）な根拠"、つまり公理です。

同様に、月曜日は火曜日の前に来て、火曜日は水曜日の前に来て、...、ということを宣言する公理を、2つの日をパラメータとして取る命題 day_before として定義できます。

帰納的な定義による命題で導入される公理では全称記号を使うこともできます。 例えば、「どの日だって歌いだしたくなるほど素敵な日だ」という事実については、 わざわざ説明する必要もないでしょう

この行は、もし d が日ならば、fdfs_any d は fine_day_for_singing d の根拠として使えるということを宣言してます。 言い換えると、d が fine_day_for_singing であるという根拠を fdfs_any を d に適用することで作ることができます。

要するに、水曜日は「歌いだしたくなるほど素敵な日」だということです。

これも同じように、最初の行は"私は命題 fine_day_for_singing wednesday に対する根拠を示し、その根拠をあとで参照するために fdfs_wed という名前を導入しようと思っている"と解釈できます。 二行目は、Coqにその根拠をどのように組み立てるかを示しています。

証明オブジェクト

同じことができる、もっと原始的な方法もあります。 Definiton の左辺を導入しようとしている名前にし、右辺を根拠の構築方法ではなく、根拠そのものにすればいいのです。

式 fdfs_any wednesday は、パラメータを受け取る公理 fdfs_anyを 特定の引数 wednesday によって具体化したものととらえることができます。 別の見方をすれば、fdfs_any を原始的な"根拠コンストラクタ"として捉えることもできます。この根拠コンストラクタは、特定の日を適用されると、その日が「歌わずにはいられないほどよい日」である根拠を表します。 型 ∀ d:day, fine_day_for_singing d はこの機能を表しています。 これは、前章で登場した多相型 ∀ X, list X において nil コンストラクタが型からその型を持つ空リストを返す関数であったことと同様です。

もうちょっと面白い例を見てみましょう。 "OK"な日とは(1)良い日であるか(2)OKな日の前日であるとしましょう。

最初のコンストラクタは"dがOKな日であることを示す一つ目の方法は、dが良い日であるという根拠を示すことである"と読めます。 二番目のは"d1がOKであることを示す別の方法は、その日が別の日 d2 の前日であり、d2がOKであるという根拠を示すことである"と読めます。

ここで wednesday がOKであることを証明したいとしましょう。 証明するには2つの方法があります 1つめは原始的な方法であり、コンストラクタの適用を何度もネストすることで、 正しい型を持つ式を書き下します。

2つめの方法は、機械に支援してもらう方法です。証明モードに入り、最終的に満たされるまでゴールやサブゴールを通してCoqに案内してもらいます。

しかし、根本的なところでこの2つの証明方法は同じです。 証明スクリプト内のコマンドを実行するときにCoqが実際にやっていることは、目的の型を持つ式を構築することと全く同じです。

この式は一般的に証明オブジェクト（Proof object）と呼ばれます。

証明オジェクトはCoqの根本を支えています。 タクティックによる証明は、自分で証明オブジェクトを書く代わりに、証明オブジェクトを構築する方法をCoqに指示する基本的なプログラムです。 もちろん、この例では証明オブジェクトはタクティックによる証明よりも短くなっています。 しかし、もっと興味深い証明では証明オブジェクトを手で構築することが苦痛に思えるほど大きく複雑になります。 この後の章では、各ステップを書くことなく複雑な証明オブジェクトを構築できる自動化されたタクティックをたくさん紹介します。

カリー・ハワード対応

この

                 命題          ~  集合 / 型
                 証明          ~  元、要素 / データ値

という類似性は、カリー・ハワード対応（もしくはカリー・ハワード同型, Curry-Howard correspondence, Curry-Howard isomorphism）と呼ばれます。 これにより多くのおもしろい性質が導けます。

集合に空集合、単集合、有限集合、無限集合があり、それぞれが0個、1個、多数の元を持っているように、命題も0個、1個、多数、無限の証明を持ちえます。 命題 P の各要素は、それぞれ異なる P の根拠です。 もし要素がないならば、P は証明不能です。 もしたくさんの要素があるならば、P には多数の異なった証明があります。

含意

これまで → 演算子(含意)を小さい命題から大きな命題を作るために使ってきました。 このような命題に対する根拠はどのようになるでしょうか? 次の文を考えてみてください。

これを日本語で書くと、もし3つの日があるとして、d1 が d2 の前日であり、d2 が d3 の前日であり、かつ d3 がOKであるということがわかっているならば、d1 もOKである、という意味になります。

okd_before2 をタクティッックを使って証明するのは簡単なはずです...

練習問題: ★, optional (okd_before2_valid)

☐

ところで、これに対応する証明オブジェクトはどんな感じでしょうか?

答: 含意としての → と、関数の型の → の記法はそっくりです。 これをそのまま解釈すると、∀ d1 d2 d3, ok_day d3 → day_before d2 d1 → day_before d3 d2 → ok_day d1 という型をもった式を見付ける必要があります。 なので探すものは6個の引数(3個の日と、3個の根拠)を受け取り、1個の根拠を返す関数です! それはこんな感じです。

練習問題: ★, optional (okd_before2_valid_defn)

下記の結果としてCoqが出力するものを予測しなさい。

帰納的に定義された型に対する帰納法の原理

Inductive でデータ型を新たに定義するたびに、Coqは帰納法の原理に対応する公理を自動生成します。

型tに対応する帰納法の原理はt_indという名前になります。 ここでは自然数に対するものを示します。

これは先ほど定義した our_nat_induction の性質とまったく同じであることに注意してください。

induction タクティックは、基本的には apply t_ind の単純なラッパーです。 もっとわかりやすくするために、induction タクティックのかわりに apply nat_ind を使っていくつかの証明をしてみる実験をしてみましょう。 例えば、Basics_J の章で見た定理の別の証明を見てみましょう。

この証明は基本的には前述のものと同じですが、細かい点で特筆すべき違いがあります。 1つめは、帰納段階の証明（"S" の場合）において、induction が自動でやってくれること（intros）を手作業で行なう必要があることです。

2つめは、nat_ind を適用する前にコンテキストに n を導入していないことです。 nat_ind の結論は限量子を含む式であり、apply で使うためにはこの結論と限量子を含んだゴールの形とぴったりと一致する必要があります。 induction タクティックはコンテキストにある変数にもゴール内の量子化された変数のどちらにでも使えます。

3つめは、apply タクティックは変数名（この場合はサブゴール内で使われる変数名）を自動で選びますが、induction は（as ... 節によって）使う名前を指定できることです。 実際には、この自動選択にはちょっと不都合な点があります。元の定理の n とは別の変数として n を再利用してしまいます。 これは Case 注釈がただの S だからです。 ほかの証明で使ってきたように省略しない形で書くと、これは n = S n という意味のなさない形になってしまいます。 このようなことがあるため、実際には nat_ind のような帰納法の原理を直接適用するよりも、素直に induction を使ったほうがよいでしょう。 しかし、ちょっとした例外を除けば実際にやりたいのは nat_ind の適用であるということを知っておくことは重要です。

練習問題: ★★ (plus_one_r')

induction タクティックを使わずに、下記の証明を完成させなさい。

☐

ほかの Inductive によって定義されたデータ型に対しても、Coqは似た形の帰納法の原理を生成します。 コンストラクタ c1 ... cn を持った型 t を定義すると、Coqは次の形の定理を生成します。
    t_ind :
       ∀ P : t → Prop,
            ... c1の場合 ... →
            ... c2の場合 ... →
            ... →
            ... cnの場合 ... →
            ∀ n : t, P n

各場合分けの形は、対応するコンストラクタの引数の数によって決まります。 一般的な規則を紹介する前に、もっと例を見てみましょう。 最初は、コンストラクタが引数を取らない場合です。

練習問題: ★ (rgb)

次のデータ型に対してCoqが生成する帰納法の原理を予測しなさい。 紙に答えを書いたのち、Coqの出力と比較しなさい。

☐

別の例を見てみましょう。引数を受け取るコンストラクタがある場合です。

練習問題: ★ (natlist1)

上記の定義をすこし変えたとしましょう。

このとき、帰納法の原理はどのようになるでしょうか？

☐

これらの例より、一般的な規則を導くことができます。

• 型宣言は複数のコンストラクタを持ち、各コンストラクタが帰納法の原理の各節に対応する。
• 各コンストラクタ c は引数 a1..an を取る。
• ai は t（定義しようとしているデータ型）、もしくは別の型 s かのどちらかである。
• 帰納法の原理において各節は以下のことを述べている。
  • "型 a1...an のすべての値 x1...xn について、各 x について P が成り立つならば、c x1 ... xn についても P が成り立つ"

練習問題: ★ (ExSet)

帰納的に定義された集合に対する帰納法の原理が次のようなものだとします。
      ExSet_ind :
         ∀ P : ExSet → Prop,
             (∀ b : bool, P (con1 b)) →
             (∀ (n : nat) (e : ExSet), P e → P (con2 n e)) →
             ∀ e : ExSet, P e

ExSet の帰納的な定義を示しなさい。

☐

多相的なデータ型ではどのようになるでしょうか？

多相的なリストの帰納的定義は natlist によく似ています。
      Inductive list (X:Type) : Type :=
        | nil : list X
        | cons : X → list X → list X.

ここでの主な違いは、定義全体が集合 X によってパラメータ化されていることです。 つまり、それぞれの X ごとに帰納型 list X を定義していることになります。 (定義本体で list が登場するときは、常にパラメータ X に適用されていることに 注意してください。) 帰納法の原理も同様に X によってパラメータ化されます。
     list_ind :
       ∀ (X : Type) (P : list X → Prop),
          P [] →
          (∀ (x : X) (l : list X), P l → P (x :: l)) →
          ∀ l : list X, P l

この表現（と list_ind の全体的な形）に注目してください。帰納法の原理全体が X によってパラメータ化されています。 別の見方をすると、list_ind は多相関数と考えることができます。この関数は、型 X が適用されると、list X に特化した帰納法の原理を返します。

練習問題: ★ (tree)

次のデータ型に対してCoqが生成する帰納法の原理を予測しなさい。 答えが書けたら、それをCoqの出力と比較しなさい。

☐

練習問題: ★ (mytype)

以下の帰納法の原理を生成する帰納的定義を探しなさい。
      mytype_ind :
        ∀ (X : Type) (P : mytype X → Prop),
            (∀ x : X, P (constr1 X x)) →
            (∀ n : nat, P (constr2 X n)) →
            (∀ m : mytype X, P m →
               ∀ n : nat, P (constr3 X m n)) →
            ∀ m : mytype X, P m

☐

練習問題: ★, optional (foo)

以下の帰納法の原理を生成する帰納的定義を探しなさい。
      foo_ind :
        ∀ (X Y : Type) (P : foo X Y → Prop),
             (∀ x : X, P (bar X Y x)) →
             (∀ y : Y, P (baz X Y y)) →
             (∀ f1 : nat → foo X Y,
               (∀ n : nat, P (f1 n)) → P (quux X Y f1)) →
             ∀ f2 : foo X Y, P f2

☐

練習問題: ★, optional (foo')

次のような帰納的定義があるとします。

foo' に対してCoqはどのような帰納法の原理を生成するでしょうか? 空欄を埋め、Coqの結果と比較しなさい
     foo'_ind :
        ∀ (X : Type) (P : foo' X → Prop),
              (∀ (l : list X) (f : foo' X),
                    _______________________ →
                    _______________________ ) →
             ___________________________________________ →
             ∀ f : foo' X, ________________________

☐

帰納法の仮定

この概念において"帰納法の仮定"はどこにあてはまるでしょうか?

数に関する帰納法の原理
       ∀ P : nat → Prop,
            P 0 →
            (∀ n : nat, P n → P (S n)) →
            ∀ n : nat, P n

は、すべての命題 P（より正確には数値 n を引数にとる命題 P ）について成り立つ一般的な文です。 この原理を使うときはいつも、nat→Prop という型を持つ式を P として選びます。

この式に名前を与えることで、証明をもっと明確にできます。 例えば、mult_0_r を"∀ n, n * 0 = 0"と宣言するかわりに、"∀ n, P_m0r n"と宣言します。 なお、ここで P_m0r は次のように定義されています。

あるいは

でも同じ意味です。

これで、証明する際に P_m0r がどこに表われるかが分かりやすくなります。

このように名前をつける手順は通常の証明では不要です。 しかし、1つ2つ試してみると、帰納法の仮定がどのようなものなのかが分かりやすくなります。 ∀ n, P_m0r n を n による帰納法（induction か apply nat_ind を使う）によって証明しようとすると、最初のサブゴールでは P_m0r 0（"P が0に対して成り立つ"）を証明しなければならず、2つめのサブゴールでは ∀ n', P_m0r n' → P_m0r (S n')（"P が n' について成り立つならば、P が S n' についても成り立つ"あるいは" P が S によって保存される"）を証明しなければなりません。 帰納法の仮定は、2つめの推論の基礎になっています -- P が n' について成り立つことを仮定することにより、それによって P が S n' について成り立つことを示すことができます。

偶数について再び

最初の方で命題に関して議論してきた例のいくつかは、偶数の概念に結びついてきます。 これまでは偶数を判定するために evenb n を計算することから始め、真偽値を返していました。 つぎに、n が偶数であることを主張する命題 even n を( evenb を使うことで）作りました。 つまり、"n が偶数である"を" evenb が n を適用されたときに true を返す"と定義していました。

偶数性の概念をそのまま定義する別の方法があります。 evenb 関数（"ある計算が true を返すなら、その数は偶数である"）を使って間接的に定義するのではなく、「偶数とは何を意味するか」を根拠を使って直接定義することができるのです。

この定義は、数 m が偶数であるという根拠を与える方法が2つあることを示しています。 第一に、0 は偶数であり、ev_0 がこれに対する根拠です。 次に、任意の n に対して m = S (S n) とし、n が偶数であるという根拠 e を与えることができるならば、m も偶数であると言え、ev_SS n e がその根拠となります。

練習問題: ★, optional (four_ev)

4が偶数であることをタクティックによる証明と証明オブジェクトによる証明で示しなさい。

☐

練習問題: ★★ (ev_plus4)

n が偶数ならば 4+n も偶数であることをタクティックによる証明と証明オブジェクトによる証明で示しなさい。

☐

練習問題: ★★ (double_even)

次の命題をタクティックによって証明しなさい。

☐

練習問題: ★★★★, optional (double_even_pfobj)

上記のタクティックによる証明でどのような証明オブジェクトが構築されるかを予想しなさい。 (答を確かめる前に、Case を除去しましょう。 これがあると証明オブジェクトが少し見づらくなります。)

☐

根拠に対する帰納法の推論

Coqの設計は非常に直交しているので、素朴な命題を根拠と共に定義するために Inductive キーワードを使った場合、その定義と関連する帰納法の原理が使えるはずです。 実際、関連する帰納法の原理は存在しており、この節ではそれをどう使うかについて見ていきます。 ウォーミングアップとして、単純な destruct が帰納的に定義された根拠に対してどのように働くかを見てみましょう。

偶数であるという根拠を作るだけでなく、偶数であるという根拠に対して推論を行います。 帰納的な宣言によって ev を導入したことにより、「 ev_0 と ev_SS が、偶数であるという根拠を作る唯一の方法である」ということが分かるだけでなく、「この2つのコンストラクタによってのみ偶数であるという根拠が構築される」ということが分かります。

言い換えると、 ev n という根拠 E があった場合、 E は2つの形式のどちらか片方であることが分かります : 「E が ev_0 (かつ n が 0 )である」か、「 E が ev_SS n' E'(かつ n が S (S n')) かつ E' が n' が偶数であるということの根拠である」かのどちらかです。

なので、これまで見てきたように帰納的に定義されたデータに対してだけでなく、帰納的に定義された根拠に対しても、 destruct タクティックを使うことは有用です。

一例として、ev n ならば ev (n-2) を示すために、 n が偶数であるという根拠に対して destruct タクティックを使ってみましょう。

練習問題: ★ (ev_minus2_n)

E の代わりに n に対して destruct するとどうなるでしょうか?

☐

n が偶数であるという根拠に対して induction を実行することもできます。 ev を満たす n に対して、先に定義した evenb 関数が true を返すことを示すために使ってみましょう。

(もちろん、 even n → ev n も成り立つはずです。 どのように証明するかは次の章で説明します。)

練習問題: ★ (ev_even_n)

この証明を E でなく n に対する帰納法として実施できますか?

☐

帰納的に定義された命題に対する帰納法の原理は、帰納的に定義された集合のそれとまったく同じ形をしているわけではありません。 今の段階では、根拠 ev n に対する帰納法は n に対する帰納法に似ているが、 ev n が成立する数についてのみ着目することができると直感的に理解しておいて問題ありません。 ev の帰納法の原理をもっと深く見て行き、実際に何を起こっているかを説明します。

練習問題: ★ (l_fails)

次の証明はうまくいきません。

     Theorem l : ∀ n,
       ev n.
     Proof.
       intros n. induction n.
         Case "O". simpl. apply ev_0.
         Case "S".
           ...

理由を簡潔に説明しない。

☐

練習問題: ★★ (ev_sum)

帰納法が必要な別の練習問題をやってみましょう。

☐

「n+2 が偶数ならば n も偶数である」という偶数に関する根拠を分析したいとします。 この種の場合分けに destruct を使ってみたくなるかもしれません。

しかし、これはうまくいきません。 例えば、最初のサブゴールにおいて、 n が 0 であるという情報が失われてしまいます。 ここで使うべきは、 inversion です。

このような inversion の使い方は最初はちょっと謎めいて思えるかもしれません。 これまでは、 inversion は等号に関する命題に対して使い、コンストラクタから元のデータを取り出すためか、別のコンストラクタを区別するためににしか使っていませんでした。 しかし、ここでは inversion が 帰納的に定義された命題に対する根拠を分析するためにも使えることを紹介しました。

ここで、inversion が一般にはどのように動作するかを説明します。 I が現在のコンテキストにおいて帰納的に宣言された仮定 P を参照しているとします。 ここで、inversion I は、Pのコンストラクタごとにサブゴールを生成します。 各サブゴールにおいて、 コンストラクタが P を証明するのに必要な条件によって I が置き換えられます。 サブゴールのうちいくつかは矛盾が存在するので、 inversion はそれらを除外します。 残っているのは、元のゴールが成り立つことを示すのに必要なサブゴールです。

先ほどの例で、 inversion は ev (S (S n)) の分析に用いられ、 これはコンストラクタ ev_SS を使って構築されていることを判定し、そのコンストラクタの引数を仮定に追加した新しいサブゴールを生成しました。(今回は使いませんでしたが、補助的な等式も生成しています。) このあとの例では、inversion のより一般的な振る舞いについて調べていきましょう。

練習問題: ★ (inversion_practice)

inversion タクティックは、仮定が矛盾していることを示し、ゴールを達成するためにも使えます。

☐

一般に、帰納的な命題には destruct の代わりに inversion を使えます。 このことは一般的に、コンストラクタごとに場合分けができることを示しています。 加えて、いくつかの補助的な等式も得ることができます。 なお、ゴールはその等式によって書き換えられていますが、その他の仮定は書き換えられていません。

練習問題: ★★★ (ev_ev_even)

何に対して帰納法を行えばいいかを探しなさい。(ちょっとトリッキーですが)

☐

練習問題: ★★★, optional (ev_plus_plus)

既存の補題を適用する必要のある練習問題です。 帰納法も場合分けも不要ですが、書き換えのうちいくつかはちょっと大変です。 Basics_J.v の plus_swap' で使った replace タクティックを使うとよいかもしれません。

☐

なぜ命題を帰納的に定義するのか?

ここまで見てきたように "ある数が偶数である" というのは次の2通りの方法で解釈されます。 間接的には「テスト用の evenb 関数」によって、直接的には「偶数であることの根拠の構築方法を帰納的に記述すること」によってです。 これら2つの偶数の定義は、ほぼ同じくらい楽に宣言できますし、同じように動きます。 どちらを選ぶかは基本的に好みの問題です。

しかし、興味深いほかの性質、例えば「テスト用の関数を書くのが難しかったり不可能だったりする」ようなことがあることを考えると、直接的な帰納的な定義のほうが好ましいと言えます。 例えば以下のように定義される MyProp という性質について考えてみましょう。

• 4 は性質 MyProp を満たす
• n が性質 MyProp を満たすならば、 4+n も満たす
• もし2+nが性質 MyProp を満たすならば、 n も満たす
• その他の数は、性質 MyProp を満たさない

これは数の集合の定義としてはなんの問題もありませんが、この定義をそのままCoqのFixPointに変換することはできません。 (それだけでなく他の言語の再帰関数に変換することもできません。) Fixpoint を用いてこの性質をテストするうまい方法を見つけられるかもしれません。(実際のところ、この場合はそれほど難しいことではありません) しかし、一般的にこういうことをしようとすると、かなりあれこれ考える必要があるでしょう。 実際、Coqの Fixpoint は停止する計算しか定義できないので、 定義しようとする性質が計算不能なものだった場合、どれだけがんばっても Fixpoint では定義できません。

一方、性質 MyProp がどのようなものかの根拠を与える帰納的な定義を書くことは、非常に簡単です。

MyProp の非形式的な定義の最初の3つの節は、帰納的な定義の最初の3つの節に反映されています。 4つ目の節は、Inductive キーワードによって強制されます。

これで、偶数のときにやったように、ある数が MyProp を満たすことの根拠を作ることができます。

練習問題: ★★ (MyProp)

MyPropに関する便利な2つの事実があります。 証明はあなたのために残してあります。

☐

これらを使って、 MyProp は全ての奇数について成り立つことと、その逆も成り立つをことを示せます。

この定理の非形式的な証明は次のようになります。

Theorem : 任意の自然数 n において、もし ev n ならば MyProp n が成り立つ。

Proof : n を nat とし、ev n の導出を E とします。 MyProp n の導出を示さなければなりません。 E の帰納法について証明を行うので、以下の2つの場合について考えなければなりません。

• E の最後のステップがev_0だった場合、 n は 0 となる。 その場合、MyProp 0が成り立つをことを示さなければならない; 補題 MyProp_0 よりこれは真である。
  
  
• E の最後のステップが ev_SS だった場合、 n = S (S n') となる n' が存在し、 ev n' の導出が存在する。 MyProp n' が成り立つという帰納法の仮定を用いて、MyProp (S (S n')) を示さなければなりません。 しかし、補題 MyProp_plustwo により、MyProp n' を示せば十分であることがわかり、さらにそれは帰納法の仮定そのものです。

練習問題: ★★★ (ev_MyProp)

☐

練習問題: ★★★, optional (ev_MyProp_informal)

ev_MyProp の 形式的な証明に対応する非形式的な証明を書きなさい。

定理: すべての自然数 n に対して、 MyProp n ならば ev n。

証明: (ここを埋める) ☐

全体像: Coqの2つの空間

これまで Coq の基本的な構造についていくつか触れてきたので、 ここでは一歩引いてそれらがどのように組み合わさっているか少しだけ見てみましょう。

Coq の式は2つの異なる空間のどちらかに属しています。

• Type は計算とデータの空間です。
• Prop は論理的表明と根拠の空間です。

2つの空間には深い類似性がありますが（それぞれについて値、帰納的な定義、限量子などについて言及できます）、 数学的構造の定義や推論において、これらはまったく異なる役割を果たします。

値

どちらのの空間もコンストラクタの無限集合をスタート地点とします。 コンストラクタは内部構造を全く持っておらず、ただのアトミックなシンボルです。 例えば、true, false, O, S, nil, cons, ev_0, ev_SS, ... などです。

最も単純な値は、コンストラクタの適用だけによって構成されます。 例えば:

• true
• O
• S (S (S O))
• ev_0
• ev_SS (S (S O)) ev_0
• ev_SS (S (S (S (S O)))) (ev_SS (S (S O)) ev_0)

そのような式は木として考えることもできます。 葉は0引数のコンストラクタ（引数なしで適用された）であり、内部ノードは1個以上の値に対して適用されたコンストラクタです。 Type 空間において、値はデータとして捉えます。 Prop において、値を根拠として捉えます。 Prop における値は、導出木と呼ばれることもあります。

関数もまた値です。例えば、

• fun x => true
• fun b => negb b
• fun n => S (S (S n))
• fun n => fun (P : ev n) => ev_SS (S (S n)) P

Type 空間の値を返す関数は、計算を表します: 入力値を受け取り、入力から計算した出力値を返します。 Prop の値を返す関数は、全量子化された根拠と呼ばれます。 すなわち、ある命題に対する根拠を作るのに入力も用います。 （作られる命題も入力を使うかもしれません。）

帰納的定義

帰納的（Inductive）な定義をするということは、全ての値の集合の「特定の部分集合に名前を与える」ということです。 例えば、帰納的な型 nat の定義は、要素の全てが自然数を表しているような集合を表します。つまり、 帰納的な定義が「全ての値の集合」から以下のような属性を持つ要素だけを抜き出して部分集合 nat を作っていると考えられます。

• 値 O はこの集合の要素である。
• この集合は、 S の適用に対し閉じている（つまり、値 n がこの集合の要素なら S n もまたこの集合の要素である）。
• これらの条件を満たす最小の集合がこの集合である。（つまり集合 nat の要素だけが上の二つの条件を満たしていて、それ以外のものはこの集合に入っていない）。

帰納的に定義された集合は、それ自身が複合的な値のコンストラクタの引数となることもあります。例えば、以下のようなものです。

• nat
• nil nat
• cons nat O (cons nat (S O) (nil nat))

また、引数や戻り値が集合となっているような関数を書くこともできます。例えば、 list は集合 X を引数にとり、 list X の集合を返す関数です（この集合の要素は、集合 X の要素を持つリストです）。

同様に、帰納的な型 ev の定義は、その数字が偶数であるという根拠となる命題を集めたものの定義です。このことは、全ての n について、この定義が全ての値の集合から以下の条件を満たす値を全て集めて部分集合 ev n を抜き出してくるような定義、ということです。

• 値 ev_0 は集合 ev O の要素である。
• この集合は ev_SS の型が正しい（well-typed な）適用に関して閉じている。
  • - つまり、もし値 e が集合 ev n の要素なら、
  値ev_SS n e は集合 ev (S (S n)) の要素である。;
• これらの条件を満たす最小の集合がこの集合である。 (つまり集合 ev n の要素だけが上の二つの条件を満たしていて、それ以外のものはこの集合に入っていない）。

型とカインド

ざっくり言うと、Coqにおける「型」は、「式の分類に使われる式」です。例えば、 bool, nat, list bool, list nat, nat→nat などは全て「型」です。bool という型は、 true や false を他の値と区別しますし、nat 型は O, S O, S (S O) など、nat→nat 型は fun n => S n のように数を引数にとって数を返す関数値を他の値と区別します。

Type や Prop 、そしてそれらの複合式（ Type → Type など）には、「ひとつ上位の」分類 -- それは, 「型（もしくは命題）の型を表す式」のようなものと考えてもらっていいですが -- が可能です。それを、単なる「型」と混同しないために「カインド」と呼ぶことにします。例えば、nat や nat→nat 、list nat などは全て Type という「カインド」を持ち、 list は Type → Type、 ev は nat → Prop というカインドを持ちます。

命題 vs. ブール値

命題とブール値は、一見とてもよく似ているように見えます。しかしこの二つは根本的に違うものです！

• ブール値は、「計算の世界における値」です。 bool 型の式は全て、（自由変数を持っていない限り）必ず true か false のどちらかに簡約することができます。
  
  
• 命題は「論理の世界にいおける型」です。これらは「証明可能（この型の式を書くことができる）」か、「証明不能（そのような式は存在しない）」かのいずれかです。従って「命題が true である」というような言い方は意味を持ちません。
  
  我々は時折、命題に対してそれが "true" か "false" というようなことを言ってしまいがちですが、厳格に言えばこれは間違っています。命題は「証明可能かそうでないか」のどちらかです。

関数 vs. 限量子

A→B という型も ∀ x:A, B という型も、どちらも型 A から型 B への関数である、という点については同じです。この二つの唯一の違いは、後者の場合戻り値の型 B が引数 x を参照できるということです。たとえば、

• 関数 fun x:nat => x + x は型 nat→nat を持っていますが、このことは任意の数 n を別の数に対応させるもの、ということです。
  
  
• 対して、関数 fun X : Type => nil (list X) は ∀ X : Type, list (list X) という型になります。これは、任意の集合 X を、 X 型のリストのリストに対応させるもの、ということになります。（もちろん、nil は通常 nil X と書く代わりに [] と書くのが普通ですが。）

実際、関数を記述するためのこれら二つの書き方はほぼ同じですが、 Coq では A→B の書き方は、x がB の定義の中に変数として現れない限り、fun x:nat => x + x のただの省略形と考えていいでしょう。例えば、好みならばこれを ∀ x:nat, nat と書いてもいいのです。

関数 vs. 含意

Type にしろ Prop にしろ、我々はその値を別の値に変換する関数を書くことができます。 また、関数はそれ自身が値です。 このことは、我々が、次のようなことが出来ることを意味しています。

• 関数を引数にしたり、関数を戻り値にしたりする高階関数を書くこと。
• 関数をコンストラクタに適用し、関数を保持したさらに複雑な値を作り出すこと。

Prop 型を扱う P→Q という型の関数は、 P の根拠を引数にとり、新たな Q の根拠を結果として生成するものです。このような関数はそれ自身が「P ならば Q である」ということの根拠であると見なせます。そのことから、P が真であるという根拠があるなら、それを関数に適用して Q が真であるという根拠を得ることができます。含意に根拠を与えるということは、根拠の関数を与えるということと同じです。このことが、我々が Coq で関数と論理学の「含意」に同じ表記を与えている理由です。これらは全く同じものなのです。

非形式的な証明

Q: 命題 P の形式的な証明と、同じ命題 P の非形式的な証明の間にはどのような関係があるのでしょうか？

A: 後者は、読む人に「どのように形式的な証明を導くか」を示すようなものとなっているべきです。

Q: どの程度細かく書く必要があるのですか？

A: この問いに唯一と言えるような解答はありません。回答には選択の幅があります。

その範囲の片方の端は、読み手にただ形式的な証明全体を与えればよいという考えです。つまり非形式的な証明は、形式的な証明をただ単に普通の言葉で書き換えただけ 、ということです。この方法は、読み手に形式的な証明を書かせるための能力を与えることはできますが、それについて何かも「教えてくれる」訳ではありません。

これに対しもう一方の端は、「その定理は真で、頑張ればできるはず」ような記述です。この方法も、「教える」ということに関してはあまりいいやり方とはいえません。なぜなら、証明を記述するときはいつも、今証明しようとしているものの奥深くにまで目を向け考えることが必要とされますが、細かく書きすぎると証明を読む側の人の多くは自分自身の力で同じ思考にたどり着くことなく、あきらめて証明の記述に頼ってしまうでしょう。

一番の答えはその中間にあります。全ての要点をかいつまんだ証明というのは、「かつてあなたが証明をしたときに非常に苦労した部分について、読む人が同じ苦労をしなくて済むようになっている」ようなものです。そしてまた、読み手が同じような苦労を何時間もかけてする必要がないよう、証明の中で使える部品などを高度に示唆するものでなければなりません（例えば、仮定 IH が何を言っているかや、帰納的な証明のどの部分に現れるかなど）。しかし、詳細が少なすぎると、証明の主要なアイデアがうまく伝わりません。

もう一つのキーポイント：もし我々が命題 P の形式的な証明と非形式的な証明について話しているならば、命題 P 自体は何も変わりません。このことは、形式的な証明も非形式的な証明も、同じ「世界」について話をしていて、同じルールに基づいていなければならない、と言うことを意味しています。

帰納法による非形式的な証明

ここまで、我々は「帰納法を使った形式的な証明の舞台裏」を覗くことにずいぶん章を割いてきました。そろそろ「帰納法を使った非形式的な証明」に話を向けてみましょう。

現実世界の数学的な事柄をやりとりするた記述された証明を見てみると、極端に風呂敷が広く衒学的なものから、逆に短く簡潔すぎるものまで様々です。理想的なものはその間のとこかにあります。もちろん、じぶんなりのスタイルを見つけるまでは、衒学的なスタイルから始めてみるほうがいいでしょう。また、学習中には、標準的なテンプレートと比較してみることも、学習の一助になるでしょう。 このような考えから、我々は以下の二つのテンプレートを用意しました。一つは「データ」に対して（「型」に潜む帰納的な構造について）帰納法を適用したもの、もう一つは「命題」に対して（命題に潜む機能的な定義について）帰納法を適用したものです。このコースが終わるまでに、あなたが行った帰納的な証明の全てに、どちらかの方法を適用してみましょう。

帰納的に定義された集合についての帰納法

Template:

• 定理: < "For all n:S, P(n),"の形で全量子化された命題。ただし S は帰納的に定義された集合。>
  
  証明: n についての帰納法で証明する。
  
  <集合 S の各コンストラクタ c について...>
  
  
  • n = c a1 ... ak と仮定して、<...もし必要なら S のそれぞれの要素 a についてIHであることをを示す。>ならば <...ここで再び P(c a1 ... ak) を示す> である。
    
    < P(n) を証明してこのケースを終わらせる...>
    
    
  • <他のケースも同様に記述する...> ☐

Example:

• Theorem: 任意の集合 X 、リスト l : list X、 自然数 n について、 もし length l = n が成り立つなら、index (S n) l = None も成り立つ。
  
  Proof: l についての帰納法で証明する。
  
  
  • まず、l = [] と仮定して、任意の n でこれが成り立つことを示す。もし length [] = n ならば index (S n) [] = None 。 これは index の定義から直接導かれる 。
    
    
  • 次に、 x と l' において l = x :: l' と仮定して、任意の n' について length l' = n' ならば index (S n') l' = None である時、任意の n について、 もし length (x::l') = n ならば index (S n) (x::l') = None を示す。
    
    n を length l = n となるような数とすると、
                length l = length (x::l') = S (length l'),
    
    これは以下の十分条件である。
                index (S (length l')) l' = None.
    
    しかしこれは仮定法の仮定から直接導かれる。 l' の length となるような n' を選択すればよい。 ☐

帰納的に定義された命題についての帰納法

帰納的に定義された証明オブジェクトは、しばしば”導出木”と呼ばれるため、この形の証明は「導出による帰納法（ induction on derivations ）」として知られています。

Template :

• Theorem : <"Q → P," という形を持った命題。ただし Q は帰納的に定義された命題（さらに一般的には、"For all x y z, Q x y z → P x y z" という形の命題）>
  
  Proof : Q の導出による帰納法で証明する。 <もしくは、さらに一般化して、" x, y, zを仮定して、Q x y z ならば P x y z を示す。Q x y zの導出による帰納法によって"...>
  
  <各コンストラクタ c による値 Q について...>
  
  
  • Q が c であることを示した最後のルールを仮定して、 <...ここで a の全ての型をコンストラクタの定義にある等式と 共に示し、型 Q を持つ a がIHであることをそれぞれ示す。> ならば <...ここで再び P を示す> である。
    
    <がんばって P を証明し、このケースを閉じる...>
    
    
  • <他のケースも同様に...> ☐

Example

• Theorem : <= という関係は推移的である -- すなわち、任意の 数値 n, m, o について、もし n <= m と m <= o が成り立つ ならば n <= o である。
  
  Proof : m <= o についての帰納法で証明する。
  
  
  • m <= o が le_n であることを示した最後のルールを仮定する。 それにより m = o であることとその結果が直接導かれる。
    
    
  • m <= o が le_S であることを示した最後のルールを仮定する。 それにより m <= o' を満たす o' について o = S o' が成り立つ。 帰納法の仮定法より n <= o' である。
    
    従ってle_S より n <= o である。 ☐

選択課題

この項では、Coq において帰納法がどのように機能しているか、もう少し詳しく示していきたいと思います。 最初にこの項を読むときは、全体を読み流す感じでもかまいません（完全に 読み飛ばすのではなく、概要だけでも眺めてください。ここに書いてあることは、 多くの Coq ユーザーにとって、概要だけでも頭に入れておくことで、いつか直面する問題に 対する回答となりえるものです。）

induction タクティックについてもう少し

induction タクティックは、実はこれまで見てきたような、いささか 低レベルな作業をこなすだけのものではありません。

自然数に関する帰納的な公理の非形式的な記述を思い出してみてください。:

• もし P n が数値 n を意味する何かの命題だとして、命題 P が全ての数値 n に ついて成り立つことを示したい場合は、このような推論を することができます。:
  • P O が成り立つことを示す
  • もし P n' が成り立つなら, P (S n') が成り立つことを示す。
  • 任意の n について P n が成り立つと結論する。

我々が証明を intros n で始め、次に induction n とすると、 これはCoqに「特定の」 n について（それを仮定取り込むことで）考えて から、その後でそれを帰納法を使って任意の数値にまで推し進めるよう 示していることになります。

このようなときに Coq が内部的に行っていることは、帰納法を適用した変数を 「再一般化（ re-generalize ）」することです。 例えば、plus の結合則を証明するケースでは、

...最初に 3個の変数を全てコンテキストに導入しています。 これはつまり"任意の n, m, p について考える"という 意味になっています...

...ここで、induction タクティックを使い P n （任意の n に ついて n + (m + p) = (n + m) + p）を証明し、すぐに、 コンテキストにある特定の n についても証明します。

induction が作成した（帰納法の手順とも言うべき）二つ目の ゴールでは、 P n' ならば任意の n' で P (S n') が成り立つ ことを証明する必要があります。 この時に induction タクティックは P (S n') をゴールにしたまま、自動的に n' と P n' を コンテキストに導入してくれます。

induction をゴールにある量化された変数に適用してもかまいません。

induction n が m をゴールに残したままにしていることに注目してください。 つまり、今証明しようとしている帰納的な性質は、∀ m で表されて いるということです。

もし induction をゴールにおいて量化された変数に対して他の量化子の後に 適用すると、induction タクティックは自動的に変数をその量化子に基づいて コンテキストに導入します。

ここで n の代わりに m を induction しましょう。...

練習問題: ★, optional (plus_explicit_prop)

plus_assoc' と plus_comm' を、その証明とともに上の mult_0_r'' と 同じスタイルになるよう書き直しなさい。このことは、それぞれの定理が 帰納法で証明された命題に明確な定義を与え、この定義された命題から定理と 証明を示しています。

☐

冒険心を満足させるために、もう少し脱線してみましょう。 Definition でパラメータ化された命題を定義できるなら、 Fixpoint でも 定義できていいのではないでしょうか？もちろんできます！しかし、この種の 「再帰的なパラメータ化」は、日常的に使われる数学の分野と必ずしも調和するわけでは ありません。そんなわけで次の練習問題は、例としてはいささか不自然かもしれません。

練習問題: ★★★★, optional (true_upto_n__true_everywhere)

true_upto_n_example を満たすような再帰関数 true_upto_n__true_everywhere を定義しなさい。

☐

Prop における帰納法の原理

最初のほうで、我々は帰納的に定義された「集合」に対して、Coqが生成する 帰納法の原理をつぶさに見てきました。ev のように、帰納的に定義された 「命題」の帰納法の原理は、やや複雑でした。これらに共通して言えることですが、 これらを ev の証明に使おうとする際、帰納的な発想のもとで ev が持ちうる ものの中から使えそうな形になっているものを探します。それは 0 が偶数であることの 根拠であったり、ある n について S (S n) は偶数であるという根拠（もちろん、 これには n 自身が偶数であるということの根拠も含まれていなければ なりませんが）だったりするでしょう。しかしながら直観的な言い方をすると、 我々が証明したいものは根拠についての事柄ではなく、数値についての事柄です。 つまり、我々は根拠をベースに数値の属性を証明できるような帰納法の原理を 必要としているわけです。

例えば、ずいぶん前にお話ししたように、ev の帰納的な定義は、 こんな感じで...
    Inductive ev : nat → Prop :=
       | ev_0 : ev O
       | ev_SS : ∀ n:nat, ev n → ev (S (S n)).

... ここから生成される帰納法の原理はこんな風になります ...
    ev_ind_max :
       ∀ P : (∀ n : nat, ev n → Prop),
            P O ev_0 →
            (∀ (n : nat) (e : ev n),
              P n e → P (S (S n)) (ev_SS n e)) →
            ∀ (n : nat) (e : ev n), P n e

... なぜなら：

• ev は数値 n でインデックスされている（ ev に属するオブジェクト e は、いずれも特定の数 n が偶数であることの根拠となっている）ため、この命題 P は n とe の両方でパラメータ化されている。-- つまり、この帰納法の原理は一つの偶数と、それが偶数であることの根拠が揃っているような主張の証明に使われる。
  
  
• 偶数であることに根拠を与える方法は二つある（ ev のコンストラクタは二つある）ので、帰納法の原理を適用すると、二つのゴールが生成されます。:
  
  
  • P が O と ev_0 で成り立つことを証明する必要がある。
    
    
  • n が偶数で e がその偶数性の根拠であるとき、もし P が n と e のもとで成り立つなら、S (S n) と ev_SS n e のもとで成り立つことを証明する必要がある。
    
    
• もしこれらのサブゴールが証明できれば、この帰納法の原理によって P が全ての偶数 n とその偶数性の根拠 e のもとで真であることが示される。

しかしこれは、私たちが求めたり必要としているものより少しだけ柔軟にできていて、偶数性の根拠の断片を属性として含むような論理的主張を証明する方法を与えてくれます。我々の興味の対象は「数値の属性が偶数である」ことの証明なのですから、その興味の対象も数値に関する主張であって、根拠に対するものではないはずです。これにより、単に n だけでパラメータ化されていて、P がすべての偶数 n で成り立つことを示せるような命題 P を証明する際に帰納法の原理を得ることがより楽になります。


       ∀ P : nat → Prop,
          ... →
             ∀ n : nat, ev n → P n

このような理由で、Coqは実際には ev のために次のような帰納法の原理を生成します。:

Coqが根拠の式 e を、命題 P のパラメータから取り去っていることに注目してください。 その結果として、仮定 ∀ (n:nat) (e:ev n), ... を ∀ (n:nat), ev n → ... に書き換えています。すなわち、我々はすでに ev n から証明可能であることの 明白な根拠を求められていないのです。

ev_ind を自然言語で書き直すと、

• P が自然数の属性である（つまり、P が全ての n についての命題である）と仮定し、P n が偶数の場合常に成り立つことを示す。これは、以下を示すのに十分である。:
  
  
  • P が 0 において成り立つ。
    
    
  • 全ての n において、もし n が偶数で P が n において成り立つなら、P は S (S n) においても成り立つ。

induction とする代わりに ev_ind を直接 apply することもできます。 以下は、これと同じパターンです。

練習問題: ★★★, optional (prop_ind)

帰納的に定義された list と MyProp に対し、Coq がどのような帰納法の原理を 生成するか、予想して書き出し、次の行を実行した結果と比較しなさい。

☐

練習問題: ★★★, optional (ev_MyProp')

もう一度 ev_MyProp を証明しなさい。ただし、今度は induction タクティックの代わりに apply MyProp_ind を使いなさい。

☐

練習問題: ★★★★, optional (MyProp_pfobj)

もう一度 MyProp_ev と ev_MyProp を証明しなさい。ただし今度は、明確な 証明オブジェクトを手作業で構築（上の ev_plus4 でやったように）することで 証明しなさい。

☐

練習問題: ★★★, optional (p_provability)

次の、帰納的に定義された命題について考えてみてください。：

これについて、どのような時に p t n が証明可能であるか、その 条件をを自然言語で説明しなさい。

☐

追加練習問題

練習問題: ★★★★ (palindromes)

palindrome（回文）は、最初から読んでも逆から読んでも同じになるような シーケンスです。

• list X でパラメータ化され、それが palindrome であることを示すような帰納的

命題 pal を定義しなさい。（ヒント：これには三つのケースが必要です。この定義は、 リストの構造に基いたものとなるはずです。まず一つのコンストラクタ、


    c : ∀ l, l = rev l → pal l

は明らかですが、これはあまりうまくいきません。）

• 以下を証明しなさい。
         ∀ l, pal (l ++ rev l).
  
  
• 以下を証明しなさい。
         ∀ l, pal l → l = rev l.
  
  

☐

練習問題: ★★★★★, optional (palindrome_converse)

一つ前の練習問題で定義した pal を使って、これを証明しなさい。
     ∀ l, l = rev l → pal l.

☐

練習問題: ★★★★ (subsequence)

あるリストが、別のリストのサブシーケンス（ subsequence ）であるとは、 最初のリストの要素が全て二つ目のリストに同じ順序で現れるということです。 ただし、その間に何か別の要素が入ってもかまいません。例えば、
    [1,2,3]

は、次のいずれのリストのサブシーケンスでもあります。
    [1,2,3]
    [1,1,1,2,2,3]
    [1,2,7,3]
    [5,6,1,9,9,2,7,3,8]

しかし、次のいずれのリストのサブシーケンスでもありません。
    [1,2]
    [1,3]
    [5,6,2,1,7,3,8]

• list nat 上に、そのリストがサブシーケンスであることを意味するような命題 subseq を定義しなさい。（ヒント：三つのケースが必要になります）
  
  
• サブシーケンスである、という関係が「反射的」であることを証明しなさい。つまり、どのようなリストも、それ自身のサブシーケンスであるということです。
  
  
• 任意のリスト l1、 l2、 l3 について、もし l1 が l2 のサブシーケンスならば、 l1 は l2 ++ l3 のサブシーケンスでもある、ということを証明しなさい。.
  
  
• （これは少し難しいですので、任意とします）サブシーケンスという関係は推移的である、つまり、 l1 が l2 のサブシーケンスであり、 l2 が l3 のサブシーケンスであるなら、 l1 は l3 のサブシーケンスである、というような関係であることを証明しなさい。（ヒント：何について帰納法を適用するか、よくよく注意して下さい。）

☐

練習問題: ★★, optional (foo_ind_principle)

次のような、帰納的な定義をしたとします：
   Inductive foo (X : Set) (Y : Set) : Set :=
     | foo1 : X → foo X Y
     | foo2 : Y → foo X Y
     | foo3 : foo X Y → foo X Y.

次の空欄を埋め、この定義のために Coq が生成する帰納法の原理を完成させなさい。


   foo_ind
        : ∀ (X Y : Set) (P : foo X Y → Prop),
          (∀ x : X, __________________________________) →
          (∀ y : Y, __________________________________) →
          (________________________________________________) →
           ________________________________________________

☐

練習問題: ★★, optional (bar_ind_principle)

次に挙げた帰納法の原理について考えてみましょう：
   bar_ind
        : ∀ P : bar → Prop,
          (∀ n : nat, P (bar1 n)) →
          (∀ b : bar, P b → P (bar2 b)) →
          (∀ (b : bool) (b0 : bar), P b0 → P (bar3 b b0)) →
          ∀ b : bar, P b

これに対応する帰納的な集合の定義を書きなさい。
   Inductive bar : Set :=
     | bar1 : ________________________________________
     | bar2 : ________________________________________
     | bar3 : ________________________________________.

☐

練習問題: ★★, optional (no_longer_than_ind)

次のような、帰納的に定義された命題が与えられたとします：
  Inductive no_longer_than (X : Set) : (list X) → nat → Prop :=
    | nlt_nil : ∀ n, no_longer_than X [] n
    | nlt_cons : ∀ x l n, no_longer_than X l n →
                               no_longer_than X (x::l) (S n)
    | nlt_succ : ∀ l n, no_longer_than X l n →
                             no_longer_than X l (S n).

この命題のために Coq が生成する帰納法の原理を完成させなさい。
  no_longer_than_ind
       : ∀ (X : Set) (P : list X → nat → Prop),
         (∀ n : nat, ____________________) →
         (∀ (x : X) (l : list X) (n : nat),
          no_longer_than X l n → ____________________ →
                                  _____________________________ →
         (∀ (l : list X) (n : nat),
          no_longer_than X l n → ____________________ →
                                  _____________________________ →
         ∀ (l : list X) (n : nat), no_longer_than X l n →
           ____________________

☐

練習問題: ★★, optional (R_provability)

Coq に次のような定義を与えたとします：
    Inductive R : nat → list nat → Prop :=
      | c1 : R 0 []
      | c2 : ∀ n l, R n l → R (S n) (n :: l)
      | c3 : ∀ n l, R (S n) l → R n l.

次のうち、証明可能なのはどの命題でしょうか？

• R 2 [1,0]
• R 1 [1,2,1,0]
• R 6 [3,2,1,0]

☐