ひとり勉強会

ひとり楽しく勉強会

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