Coqにあらかじめ組み込まれた論理は極めて小さく、帰納的定義(Inductive)、 全称量化(∀)、含意(→)だけがプリミティブです。しかしそれ以外の論理結合子 （かつ、または、否定、存在量化子、等号など）も、組み込みのものを用いて定義できます。

全称量化 と 含意

実は、→ と ∀ は 同じものです! Coqの → 記法は ∀ の 短縮記法に過ぎません。仮定に名前をつけることができることから、 ∀記法の方が一般的です。

例えば次の命題を考えてみましょう。

もしもこの命題に含まれる証明項があったら、その項は二つの引数 （一つは、数字n、もう一つはnが偶数であることの根拠E）を持つ 関数になっているはずです。 しかし根拠となるEはfunny_prop1の中では使われていませんから、これに わざわざ E という名前をつけることはちょっと馬鹿げています。 このような場合は、次のように書くこともできます。

また、より親しみ深い記法では次のようにも書けます。

これはつまり "P → Q" は単に "∀ (_:P), Q" の糖衣構文に過ぎないと いうことを示しています。

論理積、連言（Conjunction、AND）

命題 P と Q の論理積（ logical conjunction ）は、コンストラクタを 一つしか持たない Inductive を使った定義で表せます。

注意してほしいのは、前の章で取り上げた関数 ev の定義と同様に、 この定義もパラメータ化された命題になっていることです。ただしこの場合はパラメータ 自身も数値ではなく命題です。

この定義の内容を直感的に理解するのに、そうややこしく考える必要はありません。 and P Q に根拠を与えるには、P の根拠と Q の根拠が必要 だということです。もっと精確に言えば、

• もし p が P の根拠で、q が Q の根拠であるなら、conj p q を and P Q の根拠とすることができる。
  
  
• これは and P Q に根拠を与える唯一の方法であること、 即ち、もし and P Q の根拠が与えられたならば、 その根拠が conj p q の形をしており、さらに p が P の根拠であることと q が Q の根拠であることがわかるということです。

今後論理積をよく使うことになるので、 もっと馴染みのある、中置記法を導入することにしましょう。

（type_scope という注釈は、この記法が値にではなく、 命題に現れるものであることを、Coqに伝えています。）

コンストラクタ conj の型はどのようなものか考えてみましょう。

conjが四つの引数（ P 、Q という命題と、P 、Q の根拠）をとることに注目して下さい。

基本的なことから色々なことを組み立てていくエレガントさはさておき、 このような方法でconjunctionを定義することの利点は、これを含む 文を、既に知っているタクティックで証明できることです。 例えば、もしゴールが論理積を含んでいる場合、このたった一つの コンストラクタconjを適用するだけで証明できます。 それは、conjの型を見ても分かるように現在のゴールを解決してから conjunctionの二つの部分を別々に証明するべきサブゴールにします。

上の定理の証明オブジェクトをよく観察してみてください。

この型に注目してください。
    conj (ev 0) (ev 4) (... ev 0 の証明 ...) (... ev 4 の証明 ...)

さっき見た conj と同じ形をしているのが分かるでしょう。

apply conj とするかわりに split タクティックでも同じことができます。

逆に、inversion タクティックを、コンテキストにある論理積の形を した仮定に使うことで、それの構築に使われた根拠を取り出し、 コンテキストに加えることができます。

練習問題: ★, optional (proj2)

☐

この定理の証明を理解しやすくするため、再び Case タクティックに ついて話します。 この証明で起こっていることをよく観察すると、 P and Q の根拠となっている命題を抽出して、そこから逆向きに証明を 再構築していることが分かるでしょう。

練習問題: ★★ (and_assoc)

次の証明では、inversionが、入れ子構造になった命題H : P ∧ (Q ∧ R)を どのようにHP: P, HQ : Q, HR : R に分解するか、という点に注意しなが がら証明を完成させなさい。

☐

練習問題: ★★, recommended (even_ev)

