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
の証明を取る.
つまり、
意味わからん