証明ができない！ こんなとき

Coq で証明をしていて、紙の上ならできるのになぜか Coq だとできない、ということが起こります。よく Coq の証明で詰まりそうな例を二つ挙げ、どうして証明できなくなるかを説明します。

「P または P でない」について

こんな命題を示したくなったとします。

Definition eq_or_neq : forall (A : Type)(x y : A), x = y \/ x <> y.

これは「任意の型 A に対し、x と y は等しいか等しくないか」ということを表す命題です。「これは正しいし、証明できる命題だ」と思う人も多いでしょう。しかし、intros してみると仮定に A と x, y が入り、サブゴールは "x = y \/ x <> y" だけになります。

intros.

1 subgoal
A : Type
x : A
y : A
______________________________________(1/1)
x = y \/ x <> y

ここでできる操作といえば left/right を使って x = y か x <> y を示すことくらいですが、仮定には変数しかないのでどちらも証明できそうにありません。

では eq_or_neq を「正しいし証明できる」と考えたところが間違っていたのでは、と疑ってみます。

eq_or_neq の A に nat を代入した命題は、自然数に関する帰納法で証明できます(この証明は練習問題にします)。実際に n と m という自然数が与えられて、これらが等しいか等しくないかを判定したいなら、

というアルゴリズムによって判定できます。他にも list nat に対しても同じことが言えます。

では、今度は型 A を、無限に連なった自然数を一つのまとまりとする値の型だとします。別の言い方だと、nat の無限リストの型です。Coq の list は無限リストを扱えないので、list とは別の型です。そこで A の値 x、y に対して x と y が等しいか等しくないか判定しようとしてみると、困ったことになってしまいます。まず x と y の先頭の値を比べ、異なる値なら x <> y が分かります。一方 x と y の先頭が等しければ、それぞれ二番目の要素を比べ、それも等しければ三番目、……と比べていきます。しかしこうしても、x と y が完全に等しいことはどこまで比べても分かりません。つまり、無限リストの場合、任意の x、y に対してはそれらが等しいか等しくないかは分からないのです。

このように「等しいか等しくないか」が分からないケースが出てきてしまいました。実は Coq では eq_or_neq は証明できない命題なのです。

もちろん「判定できなくても、等しいか等しくないかのどちらかではあるはずだ」という考え方もあるでしょう。しかし、Coq ではその考え方を採用していません。具体的に判定できる場合のみに "x = y \/ x <> y" と表現でき、そうでないなら "x = y \/ x <> y" とは表現できません。

もっと一般に、Coq では

forall (P : Prop), P \/ ~ P

という法則が上のような理由で認められていません(x <> y は ~ x = y の意味でした)。この命題は「排中律(law of excluded middle)」と呼ばれています。eq_or_neq が、具体的にそれを判定するアルゴリズムがある場合にのみ成り立たせるように、排中律を認めないことで Coq での証明はすべてプログラムとして見なせるようになるのです。

排中律という言葉にはあまり馴染がないかもしれませんが、排中律が成り立てば背理法による証明が妥当になり、背理法による証明が妥当になるならば排中律が成り立つ、つまり排中律と「背理法による証明が妥当であること」は同値であることが知られています。ここで、背理法は P が結論のとき、~ P を仮定して矛盾を導くことをいいます。~ P が結論のとき P を仮定して矛盾を導くことは背理法とは言わないことにします。

背理法で証明をすると何が不都合なのでしょうか。たとえば「P x という性質が成り立つような x が存在する」という命題を背理法で証明したとします。すると「そのような x が存在しないと仮定すると矛盾する」ことが示されたわけですが、具体的に x を特定したわけではありません。つまりネッシーの存在を背理法で示すと、「ネッシーが存在しないと仮定すると矛盾する」を示しただけでネッシーをこの場に連れて来たわけではないのです。

逆に、背理法を使わなければ、証明は必ず具体的な x を与えるアルゴリズムになるのです。

さらに、排中律を認めないと、

forall (P : Prop), ~ ~ P -> P

という命題も成り立ちません。"~ ~ P" は "(P -> False) -> False" で、全体を言葉にすると「P でなくないならば P」になります。これも感覚的には当たり前のように成り立ちそうな命題ですが、Coq では証明できません。これは「二重否定の除去」と呼ばれます。

逆に二重否定の除去を認めないと排中律も成り立たちません。つまり「排中律」と「背理法」と「二重否定の除去」はすべて同値であることが知られています。

大雑把にいって、排中律を認めるような論理を古典論理と呼び、排中律を認めない論理を直観主義論理と呼びます。Coq では上のような理由で直観主義論理を採用しています。

直感主義論理では一見当たり前のように思っていた命題が成り立たないという不利な点もあるので、気を付ける必要があります。

