coqtop -emacs のプロンプト

プロンプトについて

ProofGeneral や、coqtop-vim は裏で coqtop -emacs というコマンドを実行して、そこと通信しています。

coqtop -emacs を実行すると、標準エラー出力に <prompt>Coq < 1 || 0 < </prompt> というのが出てきます。ここを見ると現在の coqtop の状態がわかります。今回の記事はこれの説明です。(もしかしたら8.4系のみ)

プロンプトの文法と意味

プロンプトの構造は

<prompt>$current_theorem < $whole_state_number |$theorem_stack1|...|$theorem_stackn| $theorem_state_number < </prompt>

となっています。それぞれについて説明します。

current_theorem

現在証明しようとしている定理の名前が入ります。 例えば、

Theorem plus_n_O : forall n : nat, n = n + O.

と入力すると、current_theorem は plus_n_O になります。

Goal forall n : nat, n = n + O.

の場合は、Unnamed_thm や Unnamed_thm0 ... となります。

証明モードに入っていないとき(トップレベルのとき)には、Coq と表示されます。

whole_state_number

その coqtop プロセスの状態番号です。一つのコマンドを行うと、1増えます。Back 1. を行うと1減って、その番号の状態になります。

theorem_stack

証明しようとしている定理のスタックです。

例えば、

Thoerem Theorem_A : ... .
Proof.
  
  Theorem Theorem_B : ... .
  Proof.

のように、ある命題 Theorem_A の証明モードに入っているときに、命題 Theorem_B の証明モードに入ると、theorem_stack は |Theorem_B|Theorem_A| となります。Theorem_B の証明が終わると、|Theorem_A| となります。

証明モードに入っていないときにはここは空で、|| になります。

theorem_state_number

現在の証明の状態番号です。証明モードに入っていないときは0ですが、証明モードに入ると1になります。 その後、証明を進めると1ずつ増えます。証明の状態を進めるようなコマンドではないときには増えません。Qed. を行うと、0(または theorem_stack の2番めの定理の状態番号)に戻ります。

どう使うか

プロンプトを使って、コマンドの結果の出力がどのような意味を持つかを判断することができます。

例えば、

  • whole_state_number も theorem_state_number も変化なし => エラー
  • theorem_state_number (と whole_state_number) が変化 => 現在のサブゴールの状態
  • theorem_state_number は変化せず、whole_state_number のみ変化 => その他のいろいろな情報

となります。

coqtop server を書いた

Android 開発の授業の最終課題で Android 上で動く ProofGeneral 風のアプリを作ることにしたので、JSON API で操作できる coqtop サーバを書きました。その授業の発表が終わり次第公開すると思います。