使えるタクティク集

Coq を始めて、何をやっているかは分かっても、どういうタクティクを使えば今したいことができるのか分からなくなることがあるでしょう。この5章ではそういった問題のためによく使うタクティクをまとめます。

どんなタクティクを使えばいい?

小定理を示しながら証明を進めたいとき

証明中、証明を進めるために他の小定理を示して使いたくなる状況が出てきます。ですが Coq は基本的に「今のサブゴールを示すには A が成り立てばいいからサブゴールを A に変える」というように紙の上で証明するときとは逆向きに考えていくので、証明中に別の定理を証明するのは今まで使ったタクティクだけだと難しいです。そんなときのためにあるのが、assert タクティクです。

assert タクティクは、"assert (命題)." と書いて読み込ませることによって新しいサブゴールとして (命題) を追加します。

"(S /\ P) /\ (Q /\ R) -> (P /\ S) /\ (R /\ Q)" という命題を考えます。

Goal forall (P Q R S : Prop), (S /\ P) /\ (Q /\ R) -> (P /\ S) /\ (R /\ Q).

まずは intros します。

intros.

1 subgoal
P : Prop
Q : Prop
R : Prop
S : Prop
H : (S /\ P) /\ Q /\ R
______________________________________(1/1)
(P /\ S) /\ R /\ Q

"/\" は右結合なので "(X /\ Y) /\ (Z /\ W)" は括弧を省いて "(X /\ Y) /\ Z /\ W" と表示されています。

まず H を destruct してサブゴールを split してみます。

destruct H.
split.

2 subgoals
P : Prop
Q : Prop
R : Prop
S : Prop
H : S /\ P
H0 : Q /\ R
______________________________________(1/2)
P /\ S

______________________________________(2/2)
R /\ Q

この後はそれぞれのサブゴールを split していって、さらに H や H0 を destruct でばらしていっても証明はできますが、面倒です。さらに、この命題を頭の中で証明しようと思うと、"X /\ Y -> Y /\ X" をまず示して、それと仮定の H や H0 でサブゴールがすぐ示せる、と考えるのが紙の上で証明する感覚に近いでしょう。ここで、assert タクティクを使って

forall (X Y : Prop), X /\ Y -> Y /\ X

という命題を示して、これを使って "(S /\ P) -> (P /\ S)"、"(Q /\ R) -> (R /\ Q)" を証明して全体の証明に持って行く方針にします。

ですがここで assert を使っても、今の状態での最初のサブゴール(P /\ S)にしか "forall (X Y : Prop), X /\ Y -> Y /\ X" は追加されません。試しに assert してみます。

assert (forall (X Y : Prop), X /\ Y -> Y /\ X).

3 subgoals
P : Prop
Q : Prop
R : Prop
S : Prop
H : S /\ P
H0 : Q /\ R
______________________________________(1/3)
forall X Y : Prop, X /\ Y -> Y /\ X

______________________________________(2/3)
P /\ S

______________________________________(3/3)
R /\ Q

Command Pane で二番目と三番目のサブゴールに対応する仮定を表示してみましょう。

(左のテキストボックス)Show (右のテキストボックス)2.

Result for command Show 2 . :
subgoal 2 is:
  
 P : Prop
 Q : Prop
 R : Prop
 S : Prop
 H : S /\ P
 H0 : Q /\ R
 H1 : forall X Y : Prop, X /\ Y -> Y /\ X
 ============================
 P /\ S

二番目のサブゴールに対応する仮定には "H1 : forall X Y : Prop, X /\ Y -> Y /\ X" が入っていますね。

三番目はどうかというと、

Show 3.

Result for command Show 3 . :
subgoal 3 is:
  
 P : Prop
 Q : Prop
 R : Prop
 S : Prop
 H : S /\ P
 H0 : Q /\ R
 ============================
 R /\ Q

となっており、"forall X Y : Prop, X /\ Y -> Y /\ X" は仮定に入っていません。これだと最後のサブゴールでもまた assert をしなければいけなくなってしまって冗長です。そこで、split でサブゴールが分岐する前のサブゴールに戻って assert し、その後 split すれば分岐した両方のサブゴールに対して assert で追加した仮定が入ります。

