quartz-research-note/content/Coqの勉強.md
松浦 知也 Matsuura Tomoya 72368b208c
All checks were successful
Build / build (push) Successful in 1m54s
modified frontmatter depending on timestamp
2024-02-08 18:01:44 +09:00

2.7 KiB
Raw Blame History

date
2023-12-06T20:20:54+09:00

#programming-language #memo #logic

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

備忘録

  • Inductiveが変数宣言
  • Definitionが再帰しない関数宣言
  • Fixpointが再帰関数の宣言
    • 再帰しないとwarningが出る

・・・というのは全部、あくまで普通の関数型言語で考えたら、というので、厳密には全然違う

問題はCoqがラムダキューブ最上位のCalculus of Constructionを採用しているところ。つまり次の全てが扱える

  • 項に依存する項 単純型付ラムダ計算
  • 型に依存する項ジェネリクスSystem F
  • 型に依存する型カインド多相System F \underline{\omega}
  • 型依存の型と型依存の項の両方 System F$\omega$
  • 項に依存する型(依存型) \lambda\Pi
  • 型依存の項と依存型 \lambda\Pi2
  • 型依存の項、項依存の型、型依存の項 CoC

Theoremとかで型を取って型を返す関数とかも当然作れる

inductives are truly "pieces of data"

Inductive natural : Type :=
  | O : natural
  | S : natural -> natural.

自然数を表す型naturalがあったとすると、2のことを表すS(S(O))naturalに属する項だけど、natural型という集合の一部でもある…みたいな話だよな

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