証明事例集: ゴールが……のとき

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

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

前提がゴールに等しい場合を参照。

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

intro または intros で含意の仮定を前提に移動する。

Coq < Goal P -> P.
1 subgoal

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

Unnamed_thm < intro H.
1 subgoal

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

ゴールが代数的データ型の場合

ゴールの型が代数的データ型の場合は、適当なコンストラクタを適用する。コンストラクタが引数を取る場合は、それが新たなゴールとなり得る。

ゴールが True の場合

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

Inductive True := I.

ゴールが True の場合は、引数を取らないコンストラクタ I を適用すれば証明が完了する:

Coq < Goal True.
1 subgoal

  ============================
   True

Unnamed_thm < apply I.
Proof completed.

ゴールが False の場合

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

Inductive False := .

この型はコンストラクタを持たないため、この型を持つ値は存在しない。よって、前提から False を導かない限りこれを証明することはできない。

ゴールが連言の場合 (P /\ Q の形)

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

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

従って、その (唯一の) コンストラクタ conj が適用でき、その結果二つのサブゴールが生成される。

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

  ============================
   P -> Q -> Q /\ P

Unnamed_thm < intros H1 H2.
1 subgoal

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

Unnamed_thm < apply conj.  (* 代わりに split. でもよい *)
2 subgoals

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

subgoal 2 is:
 P

Unnamed_thm < apply H2.
1 subgoal

  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.

従って、二つのコンストラクタ or_introl, or_intror のうちどちらかを適用でき、その結果新たなサブゴールが生成される。なお、P \/ Q \/ R は P \/ (Q \/ R) であることに注意。

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

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

Unnamed_thm < intro H.
1 subgoal

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

Unnamed_thm < apply or_intror.  (* 代わりに right. でもよい *)
1 subgoal

  H : Q
  ============================
   Q \/ R

Unnamed_thm < apply or_introl.  (* 代わりに left. でもよい *)
1 subgoal

  H : Q
  ============================
   Q

Unnamed_thm < apply H.
Proof completed.

ゴールが存在量化子 (exists) の場合

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

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

従ってその (唯一の) コンストラクタ ex_intro を適用すればよいのであるが、普通に apply ex_intro したのでは値 x の推論に失敗してエラーとなる。ゆえに、x を明示して適用せねばならない。

Coq < Goal exists n : nat, n = 0.
1 subgoal

  ============================
   exists n : nat, n = 0

Unnamed_thm < apply ex_intro with 0.  (* 代わりに exists 0. でもよい*)
1 subgoal

  ============================
   0 = 0

Unnamed_thm < reflexivity.
Proof completed.

eapply でメタ変数を導入し、後で実例を与えることもできる。

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

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

Unnamed_thm < eapply ex_intro.  (* 代わりに eexists. でもよい *)
1 subgoal

  ============================
   forall m : nat, m = ?31 -> m = 0

Unnamed_thm < intros m H.
1 subgoal

  m : nat
  H : m = ?31
  ============================
   m = 0

Unnamed_thm < eapply H.  (* 代わりに eexact H. や eassumption. でもよい*)
Proof completed.

ゴールが等式の場合 (a = b の形)

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

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

従って、その (唯一の) コンストラクタ refl_equal を適用すればよい。

Coq < Goal 1 = 1.
1 subgoal

  ============================
   1 = 1

Unnamed_thm < apply refl_equal.  (* 代わりに reflexivity. でもよい *)
Proof completed.

ただし、両辺が可換でない場合は apply refl_equal (reflexivity) は失敗する。このような場合は両辺が可換となるように前提を用いて式変形する (→前提が等式の場合の例)。

ゴール f a = f b を a = b に変形するには f_equal が使える。

Coq < Goal forall m n, 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 < f_equal.
1 subgoal

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

Unnamed_thm < apply H.
Proof completed.

ゴールが同値変形の繰り返しで導ける場合は congruence が使える。

Coq < Goal forall a b c d e, a = b + c -> a = e -> b + c = d -> d = e.
1 subgoal

  ============================
   forall a b c d e : nat, a = b + c -> a = e -> b + c = d -> d = e

Unnamed_thm < congruence.
Proof completed.

ゴールが否定の場合 (~ P の形)

~ P の定義は P -> False であることに注意。ゴールが含意の場合を参照。

ゴールが不等式の場合 (a <> b の形)

a <> b の定義は ~ a = b すなわち a = b -> False であることに注意。ゴールが含意の場合および前提が等式の場合を参照。