自然数とリスト: まとめ (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 等した方がいいと思います！