split 前に戻ります。

1 subgoal
P : Prop
Q : Prop
R : Prop
S : Prop
H : S /\ P
H0 : Q /\ R
______________________________________(1/1)
(P /\ S) /\ R /\ Q

assert (forall (X Y : Prop), X /\ Y -> Y /\ X).

2 subgoals
P : Prop
Q : Prop
R : Prop
S : Prop
H : S /\ P
H0 : Q /\ R
______________________________________(1/2)
forall X Y : Prop, X /\ Y -> Y /\ X

______________________________________(2/2)
(P /\ S) /\ R /\ Q

これは 2章 で証明したので、一気に書いてしまいます。

intros.
destruct H1.
split.
apply H2.
apply H1.

1 subgoal
P : Prop
Q : Prop
R : Prop
S : Prop
H : S /\ P
H0 : Q /\ R
H1 : forall X Y : Prop, X /\ Y -> Y /\ X
______________________________________(1/1)
(P /\ S) /\ R /\ Q

assert で追加したサブゴールが証明され、仮定に H1 として現れました。

ここで split を使えば、分岐するどちらのサブゴールに対しても H1 は残ります。

split.

2 subgoals
P : Prop
Q : Prop
R : Prop
S : Prop
H : S /\ P
H0 : Q /\ R
H1 : forall X Y : Prop, X /\ Y -> Y /\ X
______________________________________(1/2)
P /\ S

______________________________________(2/2)
R /\ Q

この後はそれぞれのサブゴールに H0 を apply してやれば証明終了です。

apply (H1 S P H).

1 subgoal
P : Prop
Q : Prop
R : Prop
S : Prop
H : S /\ P
H0 : Q /\ R
H1 : forall X Y : Prop, X /\ Y -> Y /\ X
______________________________________(1/1)
R /\ Q

apply (H1 Q R H0).

Proof completed.

assert と似たタクティクで、cut があります。assert は (命題) を一番上のサブゴールに追加しましたが、cut は一番上のサブゴールを (命題) -> (元のサブゴール) に変え、(命題) を次のサブゴールとして追加します。

cut は assert と同じように

cut (命題).

と使います。今回の証明の assert の部分を cut に変えてみると、

1 subgoal
P : Prop
Q : Prop
R : Prop
S : Prop
H : S /\ P
H0 : Q /\ R
______________________________________(1/1)
(P /\ S) /\ R /\ Q

cut (forall (X Y : Prop), X /\ Y -> Y /\ X).

2 subgoals
P : Prop
Q : Prop
R : Prop
S : Prop
H : S /\ P
H0 : Q /\ R
______________________________________(1/2)
(forall X Y : Prop, X /\ Y -> Y /\ X) -> (P /\ S) /\ R /\ Q

______________________________________(2/2)
forall X Y : Prop, X /\ Y -> Y /\ X

一つ目のサブゴールが (cut で指定した命題) -> (元のサブゴール) になっていますね。証明は assert のときと似ているので一度に書いておきます。

Goal forall (P Q R S : Prop), (S /\ P) /\ (Q /\ R) -> (P /\ S) /\ (R /\ Q).
intros.
destruct H.
cut (forall (X Y : Prop), X /\ Y -> Y /\ X).
intro.
split.
apply (H1 S P H).
apply (H1 Q R H0).
intros.
destruct H1.
split.
apply H2.
apply H1.
Qed.

明かに異なる値が = で結ばれているとき

証明中に仮定に明かに異る値が = で結ばれている(3 = 2 など)とき、仮定が矛盾しているので 4章 でも述べたようにただちに全体は真となります。discriminate タクティクは、= で結ばれたコンストラクタやコンストラクタの引数が異なっているときそれは矛盾であることを Coq に教えます。

以下のような例題を考えます。

Require Import List.