今度は、前の章で棚上げしていた even と ev の等価性をが別の方向から 証明してみましょう。 ここで左側のandは我々が実際に注目すべきものです。右のandは帰納法の仮定と なって帰納法による証明に結びついていくことになるでしょう。なぜこれが必要と なるかは、左側のandをそれ自身で証明しようとして、行き詰まってみると かるでしょう。

☐

練習問題: ★★

次の命題の証明を示すオブジェクトを作成しなさい。

☐

Iff （両含意）

この、"if and only if（～である時、その時に限り）" で表される 「両含意」という論理は馴染みのあるもので、次の二つの 「ならば（含意）」をandでつないだものです。

練習問題: ★ (iff_properties)

上の、 ↔ が対称であることを示す証明 (iff_sym) を使い、それが反射的で あること、推移的であることを証明しなさい。

ヒント: もしコンテキストに iff を含む仮定があれば、 inversion を使ってそれを二つの含意の式に分割することができます。 (なぜそうできるのか考えてみましょう。)

☐

練習問題: ★★ (MyProp_iff_ev)

ここまで、MyProp や ev が これらの命題がある種の数値を特徴づける（偶数、などの） ことを見てきました。 次の MyProp n ↔ ev n が任意の nで成り立つことを証明しなさい。 お遊びのつもりでかまわないので、その証明を、単純明快な証明、タクティックを 使わないにような証明に書き換えてください。（ヒント：以前に使用した定理をうまく 使えば、１行だけでかけるはずです！）

☐

Coqのいくつかのタクティックは、証明の際に低レベルな操作を避けるため iff を特別扱いします。 特に rewrite を iff に使うと、 単なる等式以上のものとして扱ってくれます。

論理和、選言（Disjunction、OR）

論理和（Disjunction、OR）も、帰納的な命題として定義できます。

コンストラクタ or_introl の型が何か考えてください。

このコンストラクタは三つの入力（ P、Q と名付けられた 命題に加え、P の根拠）を引数にとり、P ∧ Q の根拠を返します。 次に、or_intror の型を見てみましょう。

ほとんど or_introl と同じように見えますが、P ではなく Q の 根拠が要求されています。

直観的には、命題 P ∨ Q に根拠を与える方法は二つあることがわかります。

• P の根拠を与える。（そしてそれが P の根拠であることを伝える。

これがコンストラクタ or_introl の機能です）か、

• Q の根拠をコンストラクタ or_intror に与える。

P ∨ Q は二つのコンストラクタを持っているので、 P ∨ Q の形の仮定に inversion を適用すると二つのサブゴールが生成されます。

次のように、apply or_introl 、 apply or_intror の代わりに left 、 right という短縮版のタクティックを使うこともできます。

練習問題: ★★ optional (or_commut'')

or_commut の証明オブジェクトがどのようになるか、書き出してみて ください。（ただし、定義済みの証明オブジェクトを Print を使って 見てみたりしないこと。）

☐

練習問題: ★★, recommended (or_distributes_over_and_2)

☐

練習問題: ★ (or_distributes_over_and)

☐

∧ 、 ∨ のandb 、orb への関連付け

我々はすでに、Coqの計算における型(Type) と論理の命題 (Prop) との 類似性について見てきました。ここではもう一つ、bool 型を扱う andb と orb が、∧ と ∨ とのつながりともいうべきある種の類似性を 持っていることに触れましょう。 この類似性は、次の定理を見ればもっとはっきりします。これは、 andb や orb が、ある入力に対する振る舞いを、その入力に対する命題に どのように変換するかを示したものです。

練習問題: ★ (bool_prop)

☐

偽であるということ

論理学でいうところの「偽」は、Coqでは「帰納的に定義されてはいるが コンストラクタを一つも持たない命題」として定義されています。

直観的な理解: False は、根拠を示す方法を一つも持たない命題

練習問題: ★ (False_ind_principle)

