Coq Tips

このページの内容は古くなっています。Coq クィックリファレンスを見てください。

以下、Parameters A B C P Q R : Prop. を仮定。

前件 (仮定) が……の場合

仮定が `False` の場合・仮定に矛盾がある場合

矛盾の証明を参照

仮定が否定の場合 (`~A` の形)

~A の正体は A -> False であることに注意。ゴールが False の場合にこの仮定を apply することはできるが、それ以外の場面では扱いづらい。矛盾の証明も参照。

仮定が含意の場合 (`A -> B` の形)

apply で適用する。

Coq < Lemma l1 : A -> (A -> B) -> B.
1 subgoal

  ============================
   A -> (A -> B) -> B

l1 < intros.
1 subgoal

  H : A
  H0 : A -> B
  ============================
   B

l1 < apply H0.
1 subgoal

  H : A
  H0 : A -> B
  ============================
   A

l1 < exact H.
Proof completed.

l1 < Qed.
intros.
apply H0.
exact H.
l1 is defined

Coq < Lemma l2 : A -> (A -> B) -> B.
1 subgoal

  ============================
   A -> (A -> B) -> B

l2 < intros.
1 subgoal

  H : A
  H0 : A -> B
  ============================
   B

l2 < apply H0 in H.
1 subgoal

  H : B
  H0 : A -> B
  ============================
   B

l2 < exact H.
Proof completed.

仮定が連言の場合 (`A /\ B` の形)

decompose [and] や elim で複数の仮定に分ける。

Coq < Lemma l : A /\ B -> A.
1 subgoal

  ============================
   A /\ B -> A

l < intros.
1 subgoal

  H : A /\ B
  ============================
   A

l < decompose [and] H.
1 subgoal

  H : A /\ B
  H0 : A
  H1 : B
  ============================
   A

l < Restart.
1 subgoal

  ============================
   A /\ B -> A

l < intros.
1 subgoal

  H : A /\ B
  ============================
   A

l < elim H.
1 subgoal

  H : A /\ B
  ============================
   A -> B -> A

l < intros; assumption.
Proof completed.

仮定が選言の場合 (`A \/ B` の形)

inversion や decompose [or] で場合分けする。

Coq < Lemma l : A \/ B -> ~B -> A.
1 subgoal

  ============================
   A \/ B -> ~ B -> A

l < intros.
1 subgoal

  H : A \/ B
  H0 : ~ B
  ============================
   A

l < inversion H.
2 subgoals

  H : A \/ B
  H0 : ~ B
  H1 : A
  ============================
   A

subgoal 2 is:
 A

l < assumption.
1 subgoal

  H : A \/ B
  H0 : ~ B
  H1 : B
  ============================
   A

l < contradiction.
Proof completed.

l < Restart.
1 subgoal

  ============================
   A \/ B -> ~ B -> A

l < intros.
1 subgoal

  H : A \/ B
  H0 : ~ B
  ============================
   A

l < decompose [or] H.
2 subgoals

  H : A \/ B
  H0 : ~ B
  H1 : A
  ============================
   A

subgoal 2 is:
 A

l < assumption.
1 subgoal

  H : A \/ B
  H0 : ~ B
  H1 : B
  ============================
   A

l < contradiction.
Proof completed.

仮定が全称量化子 (`forall`) の場合

apply で適用する。

Coq < Parameter P : nat -> Prop.
P is assumed

Coq < Lemma l : (forall x : nat, P x) -> (exists y : nat, P y).
1 subgoal

  ============================
   (forall x : nat, P x) -> exists y : nat, P y

l < intros.
1 subgoal

  H : forall x : nat, P x
  ============================
   exists y : nat, P y

l < exists 0.
1 subgoal

  H : forall x : nat, P x
  ============================
   P 0

l < apply H.
Proof completed.

仮定が存在量化子 (`exists`) の場合

decompose [ex] や elim で量化される存在を具体化する。

Coq < Parameter P : nat -> Prop.
P is assumed

Coq < Lemma l : (exists x : nat, ~ P x) -> ~ (forall y : nat, P y).
1 subgoal

  ============================
   (exists x : nat, ~ P x) -> ~ (forall y : nat, P y)

