Isabelle方面から来た人間としてはやっぱりsledgehammerがほしいなー、と思うわけです。
そんなわけで探してみると、まさにそのものという感じの coqhammer というプロジェクトがあります。
いかにも公式っぽいサイトがありますが、GitHubのREADMEのほうがビルド・インストール方法など最新のものになっているので、とりあえず試すという場合にはこちらをみたほうがいいでしょう。
インストール方法はopamを使うのが一番簡単です。
coq-hammerを使うには当然事前にcoqを入れておく必要があります。最新のcoq-hammerはcoqのバージョン8.10を要求するので注意してください。
$ opam repo add coq-released https://coq.inria.fr/opam/released
$ opam install coq-hammer
実際に動かしてみます。ここでは対話的環境であるcoqtopを使っています。
$ coqtop
Welcome to Coq 8.10.1 (December 2019)
まずは以下のようにしてhammerプラグインをロードします。
Coq < From Hammer Require Import Hammer.
[Loading ML file newring_plugin.cmxs ... done]
[Loading ML file omega_plugin.cmxs ... done]
[Loading ML file hammer_plugin.cmxs ... done]
動作確認用の関数を定義します。
Coq < Fixpoint pow a k :=
Coq < match k with
Coq < | 0 => 1
Coq < | S(k') => a * (pow a k')
Coq < end.
pow is defined
pow is recursively defined (decreasing on 2nd argument)
上で定義した関数について、成り立って欲しい性質を書いてみます。ここでは「全ての自然数 n にたいして pow n 0 = 1 である」というのを書いています。
Coq < Theorem le1: forall n:nat, pow n 0 = 1.
1 subgoal
============================
forall n : nat, pow n 0 = 1
ここで hammer コマンドを使うと裏側でproverが動き、タクティックを組み合わせて現在のゴールを解消するような自動証明をやってくれます。
le1 < hammer.
Replace the hammer tactic with: Reconstr.scrush
No more subgoals.
Restart を使うと hammer コマンドを使う前の状態に戻せます。ここで hammer が導き出したタクティックの組み合わせで証明をやりなおすことができます。
le1 < Restart.
1 subgoal
============================
forall n : nat, pow n 0 = 1
le1 < Reconstr.scrush (** hammer *).
No more subgoals.
le1 < Qed.
le1 is defined
Reconstr.scrushはcoq-hammerが中で持ってるLtacです。
定義をみると (coq-hammerレポジトリの theories/Tactics/Reconstr.v にあります)
Ltac scrush := solve [ yisolve | eauto with yhints | scrush0 ].
みたいな感じで、あまりちゃんと読んでないですが単純化したり書き換えたりをいろいろ試して自動証明(auto)できる形まで持っていこうとしているっぽい。。？ (ん、嬉しいんかこれ。。？)
「なんかわからんけどとりあえず証明できることはわかった！」みたいな状態になりたいときは便利かもしれません。
強者からのツッコミお待ちしています！