「偽」に関する帰納的な公理を何か思いつくことができますか？

☐

False にはコンストラクタがないので、False の意味するところのものを 反転（invert）してもサブゴールが生成されません。このことはつまり、 「偽」からはどんなゴールも証明できる、ということです。

これはどういうことでしょうか？ inversion タクティックは仮定 contra を その取りうるケースに分解し、それぞれにサブゴールを生成します。ここで contra が False の根拠となっているため、そこから取りうるケースは 存在しません。このため、証明に値するサブゴールがなくなり、そこで 証明が終わってしまうのです。

逆に、False を証明する唯一の方法は、コンテキストに何か 矛盾がないかを探すことです。

実際、 False_implies_nonsense の証明は、特定の意味を持つ証明すべきこと を何も持っていないので、任意の P に対して簡単に一般化できます。

ラテン語の 「ex falso quodlibet 」は、文字通り「偽からはあなたの 望むものすべてがもたらされる」というような意味です。この定理は、 「 principle of explosion 」としても知られています。

真であるということ

Coqで「偽」を定義することができたので、同じ考え方で「真」を定義することが できるか、ということが次の関心事になります。もちろん、その答えは「Yes」です。

練習問題: ★★ (True_induction)

True を、帰納的な命題として定義しなさい。あなたの定義に対してCoqはどのような 帰納的原理を生成してくれるでしょうか。 （直観的には True はただ当たり前のように 根拠を示される命題であるべきです。代わりに、帰納的原理から帰納的な定義を逆に たどっていくほうが近道だと気づくかもしれません。）

☐

しかしながら、False とは違い、広い意味で解釈すると True には 理論的な意味で奇妙なところがあります。ゴールの証明に使うには当たり前すぎ （それゆえつまらない）、仮定として有意義な情報を与えてくれないのです。

否定

命題 P の論理的な補集合というべきものは、 not P もしくは短縮形として ~P と表されます。

直観的には 「もしP がtrueでないなら、すべてが（ False でさえ）仮定 P から導かれるということです。.

Coqで否定を扱えるようになるにはある程度慣れが必要です。 たとえ何かがどう見ても真に思える場合でも、そのことをCoqに納得させるのは 最初のうちはなかなか大変です。ウォームアップのつもりで、否定のに関する 馴染みのある定理を取り上げてみましょう。

練習問題: ★★, recommended (double_neg_inf)

double_neg の非形式的な証明を書きなさい。:

Theorem: P implies ~~P, for any proposition P.

Proof: ☐

練習問題: ★★, recommended (contrapositive)

☐

練習問題: ★ (not_both_true_and_false)

☐

練習問題: ★ ev_not_ev_S

定理 five_not_even は、「５は偶数ではない」というようなとても当たり前の 事実を確認するものです。今度はもう少し面白い例です。

☐

練習問題: ★ (informal_not_PNP)

命題 ∀ P : Prop, ~(P ∧ ~P) の形式的でない証明を（英語で）書きなさい。

☐

このうちいくつかは、古典論理ではtrueと判断できるにもかかわらず、Coqに組み込まれた機能だけでは 証明できないものがあるので注意が必要です。

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

さらなる挑戦を求める人のために、 Coq'Art book (p. 123) から一つ練習問題を 取り上げてみます。次の五つの文は、よく「古典論理の特性」と考えられている もの（Coqにビルトインされている構成的論理の対極にあるもの）です。 これらをCoqで証明することはできませんが、古典論理を使うことが必要なら、 矛盾なく「証明されていない公理」として道具に加えることができます。 これら五つの命題が等価であることを証明しなさい。

☐

不等であるということ

x <> y というのは、~(x = y) と同じことです。

不等性は、その中に「否定」を含んでいるため、やはりその扱いには ある程度の慣れが必要です。ここで一つ有用なトリックをお見せしましょう。 もし、証明すべきゴールがあり得ない式（例えばfalse = trueというような文） であった場合は、ex_falso_quodlibet という補題をapplyで適用すると、ゴールを Falseにすることができます。このことを覚えておけば、コンテキストの中の ~P という形の仮定を使うことがとても簡単になります。特に、x<>y という形の仮定の 場合はに有用です。

