quartz-research-note/content/Coqの勉強.md

1.4 KiB

#programming-language #memo #logic

Coqを用いた定理証明支援の基礎

備忘録

  • Inductiveが変数宣言

  • Definitionが再帰しない関数宣言

  • Fixpointが再帰関数の宣言

    • 再帰しないとwarningが出る
  • 証明したい命題はGoalTheoremLemma

    • Goalは後で再利用されない、最後に証明したいもの
    • TheoremLemmaに違いはない
      • こういうのめんどくさいな
  • Notationって単純な文字列置き換えマクロとして実装されてるのかしら?

  • Coqでは排中律が使えないので、ゴールの論理が論理和$A \cup B$とかの場合$A$か$B$のどちらかを証明するかを決めるしかない