l < intros.
1 subgoal

  H : exists x : nat, ~ P x
  ============================
   ~ (forall y : nat, P y)

l < decompose [ex] H.
1 subgoal

  H : exists x : nat, ~ P x
  x : nat
  H0 : ~ P x
  ============================
   ~ (forall y : nat, P y)

l < unfold not; intros.
1 subgoal

  H : exists x : nat, ~ P x
  x : nat
  H0 : ~ P x
  H1 : forall y : nat, P y
  ============================
   False

l < apply H0; apply H1.
Proof completed.

後件 (ゴール) が……の場合

ゴールが `True` の場合

exact I を使う。tauto や auto でもよい。

ゴールが `False`・否定の場合

~A の正体は A -> False であることに注意。ゴール ~A を直接導くことが難しい場合は、 unfold not で A -> False に展開し、矛盾を導く。

ゴールが含意の場合 (`A -> B` の形)

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

Coq < Lemma l : A -> A.
1 subgoal

  ============================
   A -> A

l < intro H.
1 subgoal

  H : A
  ============================
   A

ゴールが連言の場合 (`A /\ B` の形)

split でゴールを分けてそれぞれを証明する。

Coq < Lemma l : A -> B -> A /\ B.
1 subgoal

  ============================
   A -> B -> A /\ B

l < intros.
1 subgoal

  H : A
  H0 : B
  ============================
   A /\ B

l < split.
2 subgoals

  H : A
  H0 : B
  ============================
   A

subgoal 2 is:
 B

仮定 A /\ B /\ C からゴール (A /\ B) /\ C を証明するのは tauto 一発で済む。(→トートロジー)

ゴールが選言の場合 (`A \/ B` の形)

left または right でどちらか一方を選び、選んだほうを証明する。

Coq < Lemma l : A -> (A \/ B).
1 subgoal

  ============================
   A -> A \/ B

l < intro.
1 subgoal

  H : A
  ============================
   A \/ B

l < left.
1 subgoal

  H : A
  ============================
   A

l < assumption.
Proof completed.

A \/ B \/ C は A \/ (B \/ C) であることに注意。(例えば B を選ぶには right して left する)

ゴールが全称量化子 (`forall`) の場合

intro または intros で量化される値を仮定に移動する。

Coq < Lemma l : forall A : Prop, A -> A.
1 subgoal

  ============================
   forall A : Prop, A -> A

l < intros.
1 subgoal

  A : Prop
  H : A
  ============================
   A

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

exists で実例を与える。

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

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

l < exists 0.
1 subgoal

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

または、evar で実例の存在を仮定し、後で instantiate で実例を具体化する。

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

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

