andとorとnot: ド・モルガン (2.1)
andとorとnotを分けて説明するのが面倒くさいので、いきなり全部入りの定理を例にしましょう。今回のお題はド・モルガンの法則です。
Lemma De_Morgan: forall A B: Prop, ~(A \/ B) -> (~A /\ ~B). Proof.
「(AまたはB)ではない、ならば、(Aではない、かつ、Bではない）」です。∨ が「または」で、∧ が「かつ」で、「~」が否定の「ではない」です。∨と∧はバックスラッシュを使って書くので、フォント環境によっては円記号に見えてしまっているかも。その場合はすみません、心眼で￥を＼と読んで下さい。
そういえば前回は Theorem Modus_ponens と "Theorem" (定理) で書き始めましたが、今回は "Lemma" (補題) です。Coq 的には違いは何もありません。趣味の問題です。"Proposition" (命題) や "Corollary" (系)、"Fact"、"Remark" など色々ありますが趣味で使い分けて下さい。
notの扱い
さて、まず、否定の ~A は、「A -> False」の省略形です。リファレンスから引用します。Coq.Init.Logic.not:
Definition not (A:Prop) := A -> False. Notation "~ x" := (not x) : type_scope.
「Aではない」とはすなわち、「Aならば偽」「Aだと仮定すると矛盾が生じる」である。これがCoqでの、そしてCoqがベースにしている論理体系での「~」の定義であります。False の定義はあとで解説しますが、とりあえず単にそういう名前の命題と思っておいて下さい。
「ならば」の扱いなら前回やって慣れてますので、安心ですね。「"not" なんて見慣れない単語を使わないで、全部 "->" の言葉でしゃべってください」と Coq さんに伝えましょう。
unfold not.
"unfold" tactic を使います。単に、Definition ... := で定義された定義をインライン展開するだけのtacticです。
ついでに intros. しておきました。
andの扱い
示さないといけないゴールの形が、(A→False)∧(B→False) になりました。この ∧ とは何者かというと… Coq.Init.Logic.and:
Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B where "A /\ B" := (and A B) : type_scope.
こんな物体です。なにやら複雑ですが、とりあえず最後の１行は「"A∧B" という中置演算みたいな記法は、(and A B) の略記です」と言ってるだけです。本体は上２行。"Inductive" 宣言を使って、二つのことを宣言しています。
- "A∧B" という新種の命題をこれから使います！
- この "A∧B" の「公理」は A -> B -> A∧B です！
"A∧B"が成り立つのは、Aが成り立って、しかもBが成り立っているとき、その時に限ります。つまり "Aならば(Bならば(A∧B))" が無条件で成立する…そういう∧という命題を使って色々書いたり証明したりするんでよろしくお願いします、とCoqさんに伝えるのがInductive宣言です。
さてさて、定義の話はいいから、証明のやり方はどうするのでしょうか。
実は、もう我々は証明のしかたを知っています。
公理はいつでも無条件に使えるので、仮定と同じように、apply することができて…
apply conj.
"(A->False) ∧ (B->False)" を示すためには、A->False を示して、B->False を示せば、後は conj を使えば証明できます。そういう感じで証明しますんでよろしく、とCoqさんに伝えると
二つのゴールができました。
orの扱い
続いて、一つ目のゴールは "A->False" です。ゴールが "->" の形なので、何も考えず
intros.
するとゴールが "False" になりますが、仮定を眺めると False を作れるのは "H: A∨B->False" しかないので、これをapplyしておきます。
apply H.
ゴールは "A∨B" になりました。さてどうしましょう。定義を見ると Coq.Init.Logic.or:
Inductive or (A B:Prop) : Prop := | or_introl : A -> A \/ B | or_intror : B -> A \/ B where "A \/ B" := (or A B) : type_scope.
今度は、公理が２つあります。
- or_introl: "A"が成り立つなら、"AまたはB"が成り立つ
- or_intror: "B"が成り立つなら、"AまたはB"が成り立つ
まあor(または)の意味として納得の行く定義です。
というわけで、ゴールを証明するには "apply or_introl." か "apply or_intror." を使えばよいのですが…どっちが正解でしょうか？
- ゴール A∨B に、or_introl: A->(A∨B) を apply すると、新ゴールは A になります
- ゴール A∨B に、or_intror: B->(A∨B) を apply すると、新ゴールは B になります
どっちなら続きを証明できるかというと、今回は仮定に "H0: A" があるので、新ゴール A なら"exact H0."で証明完了です。というわけで、or_introl の方を使います。
apply or_introl. exact H0.
こういう風に、or のような分岐があると「どっちに行ったら証明できるか」をよく考えて選んでやる必要があります。証明の完全な機械化は難しくて、Coqのように人間が考えて証明記述してやるシステムが必要な理由の一端は、ここにあります。頑張って人類の発想力を発揮しましょう。
apply conj でできたもう一つのゴール "B->False" も、同じように証明できます。こっちは or_intror の方を使います。
intros. apply H. apply or_intror. exact H0. Qed.
証明完了！