練習問題: ★★, recommended (not_eq_beq_false)

☐

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

☐

存在量化子

もう一つの論理的接続詞は、存在量化子（ existential quantification ）です。これは、次のような定義でその意味を とらえることができます。

この ex は、型引数 X とそれに関する属性 P によって決まる命題です。 「 P を満たす x が存在する」という主張に根拠を与えるため、 ある特定の値 x （「証拠」と呼ぶことにします）を具体的に示すことで P x の根拠を得ることができます。つまりこれは、 x が性質 P を 持っていることの根拠です。

例として、このような存在量化子を持つ命題を見てみましょう。:

この、命題を証明するためには、証拠として特定の値（この場合4）を 与え、それが偶数である根拠を示す必要があります。

Coqの容易な表記法の定義は、存在量化された命題を記述するための、より 馴染みやすい表記を、ビルトインされたを全称量化子と同レベルで実現しています。 そのおかげで、「偶数となる自然数が存在する」ことを示す命題を ex nat ev と 書く代わりに、たとえば ∃ x:nat, ev x のように書くことができます。 （これを理解するためにCoqの「表記法」がどのように作用しているかを完全に 理解しないといけない、ということではありません。）

存在を示す必要がある場合には、だいたいいつも同じようなタクティックの 組み合わせが使われます。例えば、ある値の存在を証明する場合には、その値を コンストラクタ ex_intro に apply すればいいのです。ex_intro の前提 はその結論に現れないうような変数（これが「証拠」となります）を必要とするため、 apply を使用する際にはその値をきちんと提示することが必要になります。

もう一度書きますが、ここでは具体的な値を証拠として用意する必要があります。

apply ex_intro with (witness:=e) と書く代わりに、短縮形として ∃ e と記述することもできます。どちらも同じ意味です。

逆に、コンテキストに置かれた仮定の中に存在を示すものがある場合は、 それを inversion タクティックで取り除くことができます。 変数に名前を付けるため as... パターンを使っていることに注目 してください。Coqはそれを「証拠」につける名前とし、仮定が証拠を保持する 根拠をそこから得ます。 （名前をきちんと選ばないと、Coqはそれを単なる 証拠としか考えることができず、その先の証明で混乱してしまいます。）

練習問題: ★ (english_exists)

英語では、以下の命題は何を意味しているでしょうか？
      ex nat (fun n => ev (S n))

次の証明オブジェクトの定義を完成させなさい

☐

練習問題: ★ (dist_not_exists)

"全ての x についてP が成り立つ" ということと " P を満たさない x は 存在しない" ということが等価であることを証明しなさい。

☐

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

一方、古典論理の「排中律（law of the excluded middle）」が必要とされる 場合もあります。

☐

練習問題: ★★ (dist_exists_or)

存在量化子が論理和において分配法則を満たすことを証明しなさい。

☐

等しいということ（同値性）

Coqには、等価という関係すら組み込まれていませんから、次のように帰納的に定義 してやります（ここではこれまで散々使った標準ライブラリでの定義と衝突すること を防ぐために、モジュールの中で定義することにします。）

次に定義するのは、標準的な中置記法です（Coqの型引数合成を使用しています）。

この例は少し難解かもしれません。これがどういうものかを考えると、 集合 X が与えられると、「集合 X に属する値 (x and y) にインデックス された、x は y に等しい」というような命題の _集団_ を定義してくれる ということです。この集団に属する命題に根拠を与えるためには、一つの 方法しかありません。それは、コンストラクタ refl_equal に型 X とその値 x : X を適用し、x が x と等しいという根拠を生成することです。

次の定義は少し違った形になっています。 -- Coqの標準ライブラリでは こちらの定義が採用されています。

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

