Prop\_J: 命題と根拠 =================== "アルゴリズムは計算可能な証明である。"(Robert Harper) :: Require Export Poly_J. 命題によるプログラミング ------------------------ 読者への注意: この章で紹介するコンセプトは、初めて見た時には抽象的すぎるように感じられるかもしれません。たくさんの練習問題を用意しておいたので、テキストの詳細を理解する途中であっても大部分は解けるはずです。できるかぎり多くの問題、特に★の問題には重点的に挑戦するようにしてください。 これまで宣言したり証明した文は等式の形をしたものだけでした。しかし、数学で用いられる文や証明にはもっと豊かな表現力があります。この章では Coq で作れる数学的な文(命題; *proposition* )の種類と、その証明を「根拠( *evidence* )を与えること」でどのように進めていくか、もう少し詳しく、基本的な部分から見ていきましょう。 命題( *proposition* )は、"2足す2は4と等しい"のような事実に基づく主張を表現するための文です。Coq において命題は\ ``Prop``\ 型の式として書かれます。これまであまりそれについて明示的に触れてはきませんでしたが、皆さんはすでに多くの例を見てきています。 :: Check (2 + 2 = 4). Check (ble_nat 3 2 = false). 証明可能な主張も証明不能な主張も、どちらも完全な命題であると言えます。しかし単に命題であるということと、証明可能であるということは別ものです! :: Check (2 + 2 = 5). ``2 + 2 = 4``\ も\ ``2 + 2 = 5``\ も\ ``Prop``\ の型をもった妥当な式です。 これまで Coq の中で命題を使う方法は1つしか見ていません。\ ``Theorem``\ (あるいは\ ``Lemma``\ 、\ ``Example``\ )の宣言の中でだけです。 :: Theorem plus_2_2_is_4 : 2 + 2 = 4. Proof. reflexivity. Qed. しかし命題にはもっといろいろな使い方があります。例えば、他の種類の式(数字、関数、型、型関数など)と同様に、\ ``Definition``\ を使うことで命題に名前を与えることができます。 :: Definition plus_fact : Prop := 2 + 2 = 4. Check plus_fact. こうすることで、命題が使える場所ならどこでも、例えば、\ ``Theorem``\ 宣言内の主張などとして使うことができます。 :: Theorem plus_fact_is_true : plus_fact. Proof. reflexivity. Qed. ここまでに登場したすべての命題は等式の形をした命題でした。それ以外にも新しい命題の形を作ることができます。例えば、命題\ ``P``\ と\ ``Q``\ が与えられば、"``P``\ ならば\ ``Q``"という命題を作れます。 :: Definition strange_prop1 : Prop := (2 + 2 = 5) -> (99 + 26 = 42). また、自由変数\ ``n``\ を含む命題\ ``P``\ が与えられれば、\ ``forall n, P``\ という形の命題を作れます。 :: Definition strange_prop2 := forall n, (ble_nat n 17 = true) -> (ble_nat n 99 = true). 最後に、パラメータ化された命題(\ *parameterized proposition* )の定義を紹介します。例えば、"数nが偶数である"という主張はどのようになるでしょうか?偶数を判定する関数は書いてあるので、偶数であるという定義は"``n``\ が偶数であることと\ ``evenb n = true``\ は同値である"が考えられます。 :: Definition even (n:nat) : Prop := evenb n = true. これは\ ``even``\ を関数として定義します。この関数は数\ ``n``\ を適用されると、\ ``n``\ が偶数であることを示す命題を返します。 :: Check even. Check (even 4). Check (even 3). ``even``\ の型\ ``nat -> Prop``\ は3つの意味を持っています。(1) "``even``\ は数から命題への関数である。"(2) "``even``\ は数\ ``n``\ でインデックスされた命題の集りである"。(3) "``even``\ は数の性質(*property*)である。" 命題(パラメータ化された命題も含む)はCoqにおける第一級(\ *first-class*\ )市民です。このため、ほかの定義の中でこれらの命題を使うことができます。 :: Definition even_n__even_SSn (n:nat) : Prop := (even n) -> (even (S (S n))). 複数の引数を受け取るように定義することや.. :: Definition between (n m o: nat) : Prop := andb (ble_nat n o) (ble_nat o m) = true. ...部分適用もできます。 :: Definition teen : nat->Prop := between 13 19. 他の関数に、引数として命題(パラーメータ化された命題も含む)を渡すことすらできます。 :: Definition true_for_zero (P:nat->Prop) : Prop := P 0. Definition true_for_n__true_for_Sn (P:nat->Prop) (n:nat) : Prop := P n -> P (S n). 2つのアンダースコアを続けた\ ``x__y``\ という形式の名前は、"``x``\ ならば\ ``y``\ である"と読みます。 パラメータ化された命題を引数として渡す関数をさらに2つ紹介します。1つ目の関数は、ある自然数\ ``n'``\ について\ ``P``\ が真ならば常に\ ``n'``\ の次の数でも\ ``P``\ が真であることを述べています。 :: Definition preserved_by_S (P:nat->Prop) : Prop := forall n', P n' -> P (S n'). そして次の関数は、すべての自然数について与えられた命題が真であることを述べています。 :: Definition true_for_all_numbers (P:nat->Prop) : Prop := forall n, P n. これらを一つにまとめることで、自然数に関する帰納法の原理を自分で再宣言できます。パラメータ化された命題\ ``P``\ が与えられた場合、\ ``0``\ について\ ``P``\ が真であり、\ ``P n'``\ が真のとき\ ``P (S n')``\ が真であるならば、すべての自然数について\ ``P``\ は真である。 :: Definition our_nat_induction (P:nat->Prop) : Prop := (true_for_zero P) -> (preserved_by_S P) -> (true_for_all_numbers 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 good_day : day -> Prop := | gd_sat : good_day saturday | gd_sun : good_day sunday. ``Inductive``\ キーワードは、「データ値の集合を定義する場合(``Type``\ の世界)」であっても「根拠の集合を定義する場合(``Prop``\ の世界)」であってもまったく同じ意味で使われます。上記の定義の意味はそれぞれ次のようになっています: - 最初の行は「\ ``good_day``\ は日によってインデックスされた命題であること」を宣言しています。 - 二行目は\ ``gd_sat``\ コンストラクタを宣言しています。このコンストラクタは\ ``good_day saturday``\ という主張の根拠として使えます。 - 三行目は\ ``gd_sun``\ コンストラクタを宣言しています。このコンストラクタは\ ``good_day sunday``\ という主張の根拠として使えます。 言い換えると、ある日が良いということを"土曜日は良い、日曜日は良い、それだけだ"と言うことで定義しています。これによって、日曜日が良いということを証明したいときは、\ ``good_day``\ の意味を定義したときにそう言っていたかを調べるだけで済みます。 :: Theorem gds : good_day sunday. Proof. apply gd_sun. Qed. コンストラクタ\ ``gd_sun``\ は、日曜日が良いという主張を正当化する"原始的(primitive)な根拠"、つまり公理です。 同様に、月曜日は火曜日の前に来て、火曜日は水曜日の前に来て、...、ということを宣言する公理を、2つの日をパラメータとして取る命題\ ``day_before``\ として定義できます。 :: Inductive day_before : day -> day -> Prop := | db_tue : day_before tuesday monday | db_wed : day_before wednesday tuesday | db_thu : day_before thursday wednesday | db_fri : day_before friday thursday | db_sat : day_before saturday friday | db_sun : day_before sunday saturday | db_mon : day_before monday sunday. 帰納的な定義による命題で導入される公理では全称記号を使うこともできます。例えば、「どの日だって歌いだしたくなるほど素敵な日だ」という事実については、わざわざ説明する必要もないでしょう :: Inductive fine_day_for_singing : day -> Prop := | fdfs_any : forall d:day, fine_day_for_singing d. この行は、もし\ ``d``\ が日ならば、\ ``fdfs_any d``\ は\ ``fine_day_for_singing d``\ の根拠として使えるということを宣言してます。言い換えると、\ ``d``\ が\ ``fine_day_for_singing``\ であるという根拠を\ ``fdfs_any``\ を\ ``d``\ に適用することで作ることができます。 要するに、水曜日は「歌いだしたくなるほど素敵な日」だということです。 :: Theorem fdfs_wed : fine_day_for_singing wednesday. Proof. apply fdfs_any. Qed. これも同じように、最初の行は"私は命題\ ``fine_day_for_singing wednesday``\ に対する根拠を示し、その根拠をあとで参照するために\ ``fdfs_wed``\ という名前を導入しようと思っている"と解釈できます。二行目は、Coqにその根拠をどのように組み立てるかを示しています。 証明オブジェクト ~~~~~~~~~~~~~~~~ 同じことができる、もっと原始的な方法もあります。\ ``Definiton``\ の左辺を導入しようとしている名前にし、右辺を根拠の構築方法ではなく、根拠そのものにすればいいのです。 :: Definition fdfs_wed' : fine_day_for_singing wednesday := fdfs_any wednesday. Check fdfs_wed. Check fdfs_wed'. 式\ ``fdfs_any wednesday``\ は、パラメータを受け取る公理\ ``fdfs_any``\ を 特定の引数\ ``wednesday``\ によって具体化したものととらえることができます。別の見方をすれば、\ ``fdfs_any``\ を原始的な"根拠コンストラクタ"として捉えることもできます。この根拠コンストラクタは、特定の日を適用されると、その日が「歌わずにはいられないほどよい日」である根拠を表します。型\ ``forall d:day, fine_day_for_singing d``\ はこの機能を表しています。これは、前章で登場した多相型\ ``forall X, list X``\ において\ ``nil``\ コンストラクタが型からその型を持つ空リストを返す関数であったことと同様です。 もうちょっと面白い例を見てみましょう。"OK"な日とは(1)良い日であるか(2)OKな日の前日であるとしましょう。 :: Inductive ok_day : day -> Prop := | okd_gd : forall d, good_day d -> ok_day d | okd_before : forall d1 d2, ok_day d2 -> day_before d2 d1 -> ok_day d1. 最初のコンストラクタは"``d``\ がOKな日であることを示す一つ目の方法は、\ ``d``\ が良い日であるという根拠を示すことである"と読めます。二番目のは"``d1``\ がOKであることを示す別の方法は、その日が別の日\ ``d2``\ の前日であり、\ ``d2``\ がOKであるという根拠を示すことである"と読めます。 ここで\ ``wednesday``\ がOKであることを証明したいとしましょう。証明するには2つの方法があります1つめは原始的な方法であり、コンストラクタの適用を何度もネストすることで、正しい型を持つ式を書き下します。 :: Definition okdw : ok_day wednesday := okd_before wednesday thursday (okd_before thursday friday (okd_before friday saturday (okd_gd saturday gd_sat) db_sat) db_fri) db_thu. 2つめの方法は、機械に支援してもらう方法です。証明モードに入り、最終的に満たされるまでゴールやサブゴールを通してCoqに案内してもらいます。 :: Theorem okdw' : ok_day wednesday. Proof. apply okd_before with (d2:=thursday). apply okd_before with (d2:=friday). apply okd_before with (d2:=saturday). apply okd_gd. apply gd_sat. apply db_sat. apply db_fri. apply db_thu. Qed. しかし、根本的なところでこの2つの証明方法は同じです。証明スクリプト内のコマンドを実行するときにCoqが実際にやっていることは、目的の型を持つ式を構築することと全く同じです。 :: Print okdw'. この式は一般的に証明オブジェクト(Proof object)と呼ばれます。 証明オジェクトはCoqの根本を支えています。タクティックによる証明は、自分で証明オブジェクトを書く代わりに、証明オブジェクトを構築する方法をCoqに指示する基本的なプログラムです。もちろん、この例では証明オブジェクトはタクティックによる証明よりも短くなっています。しかし、もっと興味深い証明では証明オブジェクトを手で構築することが苦痛に思えるほど大きく複雑になります。この後の章では、各ステップを書くことなく複雑な証明オブジェクトを構築できる自動化されたタクティックをたくさん紹介します。 カリー・ハワード対応 ~~~~~~~~~~~~~~~~~~~~ この :: 命題 ~ 集合 / 型 証明 ~ 元、要素 / データ値 という類似性は、カリー・ハワード対応(もしくはカリー・ハワード同型, Curry-Howard correspondence, Curry-Howard isomorphism)と呼ばれます。これにより多くのおもしろい性質が導けます。 集合に空集合、単集合、有限集合、無限集合があり、それぞれが0個、1個、多数の元を持っているように、命題も0個、1個、多数、無限の証明を持ちえます。命題\ ``P``\ の各要素は、それぞれ異なる\ ``P``\ の根拠です。もし要素がないならば、\ ``P``\ は証明不能です。もしたくさんの要素があるならば、\ ``P``\ には多数の異なった証明があります。 含意 ~~~~ これまで\ ``->``\ 演算子(含意)を小さい命題から大きな命題を作るために使ってきました。このような命題に対する根拠はどのようになるでしょうか?次の文を考えてみてください。 :: Definition okd_before2 := forall d1 d2 d3, ok_day d3 -> day_before d2 d1 -> day_before d3 d2 -> ok_day d1. これを日本語で書くと、もし3つの日があるとして、\ ``d1``\ が\ ``d2``\ の前日であり、\ ``d2``\ が\ ``d3``\ の前日であり、かつ\ ``d3``\ がOKであるということがわかっているならば、\ ``d1``\ もOKである、という意味になります。 ``okd_before2``\ をタクティッックを使って証明するのは簡単なはずです... 練習問題: ★, optional (okd\_before2\_valid) ''''''''''''''''''''''''''''''''''''''''''' :: Theorem okd_before2_valid : okd_before2. Proof. (* FILL IN HERE *) Admitted. ☐ ところで、これに対応する証明オブジェクトはどんな感じでしょうか? 答: 含意としての\ ``->``\ と、関数の型の\ ``->``\ の記法はそっくりです。これをそのまま解釈すると、\ ``forall d1 d2 d3, ok_day d3 -> day_before d2 d1 -> day_before d3 d2 -> ok_day d1``\ という型をもった式を見付ける必要があります。なので探すものは6個の引数(3個の日と、3個の根拠)を受け取り、1個の根拠を返す関数です!それはこんな感じです。 :: Definition okd_before2_valid' : okd_before2 := fun (d1 d2 d3 : day) => fun (H : ok_day d3) => fun (H0 : day_before d2 d1) => fun (H1 : day_before d3 d2) => okd_before d1 d2 (okd_before d2 d3 H H1) H0. 練習問題: ★, optional (okd\_before2\_valid\_defn) ''''''''''''''''''''''''''''''''''''''''''''''''' 下記の結果としてCoqが出力するものを予測しなさい。 :: Print okd_before2_valid. 帰納的に定義された型に対する帰納法の原理 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ``Inductive``\ でデータ型を新たに定義するたびに、Coqは帰納法の原理に対応する公理を自動生成します。 型\ ``t``\ に対応する帰納法の原理は\ ``t_ind``\ という名前になります。ここでは自然数に対するものを示します。 :: Check nat_ind. これは先ほど定義した\ ``our_nat_induction``\ の性質とまったく同じであることに注意してください。 ``induction``\ タクティックは、基本的には\ ``apply t_ind``\ の単純なラッパーです。もっとわかりやすくするために、\ ``induction``\ タクティックのかわりに\ ``apply nat_ind``\ を使っていくつかの証明をしてみる実験をしてみましょう。例えば、\ ``Basics_J``\ の章で見た定理の別の証明を見てみましょう。 :: Theorem mult_0_r' : forall n:nat, n * 0 = 0. Proof. apply nat_ind. Case "O". reflexivity. Case "S". simpl. intros n IHn. rewrite -> IHn. reflexivity. Qed. この証明は基本的には前述のものと同じですが、細かい点で特筆すべき違いがあります。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``\ タクティックを使わずに、下記の証明を完成させなさい。 :: Theorem plus_one_r' : forall n:nat, n + 1 = S n. Proof. (* FILL IN HERE *) Admitted. ☐ ほかの\ ``Inductive``\ によって定義されたデータ型に対しても、Coqは似た形の帰納法の原理を生成します。コンストラクタ\ ``c1``...\ ``cn``\ を持った型\ ``t``\ を定義すると、Coqは次の形の定理を生成します。 :: t_ind : forall P : t -> Prop, ... c1の場合 ... -> ... c2の場合 ... -> ... -> ... cnの場合 ... -> forall n : t, P n 各場合分けの形は、対応するコンストラクタの引数の数によって決まります。一般的な規則を紹介する前に、もっと例を見てみましょう。最初は、コンストラクタが引数を取らない場合です。 :: Inductive yesno : Type := | yes : yesno | no : yesno. Check yesno_ind. 練習問題: ★ (rgb) ''''''''''''''''' 次のデータ型に対してCoqが生成する帰納法の原理を予測しなさい。紙に答えを書いたのち、Coqの出力と比較しなさい。 :: Inductive rgb : Type := | red : rgb | green : rgb | blue : rgb. Check rgb_ind. ☐ 別の例を見てみましょう。引数を受け取るコンストラクタがある場合です。 :: Inductive natlist : Type := | nnil : natlist | ncons : nat -> natlist -> natlist. Check natlist_ind. 練習問題: ★ (natlist1) '''''''''''''''''''''' 上記の定義をすこし変えたとしましょう。 :: Inductive natlist1 : Type := | nnil1 : natlist1 | nsnoc1 : natlist1 -> nat -> natlist1. このとき、帰納法の原理はどのようになるでしょうか? ☐ これらの例より、一般的な規則を導くことができます。 - 型宣言は複数のコンストラクタを持ち、各コンストラクタが帰納法の原理の各節に対応する。 - 各コンストラクタ\ ``c``\ は引数\ ``a1``..\ ``an``\ を取る。 - ``ai``\ は\ ``t``\ (定義しようとしているデータ型)、もしくは別の型\ ``s``\ かのどちらかである。 - 帰納法の原理において各節は以下のことを述べている。 - "型\ ``a1``...\ ``an``\ のすべての値\ ``x1``...\ ``xn``\ について、各\ ``x``\ について\ ``P``\ が成り立つならば、\ ``c x1 ... xn``\ についても\ ``P``\ が成り立つ" 練習問題: ★ (ExSet) ''''''''''''''''''' 帰納的に定義された集合に対する帰納法の原理が次のようなものだとします。 :: ExSet_ind : forall P : ExSet -> Prop, (forall b : bool, P (con1 b)) -> (forall (n : nat) (e : ExSet), P e -> P (con2 n e)) -> forall e : ExSet, P e ``ExSet``\ の帰納的な定義を示しなさい。 :: Inductive ExSet : Type := (* FILL IN HERE *) . ☐ 多相的なデータ型ではどのようになるでしょうか? 多相的なリストの帰納的定義は\ ``natlist``\ によく似ています。 :: Inductive list (X:Type) : Type := | nil : list X | cons : X -> list X -> list X. ここでの主な違いは、定義全体が集合\ ``X``\ によってパラメータ化されていることです。つまり、それぞれの\ ``X``\ ごとに帰納型\ ``list X``\ を定義していることになります。(定義本体で\ ``list``\ が登場するときは、常にパラメータ\ ``X``\ に適用されていることに注意してください。)帰納法の原理も同様に\ ``X``\ によってパラメータ化されます。 :: list_ind : forall (X : Type) (P : list X -> Prop), P [] -> (forall (x : X) (l : list X), P l -> P (x :: l)) -> forall l : list X, P l この表現(と\ ``list_ind``\ の全体的な形)に注目してください。帰納法の原理全体が\ ``X``\ によってパラメータ化されています。別の見方をすると、\ ``list_ind``\ は多相関数と考えることができます。この関数は、型\ ``X``\ が適用されると、\ ``list X``\ に特化した帰納法の原理を返します。 練習問題: ★ (tree) '''''''''''''''''' 次のデータ型に対してCoqが生成する帰納法の原理を予測しなさい。答えが書けたら、それをCoqの出力と比較しなさい。 :: Inductive tree (X:Type) : Type := | leaf : X -> tree X | node : tree X -> tree X -> tree X. Check tree_ind. ☐ 練習問題: ★ (mytype) '''''''''''''''''''' 以下の帰納法の原理を生成する帰納的定義を探しなさい。 :: mytype_ind : forall (X : Type) (P : mytype X -> Prop), (forall x : X, P (constr1 X x)) -> (forall n : nat, P (constr2 X n)) -> (forall m : mytype X, P m -> forall n : nat, P (constr3 X m n)) -> forall m : mytype X, P m ☐ 練習問題: ★, optional (foo) ''''''''''''''''''''''''''' 以下の帰納法の原理を生成する帰納的定義を探しなさい。 :: foo_ind : forall (X Y : Type) (P : foo X Y -> Prop), (forall x : X, P (bar X Y x)) -> (forall y : Y, P (baz X Y y)) -> (forall f1 : nat -> foo X Y, (forall n : nat, P (f1 n)) -> P (quux X Y f1)) -> forall f2 : foo X Y, P f2 ☐ 練習問題: ★, optional (foo') '''''''''''''''''''''''''''' 次のような帰納的定義があるとします。 :: Inductive foo' (X:Type) : Type := | C1 : list X -> foo' X -> foo' X | C2 : foo' X. ``foo'``\ に対してCoqはどのような帰納法の原理を生成するでしょうか?空欄を埋め、Coqの結果と比較しなさい :: foo'_ind : forall (X : Type) (P : foo' X -> Prop), (forall (l : list X) (f : foo' X), _______________________ -> _______________________ ) -> ___________________________________________ -> forall f : foo' X, ________________________ ☐ 帰納法の仮定 ~~~~~~~~~~~~ この概念において"帰納法の仮定"はどこにあてはまるでしょうか? 数に関する帰納法の原理 :: forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n は、すべての命題\ ``P``\ (より正確には数値 n を引数にとる命題\ ``P``\ )について成り立つ一般的な文です。この原理を使うときはいつも、\ ``nat->Prop``\ という型を持つ式を\ ``P``\ として選びます。 この式に名前を与えることで、証明をもっと明確にできます。例えば、\ ``mult_0_r``\ を"``forall n, n * 0 = 0``\ "と宣言するかわりに、"``forall n, P_m0r n``\ "と宣言します。なお、ここで\ ``P_m0r``\ は次のように定義されています。 :: Definition P_m0r (n:nat) : Prop := n * 0 = 0. あるいは :: Definition P_m0r' : nat->Prop := fun n => n * 0 = 0. でも同じ意味です。 これで、証明する際に\ ``P_m0r``\ がどこに表われるかが分かりやすくなります。 :: Theorem mult_0_r'' : forall n:nat, P_m0r n. Proof. apply nat_ind. Case "n = O". reflexivity. Case "n = S n'". unfold P_m0r. simpl. intros n' IHn'. apply IHn'. Qed. このように名前をつける手順は通常の証明では不要です。しかし、1つ2つ試してみると、帰納法の仮定がどのようなものなのかが分かりやすくなります。\ ``forall n, P_m0r n``\ を\ ``n``\ による帰納法(\ ``induction``\ か\ ``apply nat_ind``\ を使う)によって証明しようとすると、最初のサブゴールでは\ ``P_m0r 0``\ ("``P``\ が0に対して成り立つ")を証明しなければならず、2つめのサブゴールでは\ ``forall 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``\ を返すなら、その数は偶数である")を使って間接的に定義するのではなく、「偶数とは何を意味するか」を根拠を使って直接定義することができるのです。 :: Inductive ev : nat -> Prop := | ev_0 : ev O | ev_SS : forall n:nat, ev n -> ev (S (S n)). この定義は、数\ ``m``\ が偶数であるという根拠を与える方法が2つあることを示しています。第一に、\ ``0``\ は偶数であり、\ ``ev_0``\ がこれに対する根拠です。次に、任意の\ ``n``\ に対して\ ``m = S (S n)``\ とし、\ ``n``\ が偶数であるという根拠\ ``e``\ を与えることができるならば、\ ``m``\ も偶数であると言え、\ ``ev_SS n e``\ がその根拠となります。 練習問題: ★, optional (four\_ev) '''''''''''''''''''''''''''''''' 4が偶数であることをタクティックによる証明と証明オブジェクトによる証明で示しなさい。 :: Theorem four_ev' : ev 4. Proof. (* FILL IN HERE *) Admitted. Definition four_ev : ev 4 := (* FILL IN HERE *) admit. ☐ 練習問題: ★★ (ev\_plus4) '''''''''''''''''''''''' ``n``\ が偶数ならば\ ``4+n``\ も偶数であることをタクティックによる証明と証明オブジェクトによる証明で示しなさい。 :: Definition ev_plus4 : forall n, ev n -> ev (4 + n) := (* FILL IN HERE *) admit. Theorem ev_plus4' : forall n, ev n -> ev (4 + n). Proof. (* FILL IN HERE *) Admitted. ☐ 練習問題: ★★ (double\_even) ''''''''''''''''''''''''''' 次の命題をタクティックによって証明しなさい。 :: Theorem double_even : forall n, ev (double n). Proof. (* FILL IN HERE *) Admitted. ☐ 練習問題: ★★★★, 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``\ タクティックを使ってみましょう。 :: Theorem ev_minus2: forall n, ev n -> ev (pred (pred n)). Proof. intros n E. destruct E as [| n' E']. Case "E = ev_0". simpl. apply ev_0. Case "E = ev_SS n' E'". simpl. apply E'. Qed. 練習問題: ★ (ev\_minus2\_n) ''''''''''''''''''''''''''' ``E``\ の代わりに\ ``n``\ に対して\ ``destruct``\ するとどうなるでしょうか? ☐ ``n``\ が偶数であるという根拠に対して\ ``induction``\ を実行することもできます。\ ``ev``\ を満たす\ ``n``\ に対して、先に定義した\ ``evenb``\ 関数が\ ``true``\ を返すことを示すために使ってみましょう。 :: Theorem ev_even : forall n, ev n -> even n. Proof. intros n E. induction E as [| n' E']. Case "E = ev_0". unfold even. reflexivity. Case "E = ev_SS n' E'". unfold even. apply IHE'. Qed. (もちろん、\ ``even n -> ev n``\ も成り立つはずです。 どのように証明するかは次の章で説明します。) 練習問題: ★ (ev\_even\_n) ''''''''''''''''''''''''' この証明を\ ``E``\ でなく\ ``n``\ に対する帰納法として実施できますか? ☐ 帰納的に定義された命題に対する帰納法の原理は、帰納的に定義された集合のそれとまったく同じ形をしているわけではありません。今の段階では、根拠\ ``ev n``\ に対する帰納法は\ ``n``\ に対する帰納法に似ているが、\ ``ev n``\ が成立する数についてのみ着目することができると直感的に理解しておいて問題ありません。\ ``ev``\ の帰納法の原理をもっと深く見て行き、実際に何を起こっているかを説明します。 練習問題: ★ (l\_fails) '''''''''''''''''''''' :: *) FILL IN HERE 次の証明はうまくいきません。 [[ Theorem l : forall n,ev n.Proof.intros n. induction n.Case "O". simpl. apply ev\_0.Case "S"....]]理由を簡潔に説明しない。 (\* FILL IN HERE \*) ☐ 練習問題: ★★ (ev\_sum) '''''''''''''''''''''' 帰納法が必要な別の練習問題をやってみましょう。 :: Theorem ev_sum : forall n m, ev n -> ev m -> ev (n+m). Proof. (* FILL IN HERE *) Admitted. ☐ 「\ ``n+2``\ が偶数ならば\ ``n``\ も偶数である」という偶数に関する根拠を分析したいとします。この種の場合分けに\ ``destruct``\ を使ってみたくなるかもしれません。 :: Theorem SSev_ev_firsttry : forall n, ev (S (S n)) -> ev n. Proof. intros n E. destruct E as [| n' E']. Admitted. しかし、これはうまくいきません。 例えば、最初のサブゴールにおいて、\ ``n``\ が\ ``0``\ であるという情報が失われてしまいます。ここで使うべきは、\ ``inversion``\ です。 :: Theorem SSev_even : forall n, ev (S (S n)) -> ev n. Proof. intros n E. inversion E as [| n' E']. apply E'. Qed. このような\ ``inversion``\ の使い方は最初はちょっと謎めいて思えるかもしれません。これまでは、\ ``inversion``\ は等号に関する命題に対して使い、コンストラクタから元のデータを取り出すためか、別のコンストラクタを区別するためににしか使っていませんでした。しかし、ここでは\ ``inversion``\ が 帰納的に定義された命題に対する根拠を分析するためにも使えることを紹介しました。 ここで、\ ``inversion``\ が一般にはどのように動作するかを説明します。\ ``I``\ が現在のコンテキストにおいて帰納的に宣言された仮定\ ``P``\ を参照しているとします。ここで、\ ``inversion I``\ は、\ ``P``\ のコンストラクタごとにサブゴールを生成します。 各サブゴールにおいて、 コンストラクタが\ ``P``\ を証明するのに必要な条件によって\ ``I``\ が置き換えられます。サブゴールのうちいくつかは矛盾が存在するので、\ ``inversion``\ はそれらを除外します。残っているのは、元のゴールが成り立つことを示すのに必要なサブゴールです。 先ほどの例で、\ ``inversion``\ は\ ``ev (S (S n))``\ の分析に用いられ、 これはコンストラクタ\ ``ev_SS``\ を使って構築されていることを判定し、そのコンストラクタの引数を仮定に追加した新しいサブゴールを生成しました。(今回は使いませんでしたが、補助的な等式も生成しています。)このあとの例では、inversion のより一般的な振る舞いについて調べていきましょう。 練習問題: ★ (inversion\_practice) ''''''''''''''''''''''''''''''''' :: Theorem SSSSev_even : forall n, ev (S (S (S (S n)))) -> ev n. Proof. (* FILL IN HERE *) Admitted. ``inversion``\ タクティックは、仮定が矛盾していることを示し、ゴールを達成するためにも使えます。 :: Theorem even5_nonsense : ev 5 -> 2 + 2 = 9. Proof. (* FILL IN HERE *) Admitted. ☐ 一般に、帰納的な命題には\ ``destruct``\ の代わりに\ ``inversion``\ を使えます。このことは一般的に、コンストラクタごとに場合分けができることを示しています。加えて、いくつかの補助的な等式も得ることができます。なお、ゴールはその等式によって書き換えられていますが、その他の仮定は書き換えられていません。 :: Theorem ev_minus2': forall n, ev n -> ev (pred (pred n)). Proof. intros n E. inversion E as [| n' E']. Case "E = ev_0". simpl. apply ev_0. Case "E = ev_SS n' E'". simpl. apply E'. Qed. 練習問題: ★★★ (ev\_ev\_even) '''''''''''''''''''''''''''' 何に対して帰納法を行えばいいかを探しなさい。(ちょっとトリッキーですが) :: Theorem ev_ev_even : forall n m, ev (n+m) -> ev n -> ev m. Proof. (* FILL IN HERE *) Admitted. ☐ 練習問題: ★★★, optional (ev\_plus\_plus) '''''''''''''''''''''''''''''''''''''''' 既存の補題を適用する必要のある練習問題です。帰納法も場合分けも不要ですが、書き換えのうちいくつかはちょっと大変です。Basics\_J.v の\ ``plus_swap'``\ で使った\ ``replace``\ タクティックを使うとよいかもしれません。 :: Theorem ev_plus_plus : forall n m p, ev (n+m) -> ev (n+p) -> ev (m+p). Proof. (* FILL IN HERE *) Admitted. ☐ なぜ命題を帰納的に定義するのか? ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ここまで見てきたように "ある数が偶数である" というのは次の2通りの方法で解釈されます。間接的には「テスト用の\ ``evenb``\ 関数」によって、直接的には「偶数であることの根拠の構築方法を帰納的に記述すること」によってです。これら2つの偶数の定義は、ほぼ同じくらい楽に宣言できますし、同じように動きます。どちらを選ぶかは基本的に好みの問題です。 しかし、興味深いほかの性質、例えば「テスト用の関数を書くのが難しかったり不可能だったりする」ようなことがあることを考えると、直接的な帰納的な定義のほうが好ましいと言えます。例えば以下のように定義される\ ``MyProp``\ という性質について考えてみましょう。 - ``4``\ は性質\ ``MyProp``\ を満たす - ``n``\ が性質\ ``MyProp``\ を満たすならば、\ ``4+n``\ も満たす - もし\ ``2+n``\ が性質\ ``MyProp``\ を満たすならば、\ ``n``\ も満たす - その他の数は、性質\ ``MyProp``\ を満たさない これは数の集合の定義としてはなんの問題もありませんが、この定義をそのままCoqのFixPointに変換することはできません。(それだけでなく他の言語の再帰関数に変換することもできません。)\ ``Fixpoint``\ を用いてこの性質をテストするうまい方法を見つけられるかもしれません。(実際のところ、この場合はそれほど難しいことではありません)しかし、一般的にこういうことをしようとすると、かなりあれこれ考える必要があるでしょう。実際、Coqの\ ``Fixpoint``\ は停止する計算しか定義できないので、定義しようとする性質が計算不能なものだった場合、どれだけがんばっても\ ``Fixpoint``\ では定義できません。 一方、性質\ ``MyProp``\ がどのようなものかの根拠を与える帰納的な定義を書くことは、非常に簡単です。 :: Inductive MyProp : nat -> Prop := | MyProp1 : MyProp 4 | MyProp2 : forall n:nat, MyProp n -> MyProp (4 + n) | MyProp3 : forall n:nat, MyProp (2 + n) -> MyProp n. ``MyProp``\ の非形式的な定義の最初の3つの節は、帰納的な定義の最初の3つの節に反映されています。4つ目の節は、\ ``Inductive``\ キーワードによって強制されます。 これで、偶数のときにやったように、ある数が\ ``MyProp``\ を満たすことの根拠を作ることができます。 :: Theorem MyProp_ten : MyProp 10. Proof. apply MyProp3. simpl. assert (12 = 4 + 8) as H12. Case "Proof of assertion". reflexivity. rewrite -> H12. apply MyProp2. assert (8 = 4 + 4) as H8. Case "Proof of assertion". reflexivity. rewrite -> H8. apply MyProp2. apply MyProp1. Qed. 練習問題: ★★ (MyProp) ''''''''''''''''''''' MyPropに関する便利な2つの事実があります。証明はあなたのために残してあります。 :: Theorem MyProp_0 : MyProp 0. Proof. (* FILL IN HERE *) Admitted. Theorem MyProp_plustwo : forall n:nat, MyProp n -> MyProp (S (S n)). Proof. (* FILL IN HERE *) Admitted. ☐ これらを使って、\ ``MyProp``\ は全ての奇数について成り立つことと、その逆も成り立つをことを示せます。 :: Theorem MyProp_ev : forall n:nat, ev n -> MyProp n. Proof. intros n E. induction E as [| n' E']. Case "E = ev_0". apply MyProp_0. Case "E = ev_SS n' E'". apply MyProp_plustwo. apply IHE'. Qed. この定理の非形式的な証明は次のようになります。 *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) '''''''''''''''''''''''''' :: Theorem ev_MyProp : forall n:nat, MyProp n -> ev n. Proof. (* FILL IN HERE *) Admitted. ☐ 練習問題: ★★★, 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``\ の要素だけが上の二つの条件を満たしていて、それ以外のものはこの集合に入っていない)。 型と種類 (*kinds*) ~~~~~~~~~~~~~~~~~~ ざっくり言うと、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``\ など)には、「ひとつ上位の」分類 -- それは, 「型(もしくは命題)の型を表す式」のようなものと考えてもらっていいですが -- が可能です。それを、単なる「型」と混同しないために「種類 (*kinds*)」と呼ぶことにします。例えば、\ ``nat``\ や\ ``nat->nat``\ 、\ ``list nat``\ などは全て\ ``Type``\ という「種類」ですし、\ ``list``\ は\ ``Type -> Type``\ 、\ ``ev``\ は\ ``nat -> Prop``\ という種類です。 命題 vs. ブール値 ~~~~~~~~~~~~~~~~~ 命題とブール値は、一見とてもよく似ているように見えます。しかしこの二つは根本的に違うものです! - ブール値は、「計算の世界における値」です。\ ``bool``\ 型の式は全て、(自由変数を持っていない限り)必ず\ ``true``\ か\ ``false``\ のどちらかに簡約することができます。 - 命題は「論理の世界にいおける型」です。これらは「証明可能(この型の式を書くことができる)」か、「証明不能(そのような式は存在しない)」かのいずれかです。従って「命題が\ ``true``\ である」というような言い方は意味を持ちません。我々は時折、命題に対してそれが "true" か "false" というようなことを言ってしまいがちですが、厳格に言えばこれは間違っています。命題は「証明可能かそうでないか」のどちらかです。 関数 vs. 限量子 ~~~~~~~~~~~~~~~ ``A->B``\ という型も\ ``forall x:A, B``\ という型も、どちらも型\ ``A``\ から型\ ``B``\ への関数である、という点については同じです。この二つの唯一の違いは、後者の場合戻り値の型\ ``B``\ が引数\ ``x``\ を参照できるということです。たとえば、 - 関数\ ``fun x:nat => x + x``\ は型\ ``nat->nat``\ を持っていますが、このことは任意の数\ ``n``\ を別の数に対応させるもの、ということです。 - 対して、関数\ ``fun X : Type => nil (list X)``\ は\ ``forall X : Type, list (list X)``\ という型になります。これは、任意の集合\ ``X``\ を、\ ``X``\ 型のリストのリストに対応させるもの、ということになります。(もちろん、\ ``nil``\ は通常\ ``nil X``\ と書く代わりに\ ``[``] と書くのが普通ですが。) 実際、関数を記述するためのこれら二つの書き方はほぼ同じですが、 Coq では\ ``A->B``\ の書き方は、\ ``x``\ が\ ``B``\ の定義の中に変数として現れない限り、\ ``fun x:nat => x + x``\ のただの省略形と考えていいでしょう。例えば、好みならばこれを\ ``forall 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``\ についての帰納法で証明する。 - ``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``\ の導出による帰納法で証明する。 - ``Q``\ が\ ``c``\ であることを示した最後のルールを仮定して、 <...ここで\ ``a``\ の全ての型をコンストラクタの定義にある等式と共に示し、型\ ``Q``\ を持つ\ ``a``\ がIHであることをそれぞれ示す。>ならば <...ここで再び\ ``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``\ の結合則を証明するケースでは、 :: Theorem plus_assoc' : forall n m p : nat, n + (m + p) = (n + m) + p. Proof. ...最初に 3個の変数を全てコンテキストに導入しています。これはつまり"任意の\ ``n``,\ ``m``,\ ``p``\ について考える"という意味になっています... :: intros n m p. ...ここで、\ ``induction``\ タクティックを使い\ ``P n``\ (任意の\ ``n``\ について\ ``n + (m + p) = (n + m) + p``\ )を証明し、すぐに、コンテキストにある特定の\ ``n``\ についても証明します。 :: induction n as [| n']. Case "n = O". reflexivity. Case "n = S n'". ``induction``\ が作成した(帰納法の手順とも言うべき)二つ目のゴールでは、\ ``P n'``\ ならば任意の\ ``n'``\ で\ ``P (S n')``\ が成り立つことを証明する必要があります。 この時に\ ``induction``\ タクティックは\ ``P (S n')``\ をゴールにしたまま、自動的に\ ``n'``\ と\ ``P n'``\ をコンテキストに導入してくれます。 :: simpl. rewrite -> IHn'. reflexivity. Qed. ``induction``\ をゴールにある量化された変数に適用してもかまいません。 :: Theorem plus_comm' : forall n m : nat, n + m = m + n. Proof. induction n as [| n']. Case "n = O". intros m. rewrite -> plus_0_r. reflexivity. Case "n = S n'". intros m. simpl. rewrite -> IHn'. rewrite <- plus_n_Sm. reflexivity. Qed. ``induction n``\ が\ ``m``\ をゴールに残したままにしていることに注目してください。つまり、今証明しようとしている帰納的な性質は、\ ``forall m``\ で表されているということです。 もし\ ``induction``\ をゴールにおいて量化された変数に対して他の量化子の後に適用すると、\ ``induction``\ タクティックは自動的に変数をその量化子に基づいてコンテキストに導入します。 :: Theorem plus_comm'' : forall n m : nat, n + m = m + n. Proof. ここで\ ``n``\ の代わりに\ ``m``\ を induction しましょう。... :: induction m as [| m']. Case "m = O". simpl. rewrite -> plus_0_r. reflexivity. Case "m = S m'". simpl. rewrite <- IHm'. rewrite <- plus_n_Sm. reflexivity. Qed. 練習問題: ★, optional (plus\_explicit\_prop) '''''''''''''''''''''''''''''''''''''''''''' ``plus_assoc'``\ と\ ``plus_comm'``\ を、その証明とともに上の\ ``mult_0_r''``\ と同じスタイルになるよう書き直しなさい。このことは、それぞれの定理が帰納法で証明された命題に明確な定義を与え、この定義された命題から定理と証明を示しています。 :: (* FILL IN HERE *) ☐ 冒険心を満足させるために、もう少し脱線してみましょう。\ ``Definition``\ でパラメータ化された命題を定義できるなら、\ ``Fixpoint``\ でも定義できていいのではないでしょうか?もちろんできます!しかし、この種の「再帰的なパラメータ化」は、日常的に使われる数学の分野と必ずしも調和するわけではありません。そんなわけで次の練習問題は、例としてはいささか不自然かもしれません。 練習問題: ★★★★, optional (true\_upto\_n\_\_true\_everywhere) '''''''''''''''''''''''''''''''''''''''''''''''''''''''''''' ``true_upto_n_example``\ を満たすような再帰関数\ ``true_upto_n__true_everywhere``\ を定義しなさい。 :: Example true_upto_n_example : (true_upto_n__true_everywhere 3 (fun n => even n)) = (even 3 -> even 2 -> even 1 -> forall m : nat, even m). Proof. reflexivity. Qed. *) ☐ ``Prop``\ における帰納法の原理 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 最初のほうで、我々は帰納的に定義された「集合」に対して、Coqが生成する帰納法の原理をつぶさに見てきました。\ ``ev``\ のように、帰納的に定義された「命題」の帰納法の原理は、やや複雑でした。これらに共通して言えることですが、これらを\ ``ev``\ の証明に使おうとする際、帰納的な発想のもとで\ ``ev``\ が持ちうるものの中から使えそうな形になっているものを探します。それは\ ``0``\ が偶数であることの根拠であったり、ある\ ``n``\ について\ ``S (S n)``\ は偶数であるという根拠(もちろん、これには\ ``n``\ 自身が偶数であるということの根拠も含まれていなければなりませんが)だったりするでしょう。しかしながら直観的な言い方をすると、我々が証明したいものは根拠についての事柄ではなく、数値についての事柄です。つまり、我々は根拠をベースに数値の属性を証明できるような帰納法の原理を必要としているわけです。例えば、ずいぶん前にお話ししたように、\ ``ev``\ の帰納的な定義は、こんな感じで... :: Inductive ev : nat -> Prop := | ev_0 : ev O | ev_SS : forall n:nat, ev n -> ev (S (S n)). ... ここから生成される帰納法の原理はこんな風になります ... :: ev_ind_max : forall P : (forall n : nat, ev n -> Prop), P O ev_0 -> (forall (n : nat) (e : ev n), P n e -> P (S (S n)) (ev_SS n e)) -> forall (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``\ のもとでtrueであることが示される。 しかしこれは、私たちが求めたり必要としているものより少しだけ柔軟にできていて、偶数性の根拠の断片を属性として含むような論理的主張を証明する方法を与えてくれます。我々の興味の対象は「数値の属性が偶数である」ことの証明なのですから、その興味の対象も数値に関する主張であって、根拠に対するものではないはずです。これにより、単に\ ``n``\ だけでパラメータ化されていて、\ ``P``\ がすべての偶数\ ``n``\ で成り立つことを示せるような命題\ ``P``\ を証明する際に帰納法の原理を得ることがより楽になります。 :: forall P : nat -> Prop, ... -> forall n : nat, ev n -> P n このような理由で、Coqは実際には\ ``ev``\ のために次のような帰納法の原理を生成します。: :: Check ev_ind. Coqが根拠の式\ ``e``\ を、命題\ ``P``\ のパラメータから取り去っていることに注目してください。その結果として、仮定\ ``forall (n:nat) (e:ev n), ...``\ を [forall (n:nat), evn -> ...] に書き換えています。すなわち、我々はすでに\ ``ev n``\ から証明可能であることの明白な根拠を求められていないのです。 ``ev_ind``\ を自然言語で書き直すと、 - ``P``\ が自然数の属性である(つまり、\ ``P``\ が全ての\ ``n``\ についての命題である)と仮定し、\ ``P n``\ が偶数の場合常に成り立つことを示す。これは、以下を示すのに十分である。: - ``P``\ が\ ``0``\ において成り立つ。 - 全ての\ ``n``\ において、もし\ ``n``\ が偶数で\ ``P``\ が\ ``n``\ において成り立つなら、\ ``P``\ は\ ``S (S n)``\ においても成り立つ。 ``induction``\ とする代わりに\ ``ev_ind``\ を直接 apply することもできます。以下は、これと同じパターンです。 :: Theorem ev_even' : forall n, ev n -> even n. Proof. apply ev_ind. Case "ev_0". unfold even. reflexivity. Case "ev_SS". intros n' E' IHE'. unfold even. apply IHE'. Qed. 練習問題: ★★★, optional (prop\_ind) ''''''''''''''''''''''''''''''''''' 帰納的に定義された\ ``list``\ と\ ``MyProp``\ に対し、Coq がどのような帰納法の原理を生成するか、予想して書き出し、次の行を実行した結果と比較しなさい。 :: Check list_ind. Check MyProp_ind. ☐ 練習問題: ★★★, optional (ev\_MyProp') ''''''''''''''''''''''''''''''''''''' もう一度\ ``ev_MyProp``\ を証明しなさい。ただし、今度は\ ``induction``\ タクティックの代わりに\ ``apply MyProp_ind``\ を使いなさい。 :: Theorem ev_MyProp' : forall n:nat, MyProp n -> ev n. Proof. apply MyProp_ind. (* FILL IN HERE *) Admitted. ☐ 練習問題: ★★★★, optional (MyProp\_pfobj) '''''''''''''''''''''''''''''''''''''''' もう一度\ ``MyProp_ev``\ と\ ``ev_MyProp``\ を証明しなさい。ただし今度は、明確な証明オブジェクトを手作業で構築(上の\ ``ev_plus4``\ でやったように)することで証明しなさい。 :: (* FILL IN HERE *) ☐ :: Module P. 練習問題: ★★★, optional (p\_provability) '''''''''''''''''''''''''''''''''''''''' 次の、帰納的に定義された命題について考えてみてください。: :: Inductive p : (tree nat) -> nat -> Prop := | c1 : forall n, p (leaf _ n) 1 | c2 : forall t1 t2 n1 n2, p t1 n1 -> p t2 n2 -> p (node _ t1 t2) (n1 + n2) | c3 : forall t n, p t n -> p t (S n). *) FILL IN HERE これについて、どのような時に\ ``p t n``\ が証明可能であるか、その条件をを自然言語で説明しなさい。 (\* FILL IN HERE \*) ☐ :: End P. 追加練習問題 ------------ 練習問題: ★★★★ (palindromes) '''''''''''''''''''''''''''' palindrome(回文)は、最初から読んでも逆から読んでも同じになるようなシーケンスです。 - ``list X``\ でパラメータ化され、それが palindrome であることを示すような帰納的 命題\ ``pal``\ を定義しなさい。(ヒント:これには三つのケースが必要です。この定義は、リストの構造に基いたものとなるはずです。まず一つのコンストラクタ、 :: c : forall l, l = rev l -> pal l は明らかですが、これはあまりうまくいきません。) - 以下を証明しなさい。 :: forall l, pal (l ++ rev l). - 以下を証明しなさい。 :: forall l, pal l -> l = rev l. (\* FILL IN HERE \*) ☐ 練習問題: ★★★★★, optional (palindrome\_converse) '''''''''''''''''''''''''''''''''''''''''''''''' 一つ前の練習問題で定義した\ ``pal``\ を使って、これを証明しなさい。 :: forall l, l = rev l -> pal l. (* FILL IN HERE *) ☐ 練習問題: ★★★★ (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``\ のサブシーケンスである、というような関係であることを証明しなさい。(ヒント:何について帰納法を適用するか、よくよく注意して下さい。) (\* FILL IN HERE \*) ☐ 練習問題: ★★, 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 : forall (X Y : Set) (P : foo X Y -> Prop), (forall x : X, __________________________________) -> (forall y : Y, __________________________________) -> (________________________________________________) -> ________________________________________________ ☐ 練習問題: ★★, optional (bar\_ind\_principle) '''''''''''''''''''''''''''''''''''''''''''' 次に挙げた帰納法の原理について考えてみましょう: :: bar_ind : forall P : bar -> Prop, (forall n : nat, P (bar1 n)) -> (forall b : bar, P b -> P (bar2 b)) -> (forall (b : bool) (b0 : bar), P b0 -> P (bar3 b b0)) -> forall 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 : forall n, no_longer_than X [] n | nlt_cons : forall x l n, no_longer_than X l n -> no_longer_than X (x::l) (S n) | nlt_succ : forall l n, no_longer_than X l n -> no_longer_than X l (S n). この命題のために Coq が生成する帰納法の原理を完成させなさい。 :: no_longer_than_ind : forall (X : Set) (P : list X -> nat -> Prop), (forall n : nat, ____________________) -> (forall (x : X) (l : list X) (n : nat), no_longer_than X l n -> ____________________ -> _____________________________ -> (forall (l : list X) (n : nat), no_longer_than X l n -> ____________________ -> _____________________________ -> forall (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 : forall n l, R n l -> R (S n) (n :: l) | c3 : forall 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``] ☐