帰納的述語をどのように説明しますか? それらは何に使用されますか？それらの背後にある理論は何ですか？それらは依存型システムにのみ存在しますか、それとも他のシステムにも存在しますか? それらは何らかの形で GADT に関連していますか? Coqでデフォルトでtrueになっているのはなぜですか?
これは Coq の例です。
Inductive even : nat -> Prop :=
| even0 : even 0
| evens : forall p:nat, even p -> even (S (S P))
この定義をどのように使用しますか? それはデータ型ですか、それとも命題ですか？
帰納的に定義され、Prop.
それらは帰納的にプロパティを定義するために使用されます（当然）。背後にある理論は、おそらく帰納的構造の文献で見つけることができます。たとえば、CIC (誘導構造の微積分) に関する論文を検索します。
これらは GADT に多少関連していますが、従属型を使用すると、より多くのことを表現できます。私が間違っていなければ、GADT では各コンストラクターが 1 つの特定のファミリーに存在しますが、依存型を追加すると、コンストラクターは引数に基づいて異なるファミリーに存在できます。
「Coqではデフォルトで真」というのが何を意味するのかわかりません。
evenあなたが定義するように、それは帰納的なデータ型です。タイプが示すように、これはまだ命題ではありませんnat -> Prop。命題はeven 0またはになりeven 1ます。のように居住 (証明可能) することも、 のように居住しないこともできeven 0ますeven 1。