たとえば「a はリスト l の要素であるか要素でないか」という命題、

forall (A : Type)(a : A)(l : list A), InList A a l \/ ~ InList A a l

は感覚的に証明できると思ってしまうかもしれませんができません。ただし、A についての eq_or_neq、

forall (x y : A), x = y \/ x <> y

が言えれば証明できます。つまり

forall (A : Type)(a : A)(l : list A), (forall (x y : A), x = y \/ x <> y) ->
  InList A a l \/ ~ InList A a l

は証明できます。

上のように条件を追加しても証明できなく、どうしても背理法による証明が必要になった場合は、

Require Import Classical.

と書いて Classical モジュール(古典論理のモジュール)をインポートすれば、公理として

classic : forall (P : Prop), P \/ ~ P

が使えるようになります。

このように「証明できるはずだけどできない」と思っていた命題は、実は証明できない命題であることが有り得ます。示したい命題が直観主義論理で証明できるかどうかは簡単には分かりませんが、存在証明のように「具体的に与えるアルゴリズムがあるか」や「背理法を使わずに証明できるか」と色々な命題について考えていけば、感覚的に分かっていきます。

さっぱり分からないかもしれませんが、最初のうちは背理法による証明ができないことや、排中律、二重否定の除去が成り立たないことを押さえておけば、プログラムの性質の大体は証明できると思って良いでしょう。

先程登場した

forall (A : Type)(a : A)(l : list A),
  (forall (x y : A), x = y \/ x <> y) -> InList A a l \/ ~ InList A a l

の証明は、今までの知識だけで証明できるので、結果だけ書いておきます。

Goal forall (A : Type)(a : A)(l : list A),
  (forall (x y : A), x = y \/ x <> y) -> InList A a l \/ ~ InList A a l.
intros.
induction l.
 right.
 intro.
 inversion H0.

 destruct IHl.
  left.
  constructor.
  apply H0.

  destruct (H a a0).
   left.
   rewrite H1.
   constructor.

   right.
   intro.
   inversion H2.
   apply (H1 H4).
   apply (H0 H4).
Qed.

帰納法に注意

簡単な命題だと、proof-editing mode に入り、とりあえず induction タクティクを使ってみると上手く行くことがよくあります。かといってそれで何でも上手く行くわけではありません。

こんな命題を証明してみましょう。

Theorem fold_symmetric :
  forall (A:Type) (f:A -> A -> A),
    (forall x y z:A, f x (f y z) = f (f x y) z) ->
    (forall x y:A, f x y = f y x) ->
    forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l.

この命題は、関数 f : A -> A -> A が

1. 結合律(forall x y z : A, f x (f y z) = f (f x y) z)
2. 可換律(forall x y : A, f x y = f y x)

をみたしているならば、fold_left しても fold_right しても同じ、ということを表しています。 fold_left と fold_right は List モジュールにあり、定義はこうです。

Fixpoint fold_left (A B : Type)(f : A -> B -> A)(l:list B) (a0:A) : A :=
  match l with
    | nil => a0
    | cons b t => fold_left A B f t (f a0 b)
  end.

Fixpoint fold_right (A B : Type)(f : B -> A -> A)(a0 : A)(l:list B) : A :=
  match l with
    | nil => a0
    | cons b t => f b (fold_right A B f a0 t)
  end.

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

まず l について場合分けをすれば式が簡約できそうなので、destruct タクティクを使います。

destruct l.

2 subgoals
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
______________________________________(1/2)
fold_left f nil a0 = fold_right f a0 nil

______________________________________(2/2)
fold_left f (a :: l) a0 = fold_right f a0 (a :: l)

l が仮定ではなく forall の中にある状態で destruct を使ったら、勝手に intros された状態になりました。 サブゴールが "forall x0 x1 x2 x3, P x0 x1 x2 x3" の状態で destruct x2.(もしくは induction) すると、x0、x1、x2 が intro されて destruct x2.(induction) したのと同じになります。今回のように -> が l (destruct の対象)にある場合は、それらも intro されます。

一つ目のサブゴールは定義からそのまま a0 :: nil = a0 :: nil に簡約されるので、reflexivity で証明できます。

1 subgoal
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
l : list A
______________________________________(1/1)
fold_left f (a :: l) a0 = fold_right f a0 (a :: l)

simpl タクティクで整理してみると

1 subgoal
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
l : list A
______________________________________(1/1)
fold_left f l (f a0 a) = f a (fold_right f a0 l)

ここで、これを証明するには仮定が足りないようなので induction タクティクで帰納法で証明したいところです。ですがこのまま induction タクティクを使っても、証明は進まないか冗長になってしまいます。なぜかは置いておいて、ここでおまじないだと思って generalize というタクティクを使ってみましょう。

generalize a, a0.