l < evar (n' : nat).
1 subgoal

  n' := ?8 : nat
  ============================
   exists n : nat, forall m : nat, m = n -> m = 0

l < exists n'; intros.
1 subgoal

  n' := ?8 : nat
  m : nat
  H : m = n'
  ============================
   m = 0

l < instantiate (1 := 0) in (Value of n').
1 subgoal

  n' := 0 : nat
  m : nat
  H : m = n'
  ============================
   m = 0

l < exact H.
Proof completed.

eapply で直接メタ変数を導入したりメタ変数を実例と単一化したりすることもできる。

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

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

l < eapply ex_intro.
1 subgoal

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

l < intros.
1 subgoal

  m : nat
  H : m = ?4
  ============================
   m = 0

l < eapply H.  (* ここでは eapply の代わりに eexact でも可 *)
Proof completed.

ゴールが恒真命題 (トートロジー) の場合

直観主義論理の恒真命題に対しては tauto が使える。より複雑な命題に対しては intuition や firstorder を試すとよい。

ゴールが等式の場合 (`A = B` の形)

自明な等式については reflexivity (apply refl_equal) や auto が使える。

Coq < Lemma l : 3 = 3.
1 subgoal

  ============================
   3 = 3

l < reflexivity.
Proof completed.

等式の両辺を入れ替えるには symmetry を使う。

ゴール A = B を A = C と C = B に分けるには transitivity C を使う。

Coq < Lemma l : A = B -> B = C -> A = C.
1 subgoal

  ============================
   A = B -> B = C -> A = C

l < intros.
1 subgoal

  H : A = B
  H0 : B = C
  ============================
   A = C

l < transitivity B.
2 subgoals

  H : A = B
  H0 : B = C
  ============================
   A = B

subgoal 2 is:
 B = C

l < assumption.
1 subgoal

  H : A = B
  H0 : B = C
  ============================
   B = C

もっとも、同値変形の繰り返しは congruence に任せればよい。

Coq < Lemma l : 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

l < congruence.
Proof completed.

F A = F B の形を A = B の形にするには f_equal が使える。

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

l < f_equal.
1 subgoal

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

ゴールが不等式の場合 (`A <> B` の形)

A <> B の正体は ~(A = B) すなわち A = B -> False であることに注意。ゴールが False・否定の場合を参照。

構文的に自明な不等式については直接 discriminate が使える。

Coq < Lemma l : 0 <> 1.
1 subgoal

  ============================
   0 <> 1

l < discriminate.
Proof completed.

congruence はゴールが不等式の場合も使える。 (→等式の場合)

Coq < Lemma l : forall a b c d e : nat, 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

l < congruence.
Proof completed.

証明の中で補題を宣言・証明する

assert または cut を使う。

assert H を使うと、まずその補題の証明を求められる。すなわち、 H が新たなサブゴールとなる。補題の証明が終わると、その補題が仮定に加わり、元のゴールの証明に戻る。

cut H を使うと、現在のゴール G が新しいゴール H -> G に変わる。新しいゴールの証明が終った後に補題の証明を行う。

矛盾の証明

仮定の一つが False そのものの場合、または仮定から簡単に False が導ける場合は、contradiction でどんなゴールも証明できる。

Coq < Lemma l : A -> ~A -> 0 = 1.
1 subgoal

  ============================
   A -> ~ A -> 0 = 1

l < intros.
1 subgoal

  H : A
  H0 : ~ A
  ============================
   0 = 1

l < contradiction.
Proof completed.

すぐに False を導くことが難しい場合は、apply False_ind するとゴールが False に変わるので、自分で False を導く。

Coq < Lemma l : P /\ ~ P -> 0 = 1.
1 subgoal

  ============================
   P /\ ~ P -> 0 = 1

l < intros.
1 subgoal

  H : P /\ ~ P
  ============================
   0 = 1

l < apply False_ind.
1 subgoal

  H : P /\ ~ P
  ============================
   False

l < decompose [and] H.
1 subgoal

  H : P /\ ~ P
  H0 : P
  H1 : ~ P
  ============================
   False

l < apply H1; apply H0.
Proof completed.

absurd から二律背反を導くことで矛盾を示すこともできる。

Coq < Lemma l : (A -> B) -> (A -> ~B) -> ~A.
1 subgoal

  ============================
   (A -> B) -> (A -> ~ B) -> ~ A

l < intros H0 H1; unfold not; intros H.
1 subgoal

  H0 : A -> B
  H1 : A -> ~ B
  H : A
  ============================
   False

l < absurd B.
2 subgoals

  H0 : A -> B
  H1 : A -> ~ B
  H : A
  ============================
   ~ B

subgoal 2 is:
 B

l < apply H1; assumption.
1 subgoal

  H0 : A -> B
  H1 : A -> ~ B
  H : A
  ============================
   B

l < apply H0; assumption.
Proof completed.

Coq Tips

目次

前件 (仮定) が……の場合

仮定が False の場合・仮定に矛盾がある場合

仮定が否定の場合 (~A の形)

仮定が含意の場合 (A -> B の形)

仮定が連言の場合 (A /\ B の形)

仮定が選言の場合 (A \/ B の形)

仮定が全称量化子 (forall) の場合

仮定が存在量化子 (exists) の場合

後件 (ゴール) が……の場合

ゴールが True の場合

ゴールが False・否定の場合

ゴールが含意の場合 (A -> B の形)

ゴールが連言の場合 (A /\ B の形)

ゴールが選言の場合 (A \/ B の形)

ゴールが全称量化子 (forall) の場合

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