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しか使ってなくてよく分かっていなかった。
このドキュメントを読む感じだとSearchやSearchPatternを使うべきっぽいが、emacsのcoq mode(かproof-general?)のコマンドにはそれらはない。
あるのは
- SearchRewrite
- SearchAbout
- SearchConstant
- Searchregexp
- SearchIsos
のようだ。
RewriteとAboutは解説があるが、他は・・・？
特にemacsコマンドにドキュメントは書かれていないようだ
ただ、SearchIsosがC-c C-a C-oにProofGeneralでバインドされていて、使う頻度が高そう。
使ってみるとエコーエリア？に
SearchPattern (parenthesis mandatory), ex: (?X1 + _ = _ + ?X1) (default nil):
なんかSearchPatternと書いてあるし、クエリの例も求めているものっぽい。
使ってみると望み通りっぽい結果が出てきている。
これを使って進めてみよう。というメモ