これら二つの定義が等価であることを確認しなさい。

☐

二つ目の定義の優れたところは、Coqが生成する帰納法の原理が正確に 「ライプニッツの同値関係（ Leibniz equality ）」と親和している点です。 それはつまり、「x と y が等しいということは、 任意の命題 P が x でtrueとなるならば y でもtrueとなる」ということです。

一つ大事なことが残っています。確かに refl_equal は 2 = 2 というような 証明に根拠を与えることに使えます。 1 + 1 = 2 はどうでしょうか？ 答えは Yes です。実際、これらは証明としてはほとんど同じようなものだと 言えます。 その理由は Coq が二つの式がシンプルな計算ルールによって交換可能である ことをを示し、それを"同値である"として処理しているからです。 このルールは Eval simpl と同じものです。ただしこれには、 関数適用の評価、定義のインライン化、match の簡約が含まれています。

タクティックを使った同値性の証明では、 simpl を使うことで暗黙的にこの 交換ルールに触れています（reflexivity のような他のタクティックでも、明示的に、 もしくは暗黙的に含まれています）。このことは、次のような明示的な証明オブジェクトで 確認することができます。

Inversion 再び

これまでにも inversion が等値性にからむ仮定や帰納的に定義された命題に対して 使われるところを見てきました。今度もやることは変わりませんが、もう少し近くまで 寄って inversion の振る舞いを観察してみましょう。

一般的に inversion タクティックは、

• 帰納的に定義された型 P の命題 H をとる。
  
  
• その型 P の定義にある各コンストラクタ C が、
  
  
  • H が C から成っていると仮定するような新しいサブゴールを作る。
    
    
  • C の引数（前提）を、追加の仮定としてサブゴールのコンテキストに加える。
    
    
  • C の結論（戻り値の型）を現在のゴールとmatchして、 C を適用できるような一連の等式算出する。
    
    
  • そしてこれらの等式をサブゴールのコンテキストに加えてから、
    
    
  • もしこの等式が充足可能でない場合（S n = O というような式を含むなど）は、 即座にサブゴールを解決する。

例 : or で構築された仮定を反転（ invert ）すると、or に二つのコンストラクタが あるため二つのサブゴールが生成されます。コンストラクタ (P ∨ Q) の結果 （戻り値の型）は P や Q の形からくる制約を付けません。そのため追加の等式が サブゴールのコンテキストに加えられることはありません。

例 : and で構築された仮定を反転（ invert ）すると、and にはコンストラクタが 一つしかないため、サブゴールも一つしか生成されません。やはり、コンストラクタ (P ∧ Q) の結果（戻り値の型）は P や Q の形からくる制約を付けず、追加の等式が サブゴールのコンテキストに加えられることはありません。このコンストラクタは引数を二つ とりますが、それらはサブゴールのコンテキストに現れます。

例 : eq で構築された仮定を反転（ invert ）すると、これにもやはりコンストラクタが 一つしかないため、サブゴールも一つしか生成されません。しかしこの場合 コンストラクタ refl_equal の形は我々にもう少し情報を与えてくれます。 それは、eq の二つの引数は同じでなければならないという点です。 inversion タクティックはこの事実をコンテキストに加えてくれます。

命題としての関係

ev のように数値でパラメータ化された命題は、属性（ property ）と 見なすこともできます。つまり、それに属する値についてその命題が証明可能である ような nat の部分集合の定義と見ることができるということです。 同様に、引数（パラメータ）を二つ持つ命題は、その二つの「関係」を表していると 考えられます。つまり、その命題について証明可能な値のペアの集合の定義、 というわけです。

これまでにもすでに、帰納的に定義された関係の基本的なものは出てきていました。 等値性がそれです。他にも、よく使われるものとして「等しいかまたは小さい」 という関係があります。

