証明事例集: 前提が……のとき

Coq においてデータ型のプリミティブは二つある。

一つは関数の型であり、forall または -> を用いて表される。これは論理学でいうところのならばに対応している。関数に引数を与えることによって、その戻り値を得ることができる。すなわち、A -> B に A を与えることで、B を得ることができる。

もう一つは、Inductive 文によって定義された代数的データ型である。代数的データ型の値は、それに対して数学的帰納法や場合分けを行うことができる。

証明において前提を使用するということは、基本的には上記二つの操作のいづれかを行うということである。Coq での証明における前提に対する様々な操作は、以下に挙げるものもそうでないものも、いづれもこの二つの操作に帰着できるということを念頭に置かれたい。

以下の例では、全て予め Parameters P Q R : Prop. を実行してあるものとする。

前提がゴールに等しい場合

assumption で一発。

Coq < Goal P -> P.
1 subgoal

  ============================
   P -> P

Unnamed_thm < intro H.
1 subgoal

  H : P
  ============================
   P

Unnamed_thm < assumption.
Proof completed.

もちろん、exact H や apply H や refine H などでもよい。

前提が含意の場合 (P -> Q の形) および前提が全称量化子 (forall) の場合

apply で適用する。

Coq < Goal P -> (P -> Q) -> Q.
1 subgoal

  ============================
   P -> (P -> Q) -> Q

Unnamed_thm < intros H1 H2.
1 subgoal

  H1 : P
  H2 : P -> Q
  ============================
   Q

Unnamed_thm < apply H2.
1 subgoal

  H1 : P
  H2 : P -> Q
  ============================
   P

Coq < Goal P -> (P -> Q) -> Q.
1 subgoal

  ============================
   P -> (P -> Q) -> Q

Unnamed_thm < intros H1 H2.
1 subgoal

  H1 : P
  H2 : P -> Q
  ============================
   Q

Unnamed_thm < apply H2 in H1.
1 subgoal

  H1 : Q
  H2 : P -> Q
  ============================
   Q

Coq < Goal forall P : nat -> Prop, (forall n : nat, P n) -> P 0.
1 subgoal

  ============================
   forall P : nat -> Prop, (forall n : nat, P n) -> P 0

Unnamed_thm < intros P H.
1 subgoal

  P : nat -> Prop
  H : forall n : nat, P n
  ============================
   P 0

Unnamed_thm < apply H.
Proof completed.

最後の例は本来ならば apply (H 0) とすべきところだが、n が 0 であることは推論されるので、apply H だけでよい。

前提が代数的データ型の場合

前提の型が代数的データ型の場合は、induction や elim で数学的帰納法に持ち込んだり destruct や case や decompose で場合分けをしたりすることができる。

前提が True の場合

True は代数的データ型として定義されている:

Inductive True := I.

しかしその唯一のコンストラクタは引数を取らないため、これに対して数学的帰納法や場合分けをすることは意味をなさない。従って、前提に True があっても証明には何の役にも立たない。

前提が False の場合

False は代数的データ型として定義されている:

Inductive False := .

この型はコンストラクタを持たないため、場合分けの対象となる場合がない。従って、場合分けを行うと (どのようなゴールに対しても) 直ちに証明が終了する。

Coq < Goal False -> 0 = 1.
1 subgoal

  ============================
   False -> 0 = 1

Unnamed_thm < intro H.
1 subgoal

  H : False
  ============================
   0 = 1

Unnamed_thm < case H.  (* 代わりに destruct H. や inversion H. でもよい *)
Proof completed.

前提に False そのものはないが前提から False を導くことができそうな場合は、elimtype False を使うとゴールが False に変わるので、後はそれを導けば良い。

Coq < Goal P -> ~ P -> 0 = 1.
1 subgoal

  ============================
   P -> ~ P -> 0 = 1

Unnamed_thm < intros H1 H2.
1 subgoal

  H1 : P
  H2 : ~ P
  ============================
   0 = 1

Unnamed_thm < elimtype False.
1 subgoal

  H1 : P
  H2 : ~ P
  ============================
   False

Unnamed_thm < apply H2; apply H1.
Proof completed.

contradiction は、このような手続きをある程度自動化してくれる。

Coq < Goal P -> ~ P -> 0 = 1.
1 subgoal

  ============================
   P -> ~ P -> 0 = 1

Unnamed_thm < contradiction.
Proof completed.

また False を導くのに absurd を使うこともできる。absurd P はゴールを P と ~ P の二つに変え(そこから自動的に False を導いて証明を完了してくれ)る。

Coq < Goal (P -> Q) -> (P -> ~ Q) -> ~ P.
1 subgoal

  ============================
   (P -> Q) -> (P -> ~ Q) -> ~ P

Unnamed_thm < intros H1 H2 H3.
1 subgoal

  H1 : P -> Q
  H2 : P -> ~ Q
  H3 : P
  ============================
   False

Unnamed_thm < absurd Q.
2 subgoals

  H1 : P -> Q
  H2 : P -> ~ Q
  H3 : P
  ============================
   ~ Q

