Coq のタクティック、章Polyまでのメモ
(いま書きかけです)
更新の日が開いてしまいましたが、少しずつ Coq は毎日触っています。かなりタクティックが増えてきたので、メモ。まだ説明のないものも問題に出ているので、大分変なことを書いてるかもしれません。
- rewrite
- assert
- destruct
- induction
- symmetry
- unfold
- inversion
ちなみに気分転換に後ろの章を読んでたらCoq の自動化という章があり、高階タクティックや、よく使うタクティックのパターンを定義できるのですね。便利そう。
あとよく、証明の対象として交換則や結合則がでてくるので代数的構造も勉強すると面白いなと思って呼称くらいはきちんと知っておこうと本とか調べたりしてます。ネットだと代数学 - 物理のかぎしっぽが多そうですね。
Coq は関係ありませんが昨日、研究室で数理論理学の本を読んでいたらボスから著書を謹呈して頂きました(ユーモラスな方です)。トピック自体はそこそこ学部のころにやったものですが、人工知能という観点で1階述語論理やホーア論理も触れられていて、中々興味深い本です。