この定義はかなり直観的なものになります。これは、ある数値がもう一つの 数値より小さいかまたは等しい、ということを示すには二つの方法があることを 示しています。一つはそれらが同じ数であるかどうかを確認すること。もう 一つは最初の数が。二つ目の数の一つ前の数より小さいかまたは等しい、 ということの根拠を得ることです。

これはこれで <= という関係の妥当なな定義だと言えます。しかし少し観察してみると 定義の左側のに現れる n は全て同じだということがわかります。ということは、 個々のコンストラクタにではなく定義全体に全称量化子を使うことが できるということです。このことは先程 eq という関係の二番目の定義でやったことと 同じです。

少し対称性が損なわれたようにも見えますが、この二番目の定義の方がいいのです。 なぜでしょうか？それは、こちらのほうがよりシンプルな帰納法の原理を 生成してくれるからです（ eq の二番目の定義にも同じことが言えます）。

一方、最初の定義に Coq が生成する帰納法の原理には、もっと多くの量化子が 含まれることになります。これでは、帰納法を使った証明がごちゃごちゃしてしまいます。 これが le の最初の定義で生成された帰納法の原理です。

コンストラクタ le_n と le_S を使った <= にからむ証明は、前章の eq が そうであったように、属性についての証明のいくつかのパターンに倣っています。 <= の形をしたゴール（例えば 3<=3 や 3<=6 など）に、そのコンストラクタを apply することができますし、inversion のようなタクティックを使って （~(2 <= 1) の証明をしようとする際のように） コンテキストに <= を含む 仮定から情報を抽出することもできます。

ここで、定義が正しくなされているのかのチェックをしてみましょう。（注意して 欲しいのは、ここでやることが、最初のレクチャーで書いてもらった、ある種の シンプルな「ユニットテスト」のようなものですが、今回のものは以前のものと ちょっと違います。今回のものには、simpl や reflexivity はほとんど 役に立ちません。簡約だけで証明できるようなものではないからです。

「より小さい」という関係（ n < m ）は、le を使って定義できます。

他にも、数値の関係についていくつか見てみましょう。

練習問題: ★★, recommended (total_relation)

二つの自然数のペア同士の間に成り立つ帰納的な関係 total_relation を 定義しなさい。

☐

練習問題: ★★ (empty_relation)

自然数の間では決して成り立たない関係 empty_relation を帰納的に 定義しなさい。

☐

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

次は三つや四つの値の間に成り立つ関係を同じように定義してみましょう。 例えば、次のような数値の三項関係が考えられます。

• 次の命題のうち、この関係を満たすと証明できると言えるのはどれでしょうか。
  • R 1 1 2
  • R 2 2 6
    
    
• この関係 R の定義からコンストラクタ c5 を取り除くと、証明可能な命題の範囲はどのように変わるでしょうか？端的に（１文で）説明しなさい。
  
  
• この関係 R の定義からコンストラクタ c4 を取り除くと、証明可能な命題の範囲はどのように変わるでしょうか？端的に（１文で）説明しなさい。

☐

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

関係 R の、等値性に関する特性をあげ、それを証明しなさい。 それは、 もし R m n o が true なら m についてどんなことが言えるでしょうか？ n や o についてはどうでしょうか？その逆は？

☐

練習問題: ★★★, recommended (all_forallb)

リストに関する属性 all を定義しなさい。それは、型 X と属性 P : X → Prop をパラメータとし、 all X P l が「リスト l の全ての要素が 属性 P} を満たす」とするものです。

Poly.v の練習問題 forall_exists_challenge に出てきた関数 forallb を思い出してみましょう。

属性 all を使って関数 forallb の仕様を書き、それを満たすことを証明 しなさい。できるだけその仕様が厳格になるようにすること。

関数 forallb の重要な性質が、あなたの仕様から洩れている、ということは ありませんか？

☐

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

Coq の主な目的の一つは、プログラムが特定の仕様を満たしていることを 証明することです。それがどういうことか、filter 関数の定義が仕様を満たすか証明 してみましょう。まず、その関数の仕様を非形式的に書き出してみます。