1 subgoal
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
l : list A
______________________________________(1/1)
forall a1 a2 : A, fold_left f l (f a2 a1) = f a1 (fold_right f a2 l)

generalize というタクティクは、intro と逆の操作、つまりサブゴールが Q x のとき指定した仮定をサブゴールにforall x, Q x や P x -> Q x の形で追加します。

これがどう役に立つかは置いておいて、この後に induction タクティクを使ってみます。

induction l.

2 subgoals
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
______________________________________(1/2)
forall a1 a2 : A, fold_left f nil (f a2 a1) = f a1 (fold_right f a2 nil)

______________________________________(2/2)
forall a2 a3 : A,
fold_left f (a1 :: l) (f a3 a2) = f a2 (fold_right f a3 (a1 :: l))

一つ目のサブゴールは簡単に示せます。

intros.
simpl.
apply H0.

1 subgoal
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
a1 : A
l : list A
IHl : forall a a0 : A, fold_left f l (f a0 a) = f a (fold_right f a0 l)
______________________________________(1/1)
forall a2 a3 : A,
fold_left f (a1 :: l) (f a3 a2) = f a2 (fold_right f a3 (a1 :: l))

次のサブゴールは、simpl と intros で整理すると、

simpl.
intros.

1 subgoal
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
a1 : A
l : list A
IHl : forall a a0 : A, fold_left f l (f a0 a) = f a (fold_right f a0 l)
a2 : A
a3 : A
______________________________________(1/1)
fold_left f l (f (f a3 a2) a1) = f a2 (f a1 (fold_right f a3 l))

となります。この後は少しトリッキーですが、式の書き換えと apply だけで証明ができます。a2 を x、a1 を y、(fold_right f a3 l) を z として右辺を仮定の H で書き換えると、

rewrite H.

1 subgoal
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
a1 : A
l : list A
IHl : forall a a0 : A, fold_left f l (f a0 a) = f a (fold_right f a0 l)
a2 : A
a3 : A
______________________________________(1/1)
fold_left f l (f (f a3 a2) a1) = f (f a2 a1) (fold_right f a3 l)

と変形されます。ここで IHl の型の右辺は、a に (f a2 a1)、a0 に a3 を代入すれば今のサブゴールの右辺と同じ形をしていると分かります。そこで、サブゴールの左辺を fold_left f l (f a3 (f a2 a1)) に変形できれば、IHl を apply して証明を完成させられます。ですから replace タクティクを使って f (f a3 a2) a1 を f a3 (f a2 a1) に書き換えてやりましょう。

replace (f (f a3 a2) a1) with (f a3 (f a2 a1)).

2 subgoals
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
a1 : A
l : list A
IHl : forall a a0 : A, fold_left f l (f a0 a) = f a (fold_right f a0 l)
a2 : A
a3 : A
______________________________________(1/2)
fold_left f l (f a3 (f a2 a1)) = f (f a2 a1) (fold_right f a3 l)


______________________________________(2/2)
f a3 (f a2 a1) = f (f a3 a2) a1

これで実際に IHl が適用できる形になりました。

apply IHl.

1 subgoal
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
a1 : A
l : list A
IHl : forall a a0 : A, fold_left f l (f a0 a) = f a (fold_right f a0 l)
a2 : A
a3 : A
______________________________________(1/1)
f a3 (f a2 a1) = f (f a3 a2) a1

最後に残ったサブゴールは、今度は H の型そのままなので、apply で証明終了です。

apply H.

Proof completed.

証明のまとめを書きます。

Theorem fold_symmetric :
  forall (A:Type) (f:A -> A -> A),
    (forall x y z:A, f x (f y z) = f (f x y) z) ->
    (forall x y:A, f x y = f y x) ->
    forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l.
destruct l.
 reflexivity.

 simpl.
 generalize a, a0.
 induction l.
  intros.
  simpl.
  apply H0.

  simpl.
  intros.
  rewrite H.
  replace (f (f a3 a2) a1) with (f a3 (f a2 a1)).
  apply IHl.
  apply H.
Qed.

この証明では generalize を使ってみましたが、generalize はなぜ必要だったのでしょうか。試しに generalize せずに induction してみます。

generalize 前の証明図はこうでした。

1 subgoal
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
l : list A
______________________________________(1/1)
fold_left f l (f a0 a) = f a (fold_right f a0 l)

generalize してから induction した場合のサブゴールはこうでしたね。

generalize a, a0.
induction l.
intros.
simpl.
apply H0.

1 subgoal
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
a1 : A
l : list A
IHl : forall a a0 : A, fold_left f l (f a0 a) = f a (fold_right f a0 l)
______________________________________(1/1)
forall a2 a3 : A,
fold_left f (a1 :: l) (f a3 a2) = f a2 (fold_right f a3 (a1 :: l))

