読者です 読者をやめる 読者になる 読者になる

エンジニアですよ!

頑張れ俺くん、巨匠と呼ばれるその日まで

Coq入門 - 4.1

coq

https://coq.inria.fr/を見ていたら、Documentationのところにこんなものがあった。

https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf

ここにSearchのことが少し書いてあって、SearchRewriteで望むものが出てこない理由がわかった。

The command SearchRewrite is similar, but it only looks for rewriting theorems, that is, theorems where the proved predicate is an equality.

なるほど、rewriteっていうのは確かにそういうことか。

applyとは別ね。

applyしか使ってなくてよく分かっていなかった。

このドキュメントを読む感じだとSearchSearchPatternを使うべきっぽいが、emacsのcoq mode(かproof-general?)のコマンドにはそれらはない。

あるのは

  • SearchRewrite
  • SearchAbout
  • SearchConstant
  • Searchregexp
  • SearchIsos

のようだ。

RewriteとAboutは解説があるが、他は・・・?

特にemacsコマンドにドキュメントは書かれていないようだ

ただ、SearchIsosC-c C-a C-oにProofGeneralでバインドされていて、使う頻度が高そう。

使ってみるとエコーエリア?に

SearchPattern (parenthesis mandatory), ex: (?X1 + _ = _ + ?X1) (default nil): 

なんかSearchPatternと書いてあるし、クエリの例も求めているものっぽい。

使ってみると望み通りっぽい結果が出てきている。

これを使って進めてみよう。というメモ