なんとなく生きてます

雑記帳備忘録チラシの裏

Coqの帰納的命題定義の型

ちょっと複雑だったのでメモ.
Coqで帰納的に命題を定義する.
例: 自然数nは自然数m未満である.

Inductive It : nat -> nat -> Prop :=
  | It1 : forall n:nat , (It (S O) (S n))
  | It2 : forall n:nat m:nat , (It n m) -> (It (S n) (S m)).

とする. このとき、

Check It1 2. (*It 1 3型*)
Check It 1 3. (*Prop型*) (*Inductive lt : nat -> nat -> Propで定義してるから当たり前だけど*)
Check It2 1 3. (*It 1 3 -> It 2 4型*)
Check It2 2 4 (It2 1 3 (It1 2)). (*It 3 5型*)

という感じの型をとる.
要はIt n mはProp型だけど、It1, It2は引数にProp型のこれらを取らずに、 It n m型のIt n mの証明を取る.

つまり、











意味わからん