プログラマのための Coq

CSS と Coq の記事が並ぶというシュールな展開ですが、これも嫌だ力のなせるわざです。今日の証明では SearchPattern とか eapply がでてくるよ！
本日のお題は、 filter 関数を2回適用しても結果のリストの長さが変わらないという性質 FilterLength の証明です。 filter 関数と FilterLength の定義は以下のようになってます。

Require Import List.

Fixpoint filter {a : Type} (f : a -> bool) (xs : list a) :=
  match xs with
    | nil => nil
    | (cons x xs) => if f x then cons x (filter f xs)
                            else filter f xs
  end.

Theorem FilterLength :
  forall {a:Type} (f : a -> bool) (xs : list a),
  length (filter f xs) <= length xs.

では、 coqtop で対話的に証明を行っていきましょう。

$ coqtop -l length.v
coqtop -l length.v
Welcome to Coq 8.2pl1 (September 2009)

FilterLength < Show.
Show.
1 subgoal
  
  ============================
   forall (a : Type) (f : a -> bool) (xs : list a),
   length (filter f xs) <= length xs

coqtop を起動したら、まずは証明すべき内容を確認しましょう。リスト操作関数の性質を検証したい場合、リストの構造に関する帰納法を使えばなんとかなります。たぶん。

FilterLength < induction xs.
induction xs.
2 subgoals
  
  a : Type
  f : a -> bool
  ============================
   length (filter f nil) <= length nil

subgoal 2 is:
 length (filter f (a0 :: xs)) <= length (a0 :: xs)

forall はできるだけ残しておくほうがいい、というアドバイスを id:yoshihiro503 さんからもらったので、 intros を行う前に induction を使ってみました。 今回の場合は xs の構造に関する場合分けなので、xs の前に書いてある仮定(a と f : a -> bool)が仮定に入ってしまいましたが、もし FilterLength の定義において xs が先頭に書いてあった場合は f に関してはゴールに残ります。やってみましょう。定理の引数の順番を変えた FilterLength2 を定義してみました。

FilterLength2 < Show.
Show.
1 subgoal
  
  ============================
   forall (a : Type) (xs : list a) (f : a -> bool),
   length (filter f xs) <= length xs

FilterLength2 < induction xs.
induction xs.
2 subgoals
  
  a : Type
  ============================
   forall f : a -> bool, length (filter f nil) <= length nil

subgoal 2 is:
 forall f : a -> bool, length (filter f (a0 :: xs)) <= length (a0 :: xs)

FilterLength2 < 

ゴールが "forall f : ..." の形をしています。この違いが後々証明で効いてくることもあるので引数の順番には注意が必要です。引数の順番を決める際の指針が欲しいですが、経験だそうです。

では、FilterLength の証明に戻ります。

2 subgoals
  
  a : Type
  f : a -> bool
  ============================
   length (filter f nil) <= length nil

subgoal 2 is:
 length (filter f (a0 :: xs)) <= length (a0 :: xs)

1つめの subgoal は簡単そうです。simpl で簡約します。

FilterLength < simpl.
simpl.
2 subgoals
  
  a : Type
  f : a -> bool
  ============================
   0 <= 0

subgoal 2 is:
 length (filter f (a0 :: xs)) <= length (a0 :: xs)

ゴールは明らかです。両辺が同じだから reflexivity で大丈夫かな？と思うわけですが、

FilterLength < reflexivity.
reflexivity.
Toplevel input, characters 0-11:
> reflexivity.
> ^^^^^^^^^^^
Error: Tactic failure: The relation le is not a declared reflexive relation. Maybe you need to require the Setoid library.

ダメでした。 reflexivity は等式にしか使えないそうです。SearchPattern で探してみます。

FilterLength < SearchPattern (_<=_).
SearchPattern (_<=_).
Gt.gt_S_le: forall n m : nat, S m > n -> n <= m
Gt.gt_le_S: forall n m : nat, m > n -> S n <= m
Le.le_refl: forall n : nat, n <= n
Le.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p
Le.le_O_n: forall n : nat, 0 <= n
...

長いので後半は省略しました。 Le.le_refl が求めるものですので、適用しましょう。

FilterLength < apply Le.le_refl.
apply Le.le_refl.
1 subgoal
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (filter f (a0 :: xs)) <= length (a0 :: xs)

1つめの subgoal の証明が完了しました。やったね。
今回は律儀に定理を自分で探して適用しましたが、実はこれくらい簡単なゴールだと auto で証明できちゃったりします。やってみます。

FilterLength < Undo.
Undo.
2 subgoals
  
  a : Type
  f : a -> bool
  ============================
   0 <= 0

subgoal 2 is:
 length (filter f (a0 :: xs)) <= length (a0 :: xs)

