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.
© 2010 Magicant / 初出 2010-06-20