集合 X と関数 test: X→bool、リストl とその型 list X を想定する。 さらに、l が二つのリスト l1 と l2 が順序を維持したままマージされたもので、 リスト l1 の要素はすべて test を満たし、 l2 の要素はすべて満たさないと すると、filter test l = l1 が成り立つ。

リスト l が l1 と l2 を順序を維持したままマージしたものである、とは、 それが l1 と l2 の要素をすべて含んでいて、しかも 互いに入り組んではいても l1 、 l2 の要素が同じ順序になっている、ということです。例えば、


    [1,4,6,2,3]

は、以下の二つを順序を維持したままマージしたものです。
    [1,6,2]

と、
    [4,3]

課題は、この仕様をCoq の定理の形に書き直し、それを証明することです。 （ヒント：まず、一つのりすとが二つのリストをマージしたものとなっている、 ということを示す定義を書く必要がありますが、これは帰納的な関係であって、 Fixpoint で書くようなものではありません。）

☐

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

filter の振る舞いに関する特性を別の切り口で表すとこうなります。 「test の結果が true なる要素だけでできた、リスト l の すべての部分リストの中で、filter test l が最も長いリストである。」 これを形式的に記述し、それを証明しなさい。

☐

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

次の、帰納的に定義された命題は、

値 a がリスト l の要素として少なくとも一度は現れるということを 言うための、精確な方法を与えてくれます。

次の二つはappears_in に関するウォームアップ問題です。

では、 appears_in を使って命題 disjoint X l1 l2 を定義してください。 これは、型 X の二つのリスト l1 、 l2 が共通の要素を持たない場合 にのみ証明可能な命題です。

次は、 appears_in を使って帰納的な命題 no_repeats X l を定義して ください。これは, 型 X のリスト l の中のどの要素も、他の要素と 異なっている場合のみ証明できるような命題です。例えば、 no_repeats nat [1,2,3,4] や no_repeats bool [] は証明可能ですが、 no_repeats nat [1,2,1] や no_repeats bool [true,true] は証明 できないようなものです。

最後に、disjoint、 no_repeats、 ++ （リストの結合）の三つを使った、 何か面白い定理を考えて、それを証明してください。

☐

少し脱線: <= と < についてのさらなる事実

ここで少し新しいことを中断して、 <= や < といった関係についての 事実をいくつか書き溜めていくことにしましょう。それらはここから先に進む際に 必要になってくるばかりでなく、その証明自体がとてもよい練習問題に なってくれます。

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

☐

練習問題: ★★★, recommended (nostutter)

述語の帰納的な定義を定式化できるようになるというのは、これから先の学習に 必要なスキルになってきます。

この練習問題は、何の力も借りず自力で解いてください。 もし誰かの力を借りてしまった場合は、そのことをコメントに書いておいて ください。

同じ数値が連続して現れるリストを "stutters" （どもったリスト）と 呼ぶことにします。述語 "nostutter mylist" は、 mylist が「どもった リスト」でないことを意味しています。nostutter の帰納的な定義を記述しなさい。 （これは以前の練習問題に出てきた no_repeats という述語とは異なるものです。 リスト 1,4,1 は repeats ではありますが stutter ではありません。）

できた定義が、以下のテストを通過することを確認してください。 通過できないものがあったら、定義を修正してもかまいません。 あなたの書いた定義が、正しくはあるけれど私の用意した模範解答と異なって いるかもしれません。その場合、このテストを通過するために別の 証明を用意する必要があります。

以下の Example にコメントとして提示された証明には、色々な種類の nostutter の定義に対応できるようにするため、まだ説明していない タクティックがいくつか使用されています。 まずこれらのコメントをはずしただけの 状態で確認できればいいのですが、もしそうしたいなら、これらの証明をもっと 基本的なタクティックで書き換えて証明してもかまいません。

☐

練習問題: ★★★★, optional (pigeonhole principle)

