#coq #inductive >>112 例えば nat_rectならFixpointでも定義できるよ。 Variable P : nat -> Type. Axiom fO : P O. Axiom fS : forall n, P n -> P (S n). Fixpoint nat_rect' n : P n := match n with | O => fO | S m => fS m (nat_rect' m) end.
nat_rectぐらいなら、数学的帰納法なんてなじみがあるからなんとなくわかるけど、 例えば Inductive sand (A B : Set) : Set := sconj : A -> B -> sand A B. から作られるsand_rectなんかは、
sand_rect = fun (A B : Set) (P : sand A B -> Type) (f : forall (a : A) (b : B), P (sconj A B a b)) (s : sand A B) => match s as s0 return (P s0) with | sconj x x0 => f x x0 end : forall (A B : Set) (P : sand A B -> Type), (forall (a : A) (b : B), P (sconj A B a b)) -> forall s : sand A B, P s
また、pand_rectに関しては、sand_rectの(P : sand A B -> Type)の部分が なぜか(P : Type)になっている。つまりsand_rectにあるPはsand A Bを引数にとってたのに、 pand_rectにあるPはpand A Bを引数にとらなくなっている。 これさえ認めればsand_rectとpand_rectの違いは説明できます。これはなぜなんでしょう？
>>119-121 いろいろと情報提供ありがとうございます。いまはCoq'Artの14章で奮闘中です。もともと英語が苦手 なのですが、贅沢は言ってられません。TAPLって、Benjamin C. Pierceの「Types and Programming Languages」のことですよね。あたってみます。（砕けたりして。トホホ）
Inductive my : Type := O : my . my is defined my_rect is defined my_ind is defined my_rec is defined
は上手く動作するのですが
Coq < Reset my.
Coq < Inductive my : Type := O : my | 1 : my . Toplevel input, characters 32-33: > Inductive my : Type := O : my | 1 : my . > ^ Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).
Coq < Inductive my : Type := O : my | (S O) : my . Toplevel input, characters 32-33: > Inductive my : Type := O : my | (S O) : my . > ^ Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).
