coqで一階述語論理版のド・モルガンの法則の証明を行うために、必要となる知識と情報をまとめた。

この記事は、「coqでド・モルガンの法則の証明をするまで (命題論理版) 」の続きとなっている。
coqの導入方法、使い方、命題論理の証明手順、および、命題論理でのド・モルガンの定理とその証明全体については、上記のリンク先に記載している。

述語論理について

述語論理の「述語(Predicate」とは、パラメータを持った命題のことである。
Coqの構文では、とあるA: Type(もしくはA: Set)をパラメータとした、P: A->Propが述語に当たる。
述語は、Aに属する値a: Aを一つ受け取ることで、命題P a: Propとなる。
一階述語論理は、変数を述語のパラメータとしてのみ使用することに制限した論理である。

述語としては、より具体的な型を引数にとり、具体的な判定を備えた具体的な関数の場合もありうる。
しかし、命題論理の命題の名前自体に意味がなく、どのような命題であっても成立する論理を扱うように、述語論理もまた任意の述語に対して、成立する論理を扱うことが基本である。

述語はそれ単体では命題とならないので、論理式にするにはパラメータを指定する必要がある。
述語論理では、この述語に与えるパラメータを用意する手段として、∀(forall)と∃(exists)の二種類の束縛がある。

∀a: A, 〜 => 「〜は、任意のAの要素aについて成立する」
∃a: A, 〜 => 「〜は、特定のAの要素aについては成立する」

この∀と∃を混ぜ込んだ論理式が、述語論理となる。

「述語＋パラメータ」を命題とみなした場合、パラメータa0 a1 a2 ...: Aに対して、各述語Pごとにそれぞれ命題(P a0) (P a1) (P a2) ...: Propが存在するものとみなせる。
この視点での変数束縛は、命題への/\や\/をパラメータ全体に対して適用したものとみなせる。つまり:

∀ a: A, P a => True /\ (P a0) /\ (P a1) /\ (P a2) /\ ...
∃ a: A, P a => False \/ (P a0) \/ (P a1) \/ (P a2) \/ ...

という解釈が可能である。
むしろ∀や∃は、~以降をandやorの列挙に展開されるイメージ認識するつほうが、そ直感的なの意味を間違わないだろう。(特に、∃の解釈で)

そして、推論規則や証明においても、この**forall <=> `/\`および`exists` <=> \/に類似性がある**ので、述語論理での証明を考えるときも/\や\/に置き換えた命題論理での証明を想定すると、整理しやすいかもしれない。

coqでの述語論理の表現

coqでは、

∀: forall a: A, P a
∃: exists a: A, P a

と表現する。forallもexistsも後続の->より結合度が低いので、述語論理の式では多くカッコで括ることになるだろう。

(forall a: A, P a -> Q a) -> (exists a: A, Q a -> R a) -> (exists a: A, P a -> R a) => 前２つのカッコは外せない
(forall a: A, P a -> (exists a: A, P a)) => これはカッコをすべて外しても同じ

命題論理では、命題変数A B: Propを導入するためにforallを使ったが、ここでは述語のみにforallをつかうようにするために、型変数はTheoremのパラメータ構文で指定することにする。

Theorem ABBA (A B: Prop): A/\B -> B/\A.

forallでの宣言と唯一違う点は、パラメータ側に変数を置くと、証明モードでは、変数ははじめから同名で仮定リストに追加された状態で始まることである。

述語論理のためのtactic一覧

forallとexistsにも、/\や\/と同様、導入と除去の推論規則がある。

導入規則:

|- forall a: A, B a [intro a0] a0: A |- B a0
a0: A |- exists a: A, B a [exists a0] a0: A |- B a0 (a部分すべてをa0に置き換える)

除去規則の類似品:

a0: A, FA: (forall a: A, B a) |- C [specialize FA with a0 as Ba0] a0: A, FA: (forall a: A, B a), Ba0: (B a0) |- C
EA: (exists a: A, B a) |- C [destruct EA as [a0 Ba0]] a0: A, Ba0: (B a0) |- C.

またforall除去としてapplyも使用できる。これはspecializeした上で、命題としてapplyすることに相当する。

a0: A, FA: (forall a: A, B a) |- B a0 [apply FA] a0: A, FA: (forall a: A, B a) |-
a0: A, FA: (forall a: A, B a -> C) |- C [apply FA with a0] a0: A, FA: (forall a: A, B a -> C) |- B a0
a0: A, Ba0: (B a0), FA: (forall a: A, B a -> C) |- D [apply FA with a0 in Ba0] a0: A, Ba0: C, FA: (forall a: A, B a -> C) |- D
a0: A, Ba0: (B a0), FA: (forall a: A, B a -> C) |- D [apply FA with a0 in Ba0 as C1] a0: A, Ba0: (B a0), FA: (forall a: A, B a -> C), C1: C |- D

ゴールではなく仮定に対してapplyする場合、apply ~ inを使う(asを入れないと、指定した仮定を置き換える)。

普通の推論規則でのように、ゴールに対して、除去規則を使う場合は以下で可能なようだ:

a0: A |- B a0 [generalize a0 as a] a0: A |- forall a: A, B a
a: A |- B a [apply ex_ind with A (fun a0: A => B a0)] a: A |- forall x : A, B x -> B a ; a: A |- exists a0: A, B a0

coqでexactマッチさせる場合、ゴール側を一般化させずに、仮定側を具体化するほうが普通は楽だろう。

述語論理版のド・モルガンの法則

命題論理でのド・モルガンの法則の4定理は、以下のものであった。

~(A\/B) -> ~A/\~B
~A/\~B -> ~(A\/B)
~A\/~B -> ~(A/\B)
~(A/\B) -> ~A\/~B

前述した変数束縛と命題の対応関係のようにA/\Bをforall a: A, P a、A\/Bをexists a: A, P aに置き換えると、そのまま以下のようになる:

~(exists a: A, P a) -> (forall a: A, ~(P a))
(forall a: A, ~(P a)) -> ~(exists a: A, P a)
(exists a: A, ~(P a)) -> ~(forall a: A, P a)
~(forall a: A, P a) -> (exists a: A, ~(P a))

これら4つの定理が、述語飯のド・モルガンの法則となる。

命題論理のときと同様に、4つ目の定理の証明には、NNPPが必須となる。

ド・モルガンの法則1: `~(exists a: A, P a) -> (forall a: A, ~(P a))` の証明

定理と証明のコード全体:

Theorem deMorgan1 (A: Type) (P: A->Prop):
  ~(exists x: A, P x) -> (forall x: A, ~(P x)).
Proof.
  intros NxPx x0 Px0.
  apply NxPx.
  (* NxPx: ~(exists x: A, P x), x0: A, Px0: (P x0) |- exists x: A, P x *)
  exists x0.
  exact Px0.
Qed.

Print deMorgan1.

命題論理版では、splitしてそれぞれleft/rightでゴールを選んでexactで解決させた。
述語論理ではそれがx0のintroとexistsに置き換わることで、場合わけなしで解決される。

この結果の定理=関数の実装コードは、

deMorgan1 =
fun (A : Type) (P : A -> Prop) (NxPx : ~ (exists x : A, P x))
  (x0 : A) (Px0 : P x0) => NxPx (ex_intro (fun x : A => P x) x0 Px0)
     : forall (A : Type) (P : A -> Prop),
       ~ (exists x : A, P x) -> forall x : A, ~ P x

Argument scopes are [type_scope function_scope _ _]

パラメータや型部分が多いが、本体はNxPx (ex_intro (fun x : A => P x) x0 Px0)だけである。
ex_introはex型のコンストラクタで、このインスタンスの型になるex a (P a)型の構文糖がexists a: A, P aである。

ド・モルガンの法則2: `(forall a: A, ~(P a)) -> ~(exists a: A, P a)` の証明

定理と証明のコード全体:

Theorem deMorgan2 (A: Type) (P: A->Prop):
  (forall x: A, ~(P x)) -> ~(exists x: A, P x).
Proof.
  intros xNPx xPx.
  destruct xPx as [x0 Px0].
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: (P x0)  |- False *)
  specialize xNPx with x0 as NPx0.
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: (P x0), NPx0: ~(P x0)  |- False *)
  apply NPx0.
  exact Px0.
Qed.

Print deMorgan2.

命題論理版では、仮定の~A/\~Bもdestructしたが、述語版では全称除去としてspecializeが使える。

この結果の定理=関数の実装コードは、

deMorgan2 =
fun (A : Type) (P : A -> Prop) (xNPx : forall x : A, ~ P x)
  (xPx : exists x : A, P x) =>
match xPx with
| ex_intro _ x0 Px0 => let NPx0 : ~ P x0 := xNPx x0 in NPx0 Px0
end
     : forall (A : Type) (P : A -> Prop),
       (forall x : A, ~ P x) -> ~ (exists x : A, P x)

Argument scopes are [type_scope function_scope function_scope]

となった。(本体はmatch ~ end部分)

ド・モルガンの法則3: `(exists a: A, ~(P a)) -> ~(forall a: A, P a)` の証明

定理と証明のコード全体:

Theorem deMorgan3 (A: Type) (P: A->Prop):
  (exists x: A, ~(P x)) -> ~(forall x: A, P x).
Proof.
  intros xNPx xPx.
  destruct xNPx as [x0 NPx0].
  (* xPx: (forall x: A, P x),  x0: A, NPx0: ~(P x0) |- False*)
  specialize xPx with x0 as Px0.
  (* xPx: (forall x: A, P x),  x0: A, NPx0: ~(P x0), Px0: (P x0) |- False *)
  apply NPx0.
  exact Px0.
Qed.

Print deMorgan3.

命題論理同様、2とほぼ同じ手順となる。

この結果の定理=関数の実装コードは、

deMorgan3 =
fun (A : Type) (P : A -> Prop) (xNPx : exists x : A, ~ P x)
  (xPx : forall x : A, P x) =>
match xNPx with
| ex_intro _ x0 NPx0 => let Px0 : P x0 := xPx x0 in NPx0 Px0
end
     : forall (A : Type) (P : A -> Prop),
       (exists x : A, ~ P x) -> ~ (forall x : A, P x)

Argument scopes are [type_scope function_scope _]

となった。

ド・モルガンの法則4: `~(forall a: A, P a) -> (exists a: A, ~(P a))` の証明

定理と証明のコード全体:

Theorem deMorgan4 (A: Type) (P: A->Prop):
  ~(forall x: A, P x) -> (exists x: A, ~(P x)).
Proof.
  Require Import Classical.

  intro NxPx.
  apply NNPP.
  intro NxNPx.
  (* NxPx: ~(forall x: A, P x), NxNPx: ~(exists x: A, ~P x) |- False *)
  apply NxPx.
  intro x0.
  apply NNPP.
  intro NPx0.
  (* NxPx: ~(forall x: A, P x), NxNPx: ~(exists x: A, ~P x),
     x0: A, NPx0: ~(P x0) |- False *)
  apply NxNPx.
  exists x0.
  exact NPx0.
Qed.

Print deMorgan4.

1と同様、split、left/rightのかわりに、x0のintroとexistsを使う。
そのうえで、命題論理での場合と同等の位置(ゴールが、exists全体、および、P x0のとき)で、apply NNPPする。

この結果の定理=関数の実装コードは、

deMorgan4 =
fun (A : Type) (P : A -> Prop) (NxPx : ~ (forall x : A, P x)) =>
NNPP (exists x : A, ~ P x)
  (fun NxNPx : ~ (exists x : A, ~ P x) =>
   NxPx
     (fun x0 : A =>
      NNPP (P x0)
        (fun NPx0 : ~ P x0 => NxNPx (ex_intro (fun x : A => ~ P x) x0 NPx0))))
     : forall (A : Type) (P : A -> Prop),
       ~ (forall x : A, P x) -> exists x : A, ~ P x

Argument scopes are [type_scope function_scope _]

となった。

まとめ

命題論理でのド・モルガンの法則の証明では、その推論規則を網羅しており、この証明によってそれなりの証明スキルが身につけることが期待できる。
一方、一階述語論理版の述語式にはforallとexistsの入れ子になった複雑な構造はないので、これだけやって十分というものではないだろう。
むしろ、命題論理から述語論理へ学習を進める場合の、第一ステップに適した題材だと思う。

最後に、述語版deMorgan4を使ったNNPPを証明を載せ、その等価性を示しておく。

Theorem nnpp (P: Prop): ~~P -> P.
Proof.
  intro NNP.
  (*NOTE: ~~P => ~(P -> False) => ~(forall _: P, False) *)
  apply deMorgan4 in NNP as PNN.
  (* NNP: ~~P, PNN: (exists _: P, ~False) |- P *)
  destruct PNN as [P0 NN].
  exact P0.
Qed.

Print nnpp.

付録: 要素が空の可能性

(coqの系と、普通の一階述語論理と少し違う部分について)

exists a: A, B aが成立するには、exists a0でのa0のように、Aには少なくとも一つの元がなくてはいけない。
しかし、coqの型は、Falseがそうであるように、要素が一つもない空集合的な型も存在しうる。

たとえば、論理式(forall a: A, P a) -> (exists a: A, P a)は、これだけでは証明は成立しない。
この証明には、exists tacticに渡す変数が仮定リストに必要だからである。

通常の一階述語論理での存在導入規則P a => exists x, Pxでは、空集合でないとして、適当な変数aを与えられるが、これはcoqでは不可能となる。
この結論のexists a: A, ...を成立させる場合には、Aが空でない要素がある前提/仮定が必要になる。

このため、(exists a: A, True)->...のようにdestructでAの元の存在を前提に導入したり、もしくはforall a: A, ...のようにintroでAの元が1つは存在する前提を作れるように、定理を記述する必要がある。

たとえば先の例に、(exists a: A, ...)->をつけることで、

Theorem ae (A: Type) (P: A->Prop): (exists a: A, True) -> (forall a: A, P a) -> (exists a: A, P a).
Proof.
  intros eA aPa.
  destruct eA as [a0 T].
  exists a0.
  apply aPa.
Qed.

と証明できる。

このように、結論のexists a: A, ...のためには、exists a0ができる可能性を定理中に含まなくてはいけない。