FilterLength < auto.
auto.
1 subgoal
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (filter f (a0 :: xs)) <= length (a0 :: xs)

素晴らしいですね。
続きまして帰納段階の証明です。まずは簡約してみます。

FilterLength < simpl.
simpl.
1 subgoal
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (if f a0 then a0 :: filter f xs else filter f xs) <= S (length xs)

if 文が邪魔ですね。帰納法の仮定を睨むと、if 文の条件式が真でも偽でも、ゴールが証明できそうな気がします。いわゆる場合分けがしたいですね。
ここで新しいタクティック case を導入します。

FilterLength < case (f a0).
case (f a0).
2 subgoals
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (a0 :: filter f xs) <= S (length xs)

subgoal 2 is:
 length (filter f xs) <= S (length xs)

case タクティックは、引数に取った式の場合分けを行ってサブゴールとしてくれます。 induction と似ています。

FilterLength < simpl.
simpl.
2 subgoals
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   S (length (filter f xs)) <= S (length xs)

subgoal 2 is:
 length (filter f xs) <= S (length xs)

帰納法の仮定をみると、明らかな気もしますが、両辺の頭に S がついています。"n <= m -> S n <= S m" は需要の多そうな定理だと思うので、探してみます。

FilterLength < SearchPattern (S _ <= S _).
SearchPattern (S _ <= S _).
Le.le_n_S: forall n m : nat, n <= m -> S n <= S m

そのまんまありました。適用します。

FilterLength < apply Le.le_n_S.
apply Le.le_n_S.
2 subgoals
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (filter f xs) <= length xs

subgoal 2 is:
 length (filter f xs) <= S (length xs)

帰納法の仮定そのままですね。

FilterLength < apply IHxs.
apply IHxs.
1 subgoal
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (filter f xs) <= S (length xs)

さて、どうしよう。よく見ると、ゴールの左辺と IHxs の左辺が同じですね。で、この共通の式 "length (filter f xs)" は "length xs" 以下であるというのが仮定に入っている。さらに、ゴールの右辺である "S (length xs)" は明らかに "(length xs)" よりも大きいです。
ということで、 "length (filter f xs) <= length xs -> length xs <= S (length xs) -> length (filter f xs) <= S (length xs)" という流れで証明をしたいです。いわゆる推移律ですね。
自然数の推移律は明らかだし需要がありそうなので、きっと標準ライブラリに入ってるだろうということで、探してみます。

FilterLength < SearchPattern (_ <= _ -> _ <= _ -> _ <= _ ).
SearchPattern (_ <= _ -> _ <= _ -> _ <= _ ).
Error: The pattern is not simple enough.

探せませんでした。残念。推移律みたいな定理をどうやって探したらいいのかわかりませんが、とりあえず "SearchPattern (_ <= _)" としてやると一応でてきます。

FilterLength < SearchPattern (_ <= _).
...
Le.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p
...

ちょっと反則っぽいですが、求める定理 Le.le_trans が見つかりました。適用してみます。

FilterLength < apply Le.le_trans.
apply Le.le_trans.
Toplevel input, characters 0-17:
> apply Le.le_trans.
> ^^^^^^^^^^^^^^^^^
Error: Unable to find an instance for the variable m.

だめでした。まぁ、明らかにゴールと形が違うからね。coq は、ゴールが "n <= p" の形だから n と p はマッチできるけど m がよくわからん、と言っています。そんなあなたに eapply 。

FilterLength < eapply Le.le_trans.
eapply Le.le_trans.
2 subgoals
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (filter f xs) <= ?11

subgoal 2 is:
 ?11 <= S (length xs)

Le.le_trans の m のところに謎の変数 "?11" が導入されました。 Le.le_trans は "n <= m -> m <= p -> n <= p" という形で、 "n <= p" の部分がゴールにマッチしたので、あとは "n <= m" と "m <= p" がそれぞれ証明できればいいです。そういうわけでゴールが2つになりました。
あとは ?11 という変数に証明できそうなちょうどいい式を与えてやればいいです。上で見たように ?11 に length xs を与えるのが簡単そうです。今回の場合は帰納法の仮定をそのまま適用してやれば、 ?11 が length xs になります。

FilterLength < apply IHxs.
apply IHxs.
1 subgoal
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length xs <= S (length xs)

明らかなので横着します。

FilterLength < auto.
auto.
Proof completed.

やったぜ！

FilterLength < Qed.
Qed.
induction xs.
 simpl in |- *.
 auto.
 
 simpl in |- *.
 case (f a0).
  simpl in |- *.
  apply Le.le_n_S.
  apply IHxs.
  
  eapply Le.le_trans.
   apply IHxs.
   
   auto.
   
FilterLength is defined

お疲れ様でした。