Coq 記号

変数/関数定義
Definition 名前 (:型) := 定義. (* 最後ピリオド *)

Definition three : nat := 3.
Definition three' := 3.

:= で定義。

  • 型は省略出来る。(型推論が効く場合)
  • 引数のない関数か、単なる定数の区別が私には出来ません。どっかで出来るの？
    • Definitionの代わりにParameterだと、定義(:=以降)が出来ないのか。どんな風に使うのかは不明。

関数ぽいもの
Definition 名前 引数リスト(:型) (: 戻り値の型) := 定義

Definition f (x: nat) : nat := 3 * x + 1.
Definition f' (x : nat) := 3 * x + 1
Definition f'' : forall (n:nat), nat := fun (x :nat) => 3 * x + 1.
Definition f''' : nat -> nat := fun (x : nat) => 3 * x + 1.
  • 例によって型は省略出来る。
  • natは0を含む自然数を表すCoqの組込み型。
  • forall 。。 は。。型の引数を取る関数の糖衣構文だったっけ。それとも逆で、関数の方がforallの糖衣構文だったっけ。
  • > は他の関数型言語でも良くある、関数の型を宣言するアレ。hoge型引数取ってhuga型を戻すとか。連鎖可能なあれ。
hoge -> huga

=> で関数の本体を定義。=>はパターンマッチでも使うけど、パターンマッチも関数定義みたいなもんなんだろうか？

無名関数は上記の通り
fun 引数リスト(:型) => 本体
引数リストは同じ型なら纏めて書くことが出来る。

fun x y :nat => x + y.

複数の引数を型付きで書くなら括弧が必要になるようだ
fun (X : Type) (x : X) =>...
fun X : Type x : X => ... (* これはエラー *)

一時変数はlet。他の言語でもよく見掛ける気がする。

Eval compute  let x : nat := 3 in x * x.

よく似た記号がいきなり色々出て来るので混乱する。
改めて読んでやっと理解した。すぐ忘れそうな気もするけど。