一方、generalize せずに induction するとこうなります。

induction l.
simpl.
apply H0.

1 subgoal
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
a1 : A
l : list A
IHl : fold_left f l (f a0 a) = f a (fold_right f a0 l)
______________________________________(1/1)
fold_left f (a1 :: l) (f a0 a) = f a (fold_right f a0 (a1 :: l))

大きく違うところといえば、generalize したときの IHl の型には forall で a0 と a が束縛されていますが、しなかったときはそうではありません。これでどんな問題が出てくるか、先程と同じように証明を進めて見てみましょう。

rewrite H.
replace (f (f a0 a) a1) with (f a0 (f a a1)).

2 subgoals
A : Type
f : A -> A -> A
H : forall x y z : A, f x (f y z) = f (f x y) z
H0 : forall x y : A, f x y = f y x
a0 : A
a : A
a1 : A
l : list A
IHl : fold_left f l (f a0 a) = f a (fold_right f a0 l)
______________________________________(1/2)
fold_left f l (f a0 (f a a1)) = f (f a a1) (fold_right f a0 l)


______________________________________(2/2)
f a0 (f a a1) = f (f a0 a) a1

generalize したときは IHl をそのまま apply すれば良かったのですが、この状態ではそうは行きません。IHl 内では a0、a が forall で束縛されていないので、先程のように a に (f a1 a2) を代入する、といったことができないのです。

結果的に generalize を使わないと証明が進まなそうだとは分かりましたが、なぜこのようなことになるのでしょうか。generalize したときとしなかったときで、induction を使うとどう変わるのかについて考えてみます。

3章 に書いた、リストに関する帰納法の (2) を見てみます。

generalize する場合の induction する前のサブゴールはこうでした。

forall a1 a2 : A, fold_left f l (f a2 a1) = f a1 (fold_right f a2 l)

この状態で induction タクティクを使うと、帰納法の P(xs) が上の命題に対応します。よって (2) は

(2a) (forall a1 a2 : A, fold_left f xs (f a2 a1) = f a1 (fold_right f a2 xs))
  -> (forall a3 a4 : A, fold_left f (x :: xs) (f a4 a3) = f a3 (fold_right f a4 (x :: xs)))

となります。一方 generalize しない場合の induction 前のサブゴールは

fold_left f l (f a2 a1) = f a1 (fold_right f a2 l)

であり、(2) は

(2b) fold_left f xs (f a2 a1) = f a1 (fold_right f a2 xs)
  -> fold_left f (x :: xs) (f a2 a1) = f a1 (fold_right f a2 (x :: xs))

になります。(2a) と (2b) は似ているように見えて全く違う命題です。(2a) の -> の前では forall を使って a1、a2 は -> の後に出る a3、a4 とは関係ない任意の変数とされていますが、(2b) は -> の前と後とで同じ変数 a1、a2 が出てきてしまっています。その結果 (2a) は証明できたけれど (2b) は証明が進まなそうになったのです。

このように自分が今何を証明しようとしているかをはっきりさせると、「気付いたら証明できない命題を証明しようとしていた」という事態を防げます。Coq の上で証明しているうちに、だんだん機械作業になって何をしているか分からなくなることがありますが、そういうときは一旦コンピュータから離れて紙の上で証明してみるのが良いと思います。

練習問題

問10. 以下の命題

forall (n m : nat), n = m \/ n <> m

を証明しなさい。

問11. 任意の P, Q : nat -> Prop に対して、

(1) (forall n, P n -> Q n) -> ((forall n, P n) -> (forall n, Q n))

(2) ((forall n, P n) -> (forall n, Q n)) -> (forall n, P n -> Q n)

はそれぞれ成り立つか。成り立つ場合は証明し、そうでない場合は成り立たなくなるような P、Q を具体的に考えなさい。

前回の答え

Theorem problem8 : forall (n : nat), (exists m, n = 2 * m) \/ (exists m, n = 2 * m + 1).
intro.
induction n.
 left.
 exists 0.
 simpl.
 reflexivity.

 destruct IHn.
  right.
  destruct H.
  exists x.

  rewrite H.
  rewrite plus_comm.
  reflexivity.

  destruct H.
  left.
  exists (S x).
  rewrite plus_comm in H.
  rewrite mult_succ_r.
  rewrite plus_comm.
  rewrite H.
  reflexivity.
Qed.

Theorem problem9 : forall (A : Type)(l m:list A) (a:A),
  InList A a (l ++ m) -> InList A a l \/ InList A a m.
intros.
induction l.
 right.
 apply H.

 inversion H.
   subst.
   left.
   constructor.

   destruct (IHl H1).
    left.
    constructor.
    apply H3.

    right.
    apply H3.
Qed.