「鳩の巣定理（ "pigeonhole principle" ）」は、「数えるあげる」という ことについての基本的な事実を提示しています。「もし n 個の鳩の巣に n 個より多い数のものを入れようとするなら、どのような入れ方をしても いくつかの鳩の巣には必ず一つ以上のものが入ることになる。」というもので、 この、数値に関する見るからに自明な事実を証明するにも、なかなか自明とは言えない 手段が必要になります。我々は既にそれを知っているのですが...

まず、補題を二つほど証明しておきます。（既に数値のリストについては 証明済みのものですが、任意のリストについてはのものはまだないので）

そして、述語 repeats の定義をします（以前の練習問題 no_repeats に 類似したものです）。それは repeats X l が、「 l の中に少なくとも一組の 同じ要素（型 X の）を含む」という主張となるようなものです。

この「鳩の巣定理」を定式化する方法を一つ挙げておきましょう。 リスト l2 が鳩の巣に貼られたラベルの一覧を、リスト l1 はそのラベルの、 アイテムへの割り当ての一覧を表しているとします。もしラベルよりも沢山の アイテムがあったならば、少なくとも二つのアイテムに同じラベルが貼られている ことになります。おそらくこの証明には「排中律（ excluded_middle ）」が 必要になるでしょう。

☐

選択課題

∧ や ∨ のための帰納法の原理

論理積（連言）や論理和（連言）に関する帰納法の原理は、帰納的に定義された 命題に対して簡約された帰納法の原理を Coq が生成する方法をとてもよく示しています。 これについては最後の章でお話しします。とりあえずこれに挑戦してみてください。

練習問題: ★ (and_ind_principle)

連言（ conjunction ）についての帰納法の原理を予想して、確認しなさい。

☐

練習問題: ★ (or_ind_principle)

選言（ disjunction ）についての帰納法の原理を予想して、確認しなさい。

☐

命題 and P Q の帰納的な定義から、
     Inductive and (P Q : Prop) : Prop :=
       conj : P → Q → (and P Q).

我々は Coq がこのような帰納法の原理を生成することを期待します。
     and_ind_max :
       ∀ (P Q : Prop) (P0 : P ∧ Q → Prop),
            (∀ (a : P) (b : Q), P0 (conj P Q a b)) →
            ∀ a : P ∧ Q, P0 a

しかし実際には、もっとシンプルで使いやすいものが生成されます。
     and_ind :
       ∀ P Q P0 : Prop,
            (P → Q → P0) →
            P ∧ Q → P0

同様に、 or P Q の帰納的な定義が与えられると、
     Inductive or (P Q : Prop) : Prop :=
       | or_introl : P → or P Q
       | or_intror : Q → or P Q.

以下のような、原則通りの帰納法の原理を制する代わりに、
     or_ind_max :
       ∀ (P Q : Prop) (P0 : P ∨ Q → Prop),
            (∀ a : P, P0 (or_introl P Q a)) →
            (∀ b : Q, P0 (or_intror P Q b)) →
            ∀ o : P ∨ Q, P0 o

Coq はこのような帰納法の原理が生成されます。
     or_ind :
       ∀ P Q P0 : Prop,
            (P → P0) →
            (Q → P0) →
            P ∨ Q → P0

帰納法のための明白な証明オブジェクト

タクティックを使った証明は一般に簡単に済むことが多いですが、証明式を 直接書いてしまえるなら、そうしたほうが簡単な場合もあります。特に、 Coq にちょっとだけ変わった方法をとらせたい時はそうです。

nat の帰納的な定義からCoqが自動的に生成した自然数に関する帰納法の 原理を思い出してください。

===> nat_ind : forall P : nat -> Prop, P 0nat) (f0 : forall n : nat, P n -> P (S n)) => fix F (n : nat) : P n := match n as n0 return (P n0) with | 0nat) (f0 : forall n : nat, P n -> P (S n)) => fix F (n : nat) : P n := match n as n0 return (P n0) with | 0