自然数とリスト: まとめ (3.7)
駆け足でいろいろ紹介しました。
- SearchAbout でライブラリを検索
- 自然数やリストはInductiveなデータ
- = に関する証明 reflexivity, symmetry, transitivity, discriminate
- = を使った書き換え rewrite, replace
- 計算をすすめる simpl, cbv, ...
- 自動証明 omega, ring, field, ring_simplify, field_simplify
- 帰納法 induction
- intro しすぎにご用心。generalize
- 整礎帰納法
- exists
当初の予定では3回くらいにわけるつもりだったんですが、めんどくさくなったので一気に書いてしまうことにしました。駆け足すぎてよくわからなくなってしまってると思いますが、他の入門記事やチュートリアルなどと併用してください(いい加減になってきた…)。ではでは。
追伸
そういえば、このシリーズでは intros や destruct では自分で仮定に名前をつけることはせずに、Coqの自動生成にまかせちゃっているんですが、これって、コーディングスタイルとしては良くないのかもしれません。ということにさっき気づきました。H0 やら H1 やらではよく分からないですよね。本当は、ちゃんと名前をつけて intros 等した方がいいと思います!