読者です 読者をやめる 読者になる 読者になる

きくらげ観察日記

好きなことを、適当に。

Coqで前提の矛盾から定理を証明する

矛盾を導く方法は何通りかあります。

すでに前提にFalseがある場合。

まずは一番基本的な方法から。既に前提にFalseがある場合です。
Falseの定義は、以下のようになっています。

Inductive False := (* コンストラクタが1つもない *).

従って、前提にP : Falseがある場合、destruct P.してしまえばその瞬間にPのすべてのケースについて証明が終了したこととなり、定理が示せます。

Goal forall Q : Prop, False -> Q.
Proof.
  intros Q F. (* Q : Prop, F : False *)
  destruct F.
Qed

これが一番基本的な方法です。
他の方法はすべてこの操作+αを自動でやってくれているだけなので、面倒であればこの方法以外覚えなくても大丈夫です。

また、Falseから任意の命題を導く専用のタクティック、contradictionもあります。使い方は先ほどと同じです。

Goal forall Q : Prop, False -> Q.
Proof.
  intros Q F. (* F : False *)
  contradiction.
Qed.

前提からFalseが導けそうな場合。

elimtype False.をすると、ゴールがFalseになります。あとは前提を適当に弄ってFalseを導ければ証明終了です。

Goal forall P Q : Prop,
       P -> ~ P -> Q.
Proof.
  intros P Q P1 NP. (* P1 : P, NP : ~ P *)
  elimtype False. (* ここでゴールがQでなくFalseになる *)
  apply NP in P1. (* P1 : False *)
  apply P1.
Qed.

ちなみに、~ PはP -> Falseの略記なので、apply NP in P1.とするとFalseが導けます。

elimtype Falseと全く同様のことをするタクティックとして、exfalsoというものがあります。

Goal forall P Q : Prop, P -> ~ P -> Q.
Proof.
  intros P Q HP NP. (* HP : P, NP : ~ P *)
  exfalso. (* ここでゴールがFalseになる *)
  apply NP in HP.
  assumption.
Qed.

また、前提からFalseが導けそうな場合も、先ほどのcontradictionタクティックを使うことができます。

Goal forall P Q : Prop, P -> ~ P -> Q.
Proof.
  intros P Q HP NP. (* HP : P, NP : ~ P *)
  contradiction.
Qed.

また、contradiction H.とすることで、矛盾を導くヒントとして命題Hを与えることもできます。

Goal forall P Q : Prop, P -> ~ P -> Q.
Proof.
  intros P Q HP NP. (* HP : P, NP : ~ P *)
  contradiction HP.
Qed.

前提からPと~ Pが導けそうな場合。

absurd P.をすると、ゴールがPと~ Pの2つになります。それらを証明すると、そこから自動的にFalseを導いてくれて証明終了になります。

Goal forall P Q R : Prop,
       P -> Q -> (Q -> ~ P) -> R.
Proof.
  intros P Q R H0 H1 H2. (* H0 : P, H1 : Q, H2 : Q -> ~ P *)
  absurd P. (* ここでゴールが P と ~ P に変わる *)
  - (* ~ P の証明 *)
    apply H2 in H1.
    apply H1.
  - (* P の証明 *)
    apply H0.
Qed.

前提に明らかに成り立たない等式がある場合

discriminate.をすると、前提にある明らかに成り立たない不等式を自動で発見して、そこからFalseを導いて定理を証明してくれます。

Goal 0 = 1 -> 1 + 1 = 334.
Proof.
  intros H. (* H : 0 = 1 *)
  discriminate.
Qed.

このProofでは1行目にintrosをしていますが、discriminateは自動でintrosもやってくれるようなので、これは無くてもいいです。

前提に明らかに左右の等しい不等式がある場合

congruence.をすると、前提にある明らかに左右の等しい不等式を利用して定理を証明してくれます。

Goal forall (x : nat) (P : Prop),
       x <> x -> P.
Proof.
  intros x p H. (* H : x <> x. ちなみにCoqでは不等号は<>です *)
  congruence.
Qed.

ちなみにcongruenceも自動でintrosしてくれるので、1行目は必要なかったりします。