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.
帰納的に定義された型に対する帰納法の原理¶
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
alln: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
allx``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.
追加練習問題¶
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 *)
☐
一つ前の練習問題で定義したpalを使って、これを証明しなさい。
forall l, l = rev l -> pal l.
(* FILL IN HERE *)
☐
あるリストが、別のリストのサブシーケンス（ 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 *)
☐
次のような、帰納的な定義をしたとします：
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, __________________________________) ->
(________________________________________________) ->
________________________________________________
☐
次に挙げた帰納法の原理について考えてみましょう：
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 : ________________________________________.
☐
次のような、帰納的に定義された命題が与えられたとします：
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 ->
____________________
☐
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]
☐