Show Scriptコマンドによる証明の整形

Coq

(* この記事はTheorem Proving Advent Calendar 2011の5日目の記事です。 *)

Coqはタクティックを使って対話的に証明を構築していけます。その反面、注意して書かないと、読みにくい証明になってしまいます。
そんなときは、Show Scriptコマンドで整形すると楽になります。

例： 読みにくい証明

例として次のようなリストに関する補題を証明するときのことを考えてみます。

Require Import List.

Lemma rev_app_distr : forall A (x y:list A), 
  rev (x ++ y) = rev y ++ rev x.

Focusを使ってサブゴールを移動しながら証明したり、インデントなしで場合分けの証明したりすると、こんな感じの読みづらい証明になってしまいます。

Proof.
induction x as [| a l IHl].
destruct y as [| a l].
Focus 2.
simpl.
rewrite app_nil_r.
auto.
Show.
simpl.
auto.
intro y.
simpl.
rewrite (IHl y).
rewrite app_assoc.
trivial.
Qed.

Show Scriptコマンドによる証明の整形

そんなときは、Qedの直前にShow Scriptコマンドを使うと、次のような整形した証明を出力できます。

induction x as [| a l IHl].

 destruct y as [| a l].
  simpl.
  auto.
 
  simpl.
  rewrite app_nil_r.
  auto.
 
 intro y.
 simpl.
 rewrite (IHl y).
 rewrite app_assoc.
 trivial.

Focusによるサブゴールの入れ替えを元に戻して、場合分けごとにインデントしてくれます。
ただ、"現在の証明"に対してしか使えないのでQedする前でないと使えませんし、コメントはすべて消えてしまいます。

おまけ: そのほかのShow XXXコマンド

ちなみに、Show Script以外にも、証明木を表示するShow Treeコマンドもおもしろいです。
先ほどの証明をShow Treeすると、次のような証明木を出力できます。

 BY induction x as [| a l IHl]   
    A : Type
    ============================
     forall y : list A, rev (nil ++ y) = rev y ++ rev nil
 
   BY Evar change
     
      ============================
       forall y : list A, rev (nil ++ y) = rev y ++ rev nil
   
     BY destruct y as [| a l]
       
        ============================
         rev (nil ++ nil) = rev nil ++ rev nil
     
       BY Evar change
         
          ============================
           rev (nil ++ nil) = rev nil ++ rev nil

      ….

まとめ

Show Scriptコマンドで証明を整形すると、たのしいですよ。