andとorとnot以外のInductive (2.5)

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

こんなの考えてみました。

Inductive major (A B C:Prop) : Prop :=
| ab : A->B->major A B C
| bc : B->C->major A B C
| ca : C->A->major A B C.

AとBとCのうち、2個以上が成り立つなら成り立つ、多数決命題 major A B C を定義しました。例えば、こんな定理が成り立ちます。

Theorem majmaj:
 forall A B C: Prop,
   major A B C -> ~major (~A) (~B) (~C).
Proof.

とりあえず unfold not. して、intros. して…あとは仮定に major ばっかりになるので、Inductive な命題が仮定にあるときは…？練習問題です(^^)。

他に重要な例としては、Anarchy Proof の問題でも時々でてきます（Prime is decidable など）が、{A}+{B} というのがあります。これの定義はCoq.Init.Specif.sumbool:

Inductive sumbool (A B:Prop) : Set :=
  | left : A -> {A} + {B}
  | right : B -> {A} + {B} 
 where "{ A } + { B }" := (sumbool A B) : type_scope.

コンストラクタの名前が違うだけで、ほとんど A∨B と同じです。実際、∨を{}+{}に変えた

Lemma De_Morgan3:
 forall A B: Prop,
  ({A}+{B}->False) -> ((A->False) /\ (B->False)).

でも

Lemma De_Morgan4:
 forall A B: Prop,
  ((A->False) /\ (B->False)) -> ({A}+{B}->False).

でも、全く同じに、"constructor" と "destruct" を使って証明できます。試してみて下さい。練習問題です(^^)。こんな風に、見たことのない新しい命題が現れても、どれもandやorと同じく、constructorとdestructで証明にとりかかれます。簡単ですね。

※ {A}+{B} に関しては、A∨B と唯一違うところは、∨の方は:Propと宣言されてましたが、{}+}{}の方は:Setと宣言されているところです。PropとSetの違いはそのうち多分説明するような気がしますが、とりあえず証明を考える際に問題となる違いは１点だけ。

この制約のせいで、"forall A B:Prop, {A}+{B} -> A\/ B" は証明できますが、"forall A B:Prop, A\/ B -> {A}+{B}" はできません。この形になってしまったときは、destructを使わずになんとか迂回して証明することになります。

ひとり勉強会