もう今回の内容でInductiveの扱いは完璧…！といいたいところなんですが、「再帰的なInductive」の証明テクニックの解説が実はまだ残っています。次は多分それについて書きたいなあと思っています。それかFalse周りの証明をさらにいろいろ。

何度か繰り返しているように、andやorやFalseは、Coqに組み込みの摩訶不思議な何かではなく、ユーザー定義できる命題です。andやorに使える証明方法は、他のInductive命題にもそのまま使えます。試しに他に何か自作してみましょう。こんなの考えてみました。…

「コンストラクタがあるならデストラクタはないんですか」あるのです。これを語らなくては話が終わりません。コンストラクタの逆の話なので、例題も逆にしましょう。ド・モルガンの法則は逆向きにも成り立ちます。 Lemma De_Morgan2: forall A B: Prop, (~A …

ここまでの内容をまとめると、 ゴールが A∧B の形なら ∧の公理(コンストラクタ)を使う つまり apply conj. ゴールが A∨B の形なら ∨の公理(コンストラクタ)を使う つまり apply or_introl. または apply or_intror. どっちがいいかは人間が頑張って考える。 …

「プログラミング言語としてみると」さっきの証明は何をやっていたことになるんでしょう。"Inductive"は、ユーザー定義の新しい命題を定義するのでした。そして、命題＝型です。つまり、ユーザー定義の新しい型を作る機能が対応します。Haskell だと "data" …

andとorとnotを分けて説明するのが面倒くさいので、いきなり全部入りの定理を例にしましょう。今回のお題はド・モルガンの法則です。 Lemma De_Morgan: forall A B: Prop, ~(A \/ B) -> (~A /\ ~B). Proof.「(AまたはB)ではない、ならば、(Aではない、かつ、…

第２回です。前回は「forall」と「->」の扱い方でした。今回は、「ならば (->)」以外の定番の論理演算、「and」「or」「not」のお話です。実は、Coq の本当に言語組み込みの命題構成子は forall と -> だけで、「and」「or」「not」は、Coq使いなら自分で同…