subgoal 2 is:
 Q

Unnamed_thm < apply H2; apply H3.
1 subgoal

  H1 : P -> Q
  H2 : P -> ~ Q
  H3 : P
  ============================
   Q

Unnamed_thm < apply H1; apply H3.
Proof completed.

前提が連言の場合 (P /\ Q の形)

連言は代数的データ型として定義されている:

Inductive and (A B : Prop) := conj : A -> B -> A /\ B.

従って、destruct や case を使って分解することができる。

1 subgoal

  H : P /\ Q
  ============================
   P

Unnamed_thm < destruct H as [ H1 H2 ].
1 subgoal

  H1 : P
  H2 : Q
  ============================
   P

Unnamed_thm < Undo.
1 subgoal

  H : P /\ Q
  ============================
   P

Unnamed_thm < case H.
1 subgoal

  H : P /\ Q
  ============================
   P -> Q -> P

Unnamed_thm < intros H1 H2.
1 subgoal

  H : P /\ Q
  H1 : P
  H2 : Q
  ============================
   P

Unnamed_thm < apply H1.
Proof completed.

前提が選言の場合 (P \/ Q の形)

選言は代数的データ型として定義されている:

Inductive or (A B : Prop) :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B.

従って、destruct や case を使って場合分けをすることができる。

Coq < Goal P \/ Q -> (P -> R) -> (Q -> R) -> R.
1 subgoal

  ============================
   P \/ Q -> (P -> R) -> (Q -> R) -> R

Unnamed_thm < intros H1 H2 H3.
1 subgoal

  H1 : P \/ Q
  H2 : P -> R
  H3 : Q -> R
  ============================
   R

Unnamed_thm < destruct H1 as [ HA | HB ].
2 subgoals

  HA : P
  H2 : P -> R
  H3 : Q -> R
  ============================
   R

subgoal 2 is:
 R

Unnamed_thm < apply (H2 HA).
1 subgoal

  HB : Q
  H2 : P -> R
  H3 : Q -> R
  ============================
   R

Unnamed_thm < apply (H3 HB).
Proof completed.

Coq < Goal (P \/ Q) -> (P -> R) -> (Q -> R) -> R.
1 subgoal

  ============================
   P \/ Q -> (P -> R) -> (Q -> R) -> R

Unnamed_thm < intros H1 H2 H3.
1 subgoal

  H1 : P \/ Q
  H2 : P -> R
  H3 : Q -> R
  ============================
   R

Unnamed_thm < case H1.
2 subgoals

  H1 : P \/ Q
  H2 : P -> R
  H3 : Q -> R
  ============================
   P -> R

subgoal 2 is:
 Q -> R

Unnamed_thm < apply H2.
1 subgoal

  H1 : P \/ Q
  H2 : P -> R
  H3 : Q -> R
  ============================
   Q -> R

Unnamed_thm < apply H3.
Proof completed.

前提が存在量化子 (exists) の場合

存在量化子は代数的データ型として定義されている:

Inductive ex (A : Type) (P : A -> Prop) :=
    ex_intro : forall x : A, P x -> ex P.

従って、destruct や case を使って分解することができる。

Coq < Goal forall P : nat -> Prop,
Coq <   (exists n : nat, ~ P n) -> ~ (forall n : nat, P n).
1 subgoal

  ============================
   forall P : nat -> Prop, (exists n : nat, ~ P n) -> ~ (forall n : nat, P n)

Unnamed_thm < intros P H1 H2.
1 subgoal

  P : nat -> Prop
  H1 : exists n : nat, ~ P n
  H2 : forall n : nat, P n
  ============================
   False

Unnamed_thm < destruct H1 as [ n H3 ].
1 subgoal

  P : nat -> Prop
  n : nat
  H3 : ~ P n
  H2 : forall n : nat, P n
  ============================
   False

Unnamed_thm < apply H3; apply H2.
Proof completed.

Coq < Goal forall P : nat -> Prop,
Coq <   (exists n : nat, ~ P n) -> ~ (forall n : nat, P n).
1 subgoal

  ============================
   forall P : nat -> Prop, (exists n : nat, ~ P n) -> ~ (forall n : nat, P n)

Unnamed_thm < intros P H1 H2.
1 subgoal

  P : nat -> Prop
  H1 : exists n : nat, ~ P n
  H2 : forall n : nat, P n
  ============================
   False

Unnamed_thm < case H1.
1 subgoal

  P : nat -> Prop
  H1 : exists n : nat, ~ P n
  H2 : forall n : nat, P n
  ============================
   forall x : nat, ~ P x -> False

Unnamed_thm < intros n H3.
1 subgoal

  P : nat -> Prop
  H1 : exists n : nat, ~ P n
  H2 : forall n : nat, P n
  n : nat
  H3 : ~ P n
  ============================
   False

Unnamed_thm < apply H3; apply H2.
Proof completed.

前提が等式の場合 (a = b の形)

等式は代数的データ型として定義されている:

Inductive eq (A : Type) (x : A) : A -> Prop :=
    refl_equal : eq A x x.

従って、destruct や case を使って分解することができ、これによりゴールに含まれる左辺が右辺に (または右辺が左辺に) 置き換わる。しかしこのような等式を用いた式変形は destruct や case を使うよりも rewrite を使ったほうがわかりやすい。

Coq < Goal forall m n : nat, m = n -> S m = S n.
1 subgoal

  ============================
   forall m n : nat, m = n -> S m = S n

Unnamed_thm < intros m n H.
1 subgoal

  m : nat
  n : nat
  H : m = n
  ============================
   S m = S n

Unnamed_thm < rewrite H.
1 subgoal

  m : nat
  n : nat
  H : m = n
  ============================
   S n = S n

Unnamed_thm < reflexivity.
Proof completed.

あるコンストラクタ C に対し前提 C a = C b から a = b を得るには、injection を使う。

Coq < Goal forall m n : nat, S m = S n -> m = n.
1 subgoal

  ============================
   forall m n : nat, S m = S n -> m = n

Unnamed_thm < intros m n H.
1 subgoal

  m : nat
  n : nat
  H : S m = S n
  ============================
   m = n

Unnamed_thm < injection H.
1 subgoal

  m : nat
  n : nat
  H : S m = S n
  ============================
   m = n -> m = n

等式の両辺が明らかに異なるコンストラクタである場合は、discriminate を使うことで False を導き直ちに任意のゴールを証明することができる (以下の例では intro H の後に discriminate H しているが、discriminate は intros と前提の選択を自動的に行うので、実は discriminate だけで一発で解ける)。

Coq < Goal 0 = 1 -> 2 = 4.
1 subgoal

  ============================
   0 = 1 -> 2 = 4

Unnamed_thm < intro H.
1 subgoal

  H : 0 = 1
  ============================
   2 = 4

Unnamed_thm < discriminate H.
Proof completed.

rewrite の繰り返しでゴールが導ける場合は、congruence が自動的に解いてくれる (→ゴールが等式の場合の例)。

前提が否定の場合 (~ P の形)

~ P の定義は P -> False であることに注意。他の前提から P も導ける場合は、それに適用することで False を得ることができるので、任意の命題を証明できる (→前提が含意の場合, 前提が False の場合)。

Coq < Goal P -> ~ P -> 0 = 1.
1 subgoal

  ============================
   P -> ~ P -> 0 = 1

Unnamed_thm < intros H1 H2.
1 subgoal

  H1 : P
  H2 : ~ P
  ============================
   0 = 1

Unnamed_thm < apply H2 in H1.
1 subgoal

  H1 : False
  H2 : ~ P
  ============================
   0 = 1

または

Coq < Goal P -> ~ P -> 0 = 1.
1 subgoal

  ============================
   P -> ~ P -> 0 = 1

Unnamed_thm < intros H1 H2.
1 subgoal

  H1 : P
  H2 : ~ P
  ============================
   0 = 1

Unnamed_thm < elimtype False.
1 subgoal

  H1 : P
  H2 : ~ P
  ============================
   False

Unnamed_thm < apply H2.
1 subgoal

  H1 : P
  H2 : ~ P
  ============================
   P

前提が不等式の場合 (a <> b の形)

a <> b の定義は ~ a = b すなわち a = b -> False であることに注意。他の前提から a = b も導ける場合は、それに適用することで False を得ることができるので、任意の命題を証明できる (→前提が含意の場合, 前提が False の場合, 前提が等式の場合)。

Coq < Goal forall n, n <> 0 -> n = 0 -> 1 = 2.
1 subgoal

  ============================
   forall n : nat, n <> 0 -> n = 0 -> 1 = 2

Unnamed_thm < intros n H1 H2.
1 subgoal

  n : nat
  H1 : n <> 0
  H2 : n = 0
  ============================
   1 = 2

Unnamed_thm < apply H1 in H2.
1 subgoal

  n : nat
  H1 : n <> 0
  H2 : False
  ============================
   1 = 2

Unnamed_thm < case H2.
Proof completed.

不等式の両辺が明らかに等しい場合は、congruence が自動的に解いてくれる (実は上の例も congruence で一発で解ける)。

Coq < Goal forall m, m <> 0 -> exists n, m = S n.
1 subgoal

  ============================
   forall m : nat, m <> 0 -> exists n : nat, m = S n

Unnamed_thm < intros m H.
1 subgoal

  m : nat
  H : m <> 0
  ============================
   exists n : nat, m = S n

Unnamed_thm < destruct m as [ | m' ].
2 subgoals

  H : 0 <> 0
  ============================
   exists n : nat, 0 = S n

subgoal 2 is:
 exists n : nat, S m' = S n

Unnamed_thm < congruence.
1 subgoal

  m' : nat
  H : S m' <> 0
  ============================
   exists n : nat, S m' = S n

Unnamed_thm < exists m'.
1 subgoal

  m' : nat
  H : S m' <> 0
  ============================
   S m' = S m'

Unnamed_thm < reflexivity.
Proof completed.