Theorem app_eq_nil : forall (A : Type)(l l':list A), l ++ l' = nil -> l = nil /\ l' = nil.

intros して、サブゴールは /\ になるので split します。

intros.
split.

2 subgoals
l : list A
l' : list A
H : l ++ l' = nil
______________________________________(1/2)
l = nil

______________________________________(2/2)
l' = nil

l を destruct して、nil の場合と a :: l の場合に分けて考えます。

destruct l.

3 subgoals
l' : list A
H : nil ++ l' = nil
______________________________________(1/3)
nil = nil

______________________________________(2/3)
a :: l = nil

______________________________________(3/3)
l' = nil

l が nil の場合は nil = nil となり自明ですね。

reflexivity.

2 subgoals
a : A
l : list A
l' : list A
H : (a :: l) ++ l' = nil
______________________________________(1/2)
a :: l = nil

______________________________________(2/2)
l' = nil

a :: l のときはどうでしょう。仮定の H を見ると、"(a :: l) ++ l'" は明らかに nil に等しくないですが、等号で結ばれてしまっています。よって discriminate タクティクを使います。

discriminate.

1 subgoal
l : list A
l' : list A
H : l ++ l' = nil
______________________________________(1/1)
l' = nil

このサブゴールも同じ要領で示せるので、一度に書きます。

destruct l'.
 reflexivity.

 destruct l.
  discriminate.

  discriminate.
Qed.

Coq では "~ a = b" を OCaml 風に "a <> b" と書けます。~ は = より結合が弱く、"~ a = b" は "~ (a = b)" になります。~ P は P -> False のことでしたから、"a <> b" は 「a と b は等しくない」という意味ですね。サブゴールが <> で違うコンストラクタが結ばれていたときも discriminate タクティクが使えます。

次に例を示します。

Require Import List.

Goal forall (A : Type)(a : A), nil <> a :: nil.

1 subgoal
______________________________________(1/1)
forall (A : Type) (a : A), nil <> a :: nil

discriminate.

Proof completed.

等式に関する自動証明

等式に関する自動証明タクティクとして、congruence があります。congruence は、サブゴールが等式のとき、仮定にある等式の命題を使って自動的に証明を試みます。

あまり意味のない例で恐縮ですが、たとえば以下のような命題が証明できます。

Goal forall (n m : nat)(f : nat -> nat), f n = n -> S (f (f n)) = S m -> n = m.

1 subgoal
______________________________________(1/1)
forall (n m : nat) (f : nat -> nat), f n = n -> S (f (f n)) = S m -> n = m

intros.
congruence.

Proof completed.

congruence は discriminate の機能も持っています。

Require Import List.

Goal forall (A : Type)(x y : A), x :: y :: nil <> x :: nil.

1 subgoal
______________________________________(1/1)
forall (A : Type) (x y : A), x :: y :: nil <> x :: nil

intros.
congruence.

Proof completed.

rewrite でうまく書き換えできないとき

仮定に "H : a = b" がある状態で rewrite H. を使えばサブゴール中の a を b に書き換えられました。しかし a を b に書き換えたいけれど、a = b がまだ仮定にない、という状況になることがあります。そんなとき、"assert (a = b)." で a = b を示して仮定に入れ、それから rewrite する、という方法が考えられますが、それを一つの作業にまとめる replace というタクティクがあります。

replace は

replace a with b.

でサブゴールの a を b に変え、"b = a" という命題を上から二番目のサブゴールとして追加します。

また、rewrite では書き換える対象を上手く指定できなくなるケースがあり、そのようなときも replace タクティクは便利です。無理のある例ですが、たとえば以下のような状態です。

Goal forall (P Q : nat -> Prop)(a : nat), P (a * 2) \/ Q (a * 2).

1 subgoal
  
______________________________________(1/1)
forall (P Q : nat -> Prop) (a : nat), P (a * 2) \/ Q (a * 2)

intros.

1 subgoal
P : nat -> Prop
Q : nat -> Prop
a : nat
______________________________________(1/1)
P (a * 2) \/ Q (a * 2)

P や Q は具体的に何かは書きませんが、サブゴールの "a * 2" は "2 * a" に変形すれば * の定義から "a + (a + 0)" に簡約できます。ここで、何らか事情で Q に適用されている a * 2 だけを a + a の形で使いたいとします。

ここで

mult_comm : forall (n m : nat), n * m = m * n

を使って変形しようとすると、

rewrite mult_comm.

1 subgoal
P : nat -> Prop
Q : nat -> Prop
a : nat
______________________________________(1/1)
P (2 * a) \/ Q (2 * a)

となり、a * 2 が両方書き変わってしまいます。こんなとき、replace タクティクを使えば Q (a * 2) のみを Q (2 * a) に書き換えられます。

replace (Q (a * 2)) with (Q (2 * a)).

2 subgoals
P : nat -> Prop
Q : nat -> Prop
a : nat
______________________________________(1/2)
P (a * 2) \/ Q (2 * a)

______________________________________(2/2)
Q (2 * a) = Q (a * 2)

蛇足ですが 2 * a を (a + (a + 0)) に簡約するために、simpl タクティクを使ってみます。

simpl.

2 subgoals
P : nat -> Prop
Q : nat -> Prop
a : nat
b : nat
______________________________________(1/2)
P (a * 2) \/ Q (a + (a + 0))

______________________________________(2/2)
Q (2 * a) = Q (b * a)

使う変数を統一したいとき

以下のように、仮定に "a = b"、"c = d" など等式の形の命題がいくつかあり、サブゴールや他の仮定の中で a や b、c や d が入り交じっていて b を a に、d を c に統一したくなったとします。このような状況で活躍するのが subst タクティクです。

subst は、仮定に "H : X = Y" という命題があれば他の仮定とサブゴール内に現れるすべての X を Y に書き換えていきます。書き換えた後は H はもう必要ないので、自動で仮定から消してくれます。

以下の例を挙げます。

Goal forall (P : nat -> nat -> Prop)(a b c d : nat), P a d -> a = b -> c = d -> P b c.

1 subgoal
______________________________________(1/1)
forall (P : nat -> nat -> Prop) (a b c d : nat),
P a d -> a = b -> c = d -> P b c

intros.

1 subgoal
P : nat -> nat -> Prop
a : nat
b : nat
c : nat
d : nat
H : P a d
H0 : a = b
H1 : c = d
______________________________________(1/1)
P b c

rewrite を2回使う手も一つですが、このような証明図の状態を一度に整理できる subst というタクティクもあります。

subst.

1 subgoal
P : nat -> nat -> Prop
b : nat
d : nat
H : P b d
______________________________________(1/1)
P b d

項を新しい変数で置きたいとき

証明中に、ある項を新しい変数 x で "x = (項)" と置きたくなることが出てくるかもしれません。この操作は remember タクティクで実現できます。

remember タクティクは、

remember (項) as x.

と使うことにより (項)を x で置き換え、仮定に "x = (項)" を追加します。変数名にこだわりがなければ "as x" は付けず

remember (項).

と書くと Coq が変数名を自動で選んでくれます。

remember が証明で役に立つこんな性質を例として示してみます。

Require Import List.

Lemma removelast_app : forall (A : Type)(l l' : list A), l' <> nil  ->
  removelast (l++l') = l ++ removelast l'.

removelast は List モジュールで以下のように定義されており、 リストの最後の要素を取り除いたリストを返す関数です。

Fixpoint removelast (A : Type)(l:list A) : list A :=
  match l with
  | nil => nil
  | a :: nil => nil
  | a :: l => a :: removelast l
  end.

(* ただし A は省略可 *)

つまり removelast_app は、l' が空リストでなければ、「(l ++ l') の最後の要素を取り除いたリスト」と「l ++ (l' の最後の要素を取り除いたリスト)」は等しいことを表しています。

l に関しての帰納法で示してみます。

intros.
induction l.

2 subgoals
l' : list A
H : l' <> nil
______________________________________(1/2)
removelast (nil ++ l') = nil ++ removelast l'

______________________________________(2/2)
removelast ((a :: l) ++ l') = (a :: l) ++ removelast l'

一つ目のサブゴールは両辺ともに removelast l' になるので、そのまま reflexivity します。

reflexivity.

1 subgoal
a : A
l : list A
l' : list A
H : l' <> nil
IHl : removelast (l ++ l') = l ++ removelast l'
______________________________________(1/1)
removelast ((a :: l) ++ l') = (a :: l) ++ removelast l'

simpl で簡約してみると、

simpl.

1 subgoal
a : A
l : list A
l' : list A
H : l' <> nil
IHl : removelast (l ++ l') = l ++ removelast l'
______________________________________(1/1)
match l ++ l' with
| nil => nil
| _ :: _ => a :: removelast (l ++ l')
end = a :: l ++ removelast l'

となります。サブゴールは l ++ l' が nil かそうでないかで異なる結果を返すので、destruct (l ++ l') したくなるかもしれませんが、もしそうしてしまうと不都合が発生します。

destruct (l ++ l').

2 subgoals
a : A
l : list A
l' : list A
H : l' <> nil
IHl : removelast nil = l ++ removelast l'
______________________________________(1/2)
nil = a :: l ++ removelast l'

______________________________________(2/2)
a :: removelast (a0 :: l0) = a :: l ++ removelast l'

一つ目のサブゴールは l ++ l' が nil である場合ですが、仮定の H は "l' <> nil" を言っており、"l ++ l' = nil" かつ "l' <> nil" は矛盾しそうです。仮定から矛盾が導ければ apply False_ind を使って一つ目のサブゴールが示せますが、IHl やサブゴールにあった l ++ l' がそのまま nil に置き換えられているだけで"l ++ l' = nil" という情報はどこにも残っていません。

そこで、destruct する前に remember タクティクを使って "l0 = l ++ l'" という仮定を作って、destruct の対象を l0 にすれば、仮定に "nil = l ++ l'" が残ります。実際に destruct 前に戻してやってみましょう。

remember (l ++ l').

1 subgoal
a : A
l : list A
l' : list A
H : l' <> nil
l0 : list A
Heql0 : l0 = l ++ l'
IHl : removelast l0 = l ++ removelast l'
______________________________________(1/1)
match l0 with
| nil => nil
| _ :: _ => a :: removelast l0
end = a :: l ++ removelast l'

destruct l0.

2 subgoals
a : A
l : list A
l' : list A
H : l' <> nil
Heql0 : nil = l ++ l'
IHl : removelast nil = l ++ removelast l'
______________________________________(1/2)
nil = a :: l ++ removelast l'

______________________________________(2/2)
a :: removelast (a0 :: l0) = a :: l ++ removelast l'

apply False_ind でサブゴールを False に変え、仮定が矛盾していることを示せば一つ目のサブゴールは示せたことになります。ここから先は remember タクティクには関係なく、本質的でないので一度に書いてしまいます。

apply False_ind.
apply H.
destruct (app_eq_nil l l').
 rewrite Heql0.
 reflexivity.

 apply H1.
 f_equal.
 apply IHl.
Qed.

強力な destruct

case や destruct のように場合分けをするタクティクとして、inversion があります。inversion を使うと、場合分けをするコンストラクタの引数の条件を仮定に加えます。

これだけ聞いてもよく分からないと思うので、4章 で定義した InList を使った例題を挙げます。

Inductive InList (A : Type)(a : A) : list A -> Prop :=
  | headIL : forall xs, InList A a (a::xs)
  | consIL : forall x xs, InList A a xs -> InList A a (x::xs).

Goal forall (A : Type)(l : list A)(a a' : A), InList A a (a' :: l) -> a = a' \/ InList A a l.

まずは intros してみます。

intros.

1 subgoal
A : Type
l : list A
a : A
a' : A
H : InList A a (a' :: l)
______________________________________(1/1)
a = a' \/ InList A a l

"H : InList A a (a' :: l)" を headIL の場合と consIL の場合とに分けたいところです。しかし destruct を使ってしまうと、

destruct H.

2 subgoals
A : Type
l : list A
a : A
a' : A
xs : list A
______________________________________(1/2)
a = a' \/ InList A a l

______________________________________(2/2)
a = a' \/ InList A a l

となり、destruct は単に headIL で出てきた xs を仮定に加えただけで、証明はこれ以上進みそうにありません。

ここで destruct の読み込みを戻して inversion タクティクを使うとこうなります。

inversion H.

2 subgoals
A : Type
l : list A
a : A
a' : A
H : InList A a (a' :: l)
xs : list A
H1 : a = a'
H2 : xs = l
______________________________________(1/2)
a' = a' \/ InList A a' l

______________________________________(2/2)
a = a' \/ InList A a l

destruct では使えそうな仮定は増えませんでしたが、inversion は仮定に "H1 : a = a'" や "H2 : xs = l" といった headIL の引数の条件を加えています。さらにサブゴール内の a を自動的に a' に書き換えてくれているので、\/ の左側を reflexivity で示せば一つ目のサブゴールは証明できます。

left.
reflexivity.

1 subgoal
A : Type
l : list A
a : A
a' : A
H : InList A a (a' :: l)
x : A
xs : list A
H1 : InList A a l
H0 : x = a'
H2 : xs = l
______________________________________(1/1)
a = a' \/ InList A a l

今度は H が consIL の場合です。consIL の型から H1 が出てきたので、これを \/ の右側に apply すればもう証明終了です。

right.
apply H1.

Proof completed.

タクティクや定理のまとめ

これまでに沢山のタクティクや定理が出てきましたが、どういうときに何が使えるか頭の中で整理しきれないかもしれません。そこで、この小節では5章までに出てきたタクティクや定理をまとめます。

基本のタクティク

intro, instros	forall x, や P -> Q がサブゴールのとき仮定に x や P を追加する
apply X	仮定 X をサブゴールに適用する
remember x as y	x を y で置き換え、仮定に x = y を追加
assert (命題), cut (命題)	(命題) を新しいサブゴールとして追加する
generalize X	仮定 X をサブゴールに戻す(6章で登場)
exists x	サブゴールが exists a, P a のとき x を a として与える

項の書き換え

simpl	定義に基いて簡約する、仮定に H があるとき simpl in H. で H を簡約
unfold x	x が Definition や Fixpoint などで定義されているとき、x を定義の形に展開
unfold x in H	仮定 H 内で unfold x

コンストラクタを適用

constructor	適用できるコンストラクタを自動で適用
split	コンストラクタが一つのとき、それを適用
left, right	コンストラクタが二つのとき、そのうち一つ目(二つ目)を適用

場合分け(パターンマッチ)

destruct H, case H	仮定 H を場合分け
inversion H	コンストラクタの引数の条件を保存して場合分け

帰納法

induction x

x について帰納法

等式の変形

rewrite H	H : x = y のときサブゴールの x を y に書き換える
rewrite <- H	H : x = y のときサブゴールの y を x に書き換える
rewrite H in H0	仮定 H0 内で rewrite H
replace x with y	x を y に書き換え、x = y を次のサブゴールに追加する
reflexivity	x = x の形のサブゴールを証明する
subst	仮定に x1 = y1, x2 = y2, ... があるとき、仮定やサブゴールすべての x1, x2, ... を y1, y2, ... で置き換える
f_equal	サブゴールが f x = f y のとき、x = y に変える
discriminate	仮定に異るコンストラクタが = で結ばれているとき現在のサブゴールを証明する

自動証明

auto, tauto, intuition	命題論理の自動証明
auto with arith, omega	自然数に関する命題の自動証明
congruence	等式に関しての自動証明、discriminate もする

練習問題

以下の命題を証明してみてください。前回出さなかった分、自然数についての命題も入れます。

問8. forall (n : nat), (exists m, n = 2 * m) \/ (exists m, n = 2 * m + 1)

問9. forall (A : Type)(l m:list A) (a:A), InList A a (l ++ m) -> InList A